Proof of The First Isomorphism Theorem

Routine facts about restrictions of binary operations are used without comment (Toolkit for AL1).

The whole proof rests on one observation: two elements of $G$ lie in the same coset of $K$ exactly when $f$ takes the same value at them. For $g,h\in G$,

$$gK=hK\iff g^{-1}h\in K\iff f(g^{-1}h)=e_H\iff f(g)^{-1}f(h)=e_H\iff f(g)=f(h).$$

The first equivalence is Left Cosets Partition a Group and All Have the Same Cardinality (ii) and the second is the definition of the kernel (Kernel and Image of a Group Homomorphism (i)). The third holds because $f$ preserves products (Group Homomorphisms and Isomorphisms (i)) and inverses (Group Homomorphisms Preserve the Identity Element and Inverses (ii)), so that $f(g^{-1}h)=f(g)^{-1}f(h)$, and the last is Cancellation Laws and Basic Inverse Identities in a Group (v).

Consider the class $\bar f=\{(gK,f(g)):g\in G\}$. If $gK=hK$, then $f(g)=f(h)$ by the chain of equivalences above, read from left to right, so $\bar f$ is single-valued. Its domain is $G/K$, since every element of $G/K$ is a coset $gK$ (Cosets and the Index of a Subgroup (iii)), and its values lie in $f(G)$ (Kernel and Image of a Group Homomorphism (ii)). Hence $\bar f$ is a function from $G/K$ to $f(G)$ (Functions, Values of a Function, and Functions from One Class to Another (iii)) with $\bar f(gK)=f(g)$ for every $g\in G$. Any other function with these values agrees with $\bar f$ at every element of $G/K$, each element being some $gK$, and so equals $\bar f$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (i). This proves existence and uniqueness.

The product in $G/K$ is the product of cosets of The Product of Cosets of a Normal Subgroup Is Well Defined and Makes the Cosets a Group (i), as fixed by Quotient Groups (i), and $f(G)$ carries the restriction of the operation of $H$ (Subgroup Criterion and Basic Examples (ii)). For $g,h\in G$ therefore

$$\bar f\bigl((gK)(hK)\bigr)=\bar f\bigl((gh)K\bigr)=f(gh)=f(g)f(h)=\bar f(gK)\,\bar f(hK),$$

so $\bar f$ is a group homomorphism (Group Homomorphisms and Isomorphisms (i)).

It remains to show that $\bar f$ is bijective. It is surjective (Injective, Surjective and Bijective Functions between Classes (ii)), because every element of $f(G)$ has the form $f(g)=\bar f(gK)$ for some $g\in G$ (Kernel and Image of a Group Homomorphism (ii)). It is injective (Injective, Surjective and Bijective Functions between Classes (i)): if $\bar f(gK)=\bar f(hK)$, then $f(g)=f(h)$, and hence $gK=hK$ by the chain of equivalences above, read from right to left. So $\bar f$ is bijective (Injective, Surjective and Bijective Functions between Classes (iii)), and therefore a group isomorphism by Group Homomorphisms and Isomorphisms (ii). This proves (i).