Metamath Proof Explorer

Theorem ply1mulgsumlem4

Description: Lemma 4 for ply1mulgsum . (Contributed by AV, 19-Oct-2019)

Ref Expression
Hypotheses ply1mulgsum.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
ply1mulgsum.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
ply1mulgsum.a ⊢ 𝐴 = ( coe1 ‘ 𝐾 )
ply1mulgsum.c ⊢ 𝐶 = ( coe1 ‘ 𝐿 )
ply1mulgsum.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
ply1mulgsum.pm ⊢ × = ( .r ‘ 𝑃 )
ply1mulgsum.sm ⊢ · = ( ·𝑠 ‘ 𝑃 )
ply1mulgsum.rm ⊢ ∗ = ( .r ‘ 𝑅 )
ply1mulgsum.m ⊢ 𝑀 = ( mulGrp ‘ 𝑃 )
ply1mulgsum.e ⊢ ↑ = ( .g ‘ 𝑀 )
Assertion ply1mulgsumlem4 ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) · ( 𝑘 ↑ 𝑋 ) ) ) finSupp ( 0g ‘ 𝑃 ) )

Proof

Step Hyp Ref Expression
1 ply1mulgsum.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 ply1mulgsum.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
3 ply1mulgsum.a ⊢ 𝐴 = ( coe1 ‘ 𝐾 )
4 ply1mulgsum.c ⊢ 𝐶 = ( coe1 ‘ 𝐿 )
5 ply1mulgsum.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
6 ply1mulgsum.pm ⊢ × = ( .r ‘ 𝑃 )
7 ply1mulgsum.sm ⊢ · = ( ·𝑠 ‘ 𝑃 )
8 ply1mulgsum.rm ⊢ ∗ = ( .r ‘ 𝑅 )
9 ply1mulgsum.m ⊢ 𝑀 = ( mulGrp ‘ 𝑃 )
10 ply1mulgsum.e ⊢ ↑ = ( .g ‘ 𝑀 )
11 fvexd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ( 0g ‘ 𝑃 ) ∈ V )
12 ovexd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) · ( 𝑘 ↑ 𝑋 ) ) ∈ V )
13 1 2 3 4 5 6 7 8 9 10 ply1mulgsumlem2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) = ( 0g ‘ 𝑅 ) ) )
14 vex ⊢ 𝑛 ∈ V
15 csbov12g ⊢ ( 𝑛 ∈ V → ⦋ 𝑛 / 𝑘 ⦌ ( ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) · ( 𝑘 ↑ 𝑋 ) ) = ( ⦋ 𝑛 / 𝑘 ⦌ ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) · ⦋ 𝑛 / 𝑘 ⦌ ( 𝑘 ↑ 𝑋 ) ) )
16 csbov2g ⊢ ( 𝑛 ∈ V → ⦋ 𝑛 / 𝑘 ⦌ ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) = ( 𝑅 Σg ⦋ 𝑛 / 𝑘 ⦌ ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) )
17 id ⊢ ( 𝑛 ∈ V → 𝑛 ∈ V )
18 oveq2 ⊢ ( 𝑘 = 𝑛 → ( 0 ... 𝑘 ) = ( 0 ... 𝑛 ) )
19 fvoveq1 ⊢ ( 𝑘 = 𝑛 → ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) = ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) )
20 19 oveq2d ⊢ ( 𝑘 = 𝑛 → ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) = ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) )
21 18 20 mpteq12dv ⊢ ( 𝑘 = 𝑛 → ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) = ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) )
22 21 adantl ⊢ ( ( 𝑛 ∈ V ∧ 𝑘 = 𝑛 ) → ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) = ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) )
23 17 22 csbied ⊢ ( 𝑛 ∈ V → ⦋ 𝑛 / 𝑘 ⦌ ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) = ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) )
24 23 oveq2d ⊢ ( 𝑛 ∈ V → ( 𝑅 Σg ⦋ 𝑛 / 𝑘 ⦌ ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) = ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) )
25 16 24 eqtrd ⊢ ( 𝑛 ∈ V → ⦋ 𝑛 / 𝑘 ⦌ ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) = ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) )
26 csbov1g ⊢ ( 𝑛 ∈ V → ⦋ 𝑛 / 𝑘 ⦌ ( 𝑘 ↑ 𝑋 ) = ( ⦋ 𝑛 / 𝑘 ⦌ 𝑘 ↑ 𝑋 ) )
27 csbvarg ⊢ ( 𝑛 ∈ V → ⦋ 𝑛 / 𝑘 ⦌ 𝑘 = 𝑛 )
28 27 oveq1d ⊢ ( 𝑛 ∈ V → ( ⦋ 𝑛 / 𝑘 ⦌ 𝑘 ↑ 𝑋 ) = ( 𝑛 ↑ 𝑋 ) )
29 26 28 eqtrd ⊢ ( 𝑛 ∈ V → ⦋ 𝑛 / 𝑘 ⦌ ( 𝑘 ↑ 𝑋 ) = ( 𝑛 ↑ 𝑋 ) )
30 25 29 oveq12d ⊢ ( 𝑛 ∈ V → ( ⦋ 𝑛 / 𝑘 ⦌ ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) · ⦋ 𝑛 / 𝑘 ⦌ ( 𝑘 ↑ 𝑋 ) ) = ( ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) · ( 𝑛 ↑ 𝑋 ) ) )
31 15 30 eqtrd ⊢ ( 𝑛 ∈ V → ⦋ 𝑛 / 𝑘 ⦌ ( ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) · ( 𝑘 ↑ 𝑋 ) ) = ( ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) · ( 𝑛 ↑ 𝑋 ) ) )
32 14 31 ax-mp ⊢ ⦋ 𝑛 / 𝑘 ⦌ ( ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) · ( 𝑘 ↑ 𝑋 ) ) = ( ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) · ( 𝑛 ↑ 𝑋 ) )
33 oveq1 ⊢ ( ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) = ( 0g ‘ 𝑅 ) → ( ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) · ( 𝑛 ↑ 𝑋 ) ) = ( ( 0g ‘ 𝑅 ) · ( 𝑛 ↑ 𝑋 ) ) )
34 1 ply1sca ⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) )
35 34 3ad2ant1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → 𝑅 = ( Scalar ‘ 𝑃 ) )
36 35 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑅 = ( Scalar ‘ 𝑃 ) )
37 36 fveq2d ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( Scalar ‘ 𝑃 ) ) )
38 37 oveq1d ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 0g ‘ 𝑅 ) · ( 𝑛 ↑ 𝑋 ) ) = ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) · ( 𝑛 ↑ 𝑋 ) ) )
39 1 ply1lmod ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
40 39 3ad2ant1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → 𝑃 ∈ LMod )
41 40 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑃 ∈ LMod )
42 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
43 9 ringmgp ⊢ ( 𝑃 ∈ Ring → 𝑀 ∈ Mnd )
44 42 43 syl ⊢ ( 𝑅 ∈ Ring → 𝑀 ∈ Mnd )
45 44 3ad2ant1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → 𝑀 ∈ Mnd )
46 45 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑀 ∈ Mnd )
47 simpr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
48 5 1 2 vr1cl ⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ 𝐵 )
49 48 3ad2ant1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
50 49 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑋 ∈ 𝐵 )
51 9 2 mgpbas ⊢ 𝐵 = ( Base ‘ 𝑀 )
52 51 10 mulgnn0cl ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑛 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑛 ↑ 𝑋 ) ∈ 𝐵 )
53 46 47 50 52 syl3anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 ↑ 𝑋 ) ∈ 𝐵 )
54 eqid ⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
55 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑃 ) ) = ( 0g ‘ ( Scalar ‘ 𝑃 ) )
56 eqid ⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
57 2 54 7 55 56 lmod0vs ⊢ ( ( 𝑃 ∈ LMod ∧ ( 𝑛 ↑ 𝑋 ) ∈ 𝐵 ) → ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) · ( 𝑛 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) )
58 41 53 57 syl2anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) · ( 𝑛 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) )
59 38 58 eqtrd ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 0g ‘ 𝑅 ) · ( 𝑛 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) )
60 33 59 sylan9eqr ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) = ( 0g ‘ 𝑅 ) ) → ( ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) · ( 𝑛 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) )
61 32 60 syl5eq ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) = ( 0g ‘ 𝑅 ) ) → ⦋ 𝑛 / 𝑘 ⦌ ( ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) · ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) )
62 61 ex ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) = ( 0g ‘ 𝑅 ) → ⦋ 𝑛 / 𝑘 ⦌ ( ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) · ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) )
63 62 imim2d ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑠 < 𝑛 → ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) = ( 0g ‘ 𝑅 ) ) → ( 𝑠 < 𝑛 → ⦋ 𝑛 / 𝑘 ⦌ ( ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) · ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) ) )
64 63 ralimdva ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) → ( ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) = ( 0g ‘ 𝑅 ) ) → ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ⦋ 𝑛 / 𝑘 ⦌ ( ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) · ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) ) )
65 64 reximdva ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ( ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) = ( 0g ‘ 𝑅 ) ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ⦋ 𝑛 / 𝑘 ⦌ ( ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) · ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) ) )
66 13 65 mpd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ⦋ 𝑛 / 𝑘 ⦌ ( ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) · ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) )
67 11 12 66 mptnn0fsupp ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) · ( 𝑘 ↑ 𝑋 ) ) ) finSupp ( 0g ‘ 𝑃 ) )