evl1deg3

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

	Ref	Expression
Hypotheses	evl1deg1.1	$⊢ P = {Poly}_{1} (R)$
	evl1deg1.2	$⊢ O = {eval}_{1} (R)$
	evl1deg1.3	$⊢ K = {Base}_{R}$
	evl1deg1.4	$⊢ U = {Base}_{P}$
	evl1deg1.5	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	evl1deg1.6	$⊢ \underset{˙}{+} = +_{R}$
	evl1deg2.p	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{R}}$
	evl1deg3.f	$⊢ F = {coe}_{1} (M)$
	evl1deg3.e	$⊢ E = \deg_{1} (R)$
	evl1deg3.a	$⊢ A = F (3)$
	evl1deg3.b	$⊢ B = F (2)$
	evl1deg3.c	$⊢ C = F (1)$
	evl1deg3.d	$⊢ D = F (0)$
	evl1deg3.r	$⊢ φ \to R \in CRing$
	evl1deg3.m	$⊢ φ \to M \in U$
	evl1deg3.1	$⊢ φ \to E (M) = 3$
	evl1deg3.x	$⊢ φ \to X \in K$
Assertion	evl1deg3	$⊢ φ \to O (M) (X) = ((A \underset{˙}{\cdot} (3 \underset{˙}{\times} X)) \underset{˙}{+} (B \underset{˙}{\cdot} (2 \underset{˙}{\times} X))) \underset{˙}{+} ((C \underset{˙}{\cdot} X) \underset{˙}{+} D)$

Proof

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

Metamath Proof Explorer

Theorem evl1deg3

Proof