Metamath Proof Explorer

Theorem axtgupdim2

Description: Upper dimension axiom for dimension 2, Axiom A9 of Schwabhauser p. 13. Three points X , Y and Z equidistant to two given two points U and V must be colinear. (Contributed by Thierry Arnoux, 29-May-2019) (Revised by Thierry Arnoux, 11-Jul-2020)

Ref Expression
Hypotheses axtrkge.p 
|- P = ( Base ` G )
axtrkge.d 
|- .- = ( dist ` G )
axtrkge.i 
|- I = ( Itv ` G )
axtgupdim2.x 
|- ( ph -> X e. P )
axtgupdim2.y 
|- ( ph -> Y e. P )
axtgupdim2.z 
|- ( ph -> Z e. P )
axtgupdim2.u 
|- ( ph -> U e. P )
axtgupdim2.v 
|- ( ph -> V e. P )
axtgupdim2.0 
|- ( ph -> U =/= V )
axtgupdim2.1 
|- ( ph -> ( U .- X ) = ( V .- X ) )
axtgupdim2.2 
|- ( ph -> ( U .- Y ) = ( V .- Y ) )
axtgupdim2.3 
|- ( ph -> ( U .- Z ) = ( V .- Z ) )
axtgupdim2.w 
|- ( ph -> G e. V )
axtgupdim2.g 
|- ( ph -> -. G TarskiGDim>= 3 )
Assertion axtgupdim2 
|- ( ph -> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) )

Proof

Step Hyp Ref Expression
1 axtrkge.p 
 |-  P = ( Base ` G )
2 axtrkge.d 
 |-  .- = ( dist ` G )
3 axtrkge.i 
 |-  I = ( Itv ` G )
4 axtgupdim2.x 
 |-  ( ph -> X e. P )
5 axtgupdim2.y 
 |-  ( ph -> Y e. P )
6 axtgupdim2.z 
 |-  ( ph -> Z e. P )
7 axtgupdim2.u 
 |-  ( ph -> U e. P )
8 axtgupdim2.v 
 |-  ( ph -> V e. P )
9 axtgupdim2.0 
 |-  ( ph -> U =/= V )
10 axtgupdim2.1 
 |-  ( ph -> ( U .- X ) = ( V .- X ) )
11 axtgupdim2.2 
 |-  ( ph -> ( U .- Y ) = ( V .- Y ) )
12 axtgupdim2.3 
 |-  ( ph -> ( U .- Z ) = ( V .- Z ) )
13 axtgupdim2.w 
 |-  ( ph -> G e. V )
14 axtgupdim2.g 
 |-  ( ph -> -. G TarskiGDim>= 3 )
15 1 2 3 istrkg3ld 
 |-  ( G e. V -> ( G TarskiGDim>= 3 <-> E. u e. P E. v e. P ( u =/= v /\ E. x e. P E. y e. P E. z e. P ( ( ( u .- x ) = ( v .- x ) /\ ( u .- y ) = ( v .- y ) /\ ( u .- z ) = ( v .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) ) )
16 13 15 syl 
 |-  ( ph -> ( G TarskiGDim>= 3 <-> E. u e. P E. v e. P ( u =/= v /\ E. x e. P E. y e. P E. z e. P ( ( ( u .- x ) = ( v .- x ) /\ ( u .- y ) = ( v .- y ) /\ ( u .- z ) = ( v .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) ) )
17 14 16 mtbid 
 |-  ( ph -> -. E. u e. P E. v e. P ( u =/= v /\ E. x e. P E. y e. P E. z e. P ( ( ( u .- x ) = ( v .- x ) /\ ( u .- y ) = ( v .- y ) /\ ( u .- z ) = ( v .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) )
18 ralnex2 
 |-  ( A. u e. P A. v e. P -. ( u =/= v /\ E. x e. P E. y e. P E. z e. P ( ( ( u .- x ) = ( v .- x ) /\ ( u .- y ) = ( v .- y ) /\ ( u .- z ) = ( v .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) <-> -. E. u e. P E. v e. P ( u =/= v /\ E. x e. P E. y e. P E. z e. P ( ( ( u .- x ) = ( v .- x ) /\ ( u .- y ) = ( v .- y ) /\ ( u .- z ) = ( v .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) )
19 17 18 sylibr 
 |-  ( ph -> A. u e. P A. v e. P -. ( u =/= v /\ E. x e. P E. y e. P E. z e. P ( ( ( u .- x ) = ( v .- x ) /\ ( u .- y ) = ( v .- y ) /\ ( u .- z ) = ( v .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) )
20 neeq1 
 |-  ( u = U -> ( u =/= v <-> U =/= v ) )
21 oveq1 
 |-  ( u = U -> ( u .- x ) = ( U .- x ) )
22 21 eqeq1d 
 |-  ( u = U -> ( ( u .- x ) = ( v .- x ) <-> ( U .- x ) = ( v .- x ) ) )
23 oveq1 
 |-  ( u = U -> ( u .- y ) = ( U .- y ) )
24 23 eqeq1d 
 |-  ( u = U -> ( ( u .- y ) = ( v .- y ) <-> ( U .- y ) = ( v .- y ) ) )
25 oveq1 
 |-  ( u = U -> ( u .- z ) = ( U .- z ) )
26 25 eqeq1d 
 |-  ( u = U -> ( ( u .- z ) = ( v .- z ) <-> ( U .- z ) = ( v .- z ) ) )
27 22 24 26 3anbi123d 
 |-  ( u = U -> ( ( ( u .- x ) = ( v .- x ) /\ ( u .- y ) = ( v .- y ) /\ ( u .- z ) = ( v .- z ) ) <-> ( ( U .- x ) = ( v .- x ) /\ ( U .- y ) = ( v .- y ) /\ ( U .- z ) = ( v .- z ) ) ) )
28 27 anbi1d 
 |-  ( u = U -> ( ( ( ( u .- x ) = ( v .- x ) /\ ( u .- y ) = ( v .- y ) /\ ( u .- z ) = ( v .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) <-> ( ( ( U .- x ) = ( v .- x ) /\ ( U .- y ) = ( v .- y ) /\ ( U .- z ) = ( v .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) )
29 28 rexbidv 
 |-  ( u = U -> ( E. z e. P ( ( ( u .- x ) = ( v .- x ) /\ ( u .- y ) = ( v .- y ) /\ ( u .- z ) = ( v .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) <-> E. z e. P ( ( ( U .- x ) = ( v .- x ) /\ ( U .- y ) = ( v .- y ) /\ ( U .- z ) = ( v .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) )
30 29 2rexbidv 
 |-  ( u = U -> ( E. x e. P E. y e. P E. z e. P ( ( ( u .- x ) = ( v .- x ) /\ ( u .- y ) = ( v .- y ) /\ ( u .- z ) = ( v .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) <-> E. x e. P E. y e. P E. z e. P ( ( ( U .- x ) = ( v .- x ) /\ ( U .- y ) = ( v .- y ) /\ ( U .- z ) = ( v .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) )
31 20 30 anbi12d 
 |-  ( u = U -> ( ( u =/= v /\ E. x e. P E. y e. P E. z e. P ( ( ( u .- x ) = ( v .- x ) /\ ( u .- y ) = ( v .- y ) /\ ( u .- z ) = ( v .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) <-> ( U =/= v /\ E. x e. P E. y e. P E. z e. P ( ( ( U .- x ) = ( v .- x ) /\ ( U .- y ) = ( v .- y ) /\ ( U .- z ) = ( v .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) ) )
32 31 notbid 
 |-  ( u = U -> ( -. ( u =/= v /\ E. x e. P E. y e. P E. z e. P ( ( ( u .- x ) = ( v .- x ) /\ ( u .- y ) = ( v .- y ) /\ ( u .- z ) = ( v .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) <-> -. ( U =/= v /\ E. x e. P E. y e. P E. z e. P ( ( ( U .- x ) = ( v .- x ) /\ ( U .- y ) = ( v .- y ) /\ ( U .- z ) = ( v .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) ) )
33 neeq2 
 |-  ( v = V -> ( U =/= v <-> U =/= V ) )
34 oveq1 
 |-  ( v = V -> ( v .- x ) = ( V .- x ) )
35 34 eqeq2d 
 |-  ( v = V -> ( ( U .- x ) = ( v .- x ) <-> ( U .- x ) = ( V .- x ) ) )
36 oveq1 
 |-  ( v = V -> ( v .- y ) = ( V .- y ) )
37 36 eqeq2d 
 |-  ( v = V -> ( ( U .- y ) = ( v .- y ) <-> ( U .- y ) = ( V .- y ) ) )
38 oveq1 
 |-  ( v = V -> ( v .- z ) = ( V .- z ) )
39 38 eqeq2d 
 |-  ( v = V -> ( ( U .- z ) = ( v .- z ) <-> ( U .- z ) = ( V .- z ) ) )
40 35 37 39 3anbi123d 
 |-  ( v = V -> ( ( ( U .- x ) = ( v .- x ) /\ ( U .- y ) = ( v .- y ) /\ ( U .- z ) = ( v .- z ) ) <-> ( ( U .- x ) = ( V .- x ) /\ ( U .- y ) = ( V .- y ) /\ ( U .- z ) = ( V .- z ) ) ) )
41 40 anbi1d 
 |-  ( v = V -> ( ( ( ( U .- x ) = ( v .- x ) /\ ( U .- y ) = ( v .- y ) /\ ( U .- z ) = ( v .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) <-> ( ( ( U .- x ) = ( V .- x ) /\ ( U .- y ) = ( V .- y ) /\ ( U .- z ) = ( V .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) )
42 41 rexbidv 
 |-  ( v = V -> ( E. z e. P ( ( ( U .- x ) = ( v .- x ) /\ ( U .- y ) = ( v .- y ) /\ ( U .- z ) = ( v .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) <-> E. z e. P ( ( ( U .- x ) = ( V .- x ) /\ ( U .- y ) = ( V .- y ) /\ ( U .- z ) = ( V .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) )
43 42 2rexbidv 
 |-  ( v = V -> ( E. x e. P E. y e. P E. z e. P ( ( ( U .- x ) = ( v .- x ) /\ ( U .- y ) = ( v .- y ) /\ ( U .- z ) = ( v .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) <-> E. x e. P E. y e. P E. z e. P ( ( ( U .- x ) = ( V .- x ) /\ ( U .- y ) = ( V .- y ) /\ ( U .- z ) = ( V .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) )
44 33 43 anbi12d 
 |-  ( v = V -> ( ( U =/= v /\ E. x e. P E. y e. P E. z e. P ( ( ( U .- x ) = ( v .- x ) /\ ( U .- y ) = ( v .- y ) /\ ( U .- z ) = ( v .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) <-> ( U =/= V /\ E. x e. P E. y e. P E. z e. P ( ( ( U .- x ) = ( V .- x ) /\ ( U .- y ) = ( V .- y ) /\ ( U .- z ) = ( V .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) ) )
45 44 notbid 
 |-  ( v = V -> ( -. ( U =/= v /\ E. x e. P E. y e. P E. z e. P ( ( ( U .- x ) = ( v .- x ) /\ ( U .- y ) = ( v .- y ) /\ ( U .- z ) = ( v .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) <-> -. ( U =/= V /\ E. x e. P E. y e. P E. z e. P ( ( ( U .- x ) = ( V .- x ) /\ ( U .- y ) = ( V .- y ) /\ ( U .- z ) = ( V .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) ) )
46 32 45 rspc2v 
 |-  ( ( U e. P /\ V e. P ) -> ( A. u e. P A. v e. P -. ( u =/= v /\ E. x e. P E. y e. P E. z e. P ( ( ( u .- x ) = ( v .- x ) /\ ( u .- y ) = ( v .- y ) /\ ( u .- z ) = ( v .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) -> -. ( U =/= V /\ E. x e. P E. y e. P E. z e. P ( ( ( U .- x ) = ( V .- x ) /\ ( U .- y ) = ( V .- y ) /\ ( U .- z ) = ( V .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) ) )
47 7 8 46 syl2anc 
 |-  ( ph -> ( A. u e. P A. v e. P -. ( u =/= v /\ E. x e. P E. y e. P E. z e. P ( ( ( u .- x ) = ( v .- x ) /\ ( u .- y ) = ( v .- y ) /\ ( u .- z ) = ( v .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) -> -. ( U =/= V /\ E. x e. P E. y e. P E. z e. P ( ( ( U .- x ) = ( V .- x ) /\ ( U .- y ) = ( V .- y ) /\ ( U .- z ) = ( V .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) ) )
48 19 47 mpd 
 |-  ( ph -> -. ( U =/= V /\ E. x e. P E. y e. P E. z e. P ( ( ( U .- x ) = ( V .- x ) /\ ( U .- y ) = ( V .- y ) /\ ( U .- z ) = ( V .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) )
49 imnan 
 |-  ( ( U =/= V -> -. E. x e. P E. y e. P E. z e. P ( ( ( U .- x ) = ( V .- x ) /\ ( U .- y ) = ( V .- y ) /\ ( U .- z ) = ( V .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) <-> -. ( U =/= V /\ E. x e. P E. y e. P E. z e. P ( ( ( U .- x ) = ( V .- x ) /\ ( U .- y ) = ( V .- y ) /\ ( U .- z ) = ( V .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) )
50 48 49 sylibr 
 |-  ( ph -> ( U =/= V -> -. E. x e. P E. y e. P E. z e. P ( ( ( U .- x ) = ( V .- x ) /\ ( U .- y ) = ( V .- y ) /\ ( U .- z ) = ( V .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) )
51 9 50 mpd 
 |-  ( ph -> -. E. x e. P E. y e. P E. z e. P ( ( ( U .- x ) = ( V .- x ) /\ ( U .- y ) = ( V .- y ) /\ ( U .- z ) = ( V .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) )
52 ralnex3 
 |-  ( A. x e. P A. y e. P A. z e. P -. ( ( ( U .- x ) = ( V .- x ) /\ ( U .- y ) = ( V .- y ) /\ ( U .- z ) = ( V .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) <-> -. E. x e. P E. y e. P E. z e. P ( ( ( U .- x ) = ( V .- x ) /\ ( U .- y ) = ( V .- y ) /\ ( U .- z ) = ( V .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) )
53 51 52 sylibr 
 |-  ( ph -> A. x e. P A. y e. P A. z e. P -. ( ( ( U .- x ) = ( V .- x ) /\ ( U .- y ) = ( V .- y ) /\ ( U .- z ) = ( V .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) )
54 oveq2 
 |-  ( x = X -> ( U .- x ) = ( U .- X ) )
55 oveq2 
 |-  ( x = X -> ( V .- x ) = ( V .- X ) )
56 54 55 eqeq12d 
 |-  ( x = X -> ( ( U .- x ) = ( V .- x ) <-> ( U .- X ) = ( V .- X ) ) )
57 56 3anbi1d 
 |-  ( x = X -> ( ( ( U .- x ) = ( V .- x ) /\ ( U .- y ) = ( V .- y ) /\ ( U .- z ) = ( V .- z ) ) <-> ( ( U .- X ) = ( V .- X ) /\ ( U .- y ) = ( V .- y ) /\ ( U .- z ) = ( V .- z ) ) ) )
58 oveq1 
 |-  ( x = X -> ( x I y ) = ( X I y ) )
59 58 eleq2d 
 |-  ( x = X -> ( z e. ( x I y ) <-> z e. ( X I y ) ) )
60 eleq1 
 |-  ( x = X -> ( x e. ( z I y ) <-> X e. ( z I y ) ) )
61 oveq1 
 |-  ( x = X -> ( x I z ) = ( X I z ) )
62 61 eleq2d 
 |-  ( x = X -> ( y e. ( x I z ) <-> y e. ( X I z ) ) )
63 59 60 62 3orbi123d 
 |-  ( x = X -> ( ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) <-> ( z e. ( X I y ) \/ X e. ( z I y ) \/ y e. ( X I z ) ) ) )
64 63 notbid 
 |-  ( x = X -> ( -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) <-> -. ( z e. ( X I y ) \/ X e. ( z I y ) \/ y e. ( X I z ) ) ) )
65 57 64 anbi12d 
 |-  ( x = X -> ( ( ( ( U .- x ) = ( V .- x ) /\ ( U .- y ) = ( V .- y ) /\ ( U .- z ) = ( V .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) <-> ( ( ( U .- X ) = ( V .- X ) /\ ( U .- y ) = ( V .- y ) /\ ( U .- z ) = ( V .- z ) ) /\ -. ( z e. ( X I y ) \/ X e. ( z I y ) \/ y e. ( X I z ) ) ) ) )
66 65 notbid 
 |-  ( x = X -> ( -. ( ( ( U .- x ) = ( V .- x ) /\ ( U .- y ) = ( V .- y ) /\ ( U .- z ) = ( V .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) <-> -. ( ( ( U .- X ) = ( V .- X ) /\ ( U .- y ) = ( V .- y ) /\ ( U .- z ) = ( V .- z ) ) /\ -. ( z e. ( X I y ) \/ X e. ( z I y ) \/ y e. ( X I z ) ) ) ) )
67 oveq2 
 |-  ( y = Y -> ( U .- y ) = ( U .- Y ) )
68 oveq2 
 |-  ( y = Y -> ( V .- y ) = ( V .- Y ) )
69 67 68 eqeq12d 
 |-  ( y = Y -> ( ( U .- y ) = ( V .- y ) <-> ( U .- Y ) = ( V .- Y ) ) )
70 69 3anbi2d 
 |-  ( y = Y -> ( ( ( U .- X ) = ( V .- X ) /\ ( U .- y ) = ( V .- y ) /\ ( U .- z ) = ( V .- z ) ) <-> ( ( U .- X ) = ( V .- X ) /\ ( U .- Y ) = ( V .- Y ) /\ ( U .- z ) = ( V .- z ) ) ) )
71 oveq2 
 |-  ( y = Y -> ( X I y ) = ( X I Y ) )
72 71 eleq2d 
 |-  ( y = Y -> ( z e. ( X I y ) <-> z e. ( X I Y ) ) )
73 oveq2 
 |-  ( y = Y -> ( z I y ) = ( z I Y ) )
74 73 eleq2d 
 |-  ( y = Y -> ( X e. ( z I y ) <-> X e. ( z I Y ) ) )
75 eleq1 
 |-  ( y = Y -> ( y e. ( X I z ) <-> Y e. ( X I z ) ) )
76 72 74 75 3orbi123d 
 |-  ( y = Y -> ( ( z e. ( X I y ) \/ X e. ( z I y ) \/ y e. ( X I z ) ) <-> ( z e. ( X I Y ) \/ X e. ( z I Y ) \/ Y e. ( X I z ) ) ) )
77 76 notbid 
 |-  ( y = Y -> ( -. ( z e. ( X I y ) \/ X e. ( z I y ) \/ y e. ( X I z ) ) <-> -. ( z e. ( X I Y ) \/ X e. ( z I Y ) \/ Y e. ( X I z ) ) ) )
78 70 77 anbi12d 
 |-  ( y = Y -> ( ( ( ( U .- X ) = ( V .- X ) /\ ( U .- y ) = ( V .- y ) /\ ( U .- z ) = ( V .- z ) ) /\ -. ( z e. ( X I y ) \/ X e. ( z I y ) \/ y e. ( X I z ) ) ) <-> ( ( ( U .- X ) = ( V .- X ) /\ ( U .- Y ) = ( V .- Y ) /\ ( U .- z ) = ( V .- z ) ) /\ -. ( z e. ( X I Y ) \/ X e. ( z I Y ) \/ Y e. ( X I z ) ) ) ) )
79 78 notbid 
 |-  ( y = Y -> ( -. ( ( ( U .- X ) = ( V .- X ) /\ ( U .- y ) = ( V .- y ) /\ ( U .- z ) = ( V .- z ) ) /\ -. ( z e. ( X I y ) \/ X e. ( z I y ) \/ y e. ( X I z ) ) ) <-> -. ( ( ( U .- X ) = ( V .- X ) /\ ( U .- Y ) = ( V .- Y ) /\ ( U .- z ) = ( V .- z ) ) /\ -. ( z e. ( X I Y ) \/ X e. ( z I Y ) \/ Y e. ( X I z ) ) ) ) )
80 oveq2 
 |-  ( z = Z -> ( U .- z ) = ( U .- Z ) )
81 oveq2 
 |-  ( z = Z -> ( V .- z ) = ( V .- Z ) )
82 80 81 eqeq12d 
 |-  ( z = Z -> ( ( U .- z ) = ( V .- z ) <-> ( U .- Z ) = ( V .- Z ) ) )
83 82 3anbi3d 
 |-  ( z = Z -> ( ( ( U .- X ) = ( V .- X ) /\ ( U .- Y ) = ( V .- Y ) /\ ( U .- z ) = ( V .- z ) ) <-> ( ( U .- X ) = ( V .- X ) /\ ( U .- Y ) = ( V .- Y ) /\ ( U .- Z ) = ( V .- Z ) ) ) )
84 eleq1 
 |-  ( z = Z -> ( z e. ( X I Y ) <-> Z e. ( X I Y ) ) )
85 oveq1 
 |-  ( z = Z -> ( z I Y ) = ( Z I Y ) )
86 85 eleq2d 
 |-  ( z = Z -> ( X e. ( z I Y ) <-> X e. ( Z I Y ) ) )
87 oveq2 
 |-  ( z = Z -> ( X I z ) = ( X I Z ) )
88 87 eleq2d 
 |-  ( z = Z -> ( Y e. ( X I z ) <-> Y e. ( X I Z ) ) )
89 84 86 88 3orbi123d 
 |-  ( z = Z -> ( ( z e. ( X I Y ) \/ X e. ( z I Y ) \/ Y e. ( X I z ) ) <-> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) )
90 89 notbid 
 |-  ( z = Z -> ( -. ( z e. ( X I Y ) \/ X e. ( z I Y ) \/ Y e. ( X I z ) ) <-> -. ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) )
91 83 90 anbi12d 
 |-  ( z = Z -> ( ( ( ( U .- X ) = ( V .- X ) /\ ( U .- Y ) = ( V .- Y ) /\ ( U .- z ) = ( V .- z ) ) /\ -. ( z e. ( X I Y ) \/ X e. ( z I Y ) \/ Y e. ( X I z ) ) ) <-> ( ( ( U .- X ) = ( V .- X ) /\ ( U .- Y ) = ( V .- Y ) /\ ( U .- Z ) = ( V .- Z ) ) /\ -. ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) ) )
92 91 notbid 
 |-  ( z = Z -> ( -. ( ( ( U .- X ) = ( V .- X ) /\ ( U .- Y ) = ( V .- Y ) /\ ( U .- z ) = ( V .- z ) ) /\ -. ( z e. ( X I Y ) \/ X e. ( z I Y ) \/ Y e. ( X I z ) ) ) <-> -. ( ( ( U .- X ) = ( V .- X ) /\ ( U .- Y ) = ( V .- Y ) /\ ( U .- Z ) = ( V .- Z ) ) /\ -. ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) ) )
93 66 79 92 rspc3v 
 |-  ( ( X e. P /\ Y e. P /\ Z e. P ) -> ( A. x e. P A. y e. P A. z e. P -. ( ( ( U .- x ) = ( V .- x ) /\ ( U .- y ) = ( V .- y ) /\ ( U .- z ) = ( V .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) -> -. ( ( ( U .- X ) = ( V .- X ) /\ ( U .- Y ) = ( V .- Y ) /\ ( U .- Z ) = ( V .- Z ) ) /\ -. ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) ) )
94 4 5 6 93 syl3anc 
 |-  ( ph -> ( A. x e. P A. y e. P A. z e. P -. ( ( ( U .- x ) = ( V .- x ) /\ ( U .- y ) = ( V .- y ) /\ ( U .- z ) = ( V .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) -> -. ( ( ( U .- X ) = ( V .- X ) /\ ( U .- Y ) = ( V .- Y ) /\ ( U .- Z ) = ( V .- Z ) ) /\ -. ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) ) )
95 53 94 mpd 
 |-  ( ph -> -. ( ( ( U .- X ) = ( V .- X ) /\ ( U .- Y ) = ( V .- Y ) /\ ( U .- Z ) = ( V .- Z ) ) /\ -. ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) )
96 imnan 
 |-  ( ( ( ( U .- X ) = ( V .- X ) /\ ( U .- Y ) = ( V .- Y ) /\ ( U .- Z ) = ( V .- Z ) ) -> -. -. ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) <-> -. ( ( ( U .- X ) = ( V .- X ) /\ ( U .- Y ) = ( V .- Y ) /\ ( U .- Z ) = ( V .- Z ) ) /\ -. ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) )
97 95 96 sylibr 
 |-  ( ph -> ( ( ( U .- X ) = ( V .- X ) /\ ( U .- Y ) = ( V .- Y ) /\ ( U .- Z ) = ( V .- Z ) ) -> -. -. ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) )
98 10 11 12 97 mp3and 
 |-  ( ph -> -. -. ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) )
99 98 notnotrd 
 |-  ( ph -> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) )