Definition df-angmgm 29254

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 29207) , our notion of angle does not include reflex angles (angles larger than a straight angle). Therefore, like with ℕ₀, at this point, we can only build a magma , which is e.g. not isomorphic with the rotation group SO(2) . (Contributed by Thierry Arnoux, 20-Jul-2026.)

Assertion

Ref

Expression

df-angmgm

⊢ AngMgm = (𝑔 ∈ V ↦ ⦋(Base‘𝑔) / 𝑝⦌⦋{𝑑 ∈ (𝑝 ↑m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))} / 𝑎⦌({⟨(Base‘ndx), 𝑎⟩, ⟨(+g‘ndx), (𝑒 ∈ 𝑎, 𝑓 ∈ 𝑎 ↦ if((𝑒‘0) ∈ ((𝑒‘1)(LineG‘𝑔)(𝑒‘2)), ⟨“(𝑓‘0)(𝑓‘1)(℩𝑧 ∈ 𝑝 (⟨“(𝑓‘2)(𝑓‘1)𝑧”⟩(cgrA‘𝑔)𝑒 ∧ ((𝑓‘1)(dist‘𝑔)𝑧) = ((𝑒‘1)(dist‘𝑔)(𝑒‘0))))”⟩, ⟨“(𝑒‘0)(𝑒‘1)(℩𝑧 ∈ 𝑝 (⟨“(𝑒‘2)(𝑒‘1)𝑧”⟩(cgrA‘𝑔)𝑓 ∧ ((𝑒‘1)(dist‘𝑔)𝑧) = ((𝑓‘1)(dist‘𝑔)(𝑓‘0)) ∧ (((𝑒‘1)(LineG‘𝑔)(𝑒‘2)) ∩ (𝑧(Itv‘𝑔)(𝑒‘0))) ≠ ∅))”⟩))⟩, ⟨(le‘ndx), (≤∠‘𝑔)⟩} /s (cgrA‘𝑔)))

Distinct variable group:   𝑔,𝑝,𝑑,𝑎,𝑒,𝑓,𝑧

Detailed syntax breakdown of Definition df-angmgm

Step	Hyp	Ref	Expression
1		cangmgm 29253	. 2 class AngMgm
2		vg	. . 3 setvar 𝑔
3		cvv 3453	. . 3 class V
4		vp	. . . 4 setvar 𝑝
5	2	cv 1569	. . . . 5 class 𝑔
6		cbs 17305	. . . . 5 class Base
7	5, 6	cfv 6537	. . . 4 class (Base‘𝑔)
8		va	. . . . 5 setvar 𝑎
9		cc0 11127	. . . . . . . . 9 class 0
10		vd	. . . . . . . . . 10 setvar 𝑑
11	10	cv 1569	. . . . . . . . 9 class 𝑑
12	9, 11	cfv 6537	. . . . . . . 8 class (𝑑‘0)
13		c1 11128	. . . . . . . . 9 class 1
14	13, 11	cfv 6537	. . . . . . . 8 class (𝑑‘1)
15	12, 14	wne 2957	. . . . . . 7 wff (𝑑‘0) ≠ (𝑑‘1)
16		c2 12322	. . . . . . . . 9 class 2
17	16, 11	cfv 6537	. . . . . . . 8 class (𝑑‘2)
18	14, 17	wne 2957	. . . . . . 7 wff (𝑑‘1) ≠ (𝑑‘2)
19	15, 18	wa 401	. . . . . 6 wff ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))
20	4	cv 1569	. . . . . . 7 class 𝑝
21		c3 12323	. . . . . . . 8 class 3
22		cfzo 13711	. . . . . . . 8 class ..^
23	9, 21, 22	co 7416	. . . . . . 7 class (0..^3)
24		cmap 8829	. . . . . . 7 class ↑m
25	20, 23, 24	co 7416	. . . . . 6 class (𝑝 ↑m (0..^3))
26	19, 10, 25	crab 3414	. . . . 5 class {𝑑 ∈ (𝑝 ↑m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))}
27		cnx 17289	. . . . . . . . 9 class ndx
28	27, 6	cfv 6537	. . . . . . . 8 class (Base‘ndx)
29	8	cv 1569	. . . . . . . 8 class 𝑎
30	28, 29	cop 4593	. . . . . . 7 class ⟨(Base‘ndx), 𝑎⟩
31		cplusg 17346	. . . . . . . . 9 class +g
32	27, 31	cfv 6537	. . . . . . . 8 class (+g‘ndx)
33		ve	. . . . . . . . 9 setvar 𝑒
34		vf	. . . . . . . . 9 setvar 𝑓
35	33	cv 1569	. . . . . . . . . . . 12 class 𝑒
36	9, 35	cfv 6537	. . . . . . . . . . 11 class (𝑒‘0)
37	13, 35	cfv 6537	. . . . . . . . . . . 12 class (𝑒‘1)
38	16, 35	cfv 6537	. . . . . . . . . . . 12 class (𝑒‘2)
39		clng 28776	. . . . . . . . . . . . 13 class LineG
40	5, 39	cfv 6537	. . . . . . . . . . . 12 class (LineG‘𝑔)
41	37, 38, 40	co 7416	. . . . . . . . . . 11 class ((𝑒‘1)(LineG‘𝑔)(𝑒‘2))
42	36, 41	wcel 2145	. . . . . . . . . 10 wff (𝑒‘0) ∈ ((𝑒‘1)(LineG‘𝑔)(𝑒‘2))
43	34	cv 1569	. . . . . . . . . . . 12 class 𝑓
44	9, 43	cfv 6537	. . . . . . . . . . 11 class (𝑓‘0)
45	13, 43	cfv 6537	. . . . . . . . . . 11 class (𝑓‘1)
46	16, 43	cfv 6537	. . . . . . . . . . . . . . 15 class (𝑓‘2)
47		vz	. . . . . . . . . . . . . . . 16 setvar 𝑧
48	47	cv 1569	. . . . . . . . . . . . . . 15 class 𝑧
49	46, 45, 48	cs3 14915	. . . . . . . . . . . . . 14 class ⟨“(𝑓‘2)(𝑓‘1)𝑧”⟩
50		ccgra 29194	. . . . . . . . . . . . . . 15 class cgrA
51	5, 50	cfv 6537	. . . . . . . . . . . . . 14 class (cgrA‘𝑔)
52	49, 35, 51	wbr 5107	. . . . . . . . . . . . 13 wff ⟨“(𝑓‘2)(𝑓‘1)𝑧”⟩(cgrA‘𝑔)𝑒
53		cds 17355	. . . . . . . . . . . . . . . 16 class dist
54	5, 53	cfv 6537	. . . . . . . . . . . . . . 15 class (dist‘𝑔)
55	45, 48, 54	co 7416	. . . . . . . . . . . . . 14 class ((𝑓‘1)(dist‘𝑔)𝑧)
56	37, 36, 54	co 7416	. . . . . . . . . . . . . 14 class ((𝑒‘1)(dist‘𝑔)(𝑒‘0))
57	55, 56	wceq 1570	. . . . . . . . . . . . 13 wff ((𝑓‘1)(dist‘𝑔)𝑧) = ((𝑒‘1)(dist‘𝑔)(𝑒‘0))
58	52, 57	wa 401	. . . . . . . . . . . 12 wff (⟨“(𝑓‘2)(𝑓‘1)𝑧”⟩(cgrA‘𝑔)𝑒 ∧ ((𝑓‘1)(dist‘𝑔)𝑧) = ((𝑒‘1)(dist‘𝑔)(𝑒‘0)))
59	58, 47, 20	crio 7372	. . . . . . . . . . 11 class (℩𝑧 ∈ 𝑝 (⟨“(𝑓‘2)(𝑓‘1)𝑧”⟩(cgrA‘𝑔)𝑒 ∧ ((𝑓‘1)(dist‘𝑔)𝑧) = ((𝑒‘1)(dist‘𝑔)(𝑒‘0))))
60	44, 45, 59	cs3 14915	. . . . . . . . . 10 class ⟨“(𝑓‘0)(𝑓‘1)(℩𝑧 ∈ 𝑝 (⟨“(𝑓‘2)(𝑓‘1)𝑧”⟩(cgrA‘𝑔)𝑒 ∧ ((𝑓‘1)(dist‘𝑔)𝑧) = ((𝑒‘1)(dist‘𝑔)(𝑒‘0))))”⟩
61	38, 37, 48	cs3 14915	. . . . . . . . . . . . . 14 class ⟨“(𝑒‘2)(𝑒‘1)𝑧”⟩
62	61, 43, 51	wbr 5107	. . . . . . . . . . . . 13 wff ⟨“(𝑒‘2)(𝑒‘1)𝑧”⟩(cgrA‘𝑔)𝑓
63	37, 48, 54	co 7416	. . . . . . . . . . . . . 14 class ((𝑒‘1)(dist‘𝑔)𝑧)
64	45, 44, 54	co 7416	. . . . . . . . . . . . . 14 class ((𝑓‘1)(dist‘𝑔)(𝑓‘0))
65	63, 64	wceq 1570	. . . . . . . . . . . . 13 wff ((𝑒‘1)(dist‘𝑔)𝑧) = ((𝑓‘1)(dist‘𝑔)(𝑓‘0))
66		citv 28775	. . . . . . . . . . . . . . . . 17 class Itv
67	5, 66	cfv 6537	. . . . . . . . . . . . . . . 16 class (Itv‘𝑔)
68	48, 36, 67	co 7416	. . . . . . . . . . . . . . 15 class (𝑧(Itv‘𝑔)(𝑒‘0))
69	41, 68	cin 3901	. . . . . . . . . . . . . 14 class (((𝑒‘1)(LineG‘𝑔)(𝑒‘2)) ∩ (𝑧(Itv‘𝑔)(𝑒‘0)))
70		c0 4282	. . . . . . . . . . . . . 14 class ∅
71	69, 70	wne 2957	. . . . . . . . . . . . 13 wff (((𝑒‘1)(LineG‘𝑔)(𝑒‘2)) ∩ (𝑧(Itv‘𝑔)(𝑒‘0))) ≠ ∅
72	62, 65, 71	w3a 1103	. . . . . . . . . . . 12 wff (⟨“(𝑒‘2)(𝑒‘1)𝑧”⟩(cgrA‘𝑔)𝑓 ∧ ((𝑒‘1)(dist‘𝑔)𝑧) = ((𝑓‘1)(dist‘𝑔)(𝑓‘0)) ∧ (((𝑒‘1)(LineG‘𝑔)(𝑒‘2)) ∩ (𝑧(Itv‘𝑔)(𝑒‘0))) ≠ ∅)
73	72, 47, 20	crio 7372	. . . . . . . . . . 11 class (℩𝑧 ∈ 𝑝 (⟨“(𝑒‘2)(𝑒‘1)𝑧”⟩(cgrA‘𝑔)𝑓 ∧ ((𝑒‘1)(dist‘𝑔)𝑧) = ((𝑓‘1)(dist‘𝑔)(𝑓‘0)) ∧ (((𝑒‘1)(LineG‘𝑔)(𝑒‘2)) ∩ (𝑧(Itv‘𝑔)(𝑒‘0))) ≠ ∅))
74	36, 37, 73	cs3 14915	. . . . . . . . . 10 class ⟨“(𝑒‘0)(𝑒‘1)(℩𝑧 ∈ 𝑝 (⟨“(𝑒‘2)(𝑒‘1)𝑧”⟩(cgrA‘𝑔)𝑓 ∧ ((𝑒‘1)(dist‘𝑔)𝑧) = ((𝑓‘1)(dist‘𝑔)(𝑓‘0)) ∧ (((𝑒‘1)(LineG‘𝑔)(𝑒‘2)) ∩ (𝑧(Itv‘𝑔)(𝑒‘0))) ≠ ∅))”⟩
75	42, 60, 74	cif 4485	. . . . . . . . 9 class if((𝑒‘0) ∈ ((𝑒‘1)(LineG‘𝑔)(𝑒‘2)), ⟨“(𝑓‘0)(𝑓‘1)(℩𝑧 ∈ 𝑝 (⟨“(𝑓‘2)(𝑓‘1)𝑧”⟩(cgrA‘𝑔)𝑒 ∧ ((𝑓‘1)(dist‘𝑔)𝑧) = ((𝑒‘1)(dist‘𝑔)(𝑒‘0))))”⟩, ⟨“(𝑒‘0)(𝑒‘1)(℩𝑧 ∈ 𝑝 (⟨“(𝑒‘2)(𝑒‘1)𝑧”⟩(cgrA‘𝑔)𝑓 ∧ ((𝑒‘1)(dist‘𝑔)𝑧) = ((𝑓‘1)(dist‘𝑔)(𝑓‘0)) ∧ (((𝑒‘1)(LineG‘𝑔)(𝑒‘2)) ∩ (𝑧(Itv‘𝑔)(𝑒‘0))) ≠ ∅))”⟩)
76	33, 34, 29, 29, 75	cmpo 7418	. . . . . . . 8 class (𝑒 ∈ 𝑎, 𝑓 ∈ 𝑎 ↦ if((𝑒‘0) ∈ ((𝑒‘1)(LineG‘𝑔)(𝑒‘2)), ⟨“(𝑓‘0)(𝑓‘1)(℩𝑧 ∈ 𝑝 (⟨“(𝑓‘2)(𝑓‘1)𝑧”⟩(cgrA‘𝑔)𝑒 ∧ ((𝑓‘1)(dist‘𝑔)𝑧) = ((𝑒‘1)(dist‘𝑔)(𝑒‘0))))”⟩, ⟨“(𝑒‘0)(𝑒‘1)(℩𝑧 ∈ 𝑝 (⟨“(𝑒‘2)(𝑒‘1)𝑧”⟩(cgrA‘𝑔)𝑓 ∧ ((𝑒‘1)(dist‘𝑔)𝑧) = ((𝑓‘1)(dist‘𝑔)(𝑓‘0)) ∧ (((𝑒‘1)(LineG‘𝑔)(𝑒‘2)) ∩ (𝑧(Itv‘𝑔)(𝑒‘0))) ≠ ∅))”⟩))
77	32, 76	cop 4593	. . . . . . 7 class ⟨(+g‘ndx), (𝑒 ∈ 𝑎, 𝑓 ∈ 𝑎 ↦ if((𝑒‘0) ∈ ((𝑒‘1)(LineG‘𝑔)(𝑒‘2)), ⟨“(𝑓‘0)(𝑓‘1)(℩𝑧 ∈ 𝑝 (⟨“(𝑓‘2)(𝑓‘1)𝑧”⟩(cgrA‘𝑔)𝑒 ∧ ((𝑓‘1)(dist‘𝑔)𝑧) = ((𝑒‘1)(dist‘𝑔)(𝑒‘0))))”⟩, ⟨“(𝑒‘0)(𝑒‘1)(℩𝑧 ∈ 𝑝 (⟨“(𝑒‘2)(𝑒‘1)𝑧”⟩(cgrA‘𝑔)𝑓 ∧ ((𝑒‘1)(dist‘𝑔)𝑧) = ((𝑓‘1)(dist‘𝑔)(𝑓‘0)) ∧ (((𝑒‘1)(LineG‘𝑔)(𝑒‘2)) ∩ (𝑧(Itv‘𝑔)(𝑒‘0))) ≠ ∅))”⟩))⟩
78		cple 17353	. . . . . . . . 9 class le
79	27, 78	cfv 6537	. . . . . . . 8 class (le‘ndx)
80		cleag 29235	. . . . . . . . 9 class ≤∠
81	5, 80	cfv 6537	. . . . . . . 8 class (≤∠‘𝑔)
82	79, 81	cop 4593	. . . . . . 7 class ⟨(le‘ndx), (≤∠‘𝑔)⟩
83	30, 77, 82	ctp 4591	. . . . . 6 class {⟨(Base‘ndx), 𝑎⟩, ⟨(+g‘ndx), (𝑒 ∈ 𝑎, 𝑓 ∈ 𝑎 ↦ if((𝑒‘0) ∈ ((𝑒‘1)(LineG‘𝑔)(𝑒‘2)), ⟨“(𝑓‘0)(𝑓‘1)(℩𝑧 ∈ 𝑝 (⟨“(𝑓‘2)(𝑓‘1)𝑧”⟩(cgrA‘𝑔)𝑒 ∧ ((𝑓‘1)(dist‘𝑔)𝑧) = ((𝑒‘1)(dist‘𝑔)(𝑒‘0))))”⟩, ⟨“(𝑒‘0)(𝑒‘1)(℩𝑧 ∈ 𝑝 (⟨“(𝑒‘2)(𝑒‘1)𝑧”⟩(cgrA‘𝑔)𝑓 ∧ ((𝑒‘1)(dist‘𝑔)𝑧) = ((𝑓‘1)(dist‘𝑔)(𝑓‘0)) ∧ (((𝑒‘1)(LineG‘𝑔)(𝑒‘2)) ∩ (𝑧(Itv‘𝑔)(𝑒‘0))) ≠ ∅))”⟩))⟩, ⟨(le‘ndx), (≤∠‘𝑔)⟩}
84		cqus 17595	. . . . . 6 class /s
85	83, 51, 84	co 7416	. . . . 5 class ({⟨(Base‘ndx), 𝑎⟩, ⟨(+g‘ndx), (𝑒 ∈ 𝑎, 𝑓 ∈ 𝑎 ↦ if((𝑒‘0) ∈ ((𝑒‘1)(LineG‘𝑔)(𝑒‘2)), ⟨“(𝑓‘0)(𝑓‘1)(℩𝑧 ∈ 𝑝 (⟨“(𝑓‘2)(𝑓‘1)𝑧”⟩(cgrA‘𝑔)𝑒 ∧ ((𝑓‘1)(dist‘𝑔)𝑧) = ((𝑒‘1)(dist‘𝑔)(𝑒‘0))))”⟩, ⟨“(𝑒‘0)(𝑒‘1)(℩𝑧 ∈ 𝑝 (⟨“(𝑒‘2)(𝑒‘1)𝑧”⟩(cgrA‘𝑔)𝑓 ∧ ((𝑒‘1)(dist‘𝑔)𝑧) = ((𝑓‘1)(dist‘𝑔)(𝑓‘0)) ∧ (((𝑒‘1)(LineG‘𝑔)(𝑒‘2)) ∩ (𝑧(Itv‘𝑔)(𝑒‘0))) ≠ ∅))”⟩))⟩, ⟨(le‘ndx), (≤∠‘𝑔)⟩} /s (cgrA‘𝑔))
86	8, 26, 85	csb 3850	. . . 4 class ⦋{𝑑 ∈ (𝑝 ↑m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))} / 𝑎⦌({⟨(Base‘ndx), 𝑎⟩, ⟨(+g‘ndx), (𝑒 ∈ 𝑎, 𝑓 ∈ 𝑎 ↦ if((𝑒‘0) ∈ ((𝑒‘1)(LineG‘𝑔)(𝑒‘2)), ⟨“(𝑓‘0)(𝑓‘1)(℩𝑧 ∈ 𝑝 (⟨“(𝑓‘2)(𝑓‘1)𝑧”⟩(cgrA‘𝑔)𝑒 ∧ ((𝑓‘1)(dist‘𝑔)𝑧) = ((𝑒‘1)(dist‘𝑔)(𝑒‘0))))”⟩, ⟨“(𝑒‘0)(𝑒‘1)(℩𝑧 ∈ 𝑝 (⟨“(𝑒‘2)(𝑒‘1)𝑧”⟩(cgrA‘𝑔)𝑓 ∧ ((𝑒‘1)(dist‘𝑔)𝑧) = ((𝑓‘1)(dist‘𝑔)(𝑓‘0)) ∧ (((𝑒‘1)(LineG‘𝑔)(𝑒‘2)) ∩ (𝑧(Itv‘𝑔)(𝑒‘0))) ≠ ∅))”⟩))⟩, ⟨(le‘ndx), (≤∠‘𝑔)⟩} /s (cgrA‘𝑔))
87	4, 7, 86	csb 3850	. . 3 class ⦋(Base‘𝑔) / 𝑝⦌⦋{𝑑 ∈ (𝑝 ↑m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))} / 𝑎⦌({⟨(Base‘ndx), 𝑎⟩, ⟨(+g‘ndx), (𝑒 ∈ 𝑎, 𝑓 ∈ 𝑎 ↦ if((𝑒‘0) ∈ ((𝑒‘1)(LineG‘𝑔)(𝑒‘2)), ⟨“(𝑓‘0)(𝑓‘1)(℩𝑧 ∈ 𝑝 (⟨“(𝑓‘2)(𝑓‘1)𝑧”⟩(cgrA‘𝑔)𝑒 ∧ ((𝑓‘1)(dist‘𝑔)𝑧) = ((𝑒‘1)(dist‘𝑔)(𝑒‘0))))”⟩, ⟨“(𝑒‘0)(𝑒‘1)(℩𝑧 ∈ 𝑝 (⟨“(𝑒‘2)(𝑒‘1)𝑧”⟩(cgrA‘𝑔)𝑓 ∧ ((𝑒‘1)(dist‘𝑔)𝑧) = ((𝑓‘1)(dist‘𝑔)(𝑓‘0)) ∧ (((𝑒‘1)(LineG‘𝑔)(𝑒‘2)) ∩ (𝑧(Itv‘𝑔)(𝑒‘0))) ≠ ∅))”⟩))⟩, ⟨(le‘ndx), (≤∠‘𝑔)⟩} /s (cgrA‘𝑔))
88	2, 3, 87	cmpt 5190	. 2 class (𝑔 ∈ V ↦ ⦋(Base‘𝑔) / 𝑝⦌⦋{𝑑 ∈ (𝑝 ↑m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))} / 𝑎⦌({⟨(Base‘ndx), 𝑎⟩, ⟨(+g‘ndx), (𝑒 ∈ 𝑎, 𝑓 ∈ 𝑎 ↦ if((𝑒‘0) ∈ ((𝑒‘1)(LineG‘𝑔)(𝑒‘2)), ⟨“(𝑓‘0)(𝑓‘1)(℩𝑧 ∈ 𝑝 (⟨“(𝑓‘2)(𝑓‘1)𝑧”⟩(cgrA‘𝑔)𝑒 ∧ ((𝑓‘1)(dist‘𝑔)𝑧) = ((𝑒‘1)(dist‘𝑔)(𝑒‘0))))”⟩, ⟨“(𝑒‘0)(𝑒‘1)(℩𝑧 ∈ 𝑝 (⟨“(𝑒‘2)(𝑒‘1)𝑧”⟩(cgrA‘𝑔)𝑓 ∧ ((𝑒‘1)(dist‘𝑔)𝑧) = ((𝑓‘1)(dist‘𝑔)(𝑓‘0)) ∧ (((𝑒‘1)(LineG‘𝑔)(𝑒‘2)) ∩ (𝑧(Itv‘𝑔)(𝑒‘0))) ≠ ∅))”⟩))⟩, ⟨(le‘ndx), (≤∠‘𝑔)⟩} /s (cgrA‘𝑔)))
89	1, 88	wceq 1570	1 wff AngMgm = (𝑔 ∈ V ↦ ⦋(Base‘𝑔) / 𝑝⦌⦋{𝑑 ∈ (𝑝 ↑m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))} / 𝑎⦌({⟨(Base‘ndx), 𝑎⟩, ⟨(+g‘ndx), (𝑒 ∈ 𝑎, 𝑓 ∈ 𝑎 ↦ if((𝑒‘0) ∈ ((𝑒‘1)(LineG‘𝑔)(𝑒‘2)), ⟨“(𝑓‘0)(𝑓‘1)(℩𝑧 ∈ 𝑝 (⟨“(𝑓‘2)(𝑓‘1)𝑧”⟩(cgrA‘𝑔)𝑒 ∧ ((𝑓‘1)(dist‘𝑔)𝑧) = ((𝑒‘1)(dist‘𝑔)(𝑒‘0))))”⟩, ⟨“(𝑒‘0)(𝑒‘1)(℩𝑧 ∈ 𝑝 (⟨“(𝑒‘2)(𝑒‘1)𝑧”⟩(cgrA‘𝑔)𝑓 ∧ ((𝑒‘1)(dist‘𝑔)𝑧) = ((𝑓‘1)(dist‘𝑔)(𝑓‘0)) ∧ (((𝑒‘1)(LineG‘𝑔)(𝑒‘2)) ∩ (𝑧(Itv‘𝑔)(𝑒‘0))) ≠ ∅))”⟩))⟩, ⟨(le‘ndx), (≤∠‘𝑔)⟩} /s (cgrA‘𝑔)))

This definition is used by:  angmgmval  29274