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