Metamath Proof Explorer


Theorem lbssp

Description: The span of a basis is the whole space. (Contributed by Mario Carneiro, 24-Jun-2014)

Ref Expression
Hypotheses lbsss.v V=BaseW
lbsss.j J=LBasisW
lbssp.n N=LSpanW
Assertion lbssp BJNB=V

Proof

Step Hyp Ref Expression
1 lbsss.v V=BaseW
2 lbsss.j J=LBasisW
3 lbssp.n N=LSpanW
4 elfvdm BLBasisWWdomLBasis
5 4 2 eleq2s BJWdomLBasis
6 eqid ScalarW=ScalarW
7 eqid W=W
8 eqid BaseScalarW=BaseScalarW
9 eqid 0ScalarW=0ScalarW
10 1 6 7 8 2 3 9 islbs WdomLBasisBJBVNB=VxByBaseScalarW0ScalarW¬yWxNBx
11 5 10 syl BJBJBVNB=VxByBaseScalarW0ScalarW¬yWxNBx
12 11 ibi BJBVNB=VxByBaseScalarW0ScalarW¬yWxNBx
13 12 simp2d BJNB=V