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

Metamath Proof Explorer

Theorem evl1deg3

Description: Evaluation of a univariate polynomial of degree 3. (Contributed by Thierry Arnoux, 14-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 ) )
evl1deg3.f 
|- F = ( coe1 ` M )
evl1deg3.e 
|- E = ( deg1 ` R )
evl1deg3.a 
|- A = ( F ` 3 )
evl1deg3.b 
|- B = ( F ` 2 )
evl1deg3.c 
|- C = ( F ` 1 )
evl1deg3.d 
|- D = ( F ` 0 )
evl1deg3.r 
|- ( ph -> R e. CRing )
evl1deg3.m 
|- ( ph -> M e. U )
evl1deg3.1 
|- ( ph -> ( E ` M ) = 3 )
evl1deg3.x 
|- ( ph -> X e. K )
Assertion evl1deg3 
|- ( ph -> ( ( O ` M ) ` X ) = ( ( ( A .x. ( 3 .^ X ) ) .+ ( B .x. ( 2 .^ X ) ) ) .+ ( ( C .x. X ) .+ D ) ) )

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