Metamath Proof Explorer

Theorem lbsss

Description: A basis is a set of vectors. (Contributed by Mario Carneiro, 24-Jun-2014)

Ref Expression
Hypotheses lbsss.v ⊢ V = Base W
lbsss.j ⊢ J = LBasis ⁡ W
Assertion lbsss ⊢ B ∈ J → B ⊆ V

Proof

Step Hyp Ref Expression
1 lbsss.v ⊢ V = Base W
2 lbsss.j ⊢ J = LBasis ⁡ W
3 elfvdm ⊢ B ∈ LBasis ⁡ W → W ∈ dom ⁡ LBasis
4 3 2 eleq2s ⊢ B ∈ J → W ∈ dom ⁡ LBasis
5 eqid ⊢ Scalar ⁡ W = Scalar ⁡ W
6 eqid ⊢ ⋅ W = ⋅ W
7 eqid ⊢ Base Scalar ⁡ W = Base Scalar ⁡ W
8 eqid ⊢ LSpan ⁡ W = LSpan ⁡ W
9 eqid ⊢ 0 Scalar ⁡ W = 0 Scalar ⁡ W
10 1 5 6 7 2 8 9 islbs ⊢ W ∈ dom ⁡ LBasis → B ∈ J ↔ B ⊆ V ∧ LSpan ⁡ W ⁡ B = V ∧ ∀ x ∈ B ∀ y ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W ¬ y ⋅ W x ∈ LSpan ⁡ W ⁡ B ∖ x
11 4 10 syl ⊢ B ∈ J → B ∈ J ↔ B ⊆ V ∧ LSpan ⁡ W ⁡ B = V ∧ ∀ x ∈ B ∀ y ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W ¬ y ⋅ W x ∈ LSpan ⁡ W ⁡ B ∖ x
12 11 ibi ⊢ B ∈ J → B ⊆ V ∧ LSpan ⁡ W ⁡ B = V ∧ ∀ x ∈ B ∀ y ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W ¬ y ⋅ W x ∈ LSpan ⁡ W ⁡ B ∖ x
13 12 simp1d ⊢ B ∈ J → B ⊆ V