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 biimpri 
 |-  ( ( A e. K /\ A =/= .0. ) -> A e. ( K \ { .0. } ) )
9 8 adantl 
 |-  ( ( ( F e. ( LIndS ` W ) /\ E e. F ) /\ ( A e. K /\ A =/= .0. ) ) -> A e. ( K \ { .0. } ) )
10 elfvdm 
 |-  ( F e. ( LIndS ` W ) -> W e. dom LIndS )
11 eqid 
 |-  ( Base ` W ) = ( Base ` W )
12 11 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 } ) ) ) ) )
13 10 12 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 } ) ) ) ) )
14 13 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 } ) ) ) )
15 14 simprd 
 |-  ( F e. ( LIndS ` W ) -> A. e e. F A. a e. ( K \ { .0. } ) -. ( a .x. e ) e. ( N ` ( F \ { e } ) ) )
16 15 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 } ) ) )
17 oveq2 
 |-  ( e = E -> ( a .x. e ) = ( a .x. E ) )
18 sneq 
 |-  ( e = E -> { e } = { E } )
19 18 difeq2d 
 |-  ( e = E -> ( F \ { e } ) = ( F \ { E } ) )
20 19 fveq2d 
 |-  ( e = E -> ( N ` ( F \ { e } ) ) = ( N ` ( F \ { E } ) ) )
21 17 20 eleq12d 
 |-  ( e = E -> ( ( a .x. e ) e. ( N ` ( F \ { e } ) ) <-> ( a .x. E ) e. ( N ` ( F \ { E } ) ) ) )
22 21 notbid 
 |-  ( e = E -> ( -. ( a .x. e ) e. ( N ` ( F \ { e } ) ) <-> -. ( a .x. E ) e. ( N ` ( F \ { E } ) ) ) )
23 oveq1 
 |-  ( a = A -> ( a .x. E ) = ( A .x. E ) )
24 23 eleq1d 
 |-  ( a = A -> ( ( a .x. E ) e. ( N ` ( F \ { E } ) ) <-> ( A .x. E ) e. ( N ` ( F \ { E } ) ) ) )
25 24 notbid 
 |-  ( a = A -> ( -. ( a .x. E ) e. ( N ` ( F \ { E } ) ) <-> -. ( A .x. E ) e. ( N ` ( F \ { E } ) ) ) )
26 22 25 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 } ) ) )
27 6 9 16 26 syl21anc 
 |-  ( ( ( F e. ( LIndS ` W ) /\ E e. F ) /\ ( A e. K /\ A =/= .0. ) ) -> -. ( A .x. E ) e. ( N ` ( F \ { E } ) ) )