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 ) |