Metamath Proof Explorer

Theorem ply1coefsupp

Description: The decomposition of a univariate polynomial is finitely supported. Formerly part of proof for ply1coe . (Contributed by Stefan O'Rear, 21-Mar-2015) (Revised by AV, 8-Aug-2019)

Ref Expression
Hypotheses ply1coefsupp.p ⊢ P = Poly 1 ⁡ R
ply1coefsupp.x ⊢ X = var 1 ⁡ R
ply1coefsupp.b ⊢ B = Base P
ply1coefsupp.n ⊢ · ˙ = ⋅ P
ply1coefsupp.m ⊢ M = mulGrp P
ply1coefsupp.e ⊢ × ˙ = ⋅ M
ply1coefsupp.a ⊢ A = coe 1 ⁡ K
Assertion ply1coefsupp ⊢ R ∈ Ring ∧ K ∈ B → finSupp 0 P⁡ k ∈ ℕ 0 ⟼ A ⁡ k · ˙ k × ˙ X

Proof

Step Hyp Ref Expression
1 ply1coefsupp.p ⊢ P = Poly 1 ⁡ R
2 ply1coefsupp.x ⊢ X = var 1 ⁡ R
3 ply1coefsupp.b ⊢ B = Base P
4 ply1coefsupp.n ⊢ · ˙ = ⋅ P
5 ply1coefsupp.m ⊢ M = mulGrp P
6 ply1coefsupp.e ⊢ × ˙ = ⋅ M
7 ply1coefsupp.a ⊢ A = coe 1 ⁡ K
8 eqid ⊢ Scalar ⁡ P = Scalar ⁡ P
9 1 ply1lmod ⊢ R ∈ Ring → P ∈ LMod
10 9 adantr ⊢ R ∈ Ring ∧ K ∈ B → P ∈ LMod
11 nn0ex ⊢ ℕ 0 ∈ V
12 11 a1i ⊢ R ∈ Ring ∧ K ∈ B → ℕ 0 ∈ V
13 5 3 mgpbas ⊢ B = Base M
14 1 ply1ring ⊢ R ∈ Ring → P ∈ Ring
15 5 ringmgp ⊢ P ∈ Ring → M ∈ Mnd
16 14 15 syl ⊢ R ∈ Ring → M ∈ Mnd
17 16 ad2antrr ⊢ R ∈ Ring ∧ K ∈ B ∧ k ∈ ℕ 0 → M ∈ Mnd
18 simpr ⊢ R ∈ Ring ∧ K ∈ B ∧ k ∈ ℕ 0 → k ∈ ℕ 0
19 2 1 3 vr1cl ⊢ R ∈ Ring → X ∈ B
20 19 ad2antrr ⊢ R ∈ Ring ∧ K ∈ B ∧ k ∈ ℕ 0 → X ∈ B
21 13 6 17 18 20 mulgnn0cld ⊢ R ∈ Ring ∧ K ∈ B ∧ k ∈ ℕ 0 → k × ˙ X ∈ B
22 eqid ⊢ Base R = Base R
23 7 3 1 22 coe1f ⊢ K ∈ B → A : ℕ 0 ⟶ Base R
24 23 adantl ⊢ R ∈ Ring ∧ K ∈ B → A : ℕ 0 ⟶ Base R
25 eqid ⊢ 0 R = 0 R
26 7 3 1 25 coe1sfi ⊢ K ∈ B → finSupp 0 R⁡ A
27 26 adantl ⊢ R ∈ Ring ∧ K ∈ B → finSupp 0 R⁡ A
28 1 ply1sca ⊢ R ∈ Ring → R = Scalar ⁡ P
29 28 eqcomd ⊢ R ∈ Ring → Scalar ⁡ P = R
30 29 adantr ⊢ R ∈ Ring ∧ K ∈ B → Scalar ⁡ P = R
31 30 fveq2d ⊢ R ∈ Ring ∧ K ∈ B → 0 Scalar ⁡ P = 0 R
32 27 31 breqtrrd ⊢ R ∈ Ring ∧ K ∈ B → finSupp 0 Scalar ⁡ P ⁡ A
33 3 8 4 10 12 21 24 32 mptscmfsuppd ⊢ R ∈ Ring ∧ K ∈ B → finSupp 0 P⁡ k ∈ ℕ 0 ⟼ A ⁡ k · ˙ k × ˙ X