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