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		ffvelrn	$⊢ (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	mulgnn0cl	$⊢ (M \in Mnd \land a (\emptyset) \in ℕ_{0} \land X \in B) \to a (\emptyset) \underset{˙}{\times} X \in B$
85	76 81 83 84	syl3anc	$⊢ ((R \in Ring \land K \in B) \land a \in ({ℕ_{0}}^{1_{𝑜}})) \to a (\emptyset) \underset{˙}{\times} X \in B$
86	72 85	eqeltrd	$⊢ ((R \in Ring \land K \in B) \land a \in ({ℕ_{0}}^{1_{𝑜}})) \to a (\emptyset) \cdot_{{mulGrp}_{(1_{𝑜} mPoly R)}} X \in B$
87		fveq2	$⊢ c = \emptyset \to a (c) = a (\emptyset)$
88		fveq2	$⊢ c = \emptyset \to (1_{𝑜} mVar R) (c) = (1_{𝑜} mVar R) (\emptyset)$
89	2	vr1val	$⊢ X = (1_{𝑜} mVar R) (\emptyset)$
90	88 89	eqtr4di	$⊢ c = \emptyset \to (1_{𝑜} mVar R) (c) = X$
91	87 90	oveq12d	$⊢ c = \emptyset \to a (c) \cdot_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (c) = a (\emptyset) \cdot_{{mulGrp}_{(1_{𝑜} mPoly R)}} X$
92	56 91	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$
93	54 55 86 92	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$
94	49 93	syl5eq	$⊢ ((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$
95	47 94 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$
96	21 95	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)$
97	96	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))$
98	97	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))$
99		nn0ex	$⊢ ℕ_{0} \in V$
100	99	mptex	$⊢ (k \in ℕ_{0} ⟼ A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X)) \in V$
101	100	a1i	$⊢ (R \in Ring \land K \in B) \to (k \in ℕ_{0} ⟼ A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X)) \in V$
102	1	fvexi	$⊢ P \in V$
103	102	a1i	$⊢ (R \in Ring \land K \in B) \to P \in V$
104		ovexd	$⊢ (R \in Ring \land K \in B) \to 1_{𝑜} mPoly R \in V$
105	3 15	eqtr3i	$⊢ {Base}_{P} = {Base}_{(1_{𝑜} mPoly R)}$
106	105	a1i	$⊢ (R \in Ring \land K \in B) \to {Base}_{P} = {Base}_{(1_{𝑜} mPoly R)}$
107		eqid	$⊢ +_{P} = +_{P}$
108	1 8 107	ply1plusg	$⊢ +_{P} = +_{(1_{𝑜} mPoly R)}$
109	108	a1i	$⊢ (R \in Ring \land K \in B) \to +_{P} = +_{(1_{𝑜} mPoly R)}$
110	101 103 104 106 109	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))$
111		eqid	$⊢ 0_{P} = 0_{P}$
112	8 1 111	ply1mpl0	$⊢ 0_{P} = 0_{(1_{𝑜} mPoly R)}$
113	8	mpllmod	$⊢ (1_{𝑜} \in ω \land R \in Ring) \to 1_{𝑜} mPoly R \in LMod$
114	12 17 113	sylancr	$⊢ (R \in Ring \land K \in B) \to 1_{𝑜} mPoly R \in LMod$
115		lmodcmn	$⊢ 1_{𝑜} mPoly R \in LMod \to 1_{𝑜} mPoly R \in CMnd$
116	114 115	syl	$⊢ (R \in Ring \land K \in B) \to 1_{𝑜} mPoly R \in CMnd$
117	99	a1i	$⊢ (R \in Ring \land K \in B) \to ℕ_{0} \in V$
118	1	ply1lmod	$⊢ R \in Ring \to P \in LMod$
119	118	ad2antrr	$⊢ ((R \in Ring \land K \in B) \land k \in ℕ_{0}) \to P \in LMod$
120		eqid	$⊢ {Base}_{R} = {Base}_{R}$
121	7 3 1 120	coe1f	$⊢ K \in B \to A : ℕ_{0} ⟶ {Base}_{R}$
122	121	adantl	$⊢ (R \in Ring \land K \in B) \to A : ℕ_{0} ⟶ {Base}_{R}$
123	122	ffvelrnda	$⊢ ((R \in Ring \land K \in B) \land k \in ℕ_{0}) \to A (k) \in {Base}_{R}$
124	1	ply1sca	$⊢ R \in Ring \to R = Scalar (P)$
125	124	eqcomd	$⊢ R \in Ring \to Scalar (P) = R$
126	125	ad2antrr	$⊢ ((R \in Ring \land K \in B) \land k \in ℕ_{0}) \to Scalar (P) = R$
127	126	fveq2d	$⊢ ((R \in Ring \land K \in B) \land k \in ℕ_{0}) \to {Base}_{Scalar (P)} = {Base}_{R}$
128	123 127	eleqtrrd	$⊢ ((R \in Ring \land K \in B) \land k \in ℕ_{0}) \to A (k) \in {Base}_{Scalar (P)}$
129	75	ad2antrr	$⊢ ((R \in Ring \land K \in B) \land k \in ℕ_{0}) \to M \in Mnd$
130		simpr	$⊢ ((R \in Ring \land K \in B) \land k \in ℕ_{0}) \to k \in ℕ_{0}$
131	82	ad2antrr	$⊢ ((R \in Ring \land K \in B) \land k \in ℕ_{0}) \to X \in B$
132	58 6	mulgnn0cl	$⊢ (M \in Mnd \land k \in ℕ_{0} \land X \in B) \to k \underset{˙}{\times} X \in B$
133	129 130 131 132	syl3anc	$⊢ ((R \in Ring \land K \in B) \land k \in ℕ_{0}) \to k \underset{˙}{\times} X \in B$
134		eqid	$⊢ Scalar (P) = Scalar (P)$
135		eqid	$⊢ {Base}_{Scalar (P)} = {Base}_{Scalar (P)}$
136	3 134 4 135	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$
137	119 128 133 136	syl3anc	$⊢ ((R \in Ring \land K \in B) \land k \in ℕ_{0}) \to A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X) \in B$
138	137	fmpttd	$⊢ (R \in Ring \land K \in B) \to (k \in ℕ_{0} ⟼ A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X)) : ℕ_{0} ⟶ B$
139	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)))$
140		eqid	$⊢ (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) = (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset))$
141	43 99 29 140	mapsnf1o2	$⊢ (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) : {ℕ_{0}}^{1_{𝑜}} \underset{1-1 onto}{⟶} ℕ_{0}$
142	141	a1i	$⊢ (R \in Ring \land K \in B) \to (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) : {ℕ_{0}}^{1_{𝑜}} \underset{1-1 onto}{⟶} ℕ_{0}$
143	15 112 116 117 138 139 142	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)))$
144		eqidd	$⊢ (R \in Ring \land K \in B) \to (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) = (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset))$
145		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))$
146		fveq2	$⊢ k = a (\emptyset) \to A (k) = A (a (\emptyset))$
147		oveq1	$⊢ k = a (\emptyset) \to k \underset{˙}{\times} X = a (\emptyset) \underset{˙}{\times} X$
148	146 147	oveq12d	$⊢ k = a (\emptyset) \to A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X) = A (a (\emptyset)) \underset{˙}{\cdot} (a (\emptyset) \underset{˙}{\times} X)$
149	81 144 145 148	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))$
150	149	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))$
151	110 143 150	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))$
152	19 98 151	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