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 ` W )
lssssr.s
|- S = ( LSubSp ` W )
lssssr.w
|- ( ph -> W e. LMod )
lssssr.t
|- ( ph -> T C_ V )
lssssr.u
|- ( ph -> U e. S )
lssssr.1
|- ( ( ph /\ x e. ( V \ { .0. } ) ) -> ( x e. T -> x e. U ) )
Assertion lssssr
|- ( ph -> T C_ U )

Proof

Step Hyp Ref Expression
1 lssssr.o
 |-  .0. = ( 0g ` W )
2 lssssr.s
 |-  S = ( LSubSp ` W )
3 lssssr.w
 |-  ( ph -> W e. LMod )
4 lssssr.t
 |-  ( ph -> T C_ V )
5 lssssr.u
 |-  ( ph -> U e. S )
6 lssssr.1
 |-  ( ( ph /\ x e. ( V \ { .0. } ) ) -> ( x e. T -> x e. U ) )
7 simpr
 |-  ( ( ph /\ x = .0. ) -> x = .0. )
8 1 2 lss0cl
 |-  ( ( W e. LMod /\ U e. S ) -> .0. e. U )
9 3 5 8 syl2anc
 |-  ( ph -> .0. e. U )
10 9 adantr
 |-  ( ( ph /\ x = .0. ) -> .0. e. U )
11 7 10 eqeltrd
 |-  ( ( ph /\ x = .0. ) -> x e. U )
12 11 a1d
 |-  ( ( ph /\ x = .0. ) -> ( x e. T -> x e. U ) )
13 4 sseld
 |-  ( ph -> ( x e. T -> x e. V ) )
14 13 ancrd
 |-  ( ph -> ( x e. T -> ( x e. V /\ x e. T ) ) )
15 14 adantr
 |-  ( ( ph /\ x =/= .0. ) -> ( x e. T -> ( x e. V /\ x e. T ) ) )
16 eldifsn
 |-  ( x e. ( V \ { .0. } ) <-> ( x e. V /\ x =/= .0. ) )
17 16 6 sylan2br
 |-  ( ( ph /\ ( x e. V /\ x =/= .0. ) ) -> ( x e. T -> x e. U ) )
18 17 exp32
 |-  ( ph -> ( x e. V -> ( x =/= .0. -> ( x e. T -> x e. U ) ) ) )
19 18 com23
 |-  ( ph -> ( x =/= .0. -> ( x e. V -> ( x e. T -> x e. U ) ) ) )
20 19 imp4b
 |-  ( ( ph /\ x =/= .0. ) -> ( ( x e. V /\ x e. T ) -> x e. U ) )
21 15 20 syld
 |-  ( ( ph /\ x =/= .0. ) -> ( x e. T -> x e. U ) )
22 12 21 pm2.61dane
 |-  ( ph -> ( x e. T -> x e. U ) )
23 22 ssrdv
 |-  ( ph -> T C_ U )