Theorem gicqusker

Description: The image H of a group homomorphism F is isomorphic with the quotient group Q over F 's kernel K . Together with ghmker and ghmima , this is sometimes called the first isomorphism theorem for groups. (Contributed by Thierry Arnoux, 10-Mar-2025)

	Ref	Expression
Hypotheses	gicqusker.1	|- .0. = ( 0g ` H )
	gicqusker.f	|- ( ph -> F e. ( G GrpHom H ) )
	gicqusker.k	|- K = ( `' F " { .0. } )
	gicqusker.q	|- Q = ( G /s ( G ~QG K ) )
	gicqusker.s	|- ( ph -> ran F = ( Base ` H ) )
Assertion	gicqusker	|- ( ph -> Q ~=g H )

Proof

Step	Hyp	Ref	Expression
1		gicqusker.1	|- .0. = ( 0g ` H )
2		gicqusker.f	|- ( ph -> F e. ( G GrpHom H ) )
3		gicqusker.k	|- K = ( `' F " { .0. } )
4		gicqusker.q	|- Q = ( G /s ( G ~QG K ) )
5		gicqusker.s	|- ( ph -> ran F = ( Base ` H ) )
6		imaeq2	|- ( p = q -> ( F " p ) = ( F " q ) )
7	6	unieqd	|- ( p = q -> U. ( F " p ) = U. ( F " q ) )
8	7	cbvmptv	|- ( p e. ( Base ` Q ) |-> U. ( F " p ) ) = ( q e. ( Base ` Q ) |-> U. ( F " q ) )
9	1 2 3 4 8 5	ghmqusker	|- ( ph -> ( p e. ( Base ` Q ) |-> U. ( F " p ) ) e. ( Q GrpIso H ) )
10		brgici	|- ( ( p e. ( Base ` Q ) |-> U. ( F " p ) ) e. ( Q GrpIso H ) -> Q ~=g H )
11	9 10	syl	|- ( ph -> Q ~=g H )