Metamath Proof Explorer

Theorem ply1mulgsumlem3

Description: Lemma 3 for ply1mulgsum . (Contributed by AV, 20-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 ply1mulgsumlem3 ( ( 𝑅 ∈ 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 csbov2g ⊢ ( 𝑛 ∈ V → ⦋ 𝑛 / 𝑘 ⦌ ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) = ( 𝑅 Σg ⦋ 𝑛 / 𝑘 ⦌ ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) )
16 id ⊢ ( 𝑛 ∈ V → 𝑛 ∈ V )
17 oveq2 ⊢ ( 𝑘 = 𝑛 → ( 0 ... 𝑘 ) = ( 0 ... 𝑛 ) )
18 fvoveq1 ⊢ ( 𝑘 = 𝑛 → ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) = ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) )
19 18 oveq2d ⊢ ( 𝑘 = 𝑛 → ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) = ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) )
20 17 19 mpteq12dv ⊢ ( 𝑘 = 𝑛 → ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) = ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) )
21 20 adantl ⊢ ( ( 𝑛 ∈ V ∧ 𝑘 = 𝑛 ) → ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) = ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) )
22 16 21 csbied ⊢ ( 𝑛 ∈ V → ⦋ 𝑛 / 𝑘 ⦌ ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) = ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) )
23 22 oveq2d ⊢ ( 𝑛 ∈ V → ( 𝑅 Σg ⦋ 𝑛 / 𝑘 ⦌ ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) = ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) )
24 15 23 eqtrd ⊢ ( 𝑛 ∈ V → ⦋ 𝑛 / 𝑘 ⦌ ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) = ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) )
25 14 24 ax-mp ⊢ ⦋ 𝑛 / 𝑘 ⦌ ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) = ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) )
26 simpr ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) = ( 0g ‘ 𝑅 ) ) → ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) = ( 0g ‘ 𝑅 ) )
27 25 26 syl5eq ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) = ( 0g ‘ 𝑅 ) ) → ⦋ 𝑛 / 𝑘 ⦌ ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) = ( 0g ‘ 𝑅 ) )
28 27 ex ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) = ( 0g ‘ 𝑅 ) → ⦋ 𝑛 / 𝑘 ⦌ ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) = ( 0g ‘ 𝑅 ) ) )
29 28 imim2d ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑠 < 𝑛 → ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) = ( 0g ‘ 𝑅 ) ) → ( 𝑠 < 𝑛 → ⦋ 𝑛 / 𝑘 ⦌ ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) = ( 0g ‘ 𝑅 ) ) ) )
30 29 ralimdva ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) → ( ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) = ( 0g ‘ 𝑅 ) ) → ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ⦋ 𝑛 / 𝑘 ⦌ ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) = ( 0g ‘ 𝑅 ) ) ) )
31 30 reximdva ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ( ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) = ( 0g ‘ 𝑅 ) ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ⦋ 𝑛 / 𝑘 ⦌ ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) = ( 0g ‘ 𝑅 ) ) ) )
32 13 31 mpd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ⦋ 𝑛 / 𝑘 ⦌ ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) = ( 0g ‘ 𝑅 ) ) )
33 11 12 32 mptnn0fsupp ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) ) finSupp ( 0g ‘ 𝑅 ) )