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

Proof

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

Metamath Proof Explorer

Theorem rngokerinj

Proof