This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem islinds2

Description: Expanded property of an independent set 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 islinds2 
|- ( W e. Y -> ( F e. ( LIndS ` W ) <-> ( F C_ B /\ A. x e. F A. k e. ( N \ { .0. } ) -. ( k .x. x ) e. ( K ` ( 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 1 islinds 
 |-  ( W e. Y -> ( F e. ( LIndS ` W ) <-> ( F C_ B /\ ( _I |` F ) LIndF W ) ) )
8 1 fvexi 
 |-  B e. _V
9 8 ssex 
 |-  ( F C_ B -> F e. _V )
10 9 adantl 
 |-  ( ( W e. Y /\ F C_ B ) -> F e. _V )
11 resiexg 
 |-  ( F e. _V -> ( _I |` F ) e. _V )
12 10 11 syl 
 |-  ( ( W e. Y /\ F C_ B ) -> ( _I |` F ) e. _V )
13 1 2 3 4 5 6 islindf 
 |-  ( ( W e. Y /\ ( _I |` F ) e. _V ) -> ( ( _I |` F ) LIndF W <-> ( ( _I |` F ) : dom ( _I |` F ) --> B /\ A. x e. dom ( _I |` F ) A. k e. ( N \ { .0. } ) -. ( k .x. ( ( _I |` F ) ` x ) ) e. ( K ` ( ( _I |` F ) " ( dom ( _I |` F ) \ { x } ) ) ) ) ) )
14 12 13 syldan 
 |-  ( ( W e. Y /\ F C_ B ) -> ( ( _I |` F ) LIndF W <-> ( ( _I |` F ) : dom ( _I |` F ) --> B /\ A. x e. dom ( _I |` F ) A. k e. ( N \ { .0. } ) -. ( k .x. ( ( _I |` F ) ` x ) ) e. ( K ` ( ( _I |` F ) " ( dom ( _I |` F ) \ { x } ) ) ) ) ) )
15 14 pm5.32da 
 |-  ( W e. Y -> ( ( F C_ B /\ ( _I |` F ) LIndF W ) <-> ( F C_ B /\ ( ( _I |` F ) : dom ( _I |` F ) --> B /\ A. x e. dom ( _I |` F ) A. k e. ( N \ { .0. } ) -. ( k .x. ( ( _I |` F ) ` x ) ) e. ( K ` ( ( _I |` F ) " ( dom ( _I |` F ) \ { x } ) ) ) ) ) ) )
16 dmresi 
 |-  dom ( _I |` F ) = F
17 16 raleqi 
 |-  ( A. x e. dom ( _I |` F ) A. k e. ( N \ { .0. } ) -. ( k .x. ( ( _I |` F ) ` x ) ) e. ( K ` ( ( _I |` F ) " ( dom ( _I |` F ) \ { x } ) ) ) <-> A. x e. F A. k e. ( N \ { .0. } ) -. ( k .x. ( ( _I |` F ) ` x ) ) e. ( K ` ( ( _I |` F ) " ( dom ( _I |` F ) \ { x } ) ) ) )
18 fvresi 
 |-  ( x e. F -> ( ( _I |` F ) ` x ) = x )
19 18 oveq2d 
 |-  ( x e. F -> ( k .x. ( ( _I |` F ) ` x ) ) = ( k .x. x ) )
20 16 difeq1i 
 |-  ( dom ( _I |` F ) \ { x } ) = ( F \ { x } )
21 20 imaeq2i 
 |-  ( ( _I |` F ) " ( dom ( _I |` F ) \ { x } ) ) = ( ( _I |` F ) " ( F \ { x } ) )
22 difss 
 |-  ( F \ { x } ) C_ F
23 resiima 
 |-  ( ( F \ { x } ) C_ F -> ( ( _I |` F ) " ( F \ { x } ) ) = ( F \ { x } ) )
24 22 23 ax-mp 
 |-  ( ( _I |` F ) " ( F \ { x } ) ) = ( F \ { x } )
25 21 24 eqtri 
 |-  ( ( _I |` F ) " ( dom ( _I |` F ) \ { x } ) ) = ( F \ { x } )
26 25 fveq2i 
 |-  ( K ` ( ( _I |` F ) " ( dom ( _I |` F ) \ { x } ) ) ) = ( K ` ( F \ { x } ) )
27 26 a1i 
 |-  ( x e. F -> ( K ` ( ( _I |` F ) " ( dom ( _I |` F ) \ { x } ) ) ) = ( K ` ( F \ { x } ) ) )
28 19 27 eleq12d 
 |-  ( x e. F -> ( ( k .x. ( ( _I |` F ) ` x ) ) e. ( K ` ( ( _I |` F ) " ( dom ( _I |` F ) \ { x } ) ) ) <-> ( k .x. x ) e. ( K ` ( F \ { x } ) ) ) )
29 28 notbid 
 |-  ( x e. F -> ( -. ( k .x. ( ( _I |` F ) ` x ) ) e. ( K ` ( ( _I |` F ) " ( dom ( _I |` F ) \ { x } ) ) ) <-> -. ( k .x. x ) e. ( K ` ( F \ { x } ) ) ) )
30 29 ralbidv 
 |-  ( x e. F -> ( A. k e. ( N \ { .0. } ) -. ( k .x. ( ( _I |` F ) ` x ) ) e. ( K ` ( ( _I |` F ) " ( dom ( _I |` F ) \ { x } ) ) ) <-> A. k e. ( N \ { .0. } ) -. ( k .x. x ) e. ( K ` ( F \ { x } ) ) ) )
31 30 ralbiia 
 |-  ( A. x e. F A. k e. ( N \ { .0. } ) -. ( k .x. ( ( _I |` F ) ` x ) ) e. ( K ` ( ( _I |` F ) " ( dom ( _I |` F ) \ { x } ) ) ) <-> A. x e. F A. k e. ( N \ { .0. } ) -. ( k .x. x ) e. ( K ` ( F \ { x } ) ) )
32 17 31 bitri 
 |-  ( A. x e. dom ( _I |` F ) A. k e. ( N \ { .0. } ) -. ( k .x. ( ( _I |` F ) ` x ) ) e. ( K ` ( ( _I |` F ) " ( dom ( _I |` F ) \ { x } ) ) ) <-> A. x e. F A. k e. ( N \ { .0. } ) -. ( k .x. x ) e. ( K ` ( F \ { x } ) ) )
33 32 anbi2i 
 |-  ( ( ( _I |` F ) : dom ( _I |` F ) --> B /\ A. x e. dom ( _I |` F ) A. k e. ( N \ { .0. } ) -. ( k .x. ( ( _I |` F ) ` x ) ) e. ( K ` ( ( _I |` F ) " ( dom ( _I |` F ) \ { x } ) ) ) ) <-> ( ( _I |` F ) : dom ( _I |` F ) --> B /\ A. x e. F A. k e. ( N \ { .0. } ) -. ( k .x. x ) e. ( K ` ( F \ { x } ) ) ) )
34 f1oi 
 |-  ( _I |` F ) : F -1-1-onto-> F
35 f1of 
 |-  ( ( _I |` F ) : F -1-1-onto-> F -> ( _I |` F ) : F --> F )
36 34 35 ax-mp 
 |-  ( _I |` F ) : F --> F
37 16 feq2i 
 |-  ( ( _I |` F ) : dom ( _I |` F ) --> F <-> ( _I |` F ) : F --> F )
38 36 37 mpbir 
 |-  ( _I |` F ) : dom ( _I |` F ) --> F
39 fss 
 |-  ( ( ( _I |` F ) : dom ( _I |` F ) --> F /\ F C_ B ) -> ( _I |` F ) : dom ( _I |` F ) --> B )
40 38 39 mpan 
 |-  ( F C_ B -> ( _I |` F ) : dom ( _I |` F ) --> B )
41 40 biantrurd 
 |-  ( F C_ B -> ( A. x e. F A. k e. ( N \ { .0. } ) -. ( k .x. x ) e. ( K ` ( F \ { x } ) ) <-> ( ( _I |` F ) : dom ( _I |` F ) --> B /\ A. x e. F A. k e. ( N \ { .0. } ) -. ( k .x. x ) e. ( K ` ( F \ { x } ) ) ) ) )
42 33 41 bitr4id 
 |-  ( F C_ B -> ( ( ( _I |` F ) : dom ( _I |` F ) --> B /\ A. x e. dom ( _I |` F ) A. k e. ( N \ { .0. } ) -. ( k .x. ( ( _I |` F ) ` x ) ) e. ( K ` ( ( _I |` F ) " ( dom ( _I |` F ) \ { x } ) ) ) ) <-> A. x e. F A. k e. ( N \ { .0. } ) -. ( k .x. x ) e. ( K ` ( F \ { x } ) ) ) )
43 42 pm5.32i 
 |-  ( ( F C_ B /\ ( ( _I |` F ) : dom ( _I |` F ) --> B /\ A. x e. dom ( _I |` F ) A. k e. ( N \ { .0. } ) -. ( k .x. ( ( _I |` F ) ` x ) ) e. ( K ` ( ( _I |` F ) " ( dom ( _I |` F ) \ { x } ) ) ) ) ) <-> ( F C_ B /\ A. x e. F A. k e. ( N \ { .0. } ) -. ( k .x. x ) e. ( K ` ( F \ { x } ) ) ) )
44 43 a1i 
 |-  ( W e. Y -> ( ( F C_ B /\ ( ( _I |` F ) : dom ( _I |` F ) --> B /\ A. x e. dom ( _I |` F ) A. k e. ( N \ { .0. } ) -. ( k .x. ( ( _I |` F ) ` x ) ) e. ( K ` ( ( _I |` F ) " ( dom ( _I |` F ) \ { x } ) ) ) ) ) <-> ( F C_ B /\ A. x e. F A. k e. ( N \ { .0. } ) -. ( k .x. x ) e. ( K ` ( F \ { x } ) ) ) ) )
45 7 15 44 3bitrd 
 |-  ( W e. Y -> ( F e. ( LIndS ` W ) <-> ( F C_ B /\ A. x e. F A. k e. ( N \ { .0. } ) -. ( k .x. x ) e. ( K ` ( F \ { x } ) ) ) ) )