Metamath Proof Explorer

Theorem dvh3dim2

Description: There is a vector that is outside of 2 spans with a common vector. (Contributed by NM, 13-May-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 )
dvh3dim2.z 
|- ( ph -> Z e. V )
Assertion dvh3dim2 
|- ( ph -> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { X , Z } ) ) )

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 dvh3dim2.z 
 |-  ( ph -> Z e. V )
9 1 2 3 4 5 6 8 dvh3dim 
 |-  ( ph -> E. z e. V -. z e. ( N ` { X , Z } ) )
10 9 adantr 
 |-  ( ( ph /\ Y e. ( N ` { X , Z } ) ) -> E. z e. V -. z e. ( N ` { X , Z } ) )
11 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
12 1 2 5 dvhlmod 
 |-  ( ph -> U e. LMod )
13 12 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( N ` { X , Z } ) ) /\ z e. V ) -> U e. LMod )
14 3 11 4 12 6 8 lspprcl 
 |-  ( ph -> ( N ` { X , Z } ) e. ( LSubSp ` U ) )
15 14 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( N ` { X , Z } ) ) /\ z e. V ) -> ( N ` { X , Z } ) e. ( LSubSp ` U ) )
16 3 4 12 6 8 lspprid1 
 |-  ( ph -> X e. ( N ` { X , Z } ) )
17 16 ad2antrr 
 |-  ( ( ( ph /\ Y e. ( N ` { X , Z } ) ) /\ z e. V ) -> X e. ( N ` { X , Z } ) )
18 simplr 
 |-  ( ( ( ph /\ Y e. ( N ` { X , Z } ) ) /\ z e. V ) -> Y e. ( N ` { X , Z } ) )
19 11 4 13 15 17 18 lspprss 
 |-  ( ( ( ph /\ Y e. ( N ` { X , Z } ) ) /\ z e. V ) -> ( N ` { X , Y } ) C_ ( N ` { X , Z } ) )
20 19 ssneld 
 |-  ( ( ( ph /\ Y e. ( N ` { X , Z } ) ) /\ z e. V ) -> ( -. z e. ( N ` { X , Z } ) -> -. z e. ( N ` { X , Y } ) ) )
21 20 ancrd 
 |-  ( ( ( ph /\ Y e. ( N ` { X , Z } ) ) /\ z e. V ) -> ( -. z e. ( N ` { X , Z } ) -> ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { X , Z } ) ) ) )
22 21 reximdva 
 |-  ( ( ph /\ Y e. ( N ` { X , Z } ) ) -> ( E. z e. V -. z e. ( N ` { X , Z } ) -> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { X , Z } ) ) ) )
23 10 22 mpd 
 |-  ( ( ph /\ Y e. ( N ` { X , Z } ) ) -> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { X , Z } ) ) )
24 1 2 3 4 5 6 7 dvh3dim 
 |-  ( ph -> E. w e. V -. w e. ( N ` { X , Y } ) )
25 24 adantr 
 |-  ( ( ph /\ -. Y e. ( N ` { X , Z } ) ) -> E. w e. V -. w e. ( N ` { X , Y } ) )
26 simpl1l 
 |-  ( ( ( ( ph /\ -. Y e. ( N ` { X , Z } ) ) /\ w e. V /\ -. w e. ( N ` { X , Y } ) ) /\ w e. ( N ` { X , Z } ) ) -> ph )
27 26 12 syl 
 |-  ( ( ( ( ph /\ -. Y e. ( N ` { X , Z } ) ) /\ w e. V /\ -. w e. ( N ` { X , Y } ) ) /\ w e. ( N ` { X , Z } ) ) -> U e. LMod )
28 simpl2 
 |-  ( ( ( ( ph /\ -. Y e. ( N ` { X , Z } ) ) /\ w e. V /\ -. w e. ( N ` { X , Y } ) ) /\ w e. ( N ` { X , Z } ) ) -> w e. V )
29 26 7 syl 
 |-  ( ( ( ( ph /\ -. Y e. ( N ` { X , Z } ) ) /\ w e. V /\ -. w e. ( N ` { X , Y } ) ) /\ w e. ( N ` { X , Z } ) ) -> Y e. V )
30 eqid 
 |-  ( +g ` U ) = ( +g ` U )
31 3 30 lmodvacl 
 |-  ( ( U e. LMod /\ w e. V /\ Y e. V ) -> ( w ( +g ` U ) Y ) e. V )
32 27 28 29 31 syl3anc 
 |-  ( ( ( ( ph /\ -. Y e. ( N ` { X , Z } ) ) /\ w e. V /\ -. w e. ( N ` { X , Y } ) ) /\ w e. ( N ` { X , Z } ) ) -> ( w ( +g ` U ) Y ) e. V )
33 3 11 4 12 6 7 lspprcl 
 |-  ( ph -> ( N ` { X , Y } ) e. ( LSubSp ` U ) )
34 26 33 syl 
 |-  ( ( ( ( ph /\ -. Y e. ( N ` { X , Z } ) ) /\ w e. V /\ -. w e. ( N ` { X , Y } ) ) /\ w e. ( N ` { X , Z } ) ) -> ( N ` { X , Y } ) e. ( LSubSp ` U ) )
35 3 4 12 6 7 lspprid2 
 |-  ( ph -> Y e. ( N ` { X , Y } ) )
36 26 35 syl 
 |-  ( ( ( ( ph /\ -. Y e. ( N ` { X , Z } ) ) /\ w e. V /\ -. w e. ( N ` { X , Y } ) ) /\ w e. ( N ` { X , Z } ) ) -> Y e. ( N ` { X , Y } ) )
37 simpl3 
 |-  ( ( ( ( ph /\ -. Y e. ( N ` { X , Z } ) ) /\ w e. V /\ -. w e. ( N ` { X , Y } ) ) /\ w e. ( N ` { X , Z } ) ) -> -. w e. ( N ` { X , Y } ) )
38 3 30 11 27 34 36 28 37 lssvancl2 
 |-  ( ( ( ( ph /\ -. Y e. ( N ` { X , Z } ) ) /\ w e. V /\ -. w e. ( N ` { X , Y } ) ) /\ w e. ( N ` { X , Z } ) ) -> -. ( w ( +g ` U ) Y ) e. ( N ` { X , Y } ) )
39 26 14 syl 
 |-  ( ( ( ( ph /\ -. Y e. ( N ` { X , Z } ) ) /\ w e. V /\ -. w e. ( N ` { X , Y } ) ) /\ w e. ( N ` { X , Z } ) ) -> ( N ` { X , Z } ) e. ( LSubSp ` U ) )
40 simpr 
 |-  ( ( ( ( ph /\ -. Y e. ( N ` { X , Z } ) ) /\ w e. V /\ -. w e. ( N ` { X , Y } ) ) /\ w e. ( N ` { X , Z } ) ) -> w e. ( N ` { X , Z } ) )
41 simpl1r 
 |-  ( ( ( ( ph /\ -. Y e. ( N ` { X , Z } ) ) /\ w e. V /\ -. w e. ( N ` { X , Y } ) ) /\ w e. ( N ` { X , Z } ) ) -> -. Y e. ( N ` { X , Z } ) )
42 3 30 11 27 39 40 29 41 lssvancl1 
 |-  ( ( ( ( ph /\ -. Y e. ( N ` { X , Z } ) ) /\ w e. V /\ -. w e. ( N ` { X , Y } ) ) /\ w e. ( N ` { X , Z } ) ) -> -. ( w ( +g ` U ) Y ) e. ( N ` { X , Z } ) )
43 eleq1 
 |-  ( z = ( w ( +g ` U ) Y ) -> ( z e. ( N ` { X , Y } ) <-> ( w ( +g ` U ) Y ) e. ( N ` { X , Y } ) ) )
44 43 notbid 
 |-  ( z = ( w ( +g ` U ) Y ) -> ( -. z e. ( N ` { X , Y } ) <-> -. ( w ( +g ` U ) Y ) e. ( N ` { X , Y } ) ) )
45 eleq1 
 |-  ( z = ( w ( +g ` U ) Y ) -> ( z e. ( N ` { X , Z } ) <-> ( w ( +g ` U ) Y ) e. ( N ` { X , Z } ) ) )
46 45 notbid 
 |-  ( z = ( w ( +g ` U ) Y ) -> ( -. z e. ( N ` { X , Z } ) <-> -. ( w ( +g ` U ) Y ) e. ( N ` { X , Z } ) ) )
47 44 46 anbi12d 
 |-  ( z = ( w ( +g ` U ) Y ) -> ( ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { X , Z } ) ) <-> ( -. ( w ( +g ` U ) Y ) e. ( N ` { X , Y } ) /\ -. ( w ( +g ` U ) Y ) e. ( N ` { X , Z } ) ) ) )
48 47 rspcev 
 |-  ( ( ( w ( +g ` U ) Y ) e. V /\ ( -. ( w ( +g ` U ) Y ) e. ( N ` { X , Y } ) /\ -. ( w ( +g ` U ) Y ) e. ( N ` { X , Z } ) ) ) -> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { X , Z } ) ) )
49 32 38 42 48 syl12anc 
 |-  ( ( ( ( ph /\ -. Y e. ( N ` { X , Z } ) ) /\ w e. V /\ -. w e. ( N ` { X , Y } ) ) /\ w e. ( N ` { X , Z } ) ) -> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { X , Z } ) ) )
50 simpl2 
 |-  ( ( ( ( ph /\ -. Y e. ( N ` { X , Z } ) ) /\ w e. V /\ -. w e. ( N ` { X , Y } ) ) /\ -. w e. ( N ` { X , Z } ) ) -> w e. V )
51 simpl3 
 |-  ( ( ( ( ph /\ -. Y e. ( N ` { X , Z } ) ) /\ w e. V /\ -. w e. ( N ` { X , Y } ) ) /\ -. w e. ( N ` { X , Z } ) ) -> -. w e. ( N ` { X , Y } ) )
52 simpr 
 |-  ( ( ( ( ph /\ -. Y e. ( N ` { X , Z } ) ) /\ w e. V /\ -. w e. ( N ` { X , Y } ) ) /\ -. w e. ( N ` { X , Z } ) ) -> -. w e. ( N ` { X , Z } ) )
53 eleq1 
 |-  ( z = w -> ( z e. ( N ` { X , Y } ) <-> w e. ( N ` { X , Y } ) ) )
54 53 notbid 
 |-  ( z = w -> ( -. z e. ( N ` { X , Y } ) <-> -. w e. ( N ` { X , Y } ) ) )
55 eleq1 
 |-  ( z = w -> ( z e. ( N ` { X , Z } ) <-> w e. ( N ` { X , Z } ) ) )
56 55 notbid 
 |-  ( z = w -> ( -. z e. ( N ` { X , Z } ) <-> -. w e. ( N ` { X , Z } ) ) )
57 54 56 anbi12d 
 |-  ( z = w -> ( ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { X , Z } ) ) <-> ( -. w e. ( N ` { X , Y } ) /\ -. w e. ( N ` { X , Z } ) ) ) )
58 57 rspcev 
 |-  ( ( w e. V /\ ( -. w e. ( N ` { X , Y } ) /\ -. w e. ( N ` { X , Z } ) ) ) -> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { X , Z } ) ) )
59 50 51 52 58 syl12anc 
 |-  ( ( ( ( ph /\ -. Y e. ( N ` { X , Z } ) ) /\ w e. V /\ -. w e. ( N ` { X , Y } ) ) /\ -. w e. ( N ` { X , Z } ) ) -> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { X , Z } ) ) )
60 49 59 pm2.61dan 
 |-  ( ( ( ph /\ -. Y e. ( N ` { X , Z } ) ) /\ w e. V /\ -. w e. ( N ` { X , Y } ) ) -> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { X , Z } ) ) )
61 60 rexlimdv3a 
 |-  ( ( ph /\ -. Y e. ( N ` { X , Z } ) ) -> ( E. w e. V -. w e. ( N ` { X , Y } ) -> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { X , Z } ) ) ) )
62 25 61 mpd 
 |-  ( ( ph /\ -. Y e. ( N ` { X , Z } ) ) -> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { X , Z } ) ) )
63 23 62 pm2.61dan 
 |-  ( ph -> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { X , Z } ) ) )