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 ⊢ 𝑋 = ( 𝑊 ↾s 𝑈 )
Assertion lssdimle ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) → ( dim ‘ 𝑋 ) ≤ ( dim ‘ 𝑊 ) )

Proof

Step Hyp Ref Expression
1 lssdimle.x ⊢ 𝑋 = ( 𝑊 ↾s 𝑈 )
2 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
3 1 2 lsslvec ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) → 𝑋 ∈ LVec )
4 eqid ⊢ ( LBasis ‘ 𝑋 ) = ( LBasis ‘ 𝑋 )
5 4 lbsex ⊢ ( 𝑋 ∈ LVec → ( LBasis ‘ 𝑋 ) ≠ ∅ )
6 3 5 syl ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) → ( LBasis ‘ 𝑋 ) ≠ ∅ )
7 n0 ⊢ ( ( LBasis ‘ 𝑋 ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( LBasis ‘ 𝑋 ) )
8 6 7 sylib ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) → ∃ 𝑥 𝑥 ∈ ( LBasis ‘ 𝑋 ) )
9 hashss ⊢ ( ( 𝑤 ∈ ( LBasis ‘ 𝑊 ) ∧ 𝑥 ⊆ 𝑤 ) → ( ♯ ‘ 𝑥 ) ≤ ( ♯ ‘ 𝑤 ) )
10 9 adantll ⊢ ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) ∧ 𝑥 ∈ ( LBasis ‘ 𝑋 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝑊 ) ) ∧ 𝑥 ⊆ 𝑤 ) → ( ♯ ‘ 𝑥 ) ≤ ( ♯ ‘ 𝑤 ) )
11 4 dimval ⊢ ( ( 𝑋 ∈ LVec ∧ 𝑥 ∈ ( LBasis ‘ 𝑋 ) ) → ( dim ‘ 𝑋 ) = ( ♯ ‘ 𝑥 ) )
12 3 11 sylan ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) ∧ 𝑥 ∈ ( LBasis ‘ 𝑋 ) ) → ( dim ‘ 𝑋 ) = ( ♯ ‘ 𝑥 ) )
13 12 ad2antrr ⊢ ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) ∧ 𝑥 ∈ ( LBasis ‘ 𝑋 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝑊 ) ) ∧ 𝑥 ⊆ 𝑤 ) → ( dim ‘ 𝑋 ) = ( ♯ ‘ 𝑥 ) )
14 eqid ⊢ ( LBasis ‘ 𝑊 ) = ( LBasis ‘ 𝑊 )
15 14 dimval ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑤 ∈ ( LBasis ‘ 𝑊 ) ) → ( dim ‘ 𝑊 ) = ( ♯ ‘ 𝑤 ) )
16 15 ad5ant14 ⊢ ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) ∧ 𝑥 ∈ ( LBasis ‘ 𝑋 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝑊 ) ) ∧ 𝑥 ⊆ 𝑤 ) → ( dim ‘ 𝑊 ) = ( ♯ ‘ 𝑤 ) )
17 10 13 16 3brtr4d ⊢ ( ( ( ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) ∧ 𝑥 ∈ ( LBasis ‘ 𝑋 ) ) ∧ 𝑤 ∈ ( LBasis ‘ 𝑊 ) ) ∧ 𝑥 ⊆ 𝑤 ) → ( dim ‘ 𝑋 ) ≤ ( dim ‘ 𝑊 ) )
18 simpll ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) ∧ 𝑥 ∈ ( LBasis ‘ 𝑋 ) ) → 𝑊 ∈ LVec )
19 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
20 19 ad2antrr ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) ∧ 𝑥 ∈ ( LBasis ‘ 𝑋 ) ) → 𝑊 ∈ LMod )
21 simplr ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) ∧ 𝑥 ∈ ( LBasis ‘ 𝑋 ) ) → 𝑈 ∈ ( LSubSp ‘ 𝑊 ) )
22 simpr ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) ∧ 𝑥 ∈ ( LBasis ‘ 𝑋 ) ) → 𝑥 ∈ ( LBasis ‘ 𝑋 ) )
23 eqid ⊢ ( Base ‘ 𝑋 ) = ( Base ‘ 𝑋 )
24 23 4 lbsss ⊢ ( 𝑥 ∈ ( LBasis ‘ 𝑋 ) → 𝑥 ⊆ ( Base ‘ 𝑋 ) )
25 22 24 syl ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) ∧ 𝑥 ∈ ( LBasis ‘ 𝑋 ) ) → 𝑥 ⊆ ( Base ‘ 𝑋 ) )
26 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
27 26 2 lssss ⊢ ( 𝑈 ∈ ( LSubSp ‘ 𝑊 ) → 𝑈 ⊆ ( Base ‘ 𝑊 ) )
28 1 26 ressbas2 ⊢ ( 𝑈 ⊆ ( Base ‘ 𝑊 ) → 𝑈 = ( Base ‘ 𝑋 ) )
29 21 27 28 3syl ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) ∧ 𝑥 ∈ ( LBasis ‘ 𝑋 ) ) → 𝑈 = ( Base ‘ 𝑋 ) )
30 25 29 sseqtrrd ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) ∧ 𝑥 ∈ ( LBasis ‘ 𝑋 ) ) → 𝑥 ⊆ 𝑈 )
31 4 lbslinds ⊢ ( LBasis ‘ 𝑋 ) ⊆ ( LIndS ‘ 𝑋 )
32 31 22 sseldi ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) ∧ 𝑥 ∈ ( LBasis ‘ 𝑋 ) ) → 𝑥 ∈ ( LIndS ‘ 𝑋 ) )
33 2 1 lsslinds ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑥 ⊆ 𝑈 ) → ( 𝑥 ∈ ( LIndS ‘ 𝑋 ) ↔ 𝑥 ∈ ( LIndS ‘ 𝑊 ) ) )
34 33 biimpa ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑥 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( LIndS ‘ 𝑋 ) ) → 𝑥 ∈ ( LIndS ‘ 𝑊 ) )
35 20 21 30 32 34 syl31anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) ∧ 𝑥 ∈ ( LBasis ‘ 𝑋 ) ) → 𝑥 ∈ ( LIndS ‘ 𝑊 ) )
36 14 islinds4 ⊢ ( 𝑊 ∈ LVec → ( 𝑥 ∈ ( LIndS ‘ 𝑊 ) ↔ ∃ 𝑤 ∈ ( LBasis ‘ 𝑊 ) 𝑥 ⊆ 𝑤 ) )
37 36 biimpa ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑥 ∈ ( LIndS ‘ 𝑊 ) ) → ∃ 𝑤 ∈ ( LBasis ‘ 𝑊 ) 𝑥 ⊆ 𝑤 )
38 18 35 37 syl2anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) ∧ 𝑥 ∈ ( LBasis ‘ 𝑋 ) ) → ∃ 𝑤 ∈ ( LBasis ‘ 𝑊 ) 𝑥 ⊆ 𝑤 )
39 17 38 r19.29a ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) ∧ 𝑥 ∈ ( LBasis ‘ 𝑋 ) ) → ( dim ‘ 𝑋 ) ≤ ( dim ‘ 𝑊 ) )
40 8 39 exlimddv ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) → ( dim ‘ 𝑋 ) ≤ ( dim ‘ 𝑊 ) )