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

Metamath Proof Explorer

Theorem lcomfsupp

Description: A linear-combination sum is finitely supported if the coefficients are. (Contributed by Stefan O'Rear, 28-Feb-2015) (Revised by AV, 15-Jul-2019)

Ref Expression
Hypotheses lcomf.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
lcomf.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
lcomf.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
lcomf.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
lcomf.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
lcomf.g ⊢ ( 𝜑 → 𝐺 : 𝐼 ⟶ 𝐾 )
lcomf.h ⊢ ( 𝜑 → 𝐻 : 𝐼 ⟶ 𝐵 )
lcomf.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
lcomfsupp.z ⊢ 0 = ( 0g ‘ 𝑊 )
lcomfsupp.y ⊢ 𝑌 = ( 0g ‘ 𝐹 )
lcomfsupp.j ⊢ ( 𝜑 → 𝐺 finSupp 𝑌 )
Assertion lcomfsupp ( 𝜑 → ( 𝐺 ∘f · 𝐻 ) finSupp 0 )

Proof

Step Hyp Ref Expression
1 lcomf.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2 lcomf.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
3 lcomf.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
4 lcomf.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
5 lcomf.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
6 lcomf.g ⊢ ( 𝜑 → 𝐺 : 𝐼 ⟶ 𝐾 )
7 lcomf.h ⊢ ( 𝜑 → 𝐻 : 𝐼 ⟶ 𝐵 )
8 lcomf.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
9 lcomfsupp.z ⊢ 0 = ( 0g ‘ 𝑊 )
10 lcomfsupp.y ⊢ 𝑌 = ( 0g ‘ 𝐹 )
11 lcomfsupp.j ⊢ ( 𝜑 → 𝐺 finSupp 𝑌 )
12 11 fsuppimpd ⊢ ( 𝜑 → ( 𝐺 supp 𝑌 ) ∈ Fin )
13 1 2 3 4 5 6 7 8 lcomf ⊢ ( 𝜑 → ( 𝐺 ∘f · 𝐻 ) : 𝐼 ⟶ 𝐵 )
14 eldifi ⊢ ( 𝑥 ∈ ( 𝐼 ∖ ( 𝐺 supp 𝑌 ) ) → 𝑥 ∈ 𝐼 )
15 6 ffnd ⊢ ( 𝜑 → 𝐺 Fn 𝐼 )
16 15 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐺 Fn 𝐼 )
17 7 ffnd ⊢ ( 𝜑 → 𝐻 Fn 𝐼 )
18 17 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐻 Fn 𝐼 )
19 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐼 ∈ 𝑉 )
20 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑥 ∈ 𝐼 )
21 fnfvof ⊢ ( ( ( 𝐺 Fn 𝐼 ∧ 𝐻 Fn 𝐼 ) ∧ ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ 𝐼 ) ) → ( ( 𝐺 ∘f · 𝐻 ) ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) · ( 𝐻 ‘ 𝑥 ) ) )
22 16 18 19 20 21 syl22anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐺 ∘f · 𝐻 ) ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) · ( 𝐻 ‘ 𝑥 ) ) )
23 14 22 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝐺 supp 𝑌 ) ) ) → ( ( 𝐺 ∘f · 𝐻 ) ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) · ( 𝐻 ‘ 𝑥 ) ) )
24 ssidd ⊢ ( 𝜑 → ( 𝐺 supp 𝑌 ) ⊆ ( 𝐺 supp 𝑌 ) )
25 10 fvexi ⊢ 𝑌 ∈ V
26 25 a1i ⊢ ( 𝜑 → 𝑌 ∈ V )
27 6 24 8 26 suppssr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝐺 supp 𝑌 ) ) ) → ( 𝐺 ‘ 𝑥 ) = 𝑌 )
28 27 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝐺 supp 𝑌 ) ) ) → ( ( 𝐺 ‘ 𝑥 ) · ( 𝐻 ‘ 𝑥 ) ) = ( 𝑌 · ( 𝐻 ‘ 𝑥 ) ) )
29 7 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝐻 ‘ 𝑥 ) ∈ 𝐵 )
30 4 1 3 10 9 lmod0vs ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐻 ‘ 𝑥 ) ∈ 𝐵 ) → ( 𝑌 · ( 𝐻 ‘ 𝑥 ) ) = 0 )
31 5 29 30 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑌 · ( 𝐻 ‘ 𝑥 ) ) = 0 )
32 14 31 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝐺 supp 𝑌 ) ) ) → ( 𝑌 · ( 𝐻 ‘ 𝑥 ) ) = 0 )
33 23 28 32 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ ( 𝐺 supp 𝑌 ) ) ) → ( ( 𝐺 ∘f · 𝐻 ) ‘ 𝑥 ) = 0 )
34 13 33 suppss ⊢ ( 𝜑 → ( ( 𝐺 ∘f · 𝐻 ) supp 0 ) ⊆ ( 𝐺 supp 𝑌 ) )
35 12 34 ssfid ⊢ ( 𝜑 → ( ( 𝐺 ∘f · 𝐻 ) supp 0 ) ∈ Fin )
36 15 17 8 8 offun ⊢ ( 𝜑 → Fun ( 𝐺 ∘f · 𝐻 ) )
37 ovexd ⊢ ( 𝜑 → ( 𝐺 ∘f · 𝐻 ) ∈ V )
38 9 fvexi ⊢ 0 ∈ V
39 38 a1i ⊢ ( 𝜑 → 0 ∈ V )
40 funisfsupp ⊢ ( ( Fun ( 𝐺 ∘f · 𝐻 ) ∧ ( 𝐺 ∘f · 𝐻 ) ∈ V ∧ 0 ∈ V ) → ( ( 𝐺 ∘f · 𝐻 ) finSupp 0 ↔ ( ( 𝐺 ∘f · 𝐻 ) supp 0 ) ∈ Fin ) )
41 36 37 39 40 syl3anc ⊢ ( 𝜑 → ( ( 𝐺 ∘f · 𝐻 ) finSupp 0 ↔ ( ( 𝐺 ∘f · 𝐻 ) supp 0 ) ∈ Fin ) )
42 35 41 mpbird ⊢ ( 𝜑 → ( 𝐺 ∘f · 𝐻 ) finSupp 0 )