Metamath Proof Explorer

Theorem rngohom1

Description: A ring homomorphism preserves 1 . (Contributed by Jeff Madsen, 24-Jun-2011)

Ref Expression
Hypotheses rnghom1.1 
|- H = ( 2nd ` R )
rnghom1.2 
|- U = ( GId ` H )
rnghom1.3 
|- K = ( 2nd ` S )
rnghom1.4 
|- V = ( GId ` K )
Assertion rngohom1 
|- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> ( F ` U ) = V )

Proof

Step Hyp Ref Expression
1 rnghom1.1 
 |-  H = ( 2nd ` R )
2 rnghom1.2 
 |-  U = ( GId ` H )
3 rnghom1.3 
 |-  K = ( 2nd ` S )
4 rnghom1.4 
 |-  V = ( GId ` K )
5 eqid 
 |-  ( 1st ` R ) = ( 1st ` R )
6 eqid 
 |-  ran ( 1st ` R ) = ran ( 1st ` R )
7 eqid 
 |-  ( 1st ` S ) = ( 1st ` S )
8 eqid 
 |-  ran ( 1st ` S ) = ran ( 1st ` S )
9 5 1 6 2 7 3 8 4 isrngohom 
 |-  ( ( R e. RingOps /\ S e. RingOps ) -> ( F e. ( R RingOpsHom S ) <-> ( F : ran ( 1st ` R ) --> ran ( 1st ` S ) /\ ( F ` U ) = V /\ A. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) ( ( F ` ( x ( 1st ` R ) y ) ) = ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) /\ ( F ` ( x H y ) ) = ( ( F ` x ) K ( F ` y ) ) ) ) ) )
10 9 biimpa 
 |-  ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> ( F : ran ( 1st ` R ) --> ran ( 1st ` S ) /\ ( F ` U ) = V /\ A. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) ( ( F ` ( x ( 1st ` R ) y ) ) = ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) /\ ( F ` ( x H y ) ) = ( ( F ` x ) K ( F ` y ) ) ) ) )
11 10 simp2d 
 |-  ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> ( F ` U ) = V )
12 11 3impa 
 |-  ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> ( F ` U ) = V )