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 RngHom 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 RngHom 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 RngHom 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 RngHom S ) ) -> ( F ` U ) = V )
12 11 3impa
 |-  ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) -> ( F ` U ) = V )