Theorem dvhdimlem

Description: Lemma for dvh2dim and dvh3dim . TODO: make this obsolete and use dvh4dimlem directly? (Contributed by NM, 24-Apr-2015)

	Ref	Expression
Hypotheses	dvh3dim.h	|- H = ( LHyp ` K )
	dvh3dim.u	|- U = ( ( DVecH ` K ) ` W )
	dvh3dim.v	|- V = ( Base ` U )
	dvh3dim.n	|- N = ( LSpan ` U )
	dvh3dim.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	dvh3dim.x	|- ( ph -> X e. V )
	dvhdim.y	|- ( ph -> Y e. V )
	dvhdim.o	|- .0. = ( 0g ` U )
	dvhdim.x	|- ( ph -> X =/= .0. )
	dvhdimlem.y	|- ( ph -> Y =/= .0. )
Assertion	dvhdimlem	|- ( ph -> E. z e. V -. z e. ( N ` { X , Y } ) )

Proof

Step	Hyp	Ref	Expression
1		dvh3dim.h	|- H = ( LHyp ` K )
2		dvh3dim.u	|- U = ( ( DVecH ` K ) ` W )
3		dvh3dim.v	|- V = ( Base ` U )
4		dvh3dim.n	|- N = ( LSpan ` U )
5		dvh3dim.k	|- ( ph -> ( K e. HL /\ W e. H ) )
6		dvh3dim.x	|- ( ph -> X e. V )
7		dvhdim.y	|- ( ph -> Y e. V )
8		dvhdim.o	|- .0. = ( 0g ` U )
9		dvhdim.x	|- ( ph -> X =/= .0. )
10		dvhdimlem.y	|- ( ph -> Y =/= .0. )
11	1 2 3 4 5 6 7 7 8 9 10 10	dvh4dimlem	|- ( ph -> E. z e. V -. z e. ( N ` { X , Y , Y } ) )
12	1 2 5	dvhlmod	|- ( ph -> U e. LMod )
13		df-tp	|- { X , Y , Y } = ( { X , Y } u. { Y } )
14		prssi	|- ( ( X e. V /\ Y e. V ) -> { X , Y } C_ V )
15	6 7 14	syl2anc	|- ( ph -> { X , Y } C_ V )
16	7	snssd	|- ( ph -> { Y } C_ V )
17	15 16	unssd	|- ( ph -> ( { X , Y } u. { Y } ) C_ V )
18	13 17	eqsstrid	|- ( ph -> { X , Y , Y } C_ V )
19		ssun1	|- { X , Y } C_ ( { X , Y } u. { Y } )
20	19 13	sseqtrri	|- { X , Y } C_ { X , Y , Y }
21	20	a1i	|- ( ph -> { X , Y } C_ { X , Y , Y } )
22	3 4	lspss	|- ( ( U e. LMod /\ { X , Y , Y } C_ V /\ { X , Y } C_ { X , Y , Y } ) -> ( N ` { X , Y } ) C_ ( N ` { X , Y , Y } ) )
23	12 18 21 22	syl3anc	|- ( ph -> ( N ` { X , Y } ) C_ ( N ` { X , Y , Y } ) )
24	23	ssneld	|- ( ph -> ( -. z e. ( N ` { X , Y , Y } ) -> -. z e. ( N ` { X , Y } ) ) )
25	24	reximdv	|- ( ph -> ( E. z e. V -. z e. ( N ` { X , Y , Y } ) -> E. z e. V -. z e. ( N ` { X , Y } ) ) )
26	11 25	mpd	|- ( ph -> E. z e. V -. z e. ( N ` { X , Y } ) )