Theorem rngokerinj

Description: Obsolete theorem, use rhmkerinj instead. A ring homomorphism is injective if and only if its kernel is zero. (Contributed by Jeff Madsen, 16-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	rngkerinj.1	$$⊢G=1^{st}\left(R\right)$$
	rngkerinj.2	$$⊢X=\mathrm{ran}G$$
	rngkerinj.3	$$⊢W=\mathrm{GId}\left(G\right)$$
	rngkerinj.4	$$⊢J=1^{st}\left(S\right)$$
	rngkerinj.5	$$⊢Y=\mathrm{ran}J$$
	rngkerinj.6	$$⊢Z=\mathrm{GId}\left(J\right)$$
Assertion	rngokerinj	$$⊢\left(R\in \mathrm{RingOps}\wedge S\in \mathrm{RingOps}\wedge F\in \left(R\mathrm{RingOpsHom}S\right)\right)\to \left(F:X\underset{1-1}{⟶}Y\leftrightarrow F^{-1}\left[\left\{Z\right\}\right]=\left\{W\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		rngkerinj.1	$$⊢G=1^{st}\left(R\right)$$
2		rngkerinj.2	$$⊢X=\mathrm{ran}G$$
3		rngkerinj.3	$$⊢W=\mathrm{GId}\left(G\right)$$
4		rngkerinj.4	$$⊢J=1^{st}\left(S\right)$$
5		rngkerinj.5	$$⊢Y=\mathrm{ran}J$$
6		rngkerinj.6	$$⊢Z=\mathrm{GId}\left(J\right)$$
7		eqid	$$⊢1^{st}\left(R\right)=1^{st}\left(R\right)$$
8	7	rngogrpo	$$⊢R\in \mathrm{RingOps}\to 1^{st}\left(R\right)\in \mathrm{GrpOp}$$
9	8	3ad2ant1	$$⊢\left(R\in \mathrm{RingOps}\wedge S\in \mathrm{RingOps}\wedge F\in \left(R\mathrm{RingOpsHom}S\right)\right)\to 1^{st}\left(R\right)\in \mathrm{GrpOp}$$
10		eqid	$$⊢1^{st}\left(S\right)=1^{st}\left(S\right)$$
11	10	rngogrpo	$$⊢S\in \mathrm{RingOps}\to 1^{st}\left(S\right)\in \mathrm{GrpOp}$$
12	11	3ad2ant2	$$⊢\left(R\in \mathrm{RingOps}\wedge S\in \mathrm{RingOps}\wedge F\in \left(R\mathrm{RingOpsHom}S\right)\right)\to 1^{st}\left(S\right)\in \mathrm{GrpOp}$$
13	7 10	rngogrphom	$$⊢\left(R\in \mathrm{RingOps}\wedge S\in \mathrm{RingOps}\wedge F\in \left(R\mathrm{RingOpsHom}S\right)\right)\to F\in \left(1^{st}\left(R\right)\mathrm{GrpOpHom}{1}^{st}\left(S\right)\right)$$
14	1	rneqi	$$⊢\mathrm{ran}G=\mathrm{ran}{1}^{st}\left(R\right)$$
15	2 14	eqtri	$$⊢X=\mathrm{ran}{1}^{st}\left(R\right)$$
16	1	fveq2i	$$⊢\mathrm{GId}\left(G\right)=\mathrm{GId}\left(1^{st}\left(R\right)\right)$$
17	3 16	eqtri	$$⊢W=\mathrm{GId}\left(1^{st}\left(R\right)\right)$$
18	4	rneqi	$$⊢\mathrm{ran}J=\mathrm{ran}{1}^{st}\left(S\right)$$
19	5 18	eqtri	$$⊢Y=\mathrm{ran}{1}^{st}\left(S\right)$$
20	4	fveq2i	$$⊢\mathrm{GId}\left(J\right)=\mathrm{GId}\left(1^{st}\left(S\right)\right)$$
21	6 20	eqtri	$$⊢Z=\mathrm{GId}\left(1^{st}\left(S\right)\right)$$
22	15 17 19 21	grpokerinj	$$⊢\left(1^{st}\left(R\right)\in \mathrm{GrpOp}\wedge 1^{st}\left(S\right)\in \mathrm{GrpOp}\wedge F\in \left(1^{st}\left(R\right)\mathrm{GrpOpHom}{1}^{st}\left(S\right)\right)\right)\to \left(F:X\underset{1-1}{⟶}Y\leftrightarrow F^{-1}\left[\left\{Z\right\}\right]=\left\{W\right\}\right)$$
23	9 12 13 22	syl3anc	$$⊢\left(R\in \mathrm{RingOps}\wedge S\in \mathrm{RingOps}\wedge F\in \left(R\mathrm{RingOpsHom}S\right)\right)\to \left(F:X\underset{1-1}{⟶}Y\leftrightarrow F^{-1}\left[\left\{Z\right\}\right]=\left\{W\right\}\right)$$