This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐻 ) )