Metamath Proof Explorer

Theorem lsslinds

Description: Linear independence is unchanged by working in a subspace. (Contributed by Stefan O'Rear, 24-Feb-2015)

Ref Expression
Hypotheses lsslindf.u 
|- U = ( LSubSp ` W )
lsslindf.x 
|- X = ( W |`s S )
Assertion lsslinds 
|- ( ( W e. LMod /\ S e. U /\ F C_ S ) -> ( F e. ( LIndS ` X ) <-> F e. ( LIndS ` W ) ) )

Proof

Step Hyp Ref Expression
1 lsslindf.u 
 |-  U = ( LSubSp ` W )
2 lsslindf.x 
 |-  X = ( W |`s S )
3 eqid 
 |-  ( Base ` W ) = ( Base ` W )
4 3 1 lssss 
 |-  ( S e. U -> S C_ ( Base ` W ) )
5 2 3 ressbas2 
 |-  ( S C_ ( Base ` W ) -> S = ( Base ` X ) )
6 4 5 syl 
 |-  ( S e. U -> S = ( Base ` X ) )
7 6 3ad2ant2 
 |-  ( ( W e. LMod /\ S e. U /\ F C_ S ) -> S = ( Base ` X ) )
8 7 sseq2d 
 |-  ( ( W e. LMod /\ S e. U /\ F C_ S ) -> ( F C_ S <-> F C_ ( Base ` X ) ) )
9 4 3ad2ant2 
 |-  ( ( W e. LMod /\ S e. U /\ F C_ S ) -> S C_ ( Base ` W ) )
10 sstr2 
 |-  ( F C_ S -> ( S C_ ( Base ` W ) -> F C_ ( Base ` W ) ) )
11 9 10 mpan9 
 |-  ( ( ( W e. LMod /\ S e. U /\ F C_ S ) /\ F C_ S ) -> F C_ ( Base ` W ) )
12 simpl3 
 |-  ( ( ( W e. LMod /\ S e. U /\ F C_ S ) /\ F C_ ( Base ` W ) ) -> F C_ S )
13 11 12 impbida 
 |-  ( ( W e. LMod /\ S e. U /\ F C_ S ) -> ( F C_ S <-> F C_ ( Base ` W ) ) )
14 8 13 bitr3d 
 |-  ( ( W e. LMod /\ S e. U /\ F C_ S ) -> ( F C_ ( Base ` X ) <-> F C_ ( Base ` W ) ) )
15 rnresi 
 |-  ran ( _I |` F ) = F
16 15 sseq1i 
 |-  ( ran ( _I |` F ) C_ S <-> F C_ S )
17 1 2 lsslindf 
 |-  ( ( W e. LMod /\ S e. U /\ ran ( _I |` F ) C_ S ) -> ( ( _I |` F ) LIndF X <-> ( _I |` F ) LIndF W ) )
18 16 17 syl3an3br 
 |-  ( ( W e. LMod /\ S e. U /\ F C_ S ) -> ( ( _I |` F ) LIndF X <-> ( _I |` F ) LIndF W ) )
19 14 18 anbi12d 
 |-  ( ( W e. LMod /\ S e. U /\ F C_ S ) -> ( ( F C_ ( Base ` X ) /\ ( _I |` F ) LIndF X ) <-> ( F C_ ( Base ` W ) /\ ( _I |` F ) LIndF W ) ) )
20 2 ovexi 
 |-  X e. _V
21 eqid 
 |-  ( Base ` X ) = ( Base ` X )
22 21 islinds 
 |-  ( X e. _V -> ( F e. ( LIndS ` X ) <-> ( F C_ ( Base ` X ) /\ ( _I |` F ) LIndF X ) ) )
23 20 22 mp1i 
 |-  ( ( W e. LMod /\ S e. U /\ F C_ S ) -> ( F e. ( LIndS ` X ) <-> ( F C_ ( Base ` X ) /\ ( _I |` F ) LIndF X ) ) )
24 3 islinds 
 |-  ( W e. LMod -> ( F e. ( LIndS ` W ) <-> ( F C_ ( Base ` W ) /\ ( _I |` F ) LIndF W ) ) )
25 24 3ad2ant1 
 |-  ( ( W e. LMod /\ S e. U /\ F C_ S ) -> ( F e. ( LIndS ` W ) <-> ( F C_ ( Base ` W ) /\ ( _I |` F ) LIndF W ) ) )
26 19 23 25 3bitr4d 
 |-  ( ( W e. LMod /\ S e. U /\ F C_ S ) -> ( F e. ( LIndS ` X ) <-> F e. ( LIndS ` W ) ) )