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 
|- F = ( Scalar ` W )
lcomf.k 
|- K = ( Base ` F )
lcomf.s 
|- .x. = ( .s ` W )
lcomf.b 
|- B = ( Base ` W )
lcomf.w 
|- ( ph -> W e. LMod )
lcomf.g 
|- ( ph -> G : I --> K )
lcomf.h 
|- ( ph -> H : I --> B )
lcomf.i 
|- ( ph -> I e. V )
lcomfsupp.z 
|- .0. = ( 0g ` W )
lcomfsupp.y 
|- Y = ( 0g ` F )
lcomfsupp.j 
|- ( ph -> G finSupp Y )
Assertion lcomfsupp 
|- ( ph -> ( G oF .x. H ) finSupp .0. )

Proof

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