Theorem rhmqusker

Description: A surjective ring homomorphism F from G to H induces an isomorphism J from Q to H , where Q is the factor group of G by F 's kernel K . (Contributed by Thierry Arnoux, 25-Feb-2025)

	Ref	Expression
Hypotheses	rhmqusker.1	|- .0. = ( 0g ` H )
	rhmqusker.f	|- ( ph -> F e. ( G RingHom H ) )
	rhmqusker.k	|- K = ( `' F " { .0. } )
	rhmqusker.q	|- Q = ( G /s ( G ~QG K ) )
	rhmqusker.s	|- ( ph -> ran F = ( Base ` H ) )
	rhmqusker.2	|- ( ph -> G e. CRing )
	rhmqusker.j	|- J = ( q e. ( Base ` Q ) |-> U. ( F " q ) )
Assertion	rhmqusker	|- ( ph -> J e. ( Q RingIso H ) )

Proof

Step	Hyp	Ref	Expression
1		rhmqusker.1	|- .0. = ( 0g ` H )
2		rhmqusker.f	|- ( ph -> F e. ( G RingHom H ) )
3		rhmqusker.k	|- K = ( `' F " { .0. } )
4		rhmqusker.q	|- Q = ( G /s ( G ~QG K ) )
5		rhmqusker.s	|- ( ph -> ran F = ( Base ` H ) )
6		rhmqusker.2	|- ( ph -> G e. CRing )
7		rhmqusker.j	|- J = ( q e. ( Base ` Q ) |-> U. ( F " q ) )
8	1 2 3 4 7 6	rhmquskerlem	|- ( ph -> J e. ( Q RingHom H ) )
9		rhmghm	|- ( F e. ( G RingHom H ) -> F e. ( G GrpHom H ) )
10	2 9	syl	|- ( ph -> F e. ( G GrpHom H ) )
11	1 10 3 4 7 5	ghmqusker	|- ( ph -> J e. ( Q GrpIso H ) )
12		eqid	|- ( Base ` Q ) = ( Base ` Q )
13		eqid	|- ( Base ` H ) = ( Base ` H )
14	12 13	gimf1o	|- ( J e. ( Q GrpIso H ) -> J : ( Base ` Q ) -1-1-onto-> ( Base ` H ) )
15	11 14	syl	|- ( ph -> J : ( Base ` Q ) -1-1-onto-> ( Base ` H ) )
16	12 13	isrim	|- ( J e. ( Q RingIso H ) <-> ( J e. ( Q RingHom H ) /\ J : ( Base ` Q ) -1-1-onto-> ( Base ` H ) ) )
17	8 15 16	sylanbrc	|- ( ph -> J e. ( Q RingIso H ) )