Metamath Proof Explorer

Theorem lbsext

Description: For any linearly independent subset C of V , there is a basis containing the vectors in C . (Contributed by Mario Carneiro, 25-Jun-2014) (Revised by Mario Carneiro, 17-May-2015)

Ref Expression
Hypotheses lbsex.j ⊢ J = LBasis ⁡ W
lbsex.v ⊢ V = Base W
lbsex.n ⊢ N = LSpan ⁡ W
Assertion lbsext ⊢ W ∈ LVec ∧ C ⊆ V ∧ ∀ x ∈ C ¬ x ∈ N ⁡ C ∖ x → ∃ s ∈ J C ⊆ s

Proof

Step Hyp Ref Expression
1 lbsex.j ⊢ J = LBasis ⁡ W
2 lbsex.v ⊢ V = Base W
3 lbsex.n ⊢ N = LSpan ⁡ W
4 2 fvexi ⊢ V ∈ V
5 4 pwex ⊢ 𝒫 V ∈ V
6 numth3 ⊢ 𝒫 V ∈ V → 𝒫 V ∈ dom ⁡ card
7 5 6 ax-mp ⊢ 𝒫 V ∈ dom ⁡ card
8 7 jctr ⊢ W ∈ LVec → W ∈ LVec ∧ 𝒫 V ∈ dom ⁡ card
9 1 2 3 lbsextg ⊢ W ∈ LVec ∧ 𝒫 V ∈ dom ⁡ card ∧ C ⊆ V ∧ ∀ x ∈ C ¬ x ∈ N ⁡ C ∖ x → ∃ s ∈ J C ⊆ s
10 8 9 syl3an1 ⊢ W ∈ LVec ∧ C ⊆ V ∧ ∀ x ∈ C ¬ x ∈ N ⁡ C ∖ x → ∃ s ∈ J C ⊆ s