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 ⊢ N = LSpan ⁡ M
ellspd.v ⊢ B = Base M
ellspd.k ⊢ K = Base S
ellspd.s ⊢ S = Scalar ⁡ M
ellspd.z ⊢ 0 ˙ = 0 S
ellspd.t ⊢ · ˙ = ⋅ M
elfilspd.f ⊢ φ → F : I ⟶ B
elfilspd.m ⊢ φ → M ∈ LMod
elfilspd.i ⊢ φ → I ∈ Fin
Assertion elfilspd ⊢ φ → X ∈ N ⁡ F I ↔ ∃ f ∈ K I X = ∑ M f · ˙ f F

Proof

Step Hyp Ref Expression
1 ellspd.n ⊢ N = LSpan ⁡ M
2 ellspd.v ⊢ B = Base M
3 ellspd.k ⊢ K = Base S
4 ellspd.s ⊢ S = Scalar ⁡ M
5 ellspd.z ⊢ 0 ˙ = 0 S
6 ellspd.t ⊢ · ˙ = ⋅ M
7 elfilspd.f ⊢ φ → F : I ⟶ B
8 elfilspd.m ⊢ φ → M ∈ LMod
9 elfilspd.i ⊢ φ → I ∈ Fin
10 1 2 3 4 5 6 7 8 9 ellspd ⊢ φ → X ∈ N ⁡ F I ↔ ∃ f ∈ K I finSupp 0 ˙⁡ f ∧ X = ∑ M f · ˙ f F
11 elmapi ⊢ f ∈ K I → f : I ⟶ K
12 11 adantl ⊢ φ ∧ f ∈ K I → f : I ⟶ K
13 9 adantr ⊢ φ ∧ f ∈ K I → I ∈ Fin
14 5 fvexi ⊢ 0 ˙ ∈ V
15 14 a1i ⊢ φ ∧ f ∈ K I → 0 ˙ ∈ V
16 12 13 15 fdmfifsupp ⊢ φ ∧ f ∈ K I → finSupp 0 ˙⁡ f
17 16 biantrurd ⊢ φ ∧ f ∈ K I → X = ∑ M f · ˙ f F ↔ finSupp 0 ˙⁡ f ∧ X = ∑ M f · ˙ f F
18 17 rexbidva ⊢ φ → ∃ f ∈ K I X = ∑ M f · ˙ f F ↔ ∃ f ∈ K I finSupp 0 ˙⁡ f ∧ X = ∑ M f · ˙ f F
19 10 18 bitr4d ⊢ φ → X ∈ N ⁡ F I ↔ ∃ f ∈ K I X = ∑ M f · ˙ f F