Metamath Proof Explorer

Definition df-segle

Description: Define the segment length comparison relationship. This relationship expresses that the segment A B is no longer than C D . In this section, we establish various properties of this relationship showing that it is a transitive, reflexive relationship on pairs of points that is substitutive under congruence. Definition 5.4 of Schwabhauser p. 41. (Contributed by Scott Fenton, 11-Oct-2013)

Ref Expression
Assertion df-segle 
|- Seg<_ = { <. p , q >. | E. n e. NN E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( p = <. a , b >. /\ q = <. c , d >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 csegle 
 |-  Seg<_
1 vp 
 |-  p
2 vq 
 |-  q
3 vn 
 |-  n
4 cn 
 |-  NN
5 va 
 |-  a
6 cee 
 |-  EE
7 3 cv 
 |-  n
8 7 6 cfv 
 |-  ( EE ` n )
9 vb 
 |-  b
10 vc 
 |-  c
11 vd 
 |-  d
12 1 cv 
 |-  p
13 5 cv 
 |-  a
14 9 cv 
 |-  b
15 13 14 cop 
 |-  <. a , b >.
16 12 15 wceq 
 |-  p = <. a , b >.
17 2 cv 
 |-  q
18 10 cv 
 |-  c
19 11 cv 
 |-  d
20 18 19 cop 
 |-  <. c , d >.
21 17 20 wceq 
 |-  q = <. c , d >.
22 vy 
 |-  y
23 22 cv 
 |-  y
24 cbtwn 
 |-  Btwn
25 23 20 24 wbr 
 |-  y Btwn <. c , d >.
26 ccgr 
 |-  Cgr
27 18 23 cop 
 |-  <. c , y >.
28 15 27 26 wbr 
 |-  <. a , b >. Cgr <. c , y >.
29 25 28 wa 
 |-  ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. )
30 29 22 8 wrex 
 |-  E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. )
31 16 21 30 w3a 
 |-  ( p = <. a , b >. /\ q = <. c , d >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) )
32 31 11 8 wrex 
 |-  E. d e. ( EE ` n ) ( p = <. a , b >. /\ q = <. c , d >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) )
33 32 10 8 wrex 
 |-  E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( p = <. a , b >. /\ q = <. c , d >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) )
34 33 9 8 wrex 
 |-  E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( p = <. a , b >. /\ q = <. c , d >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) )
35 34 5 8 wrex 
 |-  E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( p = <. a , b >. /\ q = <. c , d >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) )
36 35 3 4 wrex 
 |-  E. n e. NN E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( p = <. a , b >. /\ q = <. c , d >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) )
37 36 1 2 copab 
 |-  { <. p , q >. | E. n e. NN E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( p = <. a , b >. /\ q = <. c , d >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) }
38 0 37 wceq 
 |-  Seg<_ = { <. p , q >. | E. n e. NN E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( p = <. a , b >. /\ q = <. c , d >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) }