Metamath Proof Explorer

Theorem islinds

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

Ref Expression
Hypothesis islinds.b 
|- B = ( Base ` W )
Assertion islinds 
|- ( W e. V -> ( X e. ( LIndS ` W ) <-> ( X C_ B /\ ( _I |` X ) LIndF W ) ) )

Proof

Step Hyp Ref Expression
1 islinds.b 
 |-  B = ( Base ` W )
2 elex 
 |-  ( W e. V -> W e. _V )
3 fveq2 
 |-  ( w = W -> ( Base ` w ) = ( Base ` W ) )
4 3 pweqd 
 |-  ( w = W -> ~P ( Base ` w ) = ~P ( Base ` W ) )
5 breq2 
 |-  ( w = W -> ( ( _I |` s ) LIndF w <-> ( _I |` s ) LIndF W ) )
6 4 5 rabeqbidv 
 |-  ( w = W -> { s e. ~P ( Base ` w ) | ( _I |` s ) LIndF w } = { s e. ~P ( Base ` W ) | ( _I |` s ) LIndF W } )
7 df-linds 
 |-  LIndS = ( w e. _V |-> { s e. ~P ( Base ` w ) | ( _I |` s ) LIndF w } )
8 fvex 
 |-  ( Base ` W ) e. _V
9 8 pwex 
 |-  ~P ( Base ` W ) e. _V
10 9 rabex 
 |-  { s e. ~P ( Base ` W ) | ( _I |` s ) LIndF W } e. _V
11 6 7 10 fvmpt 
 |-  ( W e. _V -> ( LIndS ` W ) = { s e. ~P ( Base ` W ) | ( _I |` s ) LIndF W } )
12 2 11 syl 
 |-  ( W e. V -> ( LIndS ` W ) = { s e. ~P ( Base ` W ) | ( _I |` s ) LIndF W } )
13 12 eleq2d 
 |-  ( W e. V -> ( X e. ( LIndS ` W ) <-> X e. { s e. ~P ( Base ` W ) | ( _I |` s ) LIndF W } ) )
14 reseq2 
 |-  ( s = X -> ( _I |` s ) = ( _I |` X ) )
15 14 breq1d 
 |-  ( s = X -> ( ( _I |` s ) LIndF W <-> ( _I |` X ) LIndF W ) )
16 15 elrab 
 |-  ( X e. { s e. ~P ( Base ` W ) | ( _I |` s ) LIndF W } <-> ( X e. ~P ( Base ` W ) /\ ( _I |` X ) LIndF W ) )
17 13 16 bitrdi 
 |-  ( W e. V -> ( X e. ( LIndS ` W ) <-> ( X e. ~P ( Base ` W ) /\ ( _I |` X ) LIndF W ) ) )
18 8 elpw2 
 |-  ( X e. ~P ( Base ` W ) <-> X C_ ( Base ` W ) )
19 1 sseq2i 
 |-  ( X C_ B <-> X C_ ( Base ` W ) )
20 18 19 bitr4i 
 |-  ( X e. ~P ( Base ` W ) <-> X C_ B )
21 20 anbi1i 
 |-  ( ( X e. ~P ( Base ` W ) /\ ( _I |` X ) LIndF W ) <-> ( X C_ B /\ ( _I |` X ) LIndF W ) )
22 17 21 bitrdi 
 |-  ( W e. V -> ( X e. ( LIndS ` W ) <-> ( X C_ B /\ ( _I |` X ) LIndF W ) ) )