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 RngHom 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 RngHom 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 RngHom 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 RngHom 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 RngHom 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 RngHom 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 RngHom S ) ) /\ ( A e. X /\ B e. X ) ) -> ( F ` ( A H B ) ) = ( ( F ` A ) K ( F ` B ) ) )