Metamath Proof Explorer

Theorem islindf2

Description: Property of an independent family of vectors with prior constrained domain and codomain. (Contributed by Stefan O'Rear, 26-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 islindf2 
|- ( ( W e. Y /\ I e. X /\ F : I --> B ) -> ( F LIndF W <-> A. x e. I A. k e. ( N \ { .0. } ) -. ( k .x. ( F ` x ) ) e. ( K ` ( F " ( I \ { 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 simp1 
 |-  ( ( W e. Y /\ I e. X /\ F : I --> B ) -> W e. Y )
8 simp3 
 |-  ( ( W e. Y /\ I e. X /\ F : I --> B ) -> F : I --> B )
9 simp2 
 |-  ( ( W e. Y /\ I e. X /\ F : I --> B ) -> I e. X )
10 8 9 fexd 
 |-  ( ( W e. Y /\ I e. X /\ F : I --> B ) -> F e. _V )
11 1 2 3 4 5 6 islindf 
 |-  ( ( W e. Y /\ F e. _V ) -> ( 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 } ) ) ) ) ) )
12 7 10 11 syl2anc 
 |-  ( ( W e. Y /\ I e. X /\ F : I --> B ) -> ( 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 } ) ) ) ) ) )
13 ffdm 
 |-  ( F : I --> B -> ( F : dom F --> B /\ dom F C_ I ) )
14 13 simpld 
 |-  ( F : I --> B -> F : dom F --> B )
15 14 3ad2ant3 
 |-  ( ( W e. Y /\ I e. X /\ F : I --> B ) -> F : dom F --> B )
16 15 biantrurd 
 |-  ( ( W e. Y /\ I e. X /\ F : I --> B ) -> ( A. x e. dom F A. k e. ( N \ { .0. } ) -. ( k .x. ( F ` x ) ) e. ( K ` ( 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 } ) ) ) ) ) )
17 fdm 
 |-  ( F : I --> B -> dom F = I )
18 17 3ad2ant3 
 |-  ( ( W e. Y /\ I e. X /\ F : I --> B ) -> dom F = I )
19 18 difeq1d 
 |-  ( ( W e. Y /\ I e. X /\ F : I --> B ) -> ( dom F \ { x } ) = ( I \ { x } ) )
20 19 imaeq2d 
 |-  ( ( W e. Y /\ I e. X /\ F : I --> B ) -> ( F " ( dom F \ { x } ) ) = ( F " ( I \ { x } ) ) )
21 20 fveq2d 
 |-  ( ( W e. Y /\ I e. X /\ F : I --> B ) -> ( K ` ( F " ( dom F \ { x } ) ) ) = ( K ` ( F " ( I \ { x } ) ) ) )
22 21 eleq2d 
 |-  ( ( W e. Y /\ I e. X /\ F : I --> B ) -> ( ( k .x. ( F ` x ) ) e. ( K ` ( F " ( dom F \ { x } ) ) ) <-> ( k .x. ( F ` x ) ) e. ( K ` ( F " ( I \ { x } ) ) ) ) )
23 22 notbid 
 |-  ( ( W e. Y /\ I e. X /\ F : I --> B ) -> ( -. ( k .x. ( F ` x ) ) e. ( K ` ( F " ( dom F \ { x } ) ) ) <-> -. ( k .x. ( F ` x ) ) e. ( K ` ( F " ( I \ { x } ) ) ) ) )
24 23 ralbidv 
 |-  ( ( W e. Y /\ I e. X /\ F : I --> B ) -> ( A. k e. ( N \ { .0. } ) -. ( k .x. ( F ` x ) ) e. ( K ` ( F " ( dom F \ { x } ) ) ) <-> A. k e. ( N \ { .0. } ) -. ( k .x. ( F ` x ) ) e. ( K ` ( F " ( I \ { x } ) ) ) ) )
25 18 24 raleqbidv 
 |-  ( ( W e. Y /\ I e. X /\ F : I --> B ) -> ( A. x e. dom F A. k e. ( N \ { .0. } ) -. ( k .x. ( F ` x ) ) e. ( K ` ( F " ( dom F \ { x } ) ) ) <-> A. x e. I A. k e. ( N \ { .0. } ) -. ( k .x. ( F ` x ) ) e. ( K ` ( F " ( I \ { x } ) ) ) ) )
26 12 16 25 3bitr2d 
 |-  ( ( W e. Y /\ I e. X /\ F : I --> B ) -> ( F LIndF W <-> A. x e. I A. k e. ( N \ { .0. } ) -. ( k .x. ( F ` x ) ) e. ( K ` ( F " ( I \ { x } ) ) ) ) )