angmgmaddcl

Description: Closure of 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)) ”⟩))$
	angmgmaddcl.1	$⊢ φ \to E \in A$
	angmgmaddcl.2	$⊢ φ \to F \in A$
Assertion	angmgmaddcl	$⊢ φ \to E \underset{˙}{+} F \in A$

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		angmgmaddcl.1	$⊢ φ \to E \in A$
10		angmgmaddcl.2	$⊢ φ \to F \in A$
11		simp-5r	$⊢ ((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \to E = ⟨“ x y z ”⟩$
12	11	adantr	$⊢ (((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \to E = ⟨“ x y z ”⟩$
13	12	ad6antr	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \land t \in P) \land (⟨“ w v t ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩ \land v \underset{˙}{-} t = y \underset{˙}{-} x)) \to E = ⟨“ x y z ”⟩$
14		simp-6r	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \land t \in P) \land (⟨“ w v t ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩ \land v \underset{˙}{-} t = y \underset{˙}{-} x)) \to F = ⟨“ u v w ”⟩$
15	13 14	oveq12d	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \land t \in P) \land (⟨“ w v t ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩ \land v \underset{˙}{-} t = y \underset{˙}{-} x)) \to E \underset{˙}{+} F = ⟨“ x y z ”⟩ \underset{˙}{+} ⟨“ u v w ”⟩$
16	7	ad2antrr	$⊢ ((φ \land x \in P) \land y \in P) \to G \in 𝒢_{Tarski}$
17	16	ad4antr	$⊢ ((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \to G \in 𝒢_{Tarski}$
18	17	ad9antr	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \land t \in P) \land (⟨“ w v t ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩ \land v \underset{˙}{-} t = y \underset{˙}{-} x)) \to G \in 𝒢_{Tarski}$
19		simp-9r	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \land t \in P) \land (⟨“ w v t ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩ \land v \underset{˙}{-} t = y \underset{˙}{-} x)) \to u \in P$
20		simp-8r	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \land t \in P) \land (⟨“ w v t ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩ \land v \underset{˙}{-} t = y \underset{˙}{-} x)) \to v \in P$
21		simp-7r	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \land t \in P) \land (⟨“ w v t ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩ \land v \underset{˙}{-} t = y \underset{˙}{-} x)) \to w \in P$
22		simplr	$⊢ ((φ \land x \in P) \land y \in P) \to x \in P$
23	22	ad4antr	$⊢ ((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \to x \in P$
24	23	ad9antr	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \land t \in P) \land (⟨“ w v t ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩ \land v \underset{˙}{-} t = y \underset{˙}{-} x)) \to x \in P$
25		simp-5r	$⊢ ((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \to y \in P$
26	25	ad9antr	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \land t \in P) \land (⟨“ w v t ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩ \land v \underset{˙}{-} t = y \underset{˙}{-} x)) \to y \in P$
27		simplr	$⊢ ((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \to z \in P$
28	27	ad2antrr	$⊢ ((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \to z \in P$
29	28	ad9antr	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \land t \in P) \land (⟨“ w v t ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩ \land v \underset{˙}{-} t = y \underset{˙}{-} x)) \to z \in P$
30		simp-5r	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \land t \in P) \land (⟨“ w v t ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩ \land v \underset{˙}{-} t = y \underset{˙}{-} x)) \to u \neq v$
31		simp-4r	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \land t \in P) \land (⟨“ w v t ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩ \land v \underset{˙}{-} t = y \underset{˙}{-} x)) \to v \neq w$
32		simp-11r	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \land t \in P) \land (⟨“ w v t ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩ \land v \underset{˙}{-} t = y \underset{˙}{-} x)) \to x \neq y$
33		simp-10r	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \land t \in P) \land (⟨“ w v t ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩ \land v \underset{˙}{-} t = y \underset{˙}{-} x)) \to y \neq z$
34		simpllr	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \land t \in P) \land (⟨“ w v t ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩ \land v \underset{˙}{-} t = y \underset{˙}{-} x)) \to x \in (y L z)$
35		simplr	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \land t \in P) \land (⟨“ w v t ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩ \land v \underset{˙}{-} t = y \underset{˙}{-} x)) \to t \in P$
36		simprl	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \land t \in P) \land (⟨“ w v t ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩ \land v \underset{˙}{-} t = y \underset{˙}{-} x)) \to ⟨“ w v t ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩$
37		simprr	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \land t \in P) \land (⟨“ w v t ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩ \land v \underset{˙}{-} t = y \underset{˙}{-} x)) \to v \underset{˙}{-} t = y \underset{˙}{-} x$
38	1 2 3 4 5 6 18 19 20 21 24 26 29 30 31 32 33 8 34 35 36 37	angmgmaddov2	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \land t \in P) \land (⟨“ w v t ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩ \land v \underset{˙}{-} t = y \underset{˙}{-} x)) \to ⟨“ x y z ”⟩ \underset{˙}{+} ⟨“ u v w ”⟩ = ⟨“ u v t ”⟩$
39	15 38	eqtrd	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \land t \in P) \land (⟨“ w v t ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩ \land v \underset{˙}{-} t = y \underset{˙}{-} x)) \to E \underset{˙}{+} F = ⟨“ u v t ”⟩$
40	1	fvexi	$⊢ P \in V$
41	40	a1i	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \land t \in P) \land (⟨“ w v t ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩ \land v \underset{˙}{-} t = y \underset{˙}{-} x)) \to P \in V$
42	37	eqcomd	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \land t \in P) \land (⟨“ w v t ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩ \land v \underset{˙}{-} t = y \underset{˙}{-} x)) \to y \underset{˙}{-} x = v \underset{˙}{-} t$
43	32	necomd	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \land t \in P) \land (⟨“ w v t ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩ \land v \underset{˙}{-} t = y \underset{˙}{-} x)) \to y \neq x$
44	1 4 3 18 26 24 20 35 42 43	tgcgrneq	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \land t \in P) \land (⟨“ w v t ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩ \land v \underset{˙}{-} t = y \underset{˙}{-} x)) \to v \neq t$
45	2 41 19 20 35 30 44	elcgrabasrd	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \land t \in P) \land (⟨“ w v t ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩ \land v \underset{˙}{-} t = y \underset{˙}{-} x)) \to ⟨“ u v t ”⟩ \in A$
46	39 45	eqeltrd	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \land t \in P) \land (⟨“ w v t ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩ \land v \underset{˙}{-} t = y \underset{˙}{-} x)) \to E \underset{˙}{+} F \in A$
47	16	ad2antrr	$⊢ ((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \to G \in 𝒢_{Tarski}$
48	47	ad9antr	$⊢ (((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \to G \in 𝒢_{Tarski}$
49		simp-7r	$⊢ (((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \to u \in P$
50		simp-6r	$⊢ (((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \to v \in P$
51		simp-5r	$⊢ (((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \to w \in P$
52	22	ad2antrr	$⊢ ((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \to x \in P$
53	52	ad9antr	$⊢ (((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \to x \in P$
54	25	ad7antr	$⊢ (((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \to y \in P$
55		simp-11r	$⊢ (((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \to z \in P$
56		simpllr	$⊢ (((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \to u \neq v$
57		simplr	$⊢ (((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \to v \neq w$
58		simp-9r	$⊢ (((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \to x \neq y$
59		simp-8r	$⊢ (((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \to y \neq z$
60		simpr	$⊢ (((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \to x \in (y L z)$
61	1 2 3 4 5 6 48 49 50 51 53 54 55 56 57 58 59 60	angmgmaddov2lem	$⊢ (((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \to \exists! s \in P (⟨“ w v s ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩ \land v \underset{˙}{-} s = y \underset{˙}{-} x)$
62		reurex	$⊢ \exists! s \in P (⟨“ w v s ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩ \land v \underset{˙}{-} s = y \underset{˙}{-} x) \to \exists s \in P (⟨“ w v s ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩ \land v \underset{˙}{-} s = y \underset{˙}{-} x)$
63	61 62	syl	$⊢ (((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \to \exists s \in P (⟨“ w v s ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩ \land v \underset{˙}{-} s = y \underset{˙}{-} x)$
64		eqidd	$⊢ s = t \to w = w$
65		eqidd	$⊢ s = t \to v = v$
66		id	$⊢ s = t \to s = t$
67	64 65 66	s3eqd	$⊢ s = t \to ⟨“ w v s ”⟩ = ⟨“ w v t ”⟩$
68	67	breq1d	$⊢ s = t \to (⟨“ w v s ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩ \leftrightarrow ⟨“ w v t ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩)$
69		oveq2	$⊢ s = t \to v \underset{˙}{-} s = v \underset{˙}{-} t$
70	69	eqeq1d	$⊢ s = t \to (v \underset{˙}{-} s = y \underset{˙}{-} x \leftrightarrow v \underset{˙}{-} t = y \underset{˙}{-} x)$
71	68 70	anbi12d	$⊢ s = t \to ((⟨“ w v s ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩ \land v \underset{˙}{-} s = y \underset{˙}{-} x) \leftrightarrow (⟨“ w v t ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩ \land v \underset{˙}{-} t = y \underset{˙}{-} x))$
72	71	cbvrexvw	$⊢ \exists s \in P (⟨“ w v s ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩ \land v \underset{˙}{-} s = y \underset{˙}{-} x) \leftrightarrow \exists t \in P (⟨“ w v t ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩ \land v \underset{˙}{-} t = y \underset{˙}{-} x)$
73	63 72	sylib	$⊢ (((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \to \exists t \in P (⟨“ w v t ”⟩ \underset{˙}{\sim} ⟨“ x y z ”⟩ \land v \underset{˙}{-} t = y \underset{˙}{-} x)$
74	46 73	r19.29a	$⊢ (((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land x \in (y L z)) \to E \underset{˙}{+} F \in A$
75	11	ad7antr	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \land t \in P) \land (⟨“ z y t ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩ \land y \underset{˙}{-} t = v \underset{˙}{-} u \land (y L z) \cap (t I x) \neq \emptyset)) \to E = ⟨“ x y z ”⟩$
76		simp-6r	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \land t \in P) \land (⟨“ z y t ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩ \land y \underset{˙}{-} t = v \underset{˙}{-} u \land (y L z) \cap (t I x) \neq \emptyset)) \to F = ⟨“ u v w ”⟩$
77	75 76	oveq12d	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \land t \in P) \land (⟨“ z y t ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩ \land y \underset{˙}{-} t = v \underset{˙}{-} u \land (y L z) \cap (t I x) \neq \emptyset)) \to E \underset{˙}{+} F = ⟨“ x y z ”⟩ \underset{˙}{+} ⟨“ u v w ”⟩$
78	17	ad7antr	$⊢ (((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \to G \in 𝒢_{Tarski}$
79	78	ad2antrr	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \land t \in P) \land (⟨“ z y t ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩ \land y \underset{˙}{-} t = v \underset{˙}{-} u \land (y L z) \cap (t I x) \neq \emptyset)) \to G \in 𝒢_{Tarski}$
80		simp-7r	$⊢ (((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \to u \in P$
81	80	ad2antrr	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \land t \in P) \land (⟨“ z y t ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩ \land y \underset{˙}{-} t = v \underset{˙}{-} u \land (y L z) \cap (t I x) \neq \emptyset)) \to u \in P$
82		simp-6r	$⊢ (((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \to v \in P$
83	82	ad2antrr	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \land t \in P) \land (⟨“ z y t ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩ \land y \underset{˙}{-} t = v \underset{˙}{-} u \land (y L z) \cap (t I x) \neq \emptyset)) \to v \in P$
84		simp-5r	$⊢ (((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \to w \in P$
85	84	ad2antrr	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \land t \in P) \land (⟨“ z y t ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩ \land y \underset{˙}{-} t = v \underset{˙}{-} u \land (y L z) \cap (t I x) \neq \emptyset)) \to w \in P$
86	23	ad7antr	$⊢ (((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \to x \in P$
87	86	ad2antrr	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \land t \in P) \land (⟨“ z y t ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩ \land y \underset{˙}{-} t = v \underset{˙}{-} u \land (y L z) \cap (t I x) \neq \emptyset)) \to x \in P$
88	25	ad7antr	$⊢ (((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \to y \in P$
89	88	ad2antrr	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \land t \in P) \land (⟨“ z y t ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩ \land y \underset{˙}{-} t = v \underset{˙}{-} u \land (y L z) \cap (t I x) \neq \emptyset)) \to y \in P$
90		simp-11r	$⊢ (((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \to z \in P$
91	90	ad2antrr	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \land t \in P) \land (⟨“ z y t ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩ \land y \underset{˙}{-} t = v \underset{˙}{-} u \land (y L z) \cap (t I x) \neq \emptyset)) \to z \in P$
92		simpllr	$⊢ (((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \to u \neq v$
93	92	ad2antrr	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \land t \in P) \land (⟨“ z y t ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩ \land y \underset{˙}{-} t = v \underset{˙}{-} u \land (y L z) \cap (t I x) \neq \emptyset)) \to u \neq v$
94		simplr	$⊢ (((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \to v \neq w$
95	94	ad2antrr	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \land t \in P) \land (⟨“ z y t ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩ \land y \underset{˙}{-} t = v \underset{˙}{-} u \land (y L z) \cap (t I x) \neq \emptyset)) \to v \neq w$
96		simp-9r	$⊢ (((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \to x \neq y$
97	96	ad2antrr	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \land t \in P) \land (⟨“ z y t ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩ \land y \underset{˙}{-} t = v \underset{˙}{-} u \land (y L z) \cap (t I x) \neq \emptyset)) \to x \neq y$
98		simp-8r	$⊢ (((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \to y \neq z$
99	98	ad2antrr	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \land t \in P) \land (⟨“ z y t ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩ \land y \underset{˙}{-} t = v \underset{˙}{-} u \land (y L z) \cap (t I x) \neq \emptyset)) \to y \neq z$
100		simpr	$⊢ (((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \to \neg x \in (y L z)$
101	100	ad2antrr	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \land t \in P) \land (⟨“ z y t ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩ \land y \underset{˙}{-} t = v \underset{˙}{-} u \land (y L z) \cap (t I x) \neq \emptyset)) \to \neg x \in (y L z)$
102		simplr	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \land t \in P) \land (⟨“ z y t ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩ \land y \underset{˙}{-} t = v \underset{˙}{-} u \land (y L z) \cap (t I x) \neq \emptyset)) \to t \in P$
103		simpr1	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \land t \in P) \land (⟨“ z y t ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩ \land y \underset{˙}{-} t = v \underset{˙}{-} u \land (y L z) \cap (t I x) \neq \emptyset)) \to ⟨“ z y t ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩$
104		simpr2	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \land t \in P) \land (⟨“ z y t ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩ \land y \underset{˙}{-} t = v \underset{˙}{-} u \land (y L z) \cap (t I x) \neq \emptyset)) \to y \underset{˙}{-} t = v \underset{˙}{-} u$
105		simpr3	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \land t \in P) \land (⟨“ z y t ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩ \land y \underset{˙}{-} t = v \underset{˙}{-} u \land (y L z) \cap (t I x) \neq \emptyset)) \to (y L z) \cap (t I x) \neq \emptyset$
106	1 2 3 4 5 6 79 81 83 85 87 89 91 93 95 97 99 8 101 102 103 104 105	angmgmaddov1	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \land t \in P) \land (⟨“ z y t ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩ \land y \underset{˙}{-} t = v \underset{˙}{-} u \land (y L z) \cap (t I x) \neq \emptyset)) \to ⟨“ x y z ”⟩ \underset{˙}{+} ⟨“ u v w ”⟩ = ⟨“ x y t ”⟩$
107	77 106	eqtrd	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \land t \in P) \land (⟨“ z y t ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩ \land y \underset{˙}{-} t = v \underset{˙}{-} u \land (y L z) \cap (t I x) \neq \emptyset)) \to E \underset{˙}{+} F = ⟨“ x y t ”⟩$
108	40	a1i	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \land t \in P) \land (⟨“ z y t ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩ \land y \underset{˙}{-} t = v \underset{˙}{-} u \land (y L z) \cap (t I x) \neq \emptyset)) \to P \in V$
109	104	eqcomd	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \land t \in P) \land (⟨“ z y t ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩ \land y \underset{˙}{-} t = v \underset{˙}{-} u \land (y L z) \cap (t I x) \neq \emptyset)) \to v \underset{˙}{-} u = y \underset{˙}{-} t$
110	93	necomd	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \land t \in P) \land (⟨“ z y t ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩ \land y \underset{˙}{-} t = v \underset{˙}{-} u \land (y L z) \cap (t I x) \neq \emptyset)) \to v \neq u$
111	1 4 3 79 83 81 89 102 109 110	tgcgrneq	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \land t \in P) \land (⟨“ z y t ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩ \land y \underset{˙}{-} t = v \underset{˙}{-} u \land (y L z) \cap (t I x) \neq \emptyset)) \to y \neq t$
112	2 108 87 89 102 97 111	elcgrabasrd	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \land t \in P) \land (⟨“ z y t ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩ \land y \underset{˙}{-} t = v \underset{˙}{-} u \land (y L z) \cap (t I x) \neq \emptyset)) \to ⟨“ x y t ”⟩ \in A$
113	107 112	eqeltrd	$⊢ (((((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \land t \in P) \land (⟨“ z y t ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩ \land y \underset{˙}{-} t = v \underset{˙}{-} u \land (y L z) \cap (t I x) \neq \emptyset)) \to E \underset{˙}{+} F \in A$
114	1 2 3 4 5 6 78 80 82 84 86 88 90 92 94 96 98 100	angmgmaddov1lem	$⊢ (((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \to \exists! s \in P (⟨“ z y s ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩ \land y \underset{˙}{-} s = v \underset{˙}{-} u \land (y L z) \cap (s I x) \neq \emptyset)$
115		reurex	$⊢ \exists! s \in P (⟨“ z y s ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩ \land y \underset{˙}{-} s = v \underset{˙}{-} u \land (y L z) \cap (s I x) \neq \emptyset) \to \exists s \in P (⟨“ z y s ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩ \land y \underset{˙}{-} s = v \underset{˙}{-} u \land (y L z) \cap (s I x) \neq \emptyset)$
116	114 115	syl	$⊢ (((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \to \exists s \in P (⟨“ z y s ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩ \land y \underset{˙}{-} s = v \underset{˙}{-} u \land (y L z) \cap (s I x) \neq \emptyset)$
117		eqidd	$⊢ s = t \to z = z$
118		eqidd	$⊢ s = t \to y = y$
119	117 118 66	s3eqd	$⊢ s = t \to ⟨“ z y s ”⟩ = ⟨“ z y t ”⟩$
120	119	breq1d	$⊢ s = t \to (⟨“ z y s ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩ \leftrightarrow ⟨“ z y t ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩)$
121		oveq2	$⊢ s = t \to y \underset{˙}{-} s = y \underset{˙}{-} t$
122	121	eqeq1d	$⊢ s = t \to (y \underset{˙}{-} s = v \underset{˙}{-} u \leftrightarrow y \underset{˙}{-} t = v \underset{˙}{-} u)$
123		oveq1	$⊢ s = t \to s I x = t I x$
124	123	ineq2d	$⊢ s = t \to (y L z) \cap (s I x) = (y L z) \cap (t I x)$
125	124	neeq1d	$⊢ s = t \to ((y L z) \cap (s I x) \neq \emptyset \leftrightarrow (y L z) \cap (t I x) \neq \emptyset)$
126	120 122 125	3anbi123d	$⊢ s = t \to ((⟨“ z y s ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩ \land y \underset{˙}{-} s = v \underset{˙}{-} u \land (y L z) \cap (s I x) \neq \emptyset) \leftrightarrow (⟨“ z y t ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩ \land y \underset{˙}{-} t = v \underset{˙}{-} u \land (y L z) \cap (t I x) \neq \emptyset))$
127	126	cbvrexvw	$⊢ \exists s \in P (⟨“ z y s ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩ \land y \underset{˙}{-} s = v \underset{˙}{-} u \land (y L z) \cap (s I x) \neq \emptyset) \leftrightarrow \exists t \in P (⟨“ z y t ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩ \land y \underset{˙}{-} t = v \underset{˙}{-} u \land (y L z) \cap (t I x) \neq \emptyset)$
128	116 127	sylib	$⊢ (((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \to \exists t \in P (⟨“ z y t ”⟩ \underset{˙}{\sim} ⟨“ u v w ”⟩ \land y \underset{˙}{-} t = v \underset{˙}{-} u \land (y L z) \cap (t I x) \neq \emptyset)$
129	113 128	r19.29a	$⊢ (((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \land \neg x \in (y L z)) \to E \underset{˙}{+} F \in A$
130		exmidd	$⊢ ((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to (x \in (y L z) \lor \neg x \in (y L z))$
131	74 129 130	mpjaodan	$⊢ ((((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land u \neq v) \land v \neq w) \to E \underset{˙}{+} F \in A$
132	131	anasss	$⊢ (((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land F = ⟨“ u v w ”⟩) \land (u \neq v \land v \neq w)) \to E \underset{˙}{+} F \in A$
133	132	anasss	$⊢ ((((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land w \in P) \land (F = ⟨“ u v w ”⟩ \land (u \neq v \land v \neq w))) \to E \underset{˙}{+} F \in A$
134	133	r19.29an	$⊢ (((((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \land u \in P) \land v \in P) \land \exists w \in P (F = ⟨“ u v w ”⟩ \land (u \neq v \land v \neq w))) \to E \underset{˙}{+} F \in A$
135	40 2 10	elcgrabasi	$⊢ φ \to \exists u \in P \exists v \in P \exists w \in P (F = ⟨“ u v w ”⟩ \land (u \neq v \land v \neq w))$
136	135	ad6antr	$⊢ ((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \to \exists u \in P \exists v \in P \exists w \in P (F = ⟨“ u v w ”⟩ \land (u \neq v \land v \neq w))$
137	134 136	r19.29vva	$⊢ ((((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land x \neq y) \land y \neq z) \to E \underset{˙}{+} F \in A$
138	137	anasss	$⊢ (((((φ \land x \in P) \land y \in P) \land z \in P) \land E = ⟨“ x y z ”⟩) \land (x \neq y \land y \neq z)) \to E \underset{˙}{+} F \in A$
139	138	anasss	$⊢ ((((φ \land x \in P) \land y \in P) \land z \in P) \land (E = ⟨“ x y z ”⟩ \land (x \neq y \land y \neq z))) \to E \underset{˙}{+} F \in A$
140	139	r19.29an	$⊢ (((φ \land x \in P) \land y \in P) \land \exists z \in P (E = ⟨“ x y z ”⟩ \land (x \neq y \land y \neq z))) \to E \underset{˙}{+} F \in A$
141	40 2 9	elcgrabasi	$⊢ φ \to \exists x \in P \exists y \in P \exists z \in P (E = ⟨“ x y z ”⟩ \land (x \neq y \land y \neq z))$
142	140 141	r19.29vva	$⊢ φ \to E \underset{˙}{+} F \in A$

Metamath Proof Explorer

Theorem angmgmaddcl

Proof