Metamath Proof Explorer

Theorem istrkg3ld

Description: Property of fulfilling the lower dimension 3 axiom. (Contributed by Thierry Arnoux, 12-Jul-2020)

Ref Expression
Hypotheses istrkg.p 
|- P = ( Base ` G )
istrkg.d 
|- .- = ( dist ` G )
istrkg.i 
|- I = ( Itv ` G )
Assertion 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 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 istrkg.p 
 |-  P = ( Base ` G )
2 istrkg.d 
 |-  .- = ( dist ` G )
3 istrkg.i 
 |-  I = ( Itv ` G )
4 3z 
 |-  3 e. ZZ
5 2re 
 |-  2 e. RR
6 3re 
 |-  3 e. RR
7 2lt3 
 |-  2 < 3
8 5 6 7 ltleii 
 |-  2 <_ 3
9 2z 
 |-  2 e. ZZ
10 9 eluz1i 
 |-  ( 3 e. ( ZZ>= ` 2 ) <-> ( 3 e. ZZ /\ 2 <_ 3 ) )
11 4 8 10 mpbir2an 
 |-  3 e. ( ZZ>= ` 2 )
12 1 2 3 istrkgld 
 |-  ( ( G e. V /\ 3 e. ( ZZ>= ` 2 ) ) -> ( G TarskiGDim>= 3 <-> E. f ( f : ( 1 ..^ 3 ) -1-1-> P /\ E. x e. P E. y e. P E. z e. P ( A. j e. ( 2 ..^ 3 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) ) )
13 11 12 mpan2 
 |-  ( G e. V -> ( G TarskiGDim>= 3 <-> E. f ( f : ( 1 ..^ 3 ) -1-1-> P /\ E. x e. P E. y e. P E. z e. P ( A. j e. ( 2 ..^ 3 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) ) )
14 fzo13pr 
 |-  ( 1 ..^ 3 ) = { 1 , 2 }
15 f1eq2 
 |-  ( ( 1 ..^ 3 ) = { 1 , 2 } -> ( f : ( 1 ..^ 3 ) -1-1-> P <-> f : { 1 , 2 } -1-1-> P ) )
16 14 15 ax-mp 
 |-  ( f : ( 1 ..^ 3 ) -1-1-> P <-> f : { 1 , 2 } -1-1-> P )
17 16 anbi1i 
 |-  ( ( f : ( 1 ..^ 3 ) -1-1-> P /\ E. x e. P E. y e. P E. z e. P ( A. j e. ( 2 ..^ 3 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) <-> ( f : { 1 , 2 } -1-1-> P /\ E. x e. P E. y e. P E. z e. P ( A. j e. ( 2 ..^ 3 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) )
18 17 exbii 
 |-  ( E. f ( f : ( 1 ..^ 3 ) -1-1-> P /\ E. x e. P E. y e. P E. z e. P ( A. j e. ( 2 ..^ 3 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) <-> E. f ( f : { 1 , 2 } -1-1-> P /\ E. x e. P E. y e. P E. z e. P ( A. j e. ( 2 ..^ 3 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) )
19 18 a1i 
 |-  ( G e. V -> ( E. f ( f : ( 1 ..^ 3 ) -1-1-> P /\ E. x e. P E. y e. P E. z e. P ( A. j e. ( 2 ..^ 3 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) <-> E. f ( f : { 1 , 2 } -1-1-> P /\ E. x e. P E. y e. P E. z e. P ( A. j e. ( 2 ..^ 3 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) ) )
20 1z 
 |-  1 e. ZZ
21 1ne2 
 |-  1 =/= 2
22 oveq1 
 |-  ( u = ( f ` 1 ) -> ( u .- x ) = ( ( f ` 1 ) .- x ) )
23 22 eqeq1d 
 |-  ( u = ( f ` 1 ) -> ( ( u .- x ) = ( v .- x ) <-> ( ( f ` 1 ) .- x ) = ( v .- x ) ) )
24 oveq1 
 |-  ( u = ( f ` 1 ) -> ( u .- y ) = ( ( f ` 1 ) .- y ) )
25 24 eqeq1d 
 |-  ( u = ( f ` 1 ) -> ( ( u .- y ) = ( v .- y ) <-> ( ( f ` 1 ) .- y ) = ( v .- y ) ) )
26 oveq1 
 |-  ( u = ( f ` 1 ) -> ( u .- z ) = ( ( f ` 1 ) .- z ) )
27 26 eqeq1d 
 |-  ( u = ( f ` 1 ) -> ( ( u .- z ) = ( v .- z ) <-> ( ( f ` 1 ) .- z ) = ( v .- z ) ) )
28 23 25 27 3anbi123d 
 |-  ( u = ( f ` 1 ) -> ( ( ( u .- x ) = ( v .- x ) /\ ( u .- y ) = ( v .- y ) /\ ( u .- z ) = ( v .- z ) ) <-> ( ( ( f ` 1 ) .- x ) = ( v .- x ) /\ ( ( f ` 1 ) .- y ) = ( v .- y ) /\ ( ( f ` 1 ) .- z ) = ( v .- z ) ) ) )
29 28 anbi1d 
 |-  ( u = ( f ` 1 ) -> ( ( ( ( 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 ) ) ) <-> ( ( ( ( f ` 1 ) .- x ) = ( v .- x ) /\ ( ( f ` 1 ) .- y ) = ( v .- y ) /\ ( ( f ` 1 ) .- z ) = ( v .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) )
30 29 rexbidv 
 |-  ( u = ( f ` 1 ) -> ( 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 ( ( ( ( f ` 1 ) .- x ) = ( v .- x ) /\ ( ( f ` 1 ) .- y ) = ( v .- y ) /\ ( ( f ` 1 ) .- z ) = ( v .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) )
31 30 2rexbidv 
 |-  ( u = ( f ` 1 ) -> ( 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 ( ( ( ( f ` 1 ) .- x ) = ( v .- x ) /\ ( ( f ` 1 ) .- y ) = ( v .- y ) /\ ( ( f ` 1 ) .- z ) = ( v .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) )
32 oveq1 
 |-  ( v = ( f ` 2 ) -> ( v .- x ) = ( ( f ` 2 ) .- x ) )
33 32 eqeq2d 
 |-  ( v = ( f ` 2 ) -> ( ( ( f ` 1 ) .- x ) = ( v .- x ) <-> ( ( f ` 1 ) .- x ) = ( ( f ` 2 ) .- x ) ) )
34 oveq1 
 |-  ( v = ( f ` 2 ) -> ( v .- y ) = ( ( f ` 2 ) .- y ) )
35 34 eqeq2d 
 |-  ( v = ( f ` 2 ) -> ( ( ( f ` 1 ) .- y ) = ( v .- y ) <-> ( ( f ` 1 ) .- y ) = ( ( f ` 2 ) .- y ) ) )
36 oveq1 
 |-  ( v = ( f ` 2 ) -> ( v .- z ) = ( ( f ` 2 ) .- z ) )
37 36 eqeq2d 
 |-  ( v = ( f ` 2 ) -> ( ( ( f ` 1 ) .- z ) = ( v .- z ) <-> ( ( f ` 1 ) .- z ) = ( ( f ` 2 ) .- z ) ) )
38 33 35 37 3anbi123d 
 |-  ( v = ( f ` 2 ) -> ( ( ( ( f ` 1 ) .- x ) = ( v .- x ) /\ ( ( f ` 1 ) .- y ) = ( v .- y ) /\ ( ( f ` 1 ) .- z ) = ( v .- z ) ) <-> ( ( ( f ` 1 ) .- x ) = ( ( f ` 2 ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` 2 ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` 2 ) .- z ) ) ) )
39 2p1e3 
 |-  ( 2 + 1 ) = 3
40 39 oveq2i 
 |-  ( 2 ..^ ( 2 + 1 ) ) = ( 2 ..^ 3 )
41 fzosn 
 |-  ( 2 e. ZZ -> ( 2 ..^ ( 2 + 1 ) ) = { 2 } )
42 9 41 ax-mp 
 |-  ( 2 ..^ ( 2 + 1 ) ) = { 2 }
43 40 42 eqtr3i 
 |-  ( 2 ..^ 3 ) = { 2 }
44 43 raleqi 
 |-  ( A. j e. ( 2 ..^ 3 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) <-> A. j e. { 2 } ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) )
45 fveq2 
 |-  ( j = 2 -> ( f ` j ) = ( f ` 2 ) )
46 45 oveq1d 
 |-  ( j = 2 -> ( ( f ` j ) .- x ) = ( ( f ` 2 ) .- x ) )
47 46 eqeq2d 
 |-  ( j = 2 -> ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) <-> ( ( f ` 1 ) .- x ) = ( ( f ` 2 ) .- x ) ) )
48 45 oveq1d 
 |-  ( j = 2 -> ( ( f ` j ) .- y ) = ( ( f ` 2 ) .- y ) )
49 48 eqeq2d 
 |-  ( j = 2 -> ( ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) <-> ( ( f ` 1 ) .- y ) = ( ( f ` 2 ) .- y ) ) )
50 45 oveq1d 
 |-  ( j = 2 -> ( ( f ` j ) .- z ) = ( ( f ` 2 ) .- z ) )
51 50 eqeq2d 
 |-  ( j = 2 -> ( ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) <-> ( ( f ` 1 ) .- z ) = ( ( f ` 2 ) .- z ) ) )
52 47 49 51 3anbi123d 
 |-  ( j = 2 -> ( ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) <-> ( ( ( f ` 1 ) .- x ) = ( ( f ` 2 ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` 2 ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` 2 ) .- z ) ) ) )
53 52 ralsng 
 |-  ( 2 e. ZZ -> ( A. j e. { 2 } ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) <-> ( ( ( f ` 1 ) .- x ) = ( ( f ` 2 ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` 2 ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` 2 ) .- z ) ) ) )
54 9 53 ax-mp 
 |-  ( A. j e. { 2 } ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) <-> ( ( ( f ` 1 ) .- x ) = ( ( f ` 2 ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` 2 ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` 2 ) .- z ) ) )
55 44 54 bitri 
 |-  ( A. j e. ( 2 ..^ 3 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) <-> ( ( ( f ` 1 ) .- x ) = ( ( f ` 2 ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` 2 ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` 2 ) .- z ) ) )
56 38 55 bitr4di 
 |-  ( v = ( f ` 2 ) -> ( ( ( ( f ` 1 ) .- x ) = ( v .- x ) /\ ( ( f ` 1 ) .- y ) = ( v .- y ) /\ ( ( f ` 1 ) .- z ) = ( v .- z ) ) <-> A. j e. ( 2 ..^ 3 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) ) )
57 56 anbi1d 
 |-  ( v = ( f ` 2 ) -> ( ( ( ( ( f ` 1 ) .- x ) = ( v .- x ) /\ ( ( f ` 1 ) .- y ) = ( v .- y ) /\ ( ( f ` 1 ) .- z ) = ( v .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) <-> ( A. j e. ( 2 ..^ 3 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) )
58 57 rexbidv 
 |-  ( v = ( f ` 2 ) -> ( E. z e. P ( ( ( ( f ` 1 ) .- x ) = ( v .- x ) /\ ( ( f ` 1 ) .- y ) = ( v .- y ) /\ ( ( f ` 1 ) .- z ) = ( v .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) <-> E. z e. P ( A. j e. ( 2 ..^ 3 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) )
59 58 2rexbidv 
 |-  ( v = ( f ` 2 ) -> ( E. x e. P E. y e. P E. z e. P ( ( ( ( f ` 1 ) .- x ) = ( v .- x ) /\ ( ( f ` 1 ) .- y ) = ( v .- y ) /\ ( ( f ` 1 ) .- 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 ( A. j e. ( 2 ..^ 3 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) )
60 31 59 f1prex 
 |-  ( ( 1 e. ZZ /\ 2 e. ZZ /\ 1 =/= 2 ) -> ( E. f ( f : { 1 , 2 } -1-1-> P /\ E. x e. P E. y e. P E. z e. P ( A. j e. ( 2 ..^ 3 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- 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 ) ) ) ) ) )
61 20 9 21 60 mp3an 
 |-  ( E. f ( f : { 1 , 2 } -1-1-> P /\ E. x e. P E. y e. P E. z e. P ( A. j e. ( 2 ..^ 3 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- 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 ) ) ) ) )
62 61 a1i 
 |-  ( G e. V -> ( E. f ( f : { 1 , 2 } -1-1-> P /\ E. x e. P E. y e. P E. z e. P ( A. j e. ( 2 ..^ 3 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- 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 ) ) ) ) ) )
63 13 19 62 3bitrd 
 |-  ( 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 ) ) ) ) ) )