Metamath Proof Explorer

Theorem evlslem1

Description: Lemma for evlseu , give a formula for (the unique) polynomial evaluation homomorphism. (Contributed by Stefan O'Rear, 9-Mar-2015) (Proof shortened by AV, 26-Jul-2019) (Revised by AV, 11-Apr-2024)

Ref Expression
Hypotheses evlslem1.p 
|- P = ( I mPoly R )
evlslem1.b 
|- B = ( Base ` P )
evlslem1.c 
|- C = ( Base ` S )
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 gsum ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) )
evlslem1.i 
|- ( ph -> I e. W )
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 evlslem1 
|- ( ph -> ( E e. ( P RingHom S ) /\ ( E o. A ) = F /\ ( E o. V ) = G ) )

Proof

Step Hyp Ref Expression
1 evlslem1.p 
 |-  P = ( I mPoly R )
2 evlslem1.b 
 |-  B = ( Base ` P )
3 evlslem1.c 
 |-  C = ( Base ` S )
4 evlslem1.d 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
5 evlslem1.t 
 |-  T = ( mulGrp ` S )
6 evlslem1.x 
 |-  .^ = ( .g ` T )
7 evlslem1.m 
 |-  .x. = ( .r ` S )
8 evlslem1.v 
 |-  V = ( I mVar R )
9 evlslem1.e 
 |-  E = ( p e. B |-> ( S gsum ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) )
10 evlslem1.i 
 |-  ( ph -> I e. W )
11 evlslem1.r 
 |-  ( ph -> R e. CRing )
12 evlslem1.s 
 |-  ( ph -> S e. CRing )
13 evlslem1.f 
 |-  ( ph -> F e. ( R RingHom S ) )
14 evlslem1.g 
 |-  ( ph -> G : I --> C )
15 evlslem1.a 
 |-  A = ( algSc ` P )
16 eqid 
 |-  ( 1r ` P ) = ( 1r ` P )
17 eqid 
 |-  ( 1r ` S ) = ( 1r ` S )
18 eqid 
 |-  ( .r ` P ) = ( .r ` P )
19 11 crngringd 
 |-  ( ph -> R e. Ring )
20 1 mplring 
 |-  ( ( I e. W /\ R e. Ring ) -> P e. Ring )
21 10 19 20 syl2anc 
 |-  ( ph -> P e. Ring )
22 12 crngringd 
 |-  ( ph -> S e. Ring )
23 2fveq3 
 |-  ( x = ( 1r ` R ) -> ( E ` ( A ` x ) ) = ( E ` ( A ` ( 1r ` R ) ) ) )
24 fveq2 
 |-  ( x = ( 1r ` R ) -> ( F ` x ) = ( F ` ( 1r ` R ) ) )
25 23 24 eqeq12d 
 |-  ( x = ( 1r ` R ) -> ( ( E ` ( A ` x ) ) = ( F ` x ) <-> ( E ` ( A ` ( 1r ` R ) ) ) = ( F ` ( 1r ` R ) ) ) )
26 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
27 eqid 
 |-  ( Base ` R ) = ( Base ` R )
28 10 adantr 
 |-  ( ( ph /\ x e. ( Base ` R ) ) -> I e. W )
29 19 adantr 
 |-  ( ( ph /\ x e. ( Base ` R ) ) -> R e. Ring )
30 simpr 
 |-  ( ( ph /\ x e. ( Base ` R ) ) -> x e. ( Base ` R ) )
31 1 4 26 27 15 28 29 30 mplascl 
 |-  ( ( ph /\ x e. ( Base ` R ) ) -> ( A ` x ) = ( y e. D |-> if ( y = ( I X. { 0 } ) , x , ( 0g ` R ) ) ) )
32 31 fveq2d 
 |-  ( ( ph /\ x e. ( Base ` R ) ) -> ( E ` ( A ` x ) ) = ( E ` ( y e. D |-> if ( y = ( I X. { 0 } ) , x , ( 0g ` R ) ) ) ) )
33 11 adantr 
 |-  ( ( ph /\ x e. ( Base ` R ) ) -> R e. CRing )
34 12 adantr 
 |-  ( ( ph /\ x e. ( Base ` R ) ) -> S e. CRing )
35 13 adantr 
 |-  ( ( ph /\ x e. ( Base ` R ) ) -> F e. ( R RingHom S ) )
36 14 adantr 
 |-  ( ( ph /\ x e. ( Base ` R ) ) -> G : I --> C )
37 4 psrbag0 
 |-  ( I e. W -> ( I X. { 0 } ) e. D )
38 10 37 syl 
 |-  ( ph -> ( I X. { 0 } ) e. D )
39 38 adantr 
 |-  ( ( ph /\ x e. ( Base ` R ) ) -> ( I X. { 0 } ) e. D )
40 1 2 3 27 4 5 6 7 8 9 28 33 34 35 36 26 39 30 evlslem3 
 |-  ( ( ph /\ x e. ( Base ` R ) ) -> ( E ` ( y e. D |-> if ( y = ( I X. { 0 } ) , x , ( 0g ` R ) ) ) ) = ( ( F ` x ) .x. ( T gsum ( ( I X. { 0 } ) oF .^ G ) ) ) )
41 0zd 
 |-  ( ( ph /\ x e. I ) -> 0 e. ZZ )
42 fvexd 
 |-  ( ( ph /\ x e. I ) -> ( G ` x ) e. _V )
43 fconstmpt 
 |-  ( I X. { 0 } ) = ( x e. I |-> 0 )
44 43 a1i 
 |-  ( ph -> ( I X. { 0 } ) = ( x e. I |-> 0 ) )
45 14 feqmptd 
 |-  ( ph -> G = ( x e. I |-> ( G ` x ) ) )
46 10 41 42 44 45 offval2 
 |-  ( ph -> ( ( I X. { 0 } ) oF .^ G ) = ( x e. I |-> ( 0 .^ ( G ` x ) ) ) )
47 14 ffvelrnda 
 |-  ( ( ph /\ x e. I ) -> ( G ` x ) e. C )
48 5 3 mgpbas 
 |-  C = ( Base ` T )
49 5 17 ringidval 
 |-  ( 1r ` S ) = ( 0g ` T )
50 48 49 6 mulg0 
 |-  ( ( G ` x ) e. C -> ( 0 .^ ( G ` x ) ) = ( 1r ` S ) )
51 47 50 syl 
 |-  ( ( ph /\ x e. I ) -> ( 0 .^ ( G ` x ) ) = ( 1r ` S ) )
52 51 mpteq2dva 
 |-  ( ph -> ( x e. I |-> ( 0 .^ ( G ` x ) ) ) = ( x e. I |-> ( 1r ` S ) ) )
53 46 52 eqtrd 
 |-  ( ph -> ( ( I X. { 0 } ) oF .^ G ) = ( x e. I |-> ( 1r ` S ) ) )
54 53 oveq2d 
 |-  ( ph -> ( T gsum ( ( I X. { 0 } ) oF .^ G ) ) = ( T gsum ( x e. I |-> ( 1r ` S ) ) ) )
55 5 crngmgp 
 |-  ( S e. CRing -> T e. CMnd )
56 12 55 syl 
 |-  ( ph -> T e. CMnd )
57 56 cmnmndd 
 |-  ( ph -> T e. Mnd )
58 49 gsumz 
 |-  ( ( T e. Mnd /\ I e. W ) -> ( T gsum ( x e. I |-> ( 1r ` S ) ) ) = ( 1r ` S ) )
59 57 10 58 syl2anc 
 |-  ( ph -> ( T gsum ( x e. I |-> ( 1r ` S ) ) ) = ( 1r ` S ) )
60 54 59 eqtrd 
 |-  ( ph -> ( T gsum ( ( I X. { 0 } ) oF .^ G ) ) = ( 1r ` S ) )
61 60 adantr 
 |-  ( ( ph /\ x e. ( Base ` R ) ) -> ( T gsum ( ( I X. { 0 } ) oF .^ G ) ) = ( 1r ` S ) )
62 61 oveq2d 
 |-  ( ( ph /\ x e. ( Base ` R ) ) -> ( ( F ` x ) .x. ( T gsum ( ( I X. { 0 } ) oF .^ G ) ) ) = ( ( F ` x ) .x. ( 1r ` S ) ) )
63 27 3 rhmf 
 |-  ( F e. ( R RingHom S ) -> F : ( Base ` R ) --> C )
64 13 63 syl 
 |-  ( ph -> F : ( Base ` R ) --> C )
65 64 ffvelrnda 
 |-  ( ( ph /\ x e. ( Base ` R ) ) -> ( F ` x ) e. C )
66 3 7 17 ringridm 
 |-  ( ( S e. Ring /\ ( F ` x ) e. C ) -> ( ( F ` x ) .x. ( 1r ` S ) ) = ( F ` x ) )
67 22 65 66 syl2an2r 
 |-  ( ( ph /\ x e. ( Base ` R ) ) -> ( ( F ` x ) .x. ( 1r ` S ) ) = ( F ` x ) )
68 62 67 eqtrd 
 |-  ( ( ph /\ x e. ( Base ` R ) ) -> ( ( F ` x ) .x. ( T gsum ( ( I X. { 0 } ) oF .^ G ) ) ) = ( F ` x ) )
69 32 40 68 3eqtrd 
 |-  ( ( ph /\ x e. ( Base ` R ) ) -> ( E ` ( A ` x ) ) = ( F ` x ) )
70 69 ralrimiva 
 |-  ( ph -> A. x e. ( Base ` R ) ( E ` ( A ` x ) ) = ( F ` x ) )
71 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
72 27 71 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
73 19 72 syl 
 |-  ( ph -> ( 1r ` R ) e. ( Base ` R ) )
74 25 70 73 rspcdva 
 |-  ( ph -> ( E ` ( A ` ( 1r ` R ) ) ) = ( F ` ( 1r ` R ) ) )
75 1 mplassa 
 |-  ( ( I e. W /\ R e. CRing ) -> P e. AssAlg )
76 10 11 75 syl2anc 
 |-  ( ph -> P e. AssAlg )
77 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
78 15 77 asclrhm 
 |-  ( P e. AssAlg -> A e. ( ( Scalar ` P ) RingHom P ) )
79 76 78 syl 
 |-  ( ph -> A e. ( ( Scalar ` P ) RingHom P ) )
80 1 10 11 mplsca 
 |-  ( ph -> R = ( Scalar ` P ) )
81 80 oveq1d 
 |-  ( ph -> ( R RingHom P ) = ( ( Scalar ` P ) RingHom P ) )
82 79 81 eleqtrrd 
 |-  ( ph -> A e. ( R RingHom P ) )
83 71 16 rhm1 
 |-  ( A e. ( R RingHom P ) -> ( A ` ( 1r ` R ) ) = ( 1r ` P ) )
84 82 83 syl 
 |-  ( ph -> ( A ` ( 1r ` R ) ) = ( 1r ` P ) )
85 84 fveq2d 
 |-  ( ph -> ( E ` ( A ` ( 1r ` R ) ) ) = ( E ` ( 1r ` P ) ) )
86 71 17 rhm1 
 |-  ( F e. ( R RingHom S ) -> ( F ` ( 1r ` R ) ) = ( 1r ` S ) )
87 13 86 syl 
 |-  ( ph -> ( F ` ( 1r ` R ) ) = ( 1r ` S ) )
88 74 85 87 3eqtr3d 
 |-  ( ph -> ( E ` ( 1r ` P ) ) = ( 1r ` S ) )
89 eqid 
 |-  ( +g ` P ) = ( +g ` P )
90 eqid 
 |-  ( +g ` S ) = ( +g ` S )
91 21 ringgrpd 
 |-  ( ph -> P e. Grp )
92 22 ringgrpd 
 |-  ( ph -> S e. Grp )
93 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
94 ringcmn 
 |-  ( S e. Ring -> S e. CMnd )
95 22 94 syl 
 |-  ( ph -> S e. CMnd )
96 95 adantr 
 |-  ( ( ph /\ p e. B ) -> S e. CMnd )
97 ovex 
 |-  ( NN0 ^m I ) e. _V
98 4 97 rabex2 
 |-  D e. _V
99 98 a1i 
 |-  ( ( ph /\ p e. B ) -> D e. _V )
100 10 adantr 
 |-  ( ( ph /\ p e. B ) -> I e. W )
101 11 adantr 
 |-  ( ( ph /\ p e. B ) -> R e. CRing )
102 12 adantr 
 |-  ( ( ph /\ p e. B ) -> S e. CRing )
103 13 adantr 
 |-  ( ( ph /\ p e. B ) -> F e. ( R RingHom S ) )
104 14 adantr 
 |-  ( ( ph /\ p e. B ) -> G : I --> C )
105 simpr 
 |-  ( ( ph /\ p e. B ) -> p e. B )
106 1 2 3 4 5 6 7 8 9 100 101 102 103 104 105 evlslem6 
 |-  ( ( ph /\ p e. B ) -> ( ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) : D --> C /\ ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) finSupp ( 0g ` S ) ) )
107 106 simpld 
 |-  ( ( ph /\ p e. B ) -> ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) : D --> C )
108 106 simprd 
 |-  ( ( ph /\ p e. B ) -> ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) finSupp ( 0g ` S ) )
109 3 93 96 99 107 108 gsumcl 
 |-  ( ( ph /\ p e. B ) -> ( S gsum ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) e. C )
110 109 9 fmptd 
 |-  ( ph -> E : B --> C )
111 eqid 
 |-  ( +g ` R ) = ( +g ` R )
112 simplrl 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> x e. B )
113 simplrr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> y e. B )
114 1 2 111 89 112 113 mpladd 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( x ( +g ` P ) y ) = ( x oF ( +g ` R ) y ) )
115 114 fveq1d 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( ( x ( +g ` P ) y ) ` b ) = ( ( x oF ( +g ` R ) y ) ` b ) )
116 simprl 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> x e. B )
117 1 27 2 4 116 mplelf 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> x : D --> ( Base ` R ) )
118 117 ffnd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> x Fn D )
119 118 adantr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> x Fn D )
120 simprr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> y e. B )
121 1 27 2 4 120 mplelf 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> y : D --> ( Base ` R ) )
122 121 ffnd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> y Fn D )
123 122 adantr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> y Fn D )
124 98 a1i 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> D e. _V )
125 simpr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> b e. D )
126 fnfvof 
 |-  ( ( ( x Fn D /\ y Fn D ) /\ ( D e. _V /\ b e. D ) ) -> ( ( x oF ( +g ` R ) y ) ` b ) = ( ( x ` b ) ( +g ` R ) ( y ` b ) ) )
127 119 123 124 125 126 syl22anc 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( ( x oF ( +g ` R ) y ) ` b ) = ( ( x ` b ) ( +g ` R ) ( y ` b ) ) )
128 115 127 eqtrd 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( ( x ( +g ` P ) y ) ` b ) = ( ( x ` b ) ( +g ` R ) ( y ` b ) ) )
129 128 fveq2d 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( F ` ( ( x ( +g ` P ) y ) ` b ) ) = ( F ` ( ( x ` b ) ( +g ` R ) ( y ` b ) ) ) )
130 rhmghm 
 |-  ( F e. ( R RingHom S ) -> F e. ( R GrpHom S ) )
131 13 130 syl 
 |-  ( ph -> F e. ( R GrpHom S ) )
132 131 ad2antrr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> F e. ( R GrpHom S ) )
133 117 ffvelrnda 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( x ` b ) e. ( Base ` R ) )
134 121 ffvelrnda 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( y ` b ) e. ( Base ` R ) )
135 27 111 90 ghmlin 
 |-  ( ( F e. ( R GrpHom S ) /\ ( x ` b ) e. ( Base ` R ) /\ ( y ` b ) e. ( Base ` R ) ) -> ( F ` ( ( x ` b ) ( +g ` R ) ( y ` b ) ) ) = ( ( F ` ( x ` b ) ) ( +g ` S ) ( F ` ( y ` b ) ) ) )
136 132 133 134 135 syl3anc 
 |-  ( ( ( 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 ) ) ) )
137 129 136 eqtrd 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( F ` ( ( x ( +g ` P ) y ) ` b ) ) = ( ( F ` ( x ` b ) ) ( +g ` S ) ( F ` ( y ` b ) ) ) )
138 137 oveq1d 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( ( F ` ( ( x ( +g ` P ) y ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) = ( ( ( F ` ( x ` b ) ) ( +g ` S ) ( F ` ( y ` b ) ) ) .x. ( T gsum ( b oF .^ G ) ) ) )
139 22 ad2antrr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> S e. Ring )
140 64 ad2antrr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> F : ( Base ` R ) --> C )
141 140 133 ffvelrnd 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( F ` ( x ` b ) ) e. C )
142 140 134 ffvelrnd 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( F ` ( y ` b ) ) e. C )
143 56 ad2antrr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> T e. CMnd )
144 14 ad2antrr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> G : I --> C )
145 4 48 6 143 125 144 psrbagev2 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( T gsum ( b oF .^ G ) ) e. C )
146 3 90 7 ringdir 
 |-  ( ( S e. Ring /\ ( ( F ` ( x ` b ) ) e. C /\ ( F ` ( y ` b ) ) e. C /\ ( T gsum ( b oF .^ G ) ) e. C ) ) -> ( ( ( F ` ( x ` b ) ) ( +g ` S ) ( F ` ( y ` b ) ) ) .x. ( T gsum ( b oF .^ G ) ) ) = ( ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ( +g ` S ) ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) )
147 139 141 142 145 146 syl13anc 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( ( ( F ` ( x ` b ) ) ( +g ` S ) ( F ` ( y ` b ) ) ) .x. ( T gsum ( b oF .^ G ) ) ) = ( ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ( +g ` S ) ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) )
148 138 147 eqtrd 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( ( F ` ( ( x ( +g ` P ) y ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) = ( ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ( +g ` S ) ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) )
149 148 mpteq2dva 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( b e. D |-> ( ( F ` ( ( x ( +g ` P ) y ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) = ( b e. D |-> ( ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ( +g ` S ) ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) )
150 98 a1i 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> D e. _V )
151 ovexd 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) e. _V )
152 ovexd 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) e. _V )
153 eqidd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) = ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) )
154 eqidd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) = ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) )
155 150 151 152 153 154 offval2 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) oF ( +g ` S ) ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) = ( b e. D |-> ( ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ( +g ` S ) ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) )
156 149 155 eqtr4d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( b e. D |-> ( ( F ` ( ( x ( +g ` P ) y ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) = ( ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) oF ( +g ` S ) ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) )
157 156 oveq2d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( S gsum ( b e. D |-> ( ( F ` ( ( x ( +g ` P ) y ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) = ( S gsum ( ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) oF ( +g ` S ) ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) ) )
158 95 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> S e. CMnd )
159 10 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> I e. W )
160 11 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> R e. CRing )
161 12 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> S e. CRing )
162 13 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> F e. ( R RingHom S ) )
163 14 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> G : I --> C )
164 1 2 3 4 5 6 7 8 9 159 160 161 162 163 116 evlslem6 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) : D --> C /\ ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) finSupp ( 0g ` S ) ) )
165 164 simpld 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) : D --> C )
166 1 2 3 4 5 6 7 8 9 159 160 161 162 163 120 evlslem6 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) : D --> C /\ ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) finSupp ( 0g ` S ) ) )
167 166 simpld 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) : D --> C )
168 164 simprd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) finSupp ( 0g ` S ) )
169 166 simprd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) finSupp ( 0g ` S ) )
170 3 93 90 158 150 165 167 168 169 gsumadd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( S gsum ( ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) oF ( +g ` S ) ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) ) = ( ( S gsum ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) ( +g ` S ) ( S gsum ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) ) )
171 157 170 eqtrd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( S gsum ( b e. D |-> ( ( F ` ( ( x ( +g ` P ) y ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) = ( ( S gsum ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) ( +g ` S ) ( S gsum ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) ) )
172 91 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> P e. Grp )
173 2 89 grpcl 
 |-  ( ( P e. Grp /\ x e. B /\ y e. B ) -> ( x ( +g ` P ) y ) e. B )
174 172 116 120 173 syl3anc 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` P ) y ) e. B )
175 fveq1 
 |-  ( p = ( x ( +g ` P ) y ) -> ( p ` b ) = ( ( x ( +g ` P ) y ) ` b ) )
176 175 fveq2d 
 |-  ( p = ( x ( +g ` P ) y ) -> ( F ` ( p ` b ) ) = ( F ` ( ( x ( +g ` P ) y ) ` b ) ) )
177 176 oveq1d 
 |-  ( p = ( x ( +g ` P ) y ) -> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) = ( ( F ` ( ( x ( +g ` P ) y ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) )
178 177 mpteq2dv 
 |-  ( p = ( x ( +g ` P ) y ) -> ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) = ( b e. D |-> ( ( F ` ( ( x ( +g ` P ) y ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) )
179 178 oveq2d 
 |-  ( p = ( x ( +g ` P ) y ) -> ( S gsum ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) = ( S gsum ( b e. D |-> ( ( F ` ( ( x ( +g ` P ) y ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) )
180 ovex 
 |-  ( S gsum ( b e. D |-> ( ( F ` ( ( x ( +g ` P ) y ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) e. _V
181 179 9 180 fvmpt 
 |-  ( ( x ( +g ` P ) y ) e. B -> ( E ` ( x ( +g ` P ) y ) ) = ( S gsum ( b e. D |-> ( ( F ` ( ( x ( +g ` P ) y ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) )
182 174 181 syl 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( E ` ( x ( +g ` P ) y ) ) = ( S gsum ( b e. D |-> ( ( F ` ( ( x ( +g ` P ) y ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) )
183 fveq1 
 |-  ( p = x -> ( p ` b ) = ( x ` b ) )
184 183 fveq2d 
 |-  ( p = x -> ( F ` ( p ` b ) ) = ( F ` ( x ` b ) ) )
185 184 oveq1d 
 |-  ( p = x -> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) = ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) )
186 185 mpteq2dv 
 |-  ( p = x -> ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) = ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) )
187 186 oveq2d 
 |-  ( p = x -> ( S gsum ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) = ( S gsum ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) )
188 ovex 
 |-  ( S gsum ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) e. _V
189 187 9 188 fvmpt 
 |-  ( x e. B -> ( E ` x ) = ( S gsum ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) )
190 116 189 syl 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( E ` x ) = ( S gsum ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) )
191 fveq1 
 |-  ( p = y -> ( p ` b ) = ( y ` b ) )
192 191 fveq2d 
 |-  ( p = y -> ( F ` ( p ` b ) ) = ( F ` ( y ` b ) ) )
193 192 oveq1d 
 |-  ( p = y -> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) = ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) )
194 193 mpteq2dv 
 |-  ( p = y -> ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) = ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) )
195 194 oveq2d 
 |-  ( p = y -> ( S gsum ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) = ( S gsum ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) )
196 ovex 
 |-  ( S gsum ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) e. _V
197 195 9 196 fvmpt 
 |-  ( y e. B -> ( E ` y ) = ( S gsum ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) )
198 197 ad2antll 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( E ` y ) = ( S gsum ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) )
199 190 198 oveq12d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( E ` x ) ( +g ` S ) ( E ` y ) ) = ( ( S gsum ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) ( +g ` S ) ( S gsum ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) ) )
200 171 182 199 3eqtr4d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( E ` ( x ( +g ` P ) y ) ) = ( ( E ` x ) ( +g ` S ) ( E ` y ) ) )
201 2 3 89 90 91 92 110 200 isghmd 
 |-  ( ph -> E e. ( P GrpHom S ) )
202 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
203 202 5 rhmmhm 
 |-  ( F e. ( R RingHom S ) -> F e. ( ( mulGrp ` R ) MndHom T ) )
204 13 203 syl 
 |-  ( ph -> F e. ( ( mulGrp ` R ) MndHom T ) )
205 204 adantr 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> F e. ( ( mulGrp ` R ) MndHom T ) )
206 simprll 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> x e. B )
207 1 27 2 4 206 mplelf 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> x : D --> ( Base ` R ) )
208 simprrl 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> z e. D )
209 207 208 ffvelrnd 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( x ` z ) e. ( Base ` R ) )
210 simprlr 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> y e. B )
211 1 27 2 4 210 mplelf 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> y : D --> ( Base ` R ) )
212 simprrr 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> w e. D )
213 211 212 ffvelrnd 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( y ` w ) e. ( Base ` R ) )
214 202 27 mgpbas 
 |-  ( Base ` R ) = ( Base ` ( mulGrp ` R ) )
215 eqid 
 |-  ( .r ` R ) = ( .r ` R )
216 202 215 mgpplusg 
 |-  ( .r ` R ) = ( +g ` ( mulGrp ` R ) )
217 5 7 mgpplusg 
 |-  .x. = ( +g ` T )
218 214 216 217 mhmlin 
 |-  ( ( F e. ( ( mulGrp ` R ) MndHom T ) /\ ( x ` z ) e. ( Base ` R ) /\ ( y ` w ) e. ( Base ` R ) ) -> ( F ` ( ( x ` z ) ( .r ` R ) ( y ` w ) ) ) = ( ( F ` ( x ` z ) ) .x. ( F ` ( y ` w ) ) ) )
219 205 209 213 218 syl3anc 
 |-  ( ( 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 ) ) ) )
220 57 ad2antrr 
 |-  ( ( ( ph /\ ( z e. D /\ w e. D ) ) /\ v e. I ) -> T e. Mnd )
221 simprl 
 |-  ( ( ph /\ ( z e. D /\ w e. D ) ) -> z e. D )
222 4 psrbagf 
 |-  ( z e. D -> z : I --> NN0 )
223 221 222 syl 
 |-  ( ( ph /\ ( z e. D /\ w e. D ) ) -> z : I --> NN0 )
224 223 ffvelrnda 
 |-  ( ( ( ph /\ ( z e. D /\ w e. D ) ) /\ v e. I ) -> ( z ` v ) e. NN0 )
225 4 psrbagf 
 |-  ( w e. D -> w : I --> NN0 )
226 225 ad2antll 
 |-  ( ( ph /\ ( z e. D /\ w e. D ) ) -> w : I --> NN0 )
227 226 ffvelrnda 
 |-  ( ( ( ph /\ ( z e. D /\ w e. D ) ) /\ v e. I ) -> ( w ` v ) e. NN0 )
228 14 adantr 
 |-  ( ( ph /\ ( z e. D /\ w e. D ) ) -> G : I --> C )
229 228 ffvelrnda 
 |-  ( ( ( ph /\ ( z e. D /\ w e. D ) ) /\ v e. I ) -> ( G ` v ) e. C )
230 48 6 217 mulgnn0dir 
 |-  ( ( 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 ) ) ) )
231 220 224 227 229 230 syl13anc 
 |-  ( ( ( 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 ) ) ) )
232 231 mpteq2dva 
 |-  ( ( 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 ) ) ) ) )
233 10 adantr 
 |-  ( ( ph /\ ( z e. D /\ w e. D ) ) -> I e. W )
234 ovexd 
 |-  ( ( ( ph /\ ( z e. D /\ w e. D ) ) /\ v e. I ) -> ( ( z ` v ) + ( w ` v ) ) e. _V )
235 fvexd 
 |-  ( ( ( ph /\ ( z e. D /\ w e. D ) ) /\ v e. I ) -> ( G ` v ) e. _V )
236 223 ffnd 
 |-  ( ( ph /\ ( z e. D /\ w e. D ) ) -> z Fn I )
237 226 ffnd 
 |-  ( ( ph /\ ( z e. D /\ w e. D ) ) -> w Fn I )
238 inidm 
 |-  ( I i^i I ) = I
239 eqidd 
 |-  ( ( ( ph /\ ( z e. D /\ w e. D ) ) /\ v e. I ) -> ( z ` v ) = ( z ` v ) )
240 eqidd 
 |-  ( ( ( ph /\ ( z e. D /\ w e. D ) ) /\ v e. I ) -> ( w ` v ) = ( w ` v ) )
241 236 237 233 233 238 239 240 offval 
 |-  ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( z oF + w ) = ( v e. I |-> ( ( z ` v ) + ( w ` v ) ) ) )
242 14 feqmptd 
 |-  ( ph -> G = ( v e. I |-> ( G ` v ) ) )
243 242 adantr 
 |-  ( ( ph /\ ( z e. D /\ w e. D ) ) -> G = ( v e. I |-> ( G ` v ) ) )
244 233 234 235 241 243 offval2 
 |-  ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( ( z oF + w ) oF .^ G ) = ( v e. I |-> ( ( ( z ` v ) + ( w ` v ) ) .^ ( G ` v ) ) ) )
245 ovexd 
 |-  ( ( ( ph /\ ( z e. D /\ w e. D ) ) /\ v e. I ) -> ( ( z ` v ) .^ ( G ` v ) ) e. _V )
246 ovexd 
 |-  ( ( ( ph /\ ( z e. D /\ w e. D ) ) /\ v e. I ) -> ( ( w ` v ) .^ ( G ` v ) ) e. _V )
247 14 ffnd 
 |-  ( ph -> G Fn I )
248 247 adantr 
 |-  ( ( ph /\ ( z e. D /\ w e. D ) ) -> G Fn I )
249 eqidd 
 |-  ( ( ( ph /\ ( z e. D /\ w e. D ) ) /\ v e. I ) -> ( G ` v ) = ( G ` v ) )
250 236 248 233 233 238 239 249 offval 
 |-  ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( z oF .^ G ) = ( v e. I |-> ( ( z ` v ) .^ ( G ` v ) ) ) )
251 237 248 233 233 238 240 249 offval 
 |-  ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( w oF .^ G ) = ( v e. I |-> ( ( w ` v ) .^ ( G ` v ) ) ) )
252 233 245 246 250 251 offval2 
 |-  ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( ( z oF .^ G ) oF .x. ( w oF .^ G ) ) = ( v e. I |-> ( ( ( z ` v ) .^ ( G ` v ) ) .x. ( ( w ` v ) .^ ( G ` v ) ) ) ) )
253 232 244 252 3eqtr4d 
 |-  ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( ( z oF + w ) oF .^ G ) = ( ( z oF .^ G ) oF .x. ( w oF .^ G ) ) )
254 253 oveq2d 
 |-  ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( T gsum ( ( z oF + w ) oF .^ G ) ) = ( T gsum ( ( z oF .^ G ) oF .x. ( w oF .^ G ) ) ) )
255 56 adantr 
 |-  ( ( ph /\ ( z e. D /\ w e. D ) ) -> T e. CMnd )
256 4 48 6 49 255 221 228 psrbagev1 
 |-  ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( ( z oF .^ G ) : I --> C /\ ( z oF .^ G ) finSupp ( 1r ` S ) ) )
257 256 simpld 
 |-  ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( z oF .^ G ) : I --> C )
258 simprr 
 |-  ( ( ph /\ ( z e. D /\ w e. D ) ) -> w e. D )
259 4 48 6 49 255 258 228 psrbagev1 
 |-  ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( ( w oF .^ G ) : I --> C /\ ( w oF .^ G ) finSupp ( 1r ` S ) ) )
260 259 simpld 
 |-  ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( w oF .^ G ) : I --> C )
261 256 simprd 
 |-  ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( z oF .^ G ) finSupp ( 1r ` S ) )
262 259 simprd 
 |-  ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( w oF .^ G ) finSupp ( 1r ` S ) )
263 48 49 217 255 233 257 260 261 262 gsumadd 
 |-  ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( T gsum ( ( z oF .^ G ) oF .x. ( w oF .^ G ) ) ) = ( ( T gsum ( z oF .^ G ) ) .x. ( T gsum ( w oF .^ G ) ) ) )
264 254 263 eqtrd 
 |-  ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( T gsum ( ( z oF + w ) oF .^ G ) ) = ( ( T gsum ( z oF .^ G ) ) .x. ( T gsum ( w oF .^ G ) ) ) )
265 264 adantrl 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( T gsum ( ( z oF + w ) oF .^ G ) ) = ( ( T gsum ( z oF .^ G ) ) .x. ( T gsum ( w oF .^ G ) ) ) )
266 219 265 oveq12d 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( ( F ` ( ( x ` z ) ( .r ` R ) ( y ` w ) ) ) .x. ( T gsum ( ( z oF + w ) oF .^ G ) ) ) = ( ( ( F ` ( x ` z ) ) .x. ( F ` ( y ` w ) ) ) .x. ( ( T gsum ( z oF .^ G ) ) .x. ( T gsum ( w oF .^ G ) ) ) ) )
267 56 adantr 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> T e. CMnd )
268 64 adantr 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> F : ( Base ` R ) --> C )
269 268 209 ffvelrnd 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( F ` ( x ` z ) ) e. C )
270 268 213 ffvelrnd 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( F ` ( y ` w ) ) e. C )
271 4 48 6 255 221 228 psrbagev2 
 |-  ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( T gsum ( z oF .^ G ) ) e. C )
272 271 adantrl 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( T gsum ( z oF .^ G ) ) e. C )
273 4 48 6 255 258 228 psrbagev2 
 |-  ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( T gsum ( w oF .^ G ) ) e. C )
274 273 adantrl 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( T gsum ( w oF .^ G ) ) e. C )
275 48 217 cmn4 
 |-  ( ( T e. CMnd /\ ( ( F ` ( x ` z ) ) e. C /\ ( F ` ( y ` w ) ) e. C ) /\ ( ( T gsum ( z oF .^ G ) ) e. C /\ ( T gsum ( w oF .^ G ) ) e. C ) ) -> ( ( ( F ` ( x ` z ) ) .x. ( F ` ( y ` w ) ) ) .x. ( ( T gsum ( z oF .^ G ) ) .x. ( T gsum ( w oF .^ G ) ) ) ) = ( ( ( F ` ( x ` z ) ) .x. ( T gsum ( z oF .^ G ) ) ) .x. ( ( F ` ( y ` w ) ) .x. ( T gsum ( w oF .^ G ) ) ) ) )
276 267 269 270 272 274 275 syl122anc 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( ( ( F ` ( x ` z ) ) .x. ( F ` ( y ` w ) ) ) .x. ( ( T gsum ( z oF .^ G ) ) .x. ( T gsum ( w oF .^ G ) ) ) ) = ( ( ( F ` ( x ` z ) ) .x. ( T gsum ( z oF .^ G ) ) ) .x. ( ( F ` ( y ` w ) ) .x. ( T gsum ( w oF .^ G ) ) ) ) )
277 266 276 eqtrd 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( ( F ` ( ( x ` z ) ( .r ` R ) ( y ` w ) ) ) .x. ( T gsum ( ( z oF + w ) oF .^ G ) ) ) = ( ( ( F ` ( x ` z ) ) .x. ( T gsum ( z oF .^ G ) ) ) .x. ( ( F ` ( y ` w ) ) .x. ( T gsum ( w oF .^ G ) ) ) ) )
278 10 adantr 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> I e. W )
279 11 adantr 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> R e. CRing )
280 12 adantr 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> S e. CRing )
281 13 adantr 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> F e. ( R RingHom S ) )
282 14 adantr 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> G : I --> C )
283 4 psrbagaddcl 
 |-  ( ( z e. D /\ w e. D ) -> ( z oF + w ) e. D )
284 283 ad2antll 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( z oF + w ) e. D )
285 19 adantr 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> R e. Ring )
286 27 215 ringcl 
 |-  ( ( R e. Ring /\ ( x ` z ) e. ( Base ` R ) /\ ( y ` w ) e. ( Base ` R ) ) -> ( ( x ` z ) ( .r ` R ) ( y ` w ) ) e. ( Base ` R ) )
287 285 209 213 286 syl3anc 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( ( x ` z ) ( .r ` R ) ( y ` w ) ) e. ( Base ` R ) )
288 1 2 3 27 4 5 6 7 8 9 278 279 280 281 282 26 284 287 evlslem3 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( E ` ( v e. D |-> if ( v = ( z oF + w ) , ( ( x ` z ) ( .r ` R ) ( y ` w ) ) , ( 0g ` R ) ) ) ) = ( ( F ` ( ( x ` z ) ( .r ` R ) ( y ` w ) ) ) .x. ( T gsum ( ( z oF + w ) oF .^ G ) ) ) )
289 1 2 3 27 4 5 6 7 8 9 278 279 280 281 282 26 208 209 evlslem3 
 |-  ( ( 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 gsum ( z oF .^ G ) ) ) )
290 1 2 3 27 4 5 6 7 8 9 278 279 280 281 282 26 212 213 evlslem3 
 |-  ( ( 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 gsum ( w oF .^ G ) ) ) )
291 289 290 oveq12d 
 |-  ( ( 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 gsum ( z oF .^ G ) ) ) .x. ( ( F ` ( y ` w ) ) .x. ( T gsum ( w oF .^ G ) ) ) ) )
292 277 288 291 3eqtr4d 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( E ` ( v e. D |-> if ( v = ( z oF + 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 ) ) ) ) ) )
293 1 2 7 26 4 10 11 12 201 292 evlslem2 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( E ` ( x ( .r ` P ) y ) ) = ( ( E ` x ) .x. ( E ` y ) ) )
294 2 16 17 18 7 21 22 88 293 3 89 90 110 200 isrhmd 
 |-  ( ph -> E e. ( P RingHom S ) )
295 ovex 
 |-  ( S gsum ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) e. _V
296 295 9 fnmpti 
 |-  E Fn B
297 296 a1i 
 |-  ( ph -> E Fn B )
298 27 2 rhmf 
 |-  ( A e. ( R RingHom P ) -> A : ( Base ` R ) --> B )
299 82 298 syl 
 |-  ( ph -> A : ( Base ` R ) --> B )
300 299 ffnd 
 |-  ( ph -> A Fn ( Base ` R ) )
301 299 frnd 
 |-  ( ph -> ran A C_ B )
302 fnco 
 |-  ( ( E Fn B /\ A Fn ( Base ` R ) /\ ran A C_ B ) -> ( E o. A ) Fn ( Base ` R ) )
303 297 300 301 302 syl3anc 
 |-  ( ph -> ( E o. A ) Fn ( Base ` R ) )
304 64 ffnd 
 |-  ( ph -> F Fn ( Base ` R ) )
305 fvco2 
 |-  ( ( A Fn ( Base ` R ) /\ x e. ( Base ` R ) ) -> ( ( E o. A ) ` x ) = ( E ` ( A ` x ) ) )
306 300 305 sylan 
 |-  ( ( ph /\ x e. ( Base ` R ) ) -> ( ( E o. A ) ` x ) = ( E ` ( A ` x ) ) )
307 306 69 eqtrd 
 |-  ( ( ph /\ x e. ( Base ` R ) ) -> ( ( E o. A ) ` x ) = ( F ` x ) )
308 303 304 307 eqfnfvd 
 |-  ( ph -> ( E o. A ) = F )
309 1 8 2 10 19 mvrf2 
 |-  ( ph -> V : I --> B )
310 309 ffnd 
 |-  ( ph -> V Fn I )
311 309 frnd 
 |-  ( ph -> ran V C_ B )
312 fnco 
 |-  ( ( E Fn B /\ V Fn I /\ ran V C_ B ) -> ( E o. V ) Fn I )
313 297 310 311 312 syl3anc 
 |-  ( ph -> ( E o. V ) Fn I )
314 fvco2 
 |-  ( ( V Fn I /\ x e. I ) -> ( ( E o. V ) ` x ) = ( E ` ( V ` x ) ) )
315 310 314 sylan 
 |-  ( ( ph /\ x e. I ) -> ( ( E o. V ) ` x ) = ( E ` ( V ` x ) ) )
316 10 adantr 
 |-  ( ( ph /\ x e. I ) -> I e. W )
317 11 adantr 
 |-  ( ( ph /\ x e. I ) -> R e. CRing )
318 simpr 
 |-  ( ( ph /\ x e. I ) -> x e. I )
319 8 4 26 71 316 317 318 mvrval 
 |-  ( ( ph /\ x e. I ) -> ( V ` x ) = ( y e. D |-> if ( y = ( z e. I |-> if ( z = x , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
320 319 fveq2d 
 |-  ( ( 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 ) ) ) ) )
321 12 adantr 
 |-  ( ( ph /\ x e. I ) -> S e. CRing )
322 13 adantr 
 |-  ( ( ph /\ x e. I ) -> F e. ( R RingHom S ) )
323 14 adantr 
 |-  ( ( ph /\ x e. I ) -> G : I --> C )
324 4 psrbagsn 
 |-  ( I e. W -> ( z e. I |-> if ( z = x , 1 , 0 ) ) e. D )
325 10 324 syl 
 |-  ( ph -> ( z e. I |-> if ( z = x , 1 , 0 ) ) e. D )
326 325 adantr 
 |-  ( ( ph /\ x e. I ) -> ( z e. I |-> if ( z = x , 1 , 0 ) ) e. D )
327 73 adantr 
 |-  ( ( ph /\ x e. I ) -> ( 1r ` R ) e. ( Base ` R ) )
328 1 2 3 27 4 5 6 7 8 9 316 317 321 322 323 26 326 327 evlslem3 
 |-  ( ( 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 gsum ( ( z e. I |-> if ( z = x , 1 , 0 ) ) oF .^ G ) ) ) )
329 87 adantr 
 |-  ( ( ph /\ x e. I ) -> ( F ` ( 1r ` R ) ) = ( 1r ` S ) )
330 1nn0 
 |-  1 e. NN0
331 0nn0 
 |-  0 e. NN0
332 330 331 ifcli 
 |-  if ( z = x , 1 , 0 ) e. NN0
333 332 a1i 
 |-  ( ( ph /\ z e. I ) -> if ( z = x , 1 , 0 ) e. NN0 )
334 14 ffvelrnda 
 |-  ( ( ph /\ z e. I ) -> ( G ` z ) e. C )
335 eqidd 
 |-  ( ph -> ( z e. I |-> if ( z = x , 1 , 0 ) ) = ( z e. I |-> if ( z = x , 1 , 0 ) ) )
336 14 feqmptd 
 |-  ( ph -> G = ( z e. I |-> ( G ` z ) ) )
337 10 333 334 335 336 offval2 
 |-  ( ph -> ( ( z e. I |-> if ( z = x , 1 , 0 ) ) oF .^ G ) = ( z e. I |-> ( if ( z = x , 1 , 0 ) .^ ( G ` z ) ) ) )
338 oveq1 
 |-  ( 1 = if ( z = x , 1 , 0 ) -> ( 1 .^ ( G ` z ) ) = ( if ( z = x , 1 , 0 ) .^ ( G ` z ) ) )
339 338 eqeq1d 
 |-  ( 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 ) ) ) )
340 oveq1 
 |-  ( 0 = if ( z = x , 1 , 0 ) -> ( 0 .^ ( G ` z ) ) = ( if ( z = x , 1 , 0 ) .^ ( G ` z ) ) )
341 340 eqeq1d 
 |-  ( 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 ) ) ) )
342 334 adantr 
 |-  ( ( ( ph /\ z e. I ) /\ z = x ) -> ( G ` z ) e. C )
343 48 6 mulg1 
 |-  ( ( G ` z ) e. C -> ( 1 .^ ( G ` z ) ) = ( G ` z ) )
344 342 343 syl 
 |-  ( ( ( ph /\ z e. I ) /\ z = x ) -> ( 1 .^ ( G ` z ) ) = ( G ` z ) )
345 iftrue 
 |-  ( z = x -> if ( z = x , ( G ` z ) , ( 1r ` S ) ) = ( G ` z ) )
346 345 adantl 
 |-  ( ( ( ph /\ z e. I ) /\ z = x ) -> if ( z = x , ( G ` z ) , ( 1r ` S ) ) = ( G ` z ) )
347 344 346 eqtr4d 
 |-  ( ( ( ph /\ z e. I ) /\ z = x ) -> ( 1 .^ ( G ` z ) ) = if ( z = x , ( G ` z ) , ( 1r ` S ) ) )
348 48 49 6 mulg0 
 |-  ( ( G ` z ) e. C -> ( 0 .^ ( G ` z ) ) = ( 1r ` S ) )
349 334 348 syl 
 |-  ( ( ph /\ z e. I ) -> ( 0 .^ ( G ` z ) ) = ( 1r ` S ) )
350 349 adantr 
 |-  ( ( ( ph /\ z e. I ) /\ -. z = x ) -> ( 0 .^ ( G ` z ) ) = ( 1r ` S ) )
351 iffalse 
 |-  ( -. z = x -> if ( z = x , ( G ` z ) , ( 1r ` S ) ) = ( 1r ` S ) )
352 351 adantl 
 |-  ( ( ( ph /\ z e. I ) /\ -. z = x ) -> if ( z = x , ( G ` z ) , ( 1r ` S ) ) = ( 1r ` S ) )
353 350 352 eqtr4d 
 |-  ( ( ( ph /\ z e. I ) /\ -. z = x ) -> ( 0 .^ ( G ` z ) ) = if ( z = x , ( G ` z ) , ( 1r ` S ) ) )
354 339 341 347 353 ifbothda 
 |-  ( ( ph /\ z e. I ) -> ( if ( z = x , 1 , 0 ) .^ ( G ` z ) ) = if ( z = x , ( G ` z ) , ( 1r ` S ) ) )
355 354 mpteq2dva 
 |-  ( ph -> ( z e. I |-> ( if ( z = x , 1 , 0 ) .^ ( G ` z ) ) ) = ( z e. I |-> if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) )
356 337 355 eqtrd 
 |-  ( ph -> ( ( z e. I |-> if ( z = x , 1 , 0 ) ) oF .^ G ) = ( z e. I |-> if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) )
357 356 adantr 
 |-  ( ( ph /\ x e. I ) -> ( ( z e. I |-> if ( z = x , 1 , 0 ) ) oF .^ G ) = ( z e. I |-> if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) )
358 357 oveq2d 
 |-  ( ( ph /\ x e. I ) -> ( T gsum ( ( z e. I |-> if ( z = x , 1 , 0 ) ) oF .^ G ) ) = ( T gsum ( z e. I |-> if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) ) )
359 57 adantr 
 |-  ( ( ph /\ x e. I ) -> T e. Mnd )
360 334 adantlr 
 |-  ( ( ( ph /\ x e. I ) /\ z e. I ) -> ( G ` z ) e. C )
361 3 17 ringidcl 
 |-  ( S e. Ring -> ( 1r ` S ) e. C )
362 22 361 syl 
 |-  ( ph -> ( 1r ` S ) e. C )
363 362 ad2antrr 
 |-  ( ( ( ph /\ x e. I ) /\ z e. I ) -> ( 1r ` S ) e. C )
364 360 363 ifcld 
 |-  ( ( ( ph /\ x e. I ) /\ z e. I ) -> if ( z = x , ( G ` z ) , ( 1r ` S ) ) e. C )
365 364 fmpttd 
 |-  ( ( ph /\ x e. I ) -> ( z e. I |-> if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) : I --> C )
366 eldifsnneq 
 |-  ( z e. ( I \ { x } ) -> -. z = x )
367 366 351 syl 
 |-  ( z e. ( I \ { x } ) -> if ( z = x , ( G ` z ) , ( 1r ` S ) ) = ( 1r ` S ) )
368 367 adantl 
 |-  ( ( ( ph /\ x e. I ) /\ z e. ( I \ { x } ) ) -> if ( z = x , ( G ` z ) , ( 1r ` S ) ) = ( 1r ` S ) )
369 368 316 suppss2 
 |-  ( ( ph /\ x e. I ) -> ( ( z e. I |-> if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) supp ( 1r ` S ) ) C_ { x } )
370 48 49 359 316 318 365 369 gsumpt 
 |-  ( ( ph /\ x e. I ) -> ( T gsum ( z e. I |-> if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) ) = ( ( z e. I |-> if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) ` x ) )
371 fveq2 
 |-  ( z = x -> ( G ` z ) = ( G ` x ) )
372 345 371 eqtrd 
 |-  ( z = x -> if ( z = x , ( G ` z ) , ( 1r ` S ) ) = ( G ` x ) )
373 eqid 
 |-  ( z e. I |-> if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) = ( z e. I |-> if ( z = x , ( G ` z ) , ( 1r ` S ) ) )
374 fvex 
 |-  ( G ` x ) e. _V
375 372 373 374 fvmpt 
 |-  ( x e. I -> ( ( z e. I |-> if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) ` x ) = ( G ` x ) )
376 375 adantl 
 |-  ( ( ph /\ x e. I ) -> ( ( z e. I |-> if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) ` x ) = ( G ` x ) )
377 358 370 376 3eqtrd 
 |-  ( ( ph /\ x e. I ) -> ( T gsum ( ( z e. I |-> if ( z = x , 1 , 0 ) ) oF .^ G ) ) = ( G ` x ) )
378 329 377 oveq12d 
 |-  ( ( ph /\ x e. I ) -> ( ( F ` ( 1r ` R ) ) .x. ( T gsum ( ( z e. I |-> if ( z = x , 1 , 0 ) ) oF .^ G ) ) ) = ( ( 1r ` S ) .x. ( G ` x ) ) )
379 3 7 17 ringlidm 
 |-  ( ( S e. Ring /\ ( G ` x ) e. C ) -> ( ( 1r ` S ) .x. ( G ` x ) ) = ( G ` x ) )
380 22 47 379 syl2an2r 
 |-  ( ( ph /\ x e. I ) -> ( ( 1r ` S ) .x. ( G ` x ) ) = ( G ` x ) )
381 378 380 eqtrd 
 |-  ( ( ph /\ x e. I ) -> ( ( F ` ( 1r ` R ) ) .x. ( T gsum ( ( z e. I |-> if ( z = x , 1 , 0 ) ) oF .^ G ) ) ) = ( G ` x ) )
382 320 328 381 3eqtrd 
 |-  ( ( ph /\ x e. I ) -> ( E ` ( V ` x ) ) = ( G ` x ) )
383 315 382 eqtrd 
 |-  ( ( ph /\ x e. I ) -> ( ( E o. V ) ` x ) = ( G ` x ) )
384 313 247 383 eqfnfvd 
 |-  ( ph -> ( E o. V ) = G )
385 294 308 384 3jca 
 |-  ( ph -> ( E e. ( P RingHom S ) /\ ( E o. A ) = F /\ ( E o. V ) = G ) )