MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  evlslem1 Unicode version

Theorem evlslem1 19889
Description: Lemma for evlseu 19890, give a formula for (the unique) polynomial evaluation homomorphism. (Contributed by Stefan O'Rear, 9-Mar-2015.)
Hypotheses
Ref Expression
evlslem1.p  |-  P  =  ( I mPoly  R )
evlslem1.b  |-  B  =  ( Base `  P
)
evlslem1.c  |-  C  =  ( Base `  S
)
evlslem1.k  |-  K  =  ( Base `  R
)
evlslem1.d  |-  D  =  { h  e.  ( NN0  ^m  I )  |  ( `' h " NN )  e.  Fin }
evlslem1.t  |-  T  =  (mulGrp `  S )
evlslem1.x  |-  .^  =  (.g
`  T )
evlslem1.m  |-  .x.  =  ( .r `  S )
evlslem1.v  |-  V  =  ( I mVar  R )
evlslem1.e  |-  E  =  ( p  e.  B  |->  ( S  gsumg  ( b  e.  D  |->  ( ( F `  ( p `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) ) )
evlslem1.i  |-  ( ph  ->  I  e.  _V )
evlslem1.r  |-  ( ph  ->  R  e.  CRing )
evlslem1.s  |-  ( ph  ->  S  e.  CRing )
evlslem1.f  |-  ( ph  ->  F  e.  ( R RingHom  S ) )
evlslem1.g  |-  ( ph  ->  G : I --> C )
evlslem1.a  |-  A  =  (algSc `  P )
Assertion
Ref Expression
evlslem1  |-  ( ph  ->  ( E  e.  ( P RingHom  S )  /\  ( E  o.  A )  =  F  /\  ( E  o.  V )  =  G ) )
Distinct variable groups:    p, b, B    C, b, p    ph, b, p    F, b, p    K, b    T, b, p    D, b, p    h, b, I, p    R, b, h, p    G, b, p    P, b, p    S, b, p    .x. , b, p   
.^ , b, p
Allowed substitution hints:    ph( h)    A( h, p, b)    B( h)    C( h)    D( h)    P( h)    S( h)    T( h)    .x. (
h)    E( h, p, b)    .^ ( h)    F( h)    G( h)    K( h, p)    V( h, p, b)

Proof of Theorem evlslem1
Dummy variables  x  v  w  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 evlslem1.b . . 3  |-  B  =  ( Base `  P
)
2 eqid 2404 . . 3  |-  ( 1r
`  P )  =  ( 1r `  P
)
3 eqid 2404 . . 3  |-  ( 1r
`  S )  =  ( 1r `  S
)
4 eqid 2404 . . 3  |-  ( .r
`  P )  =  ( .r `  P
)
5 evlslem1.m . . 3  |-  .x.  =  ( .r `  S )
6 evlslem1.i . . . 4  |-  ( ph  ->  I  e.  _V )
7 evlslem1.r . . . . 5  |-  ( ph  ->  R  e.  CRing )
8 crngrng 15629 . . . . 5  |-  ( R  e.  CRing  ->  R  e.  Ring )
97, 8syl 16 . . . 4  |-  ( ph  ->  R  e.  Ring )
10 evlslem1.p . . . . 5  |-  P  =  ( I mPoly  R )
1110mplrng 16470 . . . 4  |-  ( ( I  e.  _V  /\  R  e.  Ring )  ->  P  e.  Ring )
126, 9, 11syl2anc 643 . . 3  |-  ( ph  ->  P  e.  Ring )
13 evlslem1.s . . . 4  |-  ( ph  ->  S  e.  CRing )
14 crngrng 15629 . . . 4  |-  ( S  e.  CRing  ->  S  e.  Ring )
1513, 14syl 16 . . 3  |-  ( ph  ->  S  e.  Ring )
16 evlslem1.k . . . . . . 7  |-  K  =  ( Base `  R
)
17 eqid 2404 . . . . . . 7  |-  ( 1r
`  R )  =  ( 1r `  R
)
1816, 17rngidcl 15639 . . . . . 6  |-  ( R  e.  Ring  ->  ( 1r
`  R )  e.  K )
199, 18syl 16 . . . . 5  |-  ( ph  ->  ( 1r `  R
)  e.  K )
20 evlslem1.d . . . . . . . . 9  |-  D  =  { h  e.  ( NN0  ^m  I )  |  ( `' h " NN )  e.  Fin }
21 eqid 2404 . . . . . . . . 9  |-  ( 0g
`  R )  =  ( 0g `  R
)
22 evlslem1.a . . . . . . . . 9  |-  A  =  (algSc `  P )
236adantr 452 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  K )  ->  I  e.  _V )
249adantr 452 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  K )  ->  R  e.  Ring )
25 simpr 448 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  K )  ->  x  e.  K )
2610, 20, 21, 16, 22, 23, 24, 25mplascl 16511 . . . . . . . 8  |-  ( (
ph  /\  x  e.  K )  ->  ( A `  x )  =  ( y  e.  D  |->  if ( y  =  ( I  X.  { 0 } ) ,  x ,  ( 0g `  R ) ) ) )
2726fveq2d 5691 . . . . . . 7  |-  ( (
ph  /\  x  e.  K )  ->  ( E `  ( A `  x ) )  =  ( E `  (
y  e.  D  |->  if ( y  =  ( I  X.  { 0 } ) ,  x ,  ( 0g `  R ) ) ) ) )
28 evlslem1.c . . . . . . . 8  |-  C  =  ( Base `  S
)
29 evlslem1.t . . . . . . . 8  |-  T  =  (mulGrp `  S )
30 evlslem1.x . . . . . . . 8  |-  .^  =  (.g
`  T )
31 evlslem1.v . . . . . . . 8  |-  V  =  ( I mVar  R )
32 evlslem1.e . . . . . . . 8  |-  E  =  ( p  e.  B  |->  ( S  gsumg  ( b  e.  D  |->  ( ( F `  ( p `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) ) )
337adantr 452 . . . . . . . 8  |-  ( (
ph  /\  x  e.  K )  ->  R  e.  CRing )
3413adantr 452 . . . . . . . 8  |-  ( (
ph  /\  x  e.  K )  ->  S  e.  CRing )
35 evlslem1.f . . . . . . . . 9  |-  ( ph  ->  F  e.  ( R RingHom  S ) )
3635adantr 452 . . . . . . . 8  |-  ( (
ph  /\  x  e.  K )  ->  F  e.  ( R RingHom  S )
)
37 evlslem1.g . . . . . . . . 9  |-  ( ph  ->  G : I --> C )
3837adantr 452 . . . . . . . 8  |-  ( (
ph  /\  x  e.  K )  ->  G : I --> C )
3920psrbag0 16509 . . . . . . . . . 10  |-  ( I  e.  _V  ->  (
I  X.  { 0 } )  e.  D
)
406, 39syl 16 . . . . . . . . 9  |-  ( ph  ->  ( I  X.  {
0 } )  e.  D )
4140adantr 452 . . . . . . . 8  |-  ( (
ph  /\  x  e.  K )  ->  (
I  X.  { 0 } )  e.  D
)
4210, 1, 28, 16, 20, 29, 30, 5, 31, 32, 23, 33, 34, 36, 38, 21, 41, 25evlslem3 19888 . . . . . . 7  |-  ( (
ph  /\  x  e.  K )  ->  ( E `  ( y  e.  D  |->  if ( y  =  ( I  X.  { 0 } ) ,  x ,  ( 0g `  R
) ) ) )  =  ( ( F `
 x )  .x.  ( T  gsumg  ( ( I  X.  { 0 } )  o F  .^  G
) ) ) )
43 0z 10249 . . . . . . . . . . . . . . 15  |-  0  e.  ZZ
4443a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  I )  ->  0  e.  ZZ )
45 fvex 5701 . . . . . . . . . . . . . . 15  |-  ( G `
 x )  e. 
_V
4645a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  I )  ->  ( G `  x )  e.  _V )
47 fconstmpt 4880 . . . . . . . . . . . . . . 15  |-  ( I  X.  { 0 } )  =  ( x  e.  I  |->  0 )
4847a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( I  X.  {
0 } )  =  ( x  e.  I  |->  0 ) )
4937feqmptd 5738 . . . . . . . . . . . . . 14  |-  ( ph  ->  G  =  ( x  e.  I  |->  ( G `
 x ) ) )
506, 44, 46, 48, 49offval2 6281 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( I  X.  { 0 } )  o F  .^  G
)  =  ( x  e.  I  |->  ( 0 
.^  ( G `  x ) ) ) )
5137ffvelrnda 5829 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  I )  ->  ( G `  x )  e.  C )
5229, 28mgpbas 15609 . . . . . . . . . . . . . . . 16  |-  C  =  ( Base `  T
)
5329, 3rngidval 15621 . . . . . . . . . . . . . . . 16  |-  ( 1r
`  S )  =  ( 0g `  T
)
5452, 53, 30mulg0 14850 . . . . . . . . . . . . . . 15  |-  ( ( G `  x )  e.  C  ->  (
0  .^  ( G `  x ) )  =  ( 1r `  S
) )
5551, 54syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  I )  ->  (
0  .^  ( G `  x ) )  =  ( 1r `  S
) )
5655mpteq2dva 4255 . . . . . . . . . . . . 13  |-  ( ph  ->  ( x  e.  I  |->  ( 0  .^  ( G `  x )
) )  =  ( x  e.  I  |->  ( 1r `  S ) ) )
5750, 56eqtrd 2436 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( I  X.  { 0 } )  o F  .^  G
)  =  ( x  e.  I  |->  ( 1r
`  S ) ) )
5857oveq2d 6056 . . . . . . . . . . 11  |-  ( ph  ->  ( T  gsumg  ( ( I  X.  { 0 } )  o F  .^  G
) )  =  ( T  gsumg  ( x  e.  I  |->  ( 1r `  S
) ) ) )
5929crngmgp 15627 . . . . . . . . . . . . . 14  |-  ( S  e.  CRing  ->  T  e. CMnd )
6013, 59syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  T  e. CMnd )
61 cmnmnd 15382 . . . . . . . . . . . . 13  |-  ( T  e. CMnd  ->  T  e.  Mnd )
6260, 61syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  T  e.  Mnd )
6353gsumz 14736 . . . . . . . . . . . 12  |-  ( ( T  e.  Mnd  /\  I  e.  _V )  ->  ( T  gsumg  ( x  e.  I  |->  ( 1r `  S
) ) )  =  ( 1r `  S
) )
6462, 6, 63syl2anc 643 . . . . . . . . . . 11  |-  ( ph  ->  ( T  gsumg  ( x  e.  I  |->  ( 1r `  S
) ) )  =  ( 1r `  S
) )
6558, 64eqtrd 2436 . . . . . . . . . 10  |-  ( ph  ->  ( T  gsumg  ( ( I  X.  { 0 } )  o F  .^  G
) )  =  ( 1r `  S ) )
6665adantr 452 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  K )  ->  ( T  gsumg  ( ( I  X.  { 0 } )  o F  .^  G
) )  =  ( 1r `  S ) )
6766oveq2d 6056 . . . . . . . 8  |-  ( (
ph  /\  x  e.  K )  ->  (
( F `  x
)  .x.  ( T  gsumg  ( ( I  X.  {
0 } )  o F  .^  G )
) )  =  ( ( F `  x
)  .x.  ( 1r `  S ) ) )
6815adantr 452 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  K )  ->  S  e.  Ring )
6916, 28rhmf 15782 . . . . . . . . . . 11  |-  ( F  e.  ( R RingHom  S
)  ->  F : K
--> C )
7035, 69syl 16 . . . . . . . . . 10  |-  ( ph  ->  F : K --> C )
7170ffvelrnda 5829 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  K )  ->  ( F `  x )  e.  C )
7228, 5, 3rngridm 15643 . . . . . . . . 9  |-  ( ( S  e.  Ring  /\  ( F `  x )  e.  C )  ->  (
( F `  x
)  .x.  ( 1r `  S ) )  =  ( F `  x
) )
7368, 71, 72syl2anc 643 . . . . . . . 8  |-  ( (
ph  /\  x  e.  K )  ->  (
( F `  x
)  .x.  ( 1r `  S ) )  =  ( F `  x
) )
7467, 73eqtrd 2436 . . . . . . 7  |-  ( (
ph  /\  x  e.  K )  ->  (
( F `  x
)  .x.  ( T  gsumg  ( ( I  X.  {
0 } )  o F  .^  G )
) )  =  ( F `  x ) )
7527, 42, 743eqtrd 2440 . . . . . 6  |-  ( (
ph  /\  x  e.  K )  ->  ( E `  ( A `  x ) )  =  ( F `  x
) )
7675ralrimiva 2749 . . . . 5  |-  ( ph  ->  A. x  e.  K  ( E `  ( A `
 x ) )  =  ( F `  x ) )
77 fveq2 5687 . . . . . . . 8  |-  ( x  =  ( 1r `  R )  ->  ( A `  x )  =  ( A `  ( 1r `  R ) ) )
7877fveq2d 5691 . . . . . . 7  |-  ( x  =  ( 1r `  R )  ->  ( E `  ( A `  x ) )  =  ( E `  ( A `  ( 1r `  R ) ) ) )
79 fveq2 5687 . . . . . . 7  |-  ( x  =  ( 1r `  R )  ->  ( F `  x )  =  ( F `  ( 1r `  R ) ) )
8078, 79eqeq12d 2418 . . . . . 6  |-  ( x  =  ( 1r `  R )  ->  (
( E `  ( A `  x )
)  =  ( F `
 x )  <->  ( E `  ( A `  ( 1r `  R ) ) )  =  ( F `
 ( 1r `  R ) ) ) )
8180rspcva 3010 . . . . 5  |-  ( ( ( 1r `  R
)  e.  K  /\  A. x  e.  K  ( E `  ( A `
 x ) )  =  ( F `  x ) )  -> 
( E `  ( A `  ( 1r `  R ) ) )  =  ( F `  ( 1r `  R ) ) )
8219, 76, 81syl2anc 643 . . . 4  |-  ( ph  ->  ( E `  ( A `  ( 1r `  R ) ) )  =  ( F `  ( 1r `  R ) ) )
8310mplassa 16472 . . . . . . . . 9  |-  ( ( I  e.  _V  /\  R  e.  CRing )  ->  P  e. AssAlg )
846, 7, 83syl2anc 643 . . . . . . . 8  |-  ( ph  ->  P  e. AssAlg )
85 eqid 2404 . . . . . . . . 9  |-  (Scalar `  P )  =  (Scalar `  P )
8622, 85asclrhm 16355 . . . . . . . 8  |-  ( P  e. AssAlg  ->  A  e.  ( (Scalar `  P ) RingHom  P ) )
8784, 86syl 16 . . . . . . 7  |-  ( ph  ->  A  e.  ( (Scalar `  P ) RingHom  P ) )
8810, 6, 7mplsca 16463 . . . . . . . 8  |-  ( ph  ->  R  =  (Scalar `  P ) )
8988oveq1d 6055 . . . . . . 7  |-  ( ph  ->  ( R RingHom  P )  =  ( (Scalar `  P ) RingHom  P ) )
9087, 89eleqtrrd 2481 . . . . . 6  |-  ( ph  ->  A  e.  ( R RingHom  P ) )
9117, 2rhm1 15786 . . . . . 6  |-  ( A  e.  ( R RingHom  P
)  ->  ( A `  ( 1r `  R
) )  =  ( 1r `  P ) )
9290, 91syl 16 . . . . 5  |-  ( ph  ->  ( A `  ( 1r `  R ) )  =  ( 1r `  P ) )
9392fveq2d 5691 . . . 4  |-  ( ph  ->  ( E `  ( A `  ( 1r `  R ) ) )  =  ( E `  ( 1r `  P ) ) )
9417, 3rhm1 15786 . . . . 5  |-  ( F  e.  ( R RingHom  S
)  ->  ( F `  ( 1r `  R
) )  =  ( 1r `  S ) )
9535, 94syl 16 . . . 4  |-  ( ph  ->  ( F `  ( 1r `  R ) )  =  ( 1r `  S ) )
9682, 93, 953eqtr3d 2444 . . 3  |-  ( ph  ->  ( E `  ( 1r `  P ) )  =  ( 1r `  S ) )
97 eqid 2404 . . . . 5  |-  ( +g  `  P )  =  ( +g  `  P )
98 eqid 2404 . . . . 5  |-  ( +g  `  S )  =  ( +g  `  S )
99 rnggrp 15624 . . . . . 6  |-  ( P  e.  Ring  ->  P  e. 
Grp )
10012, 99syl 16 . . . . 5  |-  ( ph  ->  P  e.  Grp )
101 rnggrp 15624 . . . . . 6  |-  ( S  e.  Ring  ->  S  e. 
Grp )
10215, 101syl 16 . . . . 5  |-  ( ph  ->  S  e.  Grp )
103 eqid 2404 . . . . . . 7  |-  ( 0g
`  S )  =  ( 0g `  S
)
104 rngcmn 15649 . . . . . . . . 9  |-  ( S  e.  Ring  ->  S  e. CMnd
)
10515, 104syl 16 . . . . . . . 8  |-  ( ph  ->  S  e. CMnd )
106105adantr 452 . . . . . . 7  |-  ( (
ph  /\  p  e.  B )  ->  S  e. CMnd )
107 ovex 6065 . . . . . . . . . 10  |-  ( NN0 
^m  I )  e. 
_V
108107rabex 4314 . . . . . . . . 9  |-  { h  e.  ( NN0  ^m  I
)  |  ( `' h " NN )  e.  Fin }  e.  _V
10920, 108eqeltri 2474 . . . . . . . 8  |-  D  e. 
_V
110109a1i 11 . . . . . . 7  |-  ( (
ph  /\  p  e.  B )  ->  D  e.  _V )
1116adantr 452 . . . . . . . . 9  |-  ( (
ph  /\  p  e.  B )  ->  I  e.  _V )
1127adantr 452 . . . . . . . . 9  |-  ( (
ph  /\  p  e.  B )  ->  R  e.  CRing )
11313adantr 452 . . . . . . . . 9  |-  ( (
ph  /\  p  e.  B )  ->  S  e.  CRing )
11435adantr 452 . . . . . . . . 9  |-  ( (
ph  /\  p  e.  B )  ->  F  e.  ( R RingHom  S )
)
11537adantr 452 . . . . . . . . 9  |-  ( (
ph  /\  p  e.  B )  ->  G : I --> C )
116 simpr 448 . . . . . . . . 9  |-  ( (
ph  /\  p  e.  B )  ->  p  e.  B )
11710, 1, 28, 16, 20, 29, 30, 5, 31, 32, 111, 112, 113, 114, 115, 116evlslem6 19887 . . . . . . . 8  |-  ( (
ph  /\  p  e.  B )  ->  (
( b  e.  D  |->  ( ( F `  ( p `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) : D --> C  /\  ( `' ( b  e.  D  |->  ( ( F `  (
p `  b )
)  .x.  ( T  gsumg  ( b  o F  .^  G ) ) ) ) " ( _V 
\  { ( 0g
`  S ) } ) )  e.  Fin ) )
118117simpld 446 . . . . . . 7  |-  ( (
ph  /\  p  e.  B )  ->  (
b  e.  D  |->  ( ( F `  (
p `  b )
)  .x.  ( T  gsumg  ( b  o F  .^  G ) ) ) ) : D --> C )
119117simprd 450 . . . . . . 7  |-  ( (
ph  /\  p  e.  B )  ->  ( `' ( b  e.  D  |->  ( ( F `
 ( p `  b ) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) " ( _V  \  { ( 0g
`  S ) } ) )  e.  Fin )
12028, 103, 106, 110, 118, 119gsumcl 15476 . . . . . 6  |-  ( (
ph  /\  p  e.  B )  ->  ( S  gsumg  ( b  e.  D  |->  ( ( F `  ( p `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) )  e.  C )
121120, 32fmptd 5852 . . . . 5  |-  ( ph  ->  E : B --> C )
122 eqid 2404 . . . . . . . . . . . . . . . . 17  |-  ( +g  `  R )  =  ( +g  `  R )
123 simplrl 737 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  x  e.  B )
124 simplrr 738 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  y  e.  B )
12510, 1, 122, 97, 123, 124mpladd 16460 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  (
x ( +g  `  P
) y )  =  ( x  o F ( +g  `  R
) y ) )
126125fveq1d 5689 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  (
( x ( +g  `  P ) y ) `
 b )  =  ( ( x  o F ( +g  `  R
) y ) `  b ) )
127 simprl 733 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  ->  x  e.  B )
12810, 16, 1, 20, 127mplelf 16452 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  ->  x : D --> K )
129 ffn 5550 . . . . . . . . . . . . . . . . . 18  |-  ( x : D --> K  ->  x  Fn  D )
130128, 129syl 16 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  ->  x  Fn  D )
131130adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  x  Fn  D )
132 simprr 734 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
y  e.  B )
13310, 16, 1, 20, 132mplelf 16452 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
y : D --> K )
134 ffn 5550 . . . . . . . . . . . . . . . . . 18  |-  ( y : D --> K  -> 
y  Fn  D )
135133, 134syl 16 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
y  Fn  D )
136135adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  y  Fn  D )
137109a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  D  e.  _V )
138 simpr 448 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  b  e.  D )
139 fnfvof 6276 . . . . . . . . . . . . . . . 16  |-  ( ( ( x  Fn  D  /\  y  Fn  D
)  /\  ( D  e.  _V  /\  b  e.  D ) )  -> 
( ( x  o F ( +g  `  R
) y ) `  b )  =  ( ( x `  b
) ( +g  `  R
) ( y `  b ) ) )
140131, 136, 137, 138, 139syl22anc 1185 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  (
( x  o F ( +g  `  R
) y ) `  b )  =  ( ( x `  b
) ( +g  `  R
) ( y `  b ) ) )
141126, 140eqtrd 2436 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  (
( x ( +g  `  P ) y ) `
 b )  =  ( ( x `  b ) ( +g  `  R ) ( y `
 b ) ) )
142141fveq2d 5691 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  ( F `  ( (
x ( +g  `  P
) y ) `  b ) )  =  ( F `  (
( x `  b
) ( +g  `  R
) ( y `  b ) ) ) )
143 rhmghm 15781 . . . . . . . . . . . . . . . 16  |-  ( F  e.  ( R RingHom  S
)  ->  F  e.  ( R  GrpHom  S ) )
14435, 143syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  F  e.  ( R 
GrpHom  S ) )
145144ad2antrr 707 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  F  e.  ( R  GrpHom  S ) )
146128ffvelrnda 5829 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  (
x `  b )  e.  K )
147133ffvelrnda 5829 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  (
y `  b )  e.  K )
14816, 122, 98ghmlin 14966 . . . . . . . . . . . . . 14  |-  ( ( F  e.  ( R 
GrpHom  S )  /\  (
x `  b )  e.  K  /\  (
y `  b )  e.  K )  ->  ( F `  ( (
x `  b )
( +g  `  R ) ( y `  b
) ) )  =  ( ( F `  ( x `  b
) ) ( +g  `  S ) ( F `
 ( y `  b ) ) ) )
149145, 146, 147, 148syl3anc 1184 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  ( F `  ( (
x `  b )
( +g  `  R ) ( y `  b
) ) )  =  ( ( F `  ( x `  b
) ) ( +g  `  S ) ( F `
 ( y `  b ) ) ) )
150142, 149eqtrd 2436 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  ( F `  ( (
x ( +g  `  P
) y ) `  b ) )  =  ( ( F `  ( x `  b
) ) ( +g  `  S ) ( F `
 ( y `  b ) ) ) )
151150oveq1d 6055 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  (
( F `  (
( x ( +g  `  P ) y ) `
 b ) ) 
.x.  ( T  gsumg  ( b  o F  .^  G
) ) )  =  ( ( ( F `
 ( x `  b ) ) ( +g  `  S ) ( F `  (
y `  b )
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) )
15215ad2antrr 707 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  S  e.  Ring )
15370ad2antrr 707 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  F : K --> C )
154153, 146ffvelrnd 5830 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  ( F `  ( x `  b ) )  e.  C )
155153, 147ffvelrnd 5830 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  ( F `  ( y `  b ) )  e.  C )
15660ad2antrr 707 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  T  e. CMnd )
15737ad2antrr 707 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  G : I --> C )
1586ad2antrr 707 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  I  e.  _V )
15920, 52, 30, 53, 156, 138, 157, 158psrbagev2 16522 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  ( T  gsumg  ( b  o F 
.^  G ) )  e.  C )
16028, 98, 5rngdir 15638 . . . . . . . . . . . 12  |-  ( ( S  e.  Ring  /\  (
( F `  (
x `  b )
)  e.  C  /\  ( F `  ( y `
 b ) )  e.  C  /\  ( T  gsumg  ( b  o F 
.^  G ) )  e.  C ) )  ->  ( ( ( F `  ( x `
 b ) ) ( +g  `  S
) ( F `  ( y `  b
) ) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) )  =  ( ( ( F `  (
x `  b )
)  .x.  ( T  gsumg  ( b  o F  .^  G ) ) ) ( +g  `  S
) ( ( F `
 ( y `  b ) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) )
161152, 154, 155, 159, 160syl13anc 1186 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  (
( ( F `  ( x `  b
) ) ( +g  `  S ) ( F `
 ( y `  b ) ) ) 
.x.  ( T  gsumg  ( b  o F  .^  G
) ) )  =  ( ( ( F `
 ( x `  b ) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ( +g  `  S
) ( ( F `
 ( y `  b ) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) )
162151, 161eqtrd 2436 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  (
( F `  (
( x ( +g  `  P ) y ) `
 b ) ) 
.x.  ( T  gsumg  ( b  o F  .^  G
) ) )  =  ( ( ( F `
 ( x `  b ) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ( +g  `  S
) ( ( F `
 ( y `  b ) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) )
163162mpteq2dva 4255 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( b  e.  D  |->  ( ( F `  ( ( x ( +g  `  P ) y ) `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) )  =  ( b  e.  D  |->  ( ( ( F `  ( x `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ( +g  `  S
) ( ( F `
 ( y `  b ) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) ) )
164109a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  ->  D  e.  _V )
165 ovex 6065 . . . . . . . . . . 11  |-  ( ( F `  ( x `
 b ) ) 
.x.  ( T  gsumg  ( b  o F  .^  G
) ) )  e. 
_V
166165a1i 11 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  (
( F `  (
x `  b )
)  .x.  ( T  gsumg  ( b  o F  .^  G ) ) )  e.  _V )
167 ovex 6065 . . . . . . . . . . 11  |-  ( ( F `  ( y `
 b ) ) 
.x.  ( T  gsumg  ( b  o F  .^  G
) ) )  e. 
_V
168167a1i 11 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  (
( F `  (
y `  b )
)  .x.  ( T  gsumg  ( b  o F  .^  G ) ) )  e.  _V )
169 eqidd 2405 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( b  e.  D  |->  ( ( F `  ( x `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) )  =  ( b  e.  D  |->  ( ( F `  (
x `  b )
)  .x.  ( T  gsumg  ( b  o F  .^  G ) ) ) ) )
170 eqidd 2405 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( b  e.  D  |->  ( ( F `  ( y `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) )  =  ( b  e.  D  |->  ( ( F `  (
y `  b )
)  .x.  ( T  gsumg  ( b  o F  .^  G ) ) ) ) )
171164, 166, 168, 169, 170offval2 6281 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( ( b  e.  D  |->  ( ( F `
 ( x `  b ) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) )  o F ( +g  `  S
) ( b  e.  D  |->  ( ( F `
 ( y `  b ) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) )  =  ( b  e.  D  |->  ( ( ( F `
 ( x `  b ) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ( +g  `  S
) ( ( F `
 ( y `  b ) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) ) )
172163, 171eqtr4d 2439 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( b  e.  D  |->  ( ( F `  ( ( x ( +g  `  P ) y ) `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) )  =  ( ( b  e.  D  |->  ( ( F `  ( x `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) )  o F ( +g  `  S
) ( b  e.  D  |->  ( ( F `
 ( y `  b ) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) ) )
173172oveq2d 6056 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( S  gsumg  ( b  e.  D  |->  ( ( F `  ( ( x ( +g  `  P ) y ) `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) )  =  ( S  gsumg  ( ( b  e.  D  |->  ( ( F `
 ( x `  b ) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) )  o F ( +g  `  S
) ( b  e.  D  |->  ( ( F `
 ( y `  b ) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) ) ) )
174105adantr 452 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  ->  S  e. CMnd )
1756adantr 452 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  ->  I  e.  _V )
1767adantr 452 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  ->  R  e.  CRing )
17713adantr 452 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  ->  S  e.  CRing )
17835adantr 452 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  ->  F  e.  ( R RingHom  S ) )
17937adantr 452 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  ->  G : I --> C )
18010, 1, 28, 16, 20, 29, 30, 5, 31, 32, 175, 176, 177, 178, 179, 127evlslem6 19887 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( ( b  e.  D  |->  ( ( F `
 ( x `  b ) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) : D --> C  /\  ( `' ( b  e.  D  |->  ( ( F `  (
x `  b )
)  .x.  ( T  gsumg  ( b  o F  .^  G ) ) ) ) " ( _V 
\  { ( 0g
`  S ) } ) )  e.  Fin ) )
181180simpld 446 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( b  e.  D  |->  ( ( F `  ( x `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) : D --> C )
18210, 1, 28, 16, 20, 29, 30, 5, 31, 32, 175, 176, 177, 178, 179, 132evlslem6 19887 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( ( b  e.  D  |->  ( ( F `
 ( y `  b ) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) : D --> C  /\  ( `' ( b  e.  D  |->  ( ( F `  (
y `  b )
)  .x.  ( T  gsumg  ( b  o F  .^  G ) ) ) ) " ( _V 
\  { ( 0g
`  S ) } ) )  e.  Fin ) )
183182simpld 446 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( b  e.  D  |->  ( ( F `  ( y `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) : D --> C )
184180simprd 450 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( `' ( b  e.  D  |->  ( ( F `  ( x `
 b ) ) 
.x.  ( T  gsumg  ( b  o F  .^  G
) ) ) )
" ( _V  \  { ( 0g `  S ) } ) )  e.  Fin )
185182simprd 450 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( `' ( b  e.  D  |->  ( ( F `  ( y `
 b ) ) 
.x.  ( T  gsumg  ( b  o F  .^  G
) ) ) )
" ( _V  \  { ( 0g `  S ) } ) )  e.  Fin )
18628, 103, 98, 174, 164, 181, 183, 184, 185gsumadd 15483 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( S  gsumg  ( ( b  e.  D  |->  ( ( F `
 ( x `  b ) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) )  o F ( +g  `  S
) ( b  e.  D  |->  ( ( F `
 ( y `  b ) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) ) )  =  ( ( S 
gsumg  ( b  e.  D  |->  ( ( F `  ( x `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) ) ( +g  `  S ) ( S  gsumg  ( b  e.  D  |->  ( ( F `  ( y `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) ) ) )
187173, 186eqtrd 2436 . . . . . 6  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( S  gsumg  ( b  e.  D  |->  ( ( F `  ( ( x ( +g  `  P ) y ) `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) )  =  ( ( S  gsumg  ( b  e.  D  |->  ( ( F `  ( x `
 b ) ) 
.x.  ( T  gsumg  ( b  o F  .^  G
) ) ) ) ) ( +g  `  S
) ( S  gsumg  ( b  e.  D  |->  ( ( F `  ( y `
 b ) ) 
.x.  ( T  gsumg  ( b  o F  .^  G
) ) ) ) ) ) )
188100adantr 452 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  ->  P  e.  Grp )
1891, 97grpcl 14773 . . . . . . . 8  |-  ( ( P  e.  Grp  /\  x  e.  B  /\  y  e.  B )  ->  ( x ( +g  `  P ) y )  e.  B )
190188, 127, 132, 189syl3anc 1184 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( x ( +g  `  P ) y )  e.  B )
191 fveq1 5686 . . . . . . . . . . . 12  |-  ( p  =  ( x ( +g  `  P ) y )  ->  (
p `  b )  =  ( ( x ( +g  `  P
) y ) `  b ) )
192191fveq2d 5691 . . . . . . . . . . 11  |-  ( p  =  ( x ( +g  `  P ) y )  ->  ( F `  ( p `  b ) )  =  ( F `  (
( x ( +g  `  P ) y ) `
 b ) ) )
193192oveq1d 6055 . . . . . . . . . 10  |-  ( p  =  ( x ( +g  `  P ) y )  ->  (
( F `  (
p `  b )
)  .x.  ( T  gsumg  ( b  o F  .^  G ) ) )  =  ( ( F `
 ( ( x ( +g  `  P
) y ) `  b ) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) )
194193mpteq2dv 4256 . . . . . . . . 9  |-  ( p  =  ( x ( +g  `  P ) y )  ->  (
b  e.  D  |->  ( ( F `  (
p `  b )
)  .x.  ( T  gsumg  ( b  o F  .^  G ) ) ) )  =  ( b  e.  D  |->  ( ( F `  ( ( x ( +g  `  P
) y ) `  b ) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) )
195194oveq2d 6056 . . . . . . . 8  |-  ( p  =  ( x ( +g  `  P ) y )  ->  ( S  gsumg  ( b  e.  D  |->  ( ( F `  ( p `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) )  =  ( S  gsumg  ( b  e.  D  |->  ( ( F `  ( ( x ( +g  `  P ) y ) `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) ) )
196 ovex 6065 . . . . . . . 8  |-  ( S 
gsumg  ( b  e.  D  |->  ( ( F `  ( ( x ( +g  `  P ) y ) `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) )  e. 
_V
197195, 32, 196fvmpt 5765 . . . . . . 7  |-  ( ( x ( +g  `  P
) y )  e.  B  ->  ( E `  ( x ( +g  `  P ) y ) )  =  ( S 
gsumg  ( b  e.  D  |->  ( ( F `  ( ( x ( +g  `  P ) y ) `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) ) )
198190, 197syl 16 . . . . . 6  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( E `  (
x ( +g  `  P
) y ) )  =  ( S  gsumg  ( b  e.  D  |->  ( ( F `  ( ( x ( +g  `  P
) y ) `  b ) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) ) )
199 fveq1 5686 . . . . . . . . . . . . 13  |-  ( p  =  x  ->  (
p `  b )  =  ( x `  b ) )
200199fveq2d 5691 . . . . . . . . . . . 12  |-  ( p  =  x  ->  ( F `  ( p `  b ) )  =  ( F `  (
x `  b )
) )
201200oveq1d 6055 . . . . . . . . . . 11  |-  ( p  =  x  ->  (
( F `  (
p `  b )
)  .x.  ( T  gsumg  ( b  o F  .^  G ) ) )  =  ( ( F `
 ( x `  b ) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) )
202201mpteq2dv 4256 . . . . . . . . . 10  |-  ( p  =  x  ->  (
b  e.  D  |->  ( ( F `  (
p `  b )
)  .x.  ( T  gsumg  ( b  o F  .^  G ) ) ) )  =  ( b  e.  D  |->  ( ( F `  ( x `
 b ) ) 
.x.  ( T  gsumg  ( b  o F  .^  G
) ) ) ) )
203202oveq2d 6056 . . . . . . . . 9  |-  ( p  =  x  ->  ( S  gsumg  ( b  e.  D  |->  ( ( F `  ( p `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) )  =  ( S  gsumg  ( b  e.  D  |->  ( ( F `  ( x `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) ) )
204 ovex 6065 . . . . . . . . 9  |-  ( S 
gsumg  ( b  e.  D  |->  ( ( F `  ( x `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) )  e. 
_V
205203, 32, 204fvmpt 5765 . . . . . . . 8  |-  ( x  e.  B  ->  ( E `  x )  =  ( S  gsumg  ( b  e.  D  |->  ( ( F `  ( x `
 b ) ) 
.x.  ( T  gsumg  ( b  o F  .^  G
) ) ) ) ) )
206127, 205syl 16 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( E `  x
)  =  ( S 
gsumg  ( b  e.  D  |->  ( ( F `  ( x `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) ) )
207 fveq1 5686 . . . . . . . . . . . . 13  |-  ( p  =  y  ->  (
p `  b )  =  ( y `  b ) )
208207fveq2d 5691 . . . . . . . . . . . 12  |-  ( p  =  y  ->  ( F `  ( p `  b ) )  =  ( F `  (
y `  b )
) )
209208oveq1d 6055 . . . . . . . . . . 11  |-  ( p  =  y  ->  (
( F `  (
p `  b )
)  .x.  ( T  gsumg  ( b  o F  .^  G ) ) )  =  ( ( F `
 ( y `  b ) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) )
210209mpteq2dv 4256 . . . . . . . . . 10  |-  ( p  =  y  ->  (
b  e.  D  |->  ( ( F `  (
p `  b )
)  .x.  ( T  gsumg  ( b  o F  .^  G ) ) ) )  =  ( b  e.  D  |->  ( ( F `  ( y `
 b ) ) 
.x.  ( T  gsumg  ( b  o F  .^  G
) ) ) ) )
211210oveq2d 6056 . . . . . . . . 9  |-  ( p  =  y  ->  ( S  gsumg  ( b  e.  D  |->  ( ( F `  ( p `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) )  =  ( S  gsumg  ( b  e.  D  |->  ( ( F `  ( y `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) ) )
212 ovex 6065 . . . . . . . . 9  |-  ( S 
gsumg  ( b  e.  D  |->  ( ( F `  ( y `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) )  e. 
_V
213211, 32, 212fvmpt 5765 . . . . . . . 8  |-  ( y  e.  B  ->  ( E `  y )  =  ( S  gsumg  ( b  e.  D  |->  ( ( F `  ( y `
 b ) ) 
.x.  ( T  gsumg  ( b  o F  .^  G
) ) ) ) ) )
214213ad2antll 710 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( E `  y
)  =  ( S 
gsumg  ( b  e.  D  |->  ( ( F `  ( y `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) ) )
215206, 214oveq12d 6058 . . . . . 6  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( ( E `  x ) ( +g  `  S ) ( E `
 y ) )  =  ( ( S 
gsumg  ( b  e.  D  |->  ( ( F `  ( x `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) ) ( +g  `  S ) ( S  gsumg  ( b  e.  D  |->  ( ( F `  ( y `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) ) ) )
216187, 198, 2153eqtr4d 2446 . . . . 5  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( E `  (
x ( +g  `  P
) y ) )  =  ( ( E `
 x ) ( +g  `  S ) ( E `  y
) ) )
2171, 28, 97, 98, 100, 102, 121, 216isghmd 14970 . . . 4  |-  ( ph  ->  E  e.  ( P 
GrpHom  S ) )
218 eqid 2404 . . . . . . . . . . 11  |-  (mulGrp `  R )  =  (mulGrp `  R )
219218, 29rhmmhm 15780 . . . . . . . . . 10  |-  ( F  e.  ( R RingHom  S
)  ->  F  e.  ( (mulGrp `  R ) MndHom  T ) )
22035, 219syl 16 . . . . . . . . 9  |-  ( ph  ->  F  e.  ( (mulGrp `  R ) MndHom  T ) )
221220adantr 452 . . . . . . . 8  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  ->  F  e.  ( (mulGrp `  R ) MndHom  T ) )
222 simprll 739 . . . . . . . . . 10  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  ->  x  e.  B )
22310, 16, 1, 20, 222mplelf 16452 . . . . . . . . 9  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  ->  x : D --> K )
224 simprrl 741 . . . . . . . . 9  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  -> 
z  e.  D )
225223, 224ffvelrnd 5830 . . . . . . . 8  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  -> 
( x `  z
)  e.  K )
226 simprlr 740 . . . . . . . . . 10  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  -> 
y  e.  B )
22710, 16, 1, 20, 226mplelf 16452 . . . . . . . . 9  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  -> 
y : D --> K )
228 simprrr 742 . . . . . . . . 9  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  ->  w  e.  D )
229227, 228ffvelrnd 5830 . . . . . . . 8  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  -> 
( y `  w
)  e.  K )
230218, 16mgpbas 15609 . . . . . . . . 9  |-  K  =  ( Base `  (mulGrp `  R ) )
231 eqid 2404 . . . . . . . . . 10  |-  ( .r
`  R )  =  ( .r `  R
)
232218, 231mgpplusg 15607 . . . . . . . . 9  |-  ( .r
`  R )  =  ( +g  `  (mulGrp `  R ) )
23329, 5mgpplusg 15607 . . . . . . . . 9  |-  .x.  =  ( +g  `  T )
234230, 232, 233mhmlin 14700 . . . . . . . 8  |-  ( ( F  e.  ( (mulGrp `  R ) MndHom  T )  /\  ( x `  z )  e.  K  /\  ( y `  w
)  e.  K )  ->  ( F `  ( ( x `  z ) ( .r
`  R ) ( y `  w ) ) )  =  ( ( F `  (
x `  z )
)  .x.  ( F `  ( y `  w
) ) ) )
235221, 225, 229, 234syl3anc 1184 . . . . . . 7  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  -> 
( F `  (
( x `  z
) ( .r `  R ) ( y `
 w ) ) )  =  ( ( F `  ( x `
 z ) ) 
.x.  ( F `  ( y `  w
) ) ) )
23662ad2antrr 707 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  e.  D  /\  w  e.  D )
)  /\  v  e.  I )  ->  T  e.  Mnd )
2376adantr 452 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  ->  I  e.  _V )
238 simprl 733 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  -> 
z  e.  D )
23920psrbagf 16387 . . . . . . . . . . . . . . 15  |-  ( ( I  e.  _V  /\  z  e.  D )  ->  z : I --> NN0 )
240237, 238, 239syl2anc 643 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  -> 
z : I --> NN0 )
241240ffvelrnda 5829 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  e.  D  /\  w  e.  D )
)  /\  v  e.  I )  ->  (
z `  v )  e.  NN0 )
242 simprr 734 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  ->  w  e.  D )
24320psrbagf 16387 . . . . . . . . . . . . . . 15  |-  ( ( I  e.  _V  /\  w  e.  D )  ->  w : I --> NN0 )
244237, 242, 243syl2anc 643 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  ->  w : I --> NN0 )
245244ffvelrnda 5829 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  e.  D  /\  w  e.  D )
)  /\  v  e.  I )  ->  (
w `  v )  e.  NN0 )
24637adantr 452 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  ->  G : I --> C )
247246ffvelrnda 5829 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  e.  D  /\  w  e.  D )
)  /\  v  e.  I )  ->  ( G `  v )  e.  C )
24852, 30, 233mulgnn0dir 14868 . . . . . . . . . . . . 13  |-  ( ( T  e.  Mnd  /\  ( ( z `  v )  e.  NN0  /\  ( w `  v
)  e.  NN0  /\  ( G `  v )  e.  C ) )  ->  ( ( ( z `  v )  +  ( w `  v ) )  .^  ( G `  v ) )  =  ( ( ( z `  v
)  .^  ( G `  v ) )  .x.  ( ( w `  v )  .^  ( G `  v )
) ) )
249236, 241, 245, 247, 248syl13anc 1186 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
z  e.  D  /\  w  e.  D )
)  /\  v  e.  I )  ->  (
( ( z `  v )  +  ( w `  v ) )  .^  ( G `  v ) )  =  ( ( ( z `
 v )  .^  ( G `  v ) )  .x.  ( ( w `  v ) 
.^  ( G `  v ) ) ) )
250249mpteq2dva 4255 . . . . . . . . . . 11  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  -> 
( v  e.  I  |->  ( ( ( z `
 v )  +  ( w `  v
) )  .^  ( G `  v )
) )  =  ( v  e.  I  |->  ( ( ( z `  v )  .^  ( G `  v )
)  .x.  ( (
w `  v )  .^  ( G `  v
) ) ) ) )
251 ovex 6065 . . . . . . . . . . . . 13  |-  ( ( z `  v )  +  ( w `  v ) )  e. 
_V
252251a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
z  e.  D  /\  w  e.  D )
)  /\  v  e.  I )  ->  (
( z `  v
)  +  ( w `
 v ) )  e.  _V )
253 fvex 5701 . . . . . . . . . . . . 13  |-  ( G `
 v )  e. 
_V
254253a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
z  e.  D  /\  w  e.  D )
)  /\  v  e.  I )  ->  ( G `  v )  e.  _V )
255 ffn 5550 . . . . . . . . . . . . . 14  |-  ( z : I --> NN0  ->  z  Fn  I )
256240, 255syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  -> 
z  Fn  I )
257 ffn 5550 . . . . . . . . . . . . . 14  |-  ( w : I --> NN0  ->  w  Fn  I )
258244, 257syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  ->  w  Fn  I )
259 inidm 3510 . . . . . . . . . . . . 13  |-  ( I  i^i  I )  =  I
260 eqidd 2405 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  e.  D  /\  w  e.  D )
)  /\  v  e.  I )  ->  (
z `  v )  =  ( z `  v ) )
261 eqidd 2405 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  e.  D  /\  w  e.  D )
)  /\  v  e.  I )  ->  (
w `  v )  =  ( w `  v ) )
262256, 258, 237, 237, 259, 260, 261offval 6271 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  -> 
( z  o F  +  w )  =  ( v  e.  I  |->  ( ( z `  v )  +  ( w `  v ) ) ) )
26337feqmptd 5738 . . . . . . . . . . . . 13  |-  ( ph  ->  G  =  ( v  e.  I  |->  ( G `
 v ) ) )
264263adantr 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  ->  G  =  ( v  e.  I  |->  ( G `
 v ) ) )
265237, 252, 254, 262, 264offval2 6281 . . . . . . . . . . 11  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  -> 
( ( z  o F  +  w )  o F  .^  G
)  =  ( v  e.  I  |->  ( ( ( z `  v
)  +  ( w `
 v ) ) 
.^  ( G `  v ) ) ) )
266 ovex 6065 . . . . . . . . . . . . 13  |-  ( ( z `  v ) 
.^  ( G `  v ) )  e. 
_V
267266a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
z  e.  D  /\  w  e.  D )
)  /\  v  e.  I )  ->  (
( z `  v
)  .^  ( G `  v ) )  e. 
_V )
268 ovex 6065 . . . . . . . . . . . . 13  |-  ( ( w `  v ) 
.^  ( G `  v ) )  e. 
_V
269268a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
z  e.  D  /\  w  e.  D )
)  /\  v  e.  I )  ->  (
( w `  v
)  .^  ( G `  v ) )  e. 
_V )
270 ffn 5550 . . . . . . . . . . . . . . 15  |-  ( G : I --> C  ->  G  Fn  I )
27137, 270syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  G  Fn  I )
272271adantr 452 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  ->  G  Fn  I )
273 eqidd 2405 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  e.  D  /\  w  e.  D )
)  /\  v  e.  I )  ->  ( G `  v )  =  ( G `  v ) )
274256, 272, 237, 237, 259, 260, 273offval 6271 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  -> 
( z  o F 
.^  G )  =  ( v  e.  I  |->  ( ( z `  v )  .^  ( G `  v )
) ) )
275258, 272, 237, 237, 259, 261, 273offval 6271 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  -> 
( w  o F 
.^  G )  =  ( v  e.  I  |->  ( ( w `  v )  .^  ( G `  v )
) ) )
276237, 267, 269, 274, 275offval2 6281 . . . . . . . . . . 11  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  -> 
( ( z  o F  .^  G )  o F  .x.  ( w  o F  .^  G
) )  =  ( v  e.  I  |->  ( ( ( z `  v )  .^  ( G `  v )
)  .x.  ( (
w `  v )  .^  ( G `  v
) ) ) ) )
277250, 265, 2763eqtr4d 2446 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  -> 
( ( z  o F  +  w )  o F  .^  G
)  =  ( ( z  o F  .^  G )  o F 
.x.  ( w  o F  .^  G )
) )
278277oveq2d 6056 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  -> 
( T  gsumg  ( ( z  o F  +  w )  o F  .^  G
) )  =  ( T  gsumg  ( ( z  o F  .^  G )  o F  .x.  ( w  o F  .^  G
) ) ) )
27960adantr 452 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  ->  T  e. CMnd )
28020, 52, 30, 53, 279, 238, 246, 237psrbagev1 16521 . . . . . . . . . . 11  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  -> 
( ( z  o F  .^  G ) : I --> C  /\  ( `' ( z  o F  .^  G ) " ( _V  \  { ( 1r `  S ) } ) )  e.  Fin )
)
281280simpld 446 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  -> 
( z  o F 
.^  G ) : I --> C )
28220, 52, 30, 53, 279, 242, 246, 237psrbagev1 16521 . . . . . . . . . . 11  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  -> 
( ( w  o F  .^  G ) : I --> C  /\  ( `' ( w  o F  .^  G ) " ( _V  \  { ( 1r `  S ) } ) )  e.  Fin )
)
283282simpld 446 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  -> 
( w  o F 
.^  G ) : I --> C )
284280simprd 450 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  -> 
( `' ( z  o F  .^  G
) " ( _V 
\  { ( 1r
`  S ) } ) )  e.  Fin )
285282simprd 450 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  -> 
( `' ( w  o F  .^  G
) " ( _V 
\  { ( 1r
`  S ) } ) )  e.  Fin )
28652, 53, 233, 279, 237, 281, 283, 284, 285gsumadd 15483 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  -> 
( T  gsumg  ( ( z  o F  .^  G )  o F  .x.  ( w  o F  .^  G
) ) )  =  ( ( T  gsumg  ( z  o F  .^  G
) )  .x.  ( T  gsumg  ( w  o F 
.^  G ) ) ) )
287278, 286eqtrd 2436 . . . . . . . 8  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  -> 
( T  gsumg  ( ( z  o F  +  w )  o F  .^  G
) )  =  ( ( T  gsumg  ( z  o F 
.^  G ) ) 
.x.  ( T  gsumg  ( w  o F  .^  G
) ) ) )
288287adantrl 697 . . . . . . 7  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  -> 
( T  gsumg  ( ( z  o F  +  w )  o F  .^  G
) )  =  ( ( T  gsumg  ( z  o F 
.^  G ) ) 
.x.  ( T  gsumg  ( w  o F  .^  G
) ) ) )
289235, 288oveq12d 6058 . . . . . 6  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  -> 
( ( F `  ( ( x `  z ) ( .r
`  R ) ( y `  w ) ) )  .x.  ( T  gsumg  ( ( z  o F  +  w )  o F  .^  G
) ) )  =  ( ( ( F `
 ( x `  z ) )  .x.  ( F `  ( y `
 w ) ) )  .x.  ( ( T  gsumg  ( z  o F 
.^  G ) ) 
.x.  ( T  gsumg  ( w  o F  .^  G
) ) ) ) )
29060adantr 452 . . . . . . 7  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  ->  T  e. CMnd )
29170adantr 452 . . . . . . . 8  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  ->  F : K --> C )
292291, 225ffvelrnd 5830 . . . . . . 7  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  -> 
( F `  (
x `  z )
)  e.  C )
293291, 229ffvelrnd 5830 . . . . . . 7  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  -> 
( F `  (
y `  w )
)  e.  C )
29420, 52, 30, 53, 279, 238, 246, 237psrbagev2 16522 . . . . . . . 8  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  -> 
( T  gsumg  ( z  o F 
.^  G ) )  e.  C )
295294adantrl 697 . . . . . . 7  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  -> 
( T  gsumg  ( z  o F 
.^  G ) )  e.  C )
29620, 52, 30, 53, 279, 242, 246, 237psrbagev2 16522 . . . . . . . 8  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  -> 
( T  gsumg  ( w  o F 
.^  G ) )  e.  C )
297296adantrl 697 . . . . . . 7  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  -> 
( T  gsumg  ( w  o F 
.^  G ) )  e.  C )
29852, 233cmn4 15386 . . . . . . 7  |-  ( ( T  e. CMnd  /\  (
( F `  (
x `  z )
)  e.  C  /\  ( F `  ( y `
 w ) )  e.  C )  /\  ( ( T  gsumg  ( z  o F  .^  G
) )  e.  C  /\  ( T  gsumg  ( w  o F 
.^  G ) )  e.  C ) )  ->  ( ( ( F `  ( x `
 z ) ) 
.x.  ( F `  ( y `  w
) ) )  .x.  ( ( T  gsumg  ( z  o F  .^  G
) )  .x.  ( T  gsumg  ( w  o F 
.^  G ) ) ) )  =  ( ( ( F `  ( x `  z
) )  .x.  ( T  gsumg  ( z  o F 
.^  G ) ) )  .x.  ( ( F `  ( y `
 w ) ) 
.x.  ( T  gsumg  ( w  o F  .^  G
) ) ) ) )
299290, 292, 293, 295, 297, 298syl122anc 1193 . . . . . 6  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  -> 
( ( ( F `
 ( x `  z ) )  .x.  ( F `  ( y `
 w ) ) )  .x.  ( ( T  gsumg  ( z  o F 
.^  G ) ) 
.x.  ( T  gsumg  ( w  o F  .^  G
) ) ) )  =  ( ( ( F `  ( x `
 z ) ) 
.x.  ( T  gsumg  ( z  o F  .^  G
) ) )  .x.  ( ( F `  ( y `  w
) )  .x.  ( T  gsumg  ( w  o F 
.^  G ) ) ) ) )
300289, 299eqtrd 2436 . . . . 5  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  -> 
( ( F `  ( ( x `  z ) ( .r
`  R ) ( y `  w ) ) )  .x.  ( T  gsumg  ( ( z  o F  +  w )  o F  .^  G
) ) )  =  ( ( ( F `
 ( x `  z ) )  .x.  ( T  gsumg  ( z  o F 
.^  G ) ) )  .x.  ( ( F `  ( y `
 w ) ) 
.x.  ( T  gsumg  ( w  o F  .^  G
) ) ) ) )
3016adantr 452 . . . . . 6  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  ->  I  e.  _V )
3027adantr 452 . . . . . 6  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  ->  R  e.  CRing )
30313adantr 452 . . . . . 6  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  ->  S  e.  CRing )
30435adantr 452 . . . . . 6  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  ->  F  e.  ( R RingHom  S ) )
30537adantr 452 . . . . . 6  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  ->  G : I --> C )
30620psrbagaddcl 16390 . . . . . . 7  |-  ( ( I  e.  _V  /\  z  e.  D  /\  w  e.  D )  ->  ( z  o F  +  w )  e.  D )
307301, 224, 228, 306syl3anc 1184 . . . . . 6  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  -> 
( z  o F  +  w )  e.  D )
3089adantr 452 . . . . . . 7  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  ->  R  e.  Ring )
30916, 231rngcl 15632 . . . . . . 7  |-  ( ( R  e.  Ring  /\  (
x `  z )  e.  K  /\  (
y `  w )  e.  K )  ->  (
( x `  z
) ( .r `  R ) ( y `
 w ) )  e.  K )
310308, 225, 229, 309syl3anc 1184 . . . . . 6  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  -> 
( ( x `  z ) ( .r
`  R ) ( y `  w ) )  e.  K )
31110, 1, 28, 16, 20, 29, 30, 5, 31, 32, 301, 302, 303, 304, 305, 21, 307, 310evlslem3 19888 . . . . 5  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  -> 
( E `  (
v  e.  D  |->  if ( v  =  ( z  o F  +  w ) ,  ( ( x `  z
) ( .r `  R ) ( y `
 w ) ) ,  ( 0g `  R ) ) ) )  =  ( ( F `  ( ( x `  z ) ( .r `  R
) ( y `  w ) ) ) 
.x.  ( T  gsumg  ( ( z  o F  +  w )  o F 
.^  G ) ) ) )
31210, 1, 28, 16, 20, 29, 30, 5, 31, 32, 301, 302, 303, 304, 305, 21, 224, 225evlslem3 19888 . . . . . 6  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  -> 
( E `  (
v  e.  D  |->  if ( v  =  z ,  ( x `  z ) ,  ( 0g `  R ) ) ) )  =  ( ( F `  ( x `  z
) )  .x.  ( T  gsumg  ( z  o F 
.^  G ) ) ) )
31310, 1, 28, 16, 20, 29, 30, 5, 31, 32, 301, 302, 303, 304, 305, 21, 228, 229evlslem3 19888 . . . . . 6  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  -> 
( E `  (
v  e.  D  |->  if ( v  =  w ,  ( y `  w ) ,  ( 0g `  R ) ) ) )  =  ( ( F `  ( y `  w
) )  .x.  ( T  gsumg  ( w  o F 
.^  G ) ) ) )
314312, 313oveq12d 6058 . . . . 5  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  -> 
( ( E `  ( v  e.  D  |->  if ( v  =  z ,  ( x `
 z ) ,  ( 0g `  R
) ) ) ) 
.x.  ( E `  ( v  e.  D  |->  if ( v  =  w ,  ( y `
 w ) ,  ( 0g `  R
) ) ) ) )  =  ( ( ( F `  (
x `  z )
)  .x.  ( T  gsumg  ( z  o F  .^  G ) ) ) 
.x.  ( ( F `
 ( y `  w ) )  .x.  ( T  gsumg  ( w  o F 
.^  G ) ) ) ) )
315300, 311, 3143eqtr4d 2446 . . . 4  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  -> 
( E `  (
v  e.  D  |->  if ( v  =  ( z  o F  +  w ) ,  ( ( x `  z
) ( .r `  R ) ( y `
 w ) ) ,  ( 0g `  R ) ) ) )  =  ( ( E `  ( v  e.  D  |->  if ( v  =  z ,  ( x `  z
) ,  ( 0g
`  R ) ) ) )  .x.  ( E `  ( v  e.  D  |->  if ( v  =  w ,  ( y `  w
) ,  ( 0g
`  R ) ) ) ) ) )
31610, 1, 5, 21, 20, 6, 7, 13, 217, 315evlslem2 16523 . . 3  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( E `  (
x ( .r `  P ) y ) )  =  ( ( E `  x ) 
.x.  ( E `  y ) ) )
3171, 2, 3, 4, 5, 12, 15, 96, 316, 28, 97, 98, 121, 216isrhmd 15785 . 2  |-  ( ph  ->  E  e.  ( P RingHom  S ) )
318 ovex 6065 . . . . . 6  |-  ( S 
gsumg  ( b  e.  D  |->  ( ( F `  ( p `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) )  e. 
_V
319318, 32fnmpti 5532 . . . . 5  |-  E  Fn  B
320319a1i 11 . . . 4  |-  ( ph  ->  E  Fn  B )
32116, 1rhmf 15782 . . . . . 6  |-  ( A  e.  ( R RingHom  P
)  ->  A : K
--> B )
32290, 321syl 16 . . . . 5  |-  ( ph  ->  A : K --> B )
323 ffn 5550 . . . . 5  |-  ( A : K --> B  ->  A  Fn  K )
324322, 323syl 16 . . . 4  |-  ( ph  ->  A  Fn  K )
325 frn 5556 . . . . 5  |-  ( A : K --> B  ->  ran  A  C_  B )
326322, 325syl 16 . . . 4  |-  ( ph  ->  ran  A  C_  B
)
327 fnco 5512 . . . 4  |-  ( ( E  Fn  B  /\  A  Fn  K  /\  ran  A  C_  B )  ->  ( E  o.  A
)  Fn  K )
328320, 324, 326, 327syl3anc 1184 . . 3  |-  ( ph  ->  ( E  o.  A
)  Fn  K )
329 ffn 5550 . . . 4  |-  ( F : K --> C  ->  F  Fn  K )
33070, 329syl 16 . . 3  |-  ( ph  ->  F  Fn  K )
331 fvco2 5757 . . . . 5  |-  ( ( A  Fn  K  /\  x  e.  K )  ->  ( ( E  o.  A ) `  x
)  =  ( E `
 ( A `  x ) ) )
332324, 331sylan 458 . . . 4  |-  ( (
ph  /\  x  e.  K )  ->  (
( E  o.  A
) `  x )  =  ( E `  ( A `  x ) ) )
333332, 75eqtrd 2436 . . 3  |-  ( (
ph  /\  x  e.  K )  ->  (
( E  o.  A
) `  x )  =  ( F `  x ) )
334328, 330, 333eqfnfvd 5789 . 2  |-  ( ph  ->  ( E  o.  A
)  =  F )
33510, 31, 1, 6, 9mvrf2 16507 . . . . 5  |-  ( ph  ->  V : I --> B )
336 ffn 5550 . . . . 5  |-  ( V : I --> B  ->  V  Fn  I )
337335, 336syl 16 . . . 4  |-  ( ph  ->  V  Fn  I )
338 frn 5556 . . . . 5  |-  ( V : I --> B  ->  ran  V  C_  B )
339335, 338syl 16 . . . 4  |-  ( ph  ->  ran  V  C_  B
)
340 fnco 5512 . . . 4  |-  ( ( E  Fn  B  /\  V  Fn  I  /\  ran  V  C_  B )  ->  ( E  o.  V
)  Fn  I )
341320, 337, 339, 340syl3anc 1184 . . 3  |-  ( ph  ->  ( E  o.  V
)  Fn  I )
342 fvco2 5757 . . . . 5  |-  ( ( V  Fn  I  /\  x  e.  I )  ->  ( ( E  o.  V ) `  x
)  =  ( E `
 ( V `  x ) ) )
343337, 342sylan 458 . . . 4  |-  ( (
ph  /\  x  e.  I )  ->  (
( E  o.  V
) `  x )  =  ( E `  ( V `  x ) ) )
3446adantr 452 . . . . . . 7  |-  ( (
ph  /\  x  e.  I )  ->  I  e.  _V )
3457adantr 452 . . . . . . 7  |-  ( (
ph  /\  x  e.  I )  ->  R  e.  CRing )
346 simpr 448 . . . . . . 7  |-  ( (
ph  /\  x  e.  I )  ->  x  e.  I )
34731, 20, 21, 17, 344, 345, 346mvrval 16440 . . . . . 6  |-  ( (
ph  /\  x  e.  I )  ->  ( V `  x )  =  ( y  e.  D  |->  if ( y  =  ( z  e.  I  |->  if ( z  =  x ,  1 ,  0 ) ) ,  ( 1r `  R ) ,  ( 0g `  R ) ) ) )
348347fveq2d 5691 . . . . 5  |-  ( (
ph  /\  x  e.  I )  ->  ( E `  ( V `  x ) )  =  ( E `  (
y  e.  D  |->  if ( y  =  ( z  e.  I  |->  if ( z  =  x ,  1 ,  0 ) ) ,  ( 1r `  R ) ,  ( 0g `  R ) ) ) ) )
34913adantr 452 . . . . . 6  |-  ( (
ph  /\  x  e.  I )  ->  S  e.  CRing )
35035adantr 452 . . . . . 6  |-  ( (
ph  /\  x  e.  I )  ->  F  e.  ( R RingHom  S )
)
35137adantr 452 . . . . . 6  |-  ( (
ph  /\  x  e.  I )  ->  G : I --> C )
35220psrbagsn 16510 . . . . . . . 8  |-  ( I  e.  _V  ->  (
z  e.  I  |->  if ( z  =  x ,  1 ,  0 ) )  e.  D
)
3536, 352syl 16 . . . . . . 7  |-  ( ph  ->  ( z  e.  I  |->  if ( z  =  x ,  1 ,  0 ) )  e.  D )
354353adantr 452 . . . . . 6  |-  ( (
ph  /\  x  e.  I )  ->  (
z  e.  I  |->  if ( z  =  x ,  1 ,  0 ) )  e.  D
)
35519adantr 452 . . . . . 6  |-  ( (
ph  /\  x  e.  I )  ->  ( 1r `  R )  e.  K )
35610, 1, 28, 16, 20, 29, 30, 5, 31, 32, 344, 345, 349, 350, 351, 21, 354, 355evlslem3 19888 . . . . 5  |-  ( (
ph  /\  x  e.  I )  ->  ( E `  ( y  e.  D  |->  if ( y  =  ( z  e.  I  |->  if ( z  =  x ,  1 ,  0 ) ) ,  ( 1r
`  R ) ,  ( 0g `  R
) ) ) )  =  ( ( F `
 ( 1r `  R ) )  .x.  ( T  gsumg  ( ( z  e.  I  |->  if ( z  =  x ,  1 ,  0 ) )  o F  .^  G
) ) ) )
35795adantr 452 . . . . . . 7  |-  ( (
ph  /\  x  e.  I )  ->  ( F `  ( 1r `  R ) )  =  ( 1r `  S
) )
358 1nn0 10193 . . . . . . . . . . . . . 14  |-  1  e.  NN0
359 0nn0 10192 . . . . . . . . . . . . . 14  |-  0  e.  NN0
360358, 359keepel 3756 . . . . . . . . . . . . 13  |-  if ( z  =  x ,  1 ,  0 )  e.  NN0
361360a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  I )  ->  if ( z  =  x ,  1 ,  0 )  e.  NN0 )
36237ffvelrnda 5829 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  I )  ->  ( G `  z )  e.  C )
363 eqidd 2405 . . . . . . . . . . . 12  |-  ( ph  ->  ( z  e.  I  |->  if ( z  =  x ,  1 ,  0 ) )  =  ( z  e.  I  |->  if ( z  =  x ,  1 ,  0 ) ) )
36437feqmptd 5738 . . . . . . . . . . . 12  |-  ( ph  ->  G  =  ( z  e.  I  |->  ( G `
 z ) ) )
3656, 361, 362, 363, 364offval2 6281 . . . . . . . . . . 11  |-  ( ph  ->  ( ( z  e.  I  |->  if ( z  =  x ,  1 ,  0 ) )  o F  .^  G
)  =  ( z  e.  I  |->  ( if ( z  =  x ,  1 ,  0 )  .^  ( G `  z ) ) ) )
366 oveq1 6047 . . . . . . . . . . . . . 14  |-  ( 1  =  if ( z  =  x ,  1 ,  0 )  -> 
( 1  .^  ( G `  z )
)  =  ( if ( z  =  x ,  1 ,  0 )  .^  ( G `  z ) ) )
367366eqeq1d 2412 . . . . . . . . . . . . 13  |-  ( 1  =  if ( z  =  x ,  1 ,  0 )  -> 
( ( 1  .^  ( G `  z ) )  =  if ( z  =  x ,  ( G `  z
) ,  ( 1r
`  S ) )  <-> 
( if ( z  =  x ,  1 ,  0 )  .^  ( G `  z ) )  =  if ( z  =  x ,  ( G `  z
) ,  ( 1r
`  S ) ) ) )
368 oveq1 6047 . . . . . . . . . . . . . 14  |-  ( 0  =  if ( z  =  x ,  1 ,  0 )  -> 
( 0  .^  ( G `  z )
)  =  ( if ( z  =  x ,  1 ,  0 )  .^  ( G `  z ) ) )
369368eqeq1d 2412 . . . . . . . . . . . . 13  |-  ( 0  =  if ( z  =  x ,  1 ,  0 )  -> 
( ( 0  .^  ( G `  z ) )  =  if ( z  =  x ,  ( G `  z
) ,  ( 1r
`  S ) )  <-> 
( if ( z  =  x ,  1 ,  0 )  .^  ( G `  z ) )  =  if ( z  =  x ,  ( G `  z
) ,  ( 1r
`  S ) ) ) )
370362adantr 452 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  z  e.  I )  /\  z  =  x )  ->  ( G `  z )  e.  C )
37152, 30mulg1 14852 . . . . . . . . . . . . . . 15  |-  ( ( G `  z )  e.  C  ->  (
1  .^  ( G `  z ) )  =  ( G `  z
) )
372370, 371syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  z  e.  I )  /\  z  =  x )  ->  (
1  .^  ( G `  z ) )  =  ( G `  z
) )
373 iftrue 3705 . . . . . . . . . . . . . . 15  |-  ( z  =  x  ->  if ( z  =  x ,  ( G `  z ) ,  ( 1r `  S ) )  =  ( G `
 z ) )
374373adantl 453 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  z  e.  I )  /\  z  =  x )  ->  if ( z  =  x ,  ( G `  z ) ,  ( 1r `  S ) )  =  ( G `
 z ) )
375372, 374eqtr4d 2439 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  z  e.  I )  /\  z  =  x )  ->  (
1  .^  ( G `  z ) )  =  if ( z  =  x ,  ( G `
 z ) ,  ( 1r `  S
) ) )
37652, 53, 30mulg0 14850 . . . . . . . . . . . . . . . 16  |-  ( ( G `  z )  e.  C  ->  (
0  .^  ( G `  z ) )  =  ( 1r `  S
) )
377362, 376syl 16 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  z  e.  I )  ->  (
0  .^  ( G `  z ) )  =  ( 1r `  S
) )
378377adantr 452 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  z  e.  I )  /\  -.  z  =  x )  ->  ( 0  .^  ( G `  z )
)  =  ( 1r
`  S ) )
379 iffalse 3706 . . . . . . . . . . . . . . 15  |-  ( -.  z  =  x  ->  if ( z  =  x ,  ( G `  z ) ,  ( 1r `  S ) )  =  ( 1r
`  S ) )
380379adantl 453 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  z  e.  I )  /\  -.  z  =  x )  ->  if ( z  =  x ,  ( G `
 z ) ,  ( 1r `  S
) )  =  ( 1r `  S ) )
381378, 380eqtr4d 2439 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  z  e.  I )  /\  -.  z  =  x )  ->  ( 0  .^  ( G `  z )
)  =  if ( z  =  x ,  ( G `  z
) ,  ( 1r
`  S ) ) )
382367, 369, 375, 381ifbothda 3729 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  I )  ->  ( if ( z  =  x ,  1 ,  0 )  .^  ( G `  z ) )  =  if ( z  =  x ,  ( G `
 z ) ,  ( 1r `  S
) ) )
383382mpteq2dva 4255 . . . . . . . . . . 11  |-  ( ph  ->  ( z  e.  I  |->  ( if ( z  =  x ,  1 ,  0 )  .^  ( G `  z ) ) )  =  ( z  e.  I  |->  if ( z  =  x ,  ( G `  z ) ,  ( 1r `  S ) ) ) )
384365, 383eqtrd 2436 . . . . . . . . . 10  |-  ( ph  ->  ( ( z  e.  I  |->  if ( z  =  x ,  1 ,  0 ) )  o F  .^  G
)  =  ( z  e.  I  |->  if ( z  =  x ,  ( G `  z
) ,  ( 1r
`  S ) ) ) )
385384adantr 452 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  I )  ->  (
( z  e.  I  |->  if ( z  =  x ,  1 ,  0 ) )  o F  .^  G )  =  ( z  e.  I  |->  if ( z  =  x ,  ( G `  z ) ,  ( 1r `  S ) ) ) )
386385oveq2d 6056 . . . . . . . 8  |-  ( (
ph  /\  x  e.  I )  ->  ( T  gsumg  ( ( z  e.  I  |->  if ( z  =  x ,  1 ,  0 ) )  o F  .^  G
) )  =  ( T  gsumg  ( z  e.  I  |->  if ( z  =  x ,  ( G `
 z ) ,  ( 1r `  S
) ) ) ) )
38762adantr 452 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  I )  ->  T  e.  Mnd )
388362adantlr 696 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  I )  /\  z  e.  I )  ->  ( G `  z )  e.  C )
38928, 3rngidcl 15639 . . . . . . . . . . . . 13  |-  ( S  e.  Ring  ->  ( 1r
`  S )  e.  C )
39015, 389syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1r `  S
)  e.  C )
391390ad2antrr 707 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  I )  /\  z  e.  I )  ->  ( 1r `  S )  e.  C )
392 ifcl 3735 . . . . . . . . . . 11  |-  ( ( ( G `  z
)  e.  C  /\  ( 1r `  S )  e.  C )  ->  if ( z  =  x ,  ( G `  z ) ,  ( 1r `  S ) )  e.  C )
393388, 391, 392syl2anc 643 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  I )  /\  z  e.  I )  ->  if ( z  =  x ,  ( G `  z ) ,  ( 1r `  S ) )  e.  C )
394 eqid 2404 . . . . . . . . . 10  |-  ( z  e.  I  |->  if ( z  =  x ,  ( G `  z
) ,  ( 1r
`  S ) ) )  =  ( z  e.  I  |->  if ( z  =  x ,  ( G `  z
) ,  ( 1r
`  S ) ) )
395393, 394fmptd 5852 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  I )  ->  (
z  e.  I  |->  if ( z  =  x ,  ( G `  z ) ,  ( 1r `  S ) ) ) : I --> C )
396 eldifn 3430 . . . . . . . . . . . . 13  |-  ( z  e.  ( I  \  { x } )  ->  -.  z  e.  { x } )
397 elsn 3789 . . . . . . . . . . . . 13  |-  ( z  e.  { x }  <->  z  =  x )
398396, 397sylnib 296 . . . . . . . . . . . 12  |-  ( z  e.  ( I  \  { x } )  ->  -.  z  =  x )
399398, 379syl 16 . . . . . . . . . . 11  |-  ( z  e.  ( I  \  { x } )  ->  if ( z  =  x ,  ( G `  z ) ,  ( 1r `  S ) )  =  ( 1r `  S
) )
400399adantl 453 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  I )  /\  z  e.  ( I  \  {
x } ) )  ->  if ( z  =  x ,  ( G `  z ) ,  ( 1r `  S ) )  =  ( 1r `  S
) )
401400suppss2 6259 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  I )  ->  ( `' ( z  e.  I  |->  if ( z  =  x ,  ( G `  z ) ,  ( 1r `  S ) ) )
" ( _V  \  { ( 1r `  S ) } ) )  C_  { x } )
40252, 53, 387, 344, 346, 395, 401gsumpt 15500 . . . . . . . 8  |-  ( (
ph  /\  x  e.  I )  ->  ( T  gsumg  ( z  e.  I  |->  if ( z  =  x ,  ( G `
 z ) ,  ( 1r `  S
) ) ) )  =  ( ( z  e.  I  |->  if ( z  =  x ,  ( G `  z
) ,  ( 1r
`  S ) ) ) `  x ) )
403 fveq2 5687 . . . . . . . . . . 11  |-  ( z  =  x  ->  ( G `  z )  =  ( G `  x ) )
404373, 403eqtrd 2436 . . . . . . . . . 10  |-  ( z  =  x  ->  if ( z  =  x ,  ( G `  z ) ,  ( 1r `  S ) )  =  ( G `
 x ) )
405404, 394, 45fvmpt 5765 . . . . . . . . 9  |-  ( x  e.  I  ->  (
( z  e.  I  |->  if ( z  =  x ,  ( G `
 z ) ,  ( 1r `  S
) ) ) `  x )  =  ( G `  x ) )
406405adantl 453 . . . . . . . 8  |-  ( (
ph  /\  x  e.  I )  ->  (
( z  e.  I  |->  if ( z  =  x ,  ( G `
 z ) ,  ( 1r `  S
) ) ) `  x )  =  ( G `  x ) )
407386, 402, 4063eqtrd 2440 . . . . . . 7  |-  ( (
ph  /\  x  e.  I )  ->  ( T  gsumg  ( ( z  e.  I  |->  if ( z  =  x ,  1 ,  0 ) )  o F  .^  G
) )  =  ( G `  x ) )
408357, 407oveq12d 6058 . . . . . 6  |-  ( (
ph  /\  x  e.  I )  ->  (
( F `  ( 1r `  R ) ) 
.x.  ( T  gsumg  ( ( z  e.  I  |->  if ( z  =  x ,  1 ,  0 ) )  o F 
.^  G ) ) )  =  ( ( 1r `  S ) 
.x.  ( G `  x ) ) )
40915adantr 452 . . . . . . 7  |-  ( (
ph  /\  x  e.  I )  ->  S  e.  Ring )
41028, 5, 3rnglidm 15642 . . . . . . 7  |-  ( ( S  e.  Ring  /\  ( G `  x )  e.  C )  ->  (
( 1r `  S
)  .x.  ( G `  x ) )  =  ( G `  x
) )
411409, 51, 410syl2anc 643 . . . . . 6  |-  ( (
ph  /\  x  e.  I )  ->  (
( 1r `  S
)  .x.  ( G `  x ) )  =  ( G `  x
) )
412408, 411eqtrd 2436 . . . . 5  |-  ( (
ph  /\  x  e.  I )  ->  (
( F `  ( 1r `  R ) ) 
.x.  ( T  gsumg  ( ( z  e.  I  |->  if ( z  =  x ,  1 ,  0 ) )  o F 
.^  G ) ) )  =  ( G `
 x ) )
413348, 356, 4123eqtrd 2440 . . . 4  |-  ( (
ph  /\  x  e.  I )  ->  ( E `  ( V `  x ) )  =  ( G `  x
) )
414343, 413eqtrd 2436 . . 3  |-  ( (
ph  /\  x  e.  I )  ->  (
( E  o.  V
) `  x )  =  ( G `  x ) )
415341, 271, 414eqfnfvd 5789 . 2  |-  ( ph  ->  ( E  o.  V
)  =  G )
416317, 334, 4153jca 1134 1  |-  ( ph  ->  ( E  e.  ( P RingHom  S )  /\  ( E  o.  A )  =  F  /\  ( E  o.  V )  =  G ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 359    /\ w3a 936    = wceq 1649    e. wcel 1721   A.wral 2666   {crab 2670   _Vcvv 2916    \ cdif 3277    C_ wss 3280   ifcif 3699   {csn 3774    e. cmpt 4226    X. cxp 4835   `'ccnv 4836   ran crn 4838   "cima 4840    o. ccom 4841    Fn wfn 5408   -->wf 5409   ` cfv 5413  (class class class)co 6040    o Fcof 6262    ^m cmap 6977   Fincfn 7068   0cc0 8946   1c1 8947    + caddc 8949   NNcn 9956   NN0cn0 10177   ZZcz 10238   Basecbs 13424   +g cplusg 13484   .rcmulr 13485  Scalarcsca 13487   0gc0g 13678    gsumg cgsu 13679   Mndcmnd 14639   Grpcgrp 14640  .gcmg 14644   MndHom cmhm 14691    GrpHom cghm 14958  CMndccmn 15367  mulGrpcmgp 15603   Ringcrg 15615   CRingccrg 15616   1rcur 15617   RingHom crh 15772  AssAlgcasa 16324  algSccascl 16326   mVar cmvr 16362   mPoly cmpl 16363
This theorem is referenced by:  evlseu  19890
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-inf2 7552  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-iin 4056  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-of 6264  df-ofr 6265  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-2o 6684  df-oadd 6687  df-er 6864  df-map 6979  df-pm 6980  df-ixp 7023  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-oi 7435  df-card 7782  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-nn 9957  df-2 10014  df-3 10015  df-4 10016  df-5 10017  df-6 10018  df-7 10019  df-8 10020  df-9 10021  df-n0 10178  df-z 10239  df-uz 10445  df-fz 11000  df-fzo 11091  df-seq 11279  df-hash 11574  df-struct 13426  df-ndx 13427  df-slot 13428  df-base 13429  df-sets 13430  df-ress 13431  df-plusg 13497  df-mulr 13498  df-sca 13500  df-vsca 13501  df-tset 13503  df-0g 13682  df-gsum 13683  df-mre 13766  df-mrc 13767  df-acs 13769  df-mnd 14645  df-mhm 14693  df-submnd 14694  df-grp 14767  df-minusg 14768  df-sbg 14769  df-mulg 14770  df-subg 14896  df-ghm 14959  df-cntz 15071  df-cmn 15369  df-abl 15370  df-mgp 15604  df-rng 15618  df-cring 15619  df-ur 15620  df-rnghom 15774  df-subrg 15821  df-lmod 15907  df-lss 15964  df-assa 16327  df-ascl 16329  df-psr 16372  df-mvr 16373  df-mpl 16374
  Copyright terms: Public domain W3C validator