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