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

Theorem evlslem1 19399
Description: Lemma for evlseu 19400, 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 2283 . . 3  |-  ( 1r
`  P )  =  ( 1r `  P
)
3 eqid 2283 . . 3  |-  ( 1r
`  S )  =  ( 1r `  S
)
4 eqid 2283 . . 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 15351 . . . . 5  |-  ( R  e.  CRing  ->  R  e.  Ring )
97, 8syl 15 . . . 4  |-  ( ph  ->  R  e.  Ring )
10 evlslem1.p . . . . 5  |-  P  =  ( I mPoly  R )
1110mplrng 16196 . . . 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 15351 . . . 4  |-  ( S  e.  CRing  ->  S  e.  Ring )
1513, 14syl 15 . . 3  |-  ( ph  ->  S  e.  Ring )
16 evlslem1.k . . . . . . 7  |-  K  =  ( Base `  R
)
17 eqid 2283 . . . . . . 7  |-  ( 1r
`  R )  =  ( 1r `  R
)
1816, 17rngidcl 15361 . . . . . 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 2283 . . . . . . . . 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 16237 . . . . . . . 8  |-  ( (
ph  /\  x  e.  K )  ->  ( A `  x )  =  ( y  e.  D  |->  if ( y  =  ( I  X.  { 0 } ) ,  x ,  ( 0g `  R ) ) ) )
2726fveq2d 5529 . . . . . . 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 16235 . . . . . . . . . 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 19398 . . . . . . 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 10035 . . . . . . . . . . . . . . 15  |-  0  e.  ZZ
4443a1i 10 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  I )  ->  0  e.  ZZ )
45 fvex 5539 . . . . . . . . . . . . . . 15  |-  ( G `
 x )  e. 
_V
4645a1i 10 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  I )  ->  ( G `  x )  e.  _V )
47 fconstmpt 4732 . . . . . . . . . . . . . . 15  |-  ( I  X.  { 0 } )  =  ( x  e.  I  |->  0 )
4847a1i 10 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( I  X.  {
0 } )  =  ( x  e.  I  |->  0 ) )
4937feqmptd 5575 . . . . . . . . . . . . . 14  |-  ( ph  ->  G  =  ( x  e.  I  |->  ( G `
 x ) ) )
506, 44, 46, 48, 49offval2 6095 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( I  X.  { 0 } )  o F  .^  G
)  =  ( x  e.  I  |->  ( 0 
.^  ( G `  x ) ) ) )
51 ffvelrn 5663 . . . . . . . . . . . . . . . 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 15331 . . . . . . . . . . . . . . . 16  |-  C  =  ( Base `  T
)
5429, 3rngidval 15343 . . . . . . . . . . . . . . . 16  |-  ( 1r
`  S )  =  ( 0g `  T
)
5553, 54, 30mulg0 14572 . . . . . . . . . . . . . . 15  |-  ( ( G `  x )  e.  C  ->  (
0  .^  ( G `  x ) )  =  ( 1r `  S
) )
5652, 55syl 15 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  I )  ->  (
0  .^  ( G `  x ) )  =  ( 1r `  S
) )
5756mpteq2dva 4106 . . . . . . . . . . . . 13  |-  ( ph  ->  ( x  e.  I  |->  ( 0  .^  ( G `  x )
) )  =  ( x  e.  I  |->  ( 1r `  S ) ) )
5850, 57eqtrd 2315 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( I  X.  { 0 } )  o F  .^  G
)  =  ( x  e.  I  |->  ( 1r
`  S ) ) )
5958oveq2d 5874 . . . . . . . . . . 11  |-  ( ph  ->  ( T  gsumg  ( ( I  X.  { 0 } )  o F  .^  G
) )  =  ( T  gsumg  ( x  e.  I  |->  ( 1r `  S
) ) ) )
6029crngmgp 15349 . . . . . . . . . . . . . 14  |-  ( S  e.  CRing  ->  T  e. CMnd )
6113, 60syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  T  e. CMnd )
62 cmnmnd 15104 . . . . . . . . . . . . 13  |-  ( T  e. CMnd  ->  T  e.  Mnd )
6361, 62syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  T  e.  Mnd )
6454gsumz 14458 . . . . . . . . . . . 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 2315 . . . . . . . . . 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 5874 . . . . . . . 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 15504 . . . . . . . . . . 11  |-  ( F  e.  ( R RingHom  S
)  ->  F : K
--> C )
7135, 70syl 15 . . . . . . . . . 10  |-  ( ph  ->  F : K --> C )
72 ffvelrn 5663 . . . . . . . . . 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 15365 . . . . . . . . 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 2315 . . . . . . 7  |-  ( (
ph  /\  x  e.  K )  ->  (
( F `  x
)  .x.  ( T  gsumg  ( ( I  X.  {
0 } )  o F  .^  G )
) )  =  ( F `  x ) )
7727, 42, 763eqtrd 2319 . . . . . 6  |-  ( (
ph  /\  x  e.  K )  ->  ( E `  ( A `  x ) )  =  ( F `  x
) )
7877ralrimiva 2626 . . . . 5  |-  ( ph  ->  A. x  e.  K  ( E `  ( A `
 x ) )  =  ( F `  x ) )
79 fveq2 5525 . . . . . . . 8  |-  ( x  =  ( 1r `  R )  ->  ( A `  x )  =  ( A `  ( 1r `  R ) ) )
8079fveq2d 5529 . . . . . . 7  |-  ( x  =  ( 1r `  R )  ->  ( E `  ( A `  x ) )  =  ( E `  ( A `  ( 1r `  R ) ) ) )
81 fveq2 5525 . . . . . . 7  |-  ( x  =  ( 1r `  R )  ->  ( F `  x )  =  ( F `  ( 1r `  R ) ) )
8280, 81eqeq12d 2297 . . . . . 6  |-  ( x  =  ( 1r `  R )  ->  (
( E `  ( A `  x )
)  =  ( F `
 x )  <->  ( E `  ( A `  ( 1r `  R ) ) )  =  ( F `
 ( 1r `  R ) ) ) )
8382rspcva 2882 . . . . 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 16198 . . . . . . . . 9  |-  ( ( I  e.  _V  /\  R  e.  CRing )  ->  P  e. AssAlg )
866, 7, 85syl2anc 642 . . . . . . . 8  |-  ( ph  ->  P  e. AssAlg )
87 eqid 2283 . . . . . . . . 9  |-  (Scalar `  P )  =  (Scalar `  P )
8822, 87asclrhm 16081 . . . . . . . 8  |-  ( P  e. AssAlg  ->  A  e.  ( (Scalar `  P ) RingHom  P ) )
8986, 88syl 15 . . . . . . 7  |-  ( ph  ->  A  e.  ( (Scalar `  P ) RingHom  P ) )
9010, 6, 7mplsca 16189 . . . . . . . 8  |-  ( ph  ->  R  =  (Scalar `  P ) )
9190oveq1d 5873 . . . . . . 7  |-  ( ph  ->  ( R RingHom  P )  =  ( (Scalar `  P ) RingHom  P ) )
9289, 91eleqtrrd 2360 . . . . . 6  |-  ( ph  ->  A  e.  ( R RingHom  P ) )
9317, 2rhm1 15508 . . . . . 6  |-  ( A  e.  ( R RingHom  P
)  ->  ( A `  ( 1r `  R
) )  =  ( 1r `  P ) )
9492, 93syl 15 . . . . 5  |-  ( ph  ->  ( A `  ( 1r `  R ) )  =  ( 1r `  P ) )
9594fveq2d 5529 . . . 4  |-  ( ph  ->  ( E `  ( A `  ( 1r `  R ) ) )  =  ( E `  ( 1r `  P ) ) )
9617, 3rhm1 15508 . . . . 5  |-  ( F  e.  ( R RingHom  S
)  ->  ( F `  ( 1r `  R
) )  =  ( 1r `  S ) )
9735, 96syl 15 . . . 4  |-  ( ph  ->  ( F `  ( 1r `  R ) )  =  ( 1r `  S ) )
9884, 95, 973eqtr3d 2323 . . 3  |-  ( ph  ->  ( E `  ( 1r `  P ) )  =  ( 1r `  S ) )
99 eqid 2283 . . . . 5  |-  ( +g  `  P )  =  ( +g  `  P )
100 eqid 2283 . . . . 5  |-  ( +g  `  S )  =  ( +g  `  S )
101 rnggrp 15346 . . . . . 6  |-  ( P  e.  Ring  ->  P  e. 
Grp )
10212, 101syl 15 . . . . 5  |-  ( ph  ->  P  e.  Grp )
103 rnggrp 15346 . . . . . 6  |-  ( S  e.  Ring  ->  S  e. 
Grp )
10415, 103syl 15 . . . . 5  |-  ( ph  ->  S  e.  Grp )
105 eqid 2283 . . . . . . 7  |-  ( 0g
`  S )  =  ( 0g `  S
)
106 rngcmn 15371 . . . . . . . . 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 5883 . . . . . . . . . 10  |-  ( NN0 
^m  I )  e. 
_V
110109rabex 4165 . . . . . . . . 9  |-  { h  e.  ( NN0  ^m  I
)  |  ( `' h " NN )  e.  Fin }  e.  _V
11120, 110eqeltri 2353 . . . . . . . 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 19397 . . . . . . . 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 15198 . . . . . 6  |-  ( (
ph  /\  p  e.  B )  ->  ( S  gsumg  ( b  e.  D  |->  ( ( F `  ( p `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) )  e.  C )
123122, 32fmptd 5684 . . . . 5  |-  ( ph  ->  E : B --> C )
124 eqid 2283 . . . . . . . . . . . . . . . . 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 16186 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  (
x ( +g  `  P
) y )  =  ( x  o F ( +g  `  R
) y ) )
128127fveq1d 5527 . . . . . . . . . . . . . . 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 16178 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  ->  x : D --> K )
131 ffn 5389 . . . . . . . . . . . . . . . . . 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 16178 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
y : D --> K )
136 ffn 5389 . . . . . . . . . . . . . . . . . 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 6090 . . . . . . . . . . . . . . . 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 2315 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  (
( x ( +g  `  P ) y ) `
 b )  =  ( ( x `  b ) ( +g  `  R ) ( y `
 b ) ) )
144143fveq2d 5529 . . . . . . . . . . . . 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 15503 . . . . . . . . . . . . . . . 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 5663 . . . . . . . . . . . . . . 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 5663 . . . . . . . . . . . . . . 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 14688 . . . . . . . . . . . . . 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 2315 . . . . . . . . . . . 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 5873 . . . . . . . . . . 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 5663 . . . . . . . . . . . . 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 5663 . . . . . . . . . . . . 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 16248 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  b  e.  D )  ->  ( T  gsumg  ( b  o F 
.^  G ) )  e.  C )
16628, 100, 5rngdir 15360 . . . . . . . . . . . 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 2315 . . . . . . . . . 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 4106 . . . . . . . . 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 5883 . . . . . . . . . . 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 5883 . . . . . . . . . . 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 2284 . . . . . . . . . 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 2284 . . . . . . . . . 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 6095 . . . . . . . . 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 2318 . . . . . . . 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 5874 . . . . . . 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 19397 . . . . . . . . 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 19397 . . . . . . . . 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 15205 . . . . . . 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 2315 . . . . . 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 14495 . . . . . . . 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 5524 . . . . . . . . . . . 12  |-  ( p  =  ( x ( +g  `  P ) y )  ->  (
p `  b )  =  ( ( x ( +g  `  P
) y ) `  b ) )
198197fveq2d 5529 . . . . . . . . . . 11  |-  ( p  =  ( x ( +g  `  P ) y )  ->  ( F `  ( p `  b ) )  =  ( F `  (
( x ( +g  `  P ) y ) `
 b ) ) )
199198oveq1d 5873 . . . . . . . . . 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 4107 . . . . . . . . 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 5874 . . . . . . . 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 5883 . . . . . . . 8  |-  ( S 
gsumg  ( b  e.  D  |->  ( ( F `  ( ( x ( +g  `  P ) y ) `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) )  e. 
_V
203201, 32, 202fvmpt 5602 . . . . . . 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 5524 . . . . . . . . . . . . 13  |-  ( p  =  x  ->  (
p `  b )  =  ( x `  b ) )
206205fveq2d 5529 . . . . . . . . . . . 12  |-  ( p  =  x  ->  ( F `  ( p `  b ) )  =  ( F `  (
x `  b )
) )
207206oveq1d 5873 . . . . . . . . . . 11  |-  ( p  =  x  ->  (
( F `  (
p `  b )
)  .x.  ( T  gsumg  ( b  o F  .^  G ) ) )  =  ( ( F `
 ( x `  b ) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) )
208207mpteq2dv 4107 . . . . . . . . . 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 5874 . . . . . . . . 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 5883 . . . . . . . . 9  |-  ( S 
gsumg  ( b  e.  D  |->  ( ( F `  ( x `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) )  e. 
_V
211209, 32, 210fvmpt 5602 . . . . . . . 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 5524 . . . . . . . . . . . . 13  |-  ( p  =  y  ->  (
p `  b )  =  ( y `  b ) )
214213fveq2d 5529 . . . . . . . . . . . 12  |-  ( p  =  y  ->  ( F `  ( p `  b ) )  =  ( F `  (
y `  b )
) )
215214oveq1d 5873 . . . . . . . . . . 11  |-  ( p  =  y  ->  (
( F `  (
p `  b )
)  .x.  ( T  gsumg  ( b  o F  .^  G ) ) )  =  ( ( F `
 ( y `  b ) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) )
216215mpteq2dv 4107 . . . . . . . . . 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 5874 . . . . . . . . 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 5883 . . . . . . . . 9  |-  ( S 
gsumg  ( b  e.  D  |->  ( ( F `  ( y `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) )  e. 
_V
219217, 32, 218fvmpt 5602 . . . . . . . 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 5876 . . . . . 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 2325 . . . . 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 14692 . . . 4  |-  ( ph  ->  E  e.  ( P 
GrpHom  S ) )
224 eqid 2283 . . . . . . . . . . 11  |-  (mulGrp `  R )  =  (mulGrp `  R )
225224, 29rhmmhm 15502 . . . . . . . . . 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 16178 . . . . . . . . 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 5663 . . . . . . . . 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 16178 . . . . . . . . 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 5663 . . . . . . . . 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 15331 . . . . . . . . 9  |-  K  =  ( Base `  (mulGrp `  R ) )
239 eqid 2283 . . . . . . . . . 10  |-  ( .r
`  R )  =  ( .r `  R
)
240224, 239mgpplusg 15329 . . . . . . . . 9  |-  ( .r
`  R )  =  ( +g  `  (mulGrp `  R ) )
24129, 5mgpplusg 15329 . . . . . . . . 9  |-  .x.  =  ( +g  `  T )
242238, 240, 241mhmlin 14422 . . . . . . . 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 16113 . . . . . . . . . . . . . . 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 5663 . . . . . . . . . . . . . 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 16113 . . . . . . . . . . . . . . 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 5663 . . . . . . . . . . . . . 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 5663 . . . . . . . . . . . . . 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 14590 . . . . . . . . . . . . 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 4106 . . . . . . . . . . 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 5883 . . . . . . . . . . . . 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 5539 . . . . . . . . . . . . 13  |-  ( G `
 v )  e. 
_V
265264a1i 10 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
z  e.  D  /\  w  e.  D )
)  /\  v  e.  I )  ->  ( G `  v )  e.  _V )
266 ffn 5389 . . . . . . . . . . . . . 14  |-  ( z : I --> NN0  ->  z  Fn  I )
267248, 266syl 15 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  -> 
z  Fn  I )
268 ffn 5389 . . . . . . . . . . . . . 14  |-  ( w : I --> NN0  ->  w  Fn  I )
269253, 268syl 15 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  ->  w  Fn  I )
270 inidm 3378 . . . . . . . . . . . . 13  |-  ( I  i^i  I )  =  I
271 eqidd 2284 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  e.  D  /\  w  e.  D )
)  /\  v  e.  I )  ->  (
z `  v )  =  ( z `  v ) )
272 eqidd 2284 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  e.  D  /\  w  e.  D )
)  /\  v  e.  I )  ->  (
w `  v )  =  ( w `  v ) )
273267, 269, 245, 245, 270, 271, 272offval 6085 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  -> 
( z  o F  +  w )  =  ( v  e.  I  |->  ( ( z `  v )  +  ( w `  v ) ) ) )
27437feqmptd 5575 . . . . . . . . . . . . 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 6095 . . . . . . . . . . 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 5883 . . . . . . . . . . . . 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 5883 . . . . . . . . . . . . 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 5389 . . . . . . . . . . . . . . 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 2284 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  e.  D  /\  w  e.  D )
)  /\  v  e.  I )  ->  ( G `  v )  =  ( G `  v ) )
285267, 283, 245, 245, 270, 271, 284offval 6085 . . . . . . . . . . . 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 6085 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( z  e.  D  /\  w  e.  D ) )  -> 
( w  o F 
.^  G )  =  ( v  e.  I  |->  ( ( w `  v )  .^  ( G `  v )
) ) )
287245, 278, 280, 285, 286offval2 6095 . . . . . . . . . . 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 2325 . . . . . . . . . 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 5874 . . . . . . . . 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 16247 . . . . . . . . . . 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 16247 . . . . . . . . . . 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 15205 . . . . . . . . 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 2315 . . . . . . . 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 5876 . . . . . 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 5663 . . . . . . . 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 5663 . . . . . . . 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 16248 . . . . . . . 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 16248 . . . . . . . 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 15108 . . . . . . 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 2315 . . . . 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 16116 . . . . . . 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 15354 . . . . . . 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 19398 . . . . 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 19398 . . . . . 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 19398 . . . . . 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 5876 . . . . 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 2325 . . . 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 16249 . . 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 15507 . 2  |-  ( ph  ->  E  e.  ( P RingHom  S ) )
331 ovex 5883 . . . . . 6  |-  ( S 
gsumg  ( b  e.  D  |->  ( ( F `  ( p `  b
) )  .x.  ( T  gsumg  ( b  o F 
.^  G ) ) ) ) )  e. 
_V
332331, 32fnmpti 5372 . . . . 5  |-  E  Fn  B
333332a1i 10 . . . 4  |-  ( ph  ->  E  Fn  B )
33416, 1rhmf 15504 . . . . . 6  |-  ( A  e.  ( R RingHom  P
)  ->  A : K
--> B )
33592, 334syl 15 . . . . 5  |-  ( ph  ->  A : K --> B )
336 ffn 5389 . . . . 5  |-  ( A : K --> B  ->  A  Fn  K )
337335, 336syl 15 . . . 4  |-  ( ph  ->  A  Fn  K )
338 frn 5395 . . . . 5  |-  ( A : K --> B  ->  ran  A  C_  B )
339335, 338syl 15 . . . 4  |-  ( ph  ->  ran  A  C_  B
)
340 fnco 5352 . . . 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 5389 . . . 4  |-  ( F : K --> C  ->  F  Fn  K )
34371, 342syl 15 . . 3  |-  ( ph  ->  F  Fn  K )
344 fvco2 5594 . . . . 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 2315 . . 3  |-  ( (
ph  /\  x  e.  K )  ->  (
( E  o.  A
) `  x )  =  ( F `  x ) )
347341, 343, 346eqfnfvd 5625 . 2  |-  ( ph  ->  ( E  o.  A
)  =  F )
34810, 31, 1, 6, 9mvrf2 16233 . . . . 5  |-  ( ph  ->  V : I --> B )
349 ffn 5389 . . . . 5  |-  ( V : I --> B  ->  V  Fn  I )
350348, 349syl 15 . . . 4  |-  ( ph  ->  V  Fn  I )
351 frn 5395 . . . . 5  |-  ( V : I --> B  ->  ran  V  C_  B )
352348, 351syl 15 . . . 4  |-  ( ph  ->  ran  V  C_  B
)
353 fnco 5352 . . . 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 5594 . . . . 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 16166 . . . . . 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 5529 . . . . 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 16236 . . . . . . . 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 19398 . . . . 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 9981 . . . . . . . . . . . . . 14  |-  1  e.  NN0
372 0nn0 9980 . . . . . . . . . . . . . 14  |-  0  e.  NN0
373371, 372keepel 3622 . . . . . . . . . . . . 13  |-  if ( z  =  x ,  1 ,  0 )  e.  NN0
374373a1i 10 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  I )  ->  if ( z  =  x ,  1 ,  0 )  e.  NN0 )
375 ffvelrn 5663 . . . . . . . . . . . . 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 2284 . . . . . . . . . . . 12  |-  ( ph  ->  ( z  e.  I  |->  if ( z  =  x ,  1 ,  0 ) )  =  ( z  e.  I  |->  if ( z  =  x ,  1 ,  0 ) ) )
37837feqmptd 5575 . . . . . . . . . . . 12  |-  ( ph  ->  G  =  ( z  e.  I  |->  ( G `
 z ) ) )
3796, 374, 376, 377, 378offval2 6095 . . . . . . . . . . 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 5865 . . . . . . . . . . . . . 14  |-  ( 1  =  if ( z  =  x ,  1 ,  0 )  -> 
( 1  .^  ( G `  z )
)  =  ( if ( z  =  x ,  1 ,  0 )  .^  ( G `  z ) ) )
381380eqeq1d 2291 . . . . . . . . . . . . 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 5865 . . . . . . . . . . . . . 14  |-  ( 0  =  if ( z  =  x ,  1 ,  0 )  -> 
( 0  .^  ( G `  z )
)  =  ( if ( z  =  x ,  1 ,  0 )  .^  ( G `  z ) ) )
383382eqeq1d 2291 . . . . . . . . . . . . 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 14574 . . . . . . . . . . . . . . 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 3571 . . . . . . . . . . . . . . 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 2318 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  z  e.  I )  /\  z  =  x )  ->  (
1  .^  ( G `  z ) )  =  if ( z  =  x ,  ( G `
 z ) ,  ( 1r `  S
) ) )
39053, 54, 30mulg0 14572 . . . . . . . . . . . . . . . 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 3572 . . . . . . . . . . . . . . 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 2318 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  z  e.  I )  /\  -.  z  =  x )  ->  ( 0  .^  ( G `  z )
)  =  if ( z  =  x ,  ( G `  z
) ,  ( 1r
`  S ) ) )
396381, 383, 389, 395ifbothda 3595 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  I )  ->  ( if ( z  =  x ,  1 ,  0 )  .^  ( G `  z ) )  =  if ( z  =  x ,  ( G `
 z ) ,  ( 1r `  S
) ) )
397396mpteq2dva 4106 . . . . . . . . . . 11  |-  ( ph  ->  ( z  e.  I  |->  ( if ( z  =  x ,  1 ,  0 )  .^  ( G `  z ) ) )  =  ( z  e.  I  |->  if ( z  =  x ,  ( G `  z ) ,  ( 1r `  S ) ) ) )
398379, 397eqtrd 2315 . . . . . . . . . 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 5874 . . . . . . . 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 15361 . . . . . . . . . . . . 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 3601 . . . . . . . . . . 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 2283 . . . . . . . . . 10  |-  ( z  e.  I  |->  if ( z  =  x ,  ( G `  z
) ,  ( 1r
`  S ) ) )  =  ( z  e.  I  |->  if ( z  =  x ,  ( G `  z
) ,  ( 1r
`  S ) ) )
409407, 408fmptd 5684 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  I )  ->  (
z  e.  I  |->  if ( z  =  x ,  ( G `  z ) ,  ( 1r `  S ) ) ) : I --> C )
410 eldifn 3299 . . . . . . . . . . . . 13  |-  ( z  e.  ( I  \  { x } )  ->  -.  z  e.  { x } )
411 elsn 3655 . . . . . . . . . . . . 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 6073 . . . . . . . . 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 15222 . . . . . . . 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 5525 . . . . . . . . . . 11  |-  ( z  =  x  ->  ( G `  z )  =  ( G `  x ) )
418387, 417eqtrd 2315 . . . . . . . . . 10  |-  ( z  =  x  ->  if ( z  =  x ,  ( G `  z ) ,  ( 1r `  S ) )  =  ( G `
 x ) )
419418, 408, 45fvmpt 5602 . . . . . . . . 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 2319 . . . . . . 7  |-  ( (
ph  /\  x  e.  I )  ->  ( T  gsumg  ( ( z  e.  I  |->  if ( z  =  x ,  1 ,  0 ) )  o F  .^  G
) )  =  ( G `  x ) )
422370, 421oveq12d 5876 . . . . . 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 15364 . . . . . . 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 2315 . . . . 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 2319 . . . 4  |-  ( (
ph  /\  x  e.  I )  ->  ( E `  ( V `  x ) )  =  ( G `  x
) )
428356, 427eqtrd 2315 . . 3  |-  ( (
ph  /\  x  e.  I )  ->  (
( E  o.  V
) `  x )  =  ( G `  x ) )
429354, 282, 428eqfnfvd 5625 . 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 1623    e. wcel 1684   A.wral 2543   {crab 2547   _Vcvv 2788    \ cdif 3149    C_ wss 3152   ifcif 3565   {csn 3640    e. cmpt 4077    X. cxp 4687   `'ccnv 4688   ran crn 4690   "cima 4692    o. ccom 4693    Fn wfn 5250   -->wf 5251   ` cfv 5255  (class class class)co 5858    o Fcof 6076    ^m cmap 6772   Fincfn 6863   0cc0 8737   1c1 8738    + caddc 8740   NNcn 9746   NN0cn0 9965   ZZcz 10024   Basecbs 13148   +g cplusg 13208   .rcmulr 13209  Scalarcsca 13211   0gc0g 13400    gsumg cgsu 13401   Mndcmnd 14361   Grpcgrp 14362  .gcmg 14366   MndHom cmhm 14413    GrpHom cghm 14680  CMndccmn 15089  mulGrpcmgp 15325   Ringcrg 15337   CRingccrg 15338   1rcur 15339   RingHom crh 15494  AssAlgcasa 16050  algSccascl 16052   mVar cmvr 16088   mPoly cmpl 16089
This theorem is referenced by:  evlseu  19400
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-rep 4131  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-inf2 7342  ax-cnex 8793  ax-resscn 8794  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-addrcl 8798  ax-mulcl 8799  ax-mulrcl 8800  ax-mulcom 8801  ax-addass 8802  ax-mulass 8803  ax-distr 8804  ax-i2m1 8805  ax-1ne0 8806  ax-1rid 8807  ax-rnegex 8808  ax-rrecex 8809  ax-cnre 8810  ax-pre-lttri 8811  ax-pre-lttrn 8812  ax-pre-ltadd 8813  ax-pre-mulgt0 8814
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 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-nel 2449  df-ral 2548  df-rex 2549  df-reu 2550  df-rmo 2551  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-int 3863  df-iun 3907  df-iin 3908  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-se 4353  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-isom 5264  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-of 6078  df-ofr 6079  df-1st 6122  df-2nd 6123  df-riota 6304  df-recs 6388  df-rdg 6423  df-1o 6479  df-2o 6480  df-oadd 6483  df-er 6660  df-map 6774  df-pm 6775  df-ixp 6818  df-en 6864  df-dom 6865  df-sdom 6866  df-fin 6867  df-oi 7225  df-card 7572  df-pnf 8869  df-mnf 8870  df-xr 8871  df-ltxr 8872  df-le 8873  df-sub 9039  df-neg 9040  df-nn 9747  df-2 9804  df-3 9805  df-4 9806  df-5 9807  df-6 9808  df-7 9809  df-8 9810  df-9 9811  df-n0 9966  df-z 10025  df-uz 10231  df-fz 10783  df-fzo 10871  df-seq 11047  df-hash 11338  df-struct 13150  df-ndx 13151  df-slot 13152  df-base 13153  df-sets 13154  df-ress 13155  df-plusg 13221  df-mulr 13222  df-sca 13224  df-vsca 13225  df-tset 13227  df-0g 13404  df-gsum 13405  df-mre 13488  df-mrc 13489  df-acs 13491  df-mnd 14367  df-mhm 14415  df-submnd 14416  df-grp 14489  df-minusg 14490  df-sbg 14491  df-mulg 14492  df-subg 14618  df-ghm 14681  df-cntz 14793  df-cmn 15091  df-abl 15092  df-mgp 15326  df-rng 15340  df-cring 15341  df-ur 15342  df-rnghom 15496  df-subrg 15543  df-lmod 15629  df-lss 15690  df-assa 16053  df-ascl 16055  df-psr 16098  df-mvr 16099  df-mpl 16100
  Copyright terms: Public domain W3C validator