angmgmaddeu1

Description: There exists a unique point s satisfying the conditions of angle addition. General case. (Contributed by Thierry Arnoux, 23-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}$
	angmgmaddov.u	$⊢ φ \to U \in P$
	angmgmaddov.v	$⊢ φ \to V \in P$
	angmgmaddov.w	$⊢ φ \to W \in P$
	angmgmaddov.x	$⊢ φ \to X \in P$
	angmgmaddov.y	$⊢ φ \to Y \in P$
	angmgmaddov.z	$⊢ φ \to Z \in P$
	angmgmaddeu.1	$⊢ φ \to U \neq V$
	angmgmaddeu.2	$⊢ φ \to V \neq W$
	angmgmaddeu.3	$⊢ φ \to X \neq Y$
	angmgmaddeu.4	$⊢ φ \to Y \neq Z$
	angmgmaddeu1.1	$⊢ φ \to \neg X \in (Y L Z)$
	angmgmaddeu1.2	$⊢ φ \to \neg U \in (V L W)$
Assertion	angmgmaddeu1	$⊢ φ \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)$

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		angmgmaddov.u	$⊢ φ \to U \in P$
9		angmgmaddov.v	$⊢ φ \to V \in P$
10		angmgmaddov.w	$⊢ φ \to W \in P$
11		angmgmaddov.x	$⊢ φ \to X \in P$
12		angmgmaddov.y	$⊢ φ \to Y \in P$
13		angmgmaddov.z	$⊢ φ \to Z \in P$
14		angmgmaddeu.1	$⊢ φ \to U \neq V$
15		angmgmaddeu.2	$⊢ φ \to V \neq W$
16		angmgmaddeu.3	$⊢ φ \to X \neq Y$
17		angmgmaddeu.4	$⊢ φ \to Y \neq Z$
18		angmgmaddeu1.1	$⊢ φ \to \neg X \in (Y L Z)$
19		angmgmaddeu1.2	$⊢ φ \to \neg U \in (V L W)$
20		eqid	$⊢ {hl}_{𝒢} (G) = {hl}_{𝒢} (G)$
21	7	ad3antrrr	$⊢ (((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \to G \in 𝒢_{Tarski}$
22		simpllr	$⊢ (((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \to w \in P$
23	9	ad3antrrr	$⊢ (((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \to V \in P$
24	8	ad3antrrr	$⊢ (((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \to U \in P$
25	13	ad3antrrr	$⊢ (((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \to Z \in P$
26	12	ad3antrrr	$⊢ (((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \to Y \in P$
27	15	neneqd	$⊢ φ \to \neg V = W$
28		ioran	$⊢ \neg (U \in (V L W) \lor V = W) \leftrightarrow (\neg U \in (V L W) \land \neg V = W)$
29	19 27 28	sylanbrc	$⊢ φ \to \neg (U \in (V L W) \lor V = W)$
30	1 6 3 7 9 10 8 29	ncolrot2	$⊢ φ \to \neg (W \in (U L V) \lor U = V)$
31	1 6 3 7 8 9 10 30	ncoltgdim2	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
32		eqid	$⊢ {lInv}_{𝒢} (G) (Y L Z) = {lInv}_{𝒢} (G) (Y L Z)$
33	1 3 6 7 12 13 17	tgelrnln	$⊢ φ \to Y L Z \in ran L$
34	1 4 3 7 31 32 6 33 11	lmicl	$⊢ φ \to {lInv}_{𝒢} (G) (Y L Z) (X) \in P$
35	34	ad3antrrr	$⊢ (((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \to {lInv}_{𝒢} (G) (Y L Z) (X) \in P$
36	30	ad3antrrr	$⊢ (((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \to \neg (W \in (U L V) \lor U = V)$
37	21	adantr	$⊢ ((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land (w \in (V L U) \lor V = U)) \to G \in 𝒢_{Tarski}$
38	23	adantr	$⊢ ((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land (w \in (V L U) \lor V = U)) \to V \in P$
39	24	adantr	$⊢ ((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land (w \in (V L U) \lor V = U)) \to U \in P$
40	14	neneqd	$⊢ φ \to \neg U = V$
41	40	neqcomd	$⊢ φ \to \neg V = U$
42	41	neqned	$⊢ φ \to V \neq U$
43	42	ad4antr	$⊢ ((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land (w \in (V L U) \lor V = U)) \to V \neq U$
44	22	adantr	$⊢ ((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land (w \in (V L U) \lor V = U)) \to w \in P$
45		simpr	$⊢ (((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \to V \underset{˙}{-} w = Y \underset{˙}{-} Z$
46	45	eqcomd	$⊢ (((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \to Y \underset{˙}{-} Z = V \underset{˙}{-} w$
47	17	ad3antrrr	$⊢ (((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \to Y \neq Z$
48	1 4 3 21 26 25 23 22 46 47	tgcgrneq	$⊢ (((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \to V \neq w$
49	48	necomd	$⊢ (((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \to w \neq V$
50	49	adantr	$⊢ ((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land (w \in (V L U) \lor V = U)) \to w \neq V$
51		simpr	$⊢ ((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land (w \in (V L U) \lor V = U)) \to (w \in (V L U) \lor V = U)$
52	41	ad4antr	$⊢ ((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land (w \in (V L U) \lor V = U)) \to \neg V = U$
53	51 52	olcnd	$⊢ ((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land (w \in (V L U) \lor V = U)) \to w \in (V L U)$
54	10	ad4antr	$⊢ ((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land (w \in (V L U) \lor V = U)) \to W \in P$
55	10	ad3antrrr	$⊢ (((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \to W \in P$
56		simplr	$⊢ (((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \to w {hl}_{𝒢} (G) (V) W$
57	1 3 20 22 55 23 21 56	hlcomd	$⊢ (((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \to W {hl}_{𝒢} (G) (V) w$
58	1 3 20 55 22 23 21 6 57	hlln	$⊢ (((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \to W \in (w L V)$
59	1 3 6 21 23 22 55 48 58	lncom	$⊢ (((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \to W \in (V L w)$
60	59	adantr	$⊢ ((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land (w \in (V L U) \lor V = U)) \to W \in (V L w)$
61	1 3 6 37 38 39 43 44 50 53 54 60	tglineeltr	$⊢ ((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land (w \in (V L U) \lor V = U)) \to W \in (V L U)$
62	1 3 6 7 9 8 42	tglinecom	$⊢ φ \to V L U = U L V$
63	62	ad4antr	$⊢ ((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land (w \in (V L U) \lor V = U)) \to V L U = U L V$
64	61 63	eleqtrd	$⊢ ((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land (w \in (V L U) \lor V = U)) \to W \in (U L V)$
65	64	orcd	$⊢ ((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land (w \in (V L U) \lor V = U)) \to (W \in (U L V) \lor U = V)$
66	36 65	mtand	$⊢ (((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \to \neg (w \in (V L U) \lor V = U)$
67		eleq1	$⊢ a = c \to (a \in (P ∖ (Y L Z)) \leftrightarrow c \in (P ∖ (Y L Z)))$
68	67	adantr	$⊢ (a = c \land b = d) \to (a \in (P ∖ (Y L Z)) \leftrightarrow c \in (P ∖ (Y L Z)))$
69		eleq1	$⊢ b = d \to (b \in (P ∖ (Y L Z)) \leftrightarrow d \in (P ∖ (Y L Z)))$
70	69	adantl	$⊢ (a = c \land b = d) \to (b \in (P ∖ (Y L Z)) \leftrightarrow d \in (P ∖ (Y L Z)))$
71	68 70	anbi12d	$⊢ (a = c \land b = d) \to ((a \in (P ∖ (Y L Z)) \land b \in (P ∖ (Y L Z))) \leftrightarrow (c \in (P ∖ (Y L Z)) \land d \in (P ∖ (Y L Z))))$
72		oveq12	$⊢ (a = c \land b = d) \to a I b = c I d$
73	72	eleq2d	$⊢ (a = c \land b = d) \to (s \in (a I b) \leftrightarrow s \in (c I d))$
74	73	rexbidv	$⊢ (a = c \land b = d) \to (\exists s \in (Y L Z) s \in (a I b) \leftrightarrow \exists s \in (Y L Z) s \in (c I d))$
75		eleq1	$⊢ s = t \to (s \in (c I d) \leftrightarrow t \in (c I d))$
76	75	cbvrexvw	$⊢ \exists s \in (Y L Z) s \in (c I d) \leftrightarrow \exists t \in (Y L Z) t \in (c I d)$
77	74 76	bitrdi	$⊢ (a = c \land b = d) \to (\exists s \in (Y L Z) s \in (a I b) \leftrightarrow \exists t \in (Y L Z) t \in (c I d))$
78	71 77	anbi12d	$⊢ (a = c \land b = d) \to (((a \in (P ∖ (Y L Z)) \land b \in (P ∖ (Y L Z))) \land \exists s \in (Y L Z) s \in (a I b)) \leftrightarrow ((c \in (P ∖ (Y L Z)) \land d \in (P ∖ (Y L Z))) \land \exists t \in (Y L Z) t \in (c I d)))$
79	78	cbvopabv	$⊢ \{⟨a, b⟩ \| ((a \in (P ∖ (Y L Z)) \land b \in (P ∖ (Y L Z))) \land \exists s \in (Y L Z) s \in (a I b))\} = \{⟨c, d⟩ \| ((c \in (P ∖ (Y L Z)) \land d \in (P ∖ (Y L Z))) \land \exists t \in (Y L Z) t \in (c I d))\}$
80	1 4 3 6 7 31 33 79 32 11 18	lmiopp	$⊢ φ \to X \{⟨a, b⟩ \| ((a \in (P ∖ (Y L Z)) \land b \in (P ∖ (Y L Z))) \land \exists s \in (Y L Z) s \in (a I b))\} {lInv}_{𝒢} (G) (Y L Z) (X)$
81	1 4 3 79 6 33 7 11 34 80	oppne2	$⊢ φ \to \neg {lInv}_{𝒢} (G) (Y L Z) (X) \in (Y L Z)$
82	1 3 6 7 12 13 17	tglinecom	$⊢ φ \to Y L Z = Z L Y$
83	81 82	neleqtrd	$⊢ φ \to \neg {lInv}_{𝒢} (G) (Y L Z) (X) \in (Z L Y)$
84	17	necomd	$⊢ φ \to Z \neq Y$
85	84	neneqd	$⊢ φ \to \neg Z = Y$
86		ioran	$⊢ \neg ({lInv}_{𝒢} (G) (Y L Z) (X) \in (Z L Y) \lor Z = Y) \leftrightarrow (\neg {lInv}_{𝒢} (G) (Y L Z) (X) \in (Z L Y) \land \neg Z = Y)$
87	83 85 86	sylanbrc	$⊢ φ \to \neg ({lInv}_{𝒢} (G) (Y L Z) (X) \in (Z L Y) \lor Z = Y)$
88	1 6 3 7 13 12 34 87	ncolrot1	$⊢ φ \to \neg (Z \in (Y L {lInv}_{𝒢} (G) (Y L Z) (X)) \lor Y = {lInv}_{𝒢} (G) (Y L Z) (X))$
89	88	ad3antrrr	$⊢ (((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \to \neg (Z \in (Y L {lInv}_{𝒢} (G) (Y L Z) (X)) \lor Y = {lInv}_{𝒢} (G) (Y L Z) (X))$
90	1 4 3 21 23 22 26 25 45	tgcgrcomlr	$⊢ (((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \to w \underset{˙}{-} V = Z \underset{˙}{-} Y$
91	1 4 3 6 20 21 22 23 24 25 26 35 66 89 90	trgcopyeu	$⊢ (((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \to \exists! s \in P (⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩ \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X))$
92	5	eqcomi	$⊢ \sim_{𝒢}^{∠} (G) = \underset{˙}{\sim}$
93	92	a1i	$⊢ ((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X)) \to \sim_{𝒢}^{∠} (G) = \underset{˙}{\sim}$
94	21	ad3antrrr	$⊢ ((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X)) \to G \in 𝒢_{Tarski}$
95	25	ad3antrrr	$⊢ ((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X)) \to Z \in P$
96	26	ad3antrrr	$⊢ ((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X)) \to Y \in P$
97		simpllr	$⊢ ((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X)) \to s \in P$
98	24	ad3antrrr	$⊢ ((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X)) \to U \in P$
99	23	ad3antrrr	$⊢ ((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X)) \to V \in P$
100	22	ad3antrrr	$⊢ ((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X)) \to w \in P$
101	14	ad6antr	$⊢ ((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X)) \to U \neq V$
102	48	ad3antrrr	$⊢ ((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X)) \to V \neq w$
103	1 3 94 20 98 99 100 101 102	cgraswap	$⊢ ((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X)) \to ⟨“ U V w ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ w V U ”⟩$
104	49	ad3antrrr	$⊢ ((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X)) \to w \neq V$
105	42	ad6antr	$⊢ ((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X)) \to V \neq U$
106		simplr	$⊢ ((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X)) \to ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩$
107	1 3 94 20 100 99 98 95 96 97 104 105 106	cgrcgra	$⊢ ((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X)) \to ⟨“ w V U ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ Z Y s ”⟩$
108	1 3 94 20 98 99 100 100 99 98 103 95 96 97 107	cgratr	$⊢ ((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X)) \to ⟨“ U V w ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ Z Y s ”⟩$
109	1 3 94 20 98 99 100 95 96 97 108	cgracom	$⊢ ((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X)) \to ⟨“ Z Y s ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ U V w ”⟩$
110	55	ad3antrrr	$⊢ ((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X)) \to W \in P$
111	57	ad3antrrr	$⊢ ((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X)) \to W {hl}_{𝒢} (G) (V) w$
112	1 3 20 94 95 96 97 98 99 100 109 110 111	cgrahl2	$⊢ ((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X)) \to ⟨“ Z Y s ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ U V W ”⟩$
113	93 112	breqdi	$⊢ ((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X)) \to ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩$
114		eqid	$⊢ \sim_{𝒢} (G) = \sim_{𝒢} (G)$
115	1 4 3 114 94 100 99 98 95 96 97 106	cgr3simp2	$⊢ ((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X)) \to V \underset{˙}{-} U = Y \underset{˙}{-} s$
116	115	eqcomd	$⊢ ((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X)) \to Y \underset{˙}{-} s = V \underset{˙}{-} U$
117	33	ad6antr	$⊢ ((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X)) \to Y L Z \in ran L$
118	11	ad3antrrr	$⊢ (((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \to X \in P$
119	118	ad3antrrr	$⊢ ((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X)) \to X \in P$
120	35	ad3antrrr	$⊢ ((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X)) \to {lInv}_{𝒢} (G) (Y L Z) (X) \in P$
121		eqidd	$⊢ φ \to {hp}_{𝒢} (G) = {hp}_{𝒢} (G)$
122	121 82	fveq12d	$⊢ φ \to {hp}_{𝒢} (G) (Y L Z) = {hp}_{𝒢} (G) (Z L Y)$
123	122	eqcomd	$⊢ φ \to {hp}_{𝒢} (G) (Z L Y) = {hp}_{𝒢} (G) (Y L Z)$
124	123	ad6antr	$⊢ ((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X)) \to {hp}_{𝒢} (G) (Z L Y) = {hp}_{𝒢} (G) (Y L Z)$
125		simpr	$⊢ ((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X)) \to s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X)$
126	124 125	breqdi	$⊢ ((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X)) \to s {hp}_{𝒢} (G) (Y L Z) {lInv}_{𝒢} (G) (Y L Z) (X)$
127	1 3 6 94 117 97 79 120 126	hpgcom	$⊢ ((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X)) \to {lInv}_{𝒢} (G) (Y L Z) (X) {hp}_{𝒢} (G) (Y L Z) s$
128	21	ad2antrr	$⊢ (((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \to G \in 𝒢_{Tarski}$
129	33	ad5antr	$⊢ (((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \to Y L Z \in ran L$
130	35	ad2antrr	$⊢ (((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \to {lInv}_{𝒢} (G) (Y L Z) (X) \in P$
131		simplr	$⊢ (((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \to s \in P$
132	118	ad2antrr	$⊢ (((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \to X \in P$
133	80	ad5antr	$⊢ (((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \to X \{⟨a, b⟩ \| ((a \in (P ∖ (Y L Z)) \land b \in (P ∖ (Y L Z))) \land \exists s \in (Y L Z) s \in (a I b))\} {lInv}_{𝒢} (G) (Y L Z) (X)$
134	1 4 3 79 6 129 128 132 130 133	oppcom	$⊢ (((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \to {lInv}_{𝒢} (G) (Y L Z) (X) \{⟨a, b⟩ \| ((a \in (P ∖ (Y L Z)) \land b \in (P ∖ (Y L Z))) \land \exists s \in (Y L Z) s \in (a I b))\} X$
135	1 3 6 79 128 129 130 131 132 134	lnopp2hpgb	$⊢ (((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \to (s \{⟨a, b⟩ \| ((a \in (P ∖ (Y L Z)) \land b \in (P ∖ (Y L Z))) \land \exists s \in (Y L Z) s \in (a I b))\} X \leftrightarrow {lInv}_{𝒢} (G) (Y L Z) (X) {hp}_{𝒢} (G) (Y L Z) s)$
136	135	adantr	$⊢ ((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X)) \to (s \{⟨a, b⟩ \| ((a \in (P ∖ (Y L Z)) \land b \in (P ∖ (Y L Z))) \land \exists s \in (Y L Z) s \in (a I b))\} X \leftrightarrow {lInv}_{𝒢} (G) (Y L Z) (X) {hp}_{𝒢} (G) (Y L Z) s)$
137	127 136	mpbird	$⊢ ((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X)) \to s \{⟨a, b⟩ \| ((a \in (P ∖ (Y L Z)) \land b \in (P ∖ (Y L Z))) \land \exists s \in (Y L Z) s \in (a I b))\} X$
138	1 3 6 79 94 117 97 119 137	lnoppinn0	$⊢ ((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X)) \to (Y L Z) \cap (s I X) \neq \emptyset$
139	113 116 138	3jca	$⊢ ((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩) \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X)) \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)$
140	139	anasss	$⊢ (((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land (⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩ \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X))) \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)$
141	21	ad4antr	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 G \in 𝒢_{Tarski}$
142	22	ad4antr	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 w \in P$
143	23	ad4antr	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 V \in P$
144	24	ad4antr	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 U \in P$
145	25	ad4antr	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 Z \in P$
146	26	ad4antr	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 Y \in P$
147		simp-4r	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 s \in P$
148	90	ad4antr	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 w \underset{˙}{-} V = Z \underset{˙}{-} Y$
149		simplr	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 Y \underset{˙}{-} s = V \underset{˙}{-} U$
150	149	eqcomd	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 V \underset{˙}{-} U = Y \underset{˙}{-} s$
151	55	ad4antr	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 W \in P$
152	42	ad7antr	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 V \neq U$
153	1 4 3 141 143 144 146 147 150 152	tgcgrneq	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 Y \neq s$
154	153	necomd	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 s \neq Y$
155	47	ad4antr	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 Y \neq Z$
156	1 3 141 20 147 146 145 154 155	cgraswap	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 ⟨“ s Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ Z Y s ”⟩$
157	5	a1i	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
158		simpllr	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 ⟨“ Z Y s ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩$
159	157 158	breqdi	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 ⟨“ Z Y s ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ U V W ”⟩$
160	1 3 141 20 147 146 145 145 146 147 156 144 143 151 159	cgratr	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 ⟨“ s Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ U V W ”⟩$
161	1 3 141 20 147 146 145 144 143 151 160	cgracom	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 ⟨“ U V W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ s Y Z ”⟩$
162	118	ad4antr	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 X \in P$
163	14	ad7antr	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 U \neq V$
164	1 3 20 144 162 143 141 163	hlid	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 U {hl}_{𝒢} (G) (V) U$
165	56	ad4antr	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 w {hl}_{𝒢} (G) (V) W$
166	45	ad4antr	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 V \underset{˙}{-} w = Y \underset{˙}{-} Z$
167	1 3 20 141 144 143 151 147 146 145 161 144 4 142 164 165 150 166	cgracgr	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 U \underset{˙}{-} w = s \underset{˙}{-} Z$
168	1 4 114 141 142 143 144 145 146 147 148 150 167	trgcgr	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 ⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩$
169	122	ad7antr	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 {hp}_{𝒢} (G) (Y L Z) = {hp}_{𝒢} (G) (Z L Y)$
170	33	ad7antr	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 Y L Z \in ran L$
171	35	ad4antr	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 {lInv}_{𝒢} (G) (Y L Z) (X) \in P$
172		simpr	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 (Y L Z) \cap (s I X) \neq \emptyset$
173	147	adantr	$⊢ ((((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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) \land r \in ((Y L Z) \cap (s I X))) \to s \in P$
174	162	adantr	$⊢ ((((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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) \land r \in ((Y L Z) \cap (s I X))) \to X \in P$
175		simpr	$⊢ ((((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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) \land r \in ((Y L Z) \cap (s I X))) \to r \in ((Y L Z) \cap (s I X))$
176	175	elin1d	$⊢ ((((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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) \land r \in ((Y L Z) \cap (s I X))) \to r \in (Y L Z)$
177	36	ad4antr	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 \neg (W \in (U L V) \lor U = V)$
178	1 3 4 141 144 143 151 147 146 145 161 6 177	cgrancol	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 \neg (Z \in (s L Y) \lor s = Y)$
179	1 6 3 141 147 146 145 178	ncolrot1	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 \neg (s \in (Y L Z) \lor Y = Z)$
180	179	orsild	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 \neg s \in (Y L Z)$
181	180	adantr	$⊢ ((((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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) \land r \in ((Y L Z) \cap (s I X))) \to \neg s \in (Y L Z)$
182	18	ad8antr	$⊢ ((((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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) \land r \in ((Y L Z) \cap (s I X))) \to \neg X \in (Y L Z)$
183	175	elin2d	$⊢ ((((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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) \land r \in ((Y L Z) \cap (s I X))) \to r \in (s I X)$
184	1 4 3 79 173 174 176 181 182 183	islnoppd	$⊢ ((((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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) \land r \in ((Y L Z) \cap (s I X))) \to s \{⟨a, b⟩ \| ((a \in (P ∖ (Y L Z)) \land b \in (P ∖ (Y L Z))) \land \exists s \in (Y L Z) s \in (a I b))\} X$
185	172 184	n0limd	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 s \{⟨a, b⟩ \| ((a \in (P ∖ (Y L Z)) \land b \in (P ∖ (Y L Z))) \land \exists s \in (Y L Z) s \in (a I b))\} X$
186	80	ad7antr	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 X \{⟨a, b⟩ \| ((a \in (P ∖ (Y L Z)) \land b \in (P ∖ (Y L Z))) \land \exists s \in (Y L Z) s \in (a I b))\} {lInv}_{𝒢} (G) (Y L Z) (X)$
187	1 4 3 79 6 170 141 162 171 186	oppcom	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 {lInv}_{𝒢} (G) (Y L Z) (X) \{⟨a, b⟩ \| ((a \in (P ∖ (Y L Z)) \land b \in (P ∖ (Y L Z))) \land \exists s \in (Y L Z) s \in (a I b))\} X$
188	1 3 6 79 141 170 171 147 162 187	lnopp2hpgb	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 (s \{⟨a, b⟩ \| ((a \in (P ∖ (Y L Z)) \land b \in (P ∖ (Y L Z))) \land \exists s \in (Y L Z) s \in (a I b))\} X \leftrightarrow {lInv}_{𝒢} (G) (Y L Z) (X) {hp}_{𝒢} (G) (Y L Z) s)$
189	185 188	mpbid	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 {lInv}_{𝒢} (G) (Y L Z) (X) {hp}_{𝒢} (G) (Y L Z) s$
190	1 3 6 141 170 171 79 147 189	hpgcom	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 s {hp}_{𝒢} (G) (Y L Z) {lInv}_{𝒢} (G) (Y L Z) (X)$
191	169 190	breqdi	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X)$
192	168 191	jca	$⊢ (((((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land ⟨“ 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 (⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩ \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X))$
193	192	3anasss	$⊢ (((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \land (⟨“ 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 (⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩ \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X))$
194	140 193	impbida	$⊢ ((((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \land s \in P) \to ((⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩ \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X)) \leftrightarrow (⟨“ 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))$
195	194	reubidva	$⊢ (((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} Z) \to (\exists! s \in P (⟨“ w V U ”⟩ \sim_{𝒢} (G) ⟨“ Z Y s ”⟩ \land s {hp}_{𝒢} (G) (Z L Y) {lInv}_{𝒢} (G) (Y L Z) (X)) \leftrightarrow \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))$
196	91 195	mpbid	$⊢ (((φ \land w \in P) \land w {hl}_{𝒢} (G) (V) W) \land V \underset{˙}{-} w = Y \underset{˙}{-} 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)$
197	196	anasss	$⊢ ((φ \land w \in P) \land (w {hl}_{𝒢} (G) (V) W \land V \underset{˙}{-} w = Y \underset{˙}{-} 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)$
198	15	necomd	$⊢ φ \to W \neq V$
199	1 3 20 9 12 13 7 10 4 198 17	hlcgrex	$⊢ φ \to \exists w \in P (w {hl}_{𝒢} (G) (V) W \land V \underset{˙}{-} w = Y \underset{˙}{-} Z)$
200	197 199	r19.29a	$⊢ φ \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)$

Metamath Proof Explorer

Theorem angmgmaddeu1

Proof