This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 · 𝐹 ) ) ) )