Metamath Proof Explorer

Theorem lssdimle

Description: The dimension of a linear subspace is less than or equal to the dimension of the parent vector space. This is corollary 5.4 of Lang p. 141. (Contributed by Thierry Arnoux, 20-May-2023)

Ref Expression
Hypothesis lssdimle.x 
|- X = ( W |`s U )
Assertion lssdimle 
|- ( ( W e. LVec /\ U e. ( LSubSp ` W ) ) -> ( dim ` X ) <_ ( dim ` W ) )

Proof

Step Hyp Ref Expression
1 lssdimle.x 
 |-  X = ( W |`s U )
2 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
3 1 2 lsslvec 
 |-  ( ( W e. LVec /\ U e. ( LSubSp ` W ) ) -> X e. LVec )
4 eqid 
 |-  ( LBasis ` X ) = ( LBasis ` X )
5 4 lbsex 
 |-  ( X e. LVec -> ( LBasis ` X ) =/= (/) )
6 3 5 syl 
 |-  ( ( W e. LVec /\ U e. ( LSubSp ` W ) ) -> ( LBasis ` X ) =/= (/) )
7 n0 
 |-  ( ( LBasis ` X ) =/= (/) <-> E. x x e. ( LBasis ` X ) )
8 6 7 sylib 
 |-  ( ( W e. LVec /\ U e. ( LSubSp ` W ) ) -> E. x x e. ( LBasis ` X ) )
9 hashss 
 |-  ( ( w e. ( LBasis ` W ) /\ x C_ w ) -> ( # ` x ) <_ ( # ` w ) )
10 9 adantll 
 |-  ( ( ( ( ( W e. LVec /\ U e. ( LSubSp ` W ) ) /\ x e. ( LBasis ` X ) ) /\ w e. ( LBasis ` W ) ) /\ x C_ w ) -> ( # ` x ) <_ ( # ` w ) )
11 4 dimval 
 |-  ( ( X e. LVec /\ x e. ( LBasis ` X ) ) -> ( dim ` X ) = ( # ` x ) )
12 3 11 sylan 
 |-  ( ( ( W e. LVec /\ U e. ( LSubSp ` W ) ) /\ x e. ( LBasis ` X ) ) -> ( dim ` X ) = ( # ` x ) )
13 12 ad2antrr 
 |-  ( ( ( ( ( W e. LVec /\ U e. ( LSubSp ` W ) ) /\ x e. ( LBasis ` X ) ) /\ w e. ( LBasis ` W ) ) /\ x C_ w ) -> ( dim ` X ) = ( # ` x ) )
14 eqid 
 |-  ( LBasis ` W ) = ( LBasis ` W )
15 14 dimval 
 |-  ( ( W e. LVec /\ w e. ( LBasis ` W ) ) -> ( dim ` W ) = ( # ` w ) )
16 15 ad5ant14 
 |-  ( ( ( ( ( W e. LVec /\ U e. ( LSubSp ` W ) ) /\ x e. ( LBasis ` X ) ) /\ w e. ( LBasis ` W ) ) /\ x C_ w ) -> ( dim ` W ) = ( # ` w ) )
17 10 13 16 3brtr4d 
 |-  ( ( ( ( ( W e. LVec /\ U e. ( LSubSp ` W ) ) /\ x e. ( LBasis ` X ) ) /\ w e. ( LBasis ` W ) ) /\ x C_ w ) -> ( dim ` X ) <_ ( dim ` W ) )
18 simpll 
 |-  ( ( ( W e. LVec /\ U e. ( LSubSp ` W ) ) /\ x e. ( LBasis ` X ) ) -> W e. LVec )
19 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
20 19 ad2antrr 
 |-  ( ( ( W e. LVec /\ U e. ( LSubSp ` W ) ) /\ x e. ( LBasis ` X ) ) -> W e. LMod )
21 simplr 
 |-  ( ( ( W e. LVec /\ U e. ( LSubSp ` W ) ) /\ x e. ( LBasis ` X ) ) -> U e. ( LSubSp ` W ) )
22 simpr 
 |-  ( ( ( W e. LVec /\ U e. ( LSubSp ` W ) ) /\ x e. ( LBasis ` X ) ) -> x e. ( LBasis ` X ) )
23 eqid 
 |-  ( Base ` X ) = ( Base ` X )
24 23 4 lbsss 
 |-  ( x e. ( LBasis ` X ) -> x C_ ( Base ` X ) )
25 22 24 syl 
 |-  ( ( ( W e. LVec /\ U e. ( LSubSp ` W ) ) /\ x e. ( LBasis ` X ) ) -> x C_ ( Base ` X ) )
26 eqid 
 |-  ( Base ` W ) = ( Base ` W )
27 26 2 lssss 
 |-  ( U e. ( LSubSp ` W ) -> U C_ ( Base ` W ) )
28 1 26 ressbas2 
 |-  ( U C_ ( Base ` W ) -> U = ( Base ` X ) )
29 21 27 28 3syl 
 |-  ( ( ( W e. LVec /\ U e. ( LSubSp ` W ) ) /\ x e. ( LBasis ` X ) ) -> U = ( Base ` X ) )
30 25 29 sseqtrrd 
 |-  ( ( ( W e. LVec /\ U e. ( LSubSp ` W ) ) /\ x e. ( LBasis ` X ) ) -> x C_ U )
31 4 lbslinds 
 |-  ( LBasis ` X ) C_ ( LIndS ` X )
32 31 22 sselid 
 |-  ( ( ( W e. LVec /\ U e. ( LSubSp ` W ) ) /\ x e. ( LBasis ` X ) ) -> x e. ( LIndS ` X ) )
33 2 1 lsslinds 
 |-  ( ( W e. LMod /\ U e. ( LSubSp ` W ) /\ x C_ U ) -> ( x e. ( LIndS ` X ) <-> x e. ( LIndS ` W ) ) )
34 33 biimpa 
 |-  ( ( ( W e. LMod /\ U e. ( LSubSp ` W ) /\ x C_ U ) /\ x e. ( LIndS ` X ) ) -> x e. ( LIndS ` W ) )
35 20 21 30 32 34 syl31anc 
 |-  ( ( ( W e. LVec /\ U e. ( LSubSp ` W ) ) /\ x e. ( LBasis ` X ) ) -> x e. ( LIndS ` W ) )
36 14 islinds4 
 |-  ( W e. LVec -> ( x e. ( LIndS ` W ) <-> E. w e. ( LBasis ` W ) x C_ w ) )
37 36 biimpa 
 |-  ( ( W e. LVec /\ x e. ( LIndS ` W ) ) -> E. w e. ( LBasis ` W ) x C_ w )
38 18 35 37 syl2anc 
 |-  ( ( ( W e. LVec /\ U e. ( LSubSp ` W ) ) /\ x e. ( LBasis ` X ) ) -> E. w e. ( LBasis ` W ) x C_ w )
39 17 38 r19.29a 
 |-  ( ( ( W e. LVec /\ U e. ( LSubSp ` W ) ) /\ x e. ( LBasis ` X ) ) -> ( dim ` X ) <_ ( dim ` W ) )
40 8 39 exlimddv 
 |-  ( ( W e. LVec /\ U e. ( LSubSp ` W ) ) -> ( dim ` X ) <_ ( dim ` W ) )