Theorem cgrg3col4

Description: Lemma 11.28 of Schwabhauser p. 102. Extend a congruence of three points with a fourth colinear point. (Contributed by Thierry Arnoux, 8-Oct-2020)

	Ref	Expression
Hypotheses	isleag.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	isleag.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	isleag.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	isleag.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	isleag.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
	isleag.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
	isleag.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
	isleag.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
	cgrg3col4.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	cgrg3col4.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
	cgrg3col4.1	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
	cgrg3col4.2	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐴 𝐿 𝐶 ) ∨ 𝐴 = 𝐶 ) )
Assertion	cgrg3col4	⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝑃 ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ )

Proof

Step	Hyp	Ref	Expression
1		isleag.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		isleag.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
3		isleag.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
4		isleag.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
5		isleag.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
6		isleag.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
7		isleag.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
8		isleag.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
9		cgrg3col4.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
10		cgrg3col4.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
11		cgrg3col4.1	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
12		cgrg3col4.2	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐴 𝐿 𝐶 ) ∨ 𝐴 = 𝐶 ) )
13		eqid	⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
14	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → 𝐺 ∈ TarskiG )
15	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → 𝐴 ∈ 𝑃 )
16	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → 𝐵 ∈ 𝑃 )
17	10	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → 𝑋 ∈ 𝑃 )
18		eqid	⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
19	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → 𝐷 ∈ 𝑃 )
20	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → 𝐸 ∈ 𝑃 )
21		eqid	⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
22		simpr	⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) )
23	1 21 13 18 2 3 4 5 6 7 8 11	cgr3simp1	⊢ ( 𝜑 → ( 𝐴 ( dist ‘ 𝐺 ) 𝐵 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐸 ) )
24	23	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → ( 𝐴 ( dist ‘ 𝐺 ) 𝐵 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐸 ) )
25	1 9 13 14 15 16 17 18 19 20 21 22 24	lnext	⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → ∃ 𝑦 ∈ 𝑃 ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ )
26	11	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
27	14	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → 𝐺 ∈ TarskiG )
28	17	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → 𝑋 ∈ 𝑃 )
29	15	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → 𝐴 ∈ 𝑃 )
30		simplr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → 𝑦 ∈ 𝑃 )
31	19	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → 𝐷 ∈ 𝑃 )
32	16	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → 𝐵 ∈ 𝑃 )
33	20	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → 𝐸 ∈ 𝑃 )
34		simpr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ )
35	1 21 13 18 27 29 32 28 31 33 30 34	cgr3simp3	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → ( 𝑋 ( dist ‘ 𝐺 ) 𝐴 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝐷 ) )
36	1 21 13 27 28 29 30 31 35	tgcgrcomlr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → ( 𝐴 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝑦 ) )
37	1 21 13 18 27 29 32 28 31 33 30 34	cgr3simp2	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → ( 𝐵 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝑦 ) )
38	5	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → 𝐶 ∈ 𝑃 )
39	8	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → 𝐹 ∈ 𝑃 )
40		simpr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐴 = 𝐶 )
41	40	ad3antrrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → 𝐴 = 𝐶 )
42	41	oveq2d	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → ( 𝑋 ( dist ‘ 𝐺 ) 𝐴 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝐶 ) )
43	2	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐺 ∈ TarskiG )
44	3	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐴 ∈ 𝑃 )
45	5	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐶 ∈ 𝑃 )
46	6	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐷 ∈ 𝑃 )
47	8	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐹 ∈ 𝑃 )
48	1 21 13 18 2 3 4 5 6 7 8 11	cgr3simp3	⊢ ( 𝜑 → ( 𝐶 ( dist ‘ 𝐺 ) 𝐴 ) = ( 𝐹 ( dist ‘ 𝐺 ) 𝐷 ) )
49	1 21 13 2 5 3 8 6 48	tgcgrcomlr	⊢ ( 𝜑 → ( 𝐴 ( dist ‘ 𝐺 ) 𝐶 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐹 ) )
50	49	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → ( 𝐴 ( dist ‘ 𝐺 ) 𝐶 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐹 ) )
51	1 21 13 43 44 45 46 47 50 40	tgcgreq	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐷 = 𝐹 )
52	51	ad3antrrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → 𝐷 = 𝐹 )
53	52	oveq2d	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → ( 𝑦 ( dist ‘ 𝐺 ) 𝐷 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝐹 ) )
54	35 42 53	3eqtr3d	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → ( 𝑋 ( dist ‘ 𝐺 ) 𝐶 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝐹 ) )
55	1 21 13 27 28 38 30 39 54	tgcgrcomlr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → ( 𝐶 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐹 ( dist ‘ 𝐺 ) 𝑦 ) )
56	36 37 55	3jca	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → ( ( 𝐴 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐹 ( dist ‘ 𝐺 ) 𝑦 ) ) )
57	1 21 13 18 27 29 32 38 28 31 33 39 30	tgcgr4	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → ( ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ ↔ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ( ( 𝐴 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐹 ( dist ‘ 𝐺 ) 𝑦 ) ) ) ) )
58	26 56 57	mpbir2and	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ )
59	58	ex	⊢ ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) → ( ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ → ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ ) )
60	59	reximdva	⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → ( ∃ 𝑦 ∈ 𝑃 ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ → ∃ 𝑦 ∈ 𝑃 ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ ) )
61	25 60	mpd	⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → ∃ 𝑦 ∈ 𝑃 ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ )
62		eqid	⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
63	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → 𝐺 ∈ TarskiG )
64	63	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) → 𝐺 ∈ TarskiG )
65	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → 𝐵 ∈ 𝑃 )
66	65	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) → 𝐵 ∈ 𝑃 )
67	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → 𝐴 ∈ 𝑃 )
68	67	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) → 𝐴 ∈ 𝑃 )
69	10	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → 𝑋 ∈ 𝑃 )
70	69	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) → 𝑋 ∈ 𝑃 )
71	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → 𝐸 ∈ 𝑃 )
72	71	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) → 𝐸 ∈ 𝑃 )
73	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → 𝐷 ∈ 𝑃 )
74	73	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) → 𝐷 ∈ 𝑃 )
75		simplr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) → 𝑥 ∈ 𝑃 )
76		simpllr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) → ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) )
77		simpr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) → ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) )
78	23	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → ( 𝐴 ( dist ‘ 𝐺 ) 𝐵 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐸 ) )
79		simpr	⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) )
80	1 13 9 63 65 67 69 79	ncolne1	⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → 𝐵 ≠ 𝐴 )
81	80	necomd	⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → 𝐴 ≠ 𝐵 )
82	1 21 13 63 67 65 73 71 78 81	tgcgrneq	⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → 𝐷 ≠ 𝐸 )
83	82	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) → 𝐷 ≠ 𝐸 )
84	83	neneqd	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) → ¬ 𝐷 = 𝐸 )
85		ioran	⊢ ( ¬ ( 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) ↔ ( ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ∧ ¬ 𝐷 = 𝐸 ) )
86	77 84 85	sylanbrc	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) → ¬ ( 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) )
87	1 9 13 64 74 72 75 86	ncolcom	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) → ¬ ( 𝑥 ∈ ( 𝐸 𝐿 𝐷 ) ∨ 𝐸 = 𝐷 ) )
88	1 9 13 64 72 74 75 87	ncolrot1	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) → ¬ ( 𝐸 ∈ ( 𝐷 𝐿 𝑥 ) ∨ 𝐷 = 𝑥 ) )
89	1 21 13 2 3 4 6 7 23	tgcgrcomlr	⊢ ( 𝜑 → ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐷 ) )
90	89	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) → ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐷 ) )
91	1 21 13 9 62 64 66 68 70 72 74 75 76 88 90	trgcopy	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) → ∃ 𝑦 ∈ 𝑃 ( ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ∧ 𝑦 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐸 𝐿 𝐷 ) ) 𝑥 ) )
92	11	ad6antr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
93	64	ad2antrr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → 𝐺 ∈ TarskiG )
94	66	ad2antrr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → 𝐵 ∈ 𝑃 )
95	68	ad2antrr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → 𝐴 ∈ 𝑃 )
96	70	ad2antrr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → 𝑋 ∈ 𝑃 )
97	72	ad2antrr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → 𝐸 ∈ 𝑃 )
98	74	ad2antrr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → 𝐷 ∈ 𝑃 )
99		simplr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → 𝑦 ∈ 𝑃 )
100		simpr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ )
101	1 21 13 18 93 94 95 96 97 98 99 100	cgr3simp2	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → ( 𝐴 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝑦 ) )
102	1 21 13 18 93 94 95 96 97 98 99 100	cgr3simp3	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → ( 𝑋 ( dist ‘ 𝐺 ) 𝐵 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝐸 ) )
103	1 21 13 93 96 94 99 97 102	tgcgrcomlr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → ( 𝐵 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝑦 ) )
104	45	ad5antr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → 𝐶 ∈ 𝑃 )
105	47	ad5antr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → 𝐹 ∈ 𝑃 )
106	1 21 13 93 95 96 98 99 101	tgcgrcomlr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → ( 𝑋 ( dist ‘ 𝐺 ) 𝐴 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝐷 ) )
107		simp-6r	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → 𝐴 = 𝐶 )
108	107	oveq2d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → ( 𝑋 ( dist ‘ 𝐺 ) 𝐴 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝐶 ) )
109	51	ad5antr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → 𝐷 = 𝐹 )
110	109	oveq2d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → ( 𝑦 ( dist ‘ 𝐺 ) 𝐷 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝐹 ) )
111	106 108 110	3eqtr3d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → ( 𝑋 ( dist ‘ 𝐺 ) 𝐶 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝐹 ) )
112	1 21 13 93 96 104 99 105 111	tgcgrcomlr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → ( 𝐶 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐹 ( dist ‘ 𝐺 ) 𝑦 ) )
113	101 103 112	3jca	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → ( ( 𝐴 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐹 ( dist ‘ 𝐺 ) 𝑦 ) ) )
114	1 21 13 18 93 95 94 104 96 98 97 105 99	tgcgr4	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → ( ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ ↔ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ( ( 𝐴 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐹 ( dist ‘ 𝐺 ) 𝑦 ) ) ) ) )
115	92 113 114	mpbir2and	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ )
116	115	ex	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) → ( ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ → ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ ) )
117	116	adantrd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) → ( ( ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ∧ 𝑦 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐸 𝐿 𝐷 ) ) 𝑥 ) → ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ ) )
118	117	reximdva	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) → ( ∃ 𝑦 ∈ 𝑃 ( ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ∧ 𝑦 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐸 𝐿 𝐷 ) ) 𝑥 ) → ∃ 𝑦 ∈ 𝑃 ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ ) )
119	91 118	mpd	⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) → ∃ 𝑦 ∈ 𝑃 ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ )
120	1 9 13 63 67 69 65 79	ncoltgdim2	⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → 𝐺 DimTarskiG≥ 2 )
121	1 13 9 63 120 73 71 82	tglowdim2ln	⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → ∃ 𝑥 ∈ 𝑃 ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) )
122	119 121	r19.29a	⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → ∃ 𝑦 ∈ 𝑃 ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ )
123	61 122	pm2.61dan	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → ∃ 𝑦 ∈ 𝑃 ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ )
124	1 9 13 2 3 5 10 12	colcom	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐶 𝐿 𝐴 ) ∨ 𝐶 = 𝐴 ) )
125	1 9 13 2 5 3 10 124	colrot1	⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) )
126	1 9 13 2 3 5 10 18 6 8 21 125 49	lnext	⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝑃 ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ )
127	126	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → ∃ 𝑦 ∈ 𝑃 ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ )
128	11	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
129	2	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → 𝐺 ∈ TarskiG )
130	10	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → 𝑋 ∈ 𝑃 )
131	3	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → 𝐴 ∈ 𝑃 )
132		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → 𝑦 ∈ 𝑃 )
133	6	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → 𝐷 ∈ 𝑃 )
134	5	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → 𝐶 ∈ 𝑃 )
135	8	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → 𝐹 ∈ 𝑃 )
136		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ )
137	1 21 13 18 129 131 134 130 133 135 132 136	cgr3simp3	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → ( 𝑋 ( dist ‘ 𝐺 ) 𝐴 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝐷 ) )
138	1 21 13 129 130 131 132 133 137	tgcgrcomlr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → ( 𝐴 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝑦 ) )
139	4	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → 𝐵 ∈ 𝑃 )
140	7	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → 𝐸 ∈ 𝑃 )
141	125	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → ( 𝐶 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) )
142	23	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → ( 𝐴 ( dist ‘ 𝐺 ) 𝐵 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐸 ) )
143	1 21 13 18 2 3 4 5 6 7 8 11	cgr3simp2	⊢ ( 𝜑 → ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐹 ) )
144	1 21 13 2 4 5 7 8 143	tgcgrcomlr	⊢ ( 𝜑 → ( 𝐶 ( dist ‘ 𝐺 ) 𝐵 ) = ( 𝐹 ( dist ‘ 𝐺 ) 𝐸 ) )
145	144	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → ( 𝐶 ( dist ‘ 𝐺 ) 𝐵 ) = ( 𝐹 ( dist ‘ 𝐺 ) 𝐸 ) )
146		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → 𝐴 ≠ 𝐶 )
147	1 9 13 129 131 134 130 18 133 135 21 139 132 140 141 136 142 145 146	tgfscgr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → ( 𝑋 ( dist ‘ 𝐺 ) 𝐵 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝐸 ) )
148	1 21 13 129 130 139 132 140 147	tgcgrcomlr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → ( 𝐵 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝑦 ) )
149	1 21 13 18 129 131 134 130 133 135 132 136	cgr3simp2	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → ( 𝐶 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐹 ( dist ‘ 𝐺 ) 𝑦 ) )
150	138 148 149	3jca	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → ( ( 𝐴 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐹 ( dist ‘ 𝐺 ) 𝑦 ) ) )
151	1 21 13 18 129 131 139 134 130 133 140 135 132	tgcgr4	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → ( ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ ↔ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ( ( 𝐴 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐹 ( dist ‘ 𝐺 ) 𝑦 ) ) ) ) )
152	128 150 151	mpbir2and	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ )
153	152	ex	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) → ( ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ → ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ ) )
154	153	reximdva	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → ( ∃ 𝑦 ∈ 𝑃 ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ → ∃ 𝑦 ∈ 𝑃 ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ ) )
155	127 154	mpd	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → ∃ 𝑦 ∈ 𝑃 ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ )
156	123 155	pm2.61dane	⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝑃 ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ )