Metamath Proof Explorer

Theorem lsslss

Description: The subspaces of a subspace are the smaller subspaces. (Contributed by Stefan O'Rear, 12-Dec-2014)

Ref Expression
Hypotheses lsslss.x 
|- X = ( W |`s U )
lsslss.s 
|- S = ( LSubSp ` W )
lsslss.t 
|- T = ( LSubSp ` X )
Assertion lsslss 
|- ( ( W e. LMod /\ U e. S ) -> ( V e. T <-> ( V e. S /\ V C_ U ) ) )

Proof

Step Hyp Ref Expression
1 lsslss.x 
 |-  X = ( W |`s U )
2 lsslss.s 
 |-  S = ( LSubSp ` W )
3 lsslss.t 
 |-  T = ( LSubSp ` X )
4 1 2 lsslmod 
 |-  ( ( W e. LMod /\ U e. S ) -> X e. LMod )
5 eqid 
 |-  ( X |`s V ) = ( X |`s V )
6 eqid 
 |-  ( Base ` X ) = ( Base ` X )
7 5 6 3 islss3 
 |-  ( X e. LMod -> ( V e. T <-> ( V C_ ( Base ` X ) /\ ( X |`s V ) e. LMod ) ) )
8 4 7 syl 
 |-  ( ( W e. LMod /\ U e. S ) -> ( V e. T <-> ( V C_ ( Base ` X ) /\ ( X |`s V ) e. LMod ) ) )
9 eqid 
 |-  ( Base ` W ) = ( Base ` W )
10 9 2 lssss 
 |-  ( U e. S -> U C_ ( Base ` W ) )
11 10 adantl 
 |-  ( ( W e. LMod /\ U e. S ) -> U C_ ( Base ` W ) )
12 1 9 ressbas2 
 |-  ( U C_ ( Base ` W ) -> U = ( Base ` X ) )
13 11 12 syl 
 |-  ( ( W e. LMod /\ U e. S ) -> U = ( Base ` X ) )
14 13 sseq2d 
 |-  ( ( W e. LMod /\ U e. S ) -> ( V C_ U <-> V C_ ( Base ` X ) ) )
15 14 anbi1d 
 |-  ( ( W e. LMod /\ U e. S ) -> ( ( V C_ U /\ ( X |`s V ) e. LMod ) <-> ( V C_ ( Base ` X ) /\ ( X |`s V ) e. LMod ) ) )
16 sstr2 
 |-  ( V C_ U -> ( U C_ ( Base ` W ) -> V C_ ( Base ` W ) ) )
17 11 16 mpan9 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ V C_ U ) -> V C_ ( Base ` W ) )
18 17 biantrurd 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ V C_ U ) -> ( ( W |`s V ) e. LMod <-> ( V C_ ( Base ` W ) /\ ( W |`s V ) e. LMod ) ) )
19 1 oveq1i 
 |-  ( X |`s V ) = ( ( W |`s U ) |`s V )
20 ressabs 
 |-  ( ( U e. S /\ V C_ U ) -> ( ( W |`s U ) |`s V ) = ( W |`s V ) )
21 20 adantll 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ V C_ U ) -> ( ( W |`s U ) |`s V ) = ( W |`s V ) )
22 19 21 syl5eq 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ V C_ U ) -> ( X |`s V ) = ( W |`s V ) )
23 22 eleq1d 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ V C_ U ) -> ( ( X |`s V ) e. LMod <-> ( W |`s V ) e. LMod ) )
24 eqid 
 |-  ( W |`s V ) = ( W |`s V )
25 24 9 2 islss3 
 |-  ( W e. LMod -> ( V e. S <-> ( V C_ ( Base ` W ) /\ ( W |`s V ) e. LMod ) ) )
26 25 ad2antrr 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ V C_ U ) -> ( V e. S <-> ( V C_ ( Base ` W ) /\ ( W |`s V ) e. LMod ) ) )
27 18 23 26 3bitr4d 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ V C_ U ) -> ( ( X |`s V ) e. LMod <-> V e. S ) )
28 27 pm5.32da 
 |-  ( ( W e. LMod /\ U e. S ) -> ( ( V C_ U /\ ( X |`s V ) e. LMod ) <-> ( V C_ U /\ V e. S ) ) )
29 28 biancomd 
 |-  ( ( W e. LMod /\ U e. S ) -> ( ( V C_ U /\ ( X |`s V ) e. LMod ) <-> ( V e. S /\ V C_ U ) ) )
30 8 15 29 3bitr2d 
 |-  ( ( W e. LMod /\ U e. S ) -> ( V e. T <-> ( V e. S /\ V C_ U ) ) )