Metamath Proof Explorer

Theorem lindsind

Description: A linearly independent set is independent: no nonzero element multiple can be expressed as a linear combination of the others. (Contributed by Stefan O'Rear, 24-Feb-2015)

Ref Expression
Hypotheses lindfind.s 
|- .x. = ( .s ` W )
lindfind.n 
|- N = ( LSpan ` W )
lindfind.l 
|- L = ( Scalar ` W )
lindfind.z 
|- .0. = ( 0g ` L )
lindfind.k 
|- K = ( Base ` L )
Assertion lindsind 
|- ( ( ( F e. ( LIndS ` W ) /\ E e. F ) /\ ( A e. K /\ A =/= .0. ) ) -> -. ( A .x. E ) e. ( N ` ( F \ { E } ) ) )

Proof

Step Hyp Ref Expression
1 lindfind.s 
 |-  .x. = ( .s ` W )
2 lindfind.n 
 |-  N = ( LSpan ` W )
3 lindfind.l 
 |-  L = ( Scalar ` W )
4 lindfind.z 
 |-  .0. = ( 0g ` L )
5 lindfind.k 
 |-  K = ( Base ` L )
6 simplr 
 |-  ( ( ( F e. ( LIndS ` W ) /\ E e. F ) /\ ( A e. K /\ A =/= .0. ) ) -> E e. F )
7 eldifsn 
 |-  ( A e. ( K \ { .0. } ) <-> ( A e. K /\ A =/= .0. ) )
8 7 bilanri 
 |-  ( ( ( F e. ( LIndS ` W ) /\ E e. F ) /\ ( A e. K /\ A =/= .0. ) ) -> A e. ( K \ { .0. } ) )
9 elfvdm 
 |-  ( F e. ( LIndS ` W ) -> W e. dom LIndS )
10 eqid 
 |-  ( Base ` W ) = ( Base ` W )
11 10 1 2 3 5 4 islinds2 
 |-  ( W e. dom LIndS -> ( F e. ( LIndS ` W ) <-> ( F C_ ( Base ` W ) /\ A. e e. F A. a e. ( K \ { .0. } ) -. ( a .x. e ) e. ( N ` ( F \ { e } ) ) ) ) )
12 9 11 syl 
 |-  ( F e. ( LIndS ` W ) -> ( F e. ( LIndS ` W ) <-> ( F C_ ( Base ` W ) /\ A. e e. F A. a e. ( K \ { .0. } ) -. ( a .x. e ) e. ( N ` ( F \ { e } ) ) ) ) )
13 12 ibi 
 |-  ( F e. ( LIndS ` W ) -> ( F C_ ( Base ` W ) /\ A. e e. F A. a e. ( K \ { .0. } ) -. ( a .x. e ) e. ( N ` ( F \ { e } ) ) ) )
14 13 simprd 
 |-  ( F e. ( LIndS ` W ) -> A. e e. F A. a e. ( K \ { .0. } ) -. ( a .x. e ) e. ( N ` ( F \ { e } ) ) )
15 14 ad2antrr 
 |-  ( ( ( F e. ( LIndS ` W ) /\ E e. F ) /\ ( A e. K /\ A =/= .0. ) ) -> A. e e. F A. a e. ( K \ { .0. } ) -. ( a .x. e ) e. ( N ` ( F \ { e } ) ) )
16 oveq2 
 |-  ( e = E -> ( a .x. e ) = ( a .x. E ) )
17 sneq 
 |-  ( e = E -> { e } = { E } )
18 17 difeq2d 
 |-  ( e = E -> ( F \ { e } ) = ( F \ { E } ) )
19 18 fveq2d 
 |-  ( e = E -> ( N ` ( F \ { e } ) ) = ( N ` ( F \ { E } ) ) )
20 16 19 eleq12d 
 |-  ( e = E -> ( ( a .x. e ) e. ( N ` ( F \ { e } ) ) <-> ( a .x. E ) e. ( N ` ( F \ { E } ) ) ) )
21 20 notbid 
 |-  ( e = E -> ( -. ( a .x. e ) e. ( N ` ( F \ { e } ) ) <-> -. ( a .x. E ) e. ( N ` ( F \ { E } ) ) ) )
22 oveq1 
 |-  ( a = A -> ( a .x. E ) = ( A .x. E ) )
23 22 eleq1d 
 |-  ( a = A -> ( ( a .x. E ) e. ( N ` ( F \ { E } ) ) <-> ( A .x. E ) e. ( N ` ( F \ { E } ) ) ) )
24 23 notbid 
 |-  ( a = A -> ( -. ( a .x. E ) e. ( N ` ( F \ { E } ) ) <-> -. ( A .x. E ) e. ( N ` ( F \ { E } ) ) ) )
25 21 24 rspc2va 
 |-  ( ( ( E e. F /\ A e. ( K \ { .0. } ) ) /\ A. e e. F A. a e. ( K \ { .0. } ) -. ( a .x. e ) e. ( N ` ( F \ { e } ) ) ) -> -. ( A .x. E ) e. ( N ` ( F \ { E } ) ) )
26 6 8 15 25 syl21anc 
 |-  ( ( ( F e. ( LIndS ` W ) /\ E e. F ) /\ ( A e. K /\ A =/= .0. ) ) -> -. ( A .x. E ) e. ( N ` ( F \ { E } ) ) )