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 ) )