Metamath Proof Explorer

Definition df-cgra

Description: Define the congruence relation between angles. As for triangles we use "words of points". See iscgra for a more human readable version. (Contributed by Thierry Arnoux, 30-Jul-2020)

Ref Expression
Assertion df-cgra 
|- cgrA = ( g e. _V |-> { <. a , b >. | [. ( Base ` g ) / p ]. [. ( hlG ` g ) / k ]. ( ( a e. ( p ^m ( 0 ..^ 3 ) ) /\ b e. ( p ^m ( 0 ..^ 3 ) ) ) /\ E. x e. p E. y e. p ( a ( cgrG ` g ) <" x ( b ` 1 ) y "> /\ x ( k ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( k ` ( b ` 1 ) ) ( b ` 2 ) ) ) } )

Detailed syntax breakdown

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