ply1coe

Description: Decompose a univariate polynomial as a sum of powers. (Contributed by Stefan O'Rear, 21-Mar-2015) (Revised by AV, 7-Oct-2019)

	Ref	Expression
Hypotheses	ply1coe.p	$⊢ P = {Poly}_{1} (R)$
	ply1coe.x	$⊢ X = {var}_{1} (R)$
	ply1coe.b	$⊢ B = {Base}_{P}$
	ply1coe.n	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
	ply1coe.m	$⊢ M = {mulGrp}_{P}$
	ply1coe.e	$⊢ \underset{˙}{\times} = \cdot_{M}$
	ply1coe.a	$⊢ A = {coe}_{1} (K)$
Assertion	ply1coe	$⊢ (R \in Ring \land K \in B) \to K = \underset{k \in ℕ_{0}}{\sum_{P}} (A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X))$

Proof

Step	Hyp	Ref	Expression
1		ply1coe.p	$⊢ P = {Poly}_{1} (R)$
2		ply1coe.x	$⊢ X = {var}_{1} (R)$
3		ply1coe.b	$⊢ B = {Base}_{P}$
4		ply1coe.n	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
5		ply1coe.m	$⊢ M = {mulGrp}_{P}$
6		ply1coe.e	$⊢ \underset{˙}{\times} = \cdot_{M}$
7		ply1coe.a	$⊢ A = {coe}_{1} (K)$
8		eqid	$⊢ 1_{𝑜} mPoly R = 1_{𝑜} mPoly R$
9		psr1baslem	$⊢ {ℕ_{0}}^{1_{𝑜}} = \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d^{-1} [ℕ] \in Fin\}$
10		eqid	$⊢ 0_{R} = 0_{R}$
11		eqid	$⊢ 1_{R} = 1_{R}$
12		1onn	$⊢ 1_{𝑜} \in ω$
13	12	a1i	$⊢ (R \in Ring \land K \in B) \to 1_{𝑜} \in ω$
14	1 3	ply1bas	$⊢ B = {Base}_{(1_{𝑜} mPoly R)}$
15	1 8 4	ply1vsca	$⊢ \underset{˙}{\cdot} = \cdot_{(1_{𝑜} mPoly R)}$
16		simpl	$⊢ (R \in Ring \land K \in B) \to R \in Ring$
17		simpr	$⊢ (R \in Ring \land K \in B) \to K \in B$
18	8 9 10 11 13 14 15 16 17	mplcoe1	$⊢ (R \in Ring \land K \in B) \to K = \underset{a \in {ℕ_{0}}^{1_{𝑜}}}{\sum_{1_{𝑜} mPoly R}} (K (a) \underset{˙}{\cdot} (b \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ if (b = a, 1_{R}, 0_{R})))$
19	7	fvcoe1	$⊢ (K \in B \land a \in ({ℕ_{0}}^{1_{𝑜}})) \to K (a) = A (a (\emptyset))$
20	19	adantll	$⊢ ((R \in Ring \land K \in B) \land a \in ({ℕ_{0}}^{1_{𝑜}})) \to K (a) = A (a (\emptyset))$
21	12	a1i	$⊢ ((R \in Ring \land K \in B) \land a \in ({ℕ_{0}}^{1_{𝑜}})) \to 1_{𝑜} \in ω$
22		eqid	$⊢ {mulGrp}_{(1_{𝑜} mPoly R)} = {mulGrp}_{(1_{𝑜} mPoly R)}$
23		eqid	$⊢ \cdot_{{mulGrp}_{(1_{𝑜} mPoly R)}} = \cdot_{{mulGrp}_{(1_{𝑜} mPoly R)}}$
24		eqid	$⊢ 1_{𝑜} mVar R = 1_{𝑜} mVar R$
25		simpll	$⊢ ((R \in Ring \land K \in B) \land a \in ({ℕ_{0}}^{1_{𝑜}})) \to R \in Ring$
26		simpr	$⊢ ((R \in Ring \land K \in B) \land a \in ({ℕ_{0}}^{1_{𝑜}})) \to a \in ({ℕ_{0}}^{1_{𝑜}})$
27		eqidd	$⊢ ((R \in Ring \land K \in B) \land a \in ({ℕ_{0}}^{1_{𝑜}})) \to (1_{𝑜} mVar R) (\emptyset) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (\emptyset) = (1_{𝑜} mVar R) (\emptyset) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (\emptyset)$
28		0ex	$⊢ \emptyset \in V$
29		fveq2	$⊢ b = \emptyset \to (1_{𝑜} mVar R) (b) = (1_{𝑜} mVar R) (\emptyset)$
30	29	oveq1d	$⊢ b = \emptyset \to (1_{𝑜} mVar R) (b) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (\emptyset) = (1_{𝑜} mVar R) (\emptyset) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (\emptyset)$
31	29	oveq2d	$⊢ b = \emptyset \to (1_{𝑜} mVar R) (\emptyset) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (b) = (1_{𝑜} mVar R) (\emptyset) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (\emptyset)$
32	30 31	eqeq12d	$⊢ b = \emptyset \to ((1_{𝑜} mVar R) (b) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (\emptyset) = (1_{𝑜} mVar R) (\emptyset) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (b) \leftrightarrow (1_{𝑜} mVar R) (\emptyset) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (\emptyset) = (1_{𝑜} mVar R) (\emptyset) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (\emptyset))$
33	28 32	ralsn	$⊢ \forall b \in \{\emptyset\} (1_{𝑜} mVar R) (b) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (\emptyset) = (1_{𝑜} mVar R) (\emptyset) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (b) \leftrightarrow (1_{𝑜} mVar R) (\emptyset) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (\emptyset) = (1_{𝑜} mVar R) (\emptyset) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (\emptyset)$
34	27 33	sylibr	$⊢ ((R \in Ring \land K \in B) \land a \in ({ℕ_{0}}^{1_{𝑜}})) \to \forall b \in \{\emptyset\} (1_{𝑜} mVar R) (b) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (\emptyset) = (1_{𝑜} mVar R) (\emptyset) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (b)$
35		fveq2	$⊢ x = \emptyset \to (1_{𝑜} mVar R) (x) = (1_{𝑜} mVar R) (\emptyset)$
36	35	oveq2d	$⊢ x = \emptyset \to (1_{𝑜} mVar R) (b) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (x) = (1_{𝑜} mVar R) (b) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (\emptyset)$
37	35	oveq1d	$⊢ x = \emptyset \to (1_{𝑜} mVar R) (x) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (b) = (1_{𝑜} mVar R) (\emptyset) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (b)$
38	36 37	eqeq12d	$⊢ x = \emptyset \to ((1_{𝑜} mVar R) (b) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (x) = (1_{𝑜} mVar R) (x) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (b) \leftrightarrow (1_{𝑜} mVar R) (b) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (\emptyset) = (1_{𝑜} mVar R) (\emptyset) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (b))$
39	38	ralbidv	$⊢ x = \emptyset \to (\forall b \in \{\emptyset\} (1_{𝑜} mVar R) (b) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (x) = (1_{𝑜} mVar R) (x) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (b) \leftrightarrow \forall b \in \{\emptyset\} (1_{𝑜} mVar R) (b) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (\emptyset) = (1_{𝑜} mVar R) (\emptyset) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (b))$
40	28 39	ralsn	$⊢ \forall x \in \{\emptyset\} \forall b \in \{\emptyset\} (1_{𝑜} mVar R) (b) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (x) = (1_{𝑜} mVar R) (x) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (b) \leftrightarrow \forall b \in \{\emptyset\} (1_{𝑜} mVar R) (b) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (\emptyset) = (1_{𝑜} mVar R) (\emptyset) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (b)$
41	34 40	sylibr	$⊢ ((R \in Ring \land K \in B) \land a \in ({ℕ_{0}}^{1_{𝑜}})) \to \forall x \in \{\emptyset\} \forall b \in \{\emptyset\} (1_{𝑜} mVar R) (b) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (x) = (1_{𝑜} mVar R) (x) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (b)$
42		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
43	42	raleqi	$⊢ \forall b \in 1_{𝑜} (1_{𝑜} mVar R) (b) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (x) = (1_{𝑜} mVar R) (x) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (b) \leftrightarrow \forall b \in \{\emptyset\} (1_{𝑜} mVar R) (b) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (x) = (1_{𝑜} mVar R) (x) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (b)$
44	42 43	raleqbii	$⊢ \forall x \in 1_{𝑜} \forall b \in 1_{𝑜} (1_{𝑜} mVar R) (b) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (x) = (1_{𝑜} mVar R) (x) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (b) \leftrightarrow \forall x \in \{\emptyset\} \forall b \in \{\emptyset\} (1_{𝑜} mVar R) (b) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (x) = (1_{𝑜} mVar R) (x) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (b)$
45	41 44	sylibr	$⊢ ((R \in Ring \land K \in B) \land a \in ({ℕ_{0}}^{1_{𝑜}})) \to \forall x \in 1_{𝑜} \forall b \in 1_{𝑜} (1_{𝑜} mVar R) (b) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (x) = (1_{𝑜} mVar R) (x) +_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (b)$
46	8 9 10 11 21 22 23 24 25 26 45	mplcoe5	$⊢ ((R \in Ring \land K \in B) \land a \in ({ℕ_{0}}^{1_{𝑜}})) \to (b \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ if (b = a, 1_{R}, 0_{R})) = \underset{c \in 1_{𝑜}}{\sum_{{mulGrp}_{(1_{𝑜} mPoly R)}}} (a (c) \cdot_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (c))$
47	42	mpteq1i	$⊢ (c \in 1_{𝑜} ⟼ a (c) \cdot_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (c)) = (c \in \{\emptyset\} ⟼ a (c) \cdot_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (c))$
48	47	oveq2i	$⊢ \underset{c \in 1_{𝑜}}{\sum_{{mulGrp}_{(1_{𝑜} mPoly R)}}} (a (c) \cdot_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (c)) = \underset{c \in \{\emptyset\}}{\sum_{{mulGrp}_{(1_{𝑜} mPoly R)}}} (a (c) \cdot_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (c))$
49	8	mplring	$⊢ (1_{𝑜} \in ω \land R \in Ring) \to 1_{𝑜} mPoly R \in Ring$
50	12 49	mpan	$⊢ R \in Ring \to 1_{𝑜} mPoly R \in Ring$
51	22	ringmgp	$⊢ 1_{𝑜} mPoly R \in Ring \to {mulGrp}_{(1_{𝑜} mPoly R)} \in Mnd$
52	50 51	syl	$⊢ R \in Ring \to {mulGrp}_{(1_{𝑜} mPoly R)} \in Mnd$
53	52	ad2antrr	$⊢ ((R \in Ring \land K \in B) \land a \in ({ℕ_{0}}^{1_{𝑜}})) \to {mulGrp}_{(1_{𝑜} mPoly R)} \in Mnd$
54	28	a1i	$⊢ ((R \in Ring \land K \in B) \land a \in ({ℕ_{0}}^{1_{𝑜}})) \to \emptyset \in V$
55	22 14	mgpbas	$⊢ B = {Base}_{{mulGrp}_{(1_{𝑜} mPoly R)}}$
56	55	a1i	$⊢ (R \in Ring \land K \in B) \to B = {Base}_{{mulGrp}_{(1_{𝑜} mPoly R)}}$
57	5 3	mgpbas	$⊢ B = {Base}_{M}$
58	57	a1i	$⊢ (R \in Ring \land K \in B) \to B = {Base}_{M}$
59		ssv	$⊢ B \subseteq V$
60	59	a1i	$⊢ (R \in Ring \land K \in B) \to B \subseteq V$
61		ovexd	$⊢ ((R \in Ring \land K \in B) \land (a \in V \land b \in V)) \to a +_{{mulGrp}_{(1_{𝑜} mPoly R)}} b \in V$
62		eqid	$⊢ \cdot_{P} = \cdot_{P}$
63	1 8 62	ply1mulr	$⊢ \cdot_{P} = \cdot_{(1_{𝑜} mPoly R)}$
64	22 63	mgpplusg	$⊢ \cdot_{P} = +_{{mulGrp}_{(1_{𝑜} mPoly R)}}$
65	5 62	mgpplusg	$⊢ \cdot_{P} = +_{M}$
66	64 65	eqtr3i	$⊢ +_{{mulGrp}_{(1_{𝑜} mPoly R)}} = +_{M}$
67	66	oveqi	$⊢ a +_{{mulGrp}_{(1_{𝑜} mPoly R)}} b = a +_{M} b$
68	67	a1i	$⊢ ((R \in Ring \land K \in B) \land (a \in V \land b \in V)) \to a +_{{mulGrp}_{(1_{𝑜} mPoly R)}} b = a +_{M} b$
69	23 6 56 58 60 61 68	mulgpropd	$⊢ (R \in Ring \land K \in B) \to \cdot_{{mulGrp}_{(1_{𝑜} mPoly R)}} = \underset{˙}{\times}$
70	69	oveqd	$⊢ (R \in Ring \land K \in B) \to a (\emptyset) \cdot_{{mulGrp}_{(1_{𝑜} mPoly R)}} X = a (\emptyset) \underset{˙}{\times} X$
71	70	adantr	$⊢ ((R \in Ring \land K \in B) \land a \in ({ℕ_{0}}^{1_{𝑜}})) \to a (\emptyset) \cdot_{{mulGrp}_{(1_{𝑜} mPoly R)}} X = a (\emptyset) \underset{˙}{\times} X$
72	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
73	5	ringmgp	$⊢ P \in Ring \to M \in Mnd$
74	72 73	syl	$⊢ R \in Ring \to M \in Mnd$
75	74	ad2antrr	$⊢ ((R \in Ring \land K \in B) \land a \in ({ℕ_{0}}^{1_{𝑜}})) \to M \in Mnd$
76		elmapi	$⊢ a \in ({ℕ_{0}}^{1_{𝑜}}) \to a : 1_{𝑜} ⟶ ℕ_{0}$
77		0lt1o	$⊢ \emptyset \in 1_{𝑜}$
78		ffvelcdm	$⊢ (a : 1_{𝑜} ⟶ ℕ_{0} \land \emptyset \in 1_{𝑜}) \to a (\emptyset) \in ℕ_{0}$
79	76 77 78	sylancl	$⊢ a \in ({ℕ_{0}}^{1_{𝑜}}) \to a (\emptyset) \in ℕ_{0}$
80	79	adantl	$⊢ ((R \in Ring \land K \in B) \land a \in ({ℕ_{0}}^{1_{𝑜}})) \to a (\emptyset) \in ℕ_{0}$
81	2 1 3	vr1cl	$⊢ R \in Ring \to X \in B$
82	81	ad2antrr	$⊢ ((R \in Ring \land K \in B) \land a \in ({ℕ_{0}}^{1_{𝑜}})) \to X \in B$
83	57 6 75 80 82	mulgnn0cld	$⊢ ((R \in Ring \land K \in B) \land a \in ({ℕ_{0}}^{1_{𝑜}})) \to a (\emptyset) \underset{˙}{\times} X \in B$
84	71 83	eqeltrd	$⊢ ((R \in Ring \land K \in B) \land a \in ({ℕ_{0}}^{1_{𝑜}})) \to a (\emptyset) \cdot_{{mulGrp}_{(1_{𝑜} mPoly R)}} X \in B$
85		fveq2	$⊢ c = \emptyset \to a (c) = a (\emptyset)$
86		fveq2	$⊢ c = \emptyset \to (1_{𝑜} mVar R) (c) = (1_{𝑜} mVar R) (\emptyset)$
87	2	vr1val	$⊢ X = (1_{𝑜} mVar R) (\emptyset)$
88	86 87	eqtr4di	$⊢ c = \emptyset \to (1_{𝑜} mVar R) (c) = X$
89	85 88	oveq12d	$⊢ c = \emptyset \to a (c) \cdot_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (c) = a (\emptyset) \cdot_{{mulGrp}_{(1_{𝑜} mPoly R)}} X$
90	55 89	gsumsn	$⊢ ({mulGrp}_{(1_{𝑜} mPoly R)} \in Mnd \land \emptyset \in V \land a (\emptyset) \cdot_{{mulGrp}_{(1_{𝑜} mPoly R)}} X \in B) \to \underset{c \in \{\emptyset\}}{\sum_{{mulGrp}_{(1_{𝑜} mPoly R)}}} (a (c) \cdot_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (c)) = a (\emptyset) \cdot_{{mulGrp}_{(1_{𝑜} mPoly R)}} X$
91	53 54 84 90	syl3anc	$⊢ ((R \in Ring \land K \in B) \land a \in ({ℕ_{0}}^{1_{𝑜}})) \to \underset{c \in \{\emptyset\}}{\sum_{{mulGrp}_{(1_{𝑜} mPoly R)}}} (a (c) \cdot_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (c)) = a (\emptyset) \cdot_{{mulGrp}_{(1_{𝑜} mPoly R)}} X$
92	48 91	eqtrid	$⊢ ((R \in Ring \land K \in B) \land a \in ({ℕ_{0}}^{1_{𝑜}})) \to \underset{c \in 1_{𝑜}}{\sum_{{mulGrp}_{(1_{𝑜} mPoly R)}}} (a (c) \cdot_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (c)) = a (\emptyset) \cdot_{{mulGrp}_{(1_{𝑜} mPoly R)}} X$
93	46 92 71	3eqtrd	$⊢ ((R \in Ring \land K \in B) \land a \in ({ℕ_{0}}^{1_{𝑜}})) \to (b \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ if (b = a, 1_{R}, 0_{R})) = a (\emptyset) \underset{˙}{\times} X$
94	20 93	oveq12d	$⊢ ((R \in Ring \land K \in B) \land a \in ({ℕ_{0}}^{1_{𝑜}})) \to K (a) \underset{˙}{\cdot} (b \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ if (b = a, 1_{R}, 0_{R})) = A (a (\emptyset)) \underset{˙}{\cdot} (a (\emptyset) \underset{˙}{\times} X)$
95	94	mpteq2dva	$⊢ (R \in Ring \land K \in B) \to (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ K (a) \underset{˙}{\cdot} (b \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ if (b = a, 1_{R}, 0_{R}))) = (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ A (a (\emptyset)) \underset{˙}{\cdot} (a (\emptyset) \underset{˙}{\times} X))$
96	95	oveq2d	$⊢ (R \in Ring \land K \in B) \to \underset{a \in {ℕ_{0}}^{1_{𝑜}}}{\sum_{1_{𝑜} mPoly R}} (K (a) \underset{˙}{\cdot} (b \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ if (b = a, 1_{R}, 0_{R}))) = \underset{a \in {ℕ_{0}}^{1_{𝑜}}}{\sum_{1_{𝑜} mPoly R}} (A (a (\emptyset)) \underset{˙}{\cdot} (a (\emptyset) \underset{˙}{\times} X))$
97		nn0ex	$⊢ ℕ_{0} \in V$
98	97	mptex	$⊢ (k \in ℕ_{0} ⟼ A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X)) \in V$
99	98	a1i	$⊢ (R \in Ring \land K \in B) \to (k \in ℕ_{0} ⟼ A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X)) \in V$
100	1	fvexi	$⊢ P \in V$
101	100	a1i	$⊢ (R \in Ring \land K \in B) \to P \in V$
102		ovexd	$⊢ (R \in Ring \land K \in B) \to 1_{𝑜} mPoly R \in V$
103	3 14	eqtr3i	$⊢ {Base}_{P} = {Base}_{(1_{𝑜} mPoly R)}$
104	103	a1i	$⊢ (R \in Ring \land K \in B) \to {Base}_{P} = {Base}_{(1_{𝑜} mPoly R)}$
105		eqid	$⊢ +_{P} = +_{P}$
106	1 8 105	ply1plusg	$⊢ +_{P} = +_{(1_{𝑜} mPoly R)}$
107	106	a1i	$⊢ (R \in Ring \land K \in B) \to +_{P} = +_{(1_{𝑜} mPoly R)}$
108	99 101 102 104 107	gsumpropd	$⊢ (R \in Ring \land K \in B) \to \underset{k \in ℕ_{0}}{\sum_{P}} (A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X)) = \underset{k \in ℕ_{0}}{\sum_{1_{𝑜} mPoly R}} (A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X))$
109		eqid	$⊢ 0_{P} = 0_{P}$
110	8 1 109	ply1mpl0	$⊢ 0_{P} = 0_{(1_{𝑜} mPoly R)}$
111	8	mpllmod	$⊢ (1_{𝑜} \in ω \land R \in Ring) \to 1_{𝑜} mPoly R \in LMod$
112	12 16 111	sylancr	$⊢ (R \in Ring \land K \in B) \to 1_{𝑜} mPoly R \in LMod$
113		lmodcmn	$⊢ 1_{𝑜} mPoly R \in LMod \to 1_{𝑜} mPoly R \in CMnd$
114	112 113	syl	$⊢ (R \in Ring \land K \in B) \to 1_{𝑜} mPoly R \in CMnd$
115	97	a1i	$⊢ (R \in Ring \land K \in B) \to ℕ_{0} \in V$
116	1	ply1lmod	$⊢ R \in Ring \to P \in LMod$
117	116	ad2antrr	$⊢ ((R \in Ring \land K \in B) \land k \in ℕ_{0}) \to P \in LMod$
118		eqid	$⊢ {Base}_{R} = {Base}_{R}$
119	7 3 1 118	coe1f	$⊢ K \in B \to A : ℕ_{0} ⟶ {Base}_{R}$
120	119	adantl	$⊢ (R \in Ring \land K \in B) \to A : ℕ_{0} ⟶ {Base}_{R}$
121	120	ffvelcdmda	$⊢ ((R \in Ring \land K \in B) \land k \in ℕ_{0}) \to A (k) \in {Base}_{R}$
122	1	ply1sca	$⊢ R \in Ring \to R = Scalar (P)$
123	122	eqcomd	$⊢ R \in Ring \to Scalar (P) = R$
124	123	ad2antrr	$⊢ ((R \in Ring \land K \in B) \land k \in ℕ_{0}) \to Scalar (P) = R$
125	124	fveq2d	$⊢ ((R \in Ring \land K \in B) \land k \in ℕ_{0}) \to {Base}_{Scalar (P)} = {Base}_{R}$
126	121 125	eleqtrrd	$⊢ ((R \in Ring \land K \in B) \land k \in ℕ_{0}) \to A (k) \in {Base}_{Scalar (P)}$
127	74	ad2antrr	$⊢ ((R \in Ring \land K \in B) \land k \in ℕ_{0}) \to M \in Mnd$
128		simpr	$⊢ ((R \in Ring \land K \in B) \land k \in ℕ_{0}) \to k \in ℕ_{0}$
129	81	ad2antrr	$⊢ ((R \in Ring \land K \in B) \land k \in ℕ_{0}) \to X \in B$
130	57 6 127 128 129	mulgnn0cld	$⊢ ((R \in Ring \land K \in B) \land k \in ℕ_{0}) \to k \underset{˙}{\times} X \in B$
131		eqid	$⊢ Scalar (P) = Scalar (P)$
132		eqid	$⊢ {Base}_{Scalar (P)} = {Base}_{Scalar (P)}$
133	3 131 4 132	lmodvscl	$⊢ (P \in LMod \land A (k) \in {Base}_{Scalar (P)} \land k \underset{˙}{\times} X \in B) \to A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X) \in B$
134	117 126 130 133	syl3anc	$⊢ ((R \in Ring \land K \in B) \land k \in ℕ_{0}) \to A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X) \in B$
135	134	fmpttd	$⊢ (R \in Ring \land K \in B) \to (k \in ℕ_{0} ⟼ A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X)) : ℕ_{0} ⟶ B$
136	1 2 3 4 5 6 7	ply1coefsupp	$⊢ (R \in Ring \land K \in B) \to {finSupp}_{0_{P}} ((k \in ℕ_{0} ⟼ A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X)))$
137		eqid	$⊢ (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) = (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset))$
138	42 97 28 137	mapsnf1o2	$⊢ (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) : {ℕ_{0}}^{1_{𝑜}} \underset{1-1 onto}{⟶} ℕ_{0}$
139	138	a1i	$⊢ (R \in Ring \land K \in B) \to (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) : {ℕ_{0}}^{1_{𝑜}} \underset{1-1 onto}{⟶} ℕ_{0}$
140	14 110 114 115 135 136 139	gsumf1o	$⊢ (R \in Ring \land K \in B) \to \underset{k \in ℕ_{0}}{\sum_{1_{𝑜} mPoly R}} (A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X)) = \sum_{1_{𝑜} mPoly R} ((k \in ℕ_{0} ⟼ A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X)) \circ (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)))$
141		eqidd	$⊢ (R \in Ring \land K \in B) \to (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) = (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset))$
142		eqidd	$⊢ (R \in Ring \land K \in B) \to (k \in ℕ_{0} ⟼ A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X)) = (k \in ℕ_{0} ⟼ A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X))$
143		fveq2	$⊢ k = a (\emptyset) \to A (k) = A (a (\emptyset))$
144		oveq1	$⊢ k = a (\emptyset) \to k \underset{˙}{\times} X = a (\emptyset) \underset{˙}{\times} X$
145	143 144	oveq12d	$⊢ k = a (\emptyset) \to A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X) = A (a (\emptyset)) \underset{˙}{\cdot} (a (\emptyset) \underset{˙}{\times} X)$
146	80 141 142 145	fmptco	$⊢ (R \in Ring \land K \in B) \to (k \in ℕ_{0} ⟼ A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X)) \circ (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) = (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ A (a (\emptyset)) \underset{˙}{\cdot} (a (\emptyset) \underset{˙}{\times} X))$
147	146	oveq2d	$⊢ (R \in Ring \land K \in B) \to \sum_{1_{𝑜} mPoly R} ((k \in ℕ_{0} ⟼ A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X)) \circ (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset))) = \underset{a \in {ℕ_{0}}^{1_{𝑜}}}{\sum_{1_{𝑜} mPoly R}} (A (a (\emptyset)) \underset{˙}{\cdot} (a (\emptyset) \underset{˙}{\times} X))$
148	108 140 147	3eqtrrd	$⊢ (R \in Ring \land K \in B) \to \underset{a \in {ℕ_{0}}^{1_{𝑜}}}{\sum_{1_{𝑜} mPoly R}} (A (a (\emptyset)) \underset{˙}{\cdot} (a (\emptyset) \underset{˙}{\times} X)) = \underset{k \in ℕ_{0}}{\sum_{P}} (A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X))$
149	18 96 148	3eqtrd	$⊢ (R \in Ring \land K \in B) \to K = \underset{k \in ℕ_{0}}{\sum_{P}} (A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X))$

Metamath Proof Explorer

Theorem ply1coe

Proof