Metamath Proof Explorer

Theorem axtgupdim2ALTV

Description: Alternate version of axtgupdim2 . (Contributed by Thierry Arnoux, 29-May-2019) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 istrkg2d.p 
 |-  P = ( Base ` G )
2 istrkg2d.d 
 |-  .- = ( dist ` G )
3 istrkg2d.i 
 |-  I = ( Itv ` G )
4 axtgupdim2ALTV.x 
 |-  ( ph -> X e. P )
5 axtgupdim2ALTV.y 
 |-  ( ph -> Y e. P )
6 axtgupdim2ALTV.z 
 |-  ( ph -> Z e. P )
7 axtgupdim2ALTV.u 
 |-  ( ph -> U e. P )
8 axtgupdim2ALTV.v 
 |-  ( ph -> V e. P )
9 axtgupdim2ALTV.0 
 |-  ( ph -> U =/= V )
10 axtgupdim2ALTV.1 
 |-  ( ph -> ( X .- U ) = ( X .- V ) )
11 axtgupdim2ALTV.2 
 |-  ( ph -> ( Y .- U ) = ( Y .- V ) )
12 axtgupdim2ALTV.3 
 |-  ( ph -> ( Z .- U ) = ( Z .- V ) )
13 axtgupdim2ALTV.g 
 |-  ( ph -> G e. TarskiG2D )
14 10 11 12 3jca 
 |-  ( ph -> ( ( X .- U ) = ( X .- V ) /\ ( Y .- U ) = ( Y .- V ) /\ ( Z .- U ) = ( Z .- V ) ) )
15 1 2 3 istrkg2d 
 |-  ( G e. TarskiG2D <-> ( G e. _V /\ ( E. x e. P E. y e. P E. z e. P -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) /\ A. x e. P A. y e. P A. z e. P A. u e. P A. v e. P ( ( ( ( x .- u ) = ( x .- v ) /\ ( y .- u ) = ( y .- v ) /\ ( z .- u ) = ( z .- v ) ) /\ u =/= v ) -> ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) ) )
16 13 15 sylib 
 |-  ( ph -> ( G e. _V /\ ( E. x e. P E. y e. P E. z e. P -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) /\ A. x e. P A. y e. P A. z e. P A. u e. P A. v e. P ( ( ( ( x .- u ) = ( x .- v ) /\ ( y .- u ) = ( y .- v ) /\ ( z .- u ) = ( z .- v ) ) /\ u =/= v ) -> ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) ) )
17 16 simprrd 
 |-  ( ph -> A. x e. P A. y e. P A. z e. P A. u e. P A. v e. P ( ( ( ( x .- u ) = ( x .- v ) /\ ( y .- u ) = ( y .- v ) /\ ( z .- u ) = ( z .- v ) ) /\ u =/= v ) -> ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) )
18 oveq1 
 |-  ( x = X -> ( x .- u ) = ( X .- u ) )
19 oveq1 
 |-  ( x = X -> ( x .- v ) = ( X .- v ) )
20 18 19 eqeq12d 
 |-  ( x = X -> ( ( x .- u ) = ( x .- v ) <-> ( X .- u ) = ( X .- v ) ) )
21 20 3anbi1d 
 |-  ( x = X -> ( ( ( x .- u ) = ( x .- v ) /\ ( y .- u ) = ( y .- v ) /\ ( z .- u ) = ( z .- v ) ) <-> ( ( X .- u ) = ( X .- v ) /\ ( y .- u ) = ( y .- v ) /\ ( z .- u ) = ( z .- v ) ) ) )
22 21 anbi1d 
 |-  ( x = X -> ( ( ( ( x .- u ) = ( x .- v ) /\ ( y .- u ) = ( y .- v ) /\ ( z .- u ) = ( z .- v ) ) /\ u =/= v ) <-> ( ( ( X .- u ) = ( X .- v ) /\ ( y .- u ) = ( y .- v ) /\ ( z .- u ) = ( z .- v ) ) /\ u =/= v ) ) )
23 oveq1 
 |-  ( x = X -> ( x I y ) = ( X I y ) )
24 23 eleq2d 
 |-  ( x = X -> ( z e. ( x I y ) <-> z e. ( X I y ) ) )
25 eleq1 
 |-  ( x = X -> ( x e. ( z I y ) <-> X e. ( z I y ) ) )
26 oveq1 
 |-  ( x = X -> ( x I z ) = ( X I z ) )
27 26 eleq2d 
 |-  ( x = X -> ( y e. ( x I z ) <-> y e. ( X I z ) ) )
28 24 25 27 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 ) ) ) )
29 22 28 imbi12d 
 |-  ( x = X -> ( ( ( ( ( x .- u ) = ( x .- v ) /\ ( y .- u ) = ( y .- v ) /\ ( z .- u ) = ( z .- v ) ) /\ u =/= v ) -> ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) <-> ( ( ( ( X .- u ) = ( X .- v ) /\ ( y .- u ) = ( y .- v ) /\ ( z .- u ) = ( z .- v ) ) /\ u =/= v ) -> ( z e. ( X I y ) \/ X e. ( z I y ) \/ y e. ( X I z ) ) ) ) )
30 29 2ralbidv 
 |-  ( x = X -> ( A. u e. P A. v e. P ( ( ( ( x .- u ) = ( x .- v ) /\ ( y .- u ) = ( y .- v ) /\ ( z .- u ) = ( z .- v ) ) /\ u =/= v ) -> ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) <-> A. u e. P A. v e. P ( ( ( ( X .- u ) = ( X .- v ) /\ ( y .- u ) = ( y .- v ) /\ ( z .- u ) = ( z .- v ) ) /\ u =/= v ) -> ( z e. ( X I y ) \/ X e. ( z I y ) \/ y e. ( X I z ) ) ) ) )
31 oveq1 
 |-  ( y = Y -> ( y .- u ) = ( Y .- u ) )
32 oveq1 
 |-  ( y = Y -> ( y .- v ) = ( Y .- v ) )
33 31 32 eqeq12d 
 |-  ( y = Y -> ( ( y .- u ) = ( y .- v ) <-> ( Y .- u ) = ( Y .- v ) ) )
34 33 3anbi2d 
 |-  ( y = Y -> ( ( ( X .- u ) = ( X .- v ) /\ ( y .- u ) = ( y .- v ) /\ ( z .- u ) = ( z .- v ) ) <-> ( ( X .- u ) = ( X .- v ) /\ ( Y .- u ) = ( Y .- v ) /\ ( z .- u ) = ( z .- v ) ) ) )
35 34 anbi1d 
 |-  ( y = Y -> ( ( ( ( X .- u ) = ( X .- v ) /\ ( y .- u ) = ( y .- v ) /\ ( z .- u ) = ( z .- v ) ) /\ u =/= v ) <-> ( ( ( X .- u ) = ( X .- v ) /\ ( Y .- u ) = ( Y .- v ) /\ ( z .- u ) = ( z .- v ) ) /\ u =/= v ) ) )
36 oveq2 
 |-  ( y = Y -> ( X I y ) = ( X I Y ) )
37 36 eleq2d 
 |-  ( y = Y -> ( z e. ( X I y ) <-> z e. ( X I Y ) ) )
38 oveq2 
 |-  ( y = Y -> ( z I y ) = ( z I Y ) )
39 38 eleq2d 
 |-  ( y = Y -> ( X e. ( z I y ) <-> X e. ( z I Y ) ) )
40 eleq1 
 |-  ( y = Y -> ( y e. ( X I z ) <-> Y e. ( X I z ) ) )
41 37 39 40 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 ) ) ) )
42 35 41 imbi12d 
 |-  ( y = Y -> ( ( ( ( ( X .- u ) = ( X .- v ) /\ ( y .- u ) = ( y .- v ) /\ ( z .- u ) = ( z .- v ) ) /\ u =/= v ) -> ( z e. ( X I y ) \/ X e. ( z I y ) \/ y e. ( X I z ) ) ) <-> ( ( ( ( X .- u ) = ( X .- v ) /\ ( Y .- u ) = ( Y .- v ) /\ ( z .- u ) = ( z .- v ) ) /\ u =/= v ) -> ( z e. ( X I Y ) \/ X e. ( z I Y ) \/ Y e. ( X I z ) ) ) ) )
43 42 2ralbidv 
 |-  ( y = Y -> ( A. u e. P A. v e. P ( ( ( ( X .- u ) = ( X .- v ) /\ ( y .- u ) = ( y .- v ) /\ ( z .- u ) = ( z .- v ) ) /\ u =/= v ) -> ( z e. ( X I y ) \/ X e. ( z I y ) \/ y e. ( X I z ) ) ) <-> A. u e. P A. v e. P ( ( ( ( X .- u ) = ( X .- v ) /\ ( Y .- u ) = ( Y .- v ) /\ ( z .- u ) = ( z .- v ) ) /\ u =/= v ) -> ( z e. ( X I Y ) \/ X e. ( z I Y ) \/ Y e. ( X I z ) ) ) ) )
44 oveq1 
 |-  ( z = Z -> ( z .- u ) = ( Z .- u ) )
45 oveq1 
 |-  ( z = Z -> ( z .- v ) = ( Z .- v ) )
46 44 45 eqeq12d 
 |-  ( z = Z -> ( ( z .- u ) = ( z .- v ) <-> ( Z .- u ) = ( Z .- v ) ) )
47 46 3anbi3d 
 |-  ( z = Z -> ( ( ( X .- u ) = ( X .- v ) /\ ( Y .- u ) = ( Y .- v ) /\ ( z .- u ) = ( z .- v ) ) <-> ( ( X .- u ) = ( X .- v ) /\ ( Y .- u ) = ( Y .- v ) /\ ( Z .- u ) = ( Z .- v ) ) ) )
48 47 anbi1d 
 |-  ( z = Z -> ( ( ( ( X .- u ) = ( X .- v ) /\ ( Y .- u ) = ( Y .- v ) /\ ( z .- u ) = ( z .- v ) ) /\ u =/= v ) <-> ( ( ( X .- u ) = ( X .- v ) /\ ( Y .- u ) = ( Y .- v ) /\ ( Z .- u ) = ( Z .- v ) ) /\ u =/= v ) ) )
49 eleq1 
 |-  ( z = Z -> ( z e. ( X I Y ) <-> Z e. ( X I Y ) ) )
50 oveq1 
 |-  ( z = Z -> ( z I Y ) = ( Z I Y ) )
51 50 eleq2d 
 |-  ( z = Z -> ( X e. ( z I Y ) <-> X e. ( Z I Y ) ) )
52 oveq2 
 |-  ( z = Z -> ( X I z ) = ( X I Z ) )
53 52 eleq2d 
 |-  ( z = Z -> ( Y e. ( X I z ) <-> Y e. ( X I Z ) ) )
54 49 51 53 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 ) ) ) )
55 48 54 imbi12d 
 |-  ( z = Z -> ( ( ( ( ( X .- u ) = ( X .- v ) /\ ( Y .- u ) = ( Y .- v ) /\ ( z .- u ) = ( z .- v ) ) /\ u =/= v ) -> ( z e. ( X I Y ) \/ X e. ( z I Y ) \/ Y e. ( X I z ) ) ) <-> ( ( ( ( X .- u ) = ( X .- v ) /\ ( Y .- u ) = ( Y .- v ) /\ ( Z .- u ) = ( Z .- v ) ) /\ u =/= v ) -> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) ) )
56 55 2ralbidv 
 |-  ( z = Z -> ( A. u e. P A. v e. P ( ( ( ( X .- u ) = ( X .- v ) /\ ( Y .- u ) = ( Y .- v ) /\ ( z .- u ) = ( z .- v ) ) /\ u =/= v ) -> ( z e. ( X I Y ) \/ X e. ( z I Y ) \/ Y e. ( X I z ) ) ) <-> A. u e. P A. v e. P ( ( ( ( X .- u ) = ( X .- v ) /\ ( Y .- u ) = ( Y .- v ) /\ ( Z .- u ) = ( Z .- v ) ) /\ u =/= v ) -> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) ) )
57 30 43 56 rspc3v 
 |-  ( ( X e. P /\ Y e. P /\ Z e. P ) -> ( A. x e. P A. y e. P A. z e. P A. u e. P A. v e. P ( ( ( ( x .- u ) = ( x .- v ) /\ ( y .- u ) = ( y .- v ) /\ ( z .- u ) = ( z .- v ) ) /\ u =/= v ) -> ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) -> A. u e. P A. v e. P ( ( ( ( X .- u ) = ( X .- v ) /\ ( Y .- u ) = ( Y .- v ) /\ ( Z .- u ) = ( Z .- v ) ) /\ u =/= v ) -> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) ) )
58 4 5 6 57 syl3anc 
 |-  ( ph -> ( A. x e. P A. y e. P A. z e. P A. u e. P A. v e. P ( ( ( ( x .- u ) = ( x .- v ) /\ ( y .- u ) = ( y .- v ) /\ ( z .- u ) = ( z .- v ) ) /\ u =/= v ) -> ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) -> A. u e. P A. v e. P ( ( ( ( X .- u ) = ( X .- v ) /\ ( Y .- u ) = ( Y .- v ) /\ ( Z .- u ) = ( Z .- v ) ) /\ u =/= v ) -> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) ) )
59 17 58 mpd 
 |-  ( ph -> A. u e. P A. v e. P ( ( ( ( X .- u ) = ( X .- v ) /\ ( Y .- u ) = ( Y .- v ) /\ ( Z .- u ) = ( Z .- v ) ) /\ u =/= v ) -> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) )
60 oveq2 
 |-  ( u = U -> ( X .- u ) = ( X .- U ) )
61 60 eqeq1d 
 |-  ( u = U -> ( ( X .- u ) = ( X .- v ) <-> ( X .- U ) = ( X .- v ) ) )
62 oveq2 
 |-  ( u = U -> ( Y .- u ) = ( Y .- U ) )
63 62 eqeq1d 
 |-  ( u = U -> ( ( Y .- u ) = ( Y .- v ) <-> ( Y .- U ) = ( Y .- v ) ) )
64 oveq2 
 |-  ( u = U -> ( Z .- u ) = ( Z .- U ) )
65 64 eqeq1d 
 |-  ( u = U -> ( ( Z .- u ) = ( Z .- v ) <-> ( Z .- U ) = ( Z .- v ) ) )
66 61 63 65 3anbi123d 
 |-  ( u = U -> ( ( ( X .- u ) = ( X .- v ) /\ ( Y .- u ) = ( Y .- v ) /\ ( Z .- u ) = ( Z .- v ) ) <-> ( ( X .- U ) = ( X .- v ) /\ ( Y .- U ) = ( Y .- v ) /\ ( Z .- U ) = ( Z .- v ) ) ) )
67 neeq1 
 |-  ( u = U -> ( u =/= v <-> U =/= v ) )
68 66 67 anbi12d 
 |-  ( u = U -> ( ( ( ( X .- u ) = ( X .- v ) /\ ( Y .- u ) = ( Y .- v ) /\ ( Z .- u ) = ( Z .- v ) ) /\ u =/= v ) <-> ( ( ( X .- U ) = ( X .- v ) /\ ( Y .- U ) = ( Y .- v ) /\ ( Z .- U ) = ( Z .- v ) ) /\ U =/= v ) ) )
69 68 imbi1d 
 |-  ( u = U -> ( ( ( ( ( X .- u ) = ( X .- v ) /\ ( Y .- u ) = ( Y .- v ) /\ ( Z .- u ) = ( Z .- v ) ) /\ u =/= v ) -> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) <-> ( ( ( ( X .- U ) = ( X .- v ) /\ ( Y .- U ) = ( Y .- v ) /\ ( Z .- U ) = ( Z .- v ) ) /\ U =/= v ) -> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) ) )
70 oveq2 
 |-  ( v = V -> ( X .- v ) = ( X .- V ) )
71 70 eqeq2d 
 |-  ( v = V -> ( ( X .- U ) = ( X .- v ) <-> ( X .- U ) = ( X .- V ) ) )
72 oveq2 
 |-  ( v = V -> ( Y .- v ) = ( Y .- V ) )
73 72 eqeq2d 
 |-  ( v = V -> ( ( Y .- U ) = ( Y .- v ) <-> ( Y .- U ) = ( Y .- V ) ) )
74 oveq2 
 |-  ( v = V -> ( Z .- v ) = ( Z .- V ) )
75 74 eqeq2d 
 |-  ( v = V -> ( ( Z .- U ) = ( Z .- v ) <-> ( Z .- U ) = ( Z .- V ) ) )
76 71 73 75 3anbi123d 
 |-  ( v = V -> ( ( ( X .- U ) = ( X .- v ) /\ ( Y .- U ) = ( Y .- v ) /\ ( Z .- U ) = ( Z .- v ) ) <-> ( ( X .- U ) = ( X .- V ) /\ ( Y .- U ) = ( Y .- V ) /\ ( Z .- U ) = ( Z .- V ) ) ) )
77 neeq2 
 |-  ( v = V -> ( U =/= v <-> U =/= V ) )
78 76 77 anbi12d 
 |-  ( v = V -> ( ( ( ( X .- U ) = ( X .- v ) /\ ( Y .- U ) = ( Y .- v ) /\ ( Z .- U ) = ( Z .- v ) ) /\ U =/= v ) <-> ( ( ( X .- U ) = ( X .- V ) /\ ( Y .- U ) = ( Y .- V ) /\ ( Z .- U ) = ( Z .- V ) ) /\ U =/= V ) ) )
79 78 imbi1d 
 |-  ( v = V -> ( ( ( ( ( X .- U ) = ( X .- v ) /\ ( Y .- U ) = ( Y .- v ) /\ ( Z .- U ) = ( Z .- v ) ) /\ U =/= v ) -> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) <-> ( ( ( ( X .- U ) = ( X .- V ) /\ ( Y .- U ) = ( Y .- V ) /\ ( Z .- U ) = ( Z .- V ) ) /\ U =/= V ) -> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) ) )
80 69 79 rspc2v 
 |-  ( ( U e. P /\ V e. P ) -> ( A. u e. P A. v e. P ( ( ( ( X .- u ) = ( X .- v ) /\ ( Y .- u ) = ( Y .- v ) /\ ( Z .- u ) = ( Z .- v ) ) /\ u =/= v ) -> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) -> ( ( ( ( X .- U ) = ( X .- V ) /\ ( Y .- U ) = ( Y .- V ) /\ ( Z .- U ) = ( Z .- V ) ) /\ U =/= V ) -> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) ) )
81 7 8 80 syl2anc 
 |-  ( ph -> ( A. u e. P A. v e. P ( ( ( ( X .- u ) = ( X .- v ) /\ ( Y .- u ) = ( Y .- v ) /\ ( Z .- u ) = ( Z .- v ) ) /\ u =/= v ) -> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) -> ( ( ( ( X .- U ) = ( X .- V ) /\ ( Y .- U ) = ( Y .- V ) /\ ( Z .- U ) = ( Z .- V ) ) /\ U =/= V ) -> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) ) )
82 59 81 mpd 
 |-  ( ph -> ( ( ( ( X .- U ) = ( X .- V ) /\ ( Y .- U ) = ( Y .- V ) /\ ( Z .- U ) = ( Z .- V ) ) /\ U =/= V ) -> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) )
83 14 9 82 mp2and 
 |-  ( ph -> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) )