This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )