Metamath Proof Explorer

Theorem rngohomadd

Description: Ring homomorphisms preserve addition. (Contributed by Jeff Madsen, 3-Jan-2011)

Ref Expression
Hypotheses rnghomadd.1 
|- G = ( 1st ` R )
rnghomadd.2 
|- X = ran G
rnghomadd.3 
|- J = ( 1st ` S )
Assertion rngohomadd 
|- ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) /\ ( A e. X /\ B e. X ) ) -> ( F ` ( A G B ) ) = ( ( F ` A ) J ( F ` B ) ) )

Proof

Step Hyp Ref Expression
1 rnghomadd.1 
 |-  G = ( 1st ` R )
2 rnghomadd.2 
 |-  X = ran G
3 rnghomadd.3 
 |-  J = ( 1st ` S )
4 eqid 
 |-  ( 2nd ` R ) = ( 2nd ` R )
5 eqid 
 |-  ( GId ` ( 2nd ` R ) ) = ( GId ` ( 2nd ` R ) )
6 eqid 
 |-  ( 2nd ` S ) = ( 2nd ` S )
7 eqid 
 |-  ran J = ran J
8 eqid 
 |-  ( GId ` ( 2nd ` S ) ) = ( GId ` ( 2nd ` S ) )
9 1 4 2 5 3 6 7 8 isrngohom 
 |-  ( ( R e. RingOps /\ S e. RingOps ) -> ( F e. ( R RngHom S ) <-> ( F : X --> ran J /\ ( F ` ( GId ` ( 2nd ` R ) ) ) = ( GId ` ( 2nd ` S ) ) /\ A. x e. X A. y e. X ( ( F ` ( x G y ) ) = ( ( F ` x ) J ( F ` y ) ) /\ ( F ` ( x ( 2nd ` R ) y ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) ) ) )
10 9 biimpa 
 |-  ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RngHom S ) ) -> ( F : X --> ran J /\ ( F ` ( GId ` ( 2nd ` R ) ) ) = ( GId ` ( 2nd ` S ) ) /\ A. x e. X A. y e. X ( ( F ` ( x G y ) ) = ( ( F ` x ) J ( F ` y ) ) /\ ( F ` ( x ( 2nd ` R ) y ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) ) )
11 10 simp3d 
 |-  ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RngHom S ) ) -> A. x e. X A. y e. X ( ( F ` ( x G y ) ) = ( ( F ` x ) J ( F ` y ) ) /\ ( F ` ( x ( 2nd ` R ) y ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) )
12 11 3impa 
 |-  ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) -> A. x e. X A. y e. X ( ( F ` ( x G y ) ) = ( ( F ` x ) J ( F ` y ) ) /\ ( F ` ( x ( 2nd ` R ) y ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) )
13 simpl 
 |-  ( ( ( F ` ( x G y ) ) = ( ( F ` x ) J ( F ` y ) ) /\ ( F ` ( x ( 2nd ` R ) y ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) -> ( F ` ( x G y ) ) = ( ( F ` x ) J ( F ` y ) ) )
14 13 2ralimi 
 |-  ( A. x e. X A. y e. X ( ( F ` ( x G y ) ) = ( ( F ` x ) J ( F ` y ) ) /\ ( F ` ( x ( 2nd ` R ) y ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) -> A. x e. X A. y e. X ( F ` ( x G y ) ) = ( ( F ` x ) J ( F ` y ) ) )
15 12 14 syl 
 |-  ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) -> A. x e. X A. y e. X ( F ` ( x G y ) ) = ( ( F ` x ) J ( F ` y ) ) )
16 fvoveq1 
 |-  ( x = A -> ( F ` ( x G y ) ) = ( F ` ( A G y ) ) )
17 fveq2 
 |-  ( x = A -> ( F ` x ) = ( F ` A ) )
18 17 oveq1d 
 |-  ( x = A -> ( ( F ` x ) J ( F ` y ) ) = ( ( F ` A ) J ( F ` y ) ) )
19 16 18 eqeq12d 
 |-  ( x = A -> ( ( F ` ( x G y ) ) = ( ( F ` x ) J ( F ` y ) ) <-> ( F ` ( A G y ) ) = ( ( F ` A ) J ( F ` y ) ) ) )
20 oveq2 
 |-  ( y = B -> ( A G y ) = ( A G B ) )
21 20 fveq2d 
 |-  ( y = B -> ( F ` ( A G y ) ) = ( F ` ( A G B ) ) )
22 fveq2 
 |-  ( y = B -> ( F ` y ) = ( F ` B ) )
23 22 oveq2d 
 |-  ( y = B -> ( ( F ` A ) J ( F ` y ) ) = ( ( F ` A ) J ( F ` B ) ) )
24 21 23 eqeq12d 
 |-  ( y = B -> ( ( F ` ( A G y ) ) = ( ( F ` A ) J ( F ` y ) ) <-> ( F ` ( A G B ) ) = ( ( F ` A ) J ( F ` B ) ) ) )
25 19 24 rspc2v 
 |-  ( ( A e. X /\ B e. X ) -> ( A. x e. X A. y e. X ( F ` ( x G y ) ) = ( ( F ` x ) J ( F ` y ) ) -> ( F ` ( A G B ) ) = ( ( F ` A ) J ( F ` B ) ) ) )
26 15 25 mpan9 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) /\ ( A e. X /\ B e. X ) ) -> ( F ` ( A G B ) ) = ( ( F ` A ) J ( F ` B ) ) )