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