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	Could not format assertion : No typesetting found for \|- 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 ) ) ) with typecode \|-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cangmgm	Could not format AngMgm : No typesetting found for class AngMgm with typecode class
1		vg	$setvar g$
2		cvv	$class V$
3		cbs	$class Base$
4	1	cv	$setvar g$
5	4 3	cfv	$class {Base}_{g}$
6		vp	$setvar p$
7		vd	$setvar d$
8	6	cv	$setvar p$
9		cmap	$class ↑_{𝑚}$
10		cc0	$class 0$
11		cfzo	$class ..^$
12		c3	$class 3$
13	10 12 11	co	$class (0 ..^3)$
14	8 13 9	co	$class (p^{(0 ..^3)})$
15	7	cv	$setvar d$
16	10 15	cfv	$class d (0)$
17		c1	$class 1$
18	17 15	cfv	$class d (1)$
19	16 18	wne	$wff d (0) \neq d (1)$
20		c2	$class 2$
21	20 15	cfv	$class d (2)$
22	18 21	wne	$wff d (1) \neq d (2)$
23	19 22	wa	$wff (d (0) \neq d (1) \land d (1) \neq d (2))$
24	23 7 14	crab	$class \{d \in (p^{(0 ..^3)}) \| (d (0) \neq d (1) \land d (1) \neq d (2))\}$
25		va	$setvar a$
26		cnx	$class ndx$
27	26 3	cfv	$class {Base}_{ndx}$
28	25	cv	$setvar a$
29	27 28	cop	$class ⟨{Base}_{ndx}, a⟩$
30		cplusg	$class +_{𝑔}$
31	26 30	cfv	$class +_{ndx}$
32		ve	$setvar e$
33		vf	$setvar f$
34	32	cv	$setvar e$
35	10 34	cfv	$class e (0)$
36	17 34	cfv	$class e (1)$
37		clng	$class {Line}_{𝒢}$
38	4 37	cfv	$class {Line}_{𝒢} (g)$
39	20 34	cfv	$class e (2)$
40	36 39 38	co	$class (e (1) {Line}_{𝒢} (g) e (2))$
41	35 40	wcel	$wff e (0) \in (e (1) {Line}_{𝒢} (g) e (2))$
42	33	cv	$setvar f$
43	10 42	cfv	$class f (0)$
44	17 42	cfv	$class f (1)$
45		vz	$setvar z$
46	20 42	cfv	$class f (2)$
47	45	cv	$setvar z$
48	46 44 47	cs3	$class ⟨“ f (2) f (1) z ”⟩$
49		ccgra	$class \sim_{𝒢}^{∠}$
50	4 49	cfv	$class \sim_{𝒢}^{∠} (g)$
51	48 34 50	wbr	$wff ⟨“ f (2) f (1) z ”⟩ \sim_{𝒢}^{∠} (g) e$
52		cds	$class dist$
53	4 52	cfv	$class dist (g)$
54	44 47 53	co	$class (f (1) dist (g) z)$
55	36 35 53	co	$class (e (1) dist (g) e (0))$
56	54 55	wceq	$wff f (1) dist (g) z = e (1) dist (g) e (0)$
57	51 56	wa	$wff (⟨“ f (2) f (1) z ”⟩ \sim_{𝒢}^{∠} (g) e \land f (1) dist (g) z = e (1) dist (g) e (0))$
58	57 45 8	crio	$class (ι z \in p \| (⟨“ f (2) f (1) z ”⟩ \sim_{𝒢}^{∠} (g) e \land f (1) dist (g) z = e (1) dist (g) e (0)))$
59	43 44 58	cs3	$class ⟨“ f (0) f (1) (ι z \in p \| (⟨“ f (2) f (1) z ”⟩ \sim_{𝒢}^{∠} (g) e \land f (1) dist (g) z = e (1) dist (g) e (0))) ”⟩$
60	39 36 47	cs3	$class ⟨“ e (2) e (1) z ”⟩$
61	60 42 50	wbr	$wff ⟨“ e (2) e (1) z ”⟩ \sim_{𝒢}^{∠} (g) f$
62	36 47 53	co	$class (e (1) dist (g) z)$
63	44 43 53	co	$class (f (1) dist (g) f (0))$
64	62 63	wceq	$wff e (1) dist (g) z = f (1) dist (g) f (0)$
65		citv	$class Itv$
66	4 65	cfv	$class Itv (g)$
67	47 35 66	co	$class (z Itv (g) e (0))$
68	40 67	cin	$class ((e (1) {Line}_{𝒢} (g) e (2)) \cap (z Itv (g) e (0)))$
69		c0	$class \emptyset$
70	68 69	wne	$wff (e (1) {Line}_{𝒢} (g) e (2)) \cap (z Itv (g) e (0)) \neq \emptyset$
71	61 64 70	w3a	$wff (⟨“ e (2) e (1) z ”⟩ \sim_{𝒢}^{∠} (g) f \land e (1) dist (g) z = f (1) dist (g) f (0) \land (e (1) {Line}_{𝒢} (g) e (2)) \cap (z Itv (g) e (0)) \neq \emptyset)$
72	71 45 8	crio	$class (ι z \in p \| (⟨“ e (2) e (1) z ”⟩ \sim_{𝒢}^{∠} (g) f \land e (1) dist (g) z = f (1) dist (g) f (0) \land (e (1) {Line}_{𝒢} (g) e (2)) \cap (z Itv (g) e (0)) \neq \emptyset))$
73	35 36 72	cs3	$class ⟨“ e (0) e (1) (ι z \in p \| (⟨“ e (2) e (1) z ”⟩ \sim_{𝒢}^{∠} (g) f \land e (1) dist (g) z = f (1) dist (g) f (0) \land (e (1) {Line}_{𝒢} (g) e (2)) \cap (z Itv (g) e (0)) \neq \emptyset)) ”⟩$
74	41 59 73	cif	$class if (e (0) \in (e (1) {Line}_{𝒢} (g) e (2)), ⟨“ f (0) f (1) (ι z \in p \| (⟨“ f (2) f (1) z ”⟩ \sim_{𝒢}^{∠} (g) e \land f (1) dist (g) z = e (1) dist (g) e (0))) ”⟩, ⟨“ e (0) e (1) (ι z \in p \| (⟨“ e (2) e (1) z ”⟩ \sim_{𝒢}^{∠} (g) f \land e (1) dist (g) z = f (1) dist (g) f (0) \land (e (1) {Line}_{𝒢} (g) e (2)) \cap (z Itv (g) e (0)) \neq \emptyset)) ”⟩)$
75	32 33 28 28 74	cmpo	$class (e \in a, f \in a ⟼ if (e (0) \in (e (1) {Line}_{𝒢} (g) e (2)), ⟨“ f (0) f (1) (ι z \in p \| (⟨“ f (2) f (1) z ”⟩ \sim_{𝒢}^{∠} (g) e \land f (1) dist (g) z = e (1) dist (g) e (0))) ”⟩, ⟨“ e (0) e (1) (ι z \in p \| (⟨“ e (2) e (1) z ”⟩ \sim_{𝒢}^{∠} (g) f \land e (1) dist (g) z = f (1) dist (g) f (0) \land (e (1) {Line}_{𝒢} (g) e (2)) \cap (z Itv (g) e (0)) \neq \emptyset)) ”⟩))$
76	31 75	cop	$class ⟨+_{ndx}, (e \in a, f \in a ⟼ if (e (0) \in (e (1) {Line}_{𝒢} (g) e (2)), ⟨“ f (0) f (1) (ι z \in p \| (⟨“ f (2) f (1) z ”⟩ \sim_{𝒢}^{∠} (g) e \land f (1) dist (g) z = e (1) dist (g) e (0))) ”⟩, ⟨“ e (0) e (1) (ι z \in p \| (⟨“ e (2) e (1) z ”⟩ \sim_{𝒢}^{∠} (g) f \land e (1) dist (g) z = f (1) dist (g) f (0) \land (e (1) {Line}_{𝒢} (g) e (2)) \cap (z Itv (g) e (0)) \neq \emptyset)) ”⟩))⟩$
77		cple	$class le$
78	26 77	cfv	$class \leq_{ndx}$
79		cleag	$class \leq_{𝒢}^{∠}$
80	4 79	cfv	$class \leq_{𝒢}^{∠} (g)$
81	78 80	cop	$class ⟨\leq_{ndx}, \leq_{𝒢}^{∠} (g)⟩$
82	29 76 81	ctp	$class \{⟨{Base}_{ndx}, a⟩, ⟨+_{ndx}, (e \in a, f \in a ⟼ if (e (0) \in (e (1) {Line}_{𝒢} (g) e (2)), ⟨“ f (0) f (1) (ι z \in p \| (⟨“ f (2) f (1) z ”⟩ \sim_{𝒢}^{∠} (g) e \land f (1) dist (g) z = e (1) dist (g) e (0))) ”⟩, ⟨“ e (0) e (1) (ι z \in p \| (⟨“ e (2) e (1) z ”⟩ \sim_{𝒢}^{∠} (g) f \land e (1) dist (g) z = f (1) dist (g) f (0) \land (e (1) {Line}_{𝒢} (g) e (2)) \cap (z Itv (g) e (0)) \neq \emptyset)) ”⟩))⟩, ⟨\leq_{ndx}, \leq_{𝒢}^{∠} (g)⟩\}$
83		cqus	$class /_{𝑠}$
84	82 50 83	co	$class (\{⟨{Base}_{ndx}, a⟩, ⟨+_{ndx}, (e \in a, f \in a ⟼ if (e (0) \in (e (1) {Line}_{𝒢} (g) e (2)), ⟨“ f (0) f (1) (ι z \in p \| (⟨“ f (2) f (1) z ”⟩ \sim_{𝒢}^{∠} (g) e \land f (1) dist (g) z = e (1) dist (g) e (0))) ”⟩, ⟨“ e (0) e (1) (ι z \in p \| (⟨“ e (2) e (1) z ”⟩ \sim_{𝒢}^{∠} (g) f \land e (1) dist (g) z = f (1) dist (g) f (0) \land (e (1) {Line}_{𝒢} (g) e (2)) \cap (z Itv (g) e (0)) \neq \emptyset)) ”⟩))⟩, ⟨\leq_{ndx}, \leq_{𝒢}^{∠} (g)⟩\} /_{𝑠} \sim_{𝒢}^{∠} (g))$
85	25 24 84	csb	$class ⦋ \{d \in (p^{(0 ..^3)}) \| (d (0) \neq d (1) \land d (1) \neq d (2))\} / a ⦌ (\{⟨{Base}_{ndx}, a⟩, ⟨+_{ndx}, (e \in a, f \in a ⟼ if (e (0) \in (e (1) {Line}_{𝒢} (g) e (2)), ⟨“ f (0) f (1) (ι z \in p \| (⟨“ f (2) f (1) z ”⟩ \sim_{𝒢}^{∠} (g) e \land f (1) dist (g) z = e (1) dist (g) e (0))) ”⟩, ⟨“ e (0) e (1) (ι z \in p \| (⟨“ e (2) e (1) z ”⟩ \sim_{𝒢}^{∠} (g) f \land e (1) dist (g) z = f (1) dist (g) f (0) \land (e (1) {Line}_{𝒢} (g) e (2)) \cap (z Itv (g) e (0)) \neq \emptyset)) ”⟩))⟩, ⟨\leq_{ndx}, \leq_{𝒢}^{∠} (g)⟩\} /_{𝑠} \sim_{𝒢}^{∠} (g))$
86	6 5 85	csb	$class ⦋ {Base}_{g} / p ⦌ ⦋ \{d \in (p^{(0 ..^3)}) \| (d (0) \neq d (1) \land d (1) \neq d (2))\} / a ⦌ (\{⟨{Base}_{ndx}, a⟩, ⟨+_{ndx}, (e \in a, f \in a ⟼ if (e (0) \in (e (1) {Line}_{𝒢} (g) e (2)), ⟨“ f (0) f (1) (ι z \in p \| (⟨“ f (2) f (1) z ”⟩ \sim_{𝒢}^{∠} (g) e \land f (1) dist (g) z = e (1) dist (g) e (0))) ”⟩, ⟨“ e (0) e (1) (ι z \in p \| (⟨“ e (2) e (1) z ”⟩ \sim_{𝒢}^{∠} (g) f \land e (1) dist (g) z = f (1) dist (g) f (0) \land (e (1) {Line}_{𝒢} (g) e (2)) \cap (z Itv (g) e (0)) \neq \emptyset)) ”⟩))⟩, ⟨\leq_{ndx}, \leq_{𝒢}^{∠} (g)⟩\} /_{𝑠} \sim_{𝒢}^{∠} (g))$
87	1 2 86	cmpt	$class (g \in V ⟼ ⦋ {Base}_{g} / p ⦌ ⦋ \{d \in (p^{(0 ..^3)}) \| (d (0) \neq d (1) \land d (1) \neq d (2))\} / a ⦌ (\{⟨{Base}_{ndx}, a⟩, ⟨+_{ndx}, (e \in a, f \in a ⟼ if (e (0) \in (e (1) {Line}_{𝒢} (g) e (2)), ⟨“ f (0) f (1) (ι z \in p \| (⟨“ f (2) f (1) z ”⟩ \sim_{𝒢}^{∠} (g) e \land f (1) dist (g) z = e (1) dist (g) e (0))) ”⟩, ⟨“ e (0) e (1) (ι z \in p \| (⟨“ e (2) e (1) z ”⟩ \sim_{𝒢}^{∠} (g) f \land e (1) dist (g) z = f (1) dist (g) f (0) \land (e (1) {Line}_{𝒢} (g) e (2)) \cap (z Itv (g) e (0)) \neq \emptyset)) ”⟩))⟩, ⟨\leq_{ndx}, \leq_{𝒢}^{∠} (g)⟩\} /_{𝑠} \sim_{𝒢}^{∠} (g)))$
88	0 87	wceq	Could not format 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 ) ) ) : No typesetting found for wff 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 ) ) ) with typecode wff

Metamath Proof Explorer

Definition df-angmgm

Detailed syntax breakdown