lsatdim

Description: A line, spanned by a nonzero singleton, has dimension 1. (Contributed by Thierry Arnoux, 20-May-2023)

	Ref	Expression
Hypotheses	lbslsat.v	$⊢ V = {Base}_{W}$
	lbslsat.n	$⊢ N = LSpan (W)$
	lbslsat.z	$⊢ \underset{˙}{0} = 0_{W}$
	lbslsat.y	$⊢ Y = W ↾_{𝑠} N (\{X\})$
Assertion	lsatdim	$⊢ (W \in LVec \land X \in V \land X \neq \underset{˙}{0}) \to \dim (Y) = 1$

Step	Hyp	Ref	Expression
1		lbslsat.v	$⊢ V = {Base}_{W}$
2		lbslsat.n	$⊢ N = LSpan (W)$
3		lbslsat.z	$⊢ \underset{˙}{0} = 0_{W}$
4		lbslsat.y	$⊢ Y = W ↾_{𝑠} N (\{X\})$
5		simp1	$⊢ (W \in LVec \land X \in V \land X \neq \underset{˙}{0}) \to W \in LVec$
6		lveclmod	$⊢ W \in LVec \to W \in LMod$
7	5 6	syl	$⊢ (W \in LVec \land X \in V \land X \neq \underset{˙}{0}) \to W \in LMod$
8		simp2	$⊢ (W \in LVec \land X \in V \land X \neq \underset{˙}{0}) \to X \in V$
9	8	snssd	$⊢ (W \in LVec \land X \in V \land X \neq \underset{˙}{0}) \to \{X\} \subseteq V$
10		eqid	$⊢ LSubSp (W) = LSubSp (W)$
11	1 10 2	lspcl	$⊢ (W \in LMod \land \{X\} \subseteq V) \to N (\{X\}) \in LSubSp (W)$
12	7 9 11	syl2anc	$⊢ (W \in LVec \land X \in V \land X \neq \underset{˙}{0}) \to N (\{X\}) \in LSubSp (W)$
13	4 10	lsslvec	$⊢ (W \in LVec \land N (\{X\}) \in LSubSp (W)) \to Y \in LVec$
14	5 12 13	syl2anc	$⊢ (W \in LVec \land X \in V \land X \neq \underset{˙}{0}) \to Y \in LVec$
15	1 2 3 4	lbslsat	$⊢ (W \in LVec \land X \in V \land X \neq \underset{˙}{0}) \to \{X\} \in LBasis (Y)$
16		eqid	$⊢ LBasis (Y) = LBasis (Y)$
17	16	dimval	$⊢ (Y \in LVec \land \{X\} \in LBasis (Y)) \to \dim (Y) = \|\{X\}\|$
18	14 15 17	syl2anc	$⊢ (W \in LVec \land X \in V \land X \neq \underset{˙}{0}) \to \dim (Y) = \|\{X\}\|$
19		hashsng	$⊢ X \in V \to \|\{X\}\| = 1$
20	8 19	syl	$⊢ (W \in LVec \land X \in V \land X \neq \underset{˙}{0}) \to \|\{X\}\| = 1$
21	18 20	eqtrd	$⊢ (W \in LVec \land X \in V \land X \neq \underset{˙}{0}) \to \dim (Y) = 1$

Metamath Proof Explorer