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 1 ply1ring ⊢ R ∈ Ring → P ∈ Ring
14 5 ringmgp ⊢ P ∈ Ring → M ∈ Mnd
15 13 14 syl ⊢ R ∈ Ring → M ∈ Mnd
16 15 ad2antrr ⊢ R ∈ Ring ∧ K ∈ B ∧ k ∈ ℕ 0 → M ∈ Mnd
17 simpr ⊢ R ∈ Ring ∧ K ∈ B ∧ k ∈ ℕ 0 → k ∈ ℕ 0
18 2 1 3 vr1cl ⊢ R ∈ Ring → X ∈ B
19 18 ad2antrr ⊢ R ∈ Ring ∧ K ∈ B ∧ k ∈ ℕ 0 → X ∈ B
20 5 3 mgpbas ⊢ B = Base M
21 20 6 mulgnn0cl ⊢ M ∈ Mnd ∧ k ∈ ℕ 0 ∧ X ∈ B → k × ˙ X ∈ B
22 16 17 19 21 syl3anc ⊢ R ∈ Ring ∧ K ∈ B ∧ k ∈ ℕ 0 → k × ˙ X ∈ B
23 eqid ⊢ Base R = Base R
24 7 3 1 23 coe1f ⊢ K ∈ B → A : ℕ 0 ⟶ Base R
25 24 adantl ⊢ R ∈ Ring ∧ K ∈ B → A : ℕ 0 ⟶ Base R
26 eqid ⊢ 0 R = 0 R
27 7 3 1 26 coe1sfi ⊢ K ∈ B → finSupp 0 R⁡ A
28 27 adantl ⊢ R ∈ Ring ∧ K ∈ B → finSupp 0 R⁡ A
29 1 ply1sca ⊢ R ∈ Ring → R = Scalar ⁡ P
30 29 eqcomd ⊢ R ∈ Ring → Scalar ⁡ P = R
31 30 adantr ⊢ R ∈ Ring ∧ K ∈ B → Scalar ⁡ P = R
32 31 fveq2d ⊢ R ∈ Ring ∧ K ∈ B → 0 Scalar ⁡ P = 0 R
33 28 32 breqtrrd ⊢ R ∈ Ring ∧ K ∈ B → finSupp 0 Scalar ⁡ P ⁡ A
34 3 8 4 10 12 22 25 33 mptscmfsuppd ⊢ R ∈ Ring ∧ K ∈ B → finSupp 0 P⁡ k ∈ ℕ 0 ⟼ A ⁡ k · ˙ k × ˙ X