This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
ply1coefsupp.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
ply1coefsupp.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
ply1coefsupp.n ⊢ · = ( ·𝑠 ‘ 𝑃 )
ply1coefsupp.m ⊢ 𝑀 = ( mulGrp ‘ 𝑃 )
ply1coefsupp.e ⊢ ↑ = ( .g ‘ 𝑀 )
ply1coefsupp.a ⊢ 𝐴 = ( coe1 ‘ 𝐾 )
Assertion ply1coefsupp ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) finSupp ( 0g ‘ 𝑃 ) )

Proof

Step Hyp Ref Expression
1 ply1coefsupp.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 ply1coefsupp.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
3 ply1coefsupp.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
4 ply1coefsupp.n ⊢ · = ( ·𝑠 ‘ 𝑃 )
5 ply1coefsupp.m ⊢ 𝑀 = ( mulGrp ‘ 𝑃 )
6 ply1coefsupp.e ⊢ ↑ = ( .g ‘ 𝑀 )
7 ply1coefsupp.a ⊢ 𝐴 = ( coe1 ‘ 𝐾 )
8 eqid ⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
9 1 ply1lmod ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
10 9 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → 𝑃 ∈ LMod )
11 nn0ex ⊢ ℕ0 ∈ V
12 11 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ℕ0 ∈ V )
13 5 3 mgpbas ⊢ 𝐵 = ( Base ‘ 𝑀 )
14 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
15 5 ringmgp ⊢ ( 𝑃 ∈ Ring → 𝑀 ∈ Mnd )
16 14 15 syl ⊢ ( 𝑅 ∈ Ring → 𝑀 ∈ Mnd )
17 16 ad2antrr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑀 ∈ Mnd )
18 simpr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
19 2 1 3 vr1cl ⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ 𝐵 )
20 19 ad2antrr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑋 ∈ 𝐵 )
21 13 6 17 18 20 mulgnn0cld ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ↑ 𝑋 ) ∈ 𝐵 )
22 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
23 7 3 1 22 coe1f ⊢ ( 𝐾 ∈ 𝐵 → 𝐴 : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
24 23 adantl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → 𝐴 : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
25 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
26 7 3 1 25 coe1sfi ⊢ ( 𝐾 ∈ 𝐵 → 𝐴 finSupp ( 0g ‘ 𝑅 ) )
27 26 adantl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → 𝐴 finSupp ( 0g ‘ 𝑅 ) )
28 1 ply1sca ⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) )
29 28 eqcomd ⊢ ( 𝑅 ∈ Ring → ( Scalar ‘ 𝑃 ) = 𝑅 )
30 29 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( Scalar ‘ 𝑃 ) = 𝑅 )
31 30 fveq2d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( 0g ‘ ( Scalar ‘ 𝑃 ) ) = ( 0g ‘ 𝑅 ) )
32 27 31 breqtrrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑃 ) ) )
33 3 8 4 10 12 21 24 32 mptscmfsuppd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) finSupp ( 0g ‘ 𝑃 ) )