Metamath Proof Explorer

Theorem islindf

Description: Property of an independent family of vectors. (Contributed by Stefan O'Rear, 24-Feb-2015)

Ref Expression
Hypotheses islindf.b 
|- B = ( Base ` W )
islindf.v 
|- .x. = ( .s ` W )
islindf.k 
|- K = ( LSpan ` W )
islindf.s 
|- S = ( Scalar ` W )
islindf.n 
|- N = ( Base ` S )
islindf.z 
|- .0. = ( 0g ` S )
Assertion islindf 
|- ( ( W e. Y /\ F e. X ) -> ( F LIndF W <-> ( F : dom F --> B /\ A. x e. dom F A. k e. ( N \ { .0. } ) -. ( k .x. ( F ` x ) ) e. ( K ` ( F " ( dom F \ { x } ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 islindf.b 
 |-  B = ( Base ` W )
2 islindf.v 
 |-  .x. = ( .s ` W )
3 islindf.k 
 |-  K = ( LSpan ` W )
4 islindf.s 
 |-  S = ( Scalar ` W )
5 islindf.n 
 |-  N = ( Base ` S )
6 islindf.z 
 |-  .0. = ( 0g ` S )
7 feq1 
 |-  ( f = F -> ( f : dom f --> ( Base ` w ) <-> F : dom f --> ( Base ` w ) ) )
8 7 adantr 
 |-  ( ( f = F /\ w = W ) -> ( f : dom f --> ( Base ` w ) <-> F : dom f --> ( Base ` w ) ) )
9 dmeq 
 |-  ( f = F -> dom f = dom F )
10 9 adantr 
 |-  ( ( f = F /\ w = W ) -> dom f = dom F )
11 fveq2 
 |-  ( w = W -> ( Base ` w ) = ( Base ` W ) )
12 11 1 eqtr4di 
 |-  ( w = W -> ( Base ` w ) = B )
13 12 adantl 
 |-  ( ( f = F /\ w = W ) -> ( Base ` w ) = B )
14 10 13 feq23d 
 |-  ( ( f = F /\ w = W ) -> ( F : dom f --> ( Base ` w ) <-> F : dom F --> B ) )
15 8 14 bitrd 
 |-  ( ( f = F /\ w = W ) -> ( f : dom f --> ( Base ` w ) <-> F : dom F --> B ) )
16 fvex 
 |-  ( Scalar ` w ) e. _V
17 fveq2 
 |-  ( s = ( Scalar ` w ) -> ( Base ` s ) = ( Base ` ( Scalar ` w ) ) )
18 fveq2 
 |-  ( s = ( Scalar ` w ) -> ( 0g ` s ) = ( 0g ` ( Scalar ` w ) ) )
19 18 sneqd 
 |-  ( s = ( Scalar ` w ) -> { ( 0g ` s ) } = { ( 0g ` ( Scalar ` w ) ) } )
20 17 19 difeq12d 
 |-  ( s = ( Scalar ` w ) -> ( ( Base ` s ) \ { ( 0g ` s ) } ) = ( ( Base ` ( Scalar ` w ) ) \ { ( 0g ` ( Scalar ` w ) ) } ) )
21 20 raleqdv 
 |-  ( s = ( Scalar ` w ) -> ( A. k e. ( ( Base ` s ) \ { ( 0g ` s ) } ) -. ( k ( .s ` w ) ( f ` x ) ) e. ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) ) <-> A. k e. ( ( Base ` ( Scalar ` w ) ) \ { ( 0g ` ( Scalar ` w ) ) } ) -. ( k ( .s ` w ) ( f ` x ) ) e. ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) ) ) )
22 21 ralbidv 
 |-  ( s = ( Scalar ` w ) -> ( A. x e. dom f A. k e. ( ( Base ` s ) \ { ( 0g ` s ) } ) -. ( k ( .s ` w ) ( f ` x ) ) e. ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) ) <-> A. x e. dom f A. k e. ( ( Base ` ( Scalar ` w ) ) \ { ( 0g ` ( Scalar ` w ) ) } ) -. ( k ( .s ` w ) ( f ` x ) ) e. ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) ) ) )
23 16 22 sbcie 
 |-  ( [. ( Scalar ` w ) / s ]. A. x e. dom f A. k e. ( ( Base ` s ) \ { ( 0g ` s ) } ) -. ( k ( .s ` w ) ( f ` x ) ) e. ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) ) <-> A. x e. dom f A. k e. ( ( Base ` ( Scalar ` w ) ) \ { ( 0g ` ( Scalar ` w ) ) } ) -. ( k ( .s ` w ) ( f ` x ) ) e. ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) ) )
24 fveq2 
 |-  ( w = W -> ( Scalar ` w ) = ( Scalar ` W ) )
25 24 4 eqtr4di 
 |-  ( w = W -> ( Scalar ` w ) = S )
26 25 fveq2d 
 |-  ( w = W -> ( Base ` ( Scalar ` w ) ) = ( Base ` S ) )
27 26 5 eqtr4di 
 |-  ( w = W -> ( Base ` ( Scalar ` w ) ) = N )
28 25 fveq2d 
 |-  ( w = W -> ( 0g ` ( Scalar ` w ) ) = ( 0g ` S ) )
29 28 6 eqtr4di 
 |-  ( w = W -> ( 0g ` ( Scalar ` w ) ) = .0. )
30 29 sneqd 
 |-  ( w = W -> { ( 0g ` ( Scalar ` w ) ) } = { .0. } )
31 27 30 difeq12d 
 |-  ( w = W -> ( ( Base ` ( Scalar ` w ) ) \ { ( 0g ` ( Scalar ` w ) ) } ) = ( N \ { .0. } ) )
32 31 adantl 
 |-  ( ( f = F /\ w = W ) -> ( ( Base ` ( Scalar ` w ) ) \ { ( 0g ` ( Scalar ` w ) ) } ) = ( N \ { .0. } ) )
33 fveq2 
 |-  ( w = W -> ( .s ` w ) = ( .s ` W ) )
34 33 2 eqtr4di 
 |-  ( w = W -> ( .s ` w ) = .x. )
35 34 adantl 
 |-  ( ( f = F /\ w = W ) -> ( .s ` w ) = .x. )
36 eqidd 
 |-  ( ( f = F /\ w = W ) -> k = k )
37 fveq1 
 |-  ( f = F -> ( f ` x ) = ( F ` x ) )
38 37 adantr 
 |-  ( ( f = F /\ w = W ) -> ( f ` x ) = ( F ` x ) )
39 35 36 38 oveq123d 
 |-  ( ( f = F /\ w = W ) -> ( k ( .s ` w ) ( f ` x ) ) = ( k .x. ( F ` x ) ) )
40 fveq2 
 |-  ( w = W -> ( LSpan ` w ) = ( LSpan ` W ) )
41 40 3 eqtr4di 
 |-  ( w = W -> ( LSpan ` w ) = K )
42 41 adantl 
 |-  ( ( f = F /\ w = W ) -> ( LSpan ` w ) = K )
43 imaeq1 
 |-  ( f = F -> ( f " ( dom f \ { x } ) ) = ( F " ( dom f \ { x } ) ) )
44 9 difeq1d 
 |-  ( f = F -> ( dom f \ { x } ) = ( dom F \ { x } ) )
45 44 imaeq2d 
 |-  ( f = F -> ( F " ( dom f \ { x } ) ) = ( F " ( dom F \ { x } ) ) )
46 43 45 eqtrd 
 |-  ( f = F -> ( f " ( dom f \ { x } ) ) = ( F " ( dom F \ { x } ) ) )
47 46 adantr 
 |-  ( ( f = F /\ w = W ) -> ( f " ( dom f \ { x } ) ) = ( F " ( dom F \ { x } ) ) )
48 42 47 fveq12d 
 |-  ( ( f = F /\ w = W ) -> ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) ) = ( K ` ( F " ( dom F \ { x } ) ) ) )
49 39 48 eleq12d 
 |-  ( ( f = F /\ w = W ) -> ( ( k ( .s ` w ) ( f ` x ) ) e. ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) ) <-> ( k .x. ( F ` x ) ) e. ( K ` ( F " ( dom F \ { x } ) ) ) ) )
50 49 notbid 
 |-  ( ( f = F /\ w = W ) -> ( -. ( k ( .s ` w ) ( f ` x ) ) e. ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) ) <-> -. ( k .x. ( F ` x ) ) e. ( K ` ( F " ( dom F \ { x } ) ) ) ) )
51 32 50 raleqbidv 
 |-  ( ( f = F /\ w = W ) -> ( A. k e. ( ( Base ` ( Scalar ` w ) ) \ { ( 0g ` ( Scalar ` w ) ) } ) -. ( k ( .s ` w ) ( f ` x ) ) e. ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) ) <-> A. k e. ( N \ { .0. } ) -. ( k .x. ( F ` x ) ) e. ( K ` ( F " ( dom F \ { x } ) ) ) ) )
52 10 51 raleqbidv 
 |-  ( ( f = F /\ w = W ) -> ( A. x e. dom f A. k e. ( ( Base ` ( Scalar ` w ) ) \ { ( 0g ` ( Scalar ` w ) ) } ) -. ( k ( .s ` w ) ( f ` x ) ) e. ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) ) <-> A. x e. dom F A. k e. ( N \ { .0. } ) -. ( k .x. ( F ` x ) ) e. ( K ` ( F " ( dom F \ { x } ) ) ) ) )
53 23 52 syl5bb 
 |-  ( ( f = F /\ w = W ) -> ( [. ( Scalar ` w ) / s ]. A. x e. dom f A. k e. ( ( Base ` s ) \ { ( 0g ` s ) } ) -. ( k ( .s ` w ) ( f ` x ) ) e. ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) ) <-> A. x e. dom F A. k e. ( N \ { .0. } ) -. ( k .x. ( F ` x ) ) e. ( K ` ( F " ( dom F \ { x } ) ) ) ) )
54 15 53 anbi12d 
 |-  ( ( f = F /\ w = W ) -> ( ( f : dom f --> ( Base ` w ) /\ [. ( Scalar ` w ) / s ]. A. x e. dom f A. k e. ( ( Base ` s ) \ { ( 0g ` s ) } ) -. ( k ( .s ` w ) ( f ` x ) ) e. ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) ) ) <-> ( F : dom F --> B /\ A. x e. dom F A. k e. ( N \ { .0. } ) -. ( k .x. ( F ` x ) ) e. ( K ` ( F " ( dom F \ { x } ) ) ) ) ) )
55 df-lindf 
 |-  LIndF = { <. f , w >. | ( f : dom f --> ( Base ` w ) /\ [. ( Scalar ` w ) / s ]. A. x e. dom f A. k e. ( ( Base ` s ) \ { ( 0g ` s ) } ) -. ( k ( .s ` w ) ( f ` x ) ) e. ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) ) ) }
56 54 55 brabga 
 |-  ( ( F e. X /\ W e. Y ) -> ( F LIndF W <-> ( F : dom F --> B /\ A. x e. dom F A. k e. ( N \ { .0. } ) -. ( k .x. ( F ` x ) ) e. ( K ` ( F " ( dom F \ { x } ) ) ) ) ) )
57 56 ancoms 
 |-  ( ( W e. Y /\ F e. X ) -> ( F LIndF W <-> ( F : dom F --> B /\ A. x e. dom F A. k e. ( N \ { .0. } ) -. ( k .x. ( F ` x ) ) e. ( K ` ( F " ( dom F \ { x } ) ) ) ) ) )