tgaaddcpbl

Description: The angular addition is compatible with angle congruence: by adding congruent angles together, we obtain congruent angles. Theorem 11.22 of Schwabhauser p. 99. The angles <" X Y S "> and <" S Y Z "> are added to result in <" X Y Z "> , and <" U V T "> and <" T V W "> are added to result in <" U V W "> . (Contributed by Thierry Arnoux, 2-Aug-2026)

	Ref	Expression
Hypotheses	tgaaddcpbl.p	$⊢ P = {Base}_{G}$
	tgaaddcpbl.i	$⊢ I = Itv (G)$
	tgaaddcpbl.l	$⊢ L = {Line}_{𝒢} (G)$
	tgaaddcpbl.c	$⊢ \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
	tgaaddcpbl.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ (Y L S)) \land b \in (P ∖ (Y L S))) \land \exists s \in (Y L S) s \in (a I b))\}$
	tgaaddcpbl.q	$⊢ Q = \{⟨c, d⟩ \| ((c \in (P ∖ (V L T)) \land d \in (P ∖ (V L T))) \land \exists t \in (V L T) t \in (c I d))\}$
	tgaaddcpbl.1	$⊢ φ \to G \in 𝒢_{Tarski}$
	tgaaddcpbl.s	$⊢ φ \to S \in P$
	tgaaddcpbl.t	$⊢ φ \to T \in P$
	tgaaddcpbl.u	$⊢ φ \to U \in P$
	tgaaddcpbl.v	$⊢ φ \to V \in P$
	tgaaddcpbl.w	$⊢ φ \to W \in P$
	tgaaddcpbl.x	$⊢ φ \to X \in P$
	tgaaddcpbl.y	$⊢ φ \to Y \in P$
	tgaaddcpbl.z	$⊢ φ \to Z \in P$
	tgaaddcpbl.2	$⊢ φ \to Y \neq S$
	tgaaddcpbl.3	$⊢ φ \to V \neq T$
	tgaaddcpbl.4	$⊢ φ \to X O Z$
	tgaaddcpbl.5	$⊢ φ \to U Q W$
	tgaaddcpbl.6	$⊢ φ \to ⟨“ X Y S ”⟩ \underset{˙}{\sim} ⟨“ U V T ”⟩$
	tgaaddcpbl.7	$⊢ φ \to ⟨“ S Y Z ”⟩ \underset{˙}{\sim} ⟨“ T V W ”⟩$
Assertion	tgaaddcpbl	$⊢ φ \to ⟨“ X Y Z ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩$

Proof

Step	Hyp	Ref	Expression
1		tgaaddcpbl.p	$⊢ P = {Base}_{G}$
2		tgaaddcpbl.i	$⊢ I = Itv (G)$
3		tgaaddcpbl.l	$⊢ L = {Line}_{𝒢} (G)$
4		tgaaddcpbl.c	$⊢ \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
5		tgaaddcpbl.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ (Y L S)) \land b \in (P ∖ (Y L S))) \land \exists s \in (Y L S) s \in (a I b))\}$
6		tgaaddcpbl.q	$⊢ Q = \{⟨c, d⟩ \| ((c \in (P ∖ (V L T)) \land d \in (P ∖ (V L T))) \land \exists t \in (V L T) t \in (c I d))\}$
7		tgaaddcpbl.1	$⊢ φ \to G \in 𝒢_{Tarski}$
8		tgaaddcpbl.s	$⊢ φ \to S \in P$
9		tgaaddcpbl.t	$⊢ φ \to T \in P$
10		tgaaddcpbl.u	$⊢ φ \to U \in P$
11		tgaaddcpbl.v	$⊢ φ \to V \in P$
12		tgaaddcpbl.w	$⊢ φ \to W \in P$
13		tgaaddcpbl.x	$⊢ φ \to X \in P$
14		tgaaddcpbl.y	$⊢ φ \to Y \in P$
15		tgaaddcpbl.z	$⊢ φ \to Z \in P$
16		tgaaddcpbl.2	$⊢ φ \to Y \neq S$
17		tgaaddcpbl.3	$⊢ φ \to V \neq T$
18		tgaaddcpbl.4	$⊢ φ \to X O Z$
19		tgaaddcpbl.5	$⊢ φ \to U Q W$
20		tgaaddcpbl.6	$⊢ φ \to ⟨“ X Y S ”⟩ \underset{˙}{\sim} ⟨“ U V T ”⟩$
21		tgaaddcpbl.7	$⊢ φ \to ⟨“ S Y Z ”⟩ \underset{˙}{\sim} ⟨“ T V W ”⟩$
22	4	a1i	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
23	22	eqcomd	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to \sim_{𝒢}^{∠} (G) = \underset{˙}{\sim}$
24		eqid	$⊢ {hl}_{𝒢} (G) = {hl}_{𝒢} (G)$
25	7	ad4antr	$⊢ ((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \to G \in 𝒢_{Tarski}$
26	25	ad3antrrr	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to G \in 𝒢_{Tarski}$
27	13	ad7antr	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to X \in P$
28	14	ad4antr	$⊢ ((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \to Y \in P$
29	28	ad3antrrr	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to Y \in P$
30	15	ad4antr	$⊢ ((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \to Z \in P$
31	30	ad3antrrr	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to Z \in P$
32	10	ad7antr	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to U \in P$
33	11	ad4antr	$⊢ ((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \to V \in P$
34	33	ad3antrrr	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to V \in P$
35		simpllr	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to w \in P$
36		eqid	$⊢ dist (G) = dist (G)$
37		simp-7r	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to Y \in (X I Z)$
38		simpllr	$⊢ ((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \to u \in P$
39	38	ad3antrrr	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to u \in P$
40		simp-5r	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to u {hl}_{𝒢} (G) (V) U$
41		simplr	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to V \in (u I w)$
42	1 2 24 39 32 35 26 34 40 41	btwnhl	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to V \in (U I w)$
43	1 2 3 7 14 8 16	tglinerflx1	$⊢ φ \to Y \in (Y L S)$
44	1 2 3 7 14 8 16	tgelrnln	$⊢ φ \to Y L S \in ran L$
45	1 36 2 5 3 44 7 13 15 18	oppne1	$⊢ φ \to \neg X \in (Y L S)$
46		nelne2	$⊢ (Y \in (Y L S) \land \neg X \in (Y L S)) \to Y \neq X$
47	43 45 46	syl2anc	$⊢ φ \to Y \neq X$
48	47	necomd	$⊢ φ \to X \neq Y$
49	48	ad7antr	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to X \neq Y$
50	1 36 2 5 3 44 7 13 15 18	oppne2	$⊢ φ \to \neg Z \in (Y L S)$
51		nelne2	$⊢ (Y \in (Y L S) \land \neg Z \in (Y L S)) \to Y \neq Z$
52	43 50 51	syl2anc	$⊢ φ \to Y \neq Z$
53	52	necomd	$⊢ φ \to Z \neq Y$
54	53	ad7antr	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to Z \neq Y$
55	1 2 3 7 11 9 17	tglinerflx1	$⊢ φ \to V \in (V L T)$
56	1 36 2 6 10 12	islnopp	$⊢ φ \to (U Q W \leftrightarrow ((\neg U \in (V L T) \land \neg W \in (V L T)) \land \exists t \in (V L T) t \in (U I W)))$
57	19 56	mpbid	$⊢ φ \to ((\neg U \in (V L T) \land \neg W \in (V L T)) \land \exists t \in (V L T) t \in (U I W))$
58	57	simplld	$⊢ φ \to \neg U \in (V L T)$
59		nelne2	$⊢ (V \in (V L T) \land \neg U \in (V L T)) \to V \neq U$
60	55 58 59	syl2anc	$⊢ φ \to V \neq U$
61	60	necomd	$⊢ φ \to U \neq V$
62	61	ad7antr	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to U \neq V$
63		simpr	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to V dist (G) w = Y dist (G) Z$
64	63	eqcomd	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to Y dist (G) Z = V dist (G) w$
65	52	ad7antr	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to Y \neq Z$
66	1 36 2 26 29 31 34 35 64 65	tgcgrneq	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to V \neq w$
67	66	necomd	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to w \neq V$
68	1 2 36 26 27 29 31 32 34 35 37 42 49 54 62 67	flatcgra	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ U V w ”⟩$
69	12	ad7antr	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to W \in P$
70	8	ad7antr	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to S \in P$
71	9	ad7antr	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to T \in P$
72		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
73		eqid	$⊢ {pInv}_{𝒢} (G) (T) = {pInv}_{𝒢} (G) (T)$
74	1 36 2 3 72 7 9 73 10	mircl	$⊢ φ \to {pInv}_{𝒢} (G) (T) (U) \in P$
75	74	ad7antr	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to {pInv}_{𝒢} (G) (T) (U) \in P$
76	7	adantr	$⊢ (φ \land S \in (Y L Z)) \to G \in 𝒢_{Tarski}$
77	14	adantr	$⊢ (φ \land S \in (Y L Z)) \to Y \in P$
78	8	adantr	$⊢ (φ \land S \in (Y L Z)) \to S \in P$
79	15	adantr	$⊢ (φ \land S \in (Y L Z)) \to Z \in P$
80	16	adantr	$⊢ (φ \land S \in (Y L Z)) \to Y \neq S$
81		simpr	$⊢ (φ \land S \in (Y L Z)) \to S \in (Y L Z)$
82	52	adantr	$⊢ (φ \land S \in (Y L Z)) \to Y \neq Z$
83	1 2 3 76 77 79 82	tglinecom	$⊢ (φ \land S \in (Y L Z)) \to Y L Z = Z L Y$
84	81 83	eleqtrd	$⊢ (φ \land S \in (Y L Z)) \to S \in (Z L Y)$
85	53	adantr	$⊢ (φ \land S \in (Y L Z)) \to Z \neq Y$
86	1 2 3 76 77 78 79 80 84 85	lnrot1	$⊢ (φ \land S \in (Y L Z)) \to Z \in (Y L S)$
87	50 86	mtand	$⊢ φ \to \neg S \in (Y L Z)$
88	52	neneqd	$⊢ φ \to \neg Y = Z$
89		ioran	$⊢ \neg (S \in (Y L Z) \lor Y = Z) \leftrightarrow (\neg S \in (Y L Z) \land \neg Y = Z)$
90	87 88 89	sylanbrc	$⊢ φ \to \neg (S \in (Y L Z) \lor Y = Z)$
91	90	ad7antr	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to \neg (S \in (Y L Z) \lor Y = Z)$
92	7	adantr	$⊢ (φ \land (T \in (V L {pInv}_{𝒢} (G) (T) (U)) \lor V = {pInv}_{𝒢} (G) (T) (U))) \to G \in 𝒢_{Tarski}$
93	9	adantr	$⊢ (φ \land (T \in (V L {pInv}_{𝒢} (G) (T) (U)) \lor V = {pInv}_{𝒢} (G) (T) (U))) \to T \in P$
94	10	adantr	$⊢ (φ \land (T \in (V L {pInv}_{𝒢} (G) (T) (U)) \lor V = {pInv}_{𝒢} (G) (T) (U))) \to U \in P$
95	1 36 2 3 72 92 93 73 94	mirmir	$⊢ (φ \land (T \in (V L {pInv}_{𝒢} (G) (T) (U)) \lor V = {pInv}_{𝒢} (G) (T) (U))) \to {pInv}_{𝒢} (G) (T) ({pInv}_{𝒢} (G) (T) (U)) = U$
96	1 2 3 7 11 9 17	tgelrnln	$⊢ φ \to V L T \in ran L$
97	96	adantr	$⊢ (φ \land (T \in (V L {pInv}_{𝒢} (G) (T) (U)) \lor V = {pInv}_{𝒢} (G) (T) (U))) \to V L T \in ran L$
98	1 2 3 7 11 9 17	tglinerflx2	$⊢ φ \to T \in (V L T)$
99	98	adantr	$⊢ (φ \land (T \in (V L {pInv}_{𝒢} (G) (T) (U)) \lor V = {pInv}_{𝒢} (G) (T) (U))) \to T \in (V L T)$
100	74	adantr	$⊢ (φ \land (T \in (V L {pInv}_{𝒢} (G) (T) (U)) \lor V = {pInv}_{𝒢} (G) (T) (U))) \to {pInv}_{𝒢} (G) (T) (U) \in P$
101	11	adantr	$⊢ (φ \land (T \in (V L {pInv}_{𝒢} (G) (T) (U)) \lor V = {pInv}_{𝒢} (G) (T) (U))) \to V \in P$
102		simpr	$⊢ (φ \land (T \in (V L {pInv}_{𝒢} (G) (T) (U)) \lor V = {pInv}_{𝒢} (G) (T) (U))) \to (T \in (V L {pInv}_{𝒢} (G) (T) (U)) \lor V = {pInv}_{𝒢} (G) (T) (U))$
103	1 3 2 92 101 100 93 102	colcom	$⊢ (φ \land (T \in (V L {pInv}_{𝒢} (G) (T) (U)) \lor V = {pInv}_{𝒢} (G) (T) (U))) \to (T \in ({pInv}_{𝒢} (G) (T) (U) L V) \lor {pInv}_{𝒢} (G) (T) (U) = V)$
104	1 3 2 92 100 101 93 103	colrot1	$⊢ (φ \land (T \in (V L {pInv}_{𝒢} (G) (T) (U)) \lor V = {pInv}_{𝒢} (G) (T) (U))) \to ({pInv}_{𝒢} (G) (T) (U) \in (V L T) \lor V = T)$
105	17	neneqd	$⊢ φ \to \neg V = T$
106	105	adantr	$⊢ (φ \land (T \in (V L {pInv}_{𝒢} (G) (T) (U)) \lor V = {pInv}_{𝒢} (G) (T) (U))) \to \neg V = T$
107	104 106	olcnd	$⊢ (φ \land (T \in (V L {pInv}_{𝒢} (G) (T) (U)) \lor V = {pInv}_{𝒢} (G) (T) (U))) \to {pInv}_{𝒢} (G) (T) (U) \in (V L T)$
108	1 36 2 3 72 92 73 97 99 107	mirln	$⊢ (φ \land (T \in (V L {pInv}_{𝒢} (G) (T) (U)) \lor V = {pInv}_{𝒢} (G) (T) (U))) \to {pInv}_{𝒢} (G) (T) ({pInv}_{𝒢} (G) (T) (U)) \in (V L T)$
109	95 108	eqeltrrd	$⊢ (φ \land (T \in (V L {pInv}_{𝒢} (G) (T) (U)) \lor V = {pInv}_{𝒢} (G) (T) (U))) \to U \in (V L T)$
110	58 109	mtand	$⊢ φ \to \neg (T \in (V L {pInv}_{𝒢} (G) (T) (U)) \lor V = {pInv}_{𝒢} (G) (T) (U))$
111	110	ad7antr	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to \neg (T \in (V L {pInv}_{𝒢} (G) (T) (U)) \lor V = {pInv}_{𝒢} (G) (T) (U))$
112	4	a1i	$⊢ φ \to \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
113	112 21	breqdi	$⊢ φ \to ⟨“ S Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ T V W ”⟩$
114	113	ad7antr	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to ⟨“ S Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ T V W ”⟩$
115	112 20	breqdi	$⊢ φ \to ⟨“ X Y S ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ U V T ”⟩$
116	1 2 7 24 13 14 8 10 11 9 115	cgracom	$⊢ φ \to ⟨“ U V T ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y S ”⟩$
117	116	ad7antr	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to ⟨“ U V T ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y S ”⟩$
118	1 2 36 26 32 34 71 27 29 70 35 31 117 42 37 66 65	sacgr	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to ⟨“ w V T ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ Z Y S ”⟩$
119	1 2 36 26 35 34 71 31 29 70 118	cgraswaplr	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to ⟨“ T V w ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ S Y Z ”⟩$
120	1 2 26 24 71 34 35 70 29 31 119	cgracom	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to ⟨“ S Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ T V w ”⟩$
121	1 2 3 7 11 9 17	tglinecom	$⊢ φ \to V L T = T L V$
122	121	fveq2d	$⊢ φ \to {hp}_{𝒢} (G) (V L T) = {hp}_{𝒢} (G) (T L V)$
123	10 58	eldifd	$⊢ φ \to U \in (P ∖ (V L T))$
124	1 2 72 73 6 7 96 98 123 3	oppmir	$⊢ φ \to U Q {pInv}_{𝒢} (G) (T) (U)$
125	1 36 2 6 3 96 7 10 74 124	oppcom	$⊢ φ \to {pInv}_{𝒢} (G) (T) (U) Q U$
126	1 36 2 6 3 96 7 10 12 19	oppcom	$⊢ φ \to W Q U$
127	1 2 3 6 7 96 12 74 10 126	lnopp2hpgb	$⊢ φ \to ({pInv}_{𝒢} (G) (T) (U) Q U \leftrightarrow W {hp}_{𝒢} (G) (V L T) {pInv}_{𝒢} (G) (T) (U))$
128	125 127	mpbid	$⊢ φ \to W {hp}_{𝒢} (G) (V L T) {pInv}_{𝒢} (G) (T) (U)$
129	122 128	breqdi	$⊢ φ \to W {hp}_{𝒢} (G) (T L V) {pInv}_{𝒢} (G) (T) (U)$
130	129	ad7antr	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to W {hp}_{𝒢} (G) (T L V) {pInv}_{𝒢} (G) (T) (U)$
131	122	ad7antr	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to {hp}_{𝒢} (G) (V L T) = {hp}_{𝒢} (G) (T L V)$
132	125	ad7antr	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to {pInv}_{𝒢} (G) (T) (U) Q U$
133	96	ad7antr	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to V L T \in ran L$
134	55	ad7antr	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to V \in (V L T)$
135	25	adantr	$⊢ (((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land u \in (V L T)) \to G \in 𝒢_{Tarski}$
136	33	adantr	$⊢ (((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land u \in (V L T)) \to V \in P$
137	9	ad5antr	$⊢ (((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land u \in (V L T)) \to T \in P$
138	10	ad5antr	$⊢ (((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land u \in (V L T)) \to U \in P$
139	17	ad5antr	$⊢ (((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land u \in (V L T)) \to V \neq T$
140	38	adantr	$⊢ (((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land u \in (V L T)) \to u \in P$
141	13	ad4antr	$⊢ ((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \to X \in P$
142		simpr	$⊢ ((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \to V dist (G) u = Y dist (G) X$
143	142	eqcomd	$⊢ ((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \to Y dist (G) X = V dist (G) u$
144	47	ad4antr	$⊢ ((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \to Y \neq X$
145	1 36 2 25 28 141 33 38 143 144	tgcgrneq	$⊢ ((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \to V \neq u$
146	145	necomd	$⊢ ((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \to u \neq V$
147	146	adantr	$⊢ (((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land u \in (V L T)) \to u \neq V$
148		simpr	$⊢ (((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land u \in (V L T)) \to u \in (V L T)$
149	1 2 3 135 140 136 137 147 148 139	lnrot2	$⊢ (((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land u \in (V L T)) \to T \in (u L V)$
150	61	ad5antr	$⊢ (((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land u \in (V L T)) \to U \neq V$
151	1 2 3 135 140 136 147	tgelrnln	$⊢ (((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land u \in (V L T)) \to u L V \in ran L$
152	10	ad4antr	$⊢ ((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \to U \in P$
153		simplr	$⊢ ((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \to u {hl}_{𝒢} (G) (V) U$
154	1 2 24 38 152 33 25 153	hlcomd	$⊢ ((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \to U {hl}_{𝒢} (G) (V) u$
155	1 2 24 152 38 33 25 3 154	hlln	$⊢ ((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \to U \in (u L V)$
156	155	adantr	$⊢ (((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land u \in (V L T)) \to U \in (u L V)$
157	1 2 3 135 140 136 147	tglinerflx2	$⊢ (((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land u \in (V L T)) \to V \in (u L V)$
158	1 2 3 135 138 136 150 150 151 156 157	tglinethru	$⊢ (((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land u \in (V L T)) \to u L V = U L V$
159	149 158	eleqtrd	$⊢ (((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land u \in (V L T)) \to T \in (U L V)$
160	1 2 3 135 136 137 138 139 159 150	lnrot1	$⊢ (((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land u \in (V L T)) \to U \in (V L T)$
161	58	ad5antr	$⊢ (((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land u \in (V L T)) \to \neg U \in (V L T)$
162	160 161	pm2.65da	$⊢ ((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \to \neg u \in (V L T)$
163	162	ad3antrrr	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to \neg u \in (V L T)$
164	66	neneqd	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to \neg V = w$
165	26	adantr	$⊢ ((((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \land w \in (V L T)) \to G \in 𝒢_{Tarski}$
166	39	adantr	$⊢ ((((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \land w \in (V L T)) \to u \in P$
167	35	adantr	$⊢ ((((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \land w \in (V L T)) \to w \in P$
168	26	adantr	$⊢ ((((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \land u = w) \to G \in 𝒢_{Tarski}$
169	35	adantr	$⊢ ((((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \land u = w) \to w \in P$
170	34	adantr	$⊢ ((((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \land u = w) \to V \in P$
171		simpllr	$⊢ ((((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \land u = w) \to V \in (u I w)$
172		simpr	$⊢ ((((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \land u = w) \to u = w$
173	172	oveq1d	$⊢ ((((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \land u = w) \to u I w = w I w$
174	171 173	eleqtrd	$⊢ ((((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \land u = w) \to V \in (w I w)$
175	1 36 2 168 169 170 174	axtgbtwnid	$⊢ ((((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \land u = w) \to w = V$
176	175	eqcomd	$⊢ ((((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \land u = w) \to V = w$
177	66 176	mteqand	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to u \neq w$
178	177	adantr	$⊢ ((((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \land w \in (V L T)) \to u \neq w$
179	1 2 3 165 166 167 178	tgelrnln	$⊢ ((((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \land w \in (V L T)) \to u L w \in ran L$
180	133	adantr	$⊢ ((((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \land w \in (V L T)) \to V L T \in ran L$
181	1 2 3 165 166 167 178	tglinerflx1	$⊢ ((((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \land w \in (V L T)) \to u \in (u L w)$
182	163	adantr	$⊢ ((((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \land w \in (V L T)) \to \neg u \in (V L T)$
183		nelne1	$⊢ (u \in (u L w) \land \neg u \in (V L T)) \to u L w \neq V L T$
184	181 182 183	syl2anc	$⊢ ((((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \land w \in (V L T)) \to u L w \neq V L T$
185	34	adantr	$⊢ ((((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \land w \in (V L T)) \to V \in P$
186		simpllr	$⊢ ((((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \land w \in (V L T)) \to V \in (u I w)$
187	1 2 3 165 166 167 185 178 186	btwnlng1	$⊢ ((((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \land w \in (V L T)) \to V \in (u L w)$
188	134	adantr	$⊢ ((((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \land w \in (V L T)) \to V \in (V L T)$
189	187 188	elind	$⊢ ((((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \land w \in (V L T)) \to V \in ((u L w) \cap (V L T))$
190	1 2 3 165 166 167 178	tglinerflx2	$⊢ ((((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \land w \in (V L T)) \to w \in (u L w)$
191		simpr	$⊢ ((((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \land w \in (V L T)) \to w \in (V L T)$
192	190 191	elind	$⊢ ((((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \land w \in (V L T)) \to w \in ((u L w) \cap (V L T))$
193	1 2 3 165 179 180 184 189 192	tglineineq	$⊢ ((((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \land w \in (V L T)) \to V = w$
194	164 193	mtand	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to \neg w \in (V L T)$
195	1 36 2 6 39 35 134 163 194 41	islnoppd	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to u Q w$
196	1 36 2 6 3 133 26 24 39 32 35 195 134 40	opphl	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to U Q w$
197	1 36 2 6 3 133 26 32 35 196	oppcom	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to w Q U$
198	1 2 3 6 26 133 35 75 32 197	lnopp2hpgb	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to ({pInv}_{𝒢} (G) (T) (U) Q U \leftrightarrow w {hp}_{𝒢} (G) (V L T) {pInv}_{𝒢} (G) (T) (U))$
199	132 198	mpbid	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to w {hp}_{𝒢} (G) (V L T) {pInv}_{𝒢} (G) (T) (U)$
200	131 199	breqdi	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to w {hp}_{𝒢} (G) (T L V) {pInv}_{𝒢} (G) (T) (U)$
201	1 2 36 26 70 29 31 71 34 75 3 91 111 69 35 24 114 120 130 200	acopyeu	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to W {hl}_{𝒢} (G) (V) w$
202	1 2 24 26 27 29 31 32 34 35 68 69 201	cgrahl2	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ U V W ”⟩$
203	23 202	breqdi	$⊢ (((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land V \in (u I w)) \land V dist (G) w = Y dist (G) Z) \to ⟨“ X Y Z ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩$
204	203	anasss	$⊢ ((((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \land w \in P) \land (V \in (u I w) \land V dist (G) w = Y dist (G) Z)) \to ⟨“ X Y Z ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩$
205	1 36 2 25 38 33 28 30	axtgsegcon	$⊢ ((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \to \exists w \in P (V \in (u I w) \land V dist (G) w = Y dist (G) Z)$
206	204 205	r19.29a	$⊢ ((((φ \land Y \in (X I Z)) \land u \in P) \land u {hl}_{𝒢} (G) (V) U) \land V dist (G) u = Y dist (G) X) \to ⟨“ X Y Z ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩$
207	206	anasss	$⊢ (((φ \land Y \in (X I Z)) \land u \in P) \land (u {hl}_{𝒢} (G) (V) U \land V dist (G) u = Y dist (G) X)) \to ⟨“ X Y Z ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩$
208	1 2 24 11 14 13 7 10 36 61 47	hlcgrex	$⊢ φ \to \exists u \in P (u {hl}_{𝒢} (G) (V) U \land V dist (G) u = Y dist (G) X)$
209	208	adantr	$⊢ (φ \land Y \in (X I Z)) \to \exists u \in P (u {hl}_{𝒢} (G) (V) U \land V dist (G) u = Y dist (G) X)$
210	207 209	r19.29a	$⊢ (φ \land Y \in (X I Z)) \to ⟨“ X Y Z ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩$
211	7	adantr	$⊢ (φ \land \neg Y \in (X I Z)) \to G \in 𝒢_{Tarski}$
212	8	adantr	$⊢ (φ \land \neg Y \in (X I Z)) \to S \in P$
213	9	adantr	$⊢ (φ \land \neg Y \in (X I Z)) \to T \in P$
214	10	adantr	$⊢ (φ \land \neg Y \in (X I Z)) \to U \in P$
215	11	adantr	$⊢ (φ \land \neg Y \in (X I Z)) \to V \in P$
216	12	adantr	$⊢ (φ \land \neg Y \in (X I Z)) \to W \in P$
217	13	adantr	$⊢ (φ \land \neg Y \in (X I Z)) \to X \in P$
218	14	adantr	$⊢ (φ \land \neg Y \in (X I Z)) \to Y \in P$
219	15	adantr	$⊢ (φ \land \neg Y \in (X I Z)) \to Z \in P$
220	16	adantr	$⊢ (φ \land \neg Y \in (X I Z)) \to Y \neq S$
221	17	adantr	$⊢ (φ \land \neg Y \in (X I Z)) \to V \neq T$
222	18	adantr	$⊢ (φ \land \neg Y \in (X I Z)) \to X O Z$
223	19	adantr	$⊢ (φ \land \neg Y \in (X I Z)) \to U Q W$
224	20	adantr	$⊢ (φ \land \neg Y \in (X I Z)) \to ⟨“ X Y S ”⟩ \underset{˙}{\sim} ⟨“ U V T ”⟩$
225	21	adantr	$⊢ (φ \land \neg Y \in (X I Z)) \to ⟨“ S Y Z ”⟩ \underset{˙}{\sim} ⟨“ T V W ”⟩$
226		simpr	$⊢ (φ \land \neg Y \in (X I Z)) \to \neg Y \in (X I Z)$
227	1 2 3 4 5 6 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226	tgaaddcpbllem3	$⊢ (φ \land \neg Y \in (X I Z)) \to ⟨“ X Y Z ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩$
228	210 227	pm2.61dan	$⊢ φ \to ⟨“ X Y Z ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩$

Metamath Proof Explorer

Theorem tgaaddcpbl

Proof