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=BaseW
lbsss.j ⊢J=LBasis⁡W
Assertion lbsss ⊢B∈J→B⊆V

Proof

Step Hyp Ref Expression
1 lbsss.v ⊢V=BaseW
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 ⊢BaseScalar⁡W=BaseScalar⁡W
8 eqid ⊢LSpan⁡W=LSpan⁡W
9 eqid ⊢0Scalar⁡W=0Scalar⁡W
10 1 5 6 7 2 8 9 islbs ⊢W∈dom⁡LBasis→B∈J↔B⊆V∧LSpan⁡W⁡B=V∧∀x∈B∀y∈BaseScalar⁡W∖0Scalar⁡W¬y⋅Wx∈LSpan⁡W⁡B∖x
11 4 10 syl ⊢B∈J→B∈J↔B⊆V∧LSpan⁡W⁡B=V∧∀x∈B∀y∈BaseScalar⁡W∖0Scalar⁡W¬y⋅Wx∈LSpan⁡W⁡B∖x
12 11 ibi ⊢B∈J→B⊆V∧LSpan⁡W⁡B=V∧∀x∈B∀y∈BaseScalar⁡W∖0Scalar⁡W¬y⋅Wx∈LSpan⁡W⁡B∖x
13 12 simp1d ⊢B∈J→B⊆V