Theorem cgrg3col4 28084

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.)

Hypotheses

Ref	Expression
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

Ref	Expression
cgrg3col4	⊢ (𝜑 → ∃𝑦 ∈ 𝑃 ⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩)

Distinct variable groups:   𝑦,𝐴   𝑦,𝐵   𝑦,𝐶   𝑦,𝐷   𝑦,𝐸   𝑦,𝐹   𝑦,𝐺   𝑦,𝐿   𝑦,𝑃   𝑦,𝑋   𝜑,𝑦

Proof of Theorem cgrg3col4

Dummy variable 𝑥 is distinct from all other variables.

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397   ∨ wo 846   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   ≠ wne 2941  ∃wrex 3071   class class class wbr 5147  ‘cfv 6540  (class class class)co 7404  ⟨“cs3 14789  ⟨“cs4 14790  Basecbs 17140  distcds 17202  TarskiGcstrkg 27658  Itvcitv 27664  LineGclng 27665  cgrGccgrg 27741  hlGchlg 27831  hpGchpg 27988

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7360  df-ov 7407  df-oprab 7408  df-mpo 7409  df-om 7851  df-1st 7970  df-2nd 7971  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-oadd 8465  df-er 8699  df-map 8818  df-pm 8819  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-dju 9892  df-card 9930  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-nn 12209  df-2 12271  df-3 12272  df-4 12273  df-n0 12469  df-xnn0 12541  df-z 12555  df-uz 12819  df-fz 13481  df-fzo 13624  df-hash 14287  df-word 14461  df-concat 14517  df-s1 14542  df-s2 14795  df-s3 14796  df-s4 14797  df-trkgc 27679  df-trkgb 27680  df-trkgcb 27681  df-trkgld 27683  df-trkg 27684  df-cgrg 27742  df-ismt 27764  df-leg 27814  df-hlg 27832  df-mir 27884  df-rag 27925  df-perpg 27927  df-hpg 27989  df-mid 28005  df-lmi 28006

This theorem is referenced by: (None)