Metamath Proof Explorer

Theorem dvh4dimN

Description: There is a vector that is outside the span of 3 others. (Contributed by NM, 22-May-2015) (New usage is discouraged.)

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 dvh4dimN 
|- ( ph -> E. z e. V -. z e. ( N ` { X , Y , 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 7 8 dvh3dim 
 |-  ( ph -> E. z e. V -. z e. ( N ` { Y , Z } ) )
10 9 adantr 
 |-  ( ( ph /\ X = ( 0g ` U ) ) -> E. z e. V -. z e. ( N ` { Y , Z } ) )
11 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
12 1 2 5 dvhlmod 
 |-  ( ph -> U e. LMod )
13 prssi 
 |-  ( ( Y e. V /\ Z e. V ) -> { Y , Z } C_ V )
14 7 8 13 syl2anc 
 |-  ( ph -> { Y , Z } C_ V )
15 3 11 4 12 14 lspun0 
 |-  ( ph -> ( N ` ( { Y , Z } u. { ( 0g ` U ) } ) ) = ( N ` { Y , Z } ) )
16 tprot 
 |-  { ( 0g ` U ) , Y , Z } = { Y , Z , ( 0g ` U ) }
17 df-tp 
 |-  { Y , Z , ( 0g ` U ) } = ( { Y , Z } u. { ( 0g ` U ) } )
18 16 17 eqtr2i 
 |-  ( { Y , Z } u. { ( 0g ` U ) } ) = { ( 0g ` U ) , Y , Z }
19 tpeq1 
 |-  ( X = ( 0g ` U ) -> { X , Y , Z } = { ( 0g ` U ) , Y , Z } )
20 18 19 eqtr4id 
 |-  ( X = ( 0g ` U ) -> ( { Y , Z } u. { ( 0g ` U ) } ) = { X , Y , Z } )
21 20 fveq2d 
 |-  ( X = ( 0g ` U ) -> ( N ` ( { Y , Z } u. { ( 0g ` U ) } ) ) = ( N ` { X , Y , Z } ) )
22 15 21 sylan9req 
 |-  ( ( ph /\ X = ( 0g ` U ) ) -> ( N ` { Y , Z } ) = ( N ` { X , Y , Z } ) )
23 22 eleq2d 
 |-  ( ( ph /\ X = ( 0g ` U ) ) -> ( z e. ( N ` { Y , Z } ) <-> z e. ( N ` { X , Y , Z } ) ) )
24 23 notbid 
 |-  ( ( ph /\ X = ( 0g ` U ) ) -> ( -. z e. ( N ` { Y , Z } ) <-> -. z e. ( N ` { X , Y , Z } ) ) )
25 24 rexbidv 
 |-  ( ( ph /\ X = ( 0g ` U ) ) -> ( E. z e. V -. z e. ( N ` { Y , Z } ) <-> E. z e. V -. z e. ( N ` { X , Y , Z } ) ) )
26 10 25 mpbid 
 |-  ( ( ph /\ X = ( 0g ` U ) ) -> E. z e. V -. z e. ( N ` { X , Y , Z } ) )
27 1 2 3 4 5 6 8 dvh3dim 
 |-  ( ph -> E. z e. V -. z e. ( N ` { X , Z } ) )
28 27 adantr 
 |-  ( ( ph /\ Y = ( 0g ` U ) ) -> E. z e. V -. z e. ( N ` { X , Z } ) )
29 prssi 
 |-  ( ( X e. V /\ Z e. V ) -> { X , Z } C_ V )
30 6 8 29 syl2anc 
 |-  ( ph -> { X , Z } C_ V )
31 3 11 4 12 30 lspun0 
 |-  ( ph -> ( N ` ( { X , Z } u. { ( 0g ` U ) } ) ) = ( N ` { X , Z } ) )
32 df-tp 
 |-  { X , Z , ( 0g ` U ) } = ( { X , Z } u. { ( 0g ` U ) } )
33 tpcomb 
 |-  { X , Z , ( 0g ` U ) } = { X , ( 0g ` U ) , Z }
34 32 33 eqtr3i 
 |-  ( { X , Z } u. { ( 0g ` U ) } ) = { X , ( 0g ` U ) , Z }
35 tpeq2 
 |-  ( Y = ( 0g ` U ) -> { X , Y , Z } = { X , ( 0g ` U ) , Z } )
36 34 35 eqtr4id 
 |-  ( Y = ( 0g ` U ) -> ( { X , Z } u. { ( 0g ` U ) } ) = { X , Y , Z } )
37 36 fveq2d 
 |-  ( Y = ( 0g ` U ) -> ( N ` ( { X , Z } u. { ( 0g ` U ) } ) ) = ( N ` { X , Y , Z } ) )
38 31 37 sylan9req 
 |-  ( ( ph /\ Y = ( 0g ` U ) ) -> ( N ` { X , Z } ) = ( N ` { X , Y , Z } ) )
39 38 eleq2d 
 |-  ( ( ph /\ Y = ( 0g ` U ) ) -> ( z e. ( N ` { X , Z } ) <-> z e. ( N ` { X , Y , Z } ) ) )
40 39 notbid 
 |-  ( ( ph /\ Y = ( 0g ` U ) ) -> ( -. z e. ( N ` { X , Z } ) <-> -. z e. ( N ` { X , Y , Z } ) ) )
41 40 rexbidv 
 |-  ( ( ph /\ Y = ( 0g ` U ) ) -> ( E. z e. V -. z e. ( N ` { X , Z } ) <-> E. z e. V -. z e. ( N ` { X , Y , Z } ) ) )
42 28 41 mpbid 
 |-  ( ( ph /\ Y = ( 0g ` U ) ) -> E. z e. V -. z e. ( N ` { X , Y , Z } ) )
43 1 2 3 4 5 6 7 dvh3dim 
 |-  ( ph -> E. z e. V -. z e. ( N ` { X , Y } ) )
44 43 adantr 
 |-  ( ( ph /\ Z = ( 0g ` U ) ) -> E. z e. V -. z e. ( N ` { X , Y } ) )
45 prssi 
 |-  ( ( X e. V /\ Y e. V ) -> { X , Y } C_ V )
46 6 7 45 syl2anc 
 |-  ( ph -> { X , Y } C_ V )
47 3 11 4 12 46 lspun0 
 |-  ( ph -> ( N ` ( { X , Y } u. { ( 0g ` U ) } ) ) = ( N ` { X , Y } ) )
48 tpeq3 
 |-  ( Z = ( 0g ` U ) -> { X , Y , Z } = { X , Y , ( 0g ` U ) } )
49 df-tp 
 |-  { X , Y , ( 0g ` U ) } = ( { X , Y } u. { ( 0g ` U ) } )
50 48 49 eqtr2di 
 |-  ( Z = ( 0g ` U ) -> ( { X , Y } u. { ( 0g ` U ) } ) = { X , Y , Z } )
51 50 fveq2d 
 |-  ( Z = ( 0g ` U ) -> ( N ` ( { X , Y } u. { ( 0g ` U ) } ) ) = ( N ` { X , Y , Z } ) )
52 47 51 sylan9req 
 |-  ( ( ph /\ Z = ( 0g ` U ) ) -> ( N ` { X , Y } ) = ( N ` { X , Y , Z } ) )
53 52 eleq2d 
 |-  ( ( ph /\ Z = ( 0g ` U ) ) -> ( z e. ( N ` { X , Y } ) <-> z e. ( N ` { X , Y , Z } ) ) )
54 53 notbid 
 |-  ( ( ph /\ Z = ( 0g ` U ) ) -> ( -. z e. ( N ` { X , Y } ) <-> -. z e. ( N ` { X , Y , Z } ) ) )
55 54 rexbidv 
 |-  ( ( ph /\ Z = ( 0g ` U ) ) -> ( E. z e. V -. z e. ( N ` { X , Y } ) <-> E. z e. V -. z e. ( N ` { X , Y , Z } ) ) )
56 44 55 mpbid 
 |-  ( ( ph /\ Z = ( 0g ` U ) ) -> E. z e. V -. z e. ( N ` { X , Y , Z } ) )
57 5 adantr 
 |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) /\ Z =/= ( 0g ` U ) ) ) -> ( K e. HL /\ W e. H ) )
58 6 adantr 
 |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) /\ Z =/= ( 0g ` U ) ) ) -> X e. V )
59 7 adantr 
 |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) /\ Z =/= ( 0g ` U ) ) ) -> Y e. V )
60 8 adantr 
 |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) /\ Z =/= ( 0g ` U ) ) ) -> Z e. V )
61 simpr1 
 |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) /\ Z =/= ( 0g ` U ) ) ) -> X =/= ( 0g ` U ) )
62 simpr2 
 |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) /\ Z =/= ( 0g ` U ) ) ) -> Y =/= ( 0g ` U ) )
63 simpr3 
 |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) /\ Z =/= ( 0g ` U ) ) ) -> Z =/= ( 0g ` U ) )
64 1 2 3 4 57 58 59 60 11 61 62 63 dvh4dimlem 
 |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ Y =/= ( 0g ` U ) /\ Z =/= ( 0g ` U ) ) ) -> E. z e. V -. z e. ( N ` { X , Y , Z } ) )
65 26 42 56 64 pm2.61da3ne 
 |-  ( ph -> E. z e. V -. z e. ( N ` { X , Y , Z } ) )