Metamath Proof Explorer

Theorem dvh3dim3N

Description: There is a vector that is outside of 2 spans. TODO: decide to use either this or dvh3dim2 everywhere. If this one is needed, make dvh3dim2 into a lemma. (Contributed by NM, 21-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 )
dvh3dim3.t 
|- ( ph -> T e. V )
Assertion dvh3dim3N 
|- ( ph -> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { Z , T } ) ) )

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 dvh3dim3.t 
 |-  ( ph -> T e. V )
10 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
11 1 2 5 dvhlmod 
 |-  ( ph -> U e. LMod )
12 11 adantr 
 |-  ( ( ph /\ Y e. ( N ` { Z , T } ) ) -> U e. LMod )
13 3 10 4 11 8 9 lspprcl 
 |-  ( ph -> ( N ` { Z , T } ) e. ( LSubSp ` U ) )
14 13 adantr 
 |-  ( ( ph /\ Y e. ( N ` { Z , T } ) ) -> ( N ` { Z , T } ) e. ( LSubSp ` U ) )
15 simpr 
 |-  ( ( ph /\ Y e. ( N ` { Z , T } ) ) -> Y e. ( N ` { Z , T } ) )
16 3 4 11 8 9 lspprid2 
 |-  ( ph -> T e. ( N ` { Z , T } ) )
17 16 adantr 
 |-  ( ( ph /\ Y e. ( N ` { Z , T } ) ) -> T e. ( N ` { Z , T } ) )
18 10 4 12 14 15 17 lspprss 
 |-  ( ( ph /\ Y e. ( N ` { Z , T } ) ) -> ( N ` { Y , T } ) C_ ( N ` { Z , T } ) )
19 sspss 
 |-  ( ( N ` { Y , T } ) C_ ( N ` { Z , T } ) <-> ( ( N ` { Y , T } ) C. ( N ` { Z , T } ) \/ ( N ` { Y , T } ) = ( N ` { Z , T } ) ) )
20 18 19 sylib 
 |-  ( ( ph /\ Y e. ( N ` { Z , T } ) ) -> ( ( N ` { Y , T } ) C. ( N ` { Z , T } ) \/ ( N ` { Y , T } ) = ( N ` { Z , T } ) ) )
21 1 2 5 dvhlvec 
 |-  ( ph -> U e. LVec )
22 21 adantr 
 |-  ( ( ph /\ ( N ` { Y , T } ) C. ( N ` { Z , T } ) ) -> U e. LVec )
23 3 10 4 11 7 9 lspprcl 
 |-  ( ph -> ( N ` { Y , T } ) e. ( LSubSp ` U ) )
24 23 adantr 
 |-  ( ( ph /\ ( N ` { Y , T } ) C. ( N ` { Z , T } ) ) -> ( N ` { Y , T } ) e. ( LSubSp ` U ) )
25 8 adantr 
 |-  ( ( ph /\ ( N ` { Y , T } ) C. ( N ` { Z , T } ) ) -> Z e. V )
26 9 adantr 
 |-  ( ( ph /\ ( N ` { Y , T } ) C. ( N ` { Z , T } ) ) -> T e. V )
27 simpr 
 |-  ( ( ph /\ ( N ` { Y , T } ) C. ( N ` { Z , T } ) ) -> ( N ` { Y , T } ) C. ( N ` { Z , T } ) )
28 3 10 4 22 24 25 26 27 lspprat 
 |-  ( ( ph /\ ( N ` { Y , T } ) C. ( N ` { Z , T } ) ) -> E. w e. V ( N ` { Y , T } ) = ( N ` { w } ) )
29 5 3ad2ant1 
 |-  ( ( ph /\ w e. V /\ ( N ` { Y , T } ) = ( N ` { w } ) ) -> ( K e. HL /\ W e. H ) )
30 simp2 
 |-  ( ( ph /\ w e. V /\ ( N ` { Y , T } ) = ( N ` { w } ) ) -> w e. V )
31 6 3ad2ant1 
 |-  ( ( ph /\ w e. V /\ ( N ` { Y , T } ) = ( N ` { w } ) ) -> X e. V )
32 8 3ad2ant1 
 |-  ( ( ph /\ w e. V /\ ( N ` { Y , T } ) = ( N ` { w } ) ) -> Z e. V )
33 1 2 3 4 29 30 31 32 dvh3dim2 
 |-  ( ( ph /\ w e. V /\ ( N ` { Y , T } ) = ( N ` { w } ) ) -> E. z e. V ( -. z e. ( N ` { w , X } ) /\ -. z e. ( N ` { w , Z } ) ) )
34 11 3ad2ant1 
 |-  ( ( ph /\ w e. V /\ ( N ` { Y , T } ) = ( N ` { w } ) ) -> U e. LMod )
35 10 lsssssubg 
 |-  ( U e. LMod -> ( LSubSp ` U ) C_ ( SubGrp ` U ) )
36 34 35 syl 
 |-  ( ( ph /\ w e. V /\ ( N ` { Y , T } ) = ( N ` { w } ) ) -> ( LSubSp ` U ) C_ ( SubGrp ` U ) )
37 3 10 4 lspsncl 
 |-  ( ( U e. LMod /\ X e. V ) -> ( N ` { X } ) e. ( LSubSp ` U ) )
38 11 6 37 syl2anc 
 |-  ( ph -> ( N ` { X } ) e. ( LSubSp ` U ) )
39 38 3ad2ant1 
 |-  ( ( ph /\ w e. V /\ ( N ` { Y , T } ) = ( N ` { w } ) ) -> ( N ` { X } ) e. ( LSubSp ` U ) )
40 36 39 sseldd 
 |-  ( ( ph /\ w e. V /\ ( N ` { Y , T } ) = ( N ` { w } ) ) -> ( N ` { X } ) e. ( SubGrp ` U ) )
41 3 10 4 lspsncl 
 |-  ( ( U e. LMod /\ w e. V ) -> ( N ` { w } ) e. ( LSubSp ` U ) )
42 34 30 41 syl2anc 
 |-  ( ( ph /\ w e. V /\ ( N ` { Y , T } ) = ( N ` { w } ) ) -> ( N ` { w } ) e. ( LSubSp ` U ) )
43 36 42 sseldd 
 |-  ( ( ph /\ w e. V /\ ( N ` { Y , T } ) = ( N ` { w } ) ) -> ( N ` { w } ) e. ( SubGrp ` U ) )
44 prssi 
 |-  ( ( Y e. V /\ T e. V ) -> { Y , T } C_ V )
45 7 9 44 syl2anc 
 |-  ( ph -> { Y , T } C_ V )
46 snsspr1 
 |-  { Y } C_ { Y , T }
47 46 a1i 
 |-  ( ph -> { Y } C_ { Y , T } )
48 3 4 lspss 
 |-  ( ( U e. LMod /\ { Y , T } C_ V /\ { Y } C_ { Y , T } ) -> ( N ` { Y } ) C_ ( N ` { Y , T } ) )
49 11 45 47 48 syl3anc 
 |-  ( ph -> ( N ` { Y } ) C_ ( N ` { Y , T } ) )
50 49 3ad2ant1 
 |-  ( ( ph /\ w e. V /\ ( N ` { Y , T } ) = ( N ` { w } ) ) -> ( N ` { Y } ) C_ ( N ` { Y , T } ) )
51 simp3 
 |-  ( ( ph /\ w e. V /\ ( N ` { Y , T } ) = ( N ` { w } ) ) -> ( N ` { Y , T } ) = ( N ` { w } ) )
52 50 51 sseqtrd 
 |-  ( ( ph /\ w e. V /\ ( N ` { Y , T } ) = ( N ` { w } ) ) -> ( N ` { Y } ) C_ ( N ` { w } ) )
53 eqid 
 |-  ( LSSum ` U ) = ( LSSum ` U )
54 53 lsmless2 
 |-  ( ( ( N ` { X } ) e. ( SubGrp ` U ) /\ ( N ` { w } ) e. ( SubGrp ` U ) /\ ( N ` { Y } ) C_ ( N ` { w } ) ) -> ( ( N ` { X } ) ( LSSum ` U ) ( N ` { Y } ) ) C_ ( ( N ` { X } ) ( LSSum ` U ) ( N ` { w } ) ) )
55 40 43 52 54 syl3anc 
 |-  ( ( ph /\ w e. V /\ ( N ` { Y , T } ) = ( N ` { w } ) ) -> ( ( N ` { X } ) ( LSSum ` U ) ( N ` { Y } ) ) C_ ( ( N ` { X } ) ( LSSum ` U ) ( N ` { w } ) ) )
56 3 4 53 11 6 7 lsmpr 
 |-  ( ph -> ( N ` { X , Y } ) = ( ( N ` { X } ) ( LSSum ` U ) ( N ` { Y } ) ) )
57 56 3ad2ant1 
 |-  ( ( ph /\ w e. V /\ ( N ` { Y , T } ) = ( N ` { w } ) ) -> ( N ` { X , Y } ) = ( ( N ` { X } ) ( LSSum ` U ) ( N ` { Y } ) ) )
58 prcom 
 |-  { w , X } = { X , w }
59 58 fveq2i 
 |-  ( N ` { w , X } ) = ( N ` { X , w } )
60 3 4 53 34 31 30 lsmpr 
 |-  ( ( ph /\ w e. V /\ ( N ` { Y , T } ) = ( N ` { w } ) ) -> ( N ` { X , w } ) = ( ( N ` { X } ) ( LSSum ` U ) ( N ` { w } ) ) )
61 59 60 syl5eq 
 |-  ( ( ph /\ w e. V /\ ( N ` { Y , T } ) = ( N ` { w } ) ) -> ( N ` { w , X } ) = ( ( N ` { X } ) ( LSSum ` U ) ( N ` { w } ) ) )
62 55 57 61 3sstr4d 
 |-  ( ( ph /\ w e. V /\ ( N ` { Y , T } ) = ( N ` { w } ) ) -> ( N ` { X , Y } ) C_ ( N ` { w , X } ) )
63 62 ssneld 
 |-  ( ( ph /\ w e. V /\ ( N ` { Y , T } ) = ( N ` { w } ) ) -> ( -. z e. ( N ` { w , X } ) -> -. z e. ( N ` { X , Y } ) ) )
64 3 10 4 lspsncl 
 |-  ( ( U e. LMod /\ Z e. V ) -> ( N ` { Z } ) e. ( LSubSp ` U ) )
65 11 8 64 syl2anc 
 |-  ( ph -> ( N ` { Z } ) e. ( LSubSp ` U ) )
66 65 3ad2ant1 
 |-  ( ( ph /\ w e. V /\ ( N ` { Y , T } ) = ( N ` { w } ) ) -> ( N ` { Z } ) e. ( LSubSp ` U ) )
67 36 66 sseldd 
 |-  ( ( ph /\ w e. V /\ ( N ` { Y , T } ) = ( N ` { w } ) ) -> ( N ` { Z } ) e. ( SubGrp ` U ) )
68 snsspr2 
 |-  { T } C_ { Y , T }
69 68 a1i 
 |-  ( ph -> { T } C_ { Y , T } )
70 3 4 lspss 
 |-  ( ( U e. LMod /\ { Y , T } C_ V /\ { T } C_ { Y , T } ) -> ( N ` { T } ) C_ ( N ` { Y , T } ) )
71 11 45 69 70 syl3anc 
 |-  ( ph -> ( N ` { T } ) C_ ( N ` { Y , T } ) )
72 71 3ad2ant1 
 |-  ( ( ph /\ w e. V /\ ( N ` { Y , T } ) = ( N ` { w } ) ) -> ( N ` { T } ) C_ ( N ` { Y , T } ) )
73 72 51 sseqtrd 
 |-  ( ( ph /\ w e. V /\ ( N ` { Y , T } ) = ( N ` { w } ) ) -> ( N ` { T } ) C_ ( N ` { w } ) )
74 53 lsmless2 
 |-  ( ( ( N ` { Z } ) e. ( SubGrp ` U ) /\ ( N ` { w } ) e. ( SubGrp ` U ) /\ ( N ` { T } ) C_ ( N ` { w } ) ) -> ( ( N ` { Z } ) ( LSSum ` U ) ( N ` { T } ) ) C_ ( ( N ` { Z } ) ( LSSum ` U ) ( N ` { w } ) ) )
75 67 43 73 74 syl3anc 
 |-  ( ( ph /\ w e. V /\ ( N ` { Y , T } ) = ( N ` { w } ) ) -> ( ( N ` { Z } ) ( LSSum ` U ) ( N ` { T } ) ) C_ ( ( N ` { Z } ) ( LSSum ` U ) ( N ` { w } ) ) )
76 3 4 53 11 8 9 lsmpr 
 |-  ( ph -> ( N ` { Z , T } ) = ( ( N ` { Z } ) ( LSSum ` U ) ( N ` { T } ) ) )
77 76 3ad2ant1 
 |-  ( ( ph /\ w e. V /\ ( N ` { Y , T } ) = ( N ` { w } ) ) -> ( N ` { Z , T } ) = ( ( N ` { Z } ) ( LSSum ` U ) ( N ` { T } ) ) )
78 prcom 
 |-  { w , Z } = { Z , w }
79 78 fveq2i 
 |-  ( N ` { w , Z } ) = ( N ` { Z , w } )
80 3 4 53 34 32 30 lsmpr 
 |-  ( ( ph /\ w e. V /\ ( N ` { Y , T } ) = ( N ` { w } ) ) -> ( N ` { Z , w } ) = ( ( N ` { Z } ) ( LSSum ` U ) ( N ` { w } ) ) )
81 79 80 syl5eq 
 |-  ( ( ph /\ w e. V /\ ( N ` { Y , T } ) = ( N ` { w } ) ) -> ( N ` { w , Z } ) = ( ( N ` { Z } ) ( LSSum ` U ) ( N ` { w } ) ) )
82 75 77 81 3sstr4d 
 |-  ( ( ph /\ w e. V /\ ( N ` { Y , T } ) = ( N ` { w } ) ) -> ( N ` { Z , T } ) C_ ( N ` { w , Z } ) )
83 82 ssneld 
 |-  ( ( ph /\ w e. V /\ ( N ` { Y , T } ) = ( N ` { w } ) ) -> ( -. z e. ( N ` { w , Z } ) -> -. z e. ( N ` { Z , T } ) ) )
84 63 83 anim12d 
 |-  ( ( ph /\ w e. V /\ ( N ` { Y , T } ) = ( N ` { w } ) ) -> ( ( -. z e. ( N ` { w , X } ) /\ -. z e. ( N ` { w , Z } ) ) -> ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { Z , T } ) ) ) )
85 84 reximdv 
 |-  ( ( ph /\ w e. V /\ ( N ` { Y , T } ) = ( N ` { w } ) ) -> ( E. z e. V ( -. z e. ( N ` { w , X } ) /\ -. z e. ( N ` { w , Z } ) ) -> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { Z , T } ) ) ) )
86 33 85 mpd 
 |-  ( ( ph /\ w e. V /\ ( N ` { Y , T } ) = ( N ` { w } ) ) -> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { Z , T } ) ) )
87 86 rexlimdv3a 
 |-  ( ph -> ( E. w e. V ( N ` { Y , T } ) = ( N ` { w } ) -> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { Z , T } ) ) ) )
88 87 adantr 
 |-  ( ( ph /\ ( N ` { Y , T } ) C. ( N ` { Z , T } ) ) -> ( E. w e. V ( N ` { Y , T } ) = ( N ` { w } ) -> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { Z , T } ) ) ) )
89 28 88 mpd 
 |-  ( ( ph /\ ( N ` { Y , T } ) C. ( N ` { Z , T } ) ) -> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { Z , T } ) ) )
90 1 2 3 4 5 7 6 9 dvh3dim2 
 |-  ( ph -> E. z e. V ( -. z e. ( N ` { Y , X } ) /\ -. z e. ( N ` { Y , T } ) ) )
91 90 adantr 
 |-  ( ( ph /\ ( N ` { Y , T } ) = ( N ` { Z , T } ) ) -> E. z e. V ( -. z e. ( N ` { Y , X } ) /\ -. z e. ( N ` { Y , T } ) ) )
92 simpr 
 |-  ( ( ph /\ ( N ` { Y , T } ) = ( N ` { Z , T } ) ) -> ( N ` { Y , T } ) = ( N ` { Z , T } ) )
93 prcom 
 |-  { Y , X } = { X , Y }
94 93 fveq2i 
 |-  ( N ` { Y , X } ) = ( N ` { X , Y } )
95 94 eleq2i 
 |-  ( z e. ( N ` { Y , X } ) <-> z e. ( N ` { X , Y } ) )
96 95 notbii 
 |-  ( -. z e. ( N ` { Y , X } ) <-> -. z e. ( N ` { X , Y } ) )
97 96 a1i 
 |-  ( ( N ` { Y , T } ) = ( N ` { Z , T } ) -> ( -. z e. ( N ` { Y , X } ) <-> -. z e. ( N ` { X , Y } ) ) )
98 eleq2 
 |-  ( ( N ` { Y , T } ) = ( N ` { Z , T } ) -> ( z e. ( N ` { Y , T } ) <-> z e. ( N ` { Z , T } ) ) )
99 98 notbid 
 |-  ( ( N ` { Y , T } ) = ( N ` { Z , T } ) -> ( -. z e. ( N ` { Y , T } ) <-> -. z e. ( N ` { Z , T } ) ) )
100 97 99 anbi12d 
 |-  ( ( N ` { Y , T } ) = ( N ` { Z , T } ) -> ( ( -. z e. ( N ` { Y , X } ) /\ -. z e. ( N ` { Y , T } ) ) <-> ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { Z , T } ) ) ) )
101 92 100 syl 
 |-  ( ( ph /\ ( N ` { Y , T } ) = ( N ` { Z , T } ) ) -> ( ( -. z e. ( N ` { Y , X } ) /\ -. z e. ( N ` { Y , T } ) ) <-> ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { Z , T } ) ) ) )
102 101 rexbidv 
 |-  ( ( ph /\ ( N ` { Y , T } ) = ( N ` { Z , T } ) ) -> ( E. z e. V ( -. z e. ( N ` { Y , X } ) /\ -. z e. ( N ` { Y , T } ) ) <-> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { Z , T } ) ) ) )
103 91 102 mpbid 
 |-  ( ( ph /\ ( N ` { Y , T } ) = ( N ` { Z , T } ) ) -> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { Z , T } ) ) )
104 89 103 jaodan 
 |-  ( ( ph /\ ( ( N ` { Y , T } ) C. ( N ` { Z , T } ) \/ ( N ` { Y , T } ) = ( N ` { Z , T } ) ) ) -> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { Z , T } ) ) )
105 20 104 syldan 
 |-  ( ( ph /\ Y e. ( N ` { Z , T } ) ) -> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { Z , T } ) ) )
106 1 2 3 4 5 7 6 9 dvh3dim2 
 |-  ( ph -> E. w e. V ( -. w e. ( N ` { Y , X } ) /\ -. w e. ( N ` { Y , T } ) ) )
107 106 adantr 
 |-  ( ( ph /\ -. Y e. ( N ` { Z , T } ) ) -> E. w e. V ( -. w e. ( N ` { Y , X } ) /\ -. w e. ( N ` { Y , T } ) ) )
108 simpl1l 
 |-  ( ( ( ( ph /\ -. Y e. ( N ` { Z , T } ) ) /\ w e. V /\ ( -. w e. ( N ` { Y , X } ) /\ -. w e. ( N ` { Y , T } ) ) ) /\ w e. ( N ` { Z , T } ) ) -> ph )
109 108 11 syl 
 |-  ( ( ( ( ph /\ -. Y e. ( N ` { Z , T } ) ) /\ w e. V /\ ( -. w e. ( N ` { Y , X } ) /\ -. w e. ( N ` { Y , T } ) ) ) /\ w e. ( N ` { Z , T } ) ) -> U e. LMod )
110 simpl2 
 |-  ( ( ( ( ph /\ -. Y e. ( N ` { Z , T } ) ) /\ w e. V /\ ( -. w e. ( N ` { Y , X } ) /\ -. w e. ( N ` { Y , T } ) ) ) /\ w e. ( N ` { Z , T } ) ) -> w e. V )
111 108 7 syl 
 |-  ( ( ( ( ph /\ -. Y e. ( N ` { Z , T } ) ) /\ w e. V /\ ( -. w e. ( N ` { Y , X } ) /\ -. w e. ( N ` { Y , T } ) ) ) /\ w e. ( N ` { Z , T } ) ) -> Y e. V )
112 eqid 
 |-  ( +g ` U ) = ( +g ` U )
113 3 112 lmodvacl 
 |-  ( ( U e. LMod /\ w e. V /\ Y e. V ) -> ( w ( +g ` U ) Y ) e. V )
114 109 110 111 113 syl3anc 
 |-  ( ( ( ( ph /\ -. Y e. ( N ` { Z , T } ) ) /\ w e. V /\ ( -. w e. ( N ` { Y , X } ) /\ -. w e. ( N ` { Y , T } ) ) ) /\ w e. ( N ` { Z , T } ) ) -> ( w ( +g ` U ) Y ) e. V )
115 3 10 4 11 6 7 lspprcl 
 |-  ( ph -> ( N ` { X , Y } ) e. ( LSubSp ` U ) )
116 108 115 syl 
 |-  ( ( ( ( ph /\ -. Y e. ( N ` { Z , T } ) ) /\ w e. V /\ ( -. w e. ( N ` { Y , X } ) /\ -. w e. ( N ` { Y , T } ) ) ) /\ w e. ( N ` { Z , T } ) ) -> ( N ` { X , Y } ) e. ( LSubSp ` U ) )
117 3 4 11 6 7 lspprid2 
 |-  ( ph -> Y e. ( N ` { X , Y } ) )
118 108 117 syl 
 |-  ( ( ( ( ph /\ -. Y e. ( N ` { Z , T } ) ) /\ w e. V /\ ( -. w e. ( N ` { Y , X } ) /\ -. w e. ( N ` { Y , T } ) ) ) /\ w e. ( N ` { Z , T } ) ) -> Y e. ( N ` { X , Y } ) )
119 simpl3l 
 |-  ( ( ( ( ph /\ -. Y e. ( N ` { Z , T } ) ) /\ w e. V /\ ( -. w e. ( N ` { Y , X } ) /\ -. w e. ( N ` { Y , T } ) ) ) /\ w e. ( N ` { Z , T } ) ) -> -. w e. ( N ` { Y , X } ) )
120 94 eleq2i 
 |-  ( w e. ( N ` { Y , X } ) <-> w e. ( N ` { X , Y } ) )
121 119 120 sylnib 
 |-  ( ( ( ( ph /\ -. Y e. ( N ` { Z , T } ) ) /\ w e. V /\ ( -. w e. ( N ` { Y , X } ) /\ -. w e. ( N ` { Y , T } ) ) ) /\ w e. ( N ` { Z , T } ) ) -> -. w e. ( N ` { X , Y } ) )
122 3 112 10 109 116 118 110 121 lssvancl2 
 |-  ( ( ( ( ph /\ -. Y e. ( N ` { Z , T } ) ) /\ w e. V /\ ( -. w e. ( N ` { Y , X } ) /\ -. w e. ( N ` { Y , T } ) ) ) /\ w e. ( N ` { Z , T } ) ) -> -. ( w ( +g ` U ) Y ) e. ( N ` { X , Y } ) )
123 108 13 syl 
 |-  ( ( ( ( ph /\ -. Y e. ( N ` { Z , T } ) ) /\ w e. V /\ ( -. w e. ( N ` { Y , X } ) /\ -. w e. ( N ` { Y , T } ) ) ) /\ w e. ( N ` { Z , T } ) ) -> ( N ` { Z , T } ) e. ( LSubSp ` U ) )
124 simpr 
 |-  ( ( ( ( ph /\ -. Y e. ( N ` { Z , T } ) ) /\ w e. V /\ ( -. w e. ( N ` { Y , X } ) /\ -. w e. ( N ` { Y , T } ) ) ) /\ w e. ( N ` { Z , T } ) ) -> w e. ( N ` { Z , T } ) )
125 simpl1r 
 |-  ( ( ( ( ph /\ -. Y e. ( N ` { Z , T } ) ) /\ w e. V /\ ( -. w e. ( N ` { Y , X } ) /\ -. w e. ( N ` { Y , T } ) ) ) /\ w e. ( N ` { Z , T } ) ) -> -. Y e. ( N ` { Z , T } ) )
126 3 112 10 109 123 124 111 125 lssvancl1 
 |-  ( ( ( ( ph /\ -. Y e. ( N ` { Z , T } ) ) /\ w e. V /\ ( -. w e. ( N ` { Y , X } ) /\ -. w e. ( N ` { Y , T } ) ) ) /\ w e. ( N ` { Z , T } ) ) -> -. ( w ( +g ` U ) Y ) e. ( N ` { Z , T } ) )
127 eleq1 
 |-  ( z = ( w ( +g ` U ) Y ) -> ( z e. ( N ` { X , Y } ) <-> ( w ( +g ` U ) Y ) e. ( N ` { X , Y } ) ) )
128 127 notbid 
 |-  ( z = ( w ( +g ` U ) Y ) -> ( -. z e. ( N ` { X , Y } ) <-> -. ( w ( +g ` U ) Y ) e. ( N ` { X , Y } ) ) )
129 eleq1 
 |-  ( z = ( w ( +g ` U ) Y ) -> ( z e. ( N ` { Z , T } ) <-> ( w ( +g ` U ) Y ) e. ( N ` { Z , T } ) ) )
130 129 notbid 
 |-  ( z = ( w ( +g ` U ) Y ) -> ( -. z e. ( N ` { Z , T } ) <-> -. ( w ( +g ` U ) Y ) e. ( N ` { Z , T } ) ) )
131 128 130 anbi12d 
 |-  ( z = ( w ( +g ` U ) Y ) -> ( ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { Z , T } ) ) <-> ( -. ( w ( +g ` U ) Y ) e. ( N ` { X , Y } ) /\ -. ( w ( +g ` U ) Y ) e. ( N ` { Z , T } ) ) ) )
132 131 rspcev 
 |-  ( ( ( w ( +g ` U ) Y ) e. V /\ ( -. ( w ( +g ` U ) Y ) e. ( N ` { X , Y } ) /\ -. ( w ( +g ` U ) Y ) e. ( N ` { Z , T } ) ) ) -> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { Z , T } ) ) )
133 114 122 126 132 syl12anc 
 |-  ( ( ( ( ph /\ -. Y e. ( N ` { Z , T } ) ) /\ w e. V /\ ( -. w e. ( N ` { Y , X } ) /\ -. w e. ( N ` { Y , T } ) ) ) /\ w e. ( N ` { Z , T } ) ) -> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { Z , T } ) ) )
134 simpl2 
 |-  ( ( ( ( ph /\ -. Y e. ( N ` { Z , T } ) ) /\ w e. V /\ ( -. w e. ( N ` { Y , X } ) /\ -. w e. ( N ` { Y , T } ) ) ) /\ -. w e. ( N ` { Z , T } ) ) -> w e. V )
135 simpl3l 
 |-  ( ( ( ( ph /\ -. Y e. ( N ` { Z , T } ) ) /\ w e. V /\ ( -. w e. ( N ` { Y , X } ) /\ -. w e. ( N ` { Y , T } ) ) ) /\ -. w e. ( N ` { Z , T } ) ) -> -. w e. ( N ` { Y , X } ) )
136 135 120 sylnib 
 |-  ( ( ( ( ph /\ -. Y e. ( N ` { Z , T } ) ) /\ w e. V /\ ( -. w e. ( N ` { Y , X } ) /\ -. w e. ( N ` { Y , T } ) ) ) /\ -. w e. ( N ` { Z , T } ) ) -> -. w e. ( N ` { X , Y } ) )
137 simpr 
 |-  ( ( ( ( ph /\ -. Y e. ( N ` { Z , T } ) ) /\ w e. V /\ ( -. w e. ( N ` { Y , X } ) /\ -. w e. ( N ` { Y , T } ) ) ) /\ -. w e. ( N ` { Z , T } ) ) -> -. w e. ( N ` { Z , T } ) )
138 eleq1 
 |-  ( z = w -> ( z e. ( N ` { X , Y } ) <-> w e. ( N ` { X , Y } ) ) )
139 138 notbid 
 |-  ( z = w -> ( -. z e. ( N ` { X , Y } ) <-> -. w e. ( N ` { X , Y } ) ) )
140 eleq1 
 |-  ( z = w -> ( z e. ( N ` { Z , T } ) <-> w e. ( N ` { Z , T } ) ) )
141 140 notbid 
 |-  ( z = w -> ( -. z e. ( N ` { Z , T } ) <-> -. w e. ( N ` { Z , T } ) ) )
142 139 141 anbi12d 
 |-  ( z = w -> ( ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { Z , T } ) ) <-> ( -. w e. ( N ` { X , Y } ) /\ -. w e. ( N ` { Z , T } ) ) ) )
143 142 rspcev 
 |-  ( ( w e. V /\ ( -. w e. ( N ` { X , Y } ) /\ -. w e. ( N ` { Z , T } ) ) ) -> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { Z , T } ) ) )
144 134 136 137 143 syl12anc 
 |-  ( ( ( ( ph /\ -. Y e. ( N ` { Z , T } ) ) /\ w e. V /\ ( -. w e. ( N ` { Y , X } ) /\ -. w e. ( N ` { Y , T } ) ) ) /\ -. w e. ( N ` { Z , T } ) ) -> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { Z , T } ) ) )
145 133 144 pm2.61dan 
 |-  ( ( ( ph /\ -. Y e. ( N ` { Z , T } ) ) /\ w e. V /\ ( -. w e. ( N ` { Y , X } ) /\ -. w e. ( N ` { Y , T } ) ) ) -> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { Z , T } ) ) )
146 145 rexlimdv3a 
 |-  ( ( ph /\ -. Y e. ( N ` { Z , T } ) ) -> ( E. w e. V ( -. w e. ( N ` { Y , X } ) /\ -. w e. ( N ` { Y , T } ) ) -> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { Z , T } ) ) ) )
147 107 146 mpd 
 |-  ( ( ph /\ -. Y e. ( N ` { Z , T } ) ) -> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { Z , T } ) ) )
148 105 147 pm2.61dan 
 |-  ( ph -> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { Z , T } ) ) )