Metamath Proof Explorer


Theorem rngohommul

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

Ref Expression
Hypotheses rnghommul.1 G = 1 st R
rnghommul.2 X = ran G
rnghommul.3 H = 2 nd R
rnghommul.4 K = 2 nd S
Assertion rngohommul Could not format assertion : No typesetting found for |- ( ( ( 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 ) ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 rnghommul.1 G = 1 st R
2 rnghommul.2 X = ran G
3 rnghommul.3 H = 2 nd R
4 rnghommul.4 K = 2 nd S
5 eqid GId H = GId H
6 eqid 1 st S = 1 st S
7 eqid ran 1 st S = ran 1 st S
8 eqid GId K = GId K
9 1 3 2 5 6 4 7 8 isrngohom Could not format ( ( 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 ) ) ) ) ) ) : No typesetting found for |- ( ( 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 ) ) ) ) ) ) with typecode |-
10 9 biimpa Could not format ( ( ( 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 ) ) ) ) ) : No typesetting found for |- ( ( ( 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 ) ) ) ) ) with typecode |-
11 10 simp3d Could not format ( ( ( 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 ) ) ) ) : No typesetting found for |- ( ( ( 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 ) ) ) ) with typecode |-
12 11 3impa Could not format ( ( 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 ) ) ) ) : No typesetting found for |- ( ( 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 ) ) ) ) with typecode |-
13 simpr F x G y = F x 1 st S F y F x H y = F x K F y F x H y = F x K F y
14 13 2ralimi x X y X F x G y = F x 1 st S F y F x H y = F x K F y x X y X F x H y = F x K F y
15 12 14 syl Could not format ( ( 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 ) ) ) : No typesetting found for |- ( ( 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 ) ) ) with typecode |-
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 X B X x X y X F x H y = F x K F y F A H B = F A K F B
26 15 25 mpan9 Could not format ( ( ( 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 ) ) ) : No typesetting found for |- ( ( ( 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 ) ) ) with typecode |-