Metamath Proof Explorer

Theorem dvh4dimlem

Description: Lemma for dvh4dimN . (Contributed by NM, 22-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 )
dvh4dim.y 
|- ( ph -> Y e. V )
dvhdim.z 
|- ( ph -> Z e. V )
dvh4dim.o 
|- .0. = ( 0g ` U )
dvh4dim.x 
|- ( ph -> X =/= .0. )
dvh4dimlem.y 
|- ( ph -> Y =/= .0. )
dvh4dimlem.z 
|- ( ph -> Z =/= .0. )
Assertion dvh4dimlem 
|- ( 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 dvh4dim.y 
 |-  ( ph -> Y e. V )
8 dvhdim.z 
 |-  ( ph -> Z e. V )
9 dvh4dim.o 
 |-  .0. = ( 0g ` U )
10 dvh4dim.x 
 |-  ( ph -> X =/= .0. )
11 dvh4dimlem.y 
 |-  ( ph -> Y =/= .0. )
12 dvh4dimlem.z 
 |-  ( ph -> Z =/= .0. )
13 eqid 
 |-  ( LSSum ` U ) = ( LSSum ` U )
14 eqid 
 |-  ( LSAtoms ` U ) = ( LSAtoms ` U )
15 1 2 5 dvhlmod 
 |-  ( ph -> U e. LMod )
16 eldifsn 
 |-  ( X e. ( V \ { .0. } ) <-> ( X e. V /\ X =/= .0. ) )
17 6 10 16 sylanbrc 
 |-  ( ph -> X e. ( V \ { .0. } ) )
18 3 4 9 14 15 17 lsatlspsn 
 |-  ( ph -> ( N ` { X } ) e. ( LSAtoms ` U ) )
19 eldifsn 
 |-  ( Y e. ( V \ { .0. } ) <-> ( Y e. V /\ Y =/= .0. ) )
20 7 11 19 sylanbrc 
 |-  ( ph -> Y e. ( V \ { .0. } ) )
21 3 4 9 14 15 20 lsatlspsn 
 |-  ( ph -> ( N ` { Y } ) e. ( LSAtoms ` U ) )
22 eldifsn 
 |-  ( Z e. ( V \ { .0. } ) <-> ( Z e. V /\ Z =/= .0. ) )
23 8 12 22 sylanbrc 
 |-  ( ph -> Z e. ( V \ { .0. } ) )
24 3 4 9 14 15 23 lsatlspsn 
 |-  ( ph -> ( N ` { Z } ) e. ( LSAtoms ` U ) )
25 1 2 13 14 5 18 21 24 dvh4dimat 
 |-  ( ph -> E. p e. ( LSAtoms ` U ) -. p C_ ( ( ( N ` { X } ) ( LSSum ` U ) ( N ` { Y } ) ) ( LSSum ` U ) ( N ` { Z } ) ) )
26 15 3ad2ant1 
 |-  ( ( ph /\ p e. ( LSAtoms ` U ) /\ -. p C_ ( ( ( N ` { X } ) ( LSSum ` U ) ( N ` { Y } ) ) ( LSSum ` U ) ( N ` { Z } ) ) ) -> U e. LMod )
27 simp2 
 |-  ( ( ph /\ p e. ( LSAtoms ` U ) /\ -. p C_ ( ( ( N ` { X } ) ( LSSum ` U ) ( N ` { Y } ) ) ( LSSum ` U ) ( N ` { Z } ) ) ) -> p e. ( LSAtoms ` U ) )
28 3 4 14 islsati 
 |-  ( ( U e. LMod /\ p e. ( LSAtoms ` U ) ) -> E. z e. V p = ( N ` { z } ) )
29 26 27 28 syl2anc 
 |-  ( ( ph /\ p e. ( LSAtoms ` U ) /\ -. p C_ ( ( ( N ` { X } ) ( LSSum ` U ) ( N ` { Y } ) ) ( LSSum ` U ) ( N ` { Z } ) ) ) -> E. z e. V p = ( N ` { z } ) )
30 simp2 
 |-  ( ( ph /\ p = ( N ` { z } ) /\ z e. V ) -> p = ( N ` { z } ) )
31 15 3ad2ant1 
 |-  ( ( ph /\ p = ( N ` { z } ) /\ z e. V ) -> U e. LMod )
32 6 3ad2ant1 
 |-  ( ( ph /\ p = ( N ` { z } ) /\ z e. V ) -> X e. V )
33 7 3ad2ant1 
 |-  ( ( ph /\ p = ( N ` { z } ) /\ z e. V ) -> Y e. V )
34 3 4 13 31 32 33 lsmpr 
 |-  ( ( ph /\ p = ( N ` { z } ) /\ z e. V ) -> ( N ` { X , Y } ) = ( ( N ` { X } ) ( LSSum ` U ) ( N ` { Y } ) ) )
35 34 oveq1d 
 |-  ( ( ph /\ p = ( N ` { z } ) /\ z e. V ) -> ( ( N ` { X , Y } ) ( LSSum ` U ) ( N ` { Z } ) ) = ( ( ( N ` { X } ) ( LSSum ` U ) ( N ` { Y } ) ) ( LSSum ` U ) ( N ` { Z } ) ) )
36 prssi 
 |-  ( ( X e. V /\ Y e. V ) -> { X , Y } C_ V )
37 6 7 36 syl2anc 
 |-  ( ph -> { X , Y } C_ V )
38 37 3ad2ant1 
 |-  ( ( ph /\ p = ( N ` { z } ) /\ z e. V ) -> { X , Y } C_ V )
39 8 snssd 
 |-  ( ph -> { Z } C_ V )
40 39 3ad2ant1 
 |-  ( ( ph /\ p = ( N ` { z } ) /\ z e. V ) -> { Z } C_ V )
41 3 4 13 lsmsp2 
 |-  ( ( U e. LMod /\ { X , Y } C_ V /\ { Z } C_ V ) -> ( ( N ` { X , Y } ) ( LSSum ` U ) ( N ` { Z } ) ) = ( N ` ( { X , Y } u. { Z } ) ) )
42 31 38 40 41 syl3anc 
 |-  ( ( ph /\ p = ( N ` { z } ) /\ z e. V ) -> ( ( N ` { X , Y } ) ( LSSum ` U ) ( N ` { Z } ) ) = ( N ` ( { X , Y } u. { Z } ) ) )
43 35 42 eqtr3d 
 |-  ( ( ph /\ p = ( N ` { z } ) /\ z e. V ) -> ( ( ( N ` { X } ) ( LSSum ` U ) ( N ` { Y } ) ) ( LSSum ` U ) ( N ` { Z } ) ) = ( N ` ( { X , Y } u. { Z } ) ) )
44 30 43 sseq12d 
 |-  ( ( ph /\ p = ( N ` { z } ) /\ z e. V ) -> ( p C_ ( ( ( N ` { X } ) ( LSSum ` U ) ( N ` { Y } ) ) ( LSSum ` U ) ( N ` { Z } ) ) <-> ( N ` { z } ) C_ ( N ` ( { X , Y } u. { Z } ) ) ) )
45 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
46 37 39 unssd 
 |-  ( ph -> ( { X , Y } u. { Z } ) C_ V )
47 3 45 4 lspcl 
 |-  ( ( U e. LMod /\ ( { X , Y } u. { Z } ) C_ V ) -> ( N ` ( { X , Y } u. { Z } ) ) e. ( LSubSp ` U ) )
48 15 46 47 syl2anc 
 |-  ( ph -> ( N ` ( { X , Y } u. { Z } ) ) e. ( LSubSp ` U ) )
49 48 3ad2ant1 
 |-  ( ( ph /\ p = ( N ` { z } ) /\ z e. V ) -> ( N ` ( { X , Y } u. { Z } ) ) e. ( LSubSp ` U ) )
50 simp3 
 |-  ( ( ph /\ p = ( N ` { z } ) /\ z e. V ) -> z e. V )
51 3 45 4 31 49 50 lspsnel5 
 |-  ( ( ph /\ p = ( N ` { z } ) /\ z e. V ) -> ( z e. ( N ` ( { X , Y } u. { Z } ) ) <-> ( N ` { z } ) C_ ( N ` ( { X , Y } u. { Z } ) ) ) )
52 44 51 bitr4d 
 |-  ( ( ph /\ p = ( N ` { z } ) /\ z e. V ) -> ( p C_ ( ( ( N ` { X } ) ( LSSum ` U ) ( N ` { Y } ) ) ( LSSum ` U ) ( N ` { Z } ) ) <-> z e. ( N ` ( { X , Y } u. { Z } ) ) ) )
53 df-tp 
 |-  { X , Y , Z } = ( { X , Y } u. { Z } )
54 53 fveq2i 
 |-  ( N ` { X , Y , Z } ) = ( N ` ( { X , Y } u. { Z } ) )
55 54 eleq2i 
 |-  ( z e. ( N ` { X , Y , Z } ) <-> z e. ( N ` ( { X , Y } u. { Z } ) ) )
56 52 55 bitr4di 
 |-  ( ( ph /\ p = ( N ` { z } ) /\ z e. V ) -> ( p C_ ( ( ( N ` { X } ) ( LSSum ` U ) ( N ` { Y } ) ) ( LSSum ` U ) ( N ` { Z } ) ) <-> z e. ( N ` { X , Y , Z } ) ) )
57 56 notbid 
 |-  ( ( ph /\ p = ( N ` { z } ) /\ z e. V ) -> ( -. p C_ ( ( ( N ` { X } ) ( LSSum ` U ) ( N ` { Y } ) ) ( LSSum ` U ) ( N ` { Z } ) ) <-> -. z e. ( N ` { X , Y , Z } ) ) )
58 57 biimpd 
 |-  ( ( ph /\ p = ( N ` { z } ) /\ z e. V ) -> ( -. p C_ ( ( ( N ` { X } ) ( LSSum ` U ) ( N ` { Y } ) ) ( LSSum ` U ) ( N ` { Z } ) ) -> -. z e. ( N ` { X , Y , Z } ) ) )
59 58 3exp 
 |-  ( ph -> ( p = ( N ` { z } ) -> ( z e. V -> ( -. p C_ ( ( ( N ` { X } ) ( LSSum ` U ) ( N ` { Y } ) ) ( LSSum ` U ) ( N ` { Z } ) ) -> -. z e. ( N ` { X , Y , Z } ) ) ) ) )
60 59 com24 
 |-  ( ph -> ( -. p C_ ( ( ( N ` { X } ) ( LSSum ` U ) ( N ` { Y } ) ) ( LSSum ` U ) ( N ` { Z } ) ) -> ( z e. V -> ( p = ( N ` { z } ) -> -. z e. ( N ` { X , Y , Z } ) ) ) ) )
61 60 a1d 
 |-  ( ph -> ( p e. ( LSAtoms ` U ) -> ( -. p C_ ( ( ( N ` { X } ) ( LSSum ` U ) ( N ` { Y } ) ) ( LSSum ` U ) ( N ` { Z } ) ) -> ( z e. V -> ( p = ( N ` { z } ) -> -. z e. ( N ` { X , Y , Z } ) ) ) ) ) )
62 61 3imp 
 |-  ( ( ph /\ p e. ( LSAtoms ` U ) /\ -. p C_ ( ( ( N ` { X } ) ( LSSum ` U ) ( N ` { Y } ) ) ( LSSum ` U ) ( N ` { Z } ) ) ) -> ( z e. V -> ( p = ( N ` { z } ) -> -. z e. ( N ` { X , Y , Z } ) ) ) )
63 62 reximdvai 
 |-  ( ( ph /\ p e. ( LSAtoms ` U ) /\ -. p C_ ( ( ( N ` { X } ) ( LSSum ` U ) ( N ` { Y } ) ) ( LSSum ` U ) ( N ` { Z } ) ) ) -> ( E. z e. V p = ( N ` { z } ) -> E. z e. V -. z e. ( N ` { X , Y , Z } ) ) )
64 29 63 mpd 
 |-  ( ( ph /\ p e. ( LSAtoms ` U ) /\ -. p C_ ( ( ( N ` { X } ) ( LSSum ` U ) ( N ` { Y } ) ) ( LSSum ` U ) ( N ` { Z } ) ) ) -> E. z e. V -. z e. ( N ` { X , Y , Z } ) )
65 64 rexlimdv3a 
 |-  ( ph -> ( E. p e. ( LSAtoms ` U ) -. p C_ ( ( ( N ` { X } ) ( LSSum ` U ) ( N ` { Y } ) ) ( LSSum ` U ) ( N ` { Z } ) ) -> E. z e. V -. z e. ( N ` { X , Y , Z } ) ) )
66 25 65 mpd 
 |-  ( ph -> E. z e. V -. z e. ( N ` { X , Y , Z } ) )