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 )