Metamath Proof Explorer

Definition df-angmgm

Description: Definition of the angle addition magma. See following theorems for better readable properties. Because the textbook's definition of angle congruence does not consider orientation (cf. cgraswap ) , our notion of angle does not include reflex angles (angles larger than a straight angle). Therefore, like with NN0 , at this point, we can only build amagma , which is e.g.not isomorphic with the rotation group SO(2) . (Contributed by Thierry Arnoux, 20-Jul-2026)

Ref Expression
Assertion df-angmgm 
|- AngMgm = ( g e. _V |-> [_ ( Base ` g ) / p ]_ [_ { d e. ( p ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) } / a ]_ ( { <. ( Base ` ndx ) , a >. , <. ( +g ` ndx ) , ( e e. a , f e. a |-> if ( ( e ` 0 ) e. ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) , <" ( f ` 0 ) ( f ` 1 ) ( iota_ z e. p ( <" ( f ` 2 ) ( f ` 1 ) z "> ( cgrA ` g ) e /\ ( ( f ` 1 ) ( dist ` g ) z ) = ( ( e ` 1 ) ( dist ` g ) ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ z e. p ( <" ( e ` 2 ) ( e ` 1 ) z "> ( cgrA ` g ) f /\ ( ( e ` 1 ) ( dist ` g ) z ) = ( ( f ` 1 ) ( dist ` g ) ( f ` 0 ) ) /\ ( ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) i^i ( z ( Itv ` g ) ( e ` 0 ) ) ) =/= (/) ) ) "> ) ) >. , <. ( le ` ndx ) , ( leA ` g ) >. } /s ( cgrA ` g ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cangmgm 
 |-  AngMgm
1 vg 
 |-  g
2 cvv 
 |-  _V
3 cbs 
 |-  Base
4 1 cv 
 |-  g
5 4 3 cfv 
 |-  ( Base ` g )
6 vp 
 |-  p
7 vd 
 |-  d
8 6 cv 
 |-  p
9 cmap 
 |-  ^m
10 cc0 
 |-  0
11 cfzo 
 |-  ..^
12 c3 
 |-  3
13 10 12 11 co 
 |-  ( 0 ..^ 3 )
14 8 13 9 co 
 |-  ( p ^m ( 0 ..^ 3 ) )
15 7 cv 
 |-  d
16 10 15 cfv 
 |-  ( d ` 0 )
17 c1 
 |-  1
18 17 15 cfv 
 |-  ( d ` 1 )
19 16 18 wne 
 |-  ( d ` 0 ) =/= ( d ` 1 )
20 c2 
 |-  2
21 20 15 cfv 
 |-  ( d ` 2 )
22 18 21 wne 
 |-  ( d ` 1 ) =/= ( d ` 2 )
23 19 22 wa 
 |-  ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) )
24 23 7 14 crab 
 |-  { d e. ( p ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) }
25 va 
 |-  a
26 cnx 
 |-  ndx
27 26 3 cfv 
 |-  ( Base ` ndx )
28 25 cv 
 |-  a
29 27 28 cop 
 |-  <. ( Base ` ndx ) , a >.
30 cplusg 
 |-  +g
31 26 30 cfv 
 |-  ( +g ` ndx )
32 ve 
 |-  e
33 vf 
 |-  f
34 32 cv 
 |-  e
35 10 34 cfv 
 |-  ( e ` 0 )
36 17 34 cfv 
 |-  ( e ` 1 )
37 clng 
 |-  LineG
38 4 37 cfv 
 |-  ( LineG ` g )
39 20 34 cfv 
 |-  ( e ` 2 )
40 36 39 38 co 
 |-  ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) )
41 35 40 wcel 
 |-  ( e ` 0 ) e. ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) )
42 33 cv 
 |-  f
43 10 42 cfv 
 |-  ( f ` 0 )
44 17 42 cfv 
 |-  ( f ` 1 )
45 vz 
 |-  z
46 20 42 cfv 
 |-  ( f ` 2 )
47 45 cv 
 |-  z
48 46 44 47 cs3 
 |-  <" ( f ` 2 ) ( f ` 1 ) z ">
49 ccgra 
 |-  cgrA
50 4 49 cfv 
 |-  ( cgrA ` g )
51 48 34 50 wbr 
 |-  <" ( f ` 2 ) ( f ` 1 ) z "> ( cgrA ` g ) e
52 cds 
 |-  dist
53 4 52 cfv 
 |-  ( dist ` g )
54 44 47 53 co 
 |-  ( ( f ` 1 ) ( dist ` g ) z )
55 36 35 53 co 
 |-  ( ( e ` 1 ) ( dist ` g ) ( e ` 0 ) )
56 54 55 wceq 
 |-  ( ( f ` 1 ) ( dist ` g ) z ) = ( ( e ` 1 ) ( dist ` g ) ( e ` 0 ) )
57 51 56 wa 
 |-  ( <" ( f ` 2 ) ( f ` 1 ) z "> ( cgrA ` g ) e /\ ( ( f ` 1 ) ( dist ` g ) z ) = ( ( e ` 1 ) ( dist ` g ) ( e ` 0 ) ) )
58 57 45 8 crio 
 |-  ( iota_ z e. p ( <" ( f ` 2 ) ( f ` 1 ) z "> ( cgrA ` g ) e /\ ( ( f ` 1 ) ( dist ` g ) z ) = ( ( e ` 1 ) ( dist ` g ) ( e ` 0 ) ) ) )
59 43 44 58 cs3 
 |-  <" ( f ` 0 ) ( f ` 1 ) ( iota_ z e. p ( <" ( f ` 2 ) ( f ` 1 ) z "> ( cgrA ` g ) e /\ ( ( f ` 1 ) ( dist ` g ) z ) = ( ( e ` 1 ) ( dist ` g ) ( e ` 0 ) ) ) ) ">
60 39 36 47 cs3 
 |-  <" ( e ` 2 ) ( e ` 1 ) z ">
61 60 42 50 wbr 
 |-  <" ( e ` 2 ) ( e ` 1 ) z "> ( cgrA ` g ) f
62 36 47 53 co 
 |-  ( ( e ` 1 ) ( dist ` g ) z )
63 44 43 53 co 
 |-  ( ( f ` 1 ) ( dist ` g ) ( f ` 0 ) )
64 62 63 wceq 
 |-  ( ( e ` 1 ) ( dist ` g ) z ) = ( ( f ` 1 ) ( dist ` g ) ( f ` 0 ) )
65 citv 
 |-  Itv
66 4 65 cfv 
 |-  ( Itv ` g )
67 47 35 66 co 
 |-  ( z ( Itv ` g ) ( e ` 0 ) )
68 40 67 cin 
 |-  ( ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) i^i ( z ( Itv ` g ) ( e ` 0 ) ) )
69 c0 
 |-  (/)
70 68 69 wne 
 |-  ( ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) i^i ( z ( Itv ` g ) ( e ` 0 ) ) ) =/= (/)
71 61 64 70 w3a 
 |-  ( <" ( e ` 2 ) ( e ` 1 ) z "> ( cgrA ` g ) f /\ ( ( e ` 1 ) ( dist ` g ) z ) = ( ( f ` 1 ) ( dist ` g ) ( f ` 0 ) ) /\ ( ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) i^i ( z ( Itv ` g ) ( e ` 0 ) ) ) =/= (/) )
72 71 45 8 crio 
 |-  ( iota_ z e. p ( <" ( e ` 2 ) ( e ` 1 ) z "> ( cgrA ` g ) f /\ ( ( e ` 1 ) ( dist ` g ) z ) = ( ( f ` 1 ) ( dist ` g ) ( f ` 0 ) ) /\ ( ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) i^i ( z ( Itv ` g ) ( e ` 0 ) ) ) =/= (/) ) )
73 35 36 72 cs3 
 |-  <" ( e ` 0 ) ( e ` 1 ) ( iota_ z e. p ( <" ( e ` 2 ) ( e ` 1 ) z "> ( cgrA ` g ) f /\ ( ( e ` 1 ) ( dist ` g ) z ) = ( ( f ` 1 ) ( dist ` g ) ( f ` 0 ) ) /\ ( ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) i^i ( z ( Itv ` g ) ( e ` 0 ) ) ) =/= (/) ) ) ">
74 41 59 73 cif 
 |-  if ( ( e ` 0 ) e. ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) , <" ( f ` 0 ) ( f ` 1 ) ( iota_ z e. p ( <" ( f ` 2 ) ( f ` 1 ) z "> ( cgrA ` g ) e /\ ( ( f ` 1 ) ( dist ` g ) z ) = ( ( e ` 1 ) ( dist ` g ) ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ z e. p ( <" ( e ` 2 ) ( e ` 1 ) z "> ( cgrA ` g ) f /\ ( ( e ` 1 ) ( dist ` g ) z ) = ( ( f ` 1 ) ( dist ` g ) ( f ` 0 ) ) /\ ( ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) i^i ( z ( Itv ` g ) ( e ` 0 ) ) ) =/= (/) ) ) "> )
75 32 33 28 28 74 cmpo 
 |-  ( e e. a , f e. a |-> if ( ( e ` 0 ) e. ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) , <" ( f ` 0 ) ( f ` 1 ) ( iota_ z e. p ( <" ( f ` 2 ) ( f ` 1 ) z "> ( cgrA ` g ) e /\ ( ( f ` 1 ) ( dist ` g ) z ) = ( ( e ` 1 ) ( dist ` g ) ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ z e. p ( <" ( e ` 2 ) ( e ` 1 ) z "> ( cgrA ` g ) f /\ ( ( e ` 1 ) ( dist ` g ) z ) = ( ( f ` 1 ) ( dist ` g ) ( f ` 0 ) ) /\ ( ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) i^i ( z ( Itv ` g ) ( e ` 0 ) ) ) =/= (/) ) ) "> ) )
76 31 75 cop 
 |-  <. ( +g ` ndx ) , ( e e. a , f e. a |-> if ( ( e ` 0 ) e. ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) , <" ( f ` 0 ) ( f ` 1 ) ( iota_ z e. p ( <" ( f ` 2 ) ( f ` 1 ) z "> ( cgrA ` g ) e /\ ( ( f ` 1 ) ( dist ` g ) z ) = ( ( e ` 1 ) ( dist ` g ) ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ z e. p ( <" ( e ` 2 ) ( e ` 1 ) z "> ( cgrA ` g ) f /\ ( ( e ` 1 ) ( dist ` g ) z ) = ( ( f ` 1 ) ( dist ` g ) ( f ` 0 ) ) /\ ( ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) i^i ( z ( Itv ` g ) ( e ` 0 ) ) ) =/= (/) ) ) "> ) ) >.
77 cple 
 |-  le
78 26 77 cfv 
 |-  ( le ` ndx )
79 cleag 
 |-  leA
80 4 79 cfv 
 |-  ( leA ` g )
81 78 80 cop 
 |-  <. ( le ` ndx ) , ( leA ` g ) >.
82 29 76 81 ctp 
 |-  { <. ( Base ` ndx ) , a >. , <. ( +g ` ndx ) , ( e e. a , f e. a |-> if ( ( e ` 0 ) e. ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) , <" ( f ` 0 ) ( f ` 1 ) ( iota_ z e. p ( <" ( f ` 2 ) ( f ` 1 ) z "> ( cgrA ` g ) e /\ ( ( f ` 1 ) ( dist ` g ) z ) = ( ( e ` 1 ) ( dist ` g ) ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ z e. p ( <" ( e ` 2 ) ( e ` 1 ) z "> ( cgrA ` g ) f /\ ( ( e ` 1 ) ( dist ` g ) z ) = ( ( f ` 1 ) ( dist ` g ) ( f ` 0 ) ) /\ ( ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) i^i ( z ( Itv ` g ) ( e ` 0 ) ) ) =/= (/) ) ) "> ) ) >. , <. ( le ` ndx ) , ( leA ` g ) >. }
83 cqus 
 |-  /s
84 82 50 83 co 
 |-  ( { <. ( Base ` ndx ) , a >. , <. ( +g ` ndx ) , ( e e. a , f e. a |-> if ( ( e ` 0 ) e. ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) , <" ( f ` 0 ) ( f ` 1 ) ( iota_ z e. p ( <" ( f ` 2 ) ( f ` 1 ) z "> ( cgrA ` g ) e /\ ( ( f ` 1 ) ( dist ` g ) z ) = ( ( e ` 1 ) ( dist ` g ) ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ z e. p ( <" ( e ` 2 ) ( e ` 1 ) z "> ( cgrA ` g ) f /\ ( ( e ` 1 ) ( dist ` g ) z ) = ( ( f ` 1 ) ( dist ` g ) ( f ` 0 ) ) /\ ( ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) i^i ( z ( Itv ` g ) ( e ` 0 ) ) ) =/= (/) ) ) "> ) ) >. , <. ( le ` ndx ) , ( leA ` g ) >. } /s ( cgrA ` g ) )
85 25 24 84 csb 
 |-  [_ { d e. ( p ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) } / a ]_ ( { <. ( Base ` ndx ) , a >. , <. ( +g ` ndx ) , ( e e. a , f e. a |-> if ( ( e ` 0 ) e. ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) , <" ( f ` 0 ) ( f ` 1 ) ( iota_ z e. p ( <" ( f ` 2 ) ( f ` 1 ) z "> ( cgrA ` g ) e /\ ( ( f ` 1 ) ( dist ` g ) z ) = ( ( e ` 1 ) ( dist ` g ) ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ z e. p ( <" ( e ` 2 ) ( e ` 1 ) z "> ( cgrA ` g ) f /\ ( ( e ` 1 ) ( dist ` g ) z ) = ( ( f ` 1 ) ( dist ` g ) ( f ` 0 ) ) /\ ( ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) i^i ( z ( Itv ` g ) ( e ` 0 ) ) ) =/= (/) ) ) "> ) ) >. , <. ( le ` ndx ) , ( leA ` g ) >. } /s ( cgrA ` g ) )
86 6 5 85 csb 
 |-  [_ ( Base ` g ) / p ]_ [_ { d e. ( p ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) } / a ]_ ( { <. ( Base ` ndx ) , a >. , <. ( +g ` ndx ) , ( e e. a , f e. a |-> if ( ( e ` 0 ) e. ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) , <" ( f ` 0 ) ( f ` 1 ) ( iota_ z e. p ( <" ( f ` 2 ) ( f ` 1 ) z "> ( cgrA ` g ) e /\ ( ( f ` 1 ) ( dist ` g ) z ) = ( ( e ` 1 ) ( dist ` g ) ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ z e. p ( <" ( e ` 2 ) ( e ` 1 ) z "> ( cgrA ` g ) f /\ ( ( e ` 1 ) ( dist ` g ) z ) = ( ( f ` 1 ) ( dist ` g ) ( f ` 0 ) ) /\ ( ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) i^i ( z ( Itv ` g ) ( e ` 0 ) ) ) =/= (/) ) ) "> ) ) >. , <. ( le ` ndx ) , ( leA ` g ) >. } /s ( cgrA ` g ) )
87 1 2 86 cmpt 
 |-  ( g e. _V |-> [_ ( Base ` g ) / p ]_ [_ { d e. ( p ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) } / a ]_ ( { <. ( Base ` ndx ) , a >. , <. ( +g ` ndx ) , ( e e. a , f e. a |-> if ( ( e ` 0 ) e. ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) , <" ( f ` 0 ) ( f ` 1 ) ( iota_ z e. p ( <" ( f ` 2 ) ( f ` 1 ) z "> ( cgrA ` g ) e /\ ( ( f ` 1 ) ( dist ` g ) z ) = ( ( e ` 1 ) ( dist ` g ) ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ z e. p ( <" ( e ` 2 ) ( e ` 1 ) z "> ( cgrA ` g ) f /\ ( ( e ` 1 ) ( dist ` g ) z ) = ( ( f ` 1 ) ( dist ` g ) ( f ` 0 ) ) /\ ( ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) i^i ( z ( Itv ` g ) ( e ` 0 ) ) ) =/= (/) ) ) "> ) ) >. , <. ( le ` ndx ) , ( leA ` g ) >. } /s ( cgrA ` g ) ) )
88 0 87 wceq 
 |-  AngMgm = ( g e. _V |-> [_ ( Base ` g ) / p ]_ [_ { d e. ( p ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) } / a ]_ ( { <. ( Base ` ndx ) , a >. , <. ( +g ` ndx ) , ( e e. a , f e. a |-> if ( ( e ` 0 ) e. ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) , <" ( f ` 0 ) ( f ` 1 ) ( iota_ z e. p ( <" ( f ` 2 ) ( f ` 1 ) z "> ( cgrA ` g ) e /\ ( ( f ` 1 ) ( dist ` g ) z ) = ( ( e ` 1 ) ( dist ` g ) ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ z e. p ( <" ( e ` 2 ) ( e ` 1 ) z "> ( cgrA ` g ) f /\ ( ( e ` 1 ) ( dist ` g ) z ) = ( ( f ` 1 ) ( dist ` g ) ( f ` 0 ) ) /\ ( ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) i^i ( z ( Itv ` g ) ( e ` 0 ) ) ) =/= (/) ) ) "> ) ) >. , <. ( le ` ndx ) , ( leA ` g ) >. } /s ( cgrA ` g ) ) )