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 )