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 F = Scalar W
lcomf.k K = Base F
lcomf.s · ˙ = W
lcomf.b B = Base W
lcomf.w φ W LMod
lcomf.g φ G : I K
lcomf.h φ H : I B
lcomf.i φ I V
lcomfsupp.z 0 ˙ = 0 W
lcomfsupp.y Y = 0 F
lcomfsupp.j φ finSupp Y G
Assertion lcomfsupp φ finSupp 0 ˙ G · ˙ f H

Proof

Step Hyp Ref Expression
1 lcomf.f F = Scalar W
2 lcomf.k K = Base F
3 lcomf.s · ˙ = W
4 lcomf.b B = Base W
5 lcomf.w φ W LMod
6 lcomf.g φ G : I K
7 lcomf.h φ H : I B
8 lcomf.i φ I V
9 lcomfsupp.z 0 ˙ = 0 W
10 lcomfsupp.y Y = 0 F
11 lcomfsupp.j φ finSupp Y G
12 11 fsuppimpd φ G supp Y Fin
13 1 2 3 4 5 6 7 8 lcomf φ G · ˙ f H : I B
14 eldifi x I supp Y G x I
15 6 ffnd φ G Fn I
16 15 adantr φ x I G Fn I
17 7 ffnd φ H Fn I
18 17 adantr φ x I H Fn I
19 8 adantr φ x I I V
20 simpr φ x I x I
21 fnfvof G Fn I H Fn I I V x I G · ˙ f H x = G x · ˙ H x
22 16 18 19 20 21 syl22anc φ x I G · ˙ f H x = G x · ˙ H x
23 14 22 sylan2 φ x I supp Y G G · ˙ f H x = G x · ˙ H x
24 ssidd φ G supp Y G supp Y
25 10 fvexi Y V
26 25 a1i φ Y V
27 6 24 8 26 suppssr φ x I supp Y G G x = Y
28 27 oveq1d φ x I supp Y G G x · ˙ H x = Y · ˙ H x
29 7 ffvelrnda φ x I H x B
30 4 1 3 10 9 lmod0vs W LMod H x B Y · ˙ H x = 0 ˙
31 5 29 30 syl2an2r φ x I Y · ˙ H x = 0 ˙
32 14 31 sylan2 φ x I supp Y G Y · ˙ H x = 0 ˙
33 23 28 32 3eqtrd φ x I supp Y G G · ˙ f H x = 0 ˙
34 13 33 suppss φ G · ˙ f H supp 0 ˙ G supp Y
35 12 34 ssfid φ G · ˙ f H supp 0 ˙ Fin
36 15 17 8 8 offun φ Fun G · ˙ f H
37 ovexd φ G · ˙ f H V
38 9 fvexi 0 ˙ V
39 38 a1i φ 0 ˙ V
40 funisfsupp Fun G · ˙ f H G · ˙ f H V 0 ˙ V finSupp 0 ˙ G · ˙ f H G · ˙ f H supp 0 ˙ Fin
41 36 37 39 40 syl3anc φ finSupp 0 ˙ G · ˙ f H G · ˙ f H supp 0 ˙ Fin
42 35 41 mpbird φ finSupp 0 ˙ G · ˙ f H