Metamath Proof Explorer

Theorem rngohom0

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

Ref Expression
Hypotheses rnghom0.1 
|- G = ( 1st ` R )
rnghom0.2 
|- Z = ( GId ` G )
rnghom0.3 
|- J = ( 1st ` S )
rnghom0.4 
|- W = ( GId ` J )
Assertion rngohom0 
|- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) -> ( F ` Z ) = W )

Proof

Step Hyp Ref Expression
1 rnghom0.1 
 |-  G = ( 1st ` R )
2 rnghom0.2 
 |-  Z = ( GId ` G )
3 rnghom0.3 
 |-  J = ( 1st ` S )
4 rnghom0.4 
 |-  W = ( GId ` J )
5 1 rngogrpo 
 |-  ( R e. RingOps -> G e. GrpOp )
6 5 3ad2ant1 
 |-  ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) -> G e. GrpOp )
7 3 rngogrpo 
 |-  ( S e. RingOps -> J e. GrpOp )
8 7 3ad2ant2 
 |-  ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) -> J e. GrpOp )
9 1 3 rngogrphom 
 |-  ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) -> F e. ( G GrpOpHom J ) )
10 2 4 ghomidOLD 
 |-  ( ( G e. GrpOp /\ J e. GrpOp /\ F e. ( G GrpOpHom J ) ) -> ( F ` Z ) = W )
11 6 8 9 10 syl3anc 
 |-  ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) -> ( F ` Z ) = W )