Theorem tgaaddcpbllem1

Description: Lemma for tgaaddcpbl . (Contributed by Thierry Arnoux, 2-Aug-2026)

	Ref	Expression
Hypotheses	tgaaddcpbl.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	tgaaddcpbl.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	tgaaddcpbl.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	tgaaddcpbl.c	⊢ ∼ = ( cgrA ‘ 𝐺 )
	tgaaddcpbl.o	⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ) ∧ ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ) }
	tgaaddcpbl.q	⊢ 𝑄 = { ⟨ 𝑐 , 𝑑 ⟩ ∣ ( ( 𝑐 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ∧ 𝑑 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑉 𝐿 𝑇 ) 𝑡 ∈ ( 𝑐 𝐼 𝑑 ) ) }
	tgaaddcpbl.1	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	tgaaddcpbl.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑃 )
	tgaaddcpbl.t	⊢ ( 𝜑 → 𝑇 ∈ 𝑃 )
	tgaaddcpbl.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑃 )
	tgaaddcpbl.v	⊢ ( 𝜑 → 𝑉 ∈ 𝑃 )
	tgaaddcpbl.w	⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
	tgaaddcpbl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
	tgaaddcpbl.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
	tgaaddcpbl.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
	tgaaddcpbl.2	⊢ ( 𝜑 → 𝑌 ≠ 𝑆 )
	tgaaddcpbl.3	⊢ ( 𝜑 → 𝑉 ≠ 𝑇 )
	tgaaddcpbl.4	⊢ ( 𝜑 → 𝑋 𝑂 𝑍 )
	tgaaddcpbl.5	⊢ ( 𝜑 → 𝑈 𝑄 𝑊 )
	tgaaddcpbl.6	⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑆 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑇 ”⟩ )
	tgaaddcpbl.7	⊢ ( 𝜑 → ⟨“ 𝑆 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝑇 𝑉 𝑊 ”⟩ )
	tgaaddcpbllem3.1	⊢ ( 𝜑 → ¬ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) )
	tgaaddcpbllem1.1	⊢ 𝐾 = ( hlG ‘ 𝐺 )
	tgaaddcpbllem1.2	⊢ ( 𝜑 → 𝑅 ∈ ( 𝑌 𝐿 𝑆 ) )
	tgaaddcpbllem1.3	⊢ ( 𝜑 → 𝑅 ∈ ( 𝑋 𝐼 𝑍 ) )
	tgaaddcpbllem1.4	⊢ ( 𝜑 → 𝑅 ( 𝐾 ‘ 𝑌 ) 𝑆 )
Assertion	tgaaddcpbllem1	⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ )

Proof

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