Metamath Proof Explorer

Definition df-trkgcb

Description: Define the class of geometries fulfilling the five segment axiom, Axiom A5 of Schwabhauser p. 11, and segment construction axiom, Axiom A4 of Schwabhauser p. 11. (Contributed by Thierry Arnoux, 14-Mar-2019)

Ref Expression
Assertion 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 ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cstrkgcb 
 |-  TarskiGCB
1 vf 
 |-  f
2 cbs 
 |-  Base
3 1 cv 
 |-  f
4 3 2 cfv 
 |-  ( Base ` f )
5 vp 
 |-  p
6 cds 
 |-  dist
7 3 6 cfv 
 |-  ( dist ` f )
8 vd 
 |-  d
9 citv 
 |-  Itv
10 3 9 cfv 
 |-  ( Itv ` f )
11 vi 
 |-  i
12 vx 
 |-  x
13 5 cv 
 |-  p
14 vy 
 |-  y
15 vz 
 |-  z
16 vu 
 |-  u
17 va 
 |-  a
18 vb 
 |-  b
19 vc 
 |-  c
20 vv 
 |-  v
21 12 cv 
 |-  x
22 14 cv 
 |-  y
23 21 22 wne 
 |-  x =/= y
24 11 cv 
 |-  i
25 15 cv 
 |-  z
26 21 25 24 co 
 |-  ( x i z )
27 22 26 wcel 
 |-  y e. ( x i z )
28 18 cv 
 |-  b
29 17 cv 
 |-  a
30 19 cv 
 |-  c
31 29 30 24 co 
 |-  ( a i c )
32 28 31 wcel 
 |-  b e. ( a i c )
33 23 27 32 w3a 
 |-  ( x =/= y /\ y e. ( x i z ) /\ b e. ( a i c ) )
34 8 cv 
 |-  d
35 21 22 34 co 
 |-  ( x d y )
36 29 28 34 co 
 |-  ( a d b )
37 35 36 wceq 
 |-  ( x d y ) = ( a d b )
38 22 25 34 co 
 |-  ( y d z )
39 28 30 34 co 
 |-  ( b d c )
40 38 39 wceq 
 |-  ( y d z ) = ( b d c )
41 37 40 wa 
 |-  ( ( x d y ) = ( a d b ) /\ ( y d z ) = ( b d c ) )
42 16 cv 
 |-  u
43 21 42 34 co 
 |-  ( x d u )
44 20 cv 
 |-  v
45 29 44 34 co 
 |-  ( a d v )
46 43 45 wceq 
 |-  ( x d u ) = ( a d v )
47 22 42 34 co 
 |-  ( y d u )
48 28 44 34 co 
 |-  ( b d v )
49 47 48 wceq 
 |-  ( y d u ) = ( b d v )
50 46 49 wa 
 |-  ( ( x d u ) = ( a d v ) /\ ( y d u ) = ( b d v ) )
51 41 50 wa 
 |-  ( ( ( x d y ) = ( a d b ) /\ ( y d z ) = ( b d c ) ) /\ ( ( x d u ) = ( a d v ) /\ ( y d u ) = ( b d v ) ) )
52 33 51 wa 
 |-  ( ( 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 ) ) ) )
53 25 42 34 co 
 |-  ( z d u )
54 30 44 34 co 
 |-  ( c d v )
55 53 54 wceq 
 |-  ( z d u ) = ( c d v )
56 52 55 wi 
 |-  ( ( ( 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 ) )
57 56 20 13 wral 
 |-  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 ) )
58 57 19 13 wral 
 |-  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 ) )
59 58 18 13 wral 
 |-  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 ) )
60 59 17 13 wral 
 |-  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 ) )
61 60 16 13 wral 
 |-  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 ) )
62 61 15 13 wral 
 |-  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 ) )
63 62 14 13 wral 
 |-  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 ) )
64 63 12 13 wral 
 |-  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 ) )
65 38 36 wceq 
 |-  ( y d z ) = ( a d b )
66 27 65 wa 
 |-  ( y e. ( x i z ) /\ ( y d z ) = ( a d b ) )
67 66 15 13 wrex 
 |-  E. z e. p ( y e. ( x i z ) /\ ( y d z ) = ( a d b ) )
68 67 18 13 wral 
 |-  A. b e. p E. z e. p ( y e. ( x i z ) /\ ( y d z ) = ( a d b ) )
69 68 17 13 wral 
 |-  A. a e. p A. b e. p E. z e. p ( y e. ( x i z ) /\ ( y d z ) = ( a d b ) )
70 69 14 13 wral 
 |-  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 ) )
71 70 12 13 wral 
 |-  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 64 71 wa 
 |-  ( 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 ) ) )
73 72 11 10 wsbc 
 |-  [. ( 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 ) ) )
74 73 8 7 wsbc 
 |-  [. ( 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 ) ) )
75 74 5 4 wsbc 
 |-  [. ( 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 ) ) )
76 75 1 cab 
 |-  { 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 ) ) ) }
77 0 76 wceq 
 |-  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 ) ) ) }