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 )