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	⊢ ( 𝜑 → 𝑄 ≃𝑟 𝐻 )