angmgmaddrid

Description: The right 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	angmgmaddrid	$⊢ φ \to (E \underset{˙}{+} ⟨“ X Y X ”⟩) \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-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 u \in (v L w)) \land w {hl}_{𝒢} (G) (v) u) \land t \in P) \land t {hl}_{𝒢} (G) (Y) X) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to E = ⟨“ u v w ”⟩$
13	12	oveq1d	$⊢ (((((((((((φ \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 u \in (v L w)) \land w {hl}_{𝒢} (G) (v) u) \land t \in P) \land t {hl}_{𝒢} (G) (Y) X) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to E \underset{˙}{+} ⟨“ X Y X ”⟩ = ⟨“ u v w ”⟩ \underset{˙}{+} ⟨“ X Y X ”⟩$
14	7	ad7antr	$⊢ (((((((φ \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 u \in (v L w)) \to G \in 𝒢_{Tarski}$
15	14	ad4antr	$⊢ (((((((((((φ \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 u \in (v L w)) \land w {hl}_{𝒢} (G) (v) u) \land t \in P) \land t {hl}_{𝒢} (G) (Y) X) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to G \in 𝒢_{Tarski}$
16	9	ad7antr	$⊢ (((((((φ \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 u \in (v L w)) \to X \in P$
17	16	ad4antr	$⊢ (((((((((((φ \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 u \in (v L w)) \land w {hl}_{𝒢} (G) (v) u) \land t \in P) \land t {hl}_{𝒢} (G) (Y) X) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to X \in P$
18	10	eldifad	$⊢ φ \to Y \in P$
19	18	ad7antr	$⊢ (((((((φ \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 u \in (v L w)) \to Y \in P$
20	19	ad4antr	$⊢ (((((((((((φ \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 u \in (v L w)) \land w {hl}_{𝒢} (G) (v) u) \land t \in P) \land t {hl}_{𝒢} (G) (Y) X) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to Y \in P$
21		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 u \in (v L w)) \to u \in P$
22	21	ad4antr	$⊢ (((((((((((φ \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 u \in (v L w)) \land w {hl}_{𝒢} (G) (v) u) \land t \in P) \land t {hl}_{𝒢} (G) (Y) X) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to u \in P$
23		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 u \in (v L w)) \to v \in P$
24	23	ad4antr	$⊢ (((((((((((φ \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 u \in (v L w)) \land w {hl}_{𝒢} (G) (v) u) \land t \in P) \land t {hl}_{𝒢} (G) (Y) X) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to v \in P$
25		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 u \in (v L w)) \to w \in P$
26	25	ad4antr	$⊢ (((((((((((φ \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 u \in (v L w)) \land w {hl}_{𝒢} (G) (v) u) \land t \in P) \land t {hl}_{𝒢} (G) (Y) X) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to w \in P$
27	10	eldifsnbd	$⊢ φ \to Y \neq X$
28	27	necomd	$⊢ φ \to X \neq Y$
29	28	ad7antr	$⊢ (((((((φ \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 u \in (v L w)) \to X \neq Y$
30	29	ad4antr	$⊢ (((((((((((φ \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 u \in (v L w)) \land w {hl}_{𝒢} (G) (v) u) \land t \in P) \land t {hl}_{𝒢} (G) (Y) X) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to X \neq Y$
31	27	ad7antr	$⊢ (((((((φ \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 u \in (v L w)) \to Y \neq X$
32	31	ad4antr	$⊢ (((((((((((φ \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 u \in (v L w)) \land w {hl}_{𝒢} (G) (v) u) \land t \in P) \land t {hl}_{𝒢} (G) (Y) X) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to Y \neq X$
33		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 u \in (v L w)) \to u \neq v$
34	33	ad4antr	$⊢ (((((((((((φ \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 u \in (v L w)) \land w {hl}_{𝒢} (G) (v) u) \land t \in P) \land t {hl}_{𝒢} (G) (Y) X) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to u \neq v$
35		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 u \in (v L w)) \land w {hl}_{𝒢} (G) (v) u) \land t \in P) \land t {hl}_{𝒢} (G) (Y) X) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to v \neq w$
36		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 u \in (v L w)) \land w {hl}_{𝒢} (G) (v) u) \land t \in P) \land t {hl}_{𝒢} (G) (Y) X) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to u \in (v L w)$
37		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 u \in (v L w)) \land w {hl}_{𝒢} (G) (v) u) \land t \in P) \land t {hl}_{𝒢} (G) (Y) X) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to t \in P$
38		eqid	$⊢ {hl}_{𝒢} (G) = {hl}_{𝒢} (G)$
39		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 u \in (v L w)) \land w {hl}_{𝒢} (G) (v) u) \land t \in P) \land t {hl}_{𝒢} (G) (Y) X) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to t {hl}_{𝒢} (G) (Y) X$
40	1 3 38 37 17 20 15 39	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 u \in (v L w)) \land w {hl}_{𝒢} (G) (v) u) \land t \in P) \land t {hl}_{𝒢} (G) (Y) X) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to X {hl}_{𝒢} (G) (Y) t$
41		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 u \in (v L w)) \land w {hl}_{𝒢} (G) (v) u) \land t \in P) \land t {hl}_{𝒢} (G) (Y) X) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to w {hl}_{𝒢} (G) (v) u$
42	1 3 38 26 22 24 15 41	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 u \in (v L w)) \land w {hl}_{𝒢} (G) (v) u) \land t \in P) \land t {hl}_{𝒢} (G) (Y) X) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to u {hl}_{𝒢} (G) (v) w$
43	1 5 38 15 40 42 20 24	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 u \in (v L w)) \land w {hl}_{𝒢} (G) (v) u) \land t \in P) \land t {hl}_{𝒢} (G) (Y) X) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to ⟨“ X Y t ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩$
44		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 u \in (v L w)) \land w {hl}_{𝒢} (G) (v) u) \land t \in P) \land t {hl}_{𝒢} (G) (Y) X) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to Y \underset{˙}{-} t = v \underset{˙}{-} u$
45	1 2 3 4 5 6 15 17 20 17 22 24 26 30 32 34 35 8 36 37 43 44	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 u \in (v L w)) \land w {hl}_{𝒢} (G) (v) u) \land t \in P) \land t {hl}_{𝒢} (G) (Y) X) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to ⟨“ u v w ”⟩ \underset{˙}{+} ⟨“ X Y X ”⟩ = ⟨“ X Y t ”⟩$
46	13 45	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 u \in (v L w)) \land w {hl}_{𝒢} (G) (v) u) \land t \in P) \land t {hl}_{𝒢} (G) (Y) X) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to E \underset{˙}{+} ⟨“ X Y X ”⟩ = ⟨“ X Y t ”⟩$
47	46 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 u \in (v L w)) \land w {hl}_{𝒢} (G) (v) u) \land t \in P) \land t {hl}_{𝒢} (G) (Y) X) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to (E \underset{˙}{+} ⟨“ X Y X ”⟩) \underset{˙}{\sim} ⟨“ u v w ”⟩$
48	47	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 u \in (v L w)) \land w {hl}_{𝒢} (G) (v) u) \land t \in P) \land (t {hl}_{𝒢} (G) (Y) X \land Y \underset{˙}{-} t = v \underset{˙}{-} u)) \to (E \underset{˙}{+} ⟨“ X Y X ”⟩) \underset{˙}{\sim} ⟨“ u v w ”⟩$
49	18	ad8antr	$⊢ ((((((((φ \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 u \in (v L w)) \land w {hl}_{𝒢} (G) (v) u) \to Y \in P$
50	23	adantr	$⊢ ((((((((φ \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 u \in (v L w)) \land w {hl}_{𝒢} (G) (v) u) \to v \in P$
51	21	adantr	$⊢ ((((((((φ \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 u \in (v L w)) \land w {hl}_{𝒢} (G) (v) u) \to u \in P$
52	14	adantr	$⊢ ((((((((φ \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 u \in (v L w)) \land w {hl}_{𝒢} (G) (v) u) \to G \in 𝒢_{Tarski}$
53	16	adantr	$⊢ ((((((((φ \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 u \in (v L w)) \land w {hl}_{𝒢} (G) (v) u) \to X \in P$
54	28	ad8antr	$⊢ ((((((((φ \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 u \in (v L w)) \land w {hl}_{𝒢} (G) (v) u) \to X \neq Y$
55	33	adantr	$⊢ ((((((((φ \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 u \in (v L w)) \land w {hl}_{𝒢} (G) (v) u) \to u \neq v$
56	55	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 u \in (v L w)) \land w {hl}_{𝒢} (G) (v) u) \to v \neq u$
57	1 3 38 49 50 51 52 53 4 54 56	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) \land u \in (v L w)) \land w {hl}_{𝒢} (G) (v) u) \to \exists t \in P (t {hl}_{𝒢} (G) (Y) X \land Y \underset{˙}{-} t = v \underset{˙}{-} u)$
58	48 57	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) \land u \in (v L w)) \land w {hl}_{𝒢} (G) (v) u) \to (E \underset{˙}{+} ⟨“ X Y X ”⟩) \underset{˙}{\sim} ⟨“ u v w ”⟩$
59		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 u \in (v L w)) \land v \in (u I w)) \land t \in P) \land Y \in (X I t)) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to E = ⟨“ u v w ”⟩$
60	59	oveq1d	$⊢ (((((((((((φ \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 u \in (v L w)) \land v \in (u I w)) \land t \in P) \land Y \in (X I t)) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to E \underset{˙}{+} ⟨“ X Y X ”⟩ = ⟨“ u v w ”⟩ \underset{˙}{+} ⟨“ X Y X ”⟩$
61	14	adantr	$⊢ ((((((((φ \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 u \in (v L w)) \land v \in (u I w)) \to G \in 𝒢_{Tarski}$
62	61	ad3antrrr	$⊢ (((((((((((φ \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 u \in (v L w)) \land v \in (u I w)) \land t \in P) \land Y \in (X I t)) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to G \in 𝒢_{Tarski}$
63	16	adantr	$⊢ ((((((((φ \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 u \in (v L w)) \land v \in (u I w)) \to X \in P$
64	63	ad3antrrr	$⊢ (((((((((((φ \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 u \in (v L w)) \land v \in (u I w)) \land t \in P) \land Y \in (X I t)) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to X \in P$
65	18	ad8antr	$⊢ ((((((((φ \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 u \in (v L w)) \land v \in (u I w)) \to Y \in P$
66	65	ad3antrrr	$⊢ (((((((((((φ \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 u \in (v L w)) \land v \in (u I w)) \land t \in P) \land Y \in (X I t)) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to Y \in P$
67	21	adantr	$⊢ ((((((((φ \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 u \in (v L w)) \land v \in (u I w)) \to u \in P$
68	67	ad3antrrr	$⊢ (((((((((((φ \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 u \in (v L w)) \land v \in (u I w)) \land t \in P) \land Y \in (X I t)) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to u \in P$
69	23	adantr	$⊢ ((((((((φ \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 u \in (v L w)) \land v \in (u I w)) \to v \in P$
70	69	ad3antrrr	$⊢ (((((((((((φ \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 u \in (v L w)) \land v \in (u I w)) \land t \in P) \land Y \in (X I t)) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to v \in P$
71	25	ad4antr	$⊢ (((((((((((φ \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 u \in (v L w)) \land v \in (u I w)) \land t \in P) \land Y \in (X I t)) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to w \in P$
72	29	ad4antr	$⊢ (((((((((((φ \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 u \in (v L w)) \land v \in (u I w)) \land t \in P) \land Y \in (X I t)) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to X \neq Y$
73	72	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 u \in (v L w)) \land v \in (u I w)) \land t \in P) \land Y \in (X I t)) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to Y \neq X$
74	33	ad4antr	$⊢ (((((((((((φ \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 u \in (v L w)) \land v \in (u I w)) \land t \in P) \land Y \in (X I t)) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to u \neq v$
75		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 u \in (v L w)) \land v \in (u I w)) \land t \in P) \land Y \in (X I t)) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to v \neq w$
76		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 u \in (v L w)) \land v \in (u I w)) \land t \in P) \land Y \in (X I t)) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to u \in (v L w)$
77		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 u \in (v L w)) \land v \in (u I w)) \land t \in P) \land Y \in (X I t)) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to t \in P$
78	5	eqcomi	$⊢ \sim_{𝒢}^{∠} (G) = \underset{˙}{\sim}$
79	78	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 u \in (v L w)) \land v \in (u I w)) \land t \in P) \land Y \in (X I t)) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to \sim_{𝒢}^{∠} (G) = \underset{˙}{\sim}$
80		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 u \in (v L w)) \land v \in (u I w)) \land t \in P) \land Y \in (X I t)) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to Y \in (X I t)$
81		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 u \in (v L w)) \land v \in (u I w)) \land t \in P) \land Y \in (X I t)) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to v \in (u I w)$
82		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 u \in (v L w)) \land v \in (u I w)) \land t \in P) \land Y \in (X I t)) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to Y \underset{˙}{-} t = v \underset{˙}{-} u$
83	82	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 u \in (v L w)) \land v \in (u I w)) \land t \in P) \land Y \in (X I t)) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to v \underset{˙}{-} u = Y \underset{˙}{-} t$
84	74	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 u \in (v L w)) \land v \in (u I w)) \land t \in P) \land Y \in (X I t)) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to v \neq u$
85	1 4 3 62 70 68 66 77 83 84	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 u \in (v L w)) \land v \in (u I w)) \land t \in P) \land Y \in (X I t)) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to Y \neq t$
86	85	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 u \in (v L w)) \land v \in (u I w)) \land t \in P) \land Y \in (X I t)) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to t \neq Y$
87	75	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 u \in (v L w)) \land v \in (u I w)) \land t \in P) \land Y \in (X I t)) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to w \neq v$
88	1 3 4 62 64 66 77 68 70 71 80 81 72 86 74 87	flatcgra	$⊢ (((((((((((φ \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 u \in (v L w)) \land v \in (u I w)) \land t \in P) \land Y \in (X I t)) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to ⟨“ X Y t ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ u v w ”⟩$
89	79 88	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 u \in (v L w)) \land v \in (u I w)) \land t \in P) \land Y \in (X I t)) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to ⟨“ X Y t ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩$
90	1 2 3 4 5 6 62 64 66 64 68 70 71 72 73 74 75 8 76 77 89 82	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 u \in (v L w)) \land v \in (u I w)) \land t \in P) \land Y \in (X I t)) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to ⟨“ u v w ”⟩ \underset{˙}{+} ⟨“ X Y X ”⟩ = ⟨“ X Y t ”⟩$
91	60 90	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 u \in (v L w)) \land v \in (u I w)) \land t \in P) \land Y \in (X I t)) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to E \underset{˙}{+} ⟨“ X Y X ”⟩ = ⟨“ X Y t ”⟩$
92	91 89	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 u \in (v L w)) \land v \in (u I w)) \land t \in P) \land Y \in (X I t)) \land Y \underset{˙}{-} t = v \underset{˙}{-} u) \to (E \underset{˙}{+} ⟨“ X Y X ”⟩) \underset{˙}{\sim} ⟨“ u v w ”⟩$
93	92	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 u \in (v L w)) \land v \in (u I w)) \land t \in P) \land (Y \in (X I t) \land Y \underset{˙}{-} t = v \underset{˙}{-} u)) \to (E \underset{˙}{+} ⟨“ X Y X ”⟩) \underset{˙}{\sim} ⟨“ u v w ”⟩$
94	1 4 3 61 63 65 69 67	axtgsegcon	$⊢ ((((((((φ \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 u \in (v L w)) \land v \in (u I w)) \to \exists t \in P (Y \in (X I t) \land Y \underset{˙}{-} t = v \underset{˙}{-} u)$
95	93 94	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) \land u \in (v L w)) \land v \in (u I w)) \to (E \underset{˙}{+} ⟨“ X Y X ”⟩) \underset{˙}{\sim} ⟨“ u v w ”⟩$
96		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 u \in (v L w)) \to u \in (v L w)$
97		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 u \in (v L w)) \to v \neq w$
98	1 3 6 14 21 23 25 33 96 97	lnrot2	$⊢ (((((((φ \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 u \in (v L w)) \to w \in (u L v)$
99	1 3 38 21 23 25 14 16 6 98	lnhl	$⊢ (((((((φ \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 u \in (v L w)) \to (w {hl}_{𝒢} (G) (v) u \lor v \in (u I w))$
100	58 95 99	mpjaodan	$⊢ (((((((φ \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 u \in (v L w)) \to (E \underset{˙}{+} ⟨“ X Y X ”⟩) \underset{˙}{\sim} ⟨“ u v w ”⟩$
101		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 \neg u \in (v L w)) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to E = ⟨“ u v w ”⟩$
102	101	oveq1d	$⊢ ((((((((((φ \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 \neg u \in (v L w)) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to E \underset{˙}{+} ⟨“ X Y X ”⟩ = ⟨“ u v w ”⟩ \underset{˙}{+} ⟨“ X Y X ”⟩$
103	7	ad7antr	$⊢ (((((((φ \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 \neg u \in (v L w)) \to G \in 𝒢_{Tarski}$
104	103	ad3antrrr	$⊢ ((((((((((φ \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 \neg u \in (v L w)) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to G \in 𝒢_{Tarski}$
105	9	ad7antr	$⊢ (((((((φ \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 \neg u \in (v L w)) \to X \in P$
106	105	ad3antrrr	$⊢ ((((((((((φ \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 \neg u \in (v L w)) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to X \in P$
107	18	ad7antr	$⊢ (((((((φ \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 \neg u \in (v L w)) \to Y \in P$
108	107	ad3antrrr	$⊢ ((((((((((φ \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 \neg u \in (v L w)) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to Y \in P$
109		simp-10r	$⊢ ((((((((((φ \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 \neg u \in (v L w)) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to u \in P$
110		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 \neg u \in (v L w)) \to v \in P$
111	110	ad3antrrr	$⊢ ((((((((((φ \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 \neg u \in (v L w)) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to v \in P$
112		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 \neg u \in (v L w)) \to w \in P$
113	112	ad3antrrr	$⊢ ((((((((((φ \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 \neg u \in (v L w)) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to w \in P$
114	28	ad10antr	$⊢ ((((((((((φ \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 \neg u \in (v L w)) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to X \neq Y$
115	27	ad7antr	$⊢ (((((((φ \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 \neg u \in (v L w)) \to Y \neq X$
116	115	ad3antrrr	$⊢ ((((((((((φ \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 \neg u \in (v L w)) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to Y \neq X$
117		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 \neg u \in (v L w)) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to u \neq v$
118		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 \neg u \in (v L w)) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to v \neq w$
119		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 \neg u \in (v L w)) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to \neg u \in (v L w)$
120		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 \neg u \in (v L w)) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to t \in P$
121		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 \neg u \in (v L w)) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to t {hl}_{𝒢} (G) (v) w$
122	1 3 38 120 113 111 104 121	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 \neg u \in (v L w)) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to w {hl}_{𝒢} (G) (v) t$
123	1 3 38 106 106 108 104 114	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 \neg u \in (v L w)) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to X {hl}_{𝒢} (G) (Y) X$
124	1 5 38 104 122 123 111 108	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 \neg u \in (v L 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 ”⟩$
125		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 \neg u \in (v L 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$
126	1 3 38 113 120 111 104 6 122	hlln	$⊢ ((((((((((φ \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 \neg u \in (v L w)) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to w \in (t L v)$
127	1 6 3 104 120 111 126	tglngne	$⊢ ((((((((((φ \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 \neg u \in (v L w)) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to t \neq v$
128	1 3 6 104 111 113 120 118 126 127	lnrot1	$⊢ ((((((((((φ \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 \neg u \in (v L w)) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to t \in (v L w)$
129	1 4 3 104 120 109	tgbtwntriv1	$⊢ ((((((((((φ \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 \neg u \in (v L w)) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to t \in (t I u)$
130	128 129	elind	$⊢ ((((((((((φ \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 \neg u \in (v L w)) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to t \in ((v L w) \cap (t I u))$
131	130	ne0d	$⊢ ((((((((((φ \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 \neg u \in (v L w)) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to (v L w) \cap (t I u) \neq \emptyset$
132	1 2 3 4 5 6 104 106 108 106 109 111 113 114 116 117 118 8 119 120 124 125 131	angmgmaddov1	$⊢ ((((((((((φ \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 \neg u \in (v L w)) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to ⟨“ u v w ”⟩ \underset{˙}{+} ⟨“ X Y X ”⟩ = ⟨“ u v t ”⟩$
133	102 132	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 \neg u \in (v L w)) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to E \underset{˙}{+} ⟨“ X Y X ”⟩ = ⟨“ u v t ”⟩$
134	78	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 \neg u \in (v L w)) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to \sim_{𝒢}^{∠} (G) = \underset{˙}{\sim}$
135	127	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 \neg u \in (v L w)) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to v \neq t$
136	1 3 104 38 109 111 120 117 135	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 \neg u \in (v L 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 ”⟩$
137	1 3 38 104 109 111 120 109 111 120 136 113 122	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 \neg u \in (v L 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 ”⟩$
138	134 137	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 \neg u \in (v L 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 ”⟩$
139	133 138	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 \neg u \in (v L w)) \land t \in P) \land t {hl}_{𝒢} (G) (v) w) \land v \underset{˙}{-} t = Y \underset{˙}{-} X) \to (E \underset{˙}{+} ⟨“ X Y X ”⟩) \underset{˙}{\sim} ⟨“ u v w ”⟩$
140	139	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 \neg u \in (v L w)) \land t \in P) \land (t {hl}_{𝒢} (G) (v) w \land v \underset{˙}{-} t = Y \underset{˙}{-} X)) \to (E \underset{˙}{+} ⟨“ X Y X ”⟩) \underset{˙}{\sim} ⟨“ u v w ”⟩$
141		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 \neg u \in (v L w)) \to v \neq w$
142	141	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 \neg u \in (v L w)) \to w \neq v$
143	1 3 38 110 107 105 103 112 4 142 115	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) \land \neg u \in (v L w)) \to \exists t \in P (t {hl}_{𝒢} (G) (v) w \land v \underset{˙}{-} t = Y \underset{˙}{-} X)$
144	140 143	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) \land \neg u \in (v L w)) \to (E \underset{˙}{+} ⟨“ X Y X ”⟩) \underset{˙}{\sim} ⟨“ u v w ”⟩$
145	100 144	pm2.61dan	$⊢ ((((((φ \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 \underset{˙}{+} ⟨“ X Y X ”⟩) \underset{˙}{\sim} ⟨“ u v w ”⟩$
146		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 ”⟩$
147	145 146	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 (E \underset{˙}{+} ⟨“ X Y X ”⟩) \underset{˙}{\sim} E$
148	147	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 (E \underset{˙}{+} ⟨“ X Y X ”⟩) \underset{˙}{\sim} E$
149	148	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 (E \underset{˙}{+} ⟨“ X Y X ”⟩) \underset{˙}{\sim} E$
150	149	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 (E \underset{˙}{+} ⟨“ X Y X ”⟩) \underset{˙}{\sim} E$
151	1	fvexi	$⊢ P \in V$
152	151 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))$
153	150 152	r19.29vva	$⊢ φ \to (E \underset{˙}{+} ⟨“ X Y X ”⟩) \underset{˙}{\sim} E$

Metamath Proof Explorer

Theorem angmgmaddrid

Proof