angmgmval

Description: Explicit the value of the angle addition magma for a given geometry G . (Contributed by Thierry Arnoux, 31-Aug-2026)

	Ref	Expression
Hypotheses	angmgmval.p	$⊢ P = {Base}_{G}$
	angmgmval.a	$⊢ A = \{d \in (P^{(0 ..^3)}) \| (d (0) \neq d (1) \land d (1) \neq d (2))\}$
	angmgmval.i	$⊢ I = Itv (G)$
	angmgmval.d	$⊢ \underset{˙}{-} = dist (G)$
	angmgmval.c	$⊢ \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
	angmgmval.l	$⊢ L = {Line}_{𝒢} (G)$
	angmgmval.o	$⊢ \underset{˙}{+} = (e \in A, f \in A ⟼ if (e (0) \in (e (1) L e (2)), ⟨“ f (0) f (1) (ι s \in P \| (⟨“ f (2) f (1) s ”⟩ \underset{˙}{\sim} e \land f (1) \underset{˙}{-} s = e (1) \underset{˙}{-} e (0))) ”⟩, ⟨“ e (0) e (1) (ι s \in P \| (⟨“ e (2) e (1) s ”⟩ \underset{˙}{\sim} f \land e (1) \underset{˙}{-} s = f (1) \underset{˙}{-} f (0) \land (e (1) L e (2)) \cap (s I e (0)) \neq \emptyset)) ”⟩))$
	angmgmval.j	No typesetting found for \|- J = ( AngMgm ` G ) with typecode \|-
	angmgmval.s	$⊢ \underset{˙}{\leq} = \leq_{𝒢}^{∠} (G)$
Assertion	angmgmval	$⊢ G \in V \to J = \{⟨{Base}_{ndx}, A⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩\} /_{𝑠} \underset{˙}{\sim}$

Proof

Step	Hyp	Ref	Expression
1		angmgmval.p	$⊢ P = {Base}_{G}$
2		angmgmval.a	$⊢ A = \{d \in (P^{(0 ..^3)}) \| (d (0) \neq d (1) \land d (1) \neq d (2))\}$
3		angmgmval.i	$⊢ I = Itv (G)$
4		angmgmval.d	$⊢ \underset{˙}{-} = dist (G)$
5		angmgmval.c	$⊢ \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
6		angmgmval.l	$⊢ L = {Line}_{𝒢} (G)$
7		angmgmval.o	$⊢ \underset{˙}{+} = (e \in A, f \in A ⟼ if (e (0) \in (e (1) L e (2)), ⟨“ f (0) f (1) (ι s \in P \| (⟨“ f (2) f (1) s ”⟩ \underset{˙}{\sim} e \land f (1) \underset{˙}{-} s = e (1) \underset{˙}{-} e (0))) ”⟩, ⟨“ e (0) e (1) (ι s \in P \| (⟨“ e (2) e (1) s ”⟩ \underset{˙}{\sim} f \land e (1) \underset{˙}{-} s = f (1) \underset{˙}{-} f (0) \land (e (1) L e (2)) \cap (s I e (0)) \neq \emptyset)) ”⟩))$
8		angmgmval.j	Could not format J = ( AngMgm ` G ) : No typesetting found for \|- J = ( AngMgm ` G ) with typecode \|-
9		angmgmval.s	$⊢ \underset{˙}{\leq} = \leq_{𝒢}^{∠} (G)$
10		df-angmgm	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_ s e. p ( <" ( f ` 2 ) ( f ` 1 ) s "> ( cgrA ` g ) e /\ ( ( f ` 1 ) ( dist ` g ) s ) = ( ( e ` 1 ) ( dist ` g ) ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ s e. p ( <" ( e ` 2 ) ( e ` 1 ) s "> ( cgrA ` g ) f /\ ( ( e ` 1 ) ( dist ` g ) s ) = ( ( f ` 1 ) ( dist ` g ) ( f ` 0 ) ) /\ ( ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) i^i ( s ( Itv ` g ) ( e ` 0 ) ) ) =/= (/) ) ) "> ) ) >. , <. ( le ` ndx ) , ( leA ` g ) >. } /s ( cgrA ` g ) ) ) : 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_ s e. p ( <" ( f ` 2 ) ( f ` 1 ) s "> ( cgrA ` g ) e /\ ( ( f ` 1 ) ( dist ` g ) s ) = ( ( e ` 1 ) ( dist ` g ) ( e ` 0 ) ) ) ) "> , <" ( e ` 0 ) ( e ` 1 ) ( iota_ s e. p ( <" ( e ` 2 ) ( e ` 1 ) s "> ( cgrA ` g ) f /\ ( ( e ` 1 ) ( dist ` g ) s ) = ( ( f ` 1 ) ( dist ` g ) ( f ` 0 ) ) /\ ( ( ( e ` 1 ) ( LineG ` g ) ( e ` 2 ) ) i^i ( s ( Itv ` g ) ( e ` 0 ) ) ) =/= (/) ) ) "> ) ) >. , <. ( le ` ndx ) , ( leA ` g ) >. } /s ( cgrA ` g ) ) ) with typecode \|-
11		fvexd	$⊢ g = G \to {Base}_{g} \in V$
12		fveq2	$⊢ g = G \to {Base}_{g} = {Base}_{G}$
13	12 1	eqtr4di	$⊢ g = G \to {Base}_{g} = P$
14		eqid	$⊢ \{d \in (p^{(0 ..^3)}) \| (d (0) \neq d (1) \land d (1) \neq d (2))\} = \{d \in (p^{(0 ..^3)}) \| (d (0) \neq d (1) \land d (1) \neq d (2))\}$
15		ovexd	$⊢ (g = G \land p = P) \to p^{(0 ..^3)} \in V$
16	14 15	rabexd	$⊢ (g = G \land p = P) \to \{d \in (p^{(0 ..^3)}) \| (d (0) \neq d (1) \land d (1) \neq d (2))\} \in V$
17		oveq1	$⊢ p = P \to p^{(0 ..^3)} = P^{(0 ..^3)}$
18	17	adantl	$⊢ (g = G \land p = P) \to p^{(0 ..^3)} = P^{(0 ..^3)}$
19	18	rabeqdv	$⊢ (g = G \land p = P) \to \{d \in (p^{(0 ..^3)}) \| (d (0) \neq d (1) \land d (1) \neq d (2))\} = \{d \in (P^{(0 ..^3)}) \| (d (0) \neq d (1) \land d (1) \neq d (2))\}$
20	19 2	eqtr4di	$⊢ (g = G \land p = P) \to \{d \in (p^{(0 ..^3)}) \| (d (0) \neq d (1) \land d (1) \neq d (2))\} = A$
21		opeq2	$⊢ a = A \to ⟨{Base}_{ndx}, a⟩ = ⟨{Base}_{ndx}, A⟩$
22	21	adantl	$⊢ ((g = G \land p = P) \land a = A) \to ⟨{Base}_{ndx}, a⟩ = ⟨{Base}_{ndx}, A⟩$
23		simpr	$⊢ ((g = G \land p = P) \land a = A) \to a = A$
24		fveq2	$⊢ g = G \to {Line}_{𝒢} (g) = {Line}_{𝒢} (G)$
25	24	ad2antrr	$⊢ ((g = G \land p = P) \land a = A) \to {Line}_{𝒢} (g) = {Line}_{𝒢} (G)$
26	25 6	eqtr4di	$⊢ ((g = G \land p = P) \land a = A) \to {Line}_{𝒢} (g) = L$
27	26	oveqd	$⊢ ((g = G \land p = P) \land a = A) \to e (1) {Line}_{𝒢} (g) e (2) = e (1) L e (2)$
28	27	eleq2d	$⊢ ((g = G \land p = P) \land a = A) \to (e (0) \in (e (1) {Line}_{𝒢} (g) e (2)) \leftrightarrow e (0) \in (e (1) L e (2)))$
29		eqidd	$⊢ ((g = G \land p = P) \land a = A) \to f (0) = f (0)$
30		eqidd	$⊢ ((g = G \land p = P) \land a = A) \to f (1) = f (1)$
31		simplr	$⊢ ((g = G \land p = P) \land a = A) \to p = P$
32		fveq2	$⊢ g = G \to \sim_{𝒢}^{∠} (g) = \sim_{𝒢}^{∠} (G)$
33	32 5	eqtr4di	$⊢ g = G \to \sim_{𝒢}^{∠} (g) = \underset{˙}{\sim}$
34	33	ad2antrr	$⊢ ((g = G \land p = P) \land a = A) \to \sim_{𝒢}^{∠} (g) = \underset{˙}{\sim}$
35	34	breqd	$⊢ ((g = G \land p = P) \land a = A) \to (⟨“ f (2) f (1) s ”⟩ \sim_{𝒢}^{∠} (g) e \leftrightarrow ⟨“ f (2) f (1) s ”⟩ \underset{˙}{\sim} e)$
36		fveq2	$⊢ g = G \to dist (g) = dist (G)$
37	36 4	eqtr4di	$⊢ g = G \to dist (g) = \underset{˙}{-}$
38	37	ad2antrr	$⊢ ((g = G \land p = P) \land a = A) \to dist (g) = \underset{˙}{-}$
39	38	oveqd	$⊢ ((g = G \land p = P) \land a = A) \to f (1) dist (g) s = f (1) \underset{˙}{-} s$
40	38	oveqd	$⊢ ((g = G \land p = P) \land a = A) \to e (1) dist (g) e (0) = e (1) \underset{˙}{-} e (0)$
41	39 40	eqeq12d	$⊢ ((g = G \land p = P) \land a = A) \to (f (1) dist (g) s = e (1) dist (g) e (0) \leftrightarrow f (1) \underset{˙}{-} s = e (1) \underset{˙}{-} e (0))$
42	35 41	anbi12d	$⊢ ((g = G \land p = P) \land a = A) \to ((⟨“ f (2) f (1) s ”⟩ \sim_{𝒢}^{∠} (g) e \land f (1) dist (g) s = e (1) dist (g) e (0)) \leftrightarrow (⟨“ f (2) f (1) s ”⟩ \underset{˙}{\sim} e \land f (1) \underset{˙}{-} s = e (1) \underset{˙}{-} e (0)))$
43	31 42	riotaeqbidv	$⊢ ((g = G \land p = P) \land a = A) \to (ι s \in p \| (⟨“ f (2) f (1) s ”⟩ \sim_{𝒢}^{∠} (g) e \land f (1) dist (g) s = e (1) dist (g) e (0))) = (ι s \in P \| (⟨“ f (2) f (1) s ”⟩ \underset{˙}{\sim} e \land f (1) \underset{˙}{-} s = e (1) \underset{˙}{-} e (0)))$
44	29 30 43	s3eqd	$⊢ ((g = G \land p = P) \land a = A) \to ⟨“ f (0) f (1) (ι s \in p \| (⟨“ f (2) f (1) s ”⟩ \sim_{𝒢}^{∠} (g) e \land f (1) dist (g) s = e (1) dist (g) e (0))) ”⟩ = ⟨“ f (0) f (1) (ι s \in P \| (⟨“ f (2) f (1) s ”⟩ \underset{˙}{\sim} e \land f (1) \underset{˙}{-} s = e (1) \underset{˙}{-} e (0))) ”⟩$
45		eqidd	$⊢ ((g = G \land p = P) \land a = A) \to e (0) = e (0)$
46		eqidd	$⊢ ((g = G \land p = P) \land a = A) \to e (1) = e (1)$
47	34	breqd	$⊢ ((g = G \land p = P) \land a = A) \to (⟨“ e (2) e (1) s ”⟩ \sim_{𝒢}^{∠} (g) f \leftrightarrow ⟨“ e (2) e (1) s ”⟩ \underset{˙}{\sim} f)$
48	38	oveqd	$⊢ ((g = G \land p = P) \land a = A) \to e (1) dist (g) s = e (1) \underset{˙}{-} s$
49	38	oveqd	$⊢ ((g = G \land p = P) \land a = A) \to f (1) dist (g) f (0) = f (1) \underset{˙}{-} f (0)$
50	48 49	eqeq12d	$⊢ ((g = G \land p = P) \land a = A) \to (e (1) dist (g) s = f (1) dist (g) f (0) \leftrightarrow e (1) \underset{˙}{-} s = f (1) \underset{˙}{-} f (0))$
51		fveq2	$⊢ g = G \to Itv (g) = Itv (G)$
52	51 3	eqtr4di	$⊢ g = G \to Itv (g) = I$
53	52	ad2antrr	$⊢ ((g = G \land p = P) \land a = A) \to Itv (g) = I$
54	53	oveqd	$⊢ ((g = G \land p = P) \land a = A) \to s Itv (g) e (0) = s I e (0)$
55	27 54	ineq12d	$⊢ ((g = G \land p = P) \land a = A) \to (e (1) {Line}_{𝒢} (g) e (2)) \cap (s Itv (g) e (0)) = (e (1) L e (2)) \cap (s I e (0))$
56	55	neeq1d	$⊢ ((g = G \land p = P) \land a = A) \to ((e (1) {Line}_{𝒢} (g) e (2)) \cap (s Itv (g) e (0)) \neq \emptyset \leftrightarrow (e (1) L e (2)) \cap (s I e (0)) \neq \emptyset)$
57	47 50 56	3anbi123d	$⊢ ((g = G \land p = P) \land a = A) \to ((⟨“ e (2) e (1) s ”⟩ \sim_{𝒢}^{∠} (g) f \land e (1) dist (g) s = f (1) dist (g) f (0) \land (e (1) {Line}_{𝒢} (g) e (2)) \cap (s Itv (g) e (0)) \neq \emptyset) \leftrightarrow (⟨“ e (2) e (1) s ”⟩ \underset{˙}{\sim} f \land e (1) \underset{˙}{-} s = f (1) \underset{˙}{-} f (0) \land (e (1) L e (2)) \cap (s I e (0)) \neq \emptyset))$
58	31 57	riotaeqbidv	$⊢ ((g = G \land p = P) \land a = A) \to (ι s \in p \| (⟨“ e (2) e (1) s ”⟩ \sim_{𝒢}^{∠} (g) f \land e (1) dist (g) s = f (1) dist (g) f (0) \land (e (1) {Line}_{𝒢} (g) e (2)) \cap (s Itv (g) e (0)) \neq \emptyset)) = (ι s \in P \| (⟨“ e (2) e (1) s ”⟩ \underset{˙}{\sim} f \land e (1) \underset{˙}{-} s = f (1) \underset{˙}{-} f (0) \land (e (1) L e (2)) \cap (s I e (0)) \neq \emptyset))$
59	45 46 58	s3eqd	$⊢ ((g = G \land p = P) \land a = A) \to ⟨“ e (0) e (1) (ι s \in p \| (⟨“ e (2) e (1) s ”⟩ \sim_{𝒢}^{∠} (g) f \land e (1) dist (g) s = f (1) dist (g) f (0) \land (e (1) {Line}_{𝒢} (g) e (2)) \cap (s Itv (g) e (0)) \neq \emptyset)) ”⟩ = ⟨“ e (0) e (1) (ι s \in P \| (⟨“ e (2) e (1) s ”⟩ \underset{˙}{\sim} f \land e (1) \underset{˙}{-} s = f (1) \underset{˙}{-} f (0) \land (e (1) L e (2)) \cap (s I e (0)) \neq \emptyset)) ”⟩$
60	28 44 59	ifbieq12d	$⊢ ((g = G \land p = P) \land a = A) \to if (e (0) \in (e (1) {Line}_{𝒢} (g) e (2)), ⟨“ f (0) f (1) (ι s \in p \| (⟨“ f (2) f (1) s ”⟩ \sim_{𝒢}^{∠} (g) e \land f (1) dist (g) s = e (1) dist (g) e (0))) ”⟩, ⟨“ e (0) e (1) (ι s \in p \| (⟨“ e (2) e (1) s ”⟩ \sim_{𝒢}^{∠} (g) f \land e (1) dist (g) s = f (1) dist (g) f (0) \land (e (1) {Line}_{𝒢} (g) e (2)) \cap (s Itv (g) e (0)) \neq \emptyset)) ”⟩) = if (e (0) \in (e (1) L e (2)), ⟨“ f (0) f (1) (ι s \in P \| (⟨“ f (2) f (1) s ”⟩ \underset{˙}{\sim} e \land f (1) \underset{˙}{-} s = e (1) \underset{˙}{-} e (0))) ”⟩, ⟨“ e (0) e (1) (ι s \in P \| (⟨“ e (2) e (1) s ”⟩ \underset{˙}{\sim} f \land e (1) \underset{˙}{-} s = f (1) \underset{˙}{-} f (0) \land (e (1) L e (2)) \cap (s I e (0)) \neq \emptyset)) ”⟩)$
61	23 23 60	mpoeq123dv	$⊢ ((g = G \land p = P) \land a = A) \to (e \in a, f \in a ⟼ if (e (0) \in (e (1) {Line}_{𝒢} (g) e (2)), ⟨“ f (0) f (1) (ι s \in p \| (⟨“ f (2) f (1) s ”⟩ \sim_{𝒢}^{∠} (g) e \land f (1) dist (g) s = e (1) dist (g) e (0))) ”⟩, ⟨“ e (0) e (1) (ι s \in p \| (⟨“ e (2) e (1) s ”⟩ \sim_{𝒢}^{∠} (g) f \land e (1) dist (g) s = f (1) dist (g) f (0) \land (e (1) {Line}_{𝒢} (g) e (2)) \cap (s Itv (g) e (0)) \neq \emptyset)) ”⟩)) = (e \in A, f \in A ⟼ if (e (0) \in (e (1) L e (2)), ⟨“ f (0) f (1) (ι s \in P \| (⟨“ f (2) f (1) s ”⟩ \underset{˙}{\sim} e \land f (1) \underset{˙}{-} s = e (1) \underset{˙}{-} e (0))) ”⟩, ⟨“ e (0) e (1) (ι s \in P \| (⟨“ e (2) e (1) s ”⟩ \underset{˙}{\sim} f \land e (1) \underset{˙}{-} s = f (1) \underset{˙}{-} f (0) \land (e (1) L e (2)) \cap (s I e (0)) \neq \emptyset)) ”⟩))$
62	61 7	eqtr4di	$⊢ ((g = G \land p = P) \land a = A) \to (e \in a, f \in a ⟼ if (e (0) \in (e (1) {Line}_{𝒢} (g) e (2)), ⟨“ f (0) f (1) (ι s \in p \| (⟨“ f (2) f (1) s ”⟩ \sim_{𝒢}^{∠} (g) e \land f (1) dist (g) s = e (1) dist (g) e (0))) ”⟩, ⟨“ e (0) e (1) (ι s \in p \| (⟨“ e (2) e (1) s ”⟩ \sim_{𝒢}^{∠} (g) f \land e (1) dist (g) s = f (1) dist (g) f (0) \land (e (1) {Line}_{𝒢} (g) e (2)) \cap (s Itv (g) e (0)) \neq \emptyset)) ”⟩)) = \underset{˙}{+}$
63	62	opeq2d	$⊢ ((g = G \land p = P) \land a = A) \to ⟨+_{ndx}, (e \in a, f \in a ⟼ if (e (0) \in (e (1) {Line}_{𝒢} (g) e (2)), ⟨“ f (0) f (1) (ι s \in p \| (⟨“ f (2) f (1) s ”⟩ \sim_{𝒢}^{∠} (g) e \land f (1) dist (g) s = e (1) dist (g) e (0))) ”⟩, ⟨“ e (0) e (1) (ι s \in p \| (⟨“ e (2) e (1) s ”⟩ \sim_{𝒢}^{∠} (g) f \land e (1) dist (g) s = f (1) dist (g) f (0) \land (e (1) {Line}_{𝒢} (g) e (2)) \cap (s Itv (g) e (0)) \neq \emptyset)) ”⟩))⟩ = ⟨+_{ndx}, \underset{˙}{+}⟩$
64		fveq2	$⊢ g = G \to \leq_{𝒢}^{∠} (g) = \leq_{𝒢}^{∠} (G)$
65	64 9	eqtr4di	$⊢ g = G \to \leq_{𝒢}^{∠} (g) = \underset{˙}{\leq}$
66	65	opeq2d	$⊢ g = G \to ⟨\leq_{ndx}, \leq_{𝒢}^{∠} (g)⟩ = ⟨\leq_{ndx}, \underset{˙}{\leq}⟩$
67	66	ad2antrr	$⊢ ((g = G \land p = P) \land a = A) \to ⟨\leq_{ndx}, \leq_{𝒢}^{∠} (g)⟩ = ⟨\leq_{ndx}, \underset{˙}{\leq}⟩$
68	22 63 67	tpeq123d	$⊢ ((g = G \land p = P) \land a = A) \to \{⟨{Base}_{ndx}, a⟩, ⟨+_{ndx}, (e \in a, f \in a ⟼ if (e (0) \in (e (1) {Line}_{𝒢} (g) e (2)), ⟨“ f (0) f (1) (ι s \in p \| (⟨“ f (2) f (1) s ”⟩ \sim_{𝒢}^{∠} (g) e \land f (1) dist (g) s = e (1) dist (g) e (0))) ”⟩, ⟨“ e (0) e (1) (ι s \in p \| (⟨“ e (2) e (1) s ”⟩ \sim_{𝒢}^{∠} (g) f \land e (1) dist (g) s = f (1) dist (g) f (0) \land (e (1) {Line}_{𝒢} (g) e (2)) \cap (s Itv (g) e (0)) \neq \emptyset)) ”⟩))⟩, ⟨\leq_{ndx}, \leq_{𝒢}^{∠} (g)⟩\} = \{⟨{Base}_{ndx}, A⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩\}$
69	68 34	oveq12d	$⊢ ((g = G \land p = P) \land a = A) \to \{⟨{Base}_{ndx}, a⟩, ⟨+_{ndx}, (e \in a, f \in a ⟼ if (e (0) \in (e (1) {Line}_{𝒢} (g) e (2)), ⟨“ f (0) f (1) (ι s \in p \| (⟨“ f (2) f (1) s ”⟩ \sim_{𝒢}^{∠} (g) e \land f (1) dist (g) s = e (1) dist (g) e (0))) ”⟩, ⟨“ e (0) e (1) (ι s \in p \| (⟨“ e (2) e (1) s ”⟩ \sim_{𝒢}^{∠} (g) f \land e (1) dist (g) s = f (1) dist (g) f (0) \land (e (1) {Line}_{𝒢} (g) e (2)) \cap (s Itv (g) e (0)) \neq \emptyset)) ”⟩))⟩, ⟨\leq_{ndx}, \leq_{𝒢}^{∠} (g)⟩\} /_{𝑠} \sim_{𝒢}^{∠} (g) = \{⟨{Base}_{ndx}, A⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩\} /_{𝑠} \underset{˙}{\sim}$
70	16 20 69	csbied2	$⊢ (g = G \land p = P) \to ⦋ \{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) (ι s \in p \| (⟨“ f (2) f (1) s ”⟩ \sim_{𝒢}^{∠} (g) e \land f (1) dist (g) s = e (1) dist (g) e (0))) ”⟩, ⟨“ e (0) e (1) (ι s \in p \| (⟨“ e (2) e (1) s ”⟩ \sim_{𝒢}^{∠} (g) f \land e (1) dist (g) s = f (1) dist (g) f (0) \land (e (1) {Line}_{𝒢} (g) e (2)) \cap (s Itv (g) e (0)) \neq \emptyset)) ”⟩))⟩, ⟨\leq_{ndx}, \leq_{𝒢}^{∠} (g)⟩\} /_{𝑠} \sim_{𝒢}^{∠} (g)) = \{⟨{Base}_{ndx}, A⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩\} /_{𝑠} \underset{˙}{\sim}$
71	11 13 70	csbied2	$⊢ g = G \to ⦋ {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) (ι s \in p \| (⟨“ f (2) f (1) s ”⟩ \sim_{𝒢}^{∠} (g) e \land f (1) dist (g) s = e (1) dist (g) e (0))) ”⟩, ⟨“ e (0) e (1) (ι s \in p \| (⟨“ e (2) e (1) s ”⟩ \sim_{𝒢}^{∠} (g) f \land e (1) dist (g) s = f (1) dist (g) f (0) \land (e (1) {Line}_{𝒢} (g) e (2)) \cap (s Itv (g) e (0)) \neq \emptyset)) ”⟩))⟩, ⟨\leq_{ndx}, \leq_{𝒢}^{∠} (g)⟩\} /_{𝑠} \sim_{𝒢}^{∠} (g)) = \{⟨{Base}_{ndx}, A⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩\} /_{𝑠} \underset{˙}{\sim}$
72		elex	$⊢ G \in V \to G \in V$
73		ovexd	$⊢ G \in V \to \{⟨{Base}_{ndx}, A⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩\} /_{𝑠} \underset{˙}{\sim} \in V$
74	10 71 72 73	fvmptd3	Could not format ( G e. V -> ( AngMgm ` G ) = ( { <. ( Base ` ndx ) , A >. , <. ( +g ` ndx ) , .+ >. , <. ( le ` ndx ) , .<_ >. } /s .~ ) ) : No typesetting found for \|- ( G e. V -> ( AngMgm ` G ) = ( { <. ( Base ` ndx ) , A >. , <. ( +g ` ndx ) , .+ >. , <. ( le ` ndx ) , .<_ >. } /s .~ ) ) with typecode \|-
75	8 74	eqtrid	$⊢ G \in V \to J = \{⟨{Base}_{ndx}, A⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩\} /_{𝑠} \underset{˙}{\sim}$

Metamath Proof Explorer

Theorem angmgmval

Proof