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 e. J -> B C_ V )

Proof

Step Hyp Ref Expression
1 lbsss.v
 |-  V = ( Base ` W )
2 lbsss.j
 |-  J = ( LBasis ` W )
3 elfvdm
 |-  ( B e. ( LBasis ` W ) -> W e. dom LBasis )
4 3 2 eleq2s
 |-  ( B e. J -> W e. dom LBasis )
5 eqid
 |-  ( Scalar ` W ) = ( Scalar ` W )
6 eqid
 |-  ( .s ` W ) = ( .s ` W )
7 eqid
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
8 eqid
 |-  ( LSpan ` W ) = ( LSpan ` W )
9 eqid
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
10 1 5 6 7 2 8 9 islbs
 |-  ( W e. dom LBasis -> ( B e. J <-> ( B C_ V /\ ( ( LSpan ` W ) ` B ) = V /\ A. x e. B A. y e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( y ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( B \ { x } ) ) ) ) )
11 4 10 syl
 |-  ( B e. J -> ( B e. J <-> ( B C_ V /\ ( ( LSpan ` W ) ` B ) = V /\ A. x e. B A. y e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( y ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( B \ { x } ) ) ) ) )
12 11 ibi
 |-  ( B e. J -> ( B C_ V /\ ( ( LSpan ` W ) ` B ) = V /\ A. x e. B A. y e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( y ( .s ` W ) x ) e. ( ( LSpan ` W ) ` ( B \ { x } ) ) ) )
13 12 simp1d
 |-  ( B e. J -> B C_ V )