Theorem rngokerinj

Description: A ring homomorphism is injective if and only if its kernel is zero. (Contributed by Jeff Madsen, 16-Jun-2011)

	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	Could not format assertion : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> ( F : X -1-1-> Y <-> ( `' F " { Z } ) = { W } ) ) with typecode |-

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	Could not format ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> ( 1st ` R ) e. GrpOp ) : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> ( 1st ` R ) e. GrpOp ) with typecode |-
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	Could not format ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> ( 1st ` S ) e. GrpOp ) : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> ( 1st ` S ) e. GrpOp ) with typecode |-
13	7 10	rngogrphom	Could not format ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> F e. ( ( 1st ` R ) GrpOpHom ( 1st ` S ) ) ) : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> F e. ( ( 1st ` R ) GrpOpHom ( 1st ` S ) ) ) with typecode |-
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	Could not format ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> ( F : X -1-1-> Y <-> ( `' F " { Z } ) = { W } ) ) : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> ( F : X -1-1-> Y <-> ( `' F " { Z } ) = { W } ) ) with typecode |-