evl1deg1

Description: Evaluation of a univariate polynomial of degree 1. (Contributed by Thierry Arnoux, 8-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}$
	evl1deg1.7	$⊢ C = {coe}_{1} (M)$
	evl1deg1.8	$⊢ D = \deg_{1} (R)$
	evl1deg1.9	$⊢ A = C (1)$
	evl1deg1.10	$⊢ B = C (0)$
	evl1deg1.11	$⊢ φ \to R \in CRing$
	evl1deg1.12	$⊢ φ \to M \in U$
	evl1deg1.13	$⊢ φ \to D (M) = 1$
	evl1deg1.14	$⊢ φ \to X \in K$
Assertion	evl1deg1	$⊢ φ \to O (M) (X) = (A \underset{˙}{\cdot} X) \underset{˙}{+} B$

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		evl1deg1.7	$⊢ C = {coe}_{1} (M)$
8		evl1deg1.8	$⊢ D = \deg_{1} (R)$
9		evl1deg1.9	$⊢ A = C (1)$
10		evl1deg1.10	$⊢ B = C (0)$
11		evl1deg1.11	$⊢ φ \to R \in CRing$
12		evl1deg1.12	$⊢ φ \to M \in U$
13		evl1deg1.13	$⊢ φ \to D (M) = 1$
14		evl1deg1.14	$⊢ φ \to X \in K$
15		oveq2	$⊢ x = X \to k \cdot_{{mulGrp}_{R}} x = k \cdot_{{mulGrp}_{R}} X$
16	15	oveq2d	$⊢ x = X \to C (k) \underset{˙}{\cdot} (k \cdot_{{mulGrp}_{R}} x) = C (k) \underset{˙}{\cdot} (k \cdot_{{mulGrp}_{R}} X)$
17	16	mpteq2dv	$⊢ x = X \to (k \in ℕ_{0} ⟼ C (k) \underset{˙}{\cdot} (k \cdot_{{mulGrp}_{R}} x)) = (k \in ℕ_{0} ⟼ C (k) \underset{˙}{\cdot} (k \cdot_{{mulGrp}_{R}} X))$
18	17	oveq2d	$⊢ x = X \to \underset{k \in ℕ_{0}}{\sum_{R}} (C (k) \underset{˙}{\cdot} (k \cdot_{{mulGrp}_{R}} x)) = \underset{k \in ℕ_{0}}{\sum_{R}} (C (k) \underset{˙}{\cdot} (k \cdot_{{mulGrp}_{R}} X))$
19		eqid	$⊢ \cdot_{{mulGrp}_{R}} = \cdot_{{mulGrp}_{R}}$
20	2 1 3 4 11 12 5 19 7	evl1fpws	$⊢ φ \to O (M) = (x \in K ⟼ \underset{k \in ℕ_{0}}{\sum_{R}} (C (k) \underset{˙}{\cdot} (k \cdot_{{mulGrp}_{R}} x)))$
21		ovexd	$⊢ φ \to \underset{k \in ℕ_{0}}{\sum_{R}} (C (k) \underset{˙}{\cdot} (k \cdot_{{mulGrp}_{R}} X)) \in V$
22	18 20 14 21	fvmptd4	$⊢ φ \to O (M) (X) = \underset{k \in ℕ_{0}}{\sum_{R}} (C (k) \underset{˙}{\cdot} (k \cdot_{{mulGrp}_{R}} X))$
23		eqid	$⊢ 0_{R} = 0_{R}$
24	11	crngringd	$⊢ φ \to R \in Ring$
25	24	ringcmnd	$⊢ φ \to R \in CMnd$
26		nn0ex	$⊢ ℕ_{0} \in V$
27	26	a1i	$⊢ φ \to ℕ_{0} \in V$
28	24	adantr	$⊢ (φ \land k \in ℕ_{0}) \to R \in Ring$
29	7 4 1 3	coe1fvalcl	$⊢ (M \in U \land k \in ℕ_{0}) \to C (k) \in K$
30	12 29	sylan	$⊢ (φ \land k \in ℕ_{0}) \to C (k) \in K$
31		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
32	31 3	mgpbas	$⊢ K = {Base}_{{mulGrp}_{R}}$
33	31	ringmgp	$⊢ R \in Ring \to {mulGrp}_{R} \in Mnd$
34	24 33	syl	$⊢ φ \to {mulGrp}_{R} \in Mnd$
35	34	adantr	$⊢ (φ \land k \in ℕ_{0}) \to {mulGrp}_{R} \in Mnd$
36		simpr	$⊢ (φ \land k \in ℕ_{0}) \to k \in ℕ_{0}$
37	14	adantr	$⊢ (φ \land k \in ℕ_{0}) \to X \in K$
38	32 19 35 36 37	mulgnn0cld	$⊢ (φ \land k \in ℕ_{0}) \to k \cdot_{{mulGrp}_{R}} X \in K$
39	3 5 28 30 38	ringcld	$⊢ (φ \land k \in ℕ_{0}) \to C (k) \underset{˙}{\cdot} (k \cdot_{{mulGrp}_{R}} X) \in K$
40		fvexd	$⊢ φ \to 0_{R} \in V$
41		fveq2	$⊢ k = j \to C (k) = C (j)$
42		oveq1	$⊢ k = j \to k \cdot_{{mulGrp}_{R}} X = j \cdot_{{mulGrp}_{R}} X$
43	41 42	oveq12d	$⊢ k = j \to C (k) \underset{˙}{\cdot} (k \cdot_{{mulGrp}_{R}} X) = C (j) \underset{˙}{\cdot} (j \cdot_{{mulGrp}_{R}} X)$
44		breq1	$⊢ i = D (M) \to (i < j \leftrightarrow D (M) < j)$
45	44	imbi1d	$⊢ i = D (M) \to ((i < j \to C (j) \underset{˙}{\cdot} (j \cdot_{{mulGrp}_{R}} X) = 0_{R}) \leftrightarrow (D (M) < j \to C (j) \underset{˙}{\cdot} (j \cdot_{{mulGrp}_{R}} X) = 0_{R}))$
46	45	ralbidv	$⊢ i = D (M) \to (\forall j \in ℕ_{0} (i < j \to C (j) \underset{˙}{\cdot} (j \cdot_{{mulGrp}_{R}} X) = 0_{R}) \leftrightarrow \forall j \in ℕ_{0} (D (M) < j \to C (j) \underset{˙}{\cdot} (j \cdot_{{mulGrp}_{R}} X) = 0_{R}))$
47		1nn0	$⊢ 1 \in ℕ_{0}$
48	13 47	eqeltrdi	$⊢ φ \to D (M) \in ℕ_{0}$
49	12	ad2antrr	$⊢ ((φ \land j \in ℕ_{0}) \land D (M) < j) \to M \in U$
50		simplr	$⊢ ((φ \land j \in ℕ_{0}) \land D (M) < j) \to j \in ℕ_{0}$
51		simpr	$⊢ ((φ \land j \in ℕ_{0}) \land D (M) < j) \to D (M) < j$
52	8 1 4 23 7	deg1lt	$⊢ (M \in U \land j \in ℕ_{0} \land D (M) < j) \to C (j) = 0_{R}$
53	49 50 51 52	syl3anc	$⊢ ((φ \land j \in ℕ_{0}) \land D (M) < j) \to C (j) = 0_{R}$
54	53	oveq1d	$⊢ ((φ \land j \in ℕ_{0}) \land D (M) < j) \to C (j) \underset{˙}{\cdot} (j \cdot_{{mulGrp}_{R}} X) = 0_{R} \underset{˙}{\cdot} (j \cdot_{{mulGrp}_{R}} X)$
55	24	ad2antrr	$⊢ ((φ \land j \in ℕ_{0}) \land D (M) < j) \to R \in Ring$
56	55 33	syl	$⊢ ((φ \land j \in ℕ_{0}) \land D (M) < j) \to {mulGrp}_{R} \in Mnd$
57	14	ad2antrr	$⊢ ((φ \land j \in ℕ_{0}) \land D (M) < j) \to X \in K$
58	32 19 56 50 57	mulgnn0cld	$⊢ ((φ \land j \in ℕ_{0}) \land D (M) < j) \to j \cdot_{{mulGrp}_{R}} X \in K$
59	3 5 23 55 58	ringlzd	$⊢ ((φ \land j \in ℕ_{0}) \land D (M) < j) \to 0_{R} \underset{˙}{\cdot} (j \cdot_{{mulGrp}_{R}} X) = 0_{R}$
60	54 59	eqtrd	$⊢ ((φ \land j \in ℕ_{0}) \land D (M) < j) \to C (j) \underset{˙}{\cdot} (j \cdot_{{mulGrp}_{R}} X) = 0_{R}$
61	60	ex	$⊢ (φ \land j \in ℕ_{0}) \to (D (M) < j \to C (j) \underset{˙}{\cdot} (j \cdot_{{mulGrp}_{R}} X) = 0_{R})$
62	61	ralrimiva	$⊢ φ \to \forall j \in ℕ_{0} (D (M) < j \to C (j) \underset{˙}{\cdot} (j \cdot_{{mulGrp}_{R}} X) = 0_{R})$
63	46 48 62	rspcedvdw	$⊢ φ \to \exists i \in ℕ_{0} \forall j \in ℕ_{0} (i < j \to C (j) \underset{˙}{\cdot} (j \cdot_{{mulGrp}_{R}} X) = 0_{R})$
64	40 39 43 63	mptnn0fsuppd	$⊢ φ \to {finSupp}_{0_{R}} ((k \in ℕ_{0} ⟼ C (k) \underset{˙}{\cdot} (k \cdot_{{mulGrp}_{R}} X)))$
65		nn0disj01	$⊢ \{0, 1\} \cap ℤ_{\geq 2} = \emptyset$
66	65	a1i	$⊢ φ \to \{0, 1\} \cap ℤ_{\geq 2} = \emptyset$
67		nn0split01	$⊢ ℕ_{0} = \{0, 1\} \cup ℤ_{\geq 2}$
68	67	a1i	$⊢ φ \to ℕ_{0} = \{0, 1\} \cup ℤ_{\geq 2}$
69	3 23 6 25 27 39 64 66 68	gsumsplit2	$⊢ φ \to \underset{k \in ℕ_{0}}{\sum_{R}} (C (k) \underset{˙}{\cdot} (k \cdot_{{mulGrp}_{R}} X)) = (\underset{k \in \{0, 1\}}{\sum_{R}}, (C (k) \underset{˙}{\cdot} (k \cdot_{{mulGrp}_{R}} X))) \underset{˙}{+} (\underset{k \in ℤ_{\geq 2}}{\sum_{R}}, (C (k) \underset{˙}{\cdot} (k \cdot_{{mulGrp}_{R}} X)))$
70		0nn0	$⊢ 0 \in ℕ_{0}$
71	70	a1i	$⊢ φ \to 0 \in ℕ_{0}$
72	47	a1i	$⊢ φ \to 1 \in ℕ_{0}$
73		0ne1	$⊢ 0 \neq 1$
74	73	a1i	$⊢ φ \to 0 \neq 1$
75	7 4 1 3	coe1fvalcl	$⊢ (M \in U \land 0 \in ℕ_{0}) \to C (0) \in K$
76	12 70 75	sylancl	$⊢ φ \to C (0) \in K$
77	32 19 34 71 14	mulgnn0cld	$⊢ φ \to 0 \cdot_{{mulGrp}_{R}} X \in K$
78	3 5 24 76 77	ringcld	$⊢ φ \to C (0) \underset{˙}{\cdot} (0 \cdot_{{mulGrp}_{R}} X) \in K$
79	7 4 1 3	coe1fvalcl	$⊢ (M \in U \land 1 \in ℕ_{0}) \to C (1) \in K$
80	12 47 79	sylancl	$⊢ φ \to C (1) \in K$
81	32 19 34 72 14	mulgnn0cld	$⊢ φ \to 1 \cdot_{{mulGrp}_{R}} X \in K$
82	3 5 24 80 81	ringcld	$⊢ φ \to C (1) \underset{˙}{\cdot} (1 \cdot_{{mulGrp}_{R}} X) \in K$
83		fveq2	$⊢ k = 0 \to C (k) = C (0)$
84		oveq1	$⊢ k = 0 \to k \cdot_{{mulGrp}_{R}} X = 0 \cdot_{{mulGrp}_{R}} X$
85	83 84	oveq12d	$⊢ k = 0 \to C (k) \underset{˙}{\cdot} (k \cdot_{{mulGrp}_{R}} X) = C (0) \underset{˙}{\cdot} (0 \cdot_{{mulGrp}_{R}} X)$
86		fveq2	$⊢ k = 1 \to C (k) = C (1)$
87		oveq1	$⊢ k = 1 \to k \cdot_{{mulGrp}_{R}} X = 1 \cdot_{{mulGrp}_{R}} X$
88	86 87	oveq12d	$⊢ k = 1 \to C (k) \underset{˙}{\cdot} (k \cdot_{{mulGrp}_{R}} X) = C (1) \underset{˙}{\cdot} (1 \cdot_{{mulGrp}_{R}} X)$
89	3 6 85 88	gsumpr	$⊢ (R \in CMnd \land (0 \in ℕ_{0} \land 1 \in ℕ_{0} \land 0 \neq 1) \land (C (0) \underset{˙}{\cdot} (0 \cdot_{{mulGrp}_{R}} X) \in K \land C (1) \underset{˙}{\cdot} (1 \cdot_{{mulGrp}_{R}} X) \in K)) \to \underset{k \in \{0, 1\}}{\sum_{R}} (C (k) \underset{˙}{\cdot} (k \cdot_{{mulGrp}_{R}} X)) = (C (0) \underset{˙}{\cdot} (0 \cdot_{{mulGrp}_{R}} X)) \underset{˙}{+} (C (1) \underset{˙}{\cdot} (1 \cdot_{{mulGrp}_{R}} X))$
90	25 71 72 74 78 82 89	syl132anc	$⊢ φ \to \underset{k \in \{0, 1\}}{\sum_{R}} (C (k) \underset{˙}{\cdot} (k \cdot_{{mulGrp}_{R}} X)) = (C (0) \underset{˙}{\cdot} (0 \cdot_{{mulGrp}_{R}} X)) \underset{˙}{+} (C (1) \underset{˙}{\cdot} (1 \cdot_{{mulGrp}_{R}} X))$
91	12	adantr	$⊢ (φ \land k \in ℤ_{\geq 2}) \to M \in U$
92		2eluzge0	$⊢ 2 \in ℤ_{\geq 0}$
93		uzss	$⊢ 2 \in ℤ_{\geq 0} \to ℤ_{\geq 2} \subseteq ℤ_{\geq 0}$
94	92 93	ax-mp	$⊢ ℤ_{\geq 2} \subseteq ℤ_{\geq 0}$
95		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
96	94 95	sseqtrri	$⊢ ℤ_{\geq 2} \subseteq ℕ_{0}$
97	96	a1i	$⊢ φ \to ℤ_{\geq 2} \subseteq ℕ_{0}$
98	97	sselda	$⊢ (φ \land k \in ℤ_{\geq 2}) \to k \in ℕ_{0}$
99	13	adantr	$⊢ (φ \land k \in ℤ_{\geq 2}) \to D (M) = 1$
100		eluz2gt1	$⊢ k \in ℤ_{\geq 2} \to 1 < k$
101	100	adantl	$⊢ (φ \land k \in ℤ_{\geq 2}) \to 1 < k$
102	99 101	eqbrtrd	$⊢ (φ \land k \in ℤ_{\geq 2}) \to D (M) < k$
103	8 1 4 23 7	deg1lt	$⊢ (M \in U \land k \in ℕ_{0} \land D (M) < k) \to C (k) = 0_{R}$
104	91 98 102 103	syl3anc	$⊢ (φ \land k \in ℤ_{\geq 2}) \to C (k) = 0_{R}$
105	104	oveq1d	$⊢ (φ \land k \in ℤ_{\geq 2}) \to C (k) \underset{˙}{\cdot} (k \cdot_{{mulGrp}_{R}} X) = 0_{R} \underset{˙}{\cdot} (k \cdot_{{mulGrp}_{R}} X)$
106	24	adantr	$⊢ (φ \land k \in ℤ_{\geq 2}) \to R \in Ring$
107	106 33	syl	$⊢ (φ \land k \in ℤ_{\geq 2}) \to {mulGrp}_{R} \in Mnd$
108	14	adantr	$⊢ (φ \land k \in ℤ_{\geq 2}) \to X \in K$
109	32 19 107 98 108	mulgnn0cld	$⊢ (φ \land k \in ℤ_{\geq 2}) \to k \cdot_{{mulGrp}_{R}} X \in K$
110	3 5 23 106 109	ringlzd	$⊢ (φ \land k \in ℤ_{\geq 2}) \to 0_{R} \underset{˙}{\cdot} (k \cdot_{{mulGrp}_{R}} X) = 0_{R}$
111	105 110	eqtrd	$⊢ (φ \land k \in ℤ_{\geq 2}) \to C (k) \underset{˙}{\cdot} (k \cdot_{{mulGrp}_{R}} X) = 0_{R}$
112	111	mpteq2dva	$⊢ φ \to (k \in ℤ_{\geq 2} ⟼ C (k) \underset{˙}{\cdot} (k \cdot_{{mulGrp}_{R}} X)) = (k \in ℤ_{\geq 2} ⟼ 0_{R})$
113	112	oveq2d	$⊢ φ \to \underset{k \in ℤ_{\geq 2}}{\sum_{R}} (C (k) \underset{˙}{\cdot} (k \cdot_{{mulGrp}_{R}} X)) = \underset{k \in ℤ_{\geq 2}}{\sum_{R}} 0_{R}$
114	90 113	oveq12d	$⊢ φ \to (\underset{k \in \{0, 1\}}{\sum_{R}}, (C (k) \underset{˙}{\cdot} (k \cdot_{{mulGrp}_{R}} X))) \underset{˙}{+} (\underset{k \in ℤ_{\geq 2}}{\sum_{R}}, (C (k) \underset{˙}{\cdot} (k \cdot_{{mulGrp}_{R}} X))) = ((C (0) \underset{˙}{\cdot} (0 \cdot_{{mulGrp}_{R}} X)) \underset{˙}{+} (C (1) \underset{˙}{\cdot} (1 \cdot_{{mulGrp}_{R}} X))) \underset{˙}{+} (\underset{k \in ℤ_{\geq 2}}{\sum_{R}}, 0_{R})$
115		eqid	$⊢ 1_{R} = 1_{R}$
116	10 76	eqeltrid	$⊢ φ \to B \in K$
117	3 5 115 24 116	ringridmd	$⊢ φ \to B \underset{˙}{\cdot} 1_{R} = B$
118	117	oveq1d	$⊢ φ \to (B \underset{˙}{\cdot} 1_{R}) \underset{˙}{+} (A \underset{˙}{\cdot} X) = B \underset{˙}{+} (A \underset{˙}{\cdot} X)$
119	10	a1i	$⊢ φ \to B = C (0)$
120	31 115	ringidval	$⊢ 1_{R} = 0_{{mulGrp}_{R}}$
121	32 120 19	mulg0	$⊢ X \in K \to 0 \cdot_{{mulGrp}_{R}} X = 1_{R}$
122	14 121	syl	$⊢ φ \to 0 \cdot_{{mulGrp}_{R}} X = 1_{R}$
123	122	eqcomd	$⊢ φ \to 1_{R} = 0 \cdot_{{mulGrp}_{R}} X$
124	119 123	oveq12d	$⊢ φ \to B \underset{˙}{\cdot} 1_{R} = C (0) \underset{˙}{\cdot} (0 \cdot_{{mulGrp}_{R}} X)$
125	9	a1i	$⊢ φ \to A = C (1)$
126	32 19	mulg1	$⊢ X \in K \to 1 \cdot_{{mulGrp}_{R}} X = X$
127	14 126	syl	$⊢ φ \to 1 \cdot_{{mulGrp}_{R}} X = X$
128	127	eqcomd	$⊢ φ \to X = 1 \cdot_{{mulGrp}_{R}} X$
129	125 128	oveq12d	$⊢ φ \to A \underset{˙}{\cdot} X = C (1) \underset{˙}{\cdot} (1 \cdot_{{mulGrp}_{R}} X)$
130	124 129	oveq12d	$⊢ φ \to (B \underset{˙}{\cdot} 1_{R}) \underset{˙}{+} (A \underset{˙}{\cdot} X) = (C (0) \underset{˙}{\cdot} (0 \cdot_{{mulGrp}_{R}} X)) \underset{˙}{+} (C (1) \underset{˙}{\cdot} (1 \cdot_{{mulGrp}_{R}} X))$
131	9 80	eqeltrid	$⊢ φ \to A \in K$
132	3 5 24 131 14	ringcld	$⊢ φ \to A \underset{˙}{\cdot} X \in K$
133	3 6	ringcom	$⊢ (R \in Ring \land B \in K \land A \underset{˙}{\cdot} X \in K) \to B \underset{˙}{+} (A \underset{˙}{\cdot} X) = (A \underset{˙}{\cdot} X) \underset{˙}{+} B$
134	24 116 132 133	syl3anc	$⊢ φ \to B \underset{˙}{+} (A \underset{˙}{\cdot} X) = (A \underset{˙}{\cdot} X) \underset{˙}{+} B$
135	118 130 134	3eqtr3d	$⊢ φ \to (C (0) \underset{˙}{\cdot} (0 \cdot_{{mulGrp}_{R}} X)) \underset{˙}{+} (C (1) \underset{˙}{\cdot} (1 \cdot_{{mulGrp}_{R}} X)) = (A \underset{˙}{\cdot} X) \underset{˙}{+} B$
136	11	crnggrpd	$⊢ φ \to R \in Grp$
137	136	grpmndd	$⊢ φ \to R \in Mnd$
138		fvexd	$⊢ φ \to ℤ_{\geq 2} \in V$
139	23	gsumz	$⊢ (R \in Mnd \land ℤ_{\geq 2} \in V) \to \underset{k \in ℤ_{\geq 2}}{\sum_{R}} 0_{R} = 0_{R}$
140	137 138 139	syl2anc	$⊢ φ \to \underset{k \in ℤ_{\geq 2}}{\sum_{R}} 0_{R} = 0_{R}$
141	135 140	oveq12d	$⊢ φ \to ((C (0) \underset{˙}{\cdot} (0 \cdot_{{mulGrp}_{R}} X)) \underset{˙}{+} (C (1) \underset{˙}{\cdot} (1 \cdot_{{mulGrp}_{R}} X))) \underset{˙}{+} (\underset{k \in ℤ_{\geq 2}}{\sum_{R}}, 0_{R}) = ((A \underset{˙}{\cdot} X) \underset{˙}{+} B) \underset{˙}{+} 0_{R}$
142	3 6 136 132 116	grpcld	$⊢ φ \to (A \underset{˙}{\cdot} X) \underset{˙}{+} B \in K$
143	3 6 23 136 142	grpridd	$⊢ φ \to ((A \underset{˙}{\cdot} X) \underset{˙}{+} B) \underset{˙}{+} 0_{R} = (A \underset{˙}{\cdot} X) \underset{˙}{+} B$
144	114 141 143	3eqtrd	$⊢ φ \to (\underset{k \in \{0, 1\}}{\sum_{R}}, (C (k) \underset{˙}{\cdot} (k \cdot_{{mulGrp}_{R}} X))) \underset{˙}{+} (\underset{k \in ℤ_{\geq 2}}{\sum_{R}}, (C (k) \underset{˙}{\cdot} (k \cdot_{{mulGrp}_{R}} X))) = (A \underset{˙}{\cdot} X) \underset{˙}{+} B$
145	22 69 144	3eqtrd	$⊢ φ \to O (M) (X) = (A \underset{˙}{\cdot} X) \underset{˙}{+} B$

Metamath Proof Explorer

Theorem evl1deg1

Proof