Metamath Proof Explorer

Definition df-leg

Description: Define the less-than relationship between geometric distance congruence classes. See legval . (Contributed by Thierry Arnoux, 21-Jun-2019)

Ref Expression
Assertion df-leg 
|- leG = ( g e. _V |-> { <. e , f >. | [. ( Base ` g ) / p ]. [. ( dist ` g ) / d ]. [. ( Itv ` g ) / i ]. E. x e. p E. y e. p ( f = ( x d y ) /\ E. z e. p ( z e. ( x i y ) /\ e = ( x d z ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cleg 
 |-  leG
1 vg 
 |-  g
2 cvv 
 |-  _V
3 ve 
 |-  e
4 vf 
 |-  f
5 cbs 
 |-  Base
6 1 cv 
 |-  g
7 6 5 cfv 
 |-  ( Base ` g )
8 vp 
 |-  p
9 cds 
 |-  dist
10 6 9 cfv 
 |-  ( dist ` g )
11 vd 
 |-  d
12 citv 
 |-  Itv
13 6 12 cfv 
 |-  ( Itv ` g )
14 vi 
 |-  i
15 vx 
 |-  x
16 8 cv 
 |-  p
17 vy 
 |-  y
18 4 cv 
 |-  f
19 15 cv 
 |-  x
20 11 cv 
 |-  d
21 17 cv 
 |-  y
22 19 21 20 co 
 |-  ( x d y )
23 18 22 wceq 
 |-  f = ( x d y )
24 vz 
 |-  z
25 24 cv 
 |-  z
26 14 cv 
 |-  i
27 19 21 26 co 
 |-  ( x i y )
28 25 27 wcel 
 |-  z e. ( x i y )
29 3 cv 
 |-  e
30 19 25 20 co 
 |-  ( x d z )
31 29 30 wceq 
 |-  e = ( x d z )
32 28 31 wa 
 |-  ( z e. ( x i y ) /\ e = ( x d z ) )
33 32 24 16 wrex 
 |-  E. z e. p ( z e. ( x i y ) /\ e = ( x d z ) )
34 23 33 wa 
 |-  ( f = ( x d y ) /\ E. z e. p ( z e. ( x i y ) /\ e = ( x d z ) ) )
35 34 17 16 wrex 
 |-  E. y e. p ( f = ( x d y ) /\ E. z e. p ( z e. ( x i y ) /\ e = ( x d z ) ) )
36 35 15 16 wrex 
 |-  E. x e. p E. y e. p ( f = ( x d y ) /\ E. z e. p ( z e. ( x i y ) /\ e = ( x d z ) ) )
37 36 14 13 wsbc 
 |-  [. ( Itv ` g ) / i ]. E. x e. p E. y e. p ( f = ( x d y ) /\ E. z e. p ( z e. ( x i y ) /\ e = ( x d z ) ) )
38 37 11 10 wsbc 
 |-  [. ( dist ` g ) / d ]. [. ( Itv ` g ) / i ]. E. x e. p E. y e. p ( f = ( x d y ) /\ E. z e. p ( z e. ( x i y ) /\ e = ( x d z ) ) )
39 38 8 7 wsbc 
 |-  [. ( Base ` g ) / p ]. [. ( dist ` g ) / d ]. [. ( Itv ` g ) / i ]. E. x e. p E. y e. p ( f = ( x d y ) /\ E. z e. p ( z e. ( x i y ) /\ e = ( x d z ) ) )
40 39 3 4 copab 
 |-  { <. e , f >. | [. ( Base ` g ) / p ]. [. ( dist ` g ) / d ]. [. ( Itv ` g ) / i ]. E. x e. p E. y e. p ( f = ( x d y ) /\ E. z e. p ( z e. ( x i y ) /\ e = ( x d z ) ) ) }
41 1 2 40 cmpt 
 |-  ( g e. _V |-> { <. e , f >. | [. ( Base ` g ) / p ]. [. ( dist ` g ) / d ]. [. ( Itv ` g ) / i ]. E. x e. p E. y e. p ( f = ( x d y ) /\ E. z e. p ( z e. ( x i y ) /\ e = ( x d z ) ) ) } )
42 0 41 wceq 
 |-  leG = ( g e. _V |-> { <. e , f >. | [. ( Base ` g ) / p ]. [. ( dist ` g ) / d ]. [. ( Itv ` g ) / i ]. E. x e. p E. y e. p ( f = ( x d y ) /\ E. z e. p ( z e. ( x i y ) /\ e = ( x d z ) ) ) } )