Metamath Proof Explorer

Definition df-leag

Description: Definition of the geometrical "angle less than" relation. Definition 11.27 of Schwabhauser p. 102. (Contributed by Thierry Arnoux, 7-Oct-2020)

Ref Expression
Assertion df-leag 
|- leA = ( g e. _V |-> { <. a , b >. | ( ( a e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) /\ b e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) ) /\ E. x e. ( Base ` g ) ( x ( inA ` g ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) "> /\ <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> ( cgrA ` g ) <" ( b ` 0 ) ( b ` 1 ) x "> ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cleag 
 |-  leA
1 vg 
 |-  g
2 cvv 
 |-  _V
3 va 
 |-  a
4 vb 
 |-  b
5 3 cv 
 |-  a
6 cbs 
 |-  Base
7 1 cv 
 |-  g
8 7 6 cfv 
 |-  ( Base ` g )
9 cmap 
 |-  ^m
10 cc0 
 |-  0
11 cfzo 
 |-  ..^
12 c3 
 |-  3
13 10 12 11 co 
 |-  ( 0 ..^ 3 )
14 8 13 9 co 
 |-  ( ( Base ` g ) ^m ( 0 ..^ 3 ) )
15 5 14 wcel 
 |-  a e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) )
16 4 cv 
 |-  b
17 16 14 wcel 
 |-  b e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) )
18 15 17 wa 
 |-  ( a e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) /\ b e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) )
19 vx 
 |-  x
20 19 cv 
 |-  x
21 cinag 
 |-  inA
22 7 21 cfv 
 |-  ( inA ` g )
23 10 16 cfv 
 |-  ( b ` 0 )
24 c1 
 |-  1
25 24 16 cfv 
 |-  ( b ` 1 )
26 c2 
 |-  2
27 26 16 cfv 
 |-  ( b ` 2 )
28 23 25 27 cs3 
 |-  <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) ">
29 20 28 22 wbr 
 |-  x ( inA ` g ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) ">
30 10 5 cfv 
 |-  ( a ` 0 )
31 24 5 cfv 
 |-  ( a ` 1 )
32 26 5 cfv 
 |-  ( a ` 2 )
33 30 31 32 cs3 
 |-  <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) ">
34 ccgra 
 |-  cgrA
35 7 34 cfv 
 |-  ( cgrA ` g )
36 23 25 20 cs3 
 |-  <" ( b ` 0 ) ( b ` 1 ) x ">
37 33 36 35 wbr 
 |-  <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> ( cgrA ` g ) <" ( b ` 0 ) ( b ` 1 ) x ">
38 29 37 wa 
 |-  ( x ( inA ` g ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) "> /\ <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> ( cgrA ` g ) <" ( b ` 0 ) ( b ` 1 ) x "> )
39 38 19 8 wrex 
 |-  E. x e. ( Base ` g ) ( x ( inA ` g ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) "> /\ <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> ( cgrA ` g ) <" ( b ` 0 ) ( b ` 1 ) x "> )
40 18 39 wa 
 |-  ( ( a e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) /\ b e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) ) /\ E. x e. ( Base ` g ) ( x ( inA ` g ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) "> /\ <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> ( cgrA ` g ) <" ( b ` 0 ) ( b ` 1 ) x "> ) )
41 40 3 4 copab 
 |-  { <. a , b >. | ( ( a e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) /\ b e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) ) /\ E. x e. ( Base ` g ) ( x ( inA ` g ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) "> /\ <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> ( cgrA ` g ) <" ( b ` 0 ) ( b ` 1 ) x "> ) ) }
42 1 2 41 cmpt 
 |-  ( g e. _V |-> { <. a , b >. | ( ( a e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) /\ b e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) ) /\ E. x e. ( Base ` g ) ( x ( inA ` g ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) "> /\ <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> ( cgrA ` g ) <" ( b ` 0 ) ( b ` 1 ) x "> ) ) } )
43 0 42 wceq 
 |-  leA = ( g e. _V |-> { <. a , b >. | ( ( a e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) /\ b e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) ) /\ E. x e. ( Base ` g ) ( x ( inA ` g ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) "> /\ <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> ( cgrA ` g ) <" ( b ` 0 ) ( b ` 1 ) x "> ) ) } )