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 = ( Base ` W )
lbsss.j 
|- J = ( LBasis ` W )
lbssp.n 
|- N = ( LSpan ` W )
Assertion lbssp 
|- ( B e. J -> ( N ` B ) = V )

Proof

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