Metamath Proof Explorer


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 𝐺 = ( 1st𝑅 )
rngkerinj.2 𝑋 = ran 𝐺
rngkerinj.3 𝑊 = ( GId ‘ 𝐺 )
rngkerinj.4 𝐽 = ( 1st𝑆 )
rngkerinj.5 𝑌 = ran 𝐽
rngkerinj.6 𝑍 = ( GId ‘ 𝐽 )
Assertion rngokerinj ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) → ( 𝐹 : 𝑋1-1𝑌 ↔ ( 𝐹 “ { 𝑍 } ) = { 𝑊 } ) )

Proof

Step Hyp Ref Expression
1 rngkerinj.1 𝐺 = ( 1st𝑅 )
2 rngkerinj.2 𝑋 = ran 𝐺
3 rngkerinj.3 𝑊 = ( GId ‘ 𝐺 )
4 rngkerinj.4 𝐽 = ( 1st𝑆 )
5 rngkerinj.5 𝑌 = ran 𝐽
6 rngkerinj.6 𝑍 = ( GId ‘ 𝐽 )
7 eqid ( 1st𝑅 ) = ( 1st𝑅 )
8 7 rngogrpo ( 𝑅 ∈ RingOps → ( 1st𝑅 ) ∈ GrpOp )
9 8 3ad2ant1 ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) → ( 1st𝑅 ) ∈ GrpOp )
10 eqid ( 1st𝑆 ) = ( 1st𝑆 )
11 10 rngogrpo ( 𝑆 ∈ RingOps → ( 1st𝑆 ) ∈ GrpOp )
12 11 3ad2ant2 ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) → ( 1st𝑆 ) ∈ GrpOp )
13 7 10 rngogrphom ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) → 𝐹 ∈ ( ( 1st𝑅 ) GrpOpHom ( 1st𝑆 ) ) )
14 1 rneqi ran 𝐺 = ran ( 1st𝑅 )
15 2 14 eqtri 𝑋 = ran ( 1st𝑅 )
16 1 fveq2i ( GId ‘ 𝐺 ) = ( GId ‘ ( 1st𝑅 ) )
17 3 16 eqtri 𝑊 = ( GId ‘ ( 1st𝑅 ) )
18 4 rneqi ran 𝐽 = ran ( 1st𝑆 )
19 5 18 eqtri 𝑌 = ran ( 1st𝑆 )
20 4 fveq2i ( GId ‘ 𝐽 ) = ( GId ‘ ( 1st𝑆 ) )
21 6 20 eqtri 𝑍 = ( GId ‘ ( 1st𝑆 ) )
22 15 17 19 21 grpokerinj ( ( ( 1st𝑅 ) ∈ GrpOp ∧ ( 1st𝑆 ) ∈ GrpOp ∧ 𝐹 ∈ ( ( 1st𝑅 ) GrpOpHom ( 1st𝑆 ) ) ) → ( 𝐹 : 𝑋1-1𝑌 ↔ ( 𝐹 “ { 𝑍 } ) = { 𝑊 } ) )
23 9 12 13 22 syl3anc ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) → ( 𝐹 : 𝑋1-1𝑌 ↔ ( 𝐹 “ { 𝑍 } ) = { 𝑊 } ) )