Theorem istrkgcb 25355

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

Hypotheses

Ref	Expression
istrkg.p	|- P = ( Base ` G )
istrkg.d	|- .- = ( dist ` G )
istrkg.i	|- I = (Itv ` G )

Assertion

Ref

Expression

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 ) ) ) ) )

Distinct variable groups:   a, b, c, u, v, x, y, z, I   P, a, b, c, u, v, x, y, z   .- , a, b, c, u, v, x, y, z

Allowed substitution hints:   G( x, y, z, v, u, a, b, c)

Proof of Theorem istrkgcb

Dummy variables f d i p are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		istrkg.p	. . 3 |- P = ( Base ` G )
2		istrkg.d	. . 3 |- .- = ( dist ` G )
3		istrkg.i	. . 3 |- I = (Itv ` G )
4		simp1 1061	. . . . . 6 |- ( ( p = P /\ d = .- /\ i = I ) -> p = P )
5	4	eqcomd 2628	. . . . 5 |- ( ( p = P /\ d = .- /\ i = I ) -> P = p )
6	5	adantr 481	. . . . . 6 |- ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) -> P = p )
7	6	adantr 481	. . . . . . 7 |- ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) -> P = p )
8	7	adantr 481	. . . . . . . 8 |- ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) -> P = p )
9	8	adantr 481	. . . . . . . . 9 |- ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) -> P = p )
10	9	adantr 481	. . . . . . . . . 10 |- ( ( ( ( ( ( ( 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 772	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( 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 772	. . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( ( 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 1102	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) -> i = I )
14	13	ad6antr 772	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( 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 2628	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( 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 6667	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ( ( ( 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 2687	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ( 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 6667	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ( ( ( 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 2687	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ( 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 1402	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( ( ( 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 1101	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) -> d = .- )
22	21	ad6antr 772	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( ( ( ( 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 2628	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( 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 6667	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( 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 6667	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( 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 2637	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ( ( ( 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 6667	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( 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 6667	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( 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 2637	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ( ( ( 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 747	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ( 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 6667	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( 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 6667	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( 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 2637	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ( ( ( 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 6667	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( 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 6667	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( 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 2637	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ( ( ( 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 747	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ( 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 747	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( ( ( 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 747	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( ( ( 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 6667	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( ( ( 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 6667	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( ( ( 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 2637	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( ( ( 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 334	. . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( ( ( 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 3154	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( 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 3154	. . . . . . . . . 10 |- ( ( ( ( ( ( ( ( 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 3154	. . . . . . . . 9 |- ( ( ( ( ( ( ( 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 3154	. . . . . . . 8 |- ( ( ( ( ( ( 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 3154	. . . . . . 7 |- ( ( ( ( ( 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 3154	. . . . . 6 |- ( ( ( ( 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 3154	. . . . 5 |- ( ( ( 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 3154	. . . 4 |- ( ( 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 481	. . . . . . . 8 |- ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ a e. P ) -> P = p )
53	52	adantr 481	. . . . . . . . 9 |- ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ a e. P ) /\ b e. P ) -> P = p )
54	13	ad3antrrr 766	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( 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 2628	. . . . . . . . . . . 12 |- ( ( ( ( ( ( ( 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 6667	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( 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 2687	. . . . . . . . . 10 |- ( ( ( ( ( ( ( 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 766	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ a e. P ) /\ b e. P ) /\ z e. P ) -> d = .- )
59	58	eqcomd 2628	. . . . . . . . . . . 12 |- ( ( ( ( ( ( ( p = P /\ d = .- /\ i = I ) /\ x e. P ) /\ y e. P ) /\ a e. P ) /\ b e. P ) /\ z e. P ) -> .- = d )
60	59	oveqd 6667	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( 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 6667	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( 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 2637	. . . . . . . . . 10 |- ( ( ( ( ( ( ( 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 747	. . . . . . . . 9 |- ( ( ( ( ( ( ( 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 3155	. . . . . . . 8 |- ( ( ( ( ( ( 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 3154	. . . . . . 7 |- ( ( ( ( ( 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 3154	. . . . . 6 |- ( ( ( ( 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 3154	. . . . 5 |- ( ( ( 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 3154	. . . 4 |- ( ( 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 747	. . 3 |- ( ( 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 15917	. 2 |- ( 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 25349	. 2 |- 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 3355	1 |- ( 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 ) ) ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   _Vcvv 3200   [.wsbc 3435   ` cfv 5888  (class class class)co 6650   Basecbs 15857   distcds 15950  TarskiG_CBcstrkgcb 25332  Itvcitv 25335

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-nul 4789

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653  df-trkgcb 25349

This theorem is referenced by:  axtgsegcon  25363  axtg5seg  25364  f1otrg  25751  eengtrkg  25865