Metamath Proof Explorer

Theorem evlslem3

Description: Lemma for evlseu . Polynomial evaluation of a scaled monomial. (Contributed by Stefan O'Rear, 8-Mar-2015) (Revised by AV, 11-Apr-2024)

Ref Expression
Hypotheses evlslem3.p 
|- P = ( I mPoly R )
evlslem3.b 
|- B = ( Base ` P )
evlslem3.c 
|- C = ( Base ` S )
evlslem3.k 
|- K = ( Base ` R )
evlslem3.d 
|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
evlslem3.t 
|- T = ( mulGrp ` S )
evlslem3.x 
|- .^ = ( .g ` T )
evlslem3.m 
|- .x. = ( .r ` S )
evlslem3.v 
|- V = ( I mVar R )
evlslem3.e 
|- E = ( p e. B |-> ( S gsum ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) )
evlslem3.i 
|- ( ph -> I e. W )
evlslem3.r 
|- ( ph -> R e. CRing )
evlslem3.s 
|- ( ph -> S e. CRing )
evlslem3.f 
|- ( ph -> F e. ( R RingHom S ) )
evlslem3.g 
|- ( ph -> G : I --> C )
evlslem3.z 
|- .0. = ( 0g ` R )
evlslem3.a 
|- ( ph -> A e. D )
evlslem3.q 
|- ( ph -> H e. K )
Assertion evlslem3 
|- ( ph -> ( E ` ( x e. D |-> if ( x = A , H , .0. ) ) ) = ( ( F ` H ) .x. ( T gsum ( A oF .^ G ) ) ) )

Proof

Step Hyp Ref Expression
1 evlslem3.p 
 |-  P = ( I mPoly R )
2 evlslem3.b 
 |-  B = ( Base ` P )
3 evlslem3.c 
 |-  C = ( Base ` S )
4 evlslem3.k 
 |-  K = ( Base ` R )
5 evlslem3.d 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
6 evlslem3.t 
 |-  T = ( mulGrp ` S )
7 evlslem3.x 
 |-  .^ = ( .g ` T )
8 evlslem3.m 
 |-  .x. = ( .r ` S )
9 evlslem3.v 
 |-  V = ( I mVar R )
10 evlslem3.e 
 |-  E = ( p e. B |-> ( S gsum ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) )
11 evlslem3.i 
 |-  ( ph -> I e. W )
12 evlslem3.r 
 |-  ( ph -> R e. CRing )
13 evlslem3.s 
 |-  ( ph -> S e. CRing )
14 evlslem3.f 
 |-  ( ph -> F e. ( R RingHom S ) )
15 evlslem3.g 
 |-  ( ph -> G : I --> C )
16 evlslem3.z 
 |-  .0. = ( 0g ` R )
17 evlslem3.a 
 |-  ( ph -> A e. D )
18 evlslem3.q 
 |-  ( ph -> H e. K )
19 crngring 
 |-  ( R e. CRing -> R e. Ring )
20 12 19 syl 
 |-  ( ph -> R e. Ring )
21 1 5 16 4 11 20 2 18 17 mplmon2cl 
 |-  ( ph -> ( x e. D |-> if ( x = A , H , .0. ) ) e. B )
22 fveq1 
 |-  ( p = ( x e. D |-> if ( x = A , H , .0. ) ) -> ( p ` b ) = ( ( x e. D |-> if ( x = A , H , .0. ) ) ` b ) )
23 22 fveq2d 
 |-  ( p = ( x e. D |-> if ( x = A , H , .0. ) ) -> ( F ` ( p ` b ) ) = ( F ` ( ( x e. D |-> if ( x = A , H , .0. ) ) ` b ) ) )
24 23 oveq1d 
 |-  ( p = ( x e. D |-> if ( x = A , H , .0. ) ) -> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) = ( ( F ` ( ( x e. D |-> if ( x = A , H , .0. ) ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) )
25 24 mpteq2dv 
 |-  ( p = ( x e. D |-> if ( x = A , H , .0. ) ) -> ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) = ( b e. D |-> ( ( F ` ( ( x e. D |-> if ( x = A , H , .0. ) ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) )
26 25 oveq2d 
 |-  ( p = ( x e. D |-> if ( x = A , H , .0. ) ) -> ( S gsum ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) = ( S gsum ( b e. D |-> ( ( F ` ( ( x e. D |-> if ( x = A , H , .0. ) ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) )
27 ovex 
 |-  ( S gsum ( b e. D |-> ( ( F ` ( ( x e. D |-> if ( x = A , H , .0. ) ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) e. _V
28 26 10 27 fvmpt 
 |-  ( ( x e. D |-> if ( x = A , H , .0. ) ) e. B -> ( E ` ( x e. D |-> if ( x = A , H , .0. ) ) ) = ( S gsum ( b e. D |-> ( ( F ` ( ( x e. D |-> if ( x = A , H , .0. ) ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) )
29 21 28 syl 
 |-  ( ph -> ( E ` ( x e. D |-> if ( x = A , H , .0. ) ) ) = ( S gsum ( b e. D |-> ( ( F ` ( ( x e. D |-> if ( x = A , H , .0. ) ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) )
30 eqid 
 |-  ( x e. D |-> if ( x = A , H , .0. ) ) = ( x e. D |-> if ( x = A , H , .0. ) )
31 eqeq1 
 |-  ( x = b -> ( x = A <-> b = A ) )
32 31 ifbid 
 |-  ( x = b -> if ( x = A , H , .0. ) = if ( b = A , H , .0. ) )
33 simpr 
 |-  ( ( ph /\ b e. D ) -> b e. D )
34 16 fvexi 
 |-  .0. e. _V
35 34 a1i 
 |-  ( ph -> .0. e. _V )
36 ifexg 
 |-  ( ( H e. K /\ .0. e. _V ) -> if ( b = A , H , .0. ) e. _V )
37 18 35 36 syl2anc 
 |-  ( ph -> if ( b = A , H , .0. ) e. _V )
38 37 adantr 
 |-  ( ( ph /\ b e. D ) -> if ( b = A , H , .0. ) e. _V )
39 30 32 33 38 fvmptd3 
 |-  ( ( ph /\ b e. D ) -> ( ( x e. D |-> if ( x = A , H , .0. ) ) ` b ) = if ( b = A , H , .0. ) )
40 39 fveq2d 
 |-  ( ( ph /\ b e. D ) -> ( F ` ( ( x e. D |-> if ( x = A , H , .0. ) ) ` b ) ) = ( F ` if ( b = A , H , .0. ) ) )
41 40 oveq1d 
 |-  ( ( ph /\ b e. D ) -> ( ( F ` ( ( x e. D |-> if ( x = A , H , .0. ) ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) = ( ( F ` if ( b = A , H , .0. ) ) .x. ( T gsum ( b oF .^ G ) ) ) )
42 41 mpteq2dva 
 |-  ( ph -> ( b e. D |-> ( ( F ` ( ( x e. D |-> if ( x = A , H , .0. ) ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) = ( b e. D |-> ( ( F ` if ( b = A , H , .0. ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) )
43 42 oveq2d 
 |-  ( ph -> ( S gsum ( b e. D |-> ( ( F ` ( ( x e. D |-> if ( x = A , H , .0. ) ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) = ( S gsum ( b e. D |-> ( ( F ` if ( b = A , H , .0. ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) )
44 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
45 crngring 
 |-  ( S e. CRing -> S e. Ring )
46 13 45 syl 
 |-  ( ph -> S e. Ring )
47 ringmnd 
 |-  ( S e. Ring -> S e. Mnd )
48 46 47 syl 
 |-  ( ph -> S e. Mnd )
49 ovex 
 |-  ( NN0 ^m I ) e. _V
50 5 49 rabex2 
 |-  D e. _V
51 50 a1i 
 |-  ( ph -> D e. _V )
52 46 adantr 
 |-  ( ( ph /\ b e. D ) -> S e. Ring )
53 4 3 rhmf 
 |-  ( F e. ( R RingHom S ) -> F : K --> C )
54 14 53 syl 
 |-  ( ph -> F : K --> C )
55 4 16 ring0cl 
 |-  ( R e. Ring -> .0. e. K )
56 20 55 syl 
 |-  ( ph -> .0. e. K )
57 18 56 ifcld 
 |-  ( ph -> if ( b = A , H , .0. ) e. K )
58 54 57 ffvelrnd 
 |-  ( ph -> ( F ` if ( b = A , H , .0. ) ) e. C )
59 58 adantr 
 |-  ( ( ph /\ b e. D ) -> ( F ` if ( b = A , H , .0. ) ) e. C )
60 6 3 mgpbas 
 |-  C = ( Base ` T )
61 eqid 
 |-  ( 0g ` T ) = ( 0g ` T )
62 6 crngmgp 
 |-  ( S e. CRing -> T e. CMnd )
63 13 62 syl 
 |-  ( ph -> T e. CMnd )
64 63 adantr 
 |-  ( ( ph /\ b e. D ) -> T e. CMnd )
65 11 adantr 
 |-  ( ( ph /\ b e. D ) -> I e. W )
66 cmnmnd 
 |-  ( T e. CMnd -> T e. Mnd )
67 63 66 syl 
 |-  ( ph -> T e. Mnd )
68 67 ad2antrr 
 |-  ( ( ( ph /\ b e. D ) /\ ( y e. NN0 /\ z e. C ) ) -> T e. Mnd )
69 simprl 
 |-  ( ( ( ph /\ b e. D ) /\ ( y e. NN0 /\ z e. C ) ) -> y e. NN0 )
70 simprr 
 |-  ( ( ( ph /\ b e. D ) /\ ( y e. NN0 /\ z e. C ) ) -> z e. C )
71 60 7 mulgnn0cl 
 |-  ( ( T e. Mnd /\ y e. NN0 /\ z e. C ) -> ( y .^ z ) e. C )
72 68 69 70 71 syl3anc 
 |-  ( ( ( ph /\ b e. D ) /\ ( y e. NN0 /\ z e. C ) ) -> ( y .^ z ) e. C )
73 5 psrbagf 
 |-  ( b e. D -> b : I --> NN0 )
74 73 adantl 
 |-  ( ( ph /\ b e. D ) -> b : I --> NN0 )
75 15 adantr 
 |-  ( ( ph /\ b e. D ) -> G : I --> C )
76 inidm 
 |-  ( I i^i I ) = I
77 72 74 75 65 65 76 off 
 |-  ( ( ph /\ b e. D ) -> ( b oF .^ G ) : I --> C )
78 ovex 
 |-  ( b oF .^ G ) e. _V
79 78 a1i 
 |-  ( ( ph /\ b e. D ) -> ( b oF .^ G ) e. _V )
80 77 ffund 
 |-  ( ( ph /\ b e. D ) -> Fun ( b oF .^ G ) )
81 fvexd 
 |-  ( ( ph /\ b e. D ) -> ( 0g ` T ) e. _V )
82 5 psrbag 
 |-  ( I e. W -> ( b e. D <-> ( b : I --> NN0 /\ ( `' b " NN ) e. Fin ) ) )
83 11 82 syl 
 |-  ( ph -> ( b e. D <-> ( b : I --> NN0 /\ ( `' b " NN ) e. Fin ) ) )
84 83 simplbda 
 |-  ( ( ph /\ b e. D ) -> ( `' b " NN ) e. Fin )
85 74 ffnd 
 |-  ( ( ph /\ b e. D ) -> b Fn I )
86 85 adantr 
 |-  ( ( ( ph /\ b e. D ) /\ y e. ( I \ ( `' b " NN ) ) ) -> b Fn I )
87 15 ffnd 
 |-  ( ph -> G Fn I )
88 87 ad2antrr 
 |-  ( ( ( ph /\ b e. D ) /\ y e. ( I \ ( `' b " NN ) ) ) -> G Fn I )
89 11 ad2antrr 
 |-  ( ( ( ph /\ b e. D ) /\ y e. ( I \ ( `' b " NN ) ) ) -> I e. W )
90 eldifi 
 |-  ( y e. ( I \ ( `' b " NN ) ) -> y e. I )
91 90 adantl 
 |-  ( ( ( ph /\ b e. D ) /\ y e. ( I \ ( `' b " NN ) ) ) -> y e. I )
92 fnfvof 
 |-  ( ( ( b Fn I /\ G Fn I ) /\ ( I e. W /\ y e. I ) ) -> ( ( b oF .^ G ) ` y ) = ( ( b ` y ) .^ ( G ` y ) ) )
93 86 88 89 91 92 syl22anc 
 |-  ( ( ( ph /\ b e. D ) /\ y e. ( I \ ( `' b " NN ) ) ) -> ( ( b oF .^ G ) ` y ) = ( ( b ` y ) .^ ( G ` y ) ) )
94 ffvelrn 
 |-  ( ( b : I --> NN0 /\ y e. I ) -> ( b ` y ) e. NN0 )
95 74 90 94 syl2an 
 |-  ( ( ( ph /\ b e. D ) /\ y e. ( I \ ( `' b " NN ) ) ) -> ( b ` y ) e. NN0 )
96 elnn0 
 |-  ( ( b ` y ) e. NN0 <-> ( ( b ` y ) e. NN \/ ( b ` y ) = 0 ) )
97 95 96 sylib 
 |-  ( ( ( ph /\ b e. D ) /\ y e. ( I \ ( `' b " NN ) ) ) -> ( ( b ` y ) e. NN \/ ( b ` y ) = 0 ) )
98 eldifn 
 |-  ( y e. ( I \ ( `' b " NN ) ) -> -. y e. ( `' b " NN ) )
99 98 adantl 
 |-  ( ( ( ph /\ b e. D ) /\ y e. ( I \ ( `' b " NN ) ) ) -> -. y e. ( `' b " NN ) )
100 85 ad2antrr 
 |-  ( ( ( ( ph /\ b e. D ) /\ y e. ( I \ ( `' b " NN ) ) ) /\ ( b ` y ) e. NN ) -> b Fn I )
101 90 ad2antlr 
 |-  ( ( ( ( ph /\ b e. D ) /\ y e. ( I \ ( `' b " NN ) ) ) /\ ( b ` y ) e. NN ) -> y e. I )
102 simpr 
 |-  ( ( ( ( ph /\ b e. D ) /\ y e. ( I \ ( `' b " NN ) ) ) /\ ( b ` y ) e. NN ) -> ( b ` y ) e. NN )
103 100 101 102 elpreimad 
 |-  ( ( ( ( ph /\ b e. D ) /\ y e. ( I \ ( `' b " NN ) ) ) /\ ( b ` y ) e. NN ) -> y e. ( `' b " NN ) )
104 99 103 mtand 
 |-  ( ( ( ph /\ b e. D ) /\ y e. ( I \ ( `' b " NN ) ) ) -> -. ( b ` y ) e. NN )
105 97 104 orcnd 
 |-  ( ( ( ph /\ b e. D ) /\ y e. ( I \ ( `' b " NN ) ) ) -> ( b ` y ) = 0 )
106 105 oveq1d 
 |-  ( ( ( ph /\ b e. D ) /\ y e. ( I \ ( `' b " NN ) ) ) -> ( ( b ` y ) .^ ( G ` y ) ) = ( 0 .^ ( G ` y ) ) )
107 ffvelrn 
 |-  ( ( G : I --> C /\ y e. I ) -> ( G ` y ) e. C )
108 75 90 107 syl2an 
 |-  ( ( ( ph /\ b e. D ) /\ y e. ( I \ ( `' b " NN ) ) ) -> ( G ` y ) e. C )
109 60 61 7 mulg0 
 |-  ( ( G ` y ) e. C -> ( 0 .^ ( G ` y ) ) = ( 0g ` T ) )
110 108 109 syl 
 |-  ( ( ( ph /\ b e. D ) /\ y e. ( I \ ( `' b " NN ) ) ) -> ( 0 .^ ( G ` y ) ) = ( 0g ` T ) )
111 93 106 110 3eqtrd 
 |-  ( ( ( ph /\ b e. D ) /\ y e. ( I \ ( `' b " NN ) ) ) -> ( ( b oF .^ G ) ` y ) = ( 0g ` T ) )
112 77 111 suppss 
 |-  ( ( ph /\ b e. D ) -> ( ( b oF .^ G ) supp ( 0g ` T ) ) C_ ( `' b " NN ) )
113 suppssfifsupp 
 |-  ( ( ( ( b oF .^ G ) e. _V /\ Fun ( b oF .^ G ) /\ ( 0g ` T ) e. _V ) /\ ( ( `' b " NN ) e. Fin /\ ( ( b oF .^ G ) supp ( 0g ` T ) ) C_ ( `' b " NN ) ) ) -> ( b oF .^ G ) finSupp ( 0g ` T ) )
114 79 80 81 84 112 113 syl32anc 
 |-  ( ( ph /\ b e. D ) -> ( b oF .^ G ) finSupp ( 0g ` T ) )
115 60 61 64 65 77 114 gsumcl 
 |-  ( ( ph /\ b e. D ) -> ( T gsum ( b oF .^ G ) ) e. C )
116 3 8 ringcl 
 |-  ( ( S e. Ring /\ ( F ` if ( b = A , H , .0. ) ) e. C /\ ( T gsum ( b oF .^ G ) ) e. C ) -> ( ( F ` if ( b = A , H , .0. ) ) .x. ( T gsum ( b oF .^ G ) ) ) e. C )
117 52 59 115 116 syl3anc 
 |-  ( ( ph /\ b e. D ) -> ( ( F ` if ( b = A , H , .0. ) ) .x. ( T gsum ( b oF .^ G ) ) ) e. C )
118 117 fmpttd 
 |-  ( ph -> ( b e. D |-> ( ( F ` if ( b = A , H , .0. ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) : D --> C )
119 eldifsnneq 
 |-  ( b e. ( D \ { A } ) -> -. b = A )
120 119 iffalsed 
 |-  ( b e. ( D \ { A } ) -> if ( b = A , H , .0. ) = .0. )
121 120 adantl 
 |-  ( ( ph /\ b e. ( D \ { A } ) ) -> if ( b = A , H , .0. ) = .0. )
122 121 fveq2d 
 |-  ( ( ph /\ b e. ( D \ { A } ) ) -> ( F ` if ( b = A , H , .0. ) ) = ( F ` .0. ) )
123 rhmghm 
 |-  ( F e. ( R RingHom S ) -> F e. ( R GrpHom S ) )
124 14 123 syl 
 |-  ( ph -> F e. ( R GrpHom S ) )
125 16 44 ghmid 
 |-  ( F e. ( R GrpHom S ) -> ( F ` .0. ) = ( 0g ` S ) )
126 124 125 syl 
 |-  ( ph -> ( F ` .0. ) = ( 0g ` S ) )
127 126 adantr 
 |-  ( ( ph /\ b e. ( D \ { A } ) ) -> ( F ` .0. ) = ( 0g ` S ) )
128 122 127 eqtrd 
 |-  ( ( ph /\ b e. ( D \ { A } ) ) -> ( F ` if ( b = A , H , .0. ) ) = ( 0g ` S ) )
129 128 oveq1d 
 |-  ( ( ph /\ b e. ( D \ { A } ) ) -> ( ( F ` if ( b = A , H , .0. ) ) .x. ( T gsum ( b oF .^ G ) ) ) = ( ( 0g ` S ) .x. ( T gsum ( b oF .^ G ) ) ) )
130 46 adantr 
 |-  ( ( ph /\ b e. ( D \ { A } ) ) -> S e. Ring )
131 eldifi 
 |-  ( b e. ( D \ { A } ) -> b e. D )
132 131 115 sylan2 
 |-  ( ( ph /\ b e. ( D \ { A } ) ) -> ( T gsum ( b oF .^ G ) ) e. C )
133 3 8 44 ringlz 
 |-  ( ( S e. Ring /\ ( T gsum ( b oF .^ G ) ) e. C ) -> ( ( 0g ` S ) .x. ( T gsum ( b oF .^ G ) ) ) = ( 0g ` S ) )
134 130 132 133 syl2anc 
 |-  ( ( ph /\ b e. ( D \ { A } ) ) -> ( ( 0g ` S ) .x. ( T gsum ( b oF .^ G ) ) ) = ( 0g ` S ) )
135 129 134 eqtrd 
 |-  ( ( ph /\ b e. ( D \ { A } ) ) -> ( ( F ` if ( b = A , H , .0. ) ) .x. ( T gsum ( b oF .^ G ) ) ) = ( 0g ` S ) )
136 135 51 suppss2 
 |-  ( ph -> ( ( b e. D |-> ( ( F ` if ( b = A , H , .0. ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) supp ( 0g ` S ) ) C_ { A } )
137 3 44 48 51 17 118 136 gsumpt 
 |-  ( ph -> ( S gsum ( b e. D |-> ( ( F ` if ( b = A , H , .0. ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) = ( ( b e. D |-> ( ( F ` if ( b = A , H , .0. ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ` A ) )
138 43 137 eqtrd 
 |-  ( ph -> ( S gsum ( b e. D |-> ( ( F ` ( ( x e. D |-> if ( x = A , H , .0. ) ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) = ( ( b e. D |-> ( ( F ` if ( b = A , H , .0. ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ` A ) )
139 iftrue 
 |-  ( b = A -> if ( b = A , H , .0. ) = H )
140 139 fveq2d 
 |-  ( b = A -> ( F ` if ( b = A , H , .0. ) ) = ( F ` H ) )
141 oveq1 
 |-  ( b = A -> ( b oF .^ G ) = ( A oF .^ G ) )
142 141 oveq2d 
 |-  ( b = A -> ( T gsum ( b oF .^ G ) ) = ( T gsum ( A oF .^ G ) ) )
143 140 142 oveq12d 
 |-  ( b = A -> ( ( F ` if ( b = A , H , .0. ) ) .x. ( T gsum ( b oF .^ G ) ) ) = ( ( F ` H ) .x. ( T gsum ( A oF .^ G ) ) ) )
144 eqid 
 |-  ( b e. D |-> ( ( F ` if ( b = A , H , .0. ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) = ( b e. D |-> ( ( F ` if ( b = A , H , .0. ) ) .x. ( T gsum ( b oF .^ G ) ) ) )
145 ovex 
 |-  ( ( F ` H ) .x. ( T gsum ( A oF .^ G ) ) ) e. _V
146 143 144 145 fvmpt 
 |-  ( A e. D -> ( ( b e. D |-> ( ( F ` if ( b = A , H , .0. ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ` A ) = ( ( F ` H ) .x. ( T gsum ( A oF .^ G ) ) ) )
147 17 146 syl 
 |-  ( ph -> ( ( b e. D |-> ( ( F ` if ( b = A , H , .0. ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ` A ) = ( ( F ` H ) .x. ( T gsum ( A oF .^ G ) ) ) )
148 29 138 147 3eqtrd 
 |-  ( ph -> ( E ` ( x e. D |-> if ( x = A , H , .0. ) ) ) = ( ( F ` H ) .x. ( T gsum ( A oF .^ G ) ) ) )