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

Theorem evlslem1 19415
Description: Lemma for evlseu 19416, 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 2296 . . 3  |-  ( 1r
`  P )  =  ( 1r `  P
)
3 eqid 2296 . . 3  |-  ( 1r
`  S )  =  ( 1r `  S
)
4 eqid 2296 . . 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 15367 . . . . 5  |-  ( R  e.  CRing  ->  R  e.  Ring )
97, 8syl 15 . . . 4  |-  ( ph  ->  R  e.  Ring )
10 evlslem1.p . . . . 5  |-  P  =  ( I mPoly  R )
1110mplrng 16212 . . . 4  |-  ( ( I  e.  _V  /\  R  e.  Ring )  ->  P  e.  Ring )
126, 9, 11syl2anc 642 . . 3  |-  ( ph  ->  P  e.  Ring )
13 evlslem1.s . . . 4  |-  ( ph  ->  S  e.  CRing )
14 crngrng 15367 . . . 4  |-  ( S  e.  CRing  ->  S  e.  Ring )
1513, 14syl 15 . . 3  |-  ( ph  ->  S  e.  Ring )
16 evlslem1.k . . . . . . 7  |-  K  =  ( Base `  R
)
17 eqid 2296 . . . . . . 7  |-  ( 1r
`  R )  =  ( 1r `  R
)
1816, 17rngidcl 15377 . . . . . 6  |-  ( R  e.  Ring  ->  ( 1r
`  R )  e.  K )
199, 18syl 15 . . . . 5  |-  ( ph  ->  ( 1r `  R
)  e.  K )
20 evlslem1.d . . . . . . . . 9  |-  D  =  { h  e.  ( NN0  ^m  I )  |  ( `' h " NN )  e.  Fin }
21 eqid 2296 . . . . . . . . 9  |-  ( 0g
`  R )  =  ( 0g `  R
)
22 evlslem1.a . . . . . . . . 9  |-  A  =  (algSc `  P )
236adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  K )  ->  I  e.  _V )
249adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  K )  ->  R  e.  Ring )
25 simpr 447 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  K )  ->  x  e.  K )
2610, 20, 21, 16, 22, 23, 24, 25mplascl 16253 . . . . . . . 8  |-  ( (
ph  /\  x  e.  K )  ->  ( A `  x )  =  ( y  e.  D  |->  if ( y  =  ( I  X.  { 0 } ) ,  x ,  ( 0g `  R ) ) ) )
2726fveq2d 5545 . . . . . . 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 451 . . . . . . . 8  |-  ( (
ph  /\  x  e.  K )  ->  R  e.  CRing )
3413adantr 451 . . . . . . . 8  |-  ( (
ph  /\  x  e.  K )  ->  S  e.  CRing )
35 evlslem1.f . . . . . . . . 9  |-  ( ph  ->  F  e.  ( R RingHom  S ) )
3635adantr 451 . . . . . . . 8  |-  ( (
ph  /\  x  e.  K )  ->  F  e.  ( R RingHom  S )
)
37 evlslem1.g . . . . . . . . 9  |-  ( ph  ->  G : I --> C )
3837adantr 451 . . . . . . . 8  |-  ( (
ph  /\  x  e.  K )  ->  G : I --> C )
3920psrbag0 16251 . . . . . . . . . 10  |-  ( I  e.  _V  ->  (
I  X.  { 0 } )  e.  D
)
406, 39syl 15 . . . . . . . . 9  |-  ( ph  ->  ( I  X.  {
0 } )  e.  D )
4140adantr 451 . . . . . . . 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 19414 . . . . . . 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 10051 . . . . . . . . . . . . . . 15  |-  0  e.  ZZ
4443a1i 10 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  I )  ->  0  e.  ZZ )
45 fvex 5555 . . . . . . . . . . . . . . 15  |-  ( G `
 x )  e. 
_V
4645a1i 10 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  I )  ->  ( G `  x )  e.  _V )
47 fconstmpt 4748 . . . . . . . . . . . . . . 15  |-  ( I  X.  { 0 } )  =  ( x  e.  I  |->  0 )
4847a1i 10 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( I  X.  {
0 } )  =  ( x  e.  I  |->  0 ) )
4937feqmptd 5591 . . . . . . . . . . . . . 14  |-  ( ph  ->  G  =  ( x  e.  I  |->  ( G `
 x ) ) )
506, 44, 46, 48, 49offval2 6111 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( I  X.  { 0 } )  o F  .^  G
)  =  ( x  e.  I  |->  ( 0 
.^  ( G `  x ) ) ) )
51 ffvelrn 5679 . . . . . . . . . . . . . . . 16  |-  ( ( G : I --> C  /\  x  e.  I )  ->  ( G `  x
)  e.  C )
5237, 51sylan 457 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  I )  ->  ( G `  x )  e.  C )
5329, 28mgpbas 15347 . . . . . . . . . . . . . . . 16  |-  C  =  ( Base `  T
)
5429, 3rngidval 15359 . . . . . . . . . . . . . . . 16  |-  ( 1r
`  S )  =  ( 0g `  T
)
5553, 54, 30mulg0 14588 . . . . . . . . . . . . . . 15  |-  ( ( G `  x )  e.  C  ->  (
0  .^  ( G `  x ) )  =  ( 1r `  S
) )
5652, 55syl 15 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  I )  ->  (
0  .^  ( G `  x ) )  =  ( 1r `  S
) )
5756mpteq2dva 4122 . . . . . . . . . . . . 13  |-  ( ph  ->  ( x  e.  I  |->  ( 0  .^  ( G `  x )
) )  =  ( x  e.  I  |->  ( 1r `  S ) ) )
5850, 57eqtrd 2328 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( I  X.  { 0 } )  o F  .^  G
)  =  ( x  e.  I  |->  ( 1r
`  S ) ) )
5958oveq2d 5890 . . . . . . . . . . 11  |-  ( ph  ->  ( T  gsumg  ( ( I  X.  { 0 } )  o F  .^  G
) )  =  ( T  gsumg  ( x  e.  I  |->  ( 1r `  S
) ) ) )
6029crngmgp 15365 . . . . . . . . . . . . . 14  |-  ( S  e.  CRing  ->  T  e. CMnd )
6113, 60syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  T  e. CMnd )
62 cmnmnd 15120 . . . . . . . . . . . . 13  |-  ( T  e. CMnd  ->  T  e.  Mnd )
6361, 62syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  T  e.  Mnd )
6454gsumz 14474 . . . . . . . . . . . 12  |-  ( ( T  e.  Mnd  /\  I  e.  _V )  ->  ( T  gsumg  ( x  e.  I  |->  ( 1r `  S
) ) )  =  ( 1r `  S
) )
6563, 6, 64syl2anc 642 . . . . . . . . . . 11  |-  ( ph  ->  ( T  gsumg  ( x  e.  I  |->  ( 1r `  S
) ) )  =  ( 1r `  S
) )
6659, 65eqtrd 2328 . . . . . . . . . 10  |-  ( ph  ->  ( T  gsumg  ( ( I  X.  { 0 } )  o F  .^  G
) )  =  ( 1r `  S ) )
6766adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  K )  ->  ( T  gsumg  ( ( I  X.  { 0 } )  o F  .^  G
) )  =  ( 1r `  S ) )
6867oveq2d 5890 . . . . . . . 8  |-  ( (
ph  /\  x  e.  K )  ->  (
( F `  x
)  .x.  ( T  gsumg  ( ( I  X.  {
0 } )  o F  .^  G )
) )  =  ( ( F `  x
)  .x.  ( 1r `  S ) ) )
6915adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  K )  ->  S  e.  Ring )
7016, 28rhmf 15520 . . . . . . . . . . 11  |-  ( F  e.  ( R RingHom  S
)  ->  F : K
--> C )
7135, 70syl 15 . . . . . . . . . 10  |-  ( ph  ->  F : K --> C )
72 ffvelrn 5679 . . . . . . . . . 10  |-  ( ( F : K --> C  /\  x  e.  K )  ->  ( F `  x
)  e.  C )
7371, 72sylan 457 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  K )  ->  ( F `  x )  e.  C )
7428, 5, 3rngridm 15381 . . . . . . . . 9  |-  ( ( S  e.  Ring  /\  ( F `  x )  e.  C )  ->  (
( F `  x
)  .x.  ( 1r `  S ) )  =  ( F `  x
) )
7569, 73, 74syl2anc 642 . . . . . . . 8  |-  ( (
ph  /\  x  e.  K )  ->  (
( F `  x
)  .x.  ( 1r `  S ) )  =  ( F `  x
) )
7668, 75eqtrd 2328 . . . . . . 7  |-  ( (
ph  /\  x  e.  K )  ->  (
( F `  x
)  .x.  ( T  gsumg  ( ( I  X.  {
0 } )  o F  .^  G )
) )  =  ( F `  x ) )
7727, 42, 763eqtrd 2332 . . . . . 6  |-  ( (
ph  /\  x  e.  K )  ->  ( E `  ( A `  x ) )  =  ( F `  x
) )
7877ralrimiva 2639 . . . . 5  |-  ( ph  ->  A. x  e.  K  ( E `  ( A `
 x ) )  =  ( F `  x ) )
79 fveq2 5541 . . . . . . . 8  |-  ( x  =  ( 1r `  R )  ->  ( A `  x )  =  ( A `  ( 1r `  R ) ) )
8079fveq2d 5545 . . . . . . 7  |-  ( x  =  ( 1r `  R )  ->  ( E `  ( A `  x ) )  =  ( E `  ( A `  ( 1r `  R ) ) ) )
81 fveq2 5541 . . . . . . 7  |-  ( x  =  ( 1r `  R )  ->  ( F `  x )  =  ( F `  ( 1r `  R ) ) )
8280, 81eqeq12d 2310 . . . . . 6  |-  ( x  =  ( 1r `  R )  ->  (
( E `  ( A `  x )
)  =  ( F `
 x )  <->  ( E `  ( A `  ( 1r `  R ) ) )  =  ( F `
 ( 1r `  R ) ) ) )
8382rspcva 2895 . . . . 5  |-  ( ( ( 1r `  R
)  e.  K  /\  A. x  e.  K  ( E `  ( A `
 x ) )  =  ( F `  x ) )  -> 
( E `  ( A `  ( 1r `  R ) ) )  =  ( F `  ( 1r `  R ) ) )
8419, 78, 83syl2anc 642 . . . 4  |-  ( ph  ->  ( E `  ( A `  ( 1r `  R ) ) )  =  ( F `  ( 1r `  R ) ) )
8510mplassa 16214 . . . . . . . . 9  |-  ( ( I  e.  _V  /\  R  e.  CRing )  ->  P  e. AssAlg )
866, 7, 85syl2anc 642 . . . . . . . 8  |-  ( ph  ->  P  e. AssAlg )
87 eqid 2296 . . . . . . . . 9  |-  (Scalar `  P )  =  (Scalar `  P )
8822, 87asclrhm 16097 . . . . . . . 8  |-  ( P  e. AssAlg  ->  A  e.  ( (Scalar `  P ) RingHom  P ) )
8986, 88syl 15 . . . . . . 7  |-  ( ph  ->  A  e.  ( (Scalar `  P ) RingHom  P ) )
9010, 6, 7mplsca 16205 . . . . . . . 8  |-  ( ph  ->  R  =  (Scalar `  P ) )
9190oveq1d 5889 . . . . . . 7  |-  ( ph  ->  ( R RingHom  P )  =  ( (Scalar `  P ) RingHom  P ) )
9289, 91eleqtrrd 2373 . . . . . 6  |-  ( ph  ->  A  e.  ( R RingHom  P ) )
9317, 2rhm1 15524 . . . . . 6  |-  ( A  e.  ( R RingHom  P
)  ->  ( A `  ( 1r `  R
) )  =  ( 1r `  P ) )
9492, 93syl 15 . . . . 5  |-  ( ph  ->  ( A `  ( 1r `  R ) )  =  ( 1r `  P ) )
9594fveq2d 5545 . . . 4  |-  ( ph  ->  ( E `  ( A `  ( 1r `  R ) ) )  =  ( E `  ( 1r `  P ) ) )
9617, 3rhm1 15524 . . . . 5  |-  ( F  e.  ( R RingHom  S
)  ->  ( F `  ( 1r `  R
) )  =  ( 1r `  S ) )
9735, 96syl 15 . . . 4  |-  ( ph  ->  ( F `  ( 1r `  R ) )  =  ( 1r `  S ) )
9884, 95, 973eqtr3d 2336 . . 3  |-  ( ph  ->  ( E `  ( 1r `  P ) )  =  ( 1r `  S ) )
99 eqid 2296 . . . . 5  |-  ( +g  `  P )  =  ( +g  `  P )
100 eqid 2296 . . . . 5  |-  ( +g  `  S )  =  ( +g  `  S )
101 rnggrp 15362 . . . . . 6  |-  ( P  e.  Ring  ->  P  e. 
Grp )
10212, 101syl 15 . . . . 5  |-  ( ph  ->  P  e.  Grp )
103 rnggrp 15362 . . . . . 6  |-  ( S  e.  Ring  ->  S  e. 
Grp )
10415, 103syl 15 . . . . 5  |-  ( ph  ->  S  e.  Grp )
105 eqid 2296 . . . . . . 7  |-  ( 0g
`  S )  =  ( 0g `  S
)
106 rngcmn 15387 . . . . . . . . 9  |-  ( S  e.  Ring  ->  S  e. CMnd
)
10715, 106syl 15 . . . . . . . 8  |-  ( ph  ->  S  e. CMnd )
108107adantr 451 . . . . . . 7  |-  ( (
ph  /\  p  e.  B )  ->  S  e. CMnd )
109 ovex 5899 . . . . . . . . . 10  |-  ( NN0 
^m  I )  e. 
_V
110109rabex 4181 . . . . . . . . 9  |-  { h  e.  ( NN0  ^m  I
)  |  ( `' h " NN )  e.  Fin }  e.  _V
11120, 110eqeltri 2366 . . . . . . . 8  |-  D  e. 
_V
112111a1i 10 . . . . . . 7  |-  ( (
ph  /\  p  e.  B )  ->  D  e.  _V )
1136adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  p  e.  B )  ->  I  e.  _V )
1147adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  p  e.  B )  ->  R  e.  CRing )
11513adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  p  e.  B )  ->  S  e.  CRing )
11635adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  p  e.  B )  ->  F  e.  ( R RingHom  S )
)
11737adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  p  e.  B )  ->  G : I --> C )
118 simpr 447 . . . . . . . . 9  |-  ( (
ph  /\  p  e.  B )  ->  p  e.  B )
11910, 1, 28, 16, 20, 29, 30, 5, 31, 32, 113, 114, 115, 116, 117, 118evlslem6 19413 . . . . . . . 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 ) )
120119simpld 445 . . . . . . 7  |-  ( (
ph  /\  p  e.  B )  ->  (
b  e.  D  |->  ( ( F `  (
p `  b )
)  .x.  ( T  gsumg  ( b  o F  .^  G ) ) ) ) : D --> C )
121119simprd 449 . . . . . . 7  |-  ( (
ph  /\  p  e.  B )  ->  ( `' ( b  e.  D  |->  ( ( F `
 ( p `  b ) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) " ( _V  \  { ( 0g
`  S ) } ) )  e.  Fin )
12228, 105, 108, 112, 120, 121gsumcl 15214 . . . . . 6  |-  ( (
ph  /\  p  e.  B )  ->  ( S  gsumg  ( b  e.  D  |->  ( ( F `  ( p `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) )  e.  C )
123122, 32fmptd 5700 . . . . 5  |-  ( ph  ->  E : B --> C )
124 eqid 2296 . . . . . . . . . . . . . . . . 17  |-  ( +g  `  R )  =  ( +g  `  R )
125 simplrl 736 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  x  e.  B )
126 simplrr 737 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  y  e.  B )
12710, 1, 124, 99, 125, 126mpladd 16202 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  (
x ( +g  `  P
) y )  =  ( x  o F ( +g  `  R
) y ) )
128127fveq1d 5543 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  (
( x ( +g  `  P ) y ) `
 b )  =  ( ( x  o F ( +g  `  R
) y ) `  b ) )
129 simprl 732 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  ->  x  e.  B )
13010, 16, 1, 20, 129mplelf 16194 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  ->  x : D --> K )
131 ffn 5405 . . . . . . . . . . . . . . . . . 18  |-  ( x : D --> K  ->  x  Fn  D )
132130, 131syl 15 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  ->  x  Fn  D )
133132adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  x  Fn  D )
134 simprr 733 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
y  e.  B )
13510, 16, 1, 20, 134mplelf 16194 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
y : D --> K )
136 ffn 5405 . . . . . . . . . . . . . . . . . 18  |-  ( y : D --> K  -> 
y  Fn  D )
137135, 136syl 15 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
y  Fn  D )
138137adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  y  Fn  D )
139111a1i 10 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  D  e.  _V )
140 simpr 447 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  b  e.  D )
141 fnfvof 6106 . . . . . . . . . . . . . . . 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 ) ) )
142133, 138, 139, 140, 141syl22anc 1183 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  (
( x  o F ( +g  `  R
) y ) `  b )  =  ( ( x `  b
) ( +g  `  R
) ( y `  b ) ) )
143128, 142eqtrd 2328 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  (
( x ( +g  `  P ) y ) `
 b )  =  ( ( x `  b ) ( +g  `  R ) ( y `
 b ) ) )
144143fveq2d 5545 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  ( F `  ( (
x ( +g  `  P
) y ) `  b ) )  =  ( F `  (
( x `  b
) ( +g  `  R
) ( y `  b ) ) ) )
145 rhmghm 15519 . . . . . . . . . . . . . . . 16  |-  ( F  e.  ( R RingHom  S
)  ->  F  e.  ( R  GrpHom  S ) )
14635, 145syl 15 . . . . . . . . . . . . . . 15  |-  ( ph  ->  F  e.  ( R 
GrpHom  S ) )
147146ad2antrr 706 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  F  e.  ( R  GrpHom  S ) )
148 ffvelrn 5679 . . . . . . . . . . . . . . 15  |-  ( ( x : D --> K  /\  b  e.  D )  ->  ( x `  b
)  e.  K )
149130, 148sylan 457 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  (
x `  b )  e.  K )
150 ffvelrn 5679 . . . . . . . . . . . . . . 15  |-  ( ( y : D --> K  /\  b  e.  D )  ->  ( y `  b
)  e.  K )
151135, 150sylan 457 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  (
y `  b )  e.  K )
15216, 124, 100ghmlin 14704 . . . . . . . . . . . . . 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 ) ) ) )
153147, 149, 151, 152syl3anc 1182 . . . . . . . . . . . . 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 ) ) ) )
154144, 153eqtrd 2328 . . . . . . . . . . . 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 ) ) ) )
155154oveq1d 5889 . . . . . . . . . . 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 ) ) ) )
15615ad2antrr 706 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  S  e.  Ring )
15771ad2antrr 706 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  F : K --> C )
158 ffvelrn 5679 . . . . . . . . . . . . 13  |-  ( ( F : K --> C  /\  ( x `  b
)  e.  K )  ->  ( F `  ( x `  b
) )  e.  C
)
159157, 149, 158syl2anc 642 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  ( F `  ( x `  b ) )  e.  C )
160 ffvelrn 5679 . . . . . . . . . . . . 13  |-  ( ( F : K --> C  /\  ( y `  b
)  e.  K )  ->  ( F `  ( y `  b
) )  e.  C
)
161157, 151, 160syl2anc 642 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  ( F `  ( y `  b ) )  e.  C )
16261ad2antrr 706 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  T  e. CMnd )
16337ad2antrr 706 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  G : I --> C )
1646ad2antrr 706 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  I  e.  _V )
16520, 53, 30, 54, 162, 140, 163, 164psrbagev2 16264 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  ( T  gsumg  ( b  o F 
.^  G ) )  e.  C )
16628, 100, 5rngdir 15376 . . . . . . . . . . . 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 ) ) ) ) )
167156, 159, 161, 165, 166syl13anc 1184 . . . . . . . . . . 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 ) ) ) ) )
168155, 167eqtrd 2328 . . . . . . . . . 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 ) ) ) ) )
169168mpteq2dva 4122 . . . . . . . . 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 ) ) ) ) ) )
170111a1i 10 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  ->  D  e.  _V )
171 ovex 5899 . . . . . . . . . . 11  |-  ( ( F `  ( x `
 b ) ) 
.x.  ( T  gsumg  ( b  o F  .^  G
) ) )  e. 
_V
172171a1i 10 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  (
( F `  (
x `  b )
)  .x.  ( T  gsumg  ( b  o F  .^  G ) ) )  e.  _V )
173 ovex 5899 . . . . . . . . . . 11  |-  ( ( F `  ( y `
 b ) ) 
.x.  ( T  gsumg  ( b  o F  .^  G
) ) )  e. 
_V
174173a1i 10 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  (
( F `  (
y `  b )
)  .x.  ( T  gsumg  ( b  o F  .^  G ) ) )  e.  _V )
175 eqidd 2297 . . . . . . . . . 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 ) ) ) ) )
176 eqidd 2297 . . . . . . . . . 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 ) ) ) ) )
177170, 172, 174, 175, 176offval2 6111 . . . . . . . . 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 ) ) ) ) ) )
178169, 177eqtr4d 2331 . . . . . . . 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 ) ) ) ) ) )
179178oveq2d 5890 . . . . . . 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 ) ) ) ) ) ) )
180107adantr 451 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  ->  S  e. CMnd )
1816adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  ->  I  e.  _V )
1827adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  ->  R  e.  CRing )
18313adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  ->  S  e.  CRing )
18435adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  ->  F  e.  ( R RingHom  S ) )
18537adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  ->  G : I --> C )
18610, 1, 28, 16, 20, 29, 30, 5, 31, 32, 181, 182, 183, 184, 185, 129evlslem6 19413 . . . . . . . . 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 ) )
187186simpld 445 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( b  e.  D  |->  ( ( F `  ( x `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) : D --> C )
18810, 1, 28, 16, 20, 29, 30, 5, 31, 32, 181, 182, 183, 184, 185, 134evlslem6 19413 . . . . . . . . 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 ) )
189188simpld 445 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( b  e.  D  |->  ( ( F `  ( y `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) : D --> C )
190186simprd 449 . . . . . . . 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 )
191188simprd 449 . . . . . . . 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 )
19228, 105, 100, 180, 170, 187, 189, 190, 191gsumadd 15221 . . . . . . 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 ) ) ) ) ) ) )
193179, 192eqtrd 2328 . . . . . 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
) ) ) ) ) ) )
194102adantr 451 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  ->  P  e.  Grp )
1951, 99grpcl 14511 . . . . . . . 8  |-  ( ( P  e.  Grp  /\  x  e.  B  /\  y  e.  B )  ->  ( x ( +g  `  P ) y )  e.  B )
196194, 129, 134, 195syl3anc 1182 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( x ( +g  `  P ) y )  e.  B )
197 fveq1 5540 . . . . . . . . . . . 12  |-  ( p  =  ( x ( +g  `  P ) y )  ->  (
p `  b )  =  ( ( x ( +g  `  P
) y ) `  b ) )
198197fveq2d 5545 . . . . . . . . . . 11  |-  ( p  =  ( x ( +g  `  P ) y )  ->  ( F `  ( p `  b ) )  =  ( F `  (
( x ( +g  `  P ) y ) `
 b ) ) )
199198oveq1d 5889 . . . . . . . . . 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 ) ) ) )
200199mpteq2dv 4123 . . . . . . . . 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 ) ) ) ) )
201200oveq2d 5890 . . . . . . . 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 ) ) ) ) ) )
202 ovex 5899 . . . . . . . 8  |-  ( S 
gsumg  ( b  e.  D  |->  ( ( F `  ( ( x ( +g  `  P ) y ) `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) )  e. 
_V
203201, 32, 202fvmpt 5618 . . . . . . 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 ) ) ) ) ) )
204196, 203syl 15 . . . . . 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 ) ) ) ) ) )
205 fveq1 5540 . . . . . . . . . . . . 13  |-  ( p  =  x  ->  (
p `  b )  =  ( x `  b ) )
206205fveq2d 5545 . . . . . . . . . . . 12  |-  ( p  =  x  ->  ( F `  ( p `  b ) )  =  ( F `  (
x `  b )
) )
207206oveq1d 5889 . . . . . . . . . . 11  |-  ( p  =  x  ->  (
( F `  (
p `  b )
)  .x.  ( T  gsumg  ( b  o F  .^  G ) ) )  =  ( ( F `
 ( x `  b ) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) )
208207mpteq2dv 4123 . . . . . . . . . 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
) ) ) ) )
209208oveq2d 5890 . . . . . . . . 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 ) ) ) ) ) )
210 ovex 5899 . . . . . . . . 9  |-  ( S 
gsumg  ( b  e.  D  |->  ( ( F `  ( x `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) )  e. 
_V
211209, 32, 210fvmpt 5618 . . . . . . . 8  |-  ( x  e.  B  ->  ( E `  x )  =  ( S  gsumg  ( b  e.  D  |->  ( ( F `  ( x `
 b ) ) 
.x.  ( T  gsumg  ( b  o F  .^  G
) ) ) ) ) )
212129, 211syl 15 . . . . . . 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 ) ) ) ) ) )
213 fveq1 5540 . . . . . . . . . . . . 13  |-  ( p  =  y  ->  (
p `  b )  =  ( y `  b ) )
214213fveq2d 5545 . . . . . . . . . . . 12  |-  ( p  =  y  ->  ( F `  ( p `  b ) )  =  ( F `  (
y `  b )
) )
215214oveq1d 5889 . . . . . . . . . . 11  |-  ( p  =  y  ->  (
( F `  (
p `  b )
)  .x.  ( T  gsumg  ( b  o F  .^  G ) ) )  =  ( ( F `
 ( y `  b ) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) )
216215mpteq2dv 4123 . . . . . . . . . 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
) ) ) ) )
217216oveq2d 5890 . . . . . . . . 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 ) ) ) ) ) )
218 ovex 5899 . . . . . . . . 9  |-  ( S 
gsumg  ( b  e.  D  |->  ( ( F `  ( y `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) )  e. 
_V
219217, 32, 218fvmpt 5618 . . . . . . . 8  |-  ( y  e.  B  ->  ( E `  y )  =  ( S  gsumg  ( b  e.  D  |->  ( ( F `  ( y `
 b ) ) 
.x.  ( T  gsumg  ( b  o F  .^  G
) ) ) ) ) )
220219ad2antll 709 . . . . . . 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 ) ) ) ) ) )
221212, 220oveq12d 5892 . . . . . 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 ) ) ) ) ) ) )
222193, 204, 2213eqtr4d 2338 . . . . 5  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( E `  (
x ( +g  `  P
) y ) )  =  ( ( E `
 x ) ( +g  `  S ) ( E `  y
) ) )
2231, 28, 99, 100, 102, 104, 123, 222isghmd 14708 . . . 4  |-  ( ph  ->  E  e.  ( P 
GrpHom  S ) )
224 eqid 2296 . . . . . . . . . . 11  |-  (mulGrp `  R )  =  (mulGrp `  R )
225224, 29rhmmhm 15518 . . . . . . . . . 10  |-  ( F  e.  ( R RingHom  S
)  ->  F  e.  ( (mulGrp `  R ) MndHom  T ) )
22635, 225syl 15 . . . . . . . . 9  |-  ( ph  ->  F  e.  ( (mulGrp `  R ) MndHom  T ) )
227226adantr 451 . . . . . . . 8  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  ->  F  e.  ( (mulGrp `  R ) MndHom  T ) )
228 simprll 738 . . . . . . . . . 10  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  ->  x  e.  B )
22910, 16, 1, 20, 228mplelf 16194 . . . . . . . . 9  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  ->  x : D --> K )
230 simprrl 740 . . . . . . . . 9  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  -> 
z  e.  D )
231 ffvelrn 5679 . . . . . . . . 9  |-  ( ( x : D --> K  /\  z  e.  D )  ->  ( x `  z
)  e.  K )
232229, 230, 231syl2anc 642 . . . . . . . 8  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  -> 
( x `  z
)  e.  K )
233 simprlr 739 . . . . . . . . . 10  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  -> 
y  e.  B )
23410, 16, 1, 20, 233mplelf 16194 . . . . . . . . 9  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  -> 
y : D --> K )
235 simprrr 741 . . . . . . . . 9  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  ->  w  e.  D )
236 ffvelrn 5679 . . . . . . . . 9  |-  ( ( y : D --> K  /\  w  e.  D )  ->  ( y `  w
)  e.  K )
237234, 235, 236syl2anc 642 . . . . . . . 8  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  -> 
( y `  w
)  e.  K )
238224, 16mgpbas 15347 . . . . . . . . 9  |-  K  =  ( Base `  (mulGrp `  R ) )
239 eqid 2296 . . . . . . . . . 10  |-  ( .r
`  R )  =  ( .r `  R
)
240224, 239mgpplusg 15345 . . . . . . . . 9  |-  ( .r
`  R )  =  ( +g  `  (mulGrp `  R ) )
24129, 5mgpplusg 15345 . . . . . . . . 9  |-  .x.  =  ( +g  `  T )
242238, 240, 241mhmlin 14438 . . . . . . . 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
) ) ) )
243227, 232, 237, 242syl3anc 1182 . . . . . . 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
) ) ) )
24463ad2antrr 706 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  e.  D  /\  w  e.  D )
)  /\  v  e.  I )  ->  T  e.  Mnd )
2456adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  ->  I  e.  _V )
246 simprl 732 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  -> 
z  e.  D )
24720psrbagf 16129 . . . . . . . . . . . . . . 15  |-  ( ( I  e.  _V  /\  z  e.  D )  ->  z : I --> NN0 )
248245, 246, 247syl2anc 642 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  -> 
z : I --> NN0 )
249 ffvelrn 5679 . . . . . . . . . . . . . 14  |-  ( ( z : I --> NN0  /\  v  e.  I )  ->  ( z `  v
)  e.  NN0 )
250248, 249sylan 457 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  e.  D  /\  w  e.  D )
)  /\  v  e.  I )  ->  (
z `  v )  e.  NN0 )
251 simprr 733 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  ->  w  e.  D )
25220psrbagf 16129 . . . . . . . . . . . . . . 15  |-  ( ( I  e.  _V  /\  w  e.  D )  ->  w : I --> NN0 )
253245, 251, 252syl2anc 642 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  ->  w : I --> NN0 )
254 ffvelrn 5679 . . . . . . . . . . . . . 14  |-  ( ( w : I --> NN0  /\  v  e.  I )  ->  ( w `  v
)  e.  NN0 )
255253, 254sylan 457 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  e.  D  /\  w  e.  D )
)  /\  v  e.  I )  ->  (
w `  v )  e.  NN0 )
25637adantr 451 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  ->  G : I --> C )
257 ffvelrn 5679 . . . . . . . . . . . . . 14  |-  ( ( G : I --> C  /\  v  e.  I )  ->  ( G `  v
)  e.  C )
258256, 257sylan 457 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  e.  D  /\  w  e.  D )
)  /\  v  e.  I )  ->  ( G `  v )  e.  C )
25953, 30, 241mulgnn0dir 14606 . . . . . . . . . . . . 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 )
) ) )
260244, 250, 255, 258, 259syl13anc 1184 . . . . . . . . . . . 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 ) ) ) )
261260mpteq2dva 4122 . . . . . . . . . . 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
) ) ) ) )
262 ovex 5899 . . . . . . . . . . . . 13  |-  ( ( z `  v )  +  ( w `  v ) )  e. 
_V
263262a1i 10 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
z  e.  D  /\  w  e.  D )
)  /\  v  e.  I )  ->  (
( z `  v
)  +  ( w `
 v ) )  e.  _V )
264 fvex 5555 . . . . . . . . . . . . 13  |-  ( G `
 v )  e. 
_V
265264a1i 10 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
z  e.  D  /\  w  e.  D )
)  /\  v  e.  I )  ->  ( G `  v )  e.  _V )
266 ffn 5405 . . . . . . . . . . . . . 14  |-  ( z : I --> NN0  ->  z  Fn  I )
267248, 266syl 15 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  -> 
z  Fn  I )
268 ffn 5405 . . . . . . . . . . . . . 14  |-  ( w : I --> NN0  ->  w  Fn  I )
269253, 268syl 15 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  ->  w  Fn  I )
270 inidm 3391 . . . . . . . . . . . . 13  |-  ( I  i^i  I )  =  I
271 eqidd 2297 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  e.  D  /\  w  e.  D )
)  /\  v  e.  I )  ->  (
z `  v )  =  ( z `  v ) )
272 eqidd 2297 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  e.  D  /\  w  e.  D )
)  /\  v  e.  I )  ->  (
w `  v )  =  ( w `  v ) )
273267, 269, 245, 245, 270, 271, 272offval 6101 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  -> 
( z  o F  +  w )  =  ( v  e.  I  |->  ( ( z `  v )  +  ( w `  v ) ) ) )
27437feqmptd 5591 . . . . . . . . . . . . 13  |-  ( ph  ->  G  =  ( v  e.  I  |->  ( G `
 v ) ) )
275274adantr 451 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  ->  G  =  ( v  e.  I  |->  ( G `
 v ) ) )
276245, 263, 265, 273, 275offval2 6111 . . . . . . . . . . 11  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  -> 
( ( z  o F  +  w )  o F  .^  G
)  =  ( v  e.  I  |->  ( ( ( z `  v
)  +  ( w `
 v ) ) 
.^  ( G `  v ) ) ) )
277 ovex 5899 . . . . . . . . . . . . 13  |-  ( ( z `  v ) 
.^  ( G `  v ) )  e. 
_V
278277a1i 10 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
z  e.  D  /\  w  e.  D )
)  /\  v  e.  I )  ->  (
( z `  v
)  .^  ( G `  v ) )  e. 
_V )
279 ovex 5899 . . . . . . . . . . . . 13  |-  ( ( w `  v ) 
.^  ( G `  v ) )  e. 
_V
280279a1i 10 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
z  e.  D  /\  w  e.  D )
)  /\  v  e.  I )  ->  (
( w `  v
)  .^  ( G `  v ) )  e. 
_V )
281 ffn 5405 . . . . . . . . . . . . . . 15  |-  ( G : I --> C  ->  G  Fn  I )
28237, 281syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  G  Fn  I )
283282adantr 451 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  ->  G  Fn  I )
284 eqidd 2297 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  e.  D  /\  w  e.  D )
)  /\  v  e.  I )  ->  ( G `  v )  =  ( G `  v ) )
285267, 283, 245, 245, 270, 271, 284offval 6101 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  -> 
( z  o F 
.^  G )  =  ( v  e.  I  |->  ( ( z `  v )  .^  ( G `  v )
) ) )
286269, 283, 245, 245, 270, 272, 284offval 6101 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  -> 
( w  o F 
.^  G )  =  ( v  e.  I  |->  ( ( w `  v )  .^  ( G `  v )
) ) )
287245, 278, 280, 285, 286offval2 6111 . . . . . . . . . . 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
) ) ) ) )
288261, 276, 2873eqtr4d 2338 . . . . . . . . . 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 )
) )
289288oveq2d 5890 . . . . . . . . 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
) ) ) )
29061adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  ->  T  e. CMnd )
29120, 53, 30, 54, 290, 246, 256, 245psrbagev1 16263 . . . . . . . . . . 11  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  -> 
( ( z  o F  .^  G ) : I --> C  /\  ( `' ( z  o F  .^  G ) " ( _V  \  { ( 1r `  S ) } ) )  e.  Fin )
)
292291simpld 445 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  -> 
( z  o F 
.^  G ) : I --> C )
29320, 53, 30, 54, 290, 251, 256, 245psrbagev1 16263 . . . . . . . . . . 11  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  -> 
( ( w  o F  .^  G ) : I --> C  /\  ( `' ( w  o F  .^  G ) " ( _V  \  { ( 1r `  S ) } ) )  e.  Fin )
)
294293simpld 445 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  -> 
( w  o F 
.^  G ) : I --> C )
295291simprd 449 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  -> 
( `' ( z  o F  .^  G
) " ( _V 
\  { ( 1r
`  S ) } ) )  e.  Fin )
296293simprd 449 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  -> 
( `' ( w  o F  .^  G
) " ( _V 
\  { ( 1r
`  S ) } ) )  e.  Fin )
29753, 54, 241, 290, 245, 292, 294, 295, 296gsumadd 15221 . . . . . . . . 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 ) ) ) )
298289, 297eqtrd 2328 . . . . . . . 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
) ) ) )
299298adantrl 696 . . . . . . 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
) ) ) )
300243, 299oveq12d 5892 . . . . . 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
) ) ) ) )
30161adantr 451 . . . . . . 7  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  ->  T  e. CMnd )
30271adantr 451 . . . . . . . 8  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  ->  F : K --> C )
303 ffvelrn 5679 . . . . . . . 8  |-  ( ( F : K --> C  /\  ( x `  z
)  e.  K )  ->  ( F `  ( x `  z
) )  e.  C
)
304302, 232, 303syl2anc 642 . . . . . . 7  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  -> 
( F `  (
x `  z )
)  e.  C )
305 ffvelrn 5679 . . . . . . . 8  |-  ( ( F : K --> C  /\  ( y `  w
)  e.  K )  ->  ( F `  ( y `  w
) )  e.  C
)
306302, 237, 305syl2anc 642 . . . . . . 7  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  -> 
( F `  (
y `  w )
)  e.  C )
30720, 53, 30, 54, 290, 246, 256, 245psrbagev2 16264 . . . . . . . 8  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  -> 
( T  gsumg  ( z  o F 
.^  G ) )  e.  C )
308307adantrl 696 . . . . . . 7  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  -> 
( T  gsumg  ( z  o F 
.^  G ) )  e.  C )
30920, 53, 30, 54, 290, 251, 256, 245psrbagev2 16264 . . . . . . . 8  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  -> 
( T  gsumg  ( w  o F 
.^  G ) )  e.  C )
310309adantrl 696 . . . . . . 7  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  -> 
( T  gsumg  ( w  o F 
.^  G ) )  e.  C )
31153, 241cmn4 15124 . . . . . . 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
) ) ) ) )
312301, 304, 306, 308, 310, 311syl122anc 1191 . . . . . 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 ) ) ) ) )
313300, 312eqtrd 2328 . . . . 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
) ) ) ) )
3146adantr 451 . . . . . 6  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  ->  I  e.  _V )
3157adantr 451 . . . . . 6  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  ->  R  e.  CRing )
31613adantr 451 . . . . . 6  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  ->  S  e.  CRing )
31735adantr 451 . . . . . 6  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  ->  F  e.  ( R RingHom  S ) )
31837adantr 451 . . . . . 6  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  ->  G : I --> C )
31920psrbagaddcl 16132 . . . . . . 7  |-  ( ( I  e.  _V  /\  z  e.  D  /\  w  e.  D )  ->  ( z  o F  +  w )  e.  D )
320314, 230, 235, 319syl3anc 1182 . . . . . 6  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  -> 
( z  o F  +  w )  e.  D )
3219adantr 451 . . . . . . 7  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  ->  R  e.  Ring )
32216, 239rngcl 15370 . . . . . . 7  |-  ( ( R  e.  Ring  /\  (
x `  z )  e.  K  /\  (
y `  w )  e.  K )  ->  (
( x `  z
) ( .r `  R ) ( y `
 w ) )  e.  K )
323321, 232, 237, 322syl3anc 1182 . . . . . 6  |-  ( (
ph  /\  ( (
x  e.  B  /\  y  e.  B )  /\  ( z  e.  D  /\  w  e.  D
) ) )  -> 
( ( x `  z ) ( .r
`  R ) ( y `  w ) )  e.  K )
32410, 1, 28, 16, 20, 29, 30, 5, 31, 32, 314, 315, 316, 317, 318, 21, 320, 323evlslem3 19414 . . . . 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 ) ) ) )
32510, 1, 28, 16, 20, 29, 30, 5, 31, 32, 314, 315, 316, 317, 318, 21, 230, 232evlslem3 19414 . . . . . 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 ) ) ) )
32610, 1, 28, 16, 20, 29, 30, 5, 31, 32, 314, 315, 316, 317, 318, 21, 235, 237evlslem3 19414 . . . . . 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 ) ) ) )
327325, 326oveq12d 5892 . . . . 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 ) ) ) ) )
328313, 324, 3273eqtr4d 2338 . . . 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 ) ) ) ) ) )
32910, 1, 5, 21, 20, 6, 7, 13, 223, 328evlslem2 16265 . . 3  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( E `  (
x ( .r `  P ) y ) )  =  ( ( E `  x ) 
.x.  ( E `  y ) ) )
3301, 2, 3, 4, 5, 12, 15, 98, 329, 28, 99, 100, 123, 222isrhmd 15523 . 2  |-  ( ph  ->  E  e.  ( P RingHom  S ) )
331 ovex 5899 . . . . . 6  |-  ( S 
gsumg  ( b  e.  D  |->  ( ( F `  ( p `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) )  e. 
_V
332331, 32fnmpti 5388 . . . . 5  |-  E  Fn  B
333332a1i 10 . . . 4  |-  ( ph  ->  E  Fn  B )
33416, 1rhmf 15520 . . . . . 6  |-  ( A  e.  ( R RingHom  P
)  ->  A : K
--> B )
33592, 334syl 15 . . . . 5  |-  ( ph  ->  A : K --> B )
336 ffn 5405 . . . . 5  |-  ( A : K --> B  ->  A  Fn  K )
337335, 336syl 15 . . . 4  |-  ( ph  ->  A  Fn  K )
338 frn 5411 . . . . 5  |-  ( A : K --> B  ->  ran  A  C_  B )
339335, 338syl 15 . . . 4  |-  ( ph  ->  ran  A  C_  B
)
340 fnco 5368 . . . 4  |-  ( ( E  Fn  B  /\  A  Fn  K  /\  ran  A  C_  B )  ->  ( E  o.  A
)  Fn  K )
341333, 337, 339, 340syl3anc 1182 . . 3  |-  ( ph  ->  ( E  o.  A
)  Fn  K )
342 ffn 5405 . . . 4  |-  ( F : K --> C  ->  F  Fn  K )
34371, 342syl 15 . . 3  |-  ( ph  ->  F  Fn  K )
344 fvco2 5610 . . . . 5  |-  ( ( A  Fn  K  /\  x  e.  K )  ->  ( ( E  o.  A ) `  x
)  =  ( E `
 ( A `  x ) ) )
345337, 344sylan 457 . . . 4  |-  ( (
ph  /\  x  e.  K )  ->  (
( E  o.  A
) `  x )  =  ( E `  ( A `  x ) ) )
346345, 77eqtrd 2328 . . 3  |-  ( (
ph  /\  x  e.  K )  ->  (
( E  o.  A
) `  x )  =  ( F `  x ) )
347341, 343, 346eqfnfvd 5641 . 2  |-  ( ph  ->  ( E  o.  A
)  =  F )
34810, 31, 1, 6, 9mvrf2 16249 . . . . 5  |-  ( ph  ->  V : I --> B )
349 ffn 5405 . . . . 5  |-  ( V : I --> B  ->  V  Fn  I )
350348, 349syl 15 . . . 4  |-  ( ph  ->  V  Fn  I )
351 frn 5411 . . . . 5  |-  ( V : I --> B  ->  ran  V  C_  B )
352348, 351syl 15 . . . 4  |-  ( ph  ->  ran  V  C_  B
)
353 fnco 5368 . . . 4  |-  ( ( E  Fn  B  /\  V  Fn  I  /\  ran  V  C_  B )  ->  ( E  o.  V
)  Fn  I )
354333, 350, 352, 353syl3anc 1182 . . 3  |-  ( ph  ->  ( E  o.  V
)  Fn  I )
355 fvco2 5610 . . . . 5  |-  ( ( V  Fn  I  /\  x  e.  I )  ->  ( ( E  o.  V ) `  x
)  =  ( E `
 ( V `  x ) ) )
356350, 355sylan 457 . . . 4  |-  ( (
ph  /\  x  e.  I )  ->  (
( E  o.  V
) `  x )  =  ( E `  ( V `  x ) ) )
3576adantr 451 . . . . . . 7  |-  ( (
ph  /\  x  e.  I )  ->  I  e.  _V )
3587adantr 451 . . . . . . 7  |-  ( (
ph  /\  x  e.  I )  ->  R  e.  CRing )
359 simpr 447 . . . . . . 7  |-  ( (
ph  /\  x  e.  I )  ->  x  e.  I )
36031, 20, 21, 17, 357, 358, 359mvrval 16182 . . . . . 6  |-  ( (
ph  /\  x  e.  I )  ->  ( V `  x )  =  ( y  e.  D  |->  if ( y  =  ( z  e.  I  |->  if ( z  =  x ,  1 ,  0 ) ) ,  ( 1r `  R ) ,  ( 0g `  R ) ) ) )
361360fveq2d 5545 . . . . 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 ) ) ) ) )
36213adantr 451 . . . . . 6  |-  ( (
ph  /\  x  e.  I )  ->  S  e.  CRing )
36335adantr 451 . . . . . 6  |-  ( (
ph  /\  x  e.  I )  ->  F  e.  ( R RingHom  S )
)
36437adantr 451 . . . . . 6  |-  ( (
ph  /\  x  e.  I )  ->  G : I --> C )
36520psrbagsn 16252 . . . . . . . 8  |-  ( I  e.  _V  ->  (
z  e.  I  |->  if ( z  =  x ,  1 ,  0 ) )  e.  D
)
3666, 365syl 15 . . . . . . 7  |-  ( ph  ->  ( z  e.  I  |->  if ( z  =  x ,  1 ,  0 ) )  e.  D )
367366adantr 451 . . . . . 6  |-  ( (
ph  /\  x  e.  I )  ->  (
z  e.  I  |->  if ( z  =  x ,  1 ,  0 ) )  e.  D
)
36819adantr 451 . . . . . 6  |-  ( (
ph  /\  x  e.  I )  ->  ( 1r `  R )  e.  K )
36910, 1, 28, 16, 20, 29, 30, 5, 31, 32, 357, 358, 362, 363, 364, 21, 367, 368evlslem3 19414 . . . . 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
) ) ) )
37097adantr 451 . . . . . . 7  |-  ( (
ph  /\  x  e.  I )  ->  ( F `  ( 1r `  R ) )  =  ( 1r `  S
) )
371 1nn0 9997 . . . . . . . . . . . . . 14  |-  1  e.  NN0
372 0nn0 9996 . . . . . . . . . . . . . 14  |-  0  e.  NN0
373371, 372keepel 3635 . . . . . . . . . . . . 13  |-  if ( z  =  x ,  1 ,  0 )  e.  NN0
374373a1i 10 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  I )  ->  if ( z  =  x ,  1 ,  0 )  e.  NN0 )
375 ffvelrn 5679 . . . . . . . . . . . . 13  |-  ( ( G : I --> C  /\  z  e.  I )  ->  ( G `  z
)  e.  C )
37637, 375sylan 457 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  I )  ->  ( G `  z )  e.  C )
377 eqidd 2297 . . . . . . . . . . . 12  |-  ( ph  ->  ( z  e.  I  |->  if ( z  =  x ,  1 ,  0 ) )  =  ( z  e.  I  |->  if ( z  =  x ,  1 ,  0 ) ) )
37837feqmptd 5591 . . . . . . . . . . . 12  |-  ( ph  ->  G  =  ( z  e.  I  |->  ( G `
 z ) ) )
3796, 374, 376, 377, 378offval2 6111 . . . . . . . . . . 11  |-  ( ph  ->  ( ( z  e.  I  |->  if ( z  =  x ,  1 ,  0 ) )  o F  .^  G
)  =  ( z  e.  I  |->  ( if ( z  =  x ,  1 ,  0 )  .^  ( G `  z ) ) ) )
380 oveq1 5881 . . . . . . . . . . . . . 14  |-  ( 1  =  if ( z  =  x ,  1 ,  0 )  -> 
( 1  .^  ( G `  z )
)  =  ( if ( z  =  x ,  1 ,  0 )  .^  ( G `  z ) ) )
381380eqeq1d 2304 . . . . . . . . . . . . 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 ) ) ) )
382 oveq1 5881 . . . . . . . . . . . . . 14  |-  ( 0  =  if ( z  =  x ,  1 ,  0 )  -> 
( 0  .^  ( G `  z )
)  =  ( if ( z  =  x ,  1 ,  0 )  .^  ( G `  z ) ) )
383382eqeq1d 2304 . . . . . . . . . . . . 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 ) ) ) )
384376adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  z  e.  I )  /\  z  =  x )  ->  ( G `  z )  e.  C )
38553, 30mulg1 14590 . . . . . . . . . . . . . . 15  |-  ( ( G `  z )  e.  C  ->  (
1  .^  ( G `  z ) )  =  ( G `  z
) )
386384, 385syl 15 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  z  e.  I )  /\  z  =  x )  ->  (
1  .^  ( G `  z ) )  =  ( G `  z
) )
387 iftrue 3584 . . . . . . . . . . . . . . 15  |-  ( z  =  x  ->  if ( z  =  x ,  ( G `  z ) ,  ( 1r `  S ) )  =  ( G `
 z ) )
388387adantl 452 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  z  e.  I )  /\  z  =  x )  ->  if ( z  =  x ,  ( G `  z ) ,  ( 1r `  S ) )  =  ( G `
 z ) )
389386, 388eqtr4d 2331 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  z  e.  I )  /\  z  =  x )  ->  (
1  .^  ( G `  z ) )  =  if ( z  =  x ,  ( G `
 z ) ,  ( 1r `  S
) ) )
39053, 54, 30mulg0 14588 . . . . . . . . . . . . . . . 16  |-  ( ( G `  z )  e.  C  ->  (
0  .^  ( G `  z ) )  =  ( 1r `  S
) )
391376, 390syl 15 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  z  e.  I )  ->  (
0  .^  ( G `  z ) )  =  ( 1r `  S
) )
392391adantr 451 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  z  e.  I )  /\  -.  z  =  x )  ->  ( 0  .^  ( G `  z )
)  =  ( 1r
`  S ) )
393 iffalse 3585 . . . . . . . . . . . . . . 15  |-  ( -.  z  =  x  ->  if ( z  =  x ,  ( G `  z ) ,  ( 1r `  S ) )  =  ( 1r
`  S ) )
394393adantl 452 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  z  e.  I )  /\  -.  z  =  x )  ->  if ( z  =  x ,  ( G `
 z ) ,  ( 1r `  S
) )  =  ( 1r `  S ) )
395392, 394eqtr4d 2331 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  z  e.  I )  /\  -.  z  =  x )  ->  ( 0  .^  ( G `  z )
)  =  if ( z  =  x ,  ( G `  z
) ,  ( 1r
`  S ) ) )
396381, 383, 389, 395ifbothda 3608 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  I )  ->  ( if ( z  =  x ,  1 ,  0 )  .^  ( G `  z ) )  =  if ( z  =  x ,  ( G `
 z ) ,  ( 1r `  S
) ) )
397396mpteq2dva 4122 . . . . . . . . . . 11  |-  ( ph  ->  ( z  e.  I  |->  ( if ( z  =  x ,  1 ,  0 )  .^  ( G `  z ) ) )  =  ( z  e.  I  |->  if ( z  =  x ,  ( G `  z ) ,  ( 1r `  S ) ) ) )
398379, 397eqtrd 2328 . . . . . . . . . 10  |-  ( ph  ->  ( ( z  e.  I  |->  if ( z  =  x ,  1 ,  0 ) )  o F  .^  G
)  =  ( z  e.  I  |->  if ( z  =  x ,  ( G `  z
) ,  ( 1r
`  S ) ) ) )
399398adantr 451 . . . . . . . . 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 ) ) ) )
400399oveq2d 5890 . . . . . . . 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
) ) ) ) )
40163adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  I )  ->  T  e.  Mnd )
402376adantlr 695 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  I )  /\  z  e.  I )  ->  ( G `  z )  e.  C )
40328, 3rngidcl 15377 . . . . . . . . . . . . 13  |-  ( S  e.  Ring  ->  ( 1r
`  S )  e.  C )
40415, 403syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1r `  S
)  e.  C )
405404ad2antrr 706 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  I )  /\  z  e.  I )  ->  ( 1r `  S )  e.  C )
406 ifcl 3614 . . . . . . . . . . 11  |-  ( ( ( G `  z
)  e.  C  /\  ( 1r `  S )  e.  C )  ->  if ( z  =  x ,  ( G `  z ) ,  ( 1r `  S ) )  e.  C )
407402, 405, 406syl2anc 642 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  I )  /\  z  e.  I )  ->  if ( z  =  x ,  ( G `  z ) ,  ( 1r `  S ) )  e.  C )
408 eqid 2296 . . . . . . . . . 10  |-  ( z  e.  I  |->  if ( z  =  x ,  ( G `  z
) ,  ( 1r
`  S ) ) )  =  ( z  e.  I  |->  if ( z  =  x ,  ( G `  z
) ,  ( 1r
`  S ) ) )
409407, 408fmptd 5700 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  I )  ->  (
z  e.  I  |->  if ( z  =  x ,  ( G `  z ) ,  ( 1r `  S ) ) ) : I --> C )
410 eldifn 3312 . . . . . . . . . . . . 13  |-  ( z  e.  ( I  \  { x } )  ->  -.  z  e.  { x } )
411 elsn 3668 . . . . . . . . . . . . 13  |-  ( z  e.  { x }  <->  z  =  x )
412410, 411sylnib 295 . . . . . . . . . . . 12  |-  ( z  e.  ( I  \  { x } )  ->  -.  z  =  x )
413412, 393syl 15 . . . . . . . . . . 11  |-  ( z  e.  ( I  \  { x } )  ->  if ( z  =  x ,  ( G `  z ) ,  ( 1r `  S ) )  =  ( 1r `  S
) )
414413adantl 452 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  I )  /\  z  e.  ( I  \  {
x } ) )  ->  if ( z  =  x ,  ( G `  z ) ,  ( 1r `  S ) )  =  ( 1r `  S
) )
415414suppss2 6089 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  I )  ->  ( `' ( z  e.  I  |->  if ( z  =  x ,  ( G `  z ) ,  ( 1r `  S ) ) )
" ( _V  \  { ( 1r `  S ) } ) )  C_  { x } )
41653, 54, 401, 357, 359, 409, 415gsumpt 15238 . . . . . . . 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 ) )
417 fveq2 5541 . . . . . . . . . . 11  |-  ( z  =  x  ->  ( G `  z )  =  ( G `  x ) )
418387, 417eqtrd 2328 . . . . . . . . . 10  |-  ( z  =  x  ->  if ( z  =  x ,  ( G `  z ) ,  ( 1r `  S ) )  =  ( G `
 x ) )
419418, 408, 45fvmpt 5618 . . . . . . . . 9  |-  ( x  e.  I  ->  (
( z  e.  I  |->  if ( z  =  x ,  ( G `
 z ) ,  ( 1r `  S
) ) ) `  x )  =  ( G `  x ) )
420419adantl 452 . . . . . . . 8  |-  ( (
ph  /\  x  e.  I )  ->  (
( z  e.  I  |->  if ( z  =  x ,  ( G `
 z ) ,  ( 1r `  S
) ) ) `  x )  =  ( G `  x ) )
421400, 416, 4203eqtrd 2332 . . . . . . 7  |-  ( (
ph  /\  x  e.  I )  ->  ( T  gsumg  ( ( z  e.  I  |->  if ( z  =  x ,  1 ,  0 ) )  o F  .^  G
) )  =  ( G `  x ) )
422370, 421oveq12d 5892 . . . . . 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 ) ) )
42315adantr 451 . . . . . . 7  |-  ( (
ph  /\  x  e.  I )  ->  S  e.  Ring )
42428, 5, 3rnglidm 15380 . . . . . . 7  |-  ( ( S  e.  Ring  /\  ( G `  x )  e.  C )  ->  (
( 1r `  S
)  .x.  ( G `  x ) )  =  ( G `  x
) )
425423, 52, 424syl2anc 642 . . . . . 6  |-  ( (
ph  /\  x  e.  I )  ->  (
( 1r `  S
)  .x.  ( G `  x ) )  =  ( G `  x
) )
426422, 425eqtrd 2328 . . . . 5  |-  ( (
ph  /\  x  e.  I )  ->  (
( F `  ( 1r `  R ) ) 
.x.  ( T  gsumg  ( ( z  e.  I  |->  if ( z  =  x ,  1 ,  0 ) )  o F 
.^  G ) ) )  =  ( G `
 x ) )
427361, 369, 4263eqtrd 2332 . . . 4  |-  ( (
ph  /\  x  e.  I )  ->  ( E `  ( V `  x ) )  =  ( G `  x
) )
428356, 427eqtrd 2328 . . 3  |-  ( (
ph  /\  x  e.  I )  ->  (
( E  o.  V
) `  x )  =  ( G `  x ) )
429354, 282, 428eqfnfvd 5641 . 2  |-  ( ph  ->  ( E  o.  V
)  =  G )
430330, 347, 4293jca 1132 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 358    /\ w3a 934    = wceq 1632    e. wcel 1696   A.wral 2556   {crab 2560   _Vcvv 2801    \ cdif 3162    C_ wss 3165   ifcif 3578   {csn 3653    e. cmpt 4093    X. cxp 4703   `'ccnv 4704   ran crn 4706   "cima 4708    o. ccom 4709    Fn wfn 5266   -->wf 5267   ` cfv 5271  (class class class)co 5874    o Fcof 6092    ^m cmap 6788   Fincfn 6879   0cc0 8753   1c1 8754    + caddc 8756   NNcn 9762   NN0cn0 9981   ZZcz 10040   Basecbs 13164   +g cplusg 13224   .rcmulr 13225  Scalarcsca 13227   0gc0g 13416    gsumg cgsu 13417   Mndcmnd 14377   Grpcgrp 14378  .gcmg 14382   MndHom cmhm 14429    GrpHom cghm 14696  CMndccmn 15105  mulGrpcmgp 15341   Ringcrg 15353   CRingccrg 15354   1rcur 15355   RingHom crh 15510  AssAlgcasa 16066  algSccascl 16068   mVar cmvr 16104   mPoly cmpl 16105
This theorem is referenced by:  evlseu  19416
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-rep 4147  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528  ax-inf2 7358  ax-cnex 8809  ax-resscn 8810  ax-1cn 8811  ax-icn 8812  ax-addcl 8813  ax-addrcl 8814  ax-mulcl 8815  ax-mulrcl 8816  ax-mulcom 8817  ax-addass 8818  ax-mulass 8819  ax-distr 8820  ax-i2m1 8821  ax-1ne0 8822  ax-1rid 8823  ax-rnegex 8824  ax-rrecex 8825  ax-cnre 8826  ax-pre-lttri 8827  ax-pre-lttrn 8828  ax-pre-ltadd 8829  ax-pre-mulgt0 8830
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-nel 2462  df-ral 2561  df-rex 2562  df-reu 2563  df-rmo 2564  df-rab 2565  df-v 2803  df-sbc 3005  df-csb 3095  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-pss 3181  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-tp 3661  df-op 3662  df-uni 3844  df-int 3879  df-iun 3923  df-iin 3924  df-br 4040  df-opab 4094  df-mpt 4095  df-tr 4130  df-eprel 4321  df-id 4325  df-po 4330  df-so 4331  df-fr 4368  df-se 4369  df-we 4370  df-ord 4411  df-on 4412  df-lim 4413  df-suc 4414  df-om 4673  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279  df-isom 5280  df-ov 5877  df-oprab 5878  df-mpt2 5879  df-of 6094  df-ofr 6095  df-1st 6138  df-2nd 6139  df-riota 6320  df-recs 6404  df-rdg 6439  df-1o 6495  df-2o 6496  df-oadd 6499  df-er 6676  df-map 6790  df-pm 6791  df-ixp 6834  df-en 6880  df-dom 6881  df-sdom 6882  df-fin 6883  df-oi 7241  df-card 7588  df-pnf 8885  df-mnf 8886  df-xr 8887  df-ltxr 8888  df-le 8889  df-sub 9055  df-neg 9056  df-nn 9763  df-2 9820  df-3 9821  df-4 9822  df-5 9823  df-6 9824  df-7 9825  df-8 9826  df-9 9827  df-n0 9982  df-z 10041  df-uz 10247  df-fz 10799  df-fzo 10887  df-seq 11063  df-hash 11354  df-struct 13166  df-ndx 13167  df-slot 13168  df-base 13169  df-sets 13170  df-ress 13171  df-plusg 13237  df-mulr 13238  df-sca 13240  df-vsca 13241  df-tset 13243  df-0g 13420  df-gsum 13421  df-mre 13504  df-mrc 13505  df-acs 13507  df-mnd 14383  df-mhm 14431  df-submnd 14432  df-grp 14505  df-minusg 14506  df-sbg 14507  df-mulg 14508  df-subg 14634  df-ghm 14697  df-cntz 14809  df-cmn 15107  df-abl 15108  df-mgp 15342  df-rng 15356  df-cring 15357  df-ur 15358  df-rnghom 15512  df-subrg 15559  df-lmod 15645  df-lss 15706  df-assa 16069  df-ascl 16071  df-psr 16114  df-mvr 16115  df-mpl 16116
  Copyright terms: Public domain W3C validator