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 𝑠 U
Assertion lssdimle W LVec U LSubSp W dim X dim W

Proof

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