angmgm

Description: The angle addition magma is a magma. (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 \|-
	angmgm.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	angmgm.1	$⊢ φ \to 2 \leq \|P\|$
Assertion	angmgm	$⊢ φ \to J \in Mgm$

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		angmgm.g	$⊢ φ \to G \in 𝒢_{Tarski}$
10		angmgm.1	$⊢ φ \to 2 \leq \|P\|$
11	9	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land x \neq y) \to G \in 𝒢_{Tarski}$
12		simpllr	$⊢ (((φ \land x \in P) \land y \in P) \land x \neq y) \to x \in P$
13		simplr	$⊢ (((φ \land x \in P) \land y \in P) \land x \neq y) \to y \in P$
14		simpr	$⊢ (((φ \land x \in P) \land y \in P) \land x \neq y) \to x \neq y$
15	14	necomd	$⊢ (((φ \land x \in P) \land y \in P) \land x \neq y) \to y \neq x$
16	13 15	eldifsnd	$⊢ (((φ \land x \in P) \land y \in P) \land x \neq y) \to y \in (P ∖ \{x\})$
17	1 2 3 4 5 6 7 8 11 12 16	angmgmlem	$⊢ (((φ \land x \in P) \land y \in P) \land x \neq y) \to (J \in Mgm \land [⟨“ x y x ”⟩] \underset{˙}{\sim} = 0_{J})$
18	17	simpld	$⊢ (((φ \land x \in P) \land y \in P) \land x \neq y) \to J \in Mgm$
19	1 4 3 9 10	tglowdim1	$⊢ φ \to \exists x \in P \exists y \in P x \neq y$
20	18 19	r19.29vva	$⊢ φ \to J \in Mgm$

Metamath Proof Explorer

Theorem angmgm

Proof