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