Metamath Proof Explorer

Theorem lindfind

Description: A linearly independent family 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 lindfind 
|- ( ( ( F LIndF W /\ E e. dom F ) /\ ( A e. K /\ A =/= .0. ) ) -> -. ( A .x. ( F ` E ) ) e. ( N ` ( F " ( dom 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 LIndF W /\ E e. dom F ) /\ ( A e. K /\ A =/= .0. ) ) -> E e. dom 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 LIndF W /\ E e. dom F ) /\ ( A e. K /\ A =/= .0. ) ) -> A e. ( K \ { .0. } ) )
10 simpll 
 |-  ( ( ( F LIndF W /\ E e. dom F ) /\ ( A e. K /\ A =/= .0. ) ) -> F LIndF W )
11 3 5 elbasfv 
 |-  ( A e. K -> W e. _V )
12 11 ad2antrl 
 |-  ( ( ( F LIndF W /\ E e. dom F ) /\ ( A e. K /\ A =/= .0. ) ) -> W e. _V )
13 rellindf 
 |-  Rel LIndF
14 13 brrelex1i 
 |-  ( F LIndF W -> F e. _V )
15 14 ad2antrr 
 |-  ( ( ( F LIndF W /\ E e. dom F ) /\ ( A e. K /\ A =/= .0. ) ) -> F e. _V )
16 eqid 
 |-  ( Base ` W ) = ( Base ` W )
17 16 1 2 3 5 4 islindf 
 |-  ( ( W e. _V /\ F e. _V ) -> ( F LIndF W <-> ( F : dom F --> ( Base ` W ) /\ A. e e. dom F A. a e. ( K \ { .0. } ) -. ( a .x. ( F ` e ) ) e. ( N ` ( F " ( dom F \ { e } ) ) ) ) ) )
18 12 15 17 syl2anc 
 |-  ( ( ( F LIndF W /\ E e. dom F ) /\ ( A e. K /\ A =/= .0. ) ) -> ( F LIndF W <-> ( F : dom F --> ( Base ` W ) /\ A. e e. dom F A. a e. ( K \ { .0. } ) -. ( a .x. ( F ` e ) ) e. ( N ` ( F " ( dom F \ { e } ) ) ) ) ) )
19 10 18 mpbid 
 |-  ( ( ( F LIndF W /\ E e. dom F ) /\ ( A e. K /\ A =/= .0. ) ) -> ( F : dom F --> ( Base ` W ) /\ A. e e. dom F A. a e. ( K \ { .0. } ) -. ( a .x. ( F ` e ) ) e. ( N ` ( F " ( dom F \ { e } ) ) ) ) )
20 19 simprd 
 |-  ( ( ( F LIndF W /\ E e. dom F ) /\ ( A e. K /\ A =/= .0. ) ) -> A. e e. dom F A. a e. ( K \ { .0. } ) -. ( a .x. ( F ` e ) ) e. ( N ` ( F " ( dom F \ { e } ) ) ) )
21 fveq2 
 |-  ( e = E -> ( F ` e ) = ( F ` E ) )
22 21 oveq2d 
 |-  ( e = E -> ( a .x. ( F ` e ) ) = ( a .x. ( F ` E ) ) )
23 sneq 
 |-  ( e = E -> { e } = { E } )
24 23 difeq2d 
 |-  ( e = E -> ( dom F \ { e } ) = ( dom F \ { E } ) )
25 24 imaeq2d 
 |-  ( e = E -> ( F " ( dom F \ { e } ) ) = ( F " ( dom F \ { E } ) ) )
26 25 fveq2d 
 |-  ( e = E -> ( N ` ( F " ( dom F \ { e } ) ) ) = ( N ` ( F " ( dom F \ { E } ) ) ) )
27 22 26 eleq12d 
 |-  ( e = E -> ( ( a .x. ( F ` e ) ) e. ( N ` ( F " ( dom F \ { e } ) ) ) <-> ( a .x. ( F ` E ) ) e. ( N ` ( F " ( dom F \ { E } ) ) ) ) )
28 27 notbid 
 |-  ( e = E -> ( -. ( a .x. ( F ` e ) ) e. ( N ` ( F " ( dom F \ { e } ) ) ) <-> -. ( a .x. ( F ` E ) ) e. ( N ` ( F " ( dom F \ { E } ) ) ) ) )
29 oveq1 
 |-  ( a = A -> ( a .x. ( F ` E ) ) = ( A .x. ( F ` E ) ) )
30 29 eleq1d 
 |-  ( a = A -> ( ( a .x. ( F ` E ) ) e. ( N ` ( F " ( dom F \ { E } ) ) ) <-> ( A .x. ( F ` E ) ) e. ( N ` ( F " ( dom F \ { E } ) ) ) ) )
31 30 notbid 
 |-  ( a = A -> ( -. ( a .x. ( F ` E ) ) e. ( N ` ( F " ( dom F \ { E } ) ) ) <-> -. ( A .x. ( F ` E ) ) e. ( N ` ( F " ( dom F \ { E } ) ) ) ) )
32 28 31 rspc2va 
 |-  ( ( ( E e. dom F /\ A e. ( K \ { .0. } ) ) /\ A. e e. dom F A. a e. ( K \ { .0. } ) -. ( a .x. ( F ` e ) ) e. ( N ` ( F " ( dom F \ { e } ) ) ) ) -> -. ( A .x. ( F ` E ) ) e. ( N ` ( F " ( dom F \ { E } ) ) ) )
33 6 9 20 32 syl21anc 
 |-  ( ( ( F LIndF W /\ E e. dom F ) /\ ( A e. K /\ A =/= .0. ) ) -> -. ( A .x. ( F ` E ) ) e. ( N ` ( F " ( dom F \ { E } ) ) ) )