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. )

Metamath Proof Explorer

Theorem lcomfsupp

Proof