Metamath Proof Explorer

Theorem istrkgcb

Description: Property of being a Tarski geometry - congruence and betweenness part. (Contributed by Thierry Arnoux, 14-Mar-2019)

Ref Expression
Hypotheses istrkg.p 
|- P = ( Base ` G )
istrkg.d 
|- .- = ( dist ` G )
istrkg.i 
|- I = ( Itv ` G )
Assertion istrkgcb 
|- ( G e. TarskiGCB <-> ( G e. _V /\ ( A. x e. P A. y e. P A. z e. P A. u e. P A. a e. P A. b e. P A. c e. P A. v e. P ( ( ( x =/= y /\ y e. ( x I z ) /\ b e. ( a I c ) ) /\ ( ( ( x .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( x .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) /\ A. x e. P A. y e. P A. a e. P A. b e. P E. z e. P ( y e. ( x I z ) /\ ( y .- z ) = ( a .- b ) ) ) ) )

Proof

Step Hyp Ref Expression
1 istrkg.p 
 |-  P = ( Base ` G )
2 istrkg.d 
 |-  .- = ( dist ` G )
3 istrkg.i 
 |-  I = ( Itv ` G )
4 simp1 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> p = P )
5 4 eqcomd 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> P = p )
6 5 adantr 
 |-  ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) -> P = p )
7 6 adantr 
 |-  ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) -> P = p )
8 7 adantr 
 |-  ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) -> P = p )
9 8 adantr 
 |-  ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) -> P = p )
10 9 adantr 
 |-  ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ a e. P ) -> P = p )
11 5 ad6antr 
 |-  ( ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ a e. P ) /\ b e. P ) -> P = p )
12 6 ad6antr 
 |-  ( ( ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ a e. P ) /\ b e. P ) /\ c e. P ) -> P = p )
13 simpll3 
 |-  ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) -> i = I )
14 13 ad6antr 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ v e. P ) -> i = I )
15 14 eqcomd 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ v e. P ) -> I = i )
16 15 oveqd 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ v e. P ) -> ( x I z ) = ( x i z ) )
17 16 eleq2d 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ v e. P ) -> ( y e. ( x I z ) <-> y e. ( x i z ) ) )
18 15 oveqd 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ v e. P ) -> ( a I c ) = ( a i c ) )
19 18 eleq2d 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ v e. P ) -> ( b e. ( a I c ) <-> b e. ( a i c ) ) )
20 17 19 3anbi23d 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ v e. P ) -> ( ( x =/= y /\ y e. ( x I z ) /\ b e. ( a I c ) ) <-> ( x =/= y /\ y e. ( x i z ) /\ b e. ( a i c ) ) ) )
21 simpll2 
 |-  ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) -> d = .- )
22 21 ad6antr 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ v e. P ) -> d = .- )
23 22 eqcomd 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ v e. P ) -> .- = d )
24 23 oveqd 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ v e. P ) -> ( x .- y ) = ( x d y ) )
25 23 oveqd 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ v e. P ) -> ( a .- b ) = ( a d b ) )
26 24 25 eqeq12d 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ v e. P ) -> ( ( x .- y ) = ( a .- b ) <-> ( x d y ) = ( a d b ) ) )
27 23 oveqd 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ v e. P ) -> ( y .- z ) = ( y d z ) )
28 23 oveqd 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ v e. P ) -> ( b .- c ) = ( b d c ) )
29 27 28 eqeq12d 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ v e. P ) -> ( ( y .- z ) = ( b .- c ) <-> ( y d z ) = ( b d c ) ) )
30 26 29 anbi12d 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ v e. P ) -> ( ( ( x .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) <-> ( ( x d y ) = ( a d b ) /\ ( y d z ) = ( b d c ) ) ) )
31 23 oveqd 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ v e. P ) -> ( x .- u ) = ( x d u ) )
32 23 oveqd 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ v e. P ) -> ( a .- v ) = ( a d v ) )
33 31 32 eqeq12d 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ v e. P ) -> ( ( x .- u ) = ( a .- v ) <-> ( x d u ) = ( a d v ) ) )
34 23 oveqd 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ v e. P ) -> ( y .- u ) = ( y d u ) )
35 23 oveqd 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ v e. P ) -> ( b .- v ) = ( b d v ) )
36 34 35 eqeq12d 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ v e. P ) -> ( ( y .- u ) = ( b .- v ) <-> ( y d u ) = ( b d v ) ) )
37 33 36 anbi12d 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ v e. P ) -> ( ( ( x .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) <-> ( ( x d u ) = ( a d v ) /\ ( y d u ) = ( b d v ) ) ) )
38 30 37 anbi12d 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ v e. P ) -> ( ( ( ( x .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( x .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) <-> ( ( ( x d y ) = ( a d b ) /\ ( y d z ) = ( b d c ) ) /\ ( ( x d u ) = ( a d v ) /\ ( y d u ) = ( b d v ) ) ) ) )
39 20 38 anbi12d 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ v e. P ) -> ( ( ( x =/= y /\ y e. ( x I z ) /\ b e. ( a I c ) ) /\ ( ( ( x .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( x .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) <-> ( ( x =/= y /\ y e. ( x i z ) /\ b e. ( a i c ) ) /\ ( ( ( x d y ) = ( a d b ) /\ ( y d z ) = ( b d c ) ) /\ ( ( x d u ) = ( a d v ) /\ ( y d u ) = ( b d v ) ) ) ) ) )
40 23 oveqd 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ v e. P ) -> ( z .- u ) = ( z d u ) )
41 23 oveqd 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ v e. P ) -> ( c .- v ) = ( c d v ) )
42 40 41 eqeq12d 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ v e. P ) -> ( ( z .- u ) = ( c .- v ) <-> ( z d u ) = ( c d v ) ) )
43 39 42 imbi12d 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ v e. P ) -> ( ( ( ( x =/= y /\ y e. ( x I z ) /\ b e. ( a I c ) ) /\ ( ( ( x .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( x .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) <-> ( ( ( x =/= y /\ y e. ( x i z ) /\ b e. ( a i c ) ) /\ ( ( ( x d y ) = ( a d b ) /\ ( y d z ) = ( b d c ) ) /\ ( ( x d u ) = ( a d v ) /\ ( y d u ) = ( b d v ) ) ) ) -> ( z d u ) = ( c d v ) ) ) )
44 12 43 raleqbidva 
 |-  ( ( ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ a e. P ) /\ b e. P ) /\ c e. P ) -> ( A. v e. P ( ( ( x =/= y /\ y e. ( x I z ) /\ b e. ( a I c ) ) /\ ( ( ( x .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( x .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) <-> A. v e. p ( ( ( x =/= y /\ y e. ( x i z ) /\ b e. ( a i c ) ) /\ ( ( ( x d y ) = ( a d b ) /\ ( y d z ) = ( b d c ) ) /\ ( ( x d u ) = ( a d v ) /\ ( y d u ) = ( b d v ) ) ) ) -> ( z d u ) = ( c d v ) ) ) )
45 11 44 raleqbidva 
 |-  ( ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ a e. P ) /\ b e. P ) -> ( A. c e. P A. v e. P ( ( ( x =/= y /\ y e. ( x I z ) /\ b e. ( a I c ) ) /\ ( ( ( x .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( x .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) <-> A. c e. p A. v e. p ( ( ( x =/= y /\ y e. ( x i z ) /\ b e. ( a i c ) ) /\ ( ( ( x d y ) = ( a d b ) /\ ( y d z ) = ( b d c ) ) /\ ( ( x d u ) = ( a d v ) /\ ( y d u ) = ( b d v ) ) ) ) -> ( z d u ) = ( c d v ) ) ) )
46 10 45 raleqbidva 
 |-  ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ a e. P ) -> ( A. b e. P A. c e. P A. v e. P ( ( ( x =/= y /\ y e. ( x I z ) /\ b e. ( a I c ) ) /\ ( ( ( x .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( x .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) <-> A. b e. p A. c e. p A. v e. p ( ( ( x =/= y /\ y e. ( x i z ) /\ b e. ( a i c ) ) /\ ( ( ( x d y ) = ( a d b ) /\ ( y d z ) = ( b d c ) ) /\ ( ( x d u ) = ( a d v ) /\ ( y d u ) = ( b d v ) ) ) ) -> ( z d u ) = ( c d v ) ) ) )
47 9 46 raleqbidva 
 |-  ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) -> ( A. a e. P A. b e. P A. c e. P A. v e. P ( ( ( x =/= y /\ y e. ( x I z ) /\ b e. ( a I c ) ) /\ ( ( ( x .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( x .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) <-> A. a e. p A. b e. p A. c e. p A. v e. p ( ( ( x =/= y /\ y e. ( x i z ) /\ b e. ( a i c ) ) /\ ( ( ( x d y ) = ( a d b ) /\ ( y d z ) = ( b d c ) ) /\ ( ( x d u ) = ( a d v ) /\ ( y d u ) = ( b d v ) ) ) ) -> ( z d u ) = ( c d v ) ) ) )
48 8 47 raleqbidva 
 |-  ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) -> ( A. u e. P A. a e. P A. b e. P A. c e. P A. v e. P ( ( ( x =/= y /\ y e. ( x I z ) /\ b e. ( a I c ) ) /\ ( ( ( x .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( x .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) <-> A. u e. p A. a e. p A. b e. p A. c e. p A. v e. p ( ( ( x =/= y /\ y e. ( x i z ) /\ b e. ( a i c ) ) /\ ( ( ( x d y ) = ( a d b ) /\ ( y d z ) = ( b d c ) ) /\ ( ( x d u ) = ( a d v ) /\ ( y d u ) = ( b d v ) ) ) ) -> ( z d u ) = ( c d v ) ) ) )
49 7 48 raleqbidva 
 |-  ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) -> ( A. z e. P A. u e. P A. a e. P A. b e. P A. c e. P A. v e. P ( ( ( x =/= y /\ y e. ( x I z ) /\ b e. ( a I c ) ) /\ ( ( ( x .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( x .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) <-> A. z e. p A. u e. p A. a e. p A. b e. p A. c e. p A. v e. p ( ( ( x =/= y /\ y e. ( x i z ) /\ b e. ( a i c ) ) /\ ( ( ( x d y ) = ( a d b ) /\ ( y d z ) = ( b d c ) ) /\ ( ( x d u ) = ( a d v ) /\ ( y d u ) = ( b d v ) ) ) ) -> ( z d u ) = ( c d v ) ) ) )
50 6 49 raleqbidva 
 |-  ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) -> ( A. y e. P A. z e. P A. u e. P A. a e. P A. b e. P A. c e. P A. v e. P ( ( ( x =/= y /\ y e. ( x I z ) /\ b e. ( a I c ) ) /\ ( ( ( x .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( x .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) <-> A. y e. p A. z e. p A. u e. p A. a e. p A. b e. p A. c e. p A. v e. p ( ( ( x =/= y /\ y e. ( x i z ) /\ b e. ( a i c ) ) /\ ( ( ( x d y ) = ( a d b ) /\ ( y d z ) = ( b d c ) ) /\ ( ( x d u ) = ( a d v ) /\ ( y d u ) = ( b d v ) ) ) ) -> ( z d u ) = ( c d v ) ) ) )
51 5 50 raleqbidva 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( A. x e. P A. y e. P A. z e. P A. u e. P A. a e. P A. b e. P A. c e. P A. v e. P ( ( ( x =/= y /\ y e. ( x I z ) /\ b e. ( a I c ) ) /\ ( ( ( x .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( x .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) <-> A. x e. p A. y e. p A. z e. p A. u e. p A. a e. p A. b e. p A. c e. p A. v e. p ( ( ( x =/= y /\ y e. ( x i z ) /\ b e. ( a i c ) ) /\ ( ( ( x d y ) = ( a d b ) /\ ( y d z ) = ( b d c ) ) /\ ( ( x d u ) = ( a d v ) /\ ( y d u ) = ( b d v ) ) ) ) -> ( z d u ) = ( c d v ) ) ) )
52 7 adantr 
 |-  ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ a e. P ) -> P = p )
53 52 adantr 
 |-  ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ a e. P ) /\ b e. P ) -> P = p )
54 13 ad3antrrr 
 |-  ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ a e. P ) /\ b e. P ) /\ z e. P ) -> i = I )
55 54 eqcomd 
 |-  ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ a e. P ) /\ b e. P ) /\ z e. P ) -> I = i )
56 55 oveqd 
 |-  ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ a e. P ) /\ b e. P ) /\ z e. P ) -> ( x I z ) = ( x i z ) )
57 56 eleq2d 
 |-  ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ a e. P ) /\ b e. P ) /\ z e. P ) -> ( y e. ( x I z ) <-> y e. ( x i z ) ) )
58 21 ad3antrrr 
 |-  ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ a e. P ) /\ b e. P ) /\ z e. P ) -> d = .- )
59 58 eqcomd 
 |-  ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ a e. P ) /\ b e. P ) /\ z e. P ) -> .- = d )
60 59 oveqd 
 |-  ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ a e. P ) /\ b e. P ) /\ z e. P ) -> ( y .- z ) = ( y d z ) )
61 59 oveqd 
 |-  ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ a e. P ) /\ b e. P ) /\ z e. P ) -> ( a .- b ) = ( a d b ) )
62 60 61 eqeq12d 
 |-  ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ a e. P ) /\ b e. P ) /\ z e. P ) -> ( ( y .- z ) = ( a .- b ) <-> ( y d z ) = ( a d b ) ) )
63 57 62 anbi12d 
 |-  ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ a e. P ) /\ b e. P ) /\ z e. P ) -> ( ( y e. ( x I z ) /\ ( y .- z ) = ( a .- b ) ) <-> ( y e. ( x i z ) /\ ( y d z ) = ( a d b ) ) ) )
64 53 63 rexeqbidva 
 |-  ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ a e. P ) /\ b e. P ) -> ( E. z e. P ( y e. ( x I z ) /\ ( y .- z ) = ( a .- b ) ) <-> E. z e. p ( y e. ( x i z ) /\ ( y d z ) = ( a d b ) ) ) )
65 52 64 raleqbidva 
 |-  ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ a e. P ) -> ( A. b e. P E. z e. P ( y e. ( x I z ) /\ ( y .- z ) = ( a .- b ) ) <-> A. b e. p E. z e. p ( y e. ( x i z ) /\ ( y d z ) = ( a d b ) ) ) )
66 7 65 raleqbidva 
 |-  ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) -> ( A. a e. P A. b e. P E. z e. P ( y e. ( x I z ) /\ ( y .- z ) = ( a .- b ) ) <-> A. a e. p A. b e. p E. z e. p ( y e. ( x i z ) /\ ( y d z ) = ( a d b ) ) ) )
67 6 66 raleqbidva 
 |-  ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) -> ( A. y e. P A. a e. P A. b e. P E. z e. P ( y e. ( x I z ) /\ ( y .- z ) = ( a .- b ) ) <-> A. y e. p A. a e. p A. b e. p E. z e. p ( y e. ( x i z ) /\ ( y d z ) = ( a d b ) ) ) )
68 5 67 raleqbidva 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( A. x e. P A. y e. P A. a e. P A. b e. P E. z e. P ( y e. ( x I z ) /\ ( y .- z ) = ( a .- b ) ) <-> A. x e. p A. y e. p A. a e. p A. b e. p E. z e. p ( y e. ( x i z ) /\ ( y d z ) = ( a d b ) ) ) )
69 51 68 anbi12d 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( ( A. x e. P A. y e. P A. z e. P A. u e. P A. a e. P A. b e. P A. c e. P A. v e. P ( ( ( x =/= y /\ y e. ( x I z ) /\ b e. ( a I c ) ) /\ ( ( ( x .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( x .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) /\ A. x e. P A. y e. P A. a e. P A. b e. P E. z e. P ( y e. ( x I z ) /\ ( y .- z ) = ( a .- b ) ) ) <-> ( A. x e. p A. y e. p A. z e. p A. u e. p A. a e. p A. b e. p A. c e. p A. v e. p ( ( ( x =/= y /\ y e. ( x i z ) /\ b e. ( a i c ) ) /\ ( ( ( x d y ) = ( a d b ) /\ ( y d z ) = ( b d c ) ) /\ ( ( x d u ) = ( a d v ) /\ ( y d u ) = ( b d v ) ) ) ) -> ( z d u ) = ( c d v ) ) /\ A. x e. p A. y e. p A. a e. p A. b e. p E. z e. p ( y e. ( x i z ) /\ ( y d z ) = ( a d b ) ) ) ) )
70 1 2 3 69 sbcie3s 
 |-  ( f = G -> ( [. ( Base ` f ) / p ]. [. ( dist ` f ) / d ]. [. ( Itv ` f ) / i ]. ( A. x e. p A. y e. p A. z e. p A. u e. p A. a e. p A. b e. p A. c e. p A. v e. p ( ( ( x =/= y /\ y e. ( x i z ) /\ b e. ( a i c ) ) /\ ( ( ( x d y ) = ( a d b ) /\ ( y d z ) = ( b d c ) ) /\ ( ( x d u ) = ( a d v ) /\ ( y d u ) = ( b d v ) ) ) ) -> ( z d u ) = ( c d v ) ) /\ A. x e. p A. y e. p A. a e. p A. b e. p E. z e. p ( y e. ( x i z ) /\ ( y d z ) = ( a d b ) ) ) <-> ( A. x e. P A. y e. P A. z e. P A. u e. P A. a e. P A. b e. P A. c e. P A. v e. P ( ( ( x =/= y /\ y e. ( x I z ) /\ b e. ( a I c ) ) /\ ( ( ( x .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( x .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) /\ A. x e. P A. y e. P A. a e. P A. b e. P E. z e. P ( y e. ( x I z ) /\ ( y .- z ) = ( a .- b ) ) ) ) )
71 df-trkgcb 
 |-  TarskiGCB = { f | [. ( Base ` f ) / p ]. [. ( dist ` f ) / d ]. [. ( Itv ` f ) / i ]. ( A. x e. p A. y e. p A. z e. p A. u e. p A. a e. p A. b e. p A. c e. p A. v e. p ( ( ( x =/= y /\ y e. ( x i z ) /\ b e. ( a i c ) ) /\ ( ( ( x d y ) = ( a d b ) /\ ( y d z ) = ( b d c ) ) /\ ( ( x d u ) = ( a d v ) /\ ( y d u ) = ( b d v ) ) ) ) -> ( z d u ) = ( c d v ) ) /\ A. x e. p A. y e. p A. a e. p A. b e. p E. z e. p ( y e. ( x i z ) /\ ( y d z ) = ( a d b ) ) ) }
72 70 71 elab4g 
 |-  ( G e. TarskiGCB <-> ( G e. _V /\ ( A. x e. P A. y e. P A. z e. P A. u e. P A. a e. P A. b e. P A. c e. P A. v e. P ( ( ( x =/= y /\ y e. ( x I z ) /\ b e. ( a I c ) ) /\ ( ( ( x .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( x .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) /\ A. x e. P A. y e. P A. a e. P A. b e. P E. z e. P ( y e. ( x I z ) /\ ( y .- z ) = ( a .- b ) ) ) ) )