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 \in LVec \land U \in LSubSp (W)) \to \dim (X) \leq \dim (W)$

Proof

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

Metamath Proof Explorer

Theorem lssdimle

Proof