evl1deg2

Description: Evaluation of a univariate polynomial of degree 2. (Contributed by Thierry Arnoux, 22-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}}$
	evl1deg2.f	$⊢ F = {coe}_{1} (M)$
	evl1deg2.e	$⊢ E = \deg_{1} (R)$
	evl1deg2.a	$⊢ A = F (2)$
	evl1deg2.b	$⊢ B = F (1)$
	evl1deg2.c	$⊢ C = F (0)$
	evl1deg2.r	$⊢ φ \to R \in CRing$
	evl1deg2.m	$⊢ φ \to M \in U$
	evl1deg2.1	$⊢ φ \to E (M) = 2$
	evl1deg2.x	$⊢ φ \to X \in K$
Assertion	evl1deg2	$⊢ φ \to O (M) (X) = (A \underset{˙}{\cdot} (2 \underset{˙}{\times} X)) \underset{˙}{+} ((B \underset{˙}{\cdot} X) \underset{˙}{+} C)$

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

Metamath Proof Explorer

Theorem evl1deg2

Proof