This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ 𝐹 ∈ ( 𝑅 RingOpsHom 𝑆 ) ) → ( 𝐹 ‘ 𝑍 ) = 𝑊 )

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 ∧ 𝐹 ∈ ( 𝑅 RingOpsHom 𝑆 ) ) → 𝐺 ∈ GrpOp )
7 3 rngogrpo ⊢ ( 𝑆 ∈ RingOps → 𝐽 ∈ GrpOp )
8 7 3ad2ant2 ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RingOpsHom 𝑆 ) ) → 𝐽 ∈ GrpOp )
9 1 3 rngogrphom ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RingOpsHom 𝑆 ) ) → 𝐹 ∈ ( 𝐺 GrpOpHom 𝐽 ) )
10 2 4 ghomidOLD ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐽 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐽 ) ) → ( 𝐹 ‘ 𝑍 ) = 𝑊 )
11 6 8 9 10 syl3anc ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RingOpsHom 𝑆 ) ) → ( 𝐹 ‘ 𝑍 ) = 𝑊 )