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

Metamath Proof Explorer

Theorem ricqusker

Description: The image H of a ring homomorphism F is isomorphic with the quotient ring Q over F 's kernel K . This a part of what is sometimes called the first isomorphism theorem for rings. (Contributed by Thierry Arnoux, 10-Mar-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 )
Assertion ricqusker ( 𝜑 → 𝑄 ≃𝑟 𝐻 )

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 imaeq2 ⊢ ( 𝑝 = 𝑞 → ( 𝐹 “ 𝑝 ) = ( 𝐹 “ 𝑞 ) )
8 7 unieqd ⊢ ( 𝑝 = 𝑞 → ∪ ( 𝐹 “ 𝑝 ) = ∪ ( 𝐹 “ 𝑞 ) )
9 8 cbvmptv ⊢ ( 𝑝 ∈ ( Base ‘ 𝑄 ) ↦ ∪ ( 𝐹 “ 𝑝 ) ) = ( 𝑞 ∈ ( Base ‘ 𝑄 ) ↦ ∪ ( 𝐹 “ 𝑞 ) )
10 1 2 3 4 5 6 9 rhmqusker ⊢ ( 𝜑 → ( 𝑝 ∈ ( Base ‘ 𝑄 ) ↦ ∪ ( 𝐹 “ 𝑝 ) ) ∈ ( 𝑄 RingIso 𝐻 ) )
11 brrici ⊢ ( ( 𝑝 ∈ ( Base ‘ 𝑄 ) ↦ ∪ ( 𝐹 “ 𝑝 ) ) ∈ ( 𝑄 RingIso 𝐻 ) → 𝑄 ≃𝑟 𝐻 )
12 10 11 syl ⊢ ( 𝜑 → 𝑄 ≃𝑟 𝐻 )