lssssr

Description: Conclude subspace ordering from nonzero vector membership. ( ssrdv analog.) (Contributed by NM, 17-Aug-2014) (Revised by AV, 13-Jul-2022)

	Ref	Expression
Hypotheses	lssssr.o	$⊢ \underset{˙}{0} = 0_{W}$
	lssssr.s	$⊢ S = LSubSp (W)$
	lssssr.w	$⊢ φ \to W \in LMod$
	lssssr.t	$⊢ φ \to T \subseteq V$
	lssssr.u	$⊢ φ \to U \in S$
	lssssr.1	$⊢ (φ \land x \in (V ∖ \{\underset{˙}{0}\})) \to (x \in T \to x \in U)$
Assertion	lssssr	$⊢ φ \to T \subseteq U$

Proof

Step	Hyp	Ref	Expression
1		lssssr.o	$⊢ \underset{˙}{0} = 0_{W}$
2		lssssr.s	$⊢ S = LSubSp (W)$
3		lssssr.w	$⊢ φ \to W \in LMod$
4		lssssr.t	$⊢ φ \to T \subseteq V$
5		lssssr.u	$⊢ φ \to U \in S$
6		lssssr.1	$⊢ (φ \land x \in (V ∖ \{\underset{˙}{0}\})) \to (x \in T \to x \in U)$
7		simpr	$⊢ (φ \land x = \underset{˙}{0}) \to x = \underset{˙}{0}$
8	1 2	lss0cl	$⊢ (W \in LMod \land U \in S) \to \underset{˙}{0} \in U$
9	3 5 8	syl2anc	$⊢ φ \to \underset{˙}{0} \in U$
10	9	adantr	$⊢ (φ \land x = \underset{˙}{0}) \to \underset{˙}{0} \in U$
11	7 10	eqeltrd	$⊢ (φ \land x = \underset{˙}{0}) \to x \in U$
12	11	a1d	$⊢ (φ \land x = \underset{˙}{0}) \to (x \in T \to x \in U)$
13	4	sseld	$⊢ φ \to (x \in T \to x \in V)$
14	13	ancrd	$⊢ φ \to (x \in T \to (x \in V \land x \in T))$
15	14	adantr	$⊢ (φ \land x \neq \underset{˙}{0}) \to (x \in T \to (x \in V \land x \in T))$
16		eldifsn	$⊢ x \in (V ∖ \{\underset{˙}{0}\}) \leftrightarrow (x \in V \land x \neq \underset{˙}{0})$
17	16 6	sylan2br	$⊢ (φ \land (x \in V \land x \neq \underset{˙}{0})) \to (x \in T \to x \in U)$
18	17	exp32	$⊢ φ \to (x \in V \to (x \neq \underset{˙}{0} \to (x \in T \to x \in U)))$
19	18	com23	$⊢ φ \to (x \neq \underset{˙}{0} \to (x \in V \to (x \in T \to x \in U)))$
20	19	imp4b	$⊢ (φ \land x \neq \underset{˙}{0}) \to ((x \in V \land x \in T) \to x \in U)$
21	15 20	syld	$⊢ (φ \land x \neq \underset{˙}{0}) \to (x \in T \to x \in U)$
22	12 21	pm2.61dane	$⊢ φ \to (x \in T \to x \in U)$
23	22	ssrdv	$⊢ φ \to T \subseteq U$

Metamath Proof Explorer

Theorem lssssr

Proof