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	$⊢ \underset{˙}{0} = 0_{H}$
		rhmqusker.f	$⊢ φ \to F \in (G RingHom H)$
		rhmqusker.k	$⊢ K = F^{-1} [\{\underset{˙}{0}\}]$
		rhmqusker.q	$⊢ Q = G /_{𝑠} (G ~_{QG} K)$
		rhmqusker.s	$⊢ φ \to ran F = {Base}_{H}$
		rhmqusker.2	$⊢ φ \to G \in CRing$
	Assertion	ricqusker	$⊢ φ \to Q ≃_{𝑟} H$

Proof

Step	Hyp	Ref	Expression
1		rhmqusker.1	$⊢ \underset{˙}{0} = 0_{H}$
2		rhmqusker.f	$⊢ φ \to F \in (G RingHom H)$
3		rhmqusker.k	$⊢ K = F^{-1} [\{\underset{˙}{0}\}]$
4		rhmqusker.q	$⊢ Q = G /_{𝑠} (G ~_{QG} K)$
5		rhmqusker.s	$⊢ φ \to ran F = {Base}_{H}$
6		rhmqusker.2	$⊢ φ \to G \in CRing$
7		imaeq2	$⊢ p = q \to F [p] = F [q]$
8	7	unieqd	$⊢ p = q \to ⋃ F [p] = ⋃ F [q]$
9	8	cbvmptv	$⊢ (p \in {Base}_{Q} ⟼ ⋃ F [p]) = (q \in {Base}_{Q} ⟼ ⋃ F [q])$
10	1 2 3 4 5 6 9	rhmqusker	$⊢ φ \to (p \in {Base}_{Q} ⟼ ⋃ F [p]) \in (Q RingIso H)$
11		brrici	$⊢ (p \in {Base}_{Q} ⟼ ⋃ F [p]) \in (Q RingIso H) \to Q ≃_{𝑟} H$
12	10 11	syl	$⊢ φ \to Q ≃_{𝑟} H$