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 φ X P
axtgupdim2.y φ Y P
axtgupdim2.z φ Z P
axtgupdim2.u φ U P
axtgupdim2.v φ V P
axtgupdim2.0 φ U V
axtgupdim2.1 φ U - ˙ X = V - ˙ X
axtgupdim2.2 φ U - ˙ Y = V - ˙ Y
axtgupdim2.3 φ U - ˙ Z = V - ˙ Z
axtgupdim2.w φ G V
axtgupdim2.g φ ¬ G Dim 𝒢 3
Assertion axtgupdim2 φ Z X I Y X Z I Y Y 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 φ X P
5 axtgupdim2.y φ Y P
6 axtgupdim2.z φ Z P
7 axtgupdim2.u φ U P
8 axtgupdim2.v φ V P
9 axtgupdim2.0 φ U V
10 axtgupdim2.1 φ U - ˙ X = V - ˙ X
11 axtgupdim2.2 φ U - ˙ Y = V - ˙ Y
12 axtgupdim2.3 φ U - ˙ Z = V - ˙ Z
13 axtgupdim2.w φ G V
14 axtgupdim2.g φ ¬ G Dim 𝒢 3
15 1 2 3 istrkg3ld G V G Dim 𝒢 3 u P v P u v x P y P z P u - ˙ x = v - ˙ x u - ˙ y = v - ˙ y u - ˙ z = v - ˙ z ¬ z x I y x z I y y x I z
16 13 15 syl φ G Dim 𝒢 3 u P v P u v x P y P z P u - ˙ x = v - ˙ x u - ˙ y = v - ˙ y u - ˙ z = v - ˙ z ¬ z x I y x z I y y x I z
17 14 16 mtbid φ ¬ u P v P u v x P y P z P u - ˙ x = v - ˙ x u - ˙ y = v - ˙ y u - ˙ z = v - ˙ z ¬ z x I y x z I y y x I z
18 ralnex2 u P v P ¬ u v x P y P z P u - ˙ x = v - ˙ x u - ˙ y = v - ˙ y u - ˙ z = v - ˙ z ¬ z x I y x z I y y x I z ¬ u P v P u v x P y P z P u - ˙ x = v - ˙ x u - ˙ y = v - ˙ y u - ˙ z = v - ˙ z ¬ z x I y x z I y y x I z
19 17 18 sylibr φ u P v P ¬ u v x P y P z P u - ˙ x = v - ˙ x u - ˙ y = v - ˙ y u - ˙ z = v - ˙ z ¬ z x I y x z I y y 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 x I y x z I y y x I z U - ˙ x = v - ˙ x U - ˙ y = v - ˙ y U - ˙ z = v - ˙ z ¬ z x I y x z I y y x I z
29 28 rexbidv u = U z P u - ˙ x = v - ˙ x u - ˙ y = v - ˙ y u - ˙ z = v - ˙ z ¬ z x I y x z I y y x I z z P U - ˙ x = v - ˙ x U - ˙ y = v - ˙ y U - ˙ z = v - ˙ z ¬ z x I y x z I y y x I z
30 29 2rexbidv u = U x P y P z P u - ˙ x = v - ˙ x u - ˙ y = v - ˙ y u - ˙ z = v - ˙ z ¬ z x I y x z I y y x I z x P y P z P U - ˙ x = v - ˙ x U - ˙ y = v - ˙ y U - ˙ z = v - ˙ z ¬ z x I y x z I y y x I z
31 20 30 anbi12d u = U u v x P y P z P u - ˙ x = v - ˙ x u - ˙ y = v - ˙ y u - ˙ z = v - ˙ z ¬ z x I y x z I y y x I z U v x P y P z P U - ˙ x = v - ˙ x U - ˙ y = v - ˙ y U - ˙ z = v - ˙ z ¬ z x I y x z I y y x I z
32 31 notbid u = U ¬ u v x P y P z P u - ˙ x = v - ˙ x u - ˙ y = v - ˙ y u - ˙ z = v - ˙ z ¬ z x I y x z I y y x I z ¬ U v x P y P z P U - ˙ x = v - ˙ x U - ˙ y = v - ˙ y U - ˙ z = v - ˙ z ¬ z x I y x z I y y 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 x I y x z I y y x I z U - ˙ x = V - ˙ x U - ˙ y = V - ˙ y U - ˙ z = V - ˙ z ¬ z x I y x z I y y x I z
42 41 rexbidv v = V z P U - ˙ x = v - ˙ x U - ˙ y = v - ˙ y U - ˙ z = v - ˙ z ¬ z x I y x z I y y x I z z P U - ˙ x = V - ˙ x U - ˙ y = V - ˙ y U - ˙ z = V - ˙ z ¬ z x I y x z I y y x I z
43 42 2rexbidv v = V x P y P z P U - ˙ x = v - ˙ x U - ˙ y = v - ˙ y U - ˙ z = v - ˙ z ¬ z x I y x z I y y x I z x P y P z P U - ˙ x = V - ˙ x U - ˙ y = V - ˙ y U - ˙ z = V - ˙ z ¬ z x I y x z I y y x I z
44 33 43 anbi12d v = V U v x P y P z P U - ˙ x = v - ˙ x U - ˙ y = v - ˙ y U - ˙ z = v - ˙ z ¬ z x I y x z I y y x I z U V x P y P z P U - ˙ x = V - ˙ x U - ˙ y = V - ˙ y U - ˙ z = V - ˙ z ¬ z x I y x z I y y x I z
45 44 notbid v = V ¬ U v x P y P z P U - ˙ x = v - ˙ x U - ˙ y = v - ˙ y U - ˙ z = v - ˙ z ¬ z x I y x z I y y x I z ¬ U V x P y P z P U - ˙ x = V - ˙ x U - ˙ y = V - ˙ y U - ˙ z = V - ˙ z ¬ z x I y x z I y y x I z
46 32 45 rspc2v U P V P u P v P ¬ u v x P y P z P u - ˙ x = v - ˙ x u - ˙ y = v - ˙ y u - ˙ z = v - ˙ z ¬ z x I y x z I y y x I z ¬ U V x P y P z P U - ˙ x = V - ˙ x U - ˙ y = V - ˙ y U - ˙ z = V - ˙ z ¬ z x I y x z I y y x I z
47 7 8 46 syl2anc φ u P v P ¬ u v x P y P z P u - ˙ x = v - ˙ x u - ˙ y = v - ˙ y u - ˙ z = v - ˙ z ¬ z x I y x z I y y x I z ¬ U V x P y P z P U - ˙ x = V - ˙ x U - ˙ y = V - ˙ y U - ˙ z = V - ˙ z ¬ z x I y x z I y y x I z
48 19 47 mpd φ ¬ U V x P y P z P U - ˙ x = V - ˙ x U - ˙ y = V - ˙ y U - ˙ z = V - ˙ z ¬ z x I y x z I y y x I z
49 imnan U V ¬ x P y P z P U - ˙ x = V - ˙ x U - ˙ y = V - ˙ y U - ˙ z = V - ˙ z ¬ z x I y x z I y y x I z ¬ U V x P y P z P U - ˙ x = V - ˙ x U - ˙ y = V - ˙ y U - ˙ z = V - ˙ z ¬ z x I y x z I y y x I z
50 48 49 sylibr φ U V ¬ x P y P z P U - ˙ x = V - ˙ x U - ˙ y = V - ˙ y U - ˙ z = V - ˙ z ¬ z x I y x z I y y x I z
51 9 50 mpd φ ¬ x P y P z P U - ˙ x = V - ˙ x U - ˙ y = V - ˙ y U - ˙ z = V - ˙ z ¬ z x I y x z I y y x I z
52 ralnex3 x P y P z P ¬ U - ˙ x = V - ˙ x U - ˙ y = V - ˙ y U - ˙ z = V - ˙ z ¬ z x I y x z I y y x I z ¬ x P y P z P U - ˙ x = V - ˙ x U - ˙ y = V - ˙ y U - ˙ z = V - ˙ z ¬ z x I y x z I y y x I z
53 51 52 sylibr φ x P y P z P ¬ U - ˙ x = V - ˙ x U - ˙ y = V - ˙ y U - ˙ z = V - ˙ z ¬ z x I y x z I y y 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 x I y z X I y
60 eleq1 x = X x z I y X z I y
61 oveq1 x = X x I z = X I z
62 61 eleq2d x = X y x I z y X I z
63 59 60 62 3orbi123d x = X z x I y x z I y y x I z z X I y X z I y y X I z
64 63 notbid x = X ¬ z x I y x z I y y x I z ¬ z X I y X z I y y X I z
65 57 64 anbi12d x = X U - ˙ x = V - ˙ x U - ˙ y = V - ˙ y U - ˙ z = V - ˙ z ¬ z x I y x z I y y x I z U - ˙ X = V - ˙ X U - ˙ y = V - ˙ y U - ˙ z = V - ˙ z ¬ z X I y X z I y y X I z
66 65 notbid x = X ¬ U - ˙ x = V - ˙ x U - ˙ y = V - ˙ y U - ˙ z = V - ˙ z ¬ z x I y x z I y y x I z ¬ U - ˙ X = V - ˙ X U - ˙ y = V - ˙ y U - ˙ z = V - ˙ z ¬ z X I y X z I y y 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 X I y z X I Y
73 oveq2 y = Y z I y = z I Y
74 73 eleq2d y = Y X z I y X z I Y
75 eleq1 y = Y y X I z Y X I z
76 72 74 75 3orbi123d y = Y z X I y X z I y y X I z z X I Y X z I Y Y X I z
77 76 notbid y = Y ¬ z X I y X z I y y X I z ¬ z X I Y X z I Y Y X I z
78 70 77 anbi12d y = Y U - ˙ X = V - ˙ X U - ˙ y = V - ˙ y U - ˙ z = V - ˙ z ¬ z X I y X z I y y X I z U - ˙ X = V - ˙ X U - ˙ Y = V - ˙ Y U - ˙ z = V - ˙ z ¬ z X I Y X z I Y Y X I z
79 78 notbid y = Y ¬ U - ˙ X = V - ˙ X U - ˙ y = V - ˙ y U - ˙ z = V - ˙ z ¬ z X I y X z I y y X I z ¬ U - ˙ X = V - ˙ X U - ˙ Y = V - ˙ Y U - ˙ z = V - ˙ z ¬ z X I Y X z I Y Y 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 X I Y Z X I Y
85 oveq1 z = Z z I Y = Z I Y
86 85 eleq2d z = Z X z I Y X Z I Y
87 oveq2 z = Z X I z = X I Z
88 87 eleq2d z = Z Y X I z Y X I Z
89 84 86 88 3orbi123d z = Z z X I Y X z I Y Y X I z Z X I Y X Z I Y Y X I Z
90 89 notbid z = Z ¬ z X I Y X z I Y Y X I z ¬ Z X I Y X Z I Y Y X I Z
91 83 90 anbi12d z = Z U - ˙ X = V - ˙ X U - ˙ Y = V - ˙ Y U - ˙ z = V - ˙ z ¬ z X I Y X z I Y Y X I z U - ˙ X = V - ˙ X U - ˙ Y = V - ˙ Y U - ˙ Z = V - ˙ Z ¬ Z X I Y X Z I Y Y X I Z
92 91 notbid z = Z ¬ U - ˙ X = V - ˙ X U - ˙ Y = V - ˙ Y U - ˙ z = V - ˙ z ¬ z X I Y X z I Y Y X I z ¬ U - ˙ X = V - ˙ X U - ˙ Y = V - ˙ Y U - ˙ Z = V - ˙ Z ¬ Z X I Y X Z I Y Y X I Z
93 66 79 92 rspc3v X P Y P Z P x P y P z P ¬ U - ˙ x = V - ˙ x U - ˙ y = V - ˙ y U - ˙ z = V - ˙ z ¬ z x I y x z I y y x I z ¬ U - ˙ X = V - ˙ X U - ˙ Y = V - ˙ Y U - ˙ Z = V - ˙ Z ¬ Z X I Y X Z I Y Y X I Z
94 4 5 6 93 syl3anc φ x P y P z P ¬ U - ˙ x = V - ˙ x U - ˙ y = V - ˙ y U - ˙ z = V - ˙ z ¬ z x I y x z I y y x I z ¬ U - ˙ X = V - ˙ X U - ˙ Y = V - ˙ Y U - ˙ Z = V - ˙ Z ¬ Z X I Y X Z I Y Y X I Z
95 53 94 mpd φ ¬ U - ˙ X = V - ˙ X U - ˙ Y = V - ˙ Y U - ˙ Z = V - ˙ Z ¬ Z X I Y X Z I Y Y X I Z
96 imnan U - ˙ X = V - ˙ X U - ˙ Y = V - ˙ Y U - ˙ Z = V - ˙ Z ¬ ¬ Z X I Y X Z I Y Y X I Z ¬ U - ˙ X = V - ˙ X U - ˙ Y = V - ˙ Y U - ˙ Z = V - ˙ Z ¬ Z X I Y X Z I Y Y X I Z
97 95 96 sylibr φ U - ˙ X = V - ˙ X U - ˙ Y = V - ˙ Y U - ˙ Z = V - ˙ Z ¬ ¬ Z X I Y X Z I Y Y X I Z
98 10 11 12 97 mp3and φ ¬ ¬ Z X I Y X Z I Y Y X I Z
99 98 notnotrd φ Z X I Y X Z I Y Y X I Z