Theorem angmgm0g

Description: The identity element of the angle addition magma. (Contributed by Thierry Arnoux, 31-Aug-2026)

	Ref	Expression
Hypotheses	angmgmval.p	$$⊢P={\mathrm{Base}}_G$$
	angmgmval.a	$$⊢A=\left\{d\in \left(P^{\left(0..^3\right)}\right)|\left(d\left(0\right)\ne d\left(1\right)\wedge d\left(1\right)\ne d\left(2\right)\right)\right\}$$
	angmgmval.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	angmgmval.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	angmgmval.c	$$⊢\underset{\dot{}}{\sim }={\sim }_{𝒢}^{\angle }\left(G\right)$$
	angmgmval.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
	angmgmval.o	$$⊢\underset{\dot{}}{+}=\left(e\in A,f\in A⟼if\left(e\left(0\right)\in \left(e\left(1\right)Le\left(2\right)\right),⟨“f\left(0\right)f\left(1\right)\left(\iota s\in P|\left(⟨“f\left(2\right)f\left(1\right)s”⟩\underset{\dot{}}{\sim }e\wedge f\left(1\right)\underset{\dot{}}{-}s=e\left(1\right)\underset{\dot{}}{-}e\left(0\right)\right)\right)”⟩,⟨“e\left(0\right)e\left(1\right)\left(\iota s\in P|\left(⟨“e\left(2\right)e\left(1\right)s”⟩\underset{\dot{}}{\sim }f\wedge e\left(1\right)\underset{\dot{}}{-}s=f\left(1\right)\underset{\dot{}}{-}f\left(0\right)\wedge \left(e\left(1\right)Le\left(2\right)\right)\cap \left(sIe\left(0\right)\right)\ne \varnothing \right)\right)”⟩\right)\right)$$
	angmgmval.j	No typesetting found for |- J = ( AngMgm ` G ) with typecode |-
	angmgmlem.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	angmgmlem.x	$$⊢\phi \to X\in P$$
	angmgmlem.y	$$⊢\phi \to Y\in \left(P\setminus \left\{X\right\}\right)$$
Assertion	angmgm0g	$$⊢\phi \to \left[⟨“XYX”⟩\right]\underset{\dot{}}{\sim }=0_J$$

Proof

Step	Hyp	Ref	Expression
1		angmgmval.p	$$⊢P={\mathrm{Base}}_G$$
2		angmgmval.a	$$⊢A=\left\{d\in \left(P^{\left(0..^3\right)}\right)|\left(d\left(0\right)\ne d\left(1\right)\wedge d\left(1\right)\ne d\left(2\right)\right)\right\}$$
3		angmgmval.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		angmgmval.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
5		angmgmval.c	$$⊢\underset{\dot{}}{\sim }={\sim }_{𝒢}^{\angle }\left(G\right)$$
6		angmgmval.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
7		angmgmval.o	$$⊢\underset{\dot{}}{+}=\left(e\in A,f\in A⟼if\left(e\left(0\right)\in \left(e\left(1\right)Le\left(2\right)\right),⟨“f\left(0\right)f\left(1\right)\left(\iota s\in P|\left(⟨“f\left(2\right)f\left(1\right)s”⟩\underset{\dot{}}{\sim }e\wedge f\left(1\right)\underset{\dot{}}{-}s=e\left(1\right)\underset{\dot{}}{-}e\left(0\right)\right)\right)”⟩,⟨“e\left(0\right)e\left(1\right)\left(\iota s\in P|\left(⟨“e\left(2\right)e\left(1\right)s”⟩\underset{\dot{}}{\sim }f\wedge e\left(1\right)\underset{\dot{}}{-}s=f\left(1\right)\underset{\dot{}}{-}f\left(0\right)\wedge \left(e\left(1\right)Le\left(2\right)\right)\cap \left(sIe\left(0\right)\right)\ne \varnothing \right)\right)”⟩\right)\right)$$
8		angmgmval.j	Could not format J = ( AngMgm ` G ) : No typesetting found for |- J = ( AngMgm ` G ) with typecode |-
9		angmgmlem.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
10		angmgmlem.x	$$⊢\phi \to X\in P$$
11		angmgmlem.y	$$⊢\phi \to Y\in \left(P\setminus \left\{X\right\}\right)$$
12	1 2 3 4 5 6 7 8 9 10 11	angmgmlem	$$⊢\phi \to \left(J\in \mathrm{Mgm}\wedge \left[⟨“XYX”⟩\right]\underset{\dot{}}{\sim }=0_J\right)$$
13	12	simprd	$$⊢\phi \to \left[⟨“XYX”⟩\right]\underset{\dot{}}{\sim }=0_J$$