dvh3dim

Description: There is a vector that is outside the span of 2 others. (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 )
	dvh3dim.y	\|- ( ph -> Y e. V )
Assertion	dvh3dim	\|- ( 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		dvh3dim.y	\|- ( ph -> Y e. V )
8	1 2 3 4 5 7	dvh2dim	\|- ( ph -> E. z e. V -. z e. ( N ` { Y } ) )
9	8	adantr	\|- ( ( ph /\ X = ( 0g ` U ) ) -> E. z e. V -. z e. ( N ` { Y } ) )
10		prcom	\|- { X , Y } = { Y , X }
11		preq2	\|- ( X = ( 0g ` U ) -> { Y , X } = { Y , ( 0g ` U ) } )
12	10 11	eqtrid	\|- ( X = ( 0g ` U ) -> { X , Y } = { Y , ( 0g ` U ) } )
13	12	fveq2d	\|- ( X = ( 0g ` U ) -> ( N ` { X , Y } ) = ( N ` { Y , ( 0g ` U ) } ) )
14		eqid	\|- ( 0g ` U ) = ( 0g ` U )
15	1 2 5	dvhlmod	\|- ( ph -> U e. LMod )
16	3 14 4 15 7	lsppr0	\|- ( ph -> ( N ` { Y , ( 0g ` U ) } ) = ( N ` { Y } ) )
17	13 16	sylan9eqr	\|- ( ( ph /\ X = ( 0g ` U ) ) -> ( N ` { X , Y } ) = ( N ` { Y } ) )
18	17	eleq2d	\|- ( ( ph /\ X = ( 0g ` U ) ) -> ( z e. ( N ` { X , Y } ) <-> z e. ( N ` { Y } ) ) )
19	18	notbid	\|- ( ( ph /\ X = ( 0g ` U ) ) -> ( -. z e. ( N ` { X , Y } ) <-> -. z e. ( N ` { Y } ) ) )
20	19	rexbidv	\|- ( ( ph /\ X = ( 0g ` U ) ) -> ( E. z e. V -. z e. ( N ` { X , Y } ) <-> E. z e. V -. z e. ( N ` { Y } ) ) )
21	9 20	mpbird	\|- ( ( ph /\ X = ( 0g ` U ) ) -> E. z e. V -. z e. ( N ` { X , Y } ) )
22	1 2 3 4 5 6	dvh2dim	\|- ( ph -> E. z e. V -. z e. ( N ` { X } ) )
23	22	adantr	\|- ( ( ph /\ Y = ( 0g ` U ) ) -> E. z e. V -. z e. ( N ` { X } ) )
24		preq2	\|- ( Y = ( 0g ` U ) -> { X , Y } = { X , ( 0g ` U ) } )
25	24	fveq2d	\|- ( Y = ( 0g ` U ) -> ( N ` { X , Y } ) = ( N ` { X , ( 0g ` U ) } ) )
26	3 14 4 15 6	lsppr0	\|- ( ph -> ( N ` { X , ( 0g ` U ) } ) = ( N ` { X } ) )
27	25 26	sylan9eqr	\|- ( ( ph /\ Y = ( 0g ` U ) ) -> ( N ` { X , Y } ) = ( N ` { X } ) )
28	27	eleq2d	\|- ( ( ph /\ Y = ( 0g ` U ) ) -> ( z e. ( N ` { X , Y } ) <-> z e. ( N ` { X } ) ) )
29	28	notbid	\|- ( ( ph /\ Y = ( 0g ` U ) ) -> ( -. z e. ( N ` { X , Y } ) <-> -. z e. ( N ` { X } ) ) )
30	29	rexbidv	\|- ( ( ph /\ Y = ( 0g ` U ) ) -> ( E. z e. V -. z e. ( N ` { X , Y } ) <-> E. z e. V -. z e. ( N ` { X } ) ) )
31	23 30	mpbird	\|- ( ( ph /\ Y = ( 0g ` U ) ) -> E. z e. V -. z e. ( N ` { X , Y } ) )
32	5	adantr	\|- ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) ) ) -> ( K e. HL /\ W e. H ) )
33	6	adantr	\|- ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) ) ) -> X e. V )
34	7	adantr	\|- ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) ) ) -> Y e. V )
35		simprl	\|- ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) ) ) -> X =/= ( 0g ` U ) )
36		simprr	\|- ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) ) ) -> Y =/= ( 0g ` U ) )
37	1 2 3 4 32 33 34 14 35 36	dvhdimlem	\|- ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) ) ) -> E. z e. V -. z e. ( N ` { X , Y } ) )
38	21 31 37	pm2.61da2ne	\|- ( ph -> E. z e. V -. z e. ( N ` { X , Y } ) )

Metamath Proof Explorer

Theorem dvh3dim

Proof