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	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	lcomf.b	$⊢ B = {Base}_{W}$
	lcomf.w	$⊢ φ \to W \in LMod$
	lcomf.g	$⊢ φ \to G : I ⟶ K$
	lcomf.h	$⊢ φ \to H : I ⟶ B$
	lcomf.i	$⊢ φ \to I \in V$
	lcomfsupp.z	$⊢ \underset{˙}{0} = 0_{W}$
	lcomfsupp.y	$⊢ Y = 0_{F}$
	lcomfsupp.j	$⊢ φ \to {finSupp}_{Y} (G)$
Assertion	lcomfsupp	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((G {\underset{˙}{\cdot}}_{f} H))$

Proof

Step	Hyp	Ref	Expression
1		lcomf.f	$⊢ F = Scalar (W)$
2		lcomf.k	$⊢ K = {Base}_{F}$
3		lcomf.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
4		lcomf.b	$⊢ B = {Base}_{W}$
5		lcomf.w	$⊢ φ \to W \in LMod$
6		lcomf.g	$⊢ φ \to G : I ⟶ K$
7		lcomf.h	$⊢ φ \to H : I ⟶ B$
8		lcomf.i	$⊢ φ \to I \in V$
9		lcomfsupp.z	$⊢ \underset{˙}{0} = 0_{W}$
10		lcomfsupp.y	$⊢ Y = 0_{F}$
11		lcomfsupp.j	$⊢ φ \to {finSupp}_{Y} (G)$
12	11	fsuppimpd	$⊢ φ \to G supp Y \in Fin$
13	1 2 3 4 5 6 7 8	lcomf	$⊢ φ \to (G {\underset{˙}{\cdot}}_{f} H) : I ⟶ B$
14		eldifi	$⊢ x \in (I ∖ {supp}_{Y} (G)) \to x \in I$
15	6	ffnd	$⊢ φ \to G Fn I$
16	15	adantr	$⊢ (φ \land x \in I) \to G Fn I$
17	7	ffnd	$⊢ φ \to H Fn I$
18	17	adantr	$⊢ (φ \land x \in I) \to H Fn I$
19	8	adantr	$⊢ (φ \land x \in I) \to I \in V$
20		simpr	$⊢ (φ \land x \in I) \to x \in I$
21		fnfvof	$⊢ ((G Fn I \land H Fn I) \land (I \in V \land x \in I)) \to (G {\underset{˙}{\cdot}}_{f} H) (x) = G (x) \underset{˙}{\cdot} H (x)$
22	16 18 19 20 21	syl22anc	$⊢ (φ \land x \in I) \to (G {\underset{˙}{\cdot}}_{f} H) (x) = G (x) \underset{˙}{\cdot} H (x)$
23	14 22	sylan2	$⊢ (φ \land x \in (I ∖ {supp}_{Y} (G))) \to (G {\underset{˙}{\cdot}}_{f} H) (x) = G (x) \underset{˙}{\cdot} H (x)$
24		ssidd	$⊢ φ \to G supp Y \subseteq G supp Y$
25	10	fvexi	$⊢ Y \in V$
26	25	a1i	$⊢ φ \to Y \in V$
27	6 24 8 26	suppssr	$⊢ (φ \land x \in (I ∖ {supp}_{Y} (G))) \to G (x) = Y$
28	27	oveq1d	$⊢ (φ \land x \in (I ∖ {supp}_{Y} (G))) \to G (x) \underset{˙}{\cdot} H (x) = Y \underset{˙}{\cdot} H (x)$
29	7	ffvelrnda	$⊢ (φ \land x \in I) \to H (x) \in B$
30	4 1 3 10 9	lmod0vs	$⊢ (W \in LMod \land H (x) \in B) \to Y \underset{˙}{\cdot} H (x) = \underset{˙}{0}$
31	5 29 30	syl2an2r	$⊢ (φ \land x \in I) \to Y \underset{˙}{\cdot} H (x) = \underset{˙}{0}$
32	14 31	sylan2	$⊢ (φ \land x \in (I ∖ {supp}_{Y} (G))) \to Y \underset{˙}{\cdot} H (x) = \underset{˙}{0}$
33	23 28 32	3eqtrd	$⊢ (φ \land x \in (I ∖ {supp}_{Y} (G))) \to (G {\underset{˙}{\cdot}}_{f} H) (x) = \underset{˙}{0}$
34	13 33	suppss	$⊢ φ \to (G {\underset{˙}{\cdot}}_{f} H) supp \underset{˙}{0} \subseteq G supp Y$
35	12 34	ssfid	$⊢ φ \to (G {\underset{˙}{\cdot}}_{f} H) supp \underset{˙}{0} \in Fin$
36		inidm	$⊢ I \cap I = I$
37	15 17 8 8 36	offn	$⊢ φ \to (G {\underset{˙}{\cdot}}_{f} H) Fn I$
38		fnfun	$⊢ (G {\underset{˙}{\cdot}}_{f} H) Fn I \to Fun (G {\underset{˙}{\cdot}}_{f} H)$
39	37 38	syl	$⊢ φ \to Fun (G {\underset{˙}{\cdot}}_{f} H)$
40		ovexd	$⊢ φ \to G {\underset{˙}{\cdot}}_{f} H \in V$
41	9	fvexi	$⊢ \underset{˙}{0} \in V$
42	41	a1i	$⊢ φ \to \underset{˙}{0} \in V$
43		funisfsupp	$⊢ (Fun (G {\underset{˙}{\cdot}}_{f} H) \land G {\underset{˙}{\cdot}}_{f} H \in V \land \underset{˙}{0} \in V) \to ({finSupp}_{\underset{˙}{0}} ((G {\underset{˙}{\cdot}}_{f} H)) \leftrightarrow (G {\underset{˙}{\cdot}}_{f} H) supp \underset{˙}{0} \in Fin)$
44	39 40 42 43	syl3anc	$⊢ φ \to ({finSupp}_{\underset{˙}{0}} ((G {\underset{˙}{\cdot}}_{f} H)) \leftrightarrow (G {\underset{˙}{\cdot}}_{f} H) supp \underset{˙}{0} \in Fin)$
45	35 44	mpbird	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((G {\underset{˙}{\cdot}}_{f} H))$

Metamath Proof Explorer

Theorem lcomfsupp

Proof