Metamath Proof Explorer

Theorem istrkg2d

Description: Property of fulfilling dimension 2 axiom. (Contributed by Thierry Arnoux, 29-May-2019) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step Hyp Ref Expression
1 istrkg2d.p 
 |-  P = ( Base ` G )
2 istrkg2d.d 
 |-  .- = ( dist ` G )
3 istrkg2d.i 
 |-  I = ( Itv ` G )
4 simp1 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> p = P )
5 4 eqcomd 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> P = p )
6 simp3 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> i = I )
7 6 eqcomd 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> I = i )
8 7 oveqd 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( x I y ) = ( x i y ) )
9 8 eleq2d 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( z e. ( x I y ) <-> z e. ( x i y ) ) )
10 7 oveqd 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( z I y ) = ( z i y ) )
11 10 eleq2d 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( x e. ( z I y ) <-> x e. ( z i y ) ) )
12 7 oveqd 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( x I z ) = ( x i z ) )
13 12 eleq2d 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( y e. ( x I z ) <-> y e. ( x i z ) ) )
14 9 11 13 3orbi123d 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( ( 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 ) ) ) )
15 14 notbid 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( -. ( 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 ) ) ) )
16 5 15 rexeqbidv 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( E. z e. P -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) <-> E. z e. p -. ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) ) )
17 5 16 rexeqbidv 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( E. y e. P E. z e. P -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) <-> E. y e. p E. z e. p -. ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) ) )
18 5 17 rexeqbidv 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( 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 ) ) <-> 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 ) ) ) )
19 simp2 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> d = .- )
20 19 eqcomd 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> .- = d )
21 20 oveqd 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( x .- u ) = ( x d u ) )
22 20 oveqd 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( x .- v ) = ( x d v ) )
23 21 22 eqeq12d 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( ( x .- u ) = ( x .- v ) <-> ( x d u ) = ( x d v ) ) )
24 20 oveqd 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( y .- u ) = ( y d u ) )
25 20 oveqd 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( y .- v ) = ( y d v ) )
26 24 25 eqeq12d 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( ( y .- u ) = ( y .- v ) <-> ( y d u ) = ( y d v ) ) )
27 20 oveqd 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( z .- u ) = ( z d u ) )
28 20 oveqd 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( z .- v ) = ( z d v ) )
29 27 28 eqeq12d 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( ( z .- u ) = ( z .- v ) <-> ( z d u ) = ( z d v ) ) )
30 23 26 29 3anbi123d 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( ( ( x .- u ) = ( x .- v ) /\ ( y .- u ) = ( y .- v ) /\ ( z .- u ) = ( z .- v ) ) <-> ( ( x d u ) = ( x d v ) /\ ( y d u ) = ( y d v ) /\ ( z d u ) = ( z d v ) ) ) )
31 30 anbi1d 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( ( ( ( x .- u ) = ( x .- v ) /\ ( y .- u ) = ( y .- v ) /\ ( z .- u ) = ( z .- v ) ) /\ u =/= v ) <-> ( ( ( x d u ) = ( x d v ) /\ ( y d u ) = ( y d v ) /\ ( z d u ) = ( z d v ) ) /\ u =/= v ) ) )
32 31 14 imbi12d 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( ( ( ( ( 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 d u ) = ( x d v ) /\ ( y d u ) = ( y d v ) /\ ( z d u ) = ( z d v ) ) /\ u =/= v ) -> ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) ) ) )
33 5 32 raleqbidv 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( 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. v e. p ( ( ( ( x d u ) = ( x d v ) /\ ( y d u ) = ( y d v ) /\ ( z d u ) = ( z d v ) ) /\ u =/= v ) -> ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) ) ) )
34 5 33 raleqbidv 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( 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 d u ) = ( x d v ) /\ ( y d u ) = ( y d v ) /\ ( z d u ) = ( z d v ) ) /\ u =/= v ) -> ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) ) ) )
35 5 34 raleqbidv 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( 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. z e. p A. u e. p A. v e. p ( ( ( ( x d u ) = ( x d v ) /\ ( y d u ) = ( y d v ) /\ ( z d u ) = ( z d v ) ) /\ u =/= v ) -> ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) ) ) )
36 5 35 raleqbidv 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( 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. y e. p A. z e. p A. u e. p A. v e. p ( ( ( ( x d u ) = ( x d v ) /\ ( y d u ) = ( y d v ) /\ ( z d u ) = ( z d v ) ) /\ u =/= v ) -> ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) ) ) )
37 5 36 raleqbidv 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( 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. x e. p A. y e. p A. z e. p A. u e. p A. v e. p ( ( ( ( x d u ) = ( x d v ) /\ ( y d u ) = ( y d v ) /\ ( z d u ) = ( z d v ) ) /\ u =/= v ) -> ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) ) ) )
38 18 37 anbi12d 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( ( 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 ) ) ) ) <-> ( 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 d u ) = ( x d v ) /\ ( y d u ) = ( y d v ) /\ ( z d u ) = ( z d v ) ) /\ u =/= v ) -> ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) ) ) ) )
39 1 2 3 38 sbcie3s 
 |-  ( f = G -> ( [. ( Base ` f ) / p ]. [. ( dist ` f ) / d ]. [. ( Itv ` f ) / i ]. ( 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 d u ) = ( x d v ) /\ ( y d u ) = ( y d v ) /\ ( z d u ) = ( z d v ) ) /\ u =/= v ) -> ( 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 -. ( 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 ) ) ) ) ) )
40 df-trkg2d 
 |-  TarskiG2D = { f | [. ( Base ` f ) / p ]. [. ( dist ` f ) / d ]. [. ( Itv ` f ) / i ]. ( 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 d u ) = ( x d v ) /\ ( y d u ) = ( y d v ) /\ ( z d u ) = ( z d v ) ) /\ u =/= v ) -> ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) ) ) }
41 39 40 elab4g 
 |-  ( 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 ) ) ) ) ) )