Metamath Proof Explorer


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

Proof

Step Hyp Ref Expression
1 lssssr.o 0 = ( 0g𝑊 )
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 ( 𝜑𝑇𝑈 )