Metamath Proof Explorer

Theorem tgaaddcpbllem1

Description: Lemma for tgaaddcpbl . (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 ⊢ ∼ ˙ = ∼ 𝒢 ∠ ⁡ G
tgaaddcpbl.o ⊢ O = a b | a ∈ P ∖ Y L S ∧ b ∈ P ∖ Y L S ∧ ∃ s ∈ Y L S s ∈ a I b
tgaaddcpbl.q ⊢ Q = c d | c ∈ P ∖ V L T ∧ d ∈ P ∖ V L T ∧ ∃ t ∈ V L T t ∈ c I d
tgaaddcpbl.1 ⊢ φ → G ∈ 𝒢 Tarski
tgaaddcpbl.s ⊢ φ → S ∈ P
tgaaddcpbl.t ⊢ φ → T ∈ P
tgaaddcpbl.u ⊢ φ → U ∈ P
tgaaddcpbl.v ⊢ φ → V ∈ P
tgaaddcpbl.w ⊢ φ → W ∈ P
tgaaddcpbl.x ⊢ φ → X ∈ P
tgaaddcpbl.y ⊢ φ → Y ∈ P
tgaaddcpbl.z ⊢ φ → Z ∈ P
tgaaddcpbl.2 ⊢ φ → Y ≠ S
tgaaddcpbl.3 ⊢ φ → V ≠ T
tgaaddcpbl.4 ⊢ φ → X O Z
tgaaddcpbl.5 ⊢ φ → U Q W
tgaaddcpbl.6 ⊢ φ → ⟨“ XYS ”⟩ ∼ ˙ ⟨“ UVT ”⟩
tgaaddcpbl.7 ⊢ φ → ⟨“ SYZ ”⟩ ∼ ˙ ⟨“ TVW ”⟩
tgaaddcpbllem3.1 ⊢ φ → ¬ Y ∈ X I Z
tgaaddcpbllem1.1 ⊢ K = hl 𝒢 ⁡ G
tgaaddcpbllem1.2 ⊢ φ → R ∈ Y L S
tgaaddcpbllem1.3 ⊢ φ → R ∈ X I Z
tgaaddcpbllem1.4 ⊢ φ → R K ⁡ Y S
Assertion tgaaddcpbllem1 ⊢ φ → ⟨“ XYZ ”⟩ ∼ ˙ ⟨“ UVW ”⟩

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 ⊢ ∼ ˙ = ∼ 𝒢 ∠ ⁡ G
5 tgaaddcpbl.o ⊢ O = a b | a ∈ P ∖ Y L S ∧ b ∈ P ∖ Y L S ∧ ∃ s ∈ Y L S s ∈ a I b
6 tgaaddcpbl.q ⊢ Q = c d | c ∈ P ∖ V L T ∧ d ∈ P ∖ V L T ∧ ∃ t ∈ V L T t ∈ c I d
7 tgaaddcpbl.1 ⊢ φ → G ∈ 𝒢 Tarski
8 tgaaddcpbl.s ⊢ φ → S ∈ P
9 tgaaddcpbl.t ⊢ φ → T ∈ P
10 tgaaddcpbl.u ⊢ φ → U ∈ P
11 tgaaddcpbl.v ⊢ φ → V ∈ P
12 tgaaddcpbl.w ⊢ φ → W ∈ P
13 tgaaddcpbl.x ⊢ φ → X ∈ P
14 tgaaddcpbl.y ⊢ φ → Y ∈ P
15 tgaaddcpbl.z ⊢ φ → Z ∈ P
16 tgaaddcpbl.2 ⊢ φ → Y ≠ S
17 tgaaddcpbl.3 ⊢ φ → V ≠ T
18 tgaaddcpbl.4 ⊢ φ → X O Z
19 tgaaddcpbl.5 ⊢ φ → U Q W
20 tgaaddcpbl.6 ⊢ φ → ⟨“ XYS ”⟩ ∼ ˙ ⟨“ UVT ”⟩
21 tgaaddcpbl.7 ⊢ φ → ⟨“ SYZ ”⟩ ∼ ˙ ⟨“ TVW ”⟩
22 tgaaddcpbllem3.1 ⊢ φ → ¬ Y ∈ X I Z
23 tgaaddcpbllem1.1 ⊢ K = hl 𝒢 ⁡ G
24 tgaaddcpbllem1.2 ⊢ φ → R ∈ Y L S
25 tgaaddcpbllem1.3 ⊢ φ → R ∈ X I Z
26 tgaaddcpbllem1.4 ⊢ φ → R K ⁡ Y S
27 4 eqcomi ⊢ ∼ 𝒢 ∠ ⁡ G = ∼ ˙
28 27 a1i ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → ∼ 𝒢 ∠ ⁡ G = ∼ ˙
29 7 ad6antr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R → G ∈ 𝒢 Tarski
30 29 ad3antrrr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → G ∈ 𝒢 Tarski
31 13 ad9antr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → X ∈ P
32 14 ad9antr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → Y ∈ P
33 15 ad6antr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R → Z ∈ P
34 33 ad3antrrr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → Z ∈ P
35 10 ad9antr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → U ∈ P
36 11 ad9antr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → V ∈ P
37 simpllr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → w ∈ P
38 simp-6r ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R → u ∈ P
39 38 ad3antrrr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → u ∈ P
40 1 2 3 7 14 8 16 tglinerflx1 ⊢ φ → Y ∈ Y L S
41 eqid ⊢ dist ⁡ G = dist ⁡ G
42 1 2 3 7 14 8 16 tgelrnln ⊢ φ → Y L S ∈ ran ⁡ L
43 1 41 2 5 3 42 7 13 15 18 oppne1 ⊢ φ → ¬ X ∈ Y L S
44 nelne2 ⊢ Y ∈ Y L S ∧ ¬ X ∈ Y L S → Y ≠ X
45 40 43 44 syl2anc ⊢ φ → Y ≠ X
46 45 necomd ⊢ φ → X ≠ Y
47 46 ad9antr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → X ≠ Y
48 1 41 2 5 3 42 7 13 15 18 oppne2 ⊢ φ → ¬ Z ∈ Y L S
49 nelne2 ⊢ Y ∈ Y L S ∧ ¬ Z ∈ Y L S → Y ≠ Z
50 40 48 49 syl2anc ⊢ φ → Y ≠ Z
51 50 ad9antr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → Y ≠ Z
52 eqid ⊢ ∼ 𝒢 ⁡ G = ∼ 𝒢 ⁡ G
53 simp-7r ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → V dist ⁡ G u = Y dist ⁡ G X
54 53 eqcomd ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → Y dist ⁡ G X = V dist ⁡ G u
55 1 41 2 30 32 31 36 39 54 tgcgrcomlr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → X dist ⁡ G Y = u dist ⁡ G V
56 55 eqcomd ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → u dist ⁡ G V = X dist ⁡ G Y
57 simpllr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R → r ∈ P
58 57 ad3antrrr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → r ∈ P
59 1 3 2 7 42 24 tglnpt ⊢ φ → R ∈ P
60 59 ad6antr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R → R ∈ P
61 60 ad3antrrr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → R ∈ P
62 simp-5r ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → r K ⁡ V T
63 30 adantr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ r K ⁡ V T → G ∈ 𝒢 Tarski
64 31 adantr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ r K ⁡ V T → X ∈ P
65 61 adantr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ r K ⁡ V T → R ∈ P
66 39 adantr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ r K ⁡ V T → u ∈ P
67 58 adantr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ r K ⁡ V T → r ∈ P
68 32 adantr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ r K ⁡ V T → Y ∈ P
69 36 adantr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ r K ⁡ V T → V ∈ P
70 9 ad9antr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → T ∈ P
71 70 adantr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ r K ⁡ V T → T ∈ P
72 35 adantr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ r K ⁡ V T → U ∈ P
73 8 ad9antr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → S ∈ P
74 73 adantr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ r K ⁡ V T → S ∈ P
75 4 a1i ⊢ φ → ∼ ˙ = ∼ 𝒢 ∠ ⁡ G
76 75 20 breqdi ⊢ φ → ⟨“ XYS ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ UVT ”⟩
77 76 ad9antr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → ⟨“ XYS ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ UVT ”⟩
78 1 2 30 23 31 32 73 35 36 70 77 cgracom ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → ⟨“ UVT ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ XYS ”⟩
79 78 adantr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ r K ⁡ V T → ⟨“ UVT ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ XYS ”⟩
80 26 ad10antr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ r K ⁡ V T → R K ⁡ Y S
81 1 2 23 63 72 69 71 64 68 74 79 65 80 cgrahl2 ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ r K ⁡ V T → ⟨“ UVT ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ XYR ”⟩
82 1 2 63 23 72 69 71 64 68 65 81 cgracom ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ r K ⁡ V T → ⟨“ XYR ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ UVT ”⟩
83 simp-9r ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ r K ⁡ V T → u K ⁡ V U
84 1 2 23 63 64 68 65 72 69 71 82 66 83 cgrahl1 ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ r K ⁡ V T → ⟨“ XYR ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ uVT ”⟩
85 simpr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ r K ⁡ V T → r K ⁡ V T
86 1 2 23 63 64 68 65 66 69 71 84 67 85 cgrahl2 ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ r K ⁡ V T → ⟨“ XYR ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ uVr ”⟩
87 1 2 23 13 13 14 7 46 hlid ⊢ φ → X K ⁡ Y X
88 87 ad9antr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → X K ⁡ Y X
89 88 adantr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ r K ⁡ V T → X K ⁡ Y X
90 simpr ⊢ φ ∧ R = Y → R = Y
91 25 adantr ⊢ φ ∧ R = Y → R ∈ X I Z
92 90 91 eqeltrrd ⊢ φ ∧ R = Y → Y ∈ X I Z
93 22 92 mtand ⊢ φ → ¬ R = Y
94 93 neqned ⊢ φ → R ≠ Y
95 94 necomd ⊢ φ → Y ≠ R
96 95 ad10antr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ r K ⁡ V T → Y ≠ R
97 96 necomd ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ r K ⁡ V T → R ≠ Y
98 1 2 23 65 64 68 63 97 hlid ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ r K ⁡ V T → R K ⁡ Y R
99 54 adantr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ r K ⁡ V T → Y dist ⁡ G X = V dist ⁡ G u
100 simp-4r ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → V dist ⁡ G r = Y dist ⁡ G R
101 100 eqcomd ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → Y dist ⁡ G R = V dist ⁡ G r
102 101 adantr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ r K ⁡ V T → Y dist ⁡ G R = V dist ⁡ G r
103 1 2 23 63 64 68 65 66 69 67 86 64 41 65 89 98 99 102 cgracgr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ r K ⁡ V T → X dist ⁡ G R = u dist ⁡ G r
104 1 41 2 63 64 65 66 67 103 tgcgrcomlr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ r K ⁡ V T → R dist ⁡ G X = r dist ⁡ G u
105 62 104 mpdan ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → R dist ⁡ G X = r dist ⁡ G u
106 24 ad10antr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ r K ⁡ V T → R ∈ Y L S
107 62 106 mpdan ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → R ∈ Y L S
108 43 ad9antr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → ¬ X ∈ Y L S
109 nelne2 ⊢ R ∈ Y L S ∧ ¬ X ∈ Y L S → R ≠ X
110 107 108 109 syl2anc ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → R ≠ X
111 1 41 2 30 61 31 58 39 105 110 tgcgrneq ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → r ≠ u
112 111 necomd ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → u ≠ r
113 simplr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → r ∈ u I w
114 25 ad9antr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → R ∈ X I Z
115 105 eqcomd ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → r dist ⁡ G u = R dist ⁡ G X
116 1 41 2 30 58 39 61 31 115 tgcgrcomlr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → u dist ⁡ G r = X dist ⁡ G R
117 simpr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → r dist ⁡ G w = R dist ⁡ G Z
118 1 41 2 30 36 58 32 61 100 tgcgrcomlr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → r dist ⁡ G V = R dist ⁡ G Y
119 1 41 2 30 39 58 37 31 61 34 36 32 112 113 114 116 117 56 118 axtg5seg ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → w dist ⁡ G V = Z dist ⁡ G Y
120 1 41 2 30 37 36 34 32 119 tgcgrcomlr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → V dist ⁡ G w = Y dist ⁡ G Z
121 1 41 2 30 39 58 37 31 61 34 113 114 116 117 tgcgrextend ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → u dist ⁡ G w = X dist ⁡ G Z
122 1 41 2 30 39 37 31 34 121 tgcgrcomlr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → w dist ⁡ G u = Z dist ⁡ G X
123 1 41 52 30 39 36 37 31 32 34 56 120 122 trgcgr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → ⟨“ uVw ”⟩ ∼ 𝒢 ⁡ G ⟨“ XYZ ”⟩
124 1 41 2 52 30 39 36 37 31 32 34 123 trgcgrcom ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → ⟨“ XYZ ”⟩ ∼ 𝒢 ⁡ G ⟨“ uVw ”⟩
125 1 2 30 23 31 32 34 39 36 37 47 51 124 cgrcgra ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → ⟨“ XYZ ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ uVw ”⟩
126 62 83 mpdan ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → u K ⁡ V U
127 1 2 23 39 35 36 30 126 hlcomd ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → U K ⁡ V u
128 1 2 23 30 31 32 34 39 36 37 125 35 127 cgrahl1 ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → ⟨“ XYZ ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ UVw ”⟩
129 12 ad9antr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → W ∈ P
130 eqid ⊢ pInv 𝒢 ⁡ G = pInv 𝒢 ⁡ G
131 eqid ⊢ pInv 𝒢 ⁡ G ⁡ T = pInv 𝒢 ⁡ G ⁡ T
132 1 41 2 3 130 7 9 131 10 mircl ⊢ φ → pInv 𝒢 ⁡ G ⁡ T ⁡ U ∈ P
133 132 ad9antr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → pInv 𝒢 ⁡ G ⁡ T ⁡ U ∈ P
134 7 adantr ⊢ φ ∧ S ∈ Y L Z → G ∈ 𝒢 Tarski
135 14 adantr ⊢ φ ∧ S ∈ Y L Z → Y ∈ P
136 8 adantr ⊢ φ ∧ S ∈ Y L Z → S ∈ P
137 15 adantr ⊢ φ ∧ S ∈ Y L Z → Z ∈ P
138 16 adantr ⊢ φ ∧ S ∈ Y L Z → Y ≠ S
139 simpr ⊢ φ ∧ S ∈ Y L Z → S ∈ Y L Z
140 50 adantr ⊢ φ ∧ S ∈ Y L Z → Y ≠ Z
141 1 2 3 134 135 137 140 tglinecom ⊢ φ ∧ S ∈ Y L Z → Y L Z = Z L Y
142 139 141 eleqtrd ⊢ φ ∧ S ∈ Y L Z → S ∈ Z L Y
143 50 necomd ⊢ φ → Z ≠ Y
144 143 adantr ⊢ φ ∧ S ∈ Y L Z → Z ≠ Y
145 1 2 3 134 135 136 137 138 142 144 lnrot1 ⊢ φ ∧ S ∈ Y L Z → Z ∈ Y L S
146 48 145 mtand ⊢ φ → ¬ S ∈ Y L Z
147 50 neneqd ⊢ φ → ¬ Y = Z
148 146 147 jca ⊢ φ → ¬ S ∈ Y L Z ∧ ¬ Y = Z
149 ioran ⊢ ¬ S ∈ Y L Z ∨ Y = Z ↔ ¬ S ∈ Y L Z ∧ ¬ Y = Z
150 148 149 sylibr ⊢ φ → ¬ S ∈ Y L Z ∨ Y = Z
151 150 ad9antr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → ¬ S ∈ Y L Z ∨ Y = Z
152 1 41 2 6 10 12 islnopp ⊢ φ → U Q W ↔ ¬ U ∈ V L T ∧ ¬ W ∈ V L T ∧ ∃ t ∈ V L T t ∈ U I W
153 19 152 mpbid ⊢ φ → ¬ U ∈ V L T ∧ ¬ W ∈ V L T ∧ ∃ t ∈ V L T t ∈ U I W
154 153 simplld ⊢ φ → ¬ U ∈ V L T
155 7 adantr ⊢ φ ∧ T ∈ V L pInv 𝒢 ⁡ G ⁡ T ⁡ U ∨ V = pInv 𝒢 ⁡ G ⁡ T ⁡ U → G ∈ 𝒢 Tarski
156 9 adantr ⊢ φ ∧ T ∈ V L pInv 𝒢 ⁡ G ⁡ T ⁡ U ∨ V = pInv 𝒢 ⁡ G ⁡ T ⁡ U → T ∈ P
157 10 adantr ⊢ φ ∧ T ∈ V L pInv 𝒢 ⁡ G ⁡ T ⁡ U ∨ V = pInv 𝒢 ⁡ G ⁡ T ⁡ U → U ∈ P
158 1 41 2 3 130 155 156 131 157 mirmir ⊢ φ ∧ T ∈ V L pInv 𝒢 ⁡ G ⁡ T ⁡ U ∨ V = pInv 𝒢 ⁡ G ⁡ T ⁡ U → pInv 𝒢 ⁡ G ⁡ T ⁡ pInv 𝒢 ⁡ G ⁡ T ⁡ U = U
159 1 2 3 7 11 9 17 tgelrnln ⊢ φ → V L T ∈ ran ⁡ L
160 159 adantr ⊢ φ ∧ T ∈ V L pInv 𝒢 ⁡ G ⁡ T ⁡ U ∨ V = pInv 𝒢 ⁡ G ⁡ T ⁡ U → V L T ∈ ran ⁡ L
161 1 2 3 7 11 9 17 tglinerflx2 ⊢ φ → T ∈ V L T
162 161 adantr ⊢ φ ∧ T ∈ V L pInv 𝒢 ⁡ G ⁡ T ⁡ U ∨ V = pInv 𝒢 ⁡ G ⁡ T ⁡ U → T ∈ V L T
163 132 adantr ⊢ φ ∧ T ∈ V L pInv 𝒢 ⁡ G ⁡ T ⁡ U ∨ V = pInv 𝒢 ⁡ G ⁡ T ⁡ U → pInv 𝒢 ⁡ G ⁡ T ⁡ U ∈ P
164 11 adantr ⊢ φ ∧ T ∈ V L pInv 𝒢 ⁡ G ⁡ T ⁡ U ∨ V = pInv 𝒢 ⁡ G ⁡ T ⁡ U → V ∈ P
165 simpr ⊢ φ ∧ T ∈ V L pInv 𝒢 ⁡ G ⁡ T ⁡ U ∨ V = pInv 𝒢 ⁡ G ⁡ T ⁡ U → T ∈ V L pInv 𝒢 ⁡ G ⁡ T ⁡ U ∨ V = pInv 𝒢 ⁡ G ⁡ T ⁡ U
166 1 3 2 155 164 163 156 165 colcom ⊢ φ ∧ T ∈ V L pInv 𝒢 ⁡ G ⁡ T ⁡ U ∨ V = pInv 𝒢 ⁡ G ⁡ T ⁡ U → T ∈ pInv 𝒢 ⁡ G ⁡ T ⁡ U L V ∨ pInv 𝒢 ⁡ G ⁡ T ⁡ U = V
167 1 3 2 155 163 164 156 166 colrot1 ⊢ φ ∧ T ∈ V L pInv 𝒢 ⁡ G ⁡ T ⁡ U ∨ V = pInv 𝒢 ⁡ G ⁡ T ⁡ U → pInv 𝒢 ⁡ G ⁡ T ⁡ U ∈ V L T ∨ V = T
168 17 neneqd ⊢ φ → ¬ V = T
169 168 adantr ⊢ φ ∧ T ∈ V L pInv 𝒢 ⁡ G ⁡ T ⁡ U ∨ V = pInv 𝒢 ⁡ G ⁡ T ⁡ U → ¬ V = T
170 167 169 olcnd ⊢ φ ∧ T ∈ V L pInv 𝒢 ⁡ G ⁡ T ⁡ U ∨ V = pInv 𝒢 ⁡ G ⁡ T ⁡ U → pInv 𝒢 ⁡ G ⁡ T ⁡ U ∈ V L T
171 1 41 2 3 130 155 131 160 162 170 mirln ⊢ φ ∧ T ∈ V L pInv 𝒢 ⁡ G ⁡ T ⁡ U ∨ V = pInv 𝒢 ⁡ G ⁡ T ⁡ U → pInv 𝒢 ⁡ G ⁡ T ⁡ pInv 𝒢 ⁡ G ⁡ T ⁡ U ∈ V L T
172 158 171 eqeltrrd ⊢ φ ∧ T ∈ V L pInv 𝒢 ⁡ G ⁡ T ⁡ U ∨ V = pInv 𝒢 ⁡ G ⁡ T ⁡ U → U ∈ V L T
173 154 172 mtand ⊢ φ → ¬ T ∈ V L pInv 𝒢 ⁡ G ⁡ T ⁡ U ∨ V = pInv 𝒢 ⁡ G ⁡ T ⁡ U
174 173 ad9antr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → ¬ T ∈ V L pInv 𝒢 ⁡ G ⁡ T ⁡ U ∨ V = pInv 𝒢 ⁡ G ⁡ T ⁡ U
175 75 21 breqdi ⊢ φ → ⟨“ SYZ ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ TVW ”⟩
176 175 ad9antr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → ⟨“ SYZ ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ TVW ”⟩
177 62 97 mpdan ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → R ≠ Y
178 177 necomd ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → Y ≠ R
179 1 41 2 30 32 61 36 58 101 178 tgcgrneq ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → V ≠ r
180 179 necomd ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → r ≠ V
181 120 eqcomd ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → Y dist ⁡ G Z = V dist ⁡ G w
182 1 41 2 30 32 34 36 37 181 51 tgcgrneq ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → V ≠ w
183 1 41 2 30 58 37 61 34 117 tgcgrcomlr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → w dist ⁡ G r = Z dist ⁡ G R
184 1 41 52 30 58 36 37 61 32 34 118 120 183 trgcgr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → ⟨“ rVw ”⟩ ∼ 𝒢 ⁡ G ⟨“ RYZ ”⟩
185 1 2 30 23 58 36 37 61 32 34 180 182 184 cgrcgra ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → ⟨“ rVw ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ RYZ ”⟩
186 1 2 23 59 8 14 7 26 hlcomd ⊢ φ → S K ⁡ Y R
187 186 ad9antr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → S K ⁡ Y R
188 1 2 23 30 58 36 37 61 32 34 185 73 187 cgrahl1 ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → ⟨“ rVw ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ SYZ ”⟩
189 1 2 30 23 58 36 37 73 32 34 188 cgracom ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → ⟨“ SYZ ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ rVw ”⟩
190 1 2 23 58 70 36 30 62 hlcomd ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → T K ⁡ V r
191 1 2 23 30 73 32 34 58 36 37 189 70 190 cgrahl1 ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → ⟨“ SYZ ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ TVw ”⟩
192 1 2 3 7 11 9 17 tglinecom ⊢ φ → V L T = T L V
193 192 fveq2d ⊢ φ → hp 𝒢 ⁡ G ⁡ V L T = hp 𝒢 ⁡ G ⁡ T L V
194 10 154 eldifd ⊢ φ → U ∈ P ∖ V L T
195 1 2 130 131 6 7 159 161 194 3 oppmir ⊢ φ → U Q pInv 𝒢 ⁡ G ⁡ T ⁡ U
196 1 41 2 6 3 159 7 10 132 195 oppcom ⊢ φ → pInv 𝒢 ⁡ G ⁡ T ⁡ U Q U
197 1 41 2 6 3 159 7 10 12 19 oppcom ⊢ φ → W Q U
198 1 2 3 6 7 159 12 132 10 197 lnopp2hpgb ⊢ φ → pInv 𝒢 ⁡ G ⁡ T ⁡ U Q U ↔ W hp 𝒢 ⁡ G ⁡ V L T pInv 𝒢 ⁡ G ⁡ T ⁡ U
199 196 198 mpbid ⊢ φ → W hp 𝒢 ⁡ G ⁡ V L T pInv 𝒢 ⁡ G ⁡ T ⁡ U
200 193 199 breqdi ⊢ φ → W hp 𝒢 ⁡ G ⁡ T L V pInv 𝒢 ⁡ G ⁡ T ⁡ U
201 200 ad9antr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → W hp 𝒢 ⁡ G ⁡ T L V pInv 𝒢 ⁡ G ⁡ T ⁡ U
202 193 ad9antr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → hp 𝒢 ⁡ G ⁡ V L T = hp 𝒢 ⁡ G ⁡ T L V
203 196 ad9antr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → pInv 𝒢 ⁡ G ⁡ T ⁡ U Q U
204 159 ad9antr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → V L T ∈ ran ⁡ L
205 1 2 23 58 70 36 30 3 62 hlln ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → r ∈ T L V
206 192 ad9antr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → V L T = T L V
207 205 206 eleqtrrd ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → r ∈ V L T
208 nelne2 ⊢ R ∈ Y L S ∧ ¬ Z ∈ Y L S → R ≠ Z
209 24 48 208 syl2anc ⊢ φ → R ≠ Z
210 209 neneqd ⊢ φ → ¬ R = Z
211 210 ad9antr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → ¬ R = Z
212 30 adantr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ w ∈ V L T → G ∈ 𝒢 Tarski
213 58 adantr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ w ∈ V L T → r ∈ P
214 37 adantr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ w ∈ V L T → w ∈ P
215 61 adantr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ w ∈ V L T → R ∈ P
216 34 adantr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ w ∈ V L T → Z ∈ P
217 117 adantr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ w ∈ V L T → r dist ⁡ G w = R dist ⁡ G Z
218 121 eqcomd ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → X dist ⁡ G Z = u dist ⁡ G w
219 1 41 2 5 3 42 7 13 15 18 oppne3 ⊢ φ → X ≠ Z
220 219 ad9antr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → X ≠ Z
221 1 41 2 30 31 34 39 37 218 220 tgcgrneq ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → u ≠ w
222 1 2 3 30 39 37 221 tgelrnln ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → u L w ∈ ran ⁡ L
223 222 adantr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ w ∈ V L T → u L w ∈ ran ⁡ L
224 204 adantr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ w ∈ V L T → V L T ∈ ran ⁡ L
225 1 2 3 30 39 37 221 tglinerflx1 ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → u ∈ u L w
226 30 adantr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ u ∈ V L T → G ∈ 𝒢 Tarski
227 36 adantr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ u ∈ V L T → V ∈ P
228 70 adantr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ u ∈ V L T → T ∈ P
229 35 adantr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ u ∈ V L T → U ∈ P
230 17 ad10antr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ u ∈ V L T → V ≠ T
231 39 adantr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ u ∈ V L T → u ∈ P
232 45 ad9antr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → Y ≠ X
233 1 41 2 30 32 31 36 39 54 232 tgcgrneq ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → V ≠ u
234 233 necomd ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → u ≠ V
235 234 adantr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ u ∈ V L T → u ≠ V
236 simpr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ u ∈ V L T → u ∈ V L T
237 1 2 3 226 231 227 228 235 236 230 lnrot2 ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ u ∈ V L T → T ∈ u L V
238 1 2 3 7 11 9 17 tglinerflx1 ⊢ φ → V ∈ V L T
239 nelne2 ⊢ V ∈ V L T ∧ ¬ U ∈ V L T → V ≠ U
240 238 154 239 syl2anc ⊢ φ → V ≠ U
241 240 necomd ⊢ φ → U ≠ V
242 241 ad10antr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ u ∈ V L T → U ≠ V
243 1 2 3 226 231 227 235 tgelrnln ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ u ∈ V L T → u L V ∈ ran ⁡ L
244 1 2 23 39 35 36 30 3 126 hlln ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → u ∈ U L V
245 241 ad9antr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → U ≠ V
246 1 2 3 30 35 36 245 tglinecom ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → U L V = V L U
247 244 246 eleqtrd ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → u ∈ V L U
248 240 ad9antr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → V ≠ U
249 1 2 3 30 39 36 35 234 247 248 lnrot2 ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → U ∈ u L V
250 249 adantr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ u ∈ V L T → U ∈ u L V
251 1 2 3 226 231 227 235 tglinerflx2 ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ u ∈ V L T → V ∈ u L V
252 1 2 3 226 229 227 242 242 243 250 251 tglinethru ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ u ∈ V L T → u L V = U L V
253 237 252 eleqtrd ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ u ∈ V L T → T ∈ U L V
254 1 2 3 226 227 228 229 230 253 242 lnrot1 ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ u ∈ V L T → U ∈ V L T
255 154 ad10antr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ u ∈ V L T → ¬ U ∈ V L T
256 254 255 pm2.65da ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → ¬ u ∈ V L T
257 nelne1 ⊢ u ∈ u L w ∧ ¬ u ∈ V L T → u L w ≠ V L T
258 225 256 257 syl2anc ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → u L w ≠ V L T
259 258 adantr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ w ∈ V L T → u L w ≠ V L T
260 1 2 3 30 39 37 58 221 113 btwnlng1 ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → r ∈ u L w
261 260 adantr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ w ∈ V L T → r ∈ u L w
262 207 adantr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ w ∈ V L T → r ∈ V L T
263 261 262 elind ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ w ∈ V L T → r ∈ u L w ∩ V L T
264 1 2 3 30 39 37 221 tglinerflx2 ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → w ∈ u L w
265 264 adantr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ w ∈ V L T → w ∈ u L w
266 simpr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ w ∈ V L T → w ∈ V L T
267 265 266 elind ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ w ∈ V L T → w ∈ u L w ∩ V L T
268 1 2 3 212 223 224 259 263 267 tglineineq ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ w ∈ V L T → r = w
269 1 41 2 212 213 214 215 216 217 268 tgcgreq ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z ∧ w ∈ V L T → R = Z
270 211 269 mtand ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → ¬ w ∈ V L T
271 1 41 2 30 39 58 37 113 tgbtwncom ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → r ∈ w I u
272 1 41 2 6 37 39 207 270 256 271 islnoppd ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → w Q u
273 1 41 2 6 3 204 30 37 39 272 oppcom ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → u Q w
274 238 ad9antr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → V ∈ V L T
275 1 41 2 6 3 204 30 23 39 35 37 273 274 126 opphl ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → U Q w
276 1 41 2 6 3 204 30 35 37 275 oppcom ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → w Q U
277 1 2 3 6 30 204 37 133 35 276 lnopp2hpgb ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → pInv 𝒢 ⁡ G ⁡ T ⁡ U Q U ↔ w hp 𝒢 ⁡ G ⁡ V L T pInv 𝒢 ⁡ G ⁡ T ⁡ U
278 203 277 mpbid ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → w hp 𝒢 ⁡ G ⁡ V L T pInv 𝒢 ⁡ G ⁡ T ⁡ U
279 202 278 breqdi ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → w hp 𝒢 ⁡ G ⁡ T L V pInv 𝒢 ⁡ G ⁡ T ⁡ U
280 1 2 41 30 73 32 34 70 36 133 3 151 174 129 37 23 176 191 201 279 acopyeu ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → W K ⁡ V w
281 1 2 23 30 31 32 34 35 36 37 128 129 280 cgrahl2 ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → ⟨“ XYZ ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ UVW ”⟩
282 28 281 breqdi ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → ⟨“ XYZ ”⟩ ∼ ˙ ⟨“ UVW ”⟩
283 282 anasss ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R ∧ w ∈ P ∧ r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z → ⟨“ XYZ ”⟩ ∼ ˙ ⟨“ UVW ”⟩
284 1 41 2 29 38 57 60 33 axtgsegcon ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R → ∃ w ∈ P r ∈ u I w ∧ r dist ⁡ G w = R dist ⁡ G Z
285 283 284 r19.29a ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R → ⟨“ XYZ ”⟩ ∼ ˙ ⟨“ UVW ”⟩
286 285 anasss ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X ∧ r ∈ P ∧ r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R → ⟨“ XYZ ”⟩ ∼ ˙ ⟨“ UVW ”⟩
287 17 necomd ⊢ φ → T ≠ V
288 1 2 23 11 14 59 7 9 41 287 95 hlcgrex ⊢ φ → ∃ r ∈ P r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R
289 288 ad3antrrr ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X → ∃ r ∈ P r K ⁡ V T ∧ V dist ⁡ G r = Y dist ⁡ G R
290 286 289 r19.29a ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X → ⟨“ XYZ ”⟩ ∼ ˙ ⟨“ UVW ”⟩
291 290 anasss ⊢ φ ∧ u ∈ P ∧ u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X → ⟨“ XYZ ”⟩ ∼ ˙ ⟨“ UVW ”⟩
292 1 2 23 11 14 13 7 10 41 241 45 hlcgrex ⊢ φ → ∃ u ∈ P u K ⁡ V U ∧ V dist ⁡ G u = Y dist ⁡ G X
293 291 292 r19.29a ⊢ φ → ⟨“ XYZ ”⟩ ∼ ˙ ⟨“ UVW ”⟩