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	⊢ 0 = ( 0_g ‘ 𝑊 )
	lssssr.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
	lssssr.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	lssssr.t	⊢ ( 𝜑 → 𝑇 ⊆ 𝑉 )
	lssssr.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
	lssssr.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → ( 𝑥 ∈ 𝑇 → 𝑥 ∈ 𝑈 ) )
Assertion	lssssr	⊢ ( 𝜑 → 𝑇 ⊆ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		lssssr.o	⊢ 0 = ( 0_g ‘ 𝑊 )
2		lssssr.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3		lssssr.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
4		lssssr.t	⊢ ( 𝜑 → 𝑇 ⊆ 𝑉 )
5		lssssr.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
6		lssssr.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → ( 𝑥 ∈ 𝑇 → 𝑥 ∈ 𝑈 ) )
7		simpr	⊢ ( ( 𝜑 ∧ 𝑥 = 0 ) → 𝑥 = 0 )
8	1 2	lss0cl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → 0 ∈ 𝑈 )
9	3 5 8	syl2anc	⊢ ( 𝜑 → 0 ∈ 𝑈 )
10	9	adantr	⊢ ( ( 𝜑 ∧ 𝑥 = 0 ) → 0 ∈ 𝑈 )
11	7 10	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑥 = 0 ) → 𝑥 ∈ 𝑈 )
12	11	a1d	⊢ ( ( 𝜑 ∧ 𝑥 = 0 ) → ( 𝑥 ∈ 𝑇 → 𝑥 ∈ 𝑈 ) )
13	4	sseld	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑇 → 𝑥 ∈ 𝑉 ) )
14	13	ancrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑇 → ( 𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝑇 ) ) )
15	14	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ≠ 0 ) → ( 𝑥 ∈ 𝑇 → ( 𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝑇 ) ) )
16		eldifsn	⊢ ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ↔ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) )
17	16 6	sylan2br	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) ) → ( 𝑥 ∈ 𝑇 → 𝑥 ∈ 𝑈 ) )
18	17	exp32	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑉 → ( 𝑥 ≠ 0 → ( 𝑥 ∈ 𝑇 → 𝑥 ∈ 𝑈 ) ) ) )
19	18	com23	⊢ ( 𝜑 → ( 𝑥 ≠ 0 → ( 𝑥 ∈ 𝑉 → ( 𝑥 ∈ 𝑇 → 𝑥 ∈ 𝑈 ) ) ) )
20	19	imp4b	⊢ ( ( 𝜑 ∧ 𝑥 ≠ 0 ) → ( ( 𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝑇 ) → 𝑥 ∈ 𝑈 ) )
21	15 20	syld	⊢ ( ( 𝜑 ∧ 𝑥 ≠ 0 ) → ( 𝑥 ∈ 𝑇 → 𝑥 ∈ 𝑈 ) )
22	12 21	pm2.61dane	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑇 → 𝑥 ∈ 𝑈 ) )
23	22	ssrdv	⊢ ( 𝜑 → 𝑇 ⊆ 𝑈 )

Metamath Proof Explorer

Theorem lssssr

Proof