# Metamath Proof Explorer

## Theorem 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
ply1coe.m $⊢ M = mulGrp P$
ply1coe.e
ply1coe.a $⊢ A = coe 1 ⁡ K$
Assertion ply1coe

### 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
5 ply1coe.m $⊢ M = mulGrp P$
6 ply1coe.e
7 ply1coe.a $⊢ A = coe 1 ⁡ K$
8 eqid $⊢ 1 𝑜 mPoly R = 1 𝑜 mPoly R$
9 psr1baslem $⊢ ℕ 0 1 𝑜 = d ∈ ℕ 0 1 𝑜 | d -1 ℕ ∈ Fin$
10 eqid $⊢ 0 R = 0 R$
11 eqid $⊢ 1 R = 1 R$
12 1onn $⊢ 1 𝑜 ∈ ω$
13 12 a1i $⊢ R ∈ Ring ∧ K ∈ B → 1 𝑜 ∈ ω$
14 eqid $⊢ PwSer 1 ⁡ R = PwSer 1 ⁡ R$
15 1 14 3 ply1bas $⊢ B = Base 1 𝑜 mPoly R$
16 1 8 4 ply1vsca
17 simpl $⊢ R ∈ Ring ∧ K ∈ B → R ∈ Ring$
18 simpr $⊢ R ∈ Ring ∧ K ∈ B → K ∈ B$
19 8 9 10 11 13 15 16 17 18 mplcoe1
20 7 fvcoe1 $⊢ K ∈ B ∧ a ∈ ℕ 0 1 𝑜 → K ⁡ a = A ⁡ a ⁡ ∅$
21 20 adantll $⊢ R ∈ Ring ∧ K ∈ B ∧ a ∈ ℕ 0 1 𝑜 → K ⁡ a = A ⁡ a ⁡ ∅$
22 12 a1i $⊢ R ∈ Ring ∧ K ∈ B ∧ a ∈ ℕ 0 1 𝑜 → 1 𝑜 ∈ ω$
23 eqid $⊢ mulGrp 1 𝑜 mPoly R = mulGrp 1 𝑜 mPoly R$
24 eqid $⊢ ⋅ mulGrp 1 𝑜 mPoly R = ⋅ mulGrp 1 𝑜 mPoly R$
25 eqid $⊢ 1 𝑜 mVar R = 1 𝑜 mVar R$
26 simpll $⊢ R ∈ Ring ∧ K ∈ B ∧ a ∈ ℕ 0 1 𝑜 → R ∈ Ring$
27 simpr $⊢ R ∈ Ring ∧ K ∈ B ∧ a ∈ ℕ 0 1 𝑜 → a ∈ ℕ 0 1 𝑜$
28 eqidd $⊢ R ∈ Ring ∧ K ∈ B ∧ a ∈ ℕ 0 1 𝑜 → 1 𝑜 mVar R ⁡ ∅ + mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ ∅ = 1 𝑜 mVar R ⁡ ∅ + mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ ∅$
29 0ex $⊢ ∅ ∈ V$
30 fveq2 $⊢ b = ∅ → 1 𝑜 mVar R ⁡ b = 1 𝑜 mVar R ⁡ ∅$
31 30 oveq1d $⊢ b = ∅ → 1 𝑜 mVar R ⁡ b + mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ ∅ = 1 𝑜 mVar R ⁡ ∅ + mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ ∅$
32 30 oveq2d $⊢ b = ∅ → 1 𝑜 mVar R ⁡ ∅ + mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ b = 1 𝑜 mVar R ⁡ ∅ + mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ ∅$
33 31 32 eqeq12d $⊢ b = ∅ → 1 𝑜 mVar R ⁡ b + mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ ∅ = 1 𝑜 mVar R ⁡ ∅ + mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ b ↔ 1 𝑜 mVar R ⁡ ∅ + mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ ∅ = 1 𝑜 mVar R ⁡ ∅ + mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ ∅$
34 29 33 ralsn $⊢ ∀ b ∈ ∅ 1 𝑜 mVar R ⁡ b + mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ ∅ = 1 𝑜 mVar R ⁡ ∅ + mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ b ↔ 1 𝑜 mVar R ⁡ ∅ + mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ ∅ = 1 𝑜 mVar R ⁡ ∅ + mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ ∅$
35 28 34 sylibr $⊢ R ∈ Ring ∧ K ∈ B ∧ a ∈ ℕ 0 1 𝑜 → ∀ b ∈ ∅ 1 𝑜 mVar R ⁡ b + mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ ∅ = 1 𝑜 mVar R ⁡ ∅ + mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ b$
36 fveq2 $⊢ x = ∅ → 1 𝑜 mVar R ⁡ x = 1 𝑜 mVar R ⁡ ∅$
37 36 oveq2d $⊢ x = ∅ → 1 𝑜 mVar R ⁡ b + mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ x = 1 𝑜 mVar R ⁡ b + mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ ∅$
38 36 oveq1d $⊢ x = ∅ → 1 𝑜 mVar R ⁡ x + mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ b = 1 𝑜 mVar R ⁡ ∅ + mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ b$
39 37 38 eqeq12d $⊢ x = ∅ → 1 𝑜 mVar R ⁡ b + mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ x = 1 𝑜 mVar R ⁡ x + mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ b ↔ 1 𝑜 mVar R ⁡ b + mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ ∅ = 1 𝑜 mVar R ⁡ ∅ + mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ b$
40 39 ralbidv $⊢ x = ∅ → ∀ b ∈ ∅ 1 𝑜 mVar R ⁡ b + mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ x = 1 𝑜 mVar R ⁡ x + mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ b ↔ ∀ b ∈ ∅ 1 𝑜 mVar R ⁡ b + mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ ∅ = 1 𝑜 mVar R ⁡ ∅ + mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ b$
41 29 40 ralsn $⊢ ∀ x ∈ ∅ ∀ b ∈ ∅ 1 𝑜 mVar R ⁡ b + mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ x = 1 𝑜 mVar R ⁡ x + mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ b ↔ ∀ b ∈ ∅ 1 𝑜 mVar R ⁡ b + mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ ∅ = 1 𝑜 mVar R ⁡ ∅ + mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ b$
42 35 41 sylibr $⊢ R ∈ Ring ∧ K ∈ B ∧ a ∈ ℕ 0 1 𝑜 → ∀ x ∈ ∅ ∀ b ∈ ∅ 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 𝑜 = ∅$
44 43 raleqi $⊢ ∀ b ∈ 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 ↔ ∀ b ∈ ∅ 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 $⊢ ∀ x ∈ 1 𝑜 ∀ b ∈ 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 ↔ ∀ x ∈ ∅ ∀ b ∈ ∅ 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 ∈ Ring ∧ K ∈ B ∧ a ∈ ℕ 0 1 𝑜 → ∀ x ∈ 1 𝑜 ∀ b ∈ 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 ∈ Ring ∧ K ∈ B ∧ a ∈ ℕ 0 1 𝑜 → b ∈ ℕ 0 1 𝑜 ⟼ if b = a 1 R 0 R = ∑ mulGrp 1 𝑜 mPoly R c ∈ 1 𝑜 a ⁡ c ⋅ mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ c$
48 43 mpteq1i $⊢ c ∈ 1 𝑜 ⟼ a ⁡ c ⋅ mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ c = c ∈ ∅ ⟼ a ⁡ c ⋅ mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ c$
49 48 oveq2i $⊢ ∑ mulGrp 1 𝑜 mPoly R c ∈ 1 𝑜 a ⁡ c ⋅ mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ c = ∑ mulGrp 1 𝑜 mPoly R c ∈ ∅ a ⁡ c ⋅ mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ c$
50 8 mplring $⊢ 1 𝑜 ∈ ω ∧ R ∈ Ring → 1 𝑜 mPoly R ∈ Ring$
51 12 50 mpan $⊢ R ∈ Ring → 1 𝑜 mPoly R ∈ Ring$
52 23 ringmgp $⊢ 1 𝑜 mPoly R ∈ Ring → mulGrp 1 𝑜 mPoly R ∈ Mnd$
53 51 52 syl $⊢ R ∈ Ring → mulGrp 1 𝑜 mPoly R ∈ Mnd$
54 53 ad2antrr $⊢ R ∈ Ring ∧ K ∈ B ∧ a ∈ ℕ 0 1 𝑜 → mulGrp 1 𝑜 mPoly R ∈ Mnd$
55 29 a1i $⊢ R ∈ Ring ∧ K ∈ B ∧ a ∈ ℕ 0 1 𝑜 → ∅ ∈ V$
56 23 15 mgpbas $⊢ B = Base mulGrp 1 𝑜 mPoly R$
57 56 a1i $⊢ R ∈ Ring ∧ K ∈ B → B = Base mulGrp 1 𝑜 mPoly R$
58 5 3 mgpbas $⊢ B = Base M$
59 58 a1i $⊢ R ∈ Ring ∧ K ∈ B → B = Base M$
60 ssv $⊢ B ⊆ V$
61 60 a1i $⊢ R ∈ Ring ∧ K ∈ B → B ⊆ V$
62 ovexd $⊢ R ∈ Ring ∧ K ∈ B ∧ a ∈ V ∧ b ∈ V → a + mulGrp 1 𝑜 mPoly R b ∈ V$
63 eqid $⊢ ⋅ P = ⋅ P$
64 1 8 63 ply1mulr $⊢ ⋅ P = ⋅ 1 𝑜 mPoly R$
65 23 64 mgpplusg $⊢ ⋅ P = + mulGrp 1 𝑜 mPoly R$
66 5 63 mgpplusg $⊢ ⋅ 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 ∈ Ring ∧ K ∈ B ∧ a ∈ V ∧ b ∈ V → a + mulGrp 1 𝑜 mPoly R b = a + M b$
70 24 6 57 59 61 62 69 mulgpropd
71 70 oveqd
73 1 ply1ring $⊢ R ∈ Ring → P ∈ Ring$
74 5 ringmgp $⊢ P ∈ Ring → M ∈ Mnd$
75 73 74 syl $⊢ R ∈ Ring → M ∈ Mnd$
76 75 ad2antrr $⊢ R ∈ Ring ∧ K ∈ B ∧ a ∈ ℕ 0 1 𝑜 → M ∈ Mnd$
77 elmapi $⊢ a ∈ ℕ 0 1 𝑜 → a : 1 𝑜 ⟶ ℕ 0$
78 0lt1o $⊢ ∅ ∈ 1 𝑜$
79 ffvelrn $⊢ a : 1 𝑜 ⟶ ℕ 0 ∧ ∅ ∈ 1 𝑜 → a ⁡ ∅ ∈ ℕ 0$
80 77 78 79 sylancl $⊢ a ∈ ℕ 0 1 𝑜 → a ⁡ ∅ ∈ ℕ 0$
81 80 adantl $⊢ R ∈ Ring ∧ K ∈ B ∧ a ∈ ℕ 0 1 𝑜 → a ⁡ ∅ ∈ ℕ 0$
82 2 1 3 vr1cl $⊢ R ∈ Ring → X ∈ B$
83 82 ad2antrr $⊢ R ∈ Ring ∧ K ∈ B ∧ a ∈ ℕ 0 1 𝑜 → X ∈ B$
84 58 6 mulgnn0cl
85 76 81 83 84 syl3anc
86 72 85 eqeltrd $⊢ R ∈ Ring ∧ K ∈ B ∧ a ∈ ℕ 0 1 𝑜 → a ⁡ ∅ ⋅ mulGrp 1 𝑜 mPoly R X ∈ B$
87 fveq2 $⊢ c = ∅ → a ⁡ c = a ⁡ ∅$
88 fveq2 $⊢ c = ∅ → 1 𝑜 mVar R ⁡ c = 1 𝑜 mVar R ⁡ ∅$
89 2 vr1val $⊢ X = 1 𝑜 mVar R ⁡ ∅$
90 88 89 eqtr4di $⊢ c = ∅ → 1 𝑜 mVar R ⁡ c = X$
91 87 90 oveq12d $⊢ c = ∅ → a ⁡ c ⋅ mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ c = a ⁡ ∅ ⋅ mulGrp 1 𝑜 mPoly R X$
92 56 91 gsumsn $⊢ mulGrp 1 𝑜 mPoly R ∈ Mnd ∧ ∅ ∈ V ∧ a ⁡ ∅ ⋅ mulGrp 1 𝑜 mPoly R X ∈ B → ∑ mulGrp 1 𝑜 mPoly R c ∈ ∅ a ⁡ c ⋅ mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ c = a ⁡ ∅ ⋅ mulGrp 1 𝑜 mPoly R X$
93 54 55 86 92 syl3anc $⊢ R ∈ Ring ∧ K ∈ B ∧ a ∈ ℕ 0 1 𝑜 → ∑ mulGrp 1 𝑜 mPoly R c ∈ ∅ a ⁡ c ⋅ mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ c = a ⁡ ∅ ⋅ mulGrp 1 𝑜 mPoly R X$
94 49 93 syl5eq $⊢ R ∈ Ring ∧ K ∈ B ∧ a ∈ ℕ 0 1 𝑜 → ∑ mulGrp 1 𝑜 mPoly R c ∈ 1 𝑜 a ⁡ c ⋅ mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R ⁡ c = a ⁡ ∅ ⋅ mulGrp 1 𝑜 mPoly R X$
95 47 94 72 3eqtrd
96 21 95 oveq12d
97 96 mpteq2dva
98 97 oveq2d
99 nn0ex $⊢ ℕ 0 ∈ V$
100 99 mptex
101 100 a1i
102 1 fvexi $⊢ P ∈ V$
103 102 a1i $⊢ R ∈ Ring ∧ K ∈ B → P ∈ V$
104 ovexd $⊢ R ∈ Ring ∧ K ∈ B → 1 𝑜 mPoly R ∈ V$
105 3 15 eqtr3i $⊢ Base P = Base 1 𝑜 mPoly R$
106 105 a1i $⊢ R ∈ Ring ∧ K ∈ B → Base P = Base 1 𝑜 mPoly R$
107 eqid $⊢ + P = + P$
108 1 8 107 ply1plusg $⊢ + P = + 1 𝑜 mPoly R$
109 108 a1i $⊢ R ∈ Ring ∧ K ∈ B → + P = + 1 𝑜 mPoly R$
110 101 103 104 106 109 gsumpropd
111 eqid $⊢ 0 P = 0 P$
112 8 1 111 ply1mpl0 $⊢ 0 P = 0 1 𝑜 mPoly R$
113 8 mpllmod $⊢ 1 𝑜 ∈ ω ∧ R ∈ Ring → 1 𝑜 mPoly R ∈ LMod$
114 12 17 113 sylancr $⊢ R ∈ Ring ∧ K ∈ B → 1 𝑜 mPoly R ∈ LMod$
115 lmodcmn $⊢ 1 𝑜 mPoly R ∈ LMod → 1 𝑜 mPoly R ∈ CMnd$
116 114 115 syl $⊢ R ∈ Ring ∧ K ∈ B → 1 𝑜 mPoly R ∈ CMnd$
117 99 a1i $⊢ R ∈ Ring ∧ K ∈ B → ℕ 0 ∈ V$
118 1 ply1lmod $⊢ R ∈ Ring → P ∈ LMod$
119 118 ad2antrr $⊢ R ∈ Ring ∧ K ∈ B ∧ k ∈ ℕ 0 → P ∈ LMod$
120 eqid $⊢ Base R = Base R$
121 7 3 1 120 coe1f $⊢ K ∈ B → A : ℕ 0 ⟶ Base R$
122 121 adantl $⊢ R ∈ Ring ∧ K ∈ B → A : ℕ 0 ⟶ Base R$
123 122 ffvelrnda $⊢ R ∈ Ring ∧ K ∈ B ∧ k ∈ ℕ 0 → A ⁡ k ∈ Base R$
124 1 ply1sca $⊢ R ∈ Ring → R = Scalar ⁡ P$
125 124 eqcomd $⊢ R ∈ Ring → Scalar ⁡ P = R$
126 125 ad2antrr $⊢ R ∈ Ring ∧ K ∈ B ∧ k ∈ ℕ 0 → Scalar ⁡ P = R$
127 126 fveq2d $⊢ R ∈ Ring ∧ K ∈ B ∧ k ∈ ℕ 0 → Base Scalar ⁡ P = Base R$
128 123 127 eleqtrrd $⊢ R ∈ Ring ∧ K ∈ B ∧ k ∈ ℕ 0 → A ⁡ k ∈ Base Scalar ⁡ P$
129 75 ad2antrr $⊢ R ∈ Ring ∧ K ∈ B ∧ k ∈ ℕ 0 → M ∈ Mnd$
130 simpr $⊢ R ∈ Ring ∧ K ∈ B ∧ k ∈ ℕ 0 → k ∈ ℕ 0$
131 82 ad2antrr $⊢ R ∈ Ring ∧ K ∈ B ∧ k ∈ ℕ 0 → X ∈ B$
132 58 6 mulgnn0cl
133 129 130 131 132 syl3anc
134 eqid $⊢ Scalar ⁡ P = Scalar ⁡ P$
135 eqid $⊢ Base Scalar ⁡ P = Base Scalar ⁡ P$
136 3 134 4 135 lmodvscl
137 119 128 133 136 syl3anc
138 137 fmpttd
139 1 2 3 4 5 6 7 ply1coefsupp
140 eqid $⊢ a ∈ ℕ 0 1 𝑜 ⟼ a ⁡ ∅ = a ∈ ℕ 0 1 𝑜 ⟼ a ⁡ ∅$
141 43 99 29 140 mapsnf1o2 $⊢ a ∈ ℕ 0 1 𝑜 ⟼ a ⁡ ∅ : ℕ 0 1 𝑜 ⟶ 1-1 onto ℕ 0$
142 141 a1i $⊢ R ∈ Ring ∧ K ∈ B → a ∈ ℕ 0 1 𝑜 ⟼ a ⁡ ∅ : ℕ 0 1 𝑜 ⟶ 1-1 onto ℕ 0$
143 15 112 116 117 138 139 142 gsumf1o
144 eqidd $⊢ R ∈ Ring ∧ K ∈ B → a ∈ ℕ 0 1 𝑜 ⟼ a ⁡ ∅ = a ∈ ℕ 0 1 𝑜 ⟼ a ⁡ ∅$
145 eqidd
146 fveq2 $⊢ k = a ⁡ ∅ → A ⁡ k = A ⁡ a ⁡ ∅$
147 oveq1
148 146 147 oveq12d
149 81 144 145 148 fmptco
150 149 oveq2d
151 110 143 150 3eqtrrd
152 19 98 151 3eqtrd