Theorem elfilspd

Description: Simplified version of ellspd when the spanning set is finite: all linear combinations are then acceptable. (Contributed by Stefan O'Rear, 7-Feb-2015) (Proof shortened by AV, 21-Jul-2019)

	Ref	Expression
Hypotheses	ellspd.n	⊢ 𝑁 = ( LSpan ‘ 𝑀 )
	ellspd.v	⊢ 𝐵 = ( Base ‘ 𝑀 )
	ellspd.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
	ellspd.s	⊢ 𝑆 = ( Scalar ‘ 𝑀 )
	ellspd.z	⊢ 0 = ( 0g ‘ 𝑆 )
	ellspd.t	⊢ · = ( ·𝑠 ‘ 𝑀 )
	elfilspd.f	⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ 𝐵 )
	elfilspd.m	⊢ ( 𝜑 → 𝑀 ∈ LMod )
	elfilspd.i	⊢ ( 𝜑 → 𝐼 ∈ Fin )
Assertion	elfilspd	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ ( 𝐹 “ 𝐼 ) ) ↔ ∃ 𝑓 ∈ ( 𝐾 ↑m 𝐼 ) 𝑋 = ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ellspd.n	⊢ 𝑁 = ( LSpan ‘ 𝑀 )
2		ellspd.v	⊢ 𝐵 = ( Base ‘ 𝑀 )
3		ellspd.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
4		ellspd.s	⊢ 𝑆 = ( Scalar ‘ 𝑀 )
5		ellspd.z	⊢ 0 = ( 0g ‘ 𝑆 )
6		ellspd.t	⊢ · = ( ·𝑠 ‘ 𝑀 )
7		elfilspd.f	⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ 𝐵 )
8		elfilspd.m	⊢ ( 𝜑 → 𝑀 ∈ LMod )
9		elfilspd.i	⊢ ( 𝜑 → 𝐼 ∈ Fin )
10	1 2 3 4 5 6 7 8 9	ellspd	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ ( 𝐹 “ 𝐼 ) ) ↔ ∃ 𝑓 ∈ ( 𝐾 ↑m 𝐼 ) ( 𝑓 finSupp 0 ∧ 𝑋 = ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) ) ) )
11		elmapi	⊢ ( 𝑓 ∈ ( 𝐾 ↑m 𝐼 ) → 𝑓 : 𝐼 ⟶ 𝐾 )
12	11	adantl	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ↑m 𝐼 ) ) → 𝑓 : 𝐼 ⟶ 𝐾 )
13	9	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ↑m 𝐼 ) ) → 𝐼 ∈ Fin )
14	5	fvexi	⊢ 0 ∈ V
15	14	a1i	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ↑m 𝐼 ) ) → 0 ∈ V )
16	12 13 15	fdmfifsupp	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ↑m 𝐼 ) ) → 𝑓 finSupp 0 )
17	16	biantrurd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( 𝑋 = ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) ↔ ( 𝑓 finSupp 0 ∧ 𝑋 = ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) ) ) )
18	17	rexbidva	⊢ ( 𝜑 → ( ∃ 𝑓 ∈ ( 𝐾 ↑m 𝐼 ) 𝑋 = ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) ↔ ∃ 𝑓 ∈ ( 𝐾 ↑m 𝐼 ) ( 𝑓 finSupp 0 ∧ 𝑋 = ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) ) ) )
19	10 18	bitr4d	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ ( 𝐹 “ 𝐼 ) ) ↔ ∃ 𝑓 ∈ ( 𝐾 ↑m 𝐼 ) 𝑋 = ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) ) )