Metamath Proof Explorer

Theorem lbsind

Description: A basis is linearly independent; that is, every element has a span which trivially intersects the span of the remainder of the basis. (Contributed by Mario Carneiro, 12-Jan-2015)

Ref Expression
Hypotheses lbsss.v 
|- V = ( Base ` W )
lbsss.j 
|- J = ( LBasis ` W )
lbssp.n 
|- N = ( LSpan ` W )
lbsind.f 
|- F = ( Scalar ` W )
lbsind.s 
|- .x. = ( .s ` W )
lbsind.k 
|- K = ( Base ` F )
lbsind.z 
|- .0. = ( 0g ` F )
Assertion lbsind 
|- ( ( ( B e. J /\ E e. B ) /\ ( A e. K /\ A =/= .0. ) ) -> -. ( A .x. E ) e. ( N ` ( B \ { E } ) ) )

Proof

Step Hyp Ref Expression
1 lbsss.v 
 |-  V = ( Base ` W )
2 lbsss.j 
 |-  J = ( LBasis ` W )
3 lbssp.n 
 |-  N = ( LSpan ` W )
4 lbsind.f 
 |-  F = ( Scalar ` W )
5 lbsind.s 
 |-  .x. = ( .s ` W )
6 lbsind.k 
 |-  K = ( Base ` F )
7 lbsind.z 
 |-  .0. = ( 0g ` F )
8 eldifsn 
 |-  ( A e. ( K \ { .0. } ) <-> ( A e. K /\ A =/= .0. ) )
9 elfvdm 
 |-  ( B e. ( LBasis ` W ) -> W e. dom LBasis )
10 9 2 eleq2s 
 |-  ( B e. J -> W e. dom LBasis )
11 1 4 5 6 2 3 7 islbs 
 |-  ( W e. dom LBasis -> ( B e. J <-> ( B C_ V /\ ( N ` B ) = V /\ A. x e. B A. y e. ( K \ { .0. } ) -. ( y .x. x ) e. ( N ` ( B \ { x } ) ) ) ) )
12 10 11 syl 
 |-  ( B e. J -> ( B e. J <-> ( B C_ V /\ ( N ` B ) = V /\ A. x e. B A. y e. ( K \ { .0. } ) -. ( y .x. x ) e. ( N ` ( B \ { x } ) ) ) ) )
13 12 ibi 
 |-  ( B e. J -> ( B C_ V /\ ( N ` B ) = V /\ A. x e. B A. y e. ( K \ { .0. } ) -. ( y .x. x ) e. ( N ` ( B \ { x } ) ) ) )
14 13 simp3d 
 |-  ( B e. J -> A. x e. B A. y e. ( K \ { .0. } ) -. ( y .x. x ) e. ( N ` ( B \ { x } ) ) )
15 oveq2 
 |-  ( x = E -> ( y .x. x ) = ( y .x. E ) )
16 sneq 
 |-  ( x = E -> { x } = { E } )
17 16 difeq2d 
 |-  ( x = E -> ( B \ { x } ) = ( B \ { E } ) )
18 17 fveq2d 
 |-  ( x = E -> ( N ` ( B \ { x } ) ) = ( N ` ( B \ { E } ) ) )
19 15 18 eleq12d 
 |-  ( x = E -> ( ( y .x. x ) e. ( N ` ( B \ { x } ) ) <-> ( y .x. E ) e. ( N ` ( B \ { E } ) ) ) )
20 19 notbid 
 |-  ( x = E -> ( -. ( y .x. x ) e. ( N ` ( B \ { x } ) ) <-> -. ( y .x. E ) e. ( N ` ( B \ { E } ) ) ) )
21 oveq1 
 |-  ( y = A -> ( y .x. E ) = ( A .x. E ) )
22 21 eleq1d 
 |-  ( y = A -> ( ( y .x. E ) e. ( N ` ( B \ { E } ) ) <-> ( A .x. E ) e. ( N ` ( B \ { E } ) ) ) )
23 22 notbid 
 |-  ( y = A -> ( -. ( y .x. E ) e. ( N ` ( B \ { E } ) ) <-> -. ( A .x. E ) e. ( N ` ( B \ { E } ) ) ) )
24 20 23 rspc2v 
 |-  ( ( E e. B /\ A e. ( K \ { .0. } ) ) -> ( A. x e. B A. y e. ( K \ { .0. } ) -. ( y .x. x ) e. ( N ` ( B \ { x } ) ) -> -. ( A .x. E ) e. ( N ` ( B \ { E } ) ) ) )
25 14 24 syl5com 
 |-  ( B e. J -> ( ( E e. B /\ A e. ( K \ { .0. } ) ) -> -. ( A .x. E ) e. ( N ` ( B \ { E } ) ) ) )
26 25 impl 
 |-  ( ( ( B e. J /\ E e. B ) /\ A e. ( K \ { .0. } ) ) -> -. ( A .x. E ) e. ( N ` ( B \ { E } ) ) )
27 8 26 sylan2br 
 |-  ( ( ( B e. J /\ E e. B ) /\ ( A e. K /\ A =/= .0. ) ) -> -. ( A .x. E ) e. ( N ` ( B \ { E } ) ) )