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 1 ply1ring ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
14 5 ringmgp ( 𝑃 ∈ Ring → 𝑀 ∈ Mnd )
15 13 14 syl ( 𝑅 ∈ Ring → 𝑀 ∈ Mnd )
16 15 ad2antrr ( ( ( 𝑅 ∈ Ring ∧ 𝐾𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑀 ∈ Mnd )
17 simpr ( ( ( 𝑅 ∈ Ring ∧ 𝐾𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
18 2 1 3 vr1cl ( 𝑅 ∈ Ring → 𝑋𝐵 )
19 18 ad2antrr ( ( ( 𝑅 ∈ Ring ∧ 𝐾𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑋𝐵 )
20 5 3 mgpbas 𝐵 = ( Base ‘ 𝑀 )
21 20 6 mulgnn0cl ( ( 𝑀 ∈ Mnd ∧ 𝑘 ∈ ℕ0𝑋𝐵 ) → ( 𝑘 𝑋 ) ∈ 𝐵 )
22 16 17 19 21 syl3anc ( ( ( 𝑅 ∈ Ring ∧ 𝐾𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 𝑋 ) ∈ 𝐵 )
23 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
24 7 3 1 23 coe1f ( 𝐾𝐵𝐴 : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
25 24 adantl ( ( 𝑅 ∈ Ring ∧ 𝐾𝐵 ) → 𝐴 : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
26 eqid ( 0g𝑅 ) = ( 0g𝑅 )
27 7 3 1 26 coe1sfi ( 𝐾𝐵𝐴 finSupp ( 0g𝑅 ) )
28 27 adantl ( ( 𝑅 ∈ Ring ∧ 𝐾𝐵 ) → 𝐴 finSupp ( 0g𝑅 ) )
29 1 ply1sca ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) )
30 29 eqcomd ( 𝑅 ∈ Ring → ( Scalar ‘ 𝑃 ) = 𝑅 )
31 30 adantr ( ( 𝑅 ∈ Ring ∧ 𝐾𝐵 ) → ( Scalar ‘ 𝑃 ) = 𝑅 )
32 31 fveq2d ( ( 𝑅 ∈ Ring ∧ 𝐾𝐵 ) → ( 0g ‘ ( Scalar ‘ 𝑃 ) ) = ( 0g𝑅 ) )
33 28 32 breqtrrd ( ( 𝑅 ∈ Ring ∧ 𝐾𝐵 ) → 𝐴 finSupp ( 0g ‘ ( Scalar ‘ 𝑃 ) ) )
34 3 8 4 10 12 22 25 33 mptscmfsuppd ( ( 𝑅 ∈ Ring ∧ 𝐾𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴𝑘 ) · ( 𝑘 𝑋 ) ) ) finSupp ( 0g𝑃 ) )