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 2le3 
 |-  2 <_ 3
6 2z 
 |-  2 e. ZZ
7 6 eluz1i 
 |-  ( 3 e. ( ZZ>= ` 2 ) <-> ( 3 e. ZZ /\ 2 <_ 3 ) )
8 4 5 7 mpbir2an 
 |-  3 e. ( ZZ>= ` 2 )
9 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 ) ) ) ) ) )
10 8 9 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 ) ) ) ) ) )
11 fzo13pr 
 |-  ( 1 ..^ 3 ) = { 1 , 2 }
12 f1eq2 
 |-  ( ( 1 ..^ 3 ) = { 1 , 2 } -> ( f : ( 1 ..^ 3 ) -1-1-> P <-> f : { 1 , 2 } -1-1-> P ) )
13 11 12 ax-mp 
 |-  ( f : ( 1 ..^ 3 ) -1-1-> P <-> f : { 1 , 2 } -1-1-> P )
14 13 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 ) ) ) ) )
15 14 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 ) ) ) ) )
16 15 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 ) ) ) ) ) )
17 1z 
 |-  1 e. ZZ
18 1ne2 
 |-  1 =/= 2
19 oveq1 
 |-  ( u = ( f ` 1 ) -> ( u .- x ) = ( ( f ` 1 ) .- x ) )
20 19 eqeq1d 
 |-  ( u = ( f ` 1 ) -> ( ( u .- x ) = ( v .- x ) <-> ( ( f ` 1 ) .- x ) = ( v .- x ) ) )
21 oveq1 
 |-  ( u = ( f ` 1 ) -> ( u .- y ) = ( ( f ` 1 ) .- y ) )
22 21 eqeq1d 
 |-  ( u = ( f ` 1 ) -> ( ( u .- y ) = ( v .- y ) <-> ( ( f ` 1 ) .- y ) = ( v .- y ) ) )
23 oveq1 
 |-  ( u = ( f ` 1 ) -> ( u .- z ) = ( ( f ` 1 ) .- z ) )
24 23 eqeq1d 
 |-  ( u = ( f ` 1 ) -> ( ( u .- z ) = ( v .- z ) <-> ( ( f ` 1 ) .- z ) = ( v .- z ) ) )
25 20 22 24 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 ) ) ) )
26 25 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 ) ) ) ) )
27 26 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 ) ) ) ) )
28 27 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 ) ) ) ) )
29 oveq1 
 |-  ( v = ( f ` 2 ) -> ( v .- x ) = ( ( f ` 2 ) .- x ) )
30 29 eqeq2d 
 |-  ( v = ( f ` 2 ) -> ( ( ( f ` 1 ) .- x ) = ( v .- x ) <-> ( ( f ` 1 ) .- x ) = ( ( f ` 2 ) .- x ) ) )
31 oveq1 
 |-  ( v = ( f ` 2 ) -> ( v .- y ) = ( ( f ` 2 ) .- y ) )
32 31 eqeq2d 
 |-  ( v = ( f ` 2 ) -> ( ( ( f ` 1 ) .- y ) = ( v .- y ) <-> ( ( f ` 1 ) .- y ) = ( ( f ` 2 ) .- y ) ) )
33 oveq1 
 |-  ( v = ( f ` 2 ) -> ( v .- z ) = ( ( f ` 2 ) .- z ) )
34 33 eqeq2d 
 |-  ( v = ( f ` 2 ) -> ( ( ( f ` 1 ) .- z ) = ( v .- z ) <-> ( ( f ` 1 ) .- z ) = ( ( f ` 2 ) .- z ) ) )
35 30 32 34 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 ) ) ) )
36 2p1e3 
 |-  ( 2 + 1 ) = 3
37 36 oveq2i 
 |-  ( 2 ..^ ( 2 + 1 ) ) = ( 2 ..^ 3 )
38 fzosn 
 |-  ( 2 e. ZZ -> ( 2 ..^ ( 2 + 1 ) ) = { 2 } )
39 6 38 ax-mp 
 |-  ( 2 ..^ ( 2 + 1 ) ) = { 2 }
40 37 39 eqtr3i 
 |-  ( 2 ..^ 3 ) = { 2 }
41 40 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 ) ) )
42 fveq2 
 |-  ( j = 2 -> ( f ` j ) = ( f ` 2 ) )
43 42 oveq1d 
 |-  ( j = 2 -> ( ( f ` j ) .- x ) = ( ( f ` 2 ) .- x ) )
44 43 eqeq2d 
 |-  ( j = 2 -> ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) <-> ( ( f ` 1 ) .- x ) = ( ( f ` 2 ) .- x ) ) )
45 42 oveq1d 
 |-  ( j = 2 -> ( ( f ` j ) .- y ) = ( ( f ` 2 ) .- y ) )
46 45 eqeq2d 
 |-  ( j = 2 -> ( ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) <-> ( ( f ` 1 ) .- y ) = ( ( f ` 2 ) .- y ) ) )
47 42 oveq1d 
 |-  ( j = 2 -> ( ( f ` j ) .- z ) = ( ( f ` 2 ) .- z ) )
48 47 eqeq2d 
 |-  ( j = 2 -> ( ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) <-> ( ( f ` 1 ) .- z ) = ( ( f ` 2 ) .- z ) ) )
49 44 46 48 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 ) ) ) )
50 49 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 ) ) ) )
51 6 50 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 ) ) )
52 41 51 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 ) ) )
53 35 52 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 ) ) ) )
54 53 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 ) ) ) ) )
55 54 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 ) ) ) ) )
56 55 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 ) ) ) ) )
57 28 56 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 ) ) ) ) ) )
58 17 6 18 57 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 ) ) ) ) )
59 58 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 ) ) ) ) ) )
60 10 16 59 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 ) ) ) ) ) )