This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem evl1deg2

Description: Evaluation of a univariate polynomial of degree 2. (Contributed by Thierry Arnoux, 22-Jun-2025)

Ref Expression
Hypotheses evl1deg1.1 
|- P = ( Poly1 ` R )
evl1deg1.2 
|- O = ( eval1 ` R )
evl1deg1.3 
|- K = ( Base ` R )
evl1deg1.4 
|- U = ( Base ` P )
evl1deg1.5 
|- .x. = ( .r ` R )
evl1deg1.6 
|- .+ = ( +g ` R )
evl1deg2.p 
|- .^ = ( .g ` ( mulGrp ` R ) )
evl1deg2.f 
|- F = ( coe1 ` M )
evl1deg2.e 
|- E = ( deg1 ` R )
evl1deg2.a 
|- A = ( F ` 2 )
evl1deg2.b 
|- B = ( F ` 1 )
evl1deg2.c 
|- C = ( F ` 0 )
evl1deg2.r 
|- ( ph -> R e. CRing )
evl1deg2.m 
|- ( ph -> M e. U )
evl1deg2.1 
|- ( ph -> ( E ` M ) = 2 )
evl1deg2.x 
|- ( ph -> X e. K )
Assertion evl1deg2 
|- ( ph -> ( ( O ` M ) ` X ) = ( ( A .x. ( 2 .^ X ) ) .+ ( ( B .x. X ) .+ C ) ) )

Proof

Step Hyp Ref Expression
1 evl1deg1.1 
 |-  P = ( Poly1 ` R )
2 evl1deg1.2 
 |-  O = ( eval1 ` R )
3 evl1deg1.3 
 |-  K = ( Base ` R )
4 evl1deg1.4 
 |-  U = ( Base ` P )
5 evl1deg1.5 
 |-  .x. = ( .r ` R )
6 evl1deg1.6 
 |-  .+ = ( +g ` R )
7 evl1deg2.p 
 |-  .^ = ( .g ` ( mulGrp ` R ) )
8 evl1deg2.f 
 |-  F = ( coe1 ` M )
9 evl1deg2.e 
 |-  E = ( deg1 ` R )
10 evl1deg2.a 
 |-  A = ( F ` 2 )
11 evl1deg2.b 
 |-  B = ( F ` 1 )
12 evl1deg2.c 
 |-  C = ( F ` 0 )
13 evl1deg2.r 
 |-  ( ph -> R e. CRing )
14 evl1deg2.m 
 |-  ( ph -> M e. U )
15 evl1deg2.1 
 |-  ( ph -> ( E ` M ) = 2 )
16 evl1deg2.x 
 |-  ( ph -> X e. K )
17 oveq2 
 |-  ( x = X -> ( k .^ x ) = ( k .^ X ) )
18 17 oveq2d 
 |-  ( x = X -> ( ( F ` k ) .x. ( k .^ x ) ) = ( ( F ` k ) .x. ( k .^ X ) ) )
19 18 mpteq2dv 
 |-  ( x = X -> ( k e. NN0 |-> ( ( F ` k ) .x. ( k .^ x ) ) ) = ( k e. NN0 |-> ( ( F ` k ) .x. ( k .^ X ) ) ) )
20 19 oveq2d 
 |-  ( x = X -> ( R gsum ( k e. NN0 |-> ( ( F ` k ) .x. ( k .^ x ) ) ) ) = ( R gsum ( k e. NN0 |-> ( ( F ` k ) .x. ( k .^ X ) ) ) ) )
21 2 1 3 4 13 14 5 7 8 evl1fpws 
 |-  ( ph -> ( O ` M ) = ( x e. K |-> ( R gsum ( k e. NN0 |-> ( ( F ` k ) .x. ( k .^ x ) ) ) ) ) )
22 ovexd 
 |-  ( ph -> ( R gsum ( k e. NN0 |-> ( ( F ` k ) .x. ( k .^ X ) ) ) ) e. _V )
23 20 21 16 22 fvmptd4 
 |-  ( ph -> ( ( O ` M ) ` X ) = ( R gsum ( k e. NN0 |-> ( ( F ` k ) .x. ( k .^ X ) ) ) ) )
24 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
25 13 crngringd 
 |-  ( ph -> R e. Ring )
26 25 ringcmnd 
 |-  ( ph -> R e. CMnd )
27 nn0ex 
 |-  NN0 e. _V
28 27 a1i 
 |-  ( ph -> NN0 e. _V )
29 25 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> R e. Ring )
30 8 4 1 3 coe1fvalcl 
 |-  ( ( M e. U /\ k e. NN0 ) -> ( F ` k ) e. K )
31 14 30 sylan 
 |-  ( ( ph /\ k e. NN0 ) -> ( F ` k ) e. K )
32 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
33 32 3 mgpbas 
 |-  K = ( Base ` ( mulGrp ` R ) )
34 32 ringmgp 
 |-  ( R e. Ring -> ( mulGrp ` R ) e. Mnd )
35 25 34 syl 
 |-  ( ph -> ( mulGrp ` R ) e. Mnd )
36 35 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> ( mulGrp ` R ) e. Mnd )
37 simpr 
 |-  ( ( ph /\ k e. NN0 ) -> k e. NN0 )
38 16 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> X e. K )
39 33 7 36 37 38 mulgnn0cld 
 |-  ( ( ph /\ k e. NN0 ) -> ( k .^ X ) e. K )
40 3 5 29 31 39 ringcld 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( F ` k ) .x. ( k .^ X ) ) e. K )
41 fvexd 
 |-  ( ph -> ( 0g ` R ) e. _V )
42 fveq2 
 |-  ( k = j -> ( F ` k ) = ( F ` j ) )
43 oveq1 
 |-  ( k = j -> ( k .^ X ) = ( j .^ X ) )
44 42 43 oveq12d 
 |-  ( k = j -> ( ( F ` k ) .x. ( k .^ X ) ) = ( ( F ` j ) .x. ( j .^ X ) ) )
45 breq1 
 |-  ( i = ( E ` M ) -> ( i < j <-> ( E ` M ) < j ) )
46 45 imbi1d 
 |-  ( i = ( E ` M ) -> ( ( i < j -> ( ( F ` j ) .x. ( j .^ X ) ) = ( 0g ` R ) ) <-> ( ( E ` M ) < j -> ( ( F ` j ) .x. ( j .^ X ) ) = ( 0g ` R ) ) ) )
47 46 ralbidv 
 |-  ( i = ( E ` M ) -> ( A. j e. NN0 ( i < j -> ( ( F ` j ) .x. ( j .^ X ) ) = ( 0g ` R ) ) <-> A. j e. NN0 ( ( E ` M ) < j -> ( ( F ` j ) .x. ( j .^ X ) ) = ( 0g ` R ) ) ) )
48 2nn0 
 |-  2 e. NN0
49 48 a1i 
 |-  ( ph -> 2 e. NN0 )
50 15 49 eqeltrd 
 |-  ( ph -> ( E ` M ) e. NN0 )
51 14 ad2antrr 
 |-  ( ( ( ph /\ j e. NN0 ) /\ ( E ` M ) < j ) -> M e. U )
52 simplr 
 |-  ( ( ( ph /\ j e. NN0 ) /\ ( E ` M ) < j ) -> j e. NN0 )
53 simpr 
 |-  ( ( ( ph /\ j e. NN0 ) /\ ( E ` M ) < j ) -> ( E ` M ) < j )
54 9 1 4 24 8 deg1lt 
 |-  ( ( M e. U /\ j e. NN0 /\ ( E ` M ) < j ) -> ( F ` j ) = ( 0g ` R ) )
55 51 52 53 54 syl3anc 
 |-  ( ( ( ph /\ j e. NN0 ) /\ ( E ` M ) < j ) -> ( F ` j ) = ( 0g ` R ) )
56 55 oveq1d 
 |-  ( ( ( ph /\ j e. NN0 ) /\ ( E ` M ) < j ) -> ( ( F ` j ) .x. ( j .^ X ) ) = ( ( 0g ` R ) .x. ( j .^ X ) ) )
57 25 ad2antrr 
 |-  ( ( ( ph /\ j e. NN0 ) /\ ( E ` M ) < j ) -> R e. Ring )
58 57 34 syl 
 |-  ( ( ( ph /\ j e. NN0 ) /\ ( E ` M ) < j ) -> ( mulGrp ` R ) e. Mnd )
59 16 ad2antrr 
 |-  ( ( ( ph /\ j e. NN0 ) /\ ( E ` M ) < j ) -> X e. K )
60 33 7 58 52 59 mulgnn0cld 
 |-  ( ( ( ph /\ j e. NN0 ) /\ ( E ` M ) < j ) -> ( j .^ X ) e. K )
61 3 5 24 57 60 ringlzd 
 |-  ( ( ( ph /\ j e. NN0 ) /\ ( E ` M ) < j ) -> ( ( 0g ` R ) .x. ( j .^ X ) ) = ( 0g ` R ) )
62 56 61 eqtrd 
 |-  ( ( ( ph /\ j e. NN0 ) /\ ( E ` M ) < j ) -> ( ( F ` j ) .x. ( j .^ X ) ) = ( 0g ` R ) )
63 62 ex 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( E ` M ) < j -> ( ( F ` j ) .x. ( j .^ X ) ) = ( 0g ` R ) ) )
64 63 ralrimiva 
 |-  ( ph -> A. j e. NN0 ( ( E ` M ) < j -> ( ( F ` j ) .x. ( j .^ X ) ) = ( 0g ` R ) ) )
65 47 50 64 rspcedvdw 
 |-  ( ph -> E. i e. NN0 A. j e. NN0 ( i < j -> ( ( F ` j ) .x. ( j .^ X ) ) = ( 0g ` R ) ) )
66 41 40 44 65 mptnn0fsuppd 
 |-  ( ph -> ( k e. NN0 |-> ( ( F ` k ) .x. ( k .^ X ) ) ) finSupp ( 0g ` R ) )
67 fzouzdisj 
 |-  ( ( 0 ..^ 3 ) i^i ( ZZ>= ` 3 ) ) = (/)
68 67 a1i 
 |-  ( ph -> ( ( 0 ..^ 3 ) i^i ( ZZ>= ` 3 ) ) = (/) )
69 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
70 3nn0 
 |-  3 e. NN0
71 70 69 eleqtri 
 |-  3 e. ( ZZ>= ` 0 )
72 fzouzsplit 
 |-  ( 3 e. ( ZZ>= ` 0 ) -> ( ZZ>= ` 0 ) = ( ( 0 ..^ 3 ) u. ( ZZ>= ` 3 ) ) )
73 71 72 ax-mp 
 |-  ( ZZ>= ` 0 ) = ( ( 0 ..^ 3 ) u. ( ZZ>= ` 3 ) )
74 69 73 eqtri 
 |-  NN0 = ( ( 0 ..^ 3 ) u. ( ZZ>= ` 3 ) )
75 74 a1i 
 |-  ( ph -> NN0 = ( ( 0 ..^ 3 ) u. ( ZZ>= ` 3 ) ) )
76 3 24 6 26 28 40 66 68 75 gsumsplit2 
 |-  ( ph -> ( R gsum ( k e. NN0 |-> ( ( F ` k ) .x. ( k .^ X ) ) ) ) = ( ( R gsum ( k e. ( 0 ..^ 3 ) |-> ( ( F ` k ) .x. ( k .^ X ) ) ) ) .+ ( R gsum ( k e. ( ZZ>= ` 3 ) |-> ( ( F ` k ) .x. ( k .^ X ) ) ) ) ) )
77 fzo0to3tp 
 |-  ( 0 ..^ 3 ) = { 0 , 1 , 2 }
78 77 a1i 
 |-  ( ph -> ( 0 ..^ 3 ) = { 0 , 1 , 2 } )
79 78 mpteq1d 
 |-  ( ph -> ( k e. ( 0 ..^ 3 ) |-> ( ( F ` k ) .x. ( k .^ X ) ) ) = ( k e. { 0 , 1 , 2 } |-> ( ( F ` k ) .x. ( k .^ X ) ) ) )
80 79 oveq2d 
 |-  ( ph -> ( R gsum ( k e. ( 0 ..^ 3 ) |-> ( ( F ` k ) .x. ( k .^ X ) ) ) ) = ( R gsum ( k e. { 0 , 1 , 2 } |-> ( ( F ` k ) .x. ( k .^ X ) ) ) ) )
81 14 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` 3 ) ) -> M e. U )
82 uzss 
 |-  ( 3 e. ( ZZ>= ` 0 ) -> ( ZZ>= ` 3 ) C_ ( ZZ>= ` 0 ) )
83 71 82 ax-mp 
 |-  ( ZZ>= ` 3 ) C_ ( ZZ>= ` 0 )
84 83 69 sseqtrri 
 |-  ( ZZ>= ` 3 ) C_ NN0
85 84 a1i 
 |-  ( ph -> ( ZZ>= ` 3 ) C_ NN0 )
86 85 sselda 
 |-  ( ( ph /\ k e. ( ZZ>= ` 3 ) ) -> k e. NN0 )
87 15 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` 3 ) ) -> ( E ` M ) = 2 )
88 2p1e3 
 |-  ( 2 + 1 ) = 3
89 88 fveq2i 
 |-  ( ZZ>= ` ( 2 + 1 ) ) = ( ZZ>= ` 3 )
90 89 eleq2i 
 |-  ( k e. ( ZZ>= ` ( 2 + 1 ) ) <-> k e. ( ZZ>= ` 3 ) )
91 2z 
 |-  2 e. ZZ
92 eluzp1l 
 |-  ( ( 2 e. ZZ /\ k e. ( ZZ>= ` ( 2 + 1 ) ) ) -> 2 < k )
93 91 92 mpan 
 |-  ( k e. ( ZZ>= ` ( 2 + 1 ) ) -> 2 < k )
94 90 93 sylbir 
 |-  ( k e. ( ZZ>= ` 3 ) -> 2 < k )
95 94 adantl 
 |-  ( ( ph /\ k e. ( ZZ>= ` 3 ) ) -> 2 < k )
96 87 95 eqbrtrd 
 |-  ( ( ph /\ k e. ( ZZ>= ` 3 ) ) -> ( E ` M ) < k )
97 9 1 4 24 8 deg1lt 
 |-  ( ( M e. U /\ k e. NN0 /\ ( E ` M ) < k ) -> ( F ` k ) = ( 0g ` R ) )
98 81 86 96 97 syl3anc 
 |-  ( ( ph /\ k e. ( ZZ>= ` 3 ) ) -> ( F ` k ) = ( 0g ` R ) )
99 98 oveq1d 
 |-  ( ( ph /\ k e. ( ZZ>= ` 3 ) ) -> ( ( F ` k ) .x. ( k .^ X ) ) = ( ( 0g ` R ) .x. ( k .^ X ) ) )
100 25 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` 3 ) ) -> R e. Ring )
101 100 34 syl 
 |-  ( ( ph /\ k e. ( ZZ>= ` 3 ) ) -> ( mulGrp ` R ) e. Mnd )
102 16 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` 3 ) ) -> X e. K )
103 33 7 101 86 102 mulgnn0cld 
 |-  ( ( ph /\ k e. ( ZZ>= ` 3 ) ) -> ( k .^ X ) e. K )
104 3 5 24 100 103 ringlzd 
 |-  ( ( ph /\ k e. ( ZZ>= ` 3 ) ) -> ( ( 0g ` R ) .x. ( k .^ X ) ) = ( 0g ` R ) )
105 99 104 eqtrd 
 |-  ( ( ph /\ k e. ( ZZ>= ` 3 ) ) -> ( ( F ` k ) .x. ( k .^ X ) ) = ( 0g ` R ) )
106 105 mpteq2dva 
 |-  ( ph -> ( k e. ( ZZ>= ` 3 ) |-> ( ( F ` k ) .x. ( k .^ X ) ) ) = ( k e. ( ZZ>= ` 3 ) |-> ( 0g ` R ) ) )
107 106 oveq2d 
 |-  ( ph -> ( R gsum ( k e. ( ZZ>= ` 3 ) |-> ( ( F ` k ) .x. ( k .^ X ) ) ) ) = ( R gsum ( k e. ( ZZ>= ` 3 ) |-> ( 0g ` R ) ) ) )
108 13 crnggrpd 
 |-  ( ph -> R e. Grp )
109 108 grpmndd 
 |-  ( ph -> R e. Mnd )
110 fvexd 
 |-  ( ph -> ( ZZ>= ` 3 ) e. _V )
111 24 gsumz 
 |-  ( ( R e. Mnd /\ ( ZZ>= ` 3 ) e. _V ) -> ( R gsum ( k e. ( ZZ>= ` 3 ) |-> ( 0g ` R ) ) ) = ( 0g ` R ) )
112 109 110 111 syl2anc 
 |-  ( ph -> ( R gsum ( k e. ( ZZ>= ` 3 ) |-> ( 0g ` R ) ) ) = ( 0g ` R ) )
113 107 112 eqtrd 
 |-  ( ph -> ( R gsum ( k e. ( ZZ>= ` 3 ) |-> ( ( F ` k ) .x. ( k .^ X ) ) ) ) = ( 0g ` R ) )
114 80 113 oveq12d 
 |-  ( ph -> ( ( R gsum ( k e. ( 0 ..^ 3 ) |-> ( ( F ` k ) .x. ( k .^ X ) ) ) ) .+ ( R gsum ( k e. ( ZZ>= ` 3 ) |-> ( ( F ` k ) .x. ( k .^ X ) ) ) ) ) = ( ( R gsum ( k e. { 0 , 1 , 2 } |-> ( ( F ` k ) .x. ( k .^ X ) ) ) ) .+ ( 0g ` R ) ) )
115 tpex 
 |-  { 0 , 1 , 2 } e. _V
116 115 a1i 
 |-  ( ph -> { 0 , 1 , 2 } e. _V )
117 25 adantr 
 |-  ( ( ph /\ k e. { 0 , 1 , 2 } ) -> R e. Ring )
118 8 4 1 3 coe1f 
 |-  ( M e. U -> F : NN0 --> K )
119 14 118 syl 
 |-  ( ph -> F : NN0 --> K )
120 119 adantr 
 |-  ( ( ph /\ k e. { 0 , 1 , 2 } ) -> F : NN0 --> K )
121 fzo0ssnn0 
 |-  ( 0 ..^ 3 ) C_ NN0
122 78 121 eqsstrrdi 
 |-  ( ph -> { 0 , 1 , 2 } C_ NN0 )
123 122 sselda 
 |-  ( ( ph /\ k e. { 0 , 1 , 2 } ) -> k e. NN0 )
124 120 123 ffvelcdmd 
 |-  ( ( ph /\ k e. { 0 , 1 , 2 } ) -> ( F ` k ) e. K )
125 123 39 syldan 
 |-  ( ( ph /\ k e. { 0 , 1 , 2 } ) -> ( k .^ X ) e. K )
126 3 5 117 124 125 ringcld 
 |-  ( ( ph /\ k e. { 0 , 1 , 2 } ) -> ( ( F ` k ) .x. ( k .^ X ) ) e. K )
127 126 fmpttd 
 |-  ( ph -> ( k e. { 0 , 1 , 2 } |-> ( ( F ` k ) .x. ( k .^ X ) ) ) : { 0 , 1 , 2 } --> K )
128 fzofi 
 |-  ( 0 ..^ 3 ) e. Fin
129 78 128 eqeltrrdi 
 |-  ( ph -> { 0 , 1 , 2 } e. Fin )
130 127 129 41 fidmfisupp 
 |-  ( ph -> ( k e. { 0 , 1 , 2 } |-> ( ( F ` k ) .x. ( k .^ X ) ) ) finSupp ( 0g ` R ) )
131 3 24 26 116 127 130 gsumcl 
 |-  ( ph -> ( R gsum ( k e. { 0 , 1 , 2 } |-> ( ( F ` k ) .x. ( k .^ X ) ) ) ) e. K )
132 3 6 24 108 131 grpridd 
 |-  ( ph -> ( ( R gsum ( k e. { 0 , 1 , 2 } |-> ( ( F ` k ) .x. ( k .^ X ) ) ) ) .+ ( 0g ` R ) ) = ( R gsum ( k e. { 0 , 1 , 2 } |-> ( ( F ` k ) .x. ( k .^ X ) ) ) ) )
133 fveq2 
 |-  ( k = 0 -> ( F ` k ) = ( F ` 0 ) )
134 133 12 eqtr4di 
 |-  ( k = 0 -> ( F ` k ) = C )
135 oveq1 
 |-  ( k = 0 -> ( k .^ X ) = ( 0 .^ X ) )
136 134 135 oveq12d 
 |-  ( k = 0 -> ( ( F ` k ) .x. ( k .^ X ) ) = ( C .x. ( 0 .^ X ) ) )
137 fveq2 
 |-  ( k = 1 -> ( F ` k ) = ( F ` 1 ) )
138 137 11 eqtr4di 
 |-  ( k = 1 -> ( F ` k ) = B )
139 oveq1 
 |-  ( k = 1 -> ( k .^ X ) = ( 1 .^ X ) )
140 138 139 oveq12d 
 |-  ( k = 1 -> ( ( F ` k ) .x. ( k .^ X ) ) = ( B .x. ( 1 .^ X ) ) )
141 fveq2 
 |-  ( k = 2 -> ( F ` k ) = ( F ` 2 ) )
142 141 10 eqtr4di 
 |-  ( k = 2 -> ( F ` k ) = A )
143 oveq1 
 |-  ( k = 2 -> ( k .^ X ) = ( 2 .^ X ) )
144 142 143 oveq12d 
 |-  ( k = 2 -> ( ( F ` k ) .x. ( k .^ X ) ) = ( A .x. ( 2 .^ X ) ) )
145 0nn0 
 |-  0 e. NN0
146 145 a1i 
 |-  ( ph -> 0 e. NN0 )
147 1nn0 
 |-  1 e. NN0
148 147 a1i 
 |-  ( ph -> 1 e. NN0 )
149 0ne1 
 |-  0 =/= 1
150 149 a1i 
 |-  ( ph -> 0 =/= 1 )
151 1ne2 
 |-  1 =/= 2
152 151 a1i 
 |-  ( ph -> 1 =/= 2 )
153 0ne2 
 |-  0 =/= 2
154 153 a1i 
 |-  ( ph -> 0 =/= 2 )
155 8 4 1 3 coe1fvalcl 
 |-  ( ( M e. U /\ 0 e. NN0 ) -> ( F ` 0 ) e. K )
156 14 145 155 sylancl 
 |-  ( ph -> ( F ` 0 ) e. K )
157 12 156 eqeltrid 
 |-  ( ph -> C e. K )
158 33 7 35 146 16 mulgnn0cld 
 |-  ( ph -> ( 0 .^ X ) e. K )
159 3 5 25 157 158 ringcld 
 |-  ( ph -> ( C .x. ( 0 .^ X ) ) e. K )
160 8 4 1 3 coe1fvalcl 
 |-  ( ( M e. U /\ 1 e. NN0 ) -> ( F ` 1 ) e. K )
161 14 147 160 sylancl 
 |-  ( ph -> ( F ` 1 ) e. K )
162 11 161 eqeltrid 
 |-  ( ph -> B e. K )
163 33 7 35 148 16 mulgnn0cld 
 |-  ( ph -> ( 1 .^ X ) e. K )
164 3 5 25 162 163 ringcld 
 |-  ( ph -> ( B .x. ( 1 .^ X ) ) e. K )
165 8 4 1 3 coe1fvalcl 
 |-  ( ( M e. U /\ 2 e. NN0 ) -> ( F ` 2 ) e. K )
166 14 48 165 sylancl 
 |-  ( ph -> ( F ` 2 ) e. K )
167 10 166 eqeltrid 
 |-  ( ph -> A e. K )
168 33 7 35 49 16 mulgnn0cld 
 |-  ( ph -> ( 2 .^ X ) e. K )
169 3 5 25 167 168 ringcld 
 |-  ( ph -> ( A .x. ( 2 .^ X ) ) e. K )
170 3 6 136 140 144 26 146 148 49 150 152 154 159 164 169 gsumtp 
 |-  ( ph -> ( R gsum ( k e. { 0 , 1 , 2 } |-> ( ( F ` k ) .x. ( k .^ X ) ) ) ) = ( ( ( C .x. ( 0 .^ X ) ) .+ ( B .x. ( 1 .^ X ) ) ) .+ ( A .x. ( 2 .^ X ) ) ) )
171 3 6 108 159 164 grpcld 
 |-  ( ph -> ( ( C .x. ( 0 .^ X ) ) .+ ( B .x. ( 1 .^ X ) ) ) e. K )
172 3 6 cmncom 
 |-  ( ( R e. CMnd /\ ( ( C .x. ( 0 .^ X ) ) .+ ( B .x. ( 1 .^ X ) ) ) e. K /\ ( A .x. ( 2 .^ X ) ) e. K ) -> ( ( ( C .x. ( 0 .^ X ) ) .+ ( B .x. ( 1 .^ X ) ) ) .+ ( A .x. ( 2 .^ X ) ) ) = ( ( A .x. ( 2 .^ X ) ) .+ ( ( C .x. ( 0 .^ X ) ) .+ ( B .x. ( 1 .^ X ) ) ) ) )
173 26 171 169 172 syl3anc 
 |-  ( ph -> ( ( ( C .x. ( 0 .^ X ) ) .+ ( B .x. ( 1 .^ X ) ) ) .+ ( A .x. ( 2 .^ X ) ) ) = ( ( A .x. ( 2 .^ X ) ) .+ ( ( C .x. ( 0 .^ X ) ) .+ ( B .x. ( 1 .^ X ) ) ) ) )
174 3 6 cmncom 
 |-  ( ( R e. CMnd /\ ( C .x. ( 0 .^ X ) ) e. K /\ ( B .x. ( 1 .^ X ) ) e. K ) -> ( ( C .x. ( 0 .^ X ) ) .+ ( B .x. ( 1 .^ X ) ) ) = ( ( B .x. ( 1 .^ X ) ) .+ ( C .x. ( 0 .^ X ) ) ) )
175 26 159 164 174 syl3anc 
 |-  ( ph -> ( ( C .x. ( 0 .^ X ) ) .+ ( B .x. ( 1 .^ X ) ) ) = ( ( B .x. ( 1 .^ X ) ) .+ ( C .x. ( 0 .^ X ) ) ) )
176 33 7 mulg1 
 |-  ( X e. K -> ( 1 .^ X ) = X )
177 16 176 syl 
 |-  ( ph -> ( 1 .^ X ) = X )
178 177 oveq2d 
 |-  ( ph -> ( B .x. ( 1 .^ X ) ) = ( B .x. X ) )
179 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
180 32 179 ringidval 
 |-  ( 1r ` R ) = ( 0g ` ( mulGrp ` R ) )
181 33 180 7 mulg0 
 |-  ( X e. K -> ( 0 .^ X ) = ( 1r ` R ) )
182 16 181 syl 
 |-  ( ph -> ( 0 .^ X ) = ( 1r ` R ) )
183 182 oveq2d 
 |-  ( ph -> ( C .x. ( 0 .^ X ) ) = ( C .x. ( 1r ` R ) ) )
184 3 5 179 25 157 ringridmd 
 |-  ( ph -> ( C .x. ( 1r ` R ) ) = C )
185 183 184 eqtrd 
 |-  ( ph -> ( C .x. ( 0 .^ X ) ) = C )
186 178 185 oveq12d 
 |-  ( ph -> ( ( B .x. ( 1 .^ X ) ) .+ ( C .x. ( 0 .^ X ) ) ) = ( ( B .x. X ) .+ C ) )
187 175 186 eqtrd 
 |-  ( ph -> ( ( C .x. ( 0 .^ X ) ) .+ ( B .x. ( 1 .^ X ) ) ) = ( ( B .x. X ) .+ C ) )
188 187 oveq2d 
 |-  ( ph -> ( ( A .x. ( 2 .^ X ) ) .+ ( ( C .x. ( 0 .^ X ) ) .+ ( B .x. ( 1 .^ X ) ) ) ) = ( ( A .x. ( 2 .^ X ) ) .+ ( ( B .x. X ) .+ C ) ) )
189 170 173 188 3eqtrd 
 |-  ( ph -> ( R gsum ( k e. { 0 , 1 , 2 } |-> ( ( F ` k ) .x. ( k .^ X ) ) ) ) = ( ( A .x. ( 2 .^ X ) ) .+ ( ( B .x. X ) .+ C ) ) )
190 114 132 189 3eqtrd 
 |-  ( ph -> ( ( R gsum ( k e. ( 0 ..^ 3 ) |-> ( ( F ` k ) .x. ( k .^ X ) ) ) ) .+ ( R gsum ( k e. ( ZZ>= ` 3 ) |-> ( ( F ` k ) .x. ( k .^ X ) ) ) ) ) = ( ( A .x. ( 2 .^ X ) ) .+ ( ( B .x. X ) .+ C ) ) )
191 23 76 190 3eqtrd 
 |-  ( ph -> ( ( O ` M ) ` X ) = ( ( A .x. ( 2 .^ X ) ) .+ ( ( B .x. X ) .+ C ) ) )