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

Proof

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