Metamath Proof Explorer

Theorem ply1mulgsumlem4

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

Ref Expression
Hypotheses ply1mulgsum.p ⊢P=Poly1⁡R
ply1mulgsum.b ⊢B=BaseP
ply1mulgsum.a ⊢A=coe1⁡K
ply1mulgsum.c ⊢C=coe1⁡L
ply1mulgsum.x ⊢X=var1⁡R
ply1mulgsum.pm ⊢×˙=⋅P
ply1mulgsum.sm ⊢·˙=⋅P
ply1mulgsum.rm ⊢∗˙=⋅R
ply1mulgsum.m ⊢M=mulGrpP
ply1mulgsum.e ⊢×˙=⋅M
Assertion ply1mulgsumlem4 ⊢R∈Ring∧K∈B∧L∈B→finSupp0P⁡k∈ℕ0⟼∑Rl=0kA⁡l∗˙C⁡k−l·˙k×˙X

Proof

Step Hyp Ref Expression
1 ply1mulgsum.p ⊢P=Poly1⁡R
2 ply1mulgsum.b ⊢B=BaseP
3 ply1mulgsum.a ⊢A=coe1⁡K
4 ply1mulgsum.c ⊢C=coe1⁡L
5 ply1mulgsum.x ⊢X=var1⁡R
6 ply1mulgsum.pm ⊢×˙=⋅P
7 ply1mulgsum.sm ⊢·˙=⋅P
8 ply1mulgsum.rm ⊢∗˙=⋅R
9 ply1mulgsum.m ⊢M=mulGrpP
10 ply1mulgsum.e ⊢×˙=⋅M
11 fvexd ⊢R∈Ring∧K∈B∧L∈B→0P∈V
12 ovexd ⊢R∈Ring∧K∈B∧L∈B∧k∈ℕ0→∑Rl=0kA⁡l∗˙C⁡k−l·˙k×˙X∈V
13 1 2 3 4 5 6 7 8 9 10 ply1mulgsumlem2 ⊢R∈Ring∧K∈B∧L∈B→∃s∈ℕ0∀n∈ℕ0s<n→∑Rl=0nA⁡l∗˙C⁡n−l=0R
14 vex ⊢n∈V
15 csbov12g ⊢n∈V→⦋n/k⦌∑Rl=0kA⁡l∗˙C⁡k−l·˙k×˙X=⦋n/k⦌∑Rl=0kA⁡l∗˙C⁡k−l·˙⦋n/k⦌k×˙X
16 csbov2g ⊢n∈V→⦋n/k⦌∑Rl=0kA⁡l∗˙C⁡k−l=∑R⦋n/k⦌l∈0…k⟼A⁡l∗˙C⁡k−l
17 id ⊢n∈V→n∈V
18 oveq2 ⊢k=n→0…k=0…n
19 fvoveq1 ⊢k=n→C⁡k−l=C⁡n−l
20 19 oveq2d ⊢k=n→A⁡l∗˙C⁡k−l=A⁡l∗˙C⁡n−l
21 18 20 mpteq12dv ⊢k=n→l∈0…k⟼A⁡l∗˙C⁡k−l=l∈0…n⟼A⁡l∗˙C⁡n−l
22 21 adantl ⊢n∈V∧k=n→l∈0…k⟼A⁡l∗˙C⁡k−l=l∈0…n⟼A⁡l∗˙C⁡n−l
23 17 22 csbied ⊢n∈V→⦋n/k⦌l∈0…k⟼A⁡l∗˙C⁡k−l=l∈0…n⟼A⁡l∗˙C⁡n−l
24 23 oveq2d ⊢n∈V→∑R⦋n/k⦌l∈0…k⟼A⁡l∗˙C⁡k−l=∑Rl=0nA⁡l∗˙C⁡n−l
25 16 24 eqtrd ⊢n∈V→⦋n/k⦌∑Rl=0kA⁡l∗˙C⁡k−l=∑Rl=0nA⁡l∗˙C⁡n−l
26 csbov1g ⊢n∈V→⦋n/k⦌k×˙X=⦋n/k⦌k×˙X
27 csbvarg ⊢n∈V→⦋n/k⦌k=n
28 27 oveq1d ⊢n∈V→⦋n/k⦌k×˙X=n×˙X
29 26 28 eqtrd ⊢n∈V→⦋n/k⦌k×˙X=n×˙X
30 25 29 oveq12d ⊢n∈V→⦋n/k⦌∑Rl=0kA⁡l∗˙C⁡k−l·˙⦋n/k⦌k×˙X=∑Rl=0nA⁡l∗˙C⁡n−l·˙n×˙X
31 15 30 eqtrd ⊢n∈V→⦋n/k⦌∑Rl=0kA⁡l∗˙C⁡k−l·˙k×˙X=∑Rl=0nA⁡l∗˙C⁡n−l·˙n×˙X
32 14 31 ax-mp ⊢⦋n/k⦌∑Rl=0kA⁡l∗˙C⁡k−l·˙k×˙X=∑Rl=0nA⁡l∗˙C⁡n−l·˙n×˙X
33 oveq1 ⊢∑Rl=0nA⁡l∗˙C⁡n−l=0R→∑Rl=0nA⁡l∗˙C⁡n−l·˙n×˙X=0R·˙n×˙X
34 1 ply1sca ⊢R∈Ring→R=Scalar⁡P
35 34 3ad2ant1 ⊢R∈Ring∧K∈B∧L∈B→R=Scalar⁡P
36 35 ad2antrr ⊢R∈Ring∧K∈B∧L∈B∧s∈ℕ0∧n∈ℕ0→R=Scalar⁡P
37 36 fveq2d ⊢R∈Ring∧K∈B∧L∈B∧s∈ℕ0∧n∈ℕ0→0R=0Scalar⁡P
38 37 oveq1d ⊢R∈Ring∧K∈B∧L∈B∧s∈ℕ0∧n∈ℕ0→0R·˙n×˙X=0Scalar⁡P·˙n×˙X
39 1 ply1lmod ⊢R∈Ring→P∈LMod
40 39 3ad2ant1 ⊢R∈Ring∧K∈B∧L∈B→P∈LMod
41 40 ad2antrr ⊢R∈Ring∧K∈B∧L∈B∧s∈ℕ0∧n∈ℕ0→P∈LMod
42 9 2 mgpbas ⊢B=BaseM
43 1 ply1ring ⊢R∈Ring→P∈Ring
44 9 ringmgp ⊢P∈Ring→M∈Mnd
45 43 44 syl ⊢R∈Ring→M∈Mnd
46 45 3ad2ant1 ⊢R∈Ring∧K∈B∧L∈B→M∈Mnd
47 46 ad2antrr ⊢R∈Ring∧K∈B∧L∈B∧s∈ℕ0∧n∈ℕ0→M∈Mnd
48 simpr ⊢R∈Ring∧K∈B∧L∈B∧s∈ℕ0∧n∈ℕ0→n∈ℕ0
49 5 1 2 vr1cl ⊢R∈Ring→X∈B
50 49 3ad2ant1 ⊢R∈Ring∧K∈B∧L∈B→X∈B
51 50 ad2antrr ⊢R∈Ring∧K∈B∧L∈B∧s∈ℕ0∧n∈ℕ0→X∈B
52 42 10 47 48 51 mulgnn0cld ⊢R∈Ring∧K∈B∧L∈B∧s∈ℕ0∧n∈ℕ0→n×˙X∈B
53 eqid ⊢Scalar⁡P=Scalar⁡P
54 eqid ⊢0Scalar⁡P=0Scalar⁡P
55 eqid ⊢0P=0P
56 2 53 7 54 55 lmod0vs ⊢P∈LMod∧n×˙X∈B→0Scalar⁡P·˙n×˙X=0P
57 41 52 56 syl2anc ⊢R∈Ring∧K∈B∧L∈B∧s∈ℕ0∧n∈ℕ0→0Scalar⁡P·˙n×˙X=0P
58 38 57 eqtrd ⊢R∈Ring∧K∈B∧L∈B∧s∈ℕ0∧n∈ℕ0→0R·˙n×˙X=0P
59 33 58 sylan9eqr ⊢R∈Ring∧K∈B∧L∈B∧s∈ℕ0∧n∈ℕ0∧∑Rl=0nA⁡l∗˙C⁡n−l=0R→∑Rl=0nA⁡l∗˙C⁡n−l·˙n×˙X=0P
60 32 59 eqtrid ⊢R∈Ring∧K∈B∧L∈B∧s∈ℕ0∧n∈ℕ0∧∑Rl=0nA⁡l∗˙C⁡n−l=0R→⦋n/k⦌∑Rl=0kA⁡l∗˙C⁡k−l·˙k×˙X=0P
61 60 ex ⊢R∈Ring∧K∈B∧L∈B∧s∈ℕ0∧n∈ℕ0→∑Rl=0nA⁡l∗˙C⁡n−l=0R→⦋n/k⦌∑Rl=0kA⁡l∗˙C⁡k−l·˙k×˙X=0P
62 61 imim2d ⊢R∈Ring∧K∈B∧L∈B∧s∈ℕ0∧n∈ℕ0→s<n→∑Rl=0nA⁡l∗˙C⁡n−l=0R→s<n→⦋n/k⦌∑Rl=0kA⁡l∗˙C⁡k−l·˙k×˙X=0P
63 62 ralimdva ⊢R∈Ring∧K∈B∧L∈B∧s∈ℕ0→∀n∈ℕ0s<n→∑Rl=0nA⁡l∗˙C⁡n−l=0R→∀n∈ℕ0s<n→⦋n/k⦌∑Rl=0kA⁡l∗˙C⁡k−l·˙k×˙X=0P
64 63 reximdva ⊢R∈Ring∧K∈B∧L∈B→∃s∈ℕ0∀n∈ℕ0s<n→∑Rl=0nA⁡l∗˙C⁡n−l=0R→∃s∈ℕ0∀n∈ℕ0s<n→⦋n/k⦌∑Rl=0kA⁡l∗˙C⁡k−l·˙k×˙X=0P
65 13 64 mpd ⊢R∈Ring∧K∈B∧L∈B→∃s∈ℕ0∀n∈ℕ0s<n→⦋n/k⦌∑Rl=0kA⁡l∗˙C⁡k−l·˙k×˙X=0P
66 11 12 65 mptnn0fsupp ⊢R∈Ring∧K∈B∧L∈B→finSupp0P⁡k∈ℕ0⟼∑Rl=0kA⁡l∗˙C⁡k−l·˙k×˙X