angmgmaddlid

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

	Ref	Expression
Hypotheses	angmgmadd.p	$⊢ P = {Base}_{G}$
	angmgmadd.a	$⊢ A = \{d \in (P^{(0 ..^3)}) \| (d (0) \neq d (1) \land d (1) \neq d (2))\}$
	angmgmadd.i	$⊢ I = Itv (G)$
	angmgmadd.d	$⊢ \underset{˙}{-} = dist (G)$
	angmgmadd.c	$⊢ \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
	angmgmadd.l	$⊢ L = {Line}_{𝒢} (G)$
	angmgmadd.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	angmgmadd.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)) ”⟩))$
	angmgmaddlid.x	$⊢ φ \to X \in P$
	angmgmaddlid.y	$⊢ φ \to Y \in (P ∖ \{X\})$
	angmgmaddlid.e	$⊢ φ \to E \in A$
Assertion	angmgmaddlid	$⊢ φ \to (⟨“ X Y X ”⟩ \underset{˙}{+} E) \underset{˙}{\sim} E$

Proof

Step	Hyp	Ref	Expression
1		angmgmadd.p	$⊢ P = {Base}_{G}$
2		angmgmadd.a	$⊢ A = \{d \in (P^{(0 ..^3)}) \| (d (0) \neq d (1) \land d (1) \neq d (2))\}$
3		angmgmadd.i	$⊢ I = Itv (G)$
4		angmgmadd.d	$⊢ \underset{˙}{-} = dist (G)$
5		angmgmadd.c	$⊢ \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
6		angmgmadd.l	$⊢ L = {Line}_{𝒢} (G)$
7		angmgmadd.g	$⊢ φ \to G \in 𝒢_{Tarski}$
8		angmgmadd.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)) ”⟩))$
9		angmgmaddlid.x	$⊢ φ \to X \in P$
10		angmgmaddlid.y	$⊢ φ \to Y \in (P ∖ \{X\})$
11		angmgmaddlid.e	$⊢ φ \to E \in A$
12		simp-6r	$⊢ (((((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to E = ⟨“ u v w ”⟩$
13	12	oveq2d	$⊢ (((((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to ⟨“ X Y X ”⟩ \underset{˙}{+} E = ⟨“ X Y X ”⟩ \underset{˙}{+} ⟨“ u v w ”⟩$
14	7	ad9antr	$⊢ (((((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to G \in 𝒢_{Tarski}$
15		simp-9r	$⊢ (((((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to u \in P$
16		simp-8r	$⊢ (((((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to v \in P$
17		simp-7r	$⊢ (((((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to w \in P$
18	9	ad9antr	$⊢ (((((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to X \in P$
19	10	eldifad	$⊢ φ \to Y \in P$
20	19	ad9antr	$⊢ (((((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to Y \in P$
21		simp-5r	$⊢ (((((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to u \neq v$
22		simp-4r	$⊢ (((((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to v \neq w$
23	10	eldifsnbd	$⊢ φ \to Y \neq X$
24	23	necomd	$⊢ φ \to X \neq Y$
25	24	ad9antr	$⊢ (((((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to X \neq Y$
26	25	necomd	$⊢ (((((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to Y \neq X$
27	1 3 6 14 20 18 26	tglinerflx2	$⊢ (((((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to X \in (Y L X)$
28		simpllr	$⊢ (((((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to t \in P$
29		eqid	$⊢ {hl}_{𝒢} (G) = {hl}_{𝒢} (G)$
30		simplr	$⊢ (((((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to t {hl}_{𝒢} (G) (v) w$
31	1 3 29 28 17 16 14 30	hlcomd	$⊢ (((((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to w {hl}_{𝒢} (G) (v) t$
32	1 3 29 18 15 20 14 25	hlid	$⊢ (((((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to X {hl}_{𝒢} (G) (Y) X$
33	1 5 29 14 31 32 16 20	zerocgra	$⊢ (((((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to ⟨“ w v t ”⟩ \underset{˙}{\sim} ⟨“ X Y X ”⟩$
34		simpr	$⊢ (((((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to v \underset{˙}{-} t = Y \underset{˙}{-} X$
35	1 2 3 4 5 6 14 15 16 17 18 20 18 21 22 25 26 8 27 28 33 34	angmgmaddov2	$⊢ (((((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to ⟨“ X Y X ”⟩ \underset{˙}{+} ⟨“ u v w ”⟩ = ⟨“ u v t ”⟩$
36	13 35	eqtrd	$⊢ (((((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to ⟨“ X Y X ”⟩ \underset{˙}{+} E = ⟨“ u v t ”⟩$
37	5	eqcomi	$⊢ \sim_{𝒢}^{∠} (G) = \underset{˙}{\sim}$
38	37	a1i	$⊢ (((((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to \sim_{𝒢}^{∠} (G) = \underset{˙}{\sim}$
39	34	eqcomd	$⊢ (((((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to Y \underset{˙}{-} X = v \underset{˙}{-} t$
40	1 4 3 14 20 18 16 28 39 26	tgcgrneq	$⊢ (((((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to v \neq t$
41	1 3 14 29 15 16 28 21 40	cgraid	$⊢ (((((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to ⟨“ u v t ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ u v t ”⟩$
42	1 3 29 14 15 16 28 15 16 28 41 17 31	cgrahl2	$⊢ (((((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to ⟨“ u v t ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ u v w ”⟩$
43	38 42	breqdi	$⊢ (((((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to ⟨“ u v t ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩$
44	36 43	eqbrtrd	$⊢ (((((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to (⟨“ X Y X ”⟩ \underset{˙}{+} E) \underset{˙}{\sim} ⟨“ u v w ”⟩$
45	44	anasss	$⊢ ((((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land t \in P) \land (t {hl}_{𝒢} (G) (v) w \land v \underset{˙}{-} t = Y \underset{˙}{-} X)) \to (⟨“ X Y X ”⟩ \underset{˙}{+} E) \underset{˙}{\sim} ⟨“ u v w ”⟩$
46		simp-5r	$⊢ ((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to v \in P$
47	19	ad6antr	$⊢ ((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to Y \in P$
48	9	ad6antr	$⊢ ((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to X \in P$
49	7	ad6antr	$⊢ ((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to G \in 𝒢_{Tarski}$
50		simp-4r	$⊢ ((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to w \in P$
51		simpr	$⊢ ((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to v \neq w$
52	51	necomd	$⊢ ((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to w \neq v$
53	23	ad6antr	$⊢ ((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to Y \neq X$
54	1 3 29 46 47 48 49 50 4 52 53	hlcgrex	$⊢ ((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to \exists t \in P (t {hl}_{𝒢} (G) (v) w \land v \underset{˙}{-} t = Y \underset{˙}{-} X)$
55	45 54	r19.29a	$⊢ ((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to (⟨“ X Y X ”⟩ \underset{˙}{+} E) \underset{˙}{\sim} ⟨“ u v w ”⟩$
56		simpllr	$⊢ ((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to E = ⟨“ u v w ”⟩$
57	55 56	breqtrrd	$⊢ ((((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to (⟨“ X Y X ”⟩ \underset{˙}{+} E) \underset{˙}{\sim} E$
58	57	anasss	$⊢ (((((φ \land u \in P) \land v \in P) \land w \in P) \land E = ⟨“ u v w ”⟩) \land (u \neq v \land v \neq w)) \to (⟨“ X Y X ”⟩ \underset{˙}{+} E) \underset{˙}{\sim} E$
59	58	anasss	$⊢ ((((φ \land u \in P) \land v \in P) \land w \in P) \land (E = ⟨“ u v w ”⟩ \land (u \neq v \land v \neq w))) \to (⟨“ X Y X ”⟩ \underset{˙}{+} E) \underset{˙}{\sim} E$
60	59	r19.29an	$⊢ (((φ \land u \in P) \land v \in P) \land \exists w \in P (E = ⟨“ u v w ”⟩ \land (u \neq v \land v \neq w))) \to (⟨“ X Y X ”⟩ \underset{˙}{+} E) \underset{˙}{\sim} E$
61	1	fvexi	$⊢ P \in V$
62	61 2 11	elcgrabasi	$⊢ φ \to \exists u \in P \exists v \in P \exists w \in P (E = ⟨“ u v w ”⟩ \land (u \neq v \land v \neq w))$
63	60 62	r19.29vva	$⊢ φ \to (⟨“ X Y X ”⟩ \underset{˙}{+} E) \underset{˙}{\sim} E$

Metamath Proof Explorer

Theorem angmgmaddlid

Proof