Metamath Proof Explorer

Theorem rngohommul

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

Ref Expression
Hypotheses rnghommul.1 
|- G = ( 1st ` R )
rnghommul.2 
|- X = ran G
rnghommul.3 
|- H = ( 2nd ` R )
rnghommul.4 
|- K = ( 2nd ` S )
Assertion rngohommul 
|- ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( A e. X /\ B e. X ) ) -> ( F ` ( A H B ) ) = ( ( F ` A ) K ( F ` B ) ) )

Proof

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