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 ‘ 𝐻 )
	rhmqusker.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 RingHom 𝐻 ) )
	rhmqusker.k	⊢ 𝐾 = ( ◡ 𝐹 “ { 0 } )
	rhmqusker.q	⊢ 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝐾 ) )
	rhmqusker.s	⊢ ( 𝜑 → ran 𝐹 = ( Base ‘ 𝐻 ) )
	rhmqusker.2	⊢ ( 𝜑 → 𝐺 ∈ CRing )
	rhmqusker.j	⊢ 𝐽 = ( 𝑞 ∈ ( Base ‘ 𝑄 ) ↦ ∪ ( 𝐹 “ 𝑞 ) )
Assertion	rhmqusker	⊢ ( 𝜑 → 𝐽 ∈ ( 𝑄 RingIso 𝐻 ) )

Proof

Step	Hyp	Ref	Expression
1		rhmqusker.1	⊢ 0 = ( 0g ‘ 𝐻 )
2		rhmqusker.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 RingHom 𝐻 ) )
3		rhmqusker.k	⊢ 𝐾 = ( ◡ 𝐹 “ { 0 } )
4		rhmqusker.q	⊢ 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝐾 ) )
5		rhmqusker.s	⊢ ( 𝜑 → ran 𝐹 = ( Base ‘ 𝐻 ) )
6		rhmqusker.2	⊢ ( 𝜑 → 𝐺 ∈ CRing )
7		rhmqusker.j	⊢ 𝐽 = ( 𝑞 ∈ ( Base ‘ 𝑄 ) ↦ ∪ ( 𝐹 “ 𝑞 ) )
8	1 2 3 4 7 6	rhmquskerlem	⊢ ( 𝜑 → 𝐽 ∈ ( 𝑄 RingHom 𝐻 ) )
9		rhmghm	⊢ ( 𝐹 ∈ ( 𝐺 RingHom 𝐻 ) → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )
10	2 9	syl	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )
11	1 10 3 4 7 5	ghmqusker	⊢ ( 𝜑 → 𝐽 ∈ ( 𝑄 GrpIso 𝐻 ) )
12		eqid	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
13		eqid	⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
14	12 13	gimf1o	⊢ ( 𝐽 ∈ ( 𝑄 GrpIso 𝐻 ) → 𝐽 : ( Base ‘ 𝑄 ) –1-1-onto→ ( Base ‘ 𝐻 ) )
15	11 14	syl	⊢ ( 𝜑 → 𝐽 : ( Base ‘ 𝑄 ) –1-1-onto→ ( Base ‘ 𝐻 ) )
16	12 13	isrim	⊢ ( 𝐽 ∈ ( 𝑄 RingIso 𝐻 ) ↔ ( 𝐽 ∈ ( 𝑄 RingHom 𝐻 ) ∧ 𝐽 : ( Base ‘ 𝑄 ) –1-1-onto→ ( Base ‘ 𝐻 ) ) )
17	8 15 16	sylanbrc	⊢ ( 𝜑 → 𝐽 ∈ ( 𝑄 RingIso 𝐻 ) )