Theorem rngohom0

Description: A ring homomorphism preserves 0 . (Contributed by Jeff Madsen, 2-Jan-2011)

	Ref	Expression
Hypotheses	rnghom0.1	⊢ 𝐺 = ( 1st ‘ 𝑅 )
	rnghom0.2	⊢ 𝑍 = ( GId ‘ 𝐺 )
	rnghom0.3	⊢ 𝐽 = ( 1st ‘ 𝑆 )
	rnghom0.4	⊢ 𝑊 = ( GId ‘ 𝐽 )
Assertion	rngohom0	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) → ( 𝐹 ‘ 𝑍 ) = 𝑊 )

Proof

Step	Hyp	Ref	Expression
1		rnghom0.1	⊢ 𝐺 = ( 1st ‘ 𝑅 )
2		rnghom0.2	⊢ 𝑍 = ( GId ‘ 𝐺 )
3		rnghom0.3	⊢ 𝐽 = ( 1st ‘ 𝑆 )
4		rnghom0.4	⊢ 𝑊 = ( GId ‘ 𝐽 )
5	1	rngogrpo	⊢ ( 𝑅 ∈ RingOps → 𝐺 ∈ GrpOp )
6	5	3ad2ant1	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) → 𝐺 ∈ GrpOp )
7	3	rngogrpo	⊢ ( 𝑆 ∈ RingOps → 𝐽 ∈ GrpOp )
8	7	3ad2ant2	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) → 𝐽 ∈ GrpOp )
9	1 3	rngogrphom	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) → 𝐹 ∈ ( 𝐺 GrpOpHom 𝐽 ) )
10	2 4	ghomidOLD	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐽 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐽 ) ) → ( 𝐹 ‘ 𝑍 ) = 𝑊 )
11	6 8 9 10	syl3anc	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) → ( 𝐹 ‘ 𝑍 ) = 𝑊 )