MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cgrg3col4 Structured version   Visualization version   GIF version

Theorem cgrg3col4 27503
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.
StepHypRef Expression
1 isleag.p . . . . 5 𝑃 = (Base‘𝐺)
2 cgrg3col4.l . . . . 5 𝐿 = (LineG‘𝐺)
3 eqid 2736 . . . . 5 (Itv‘𝐺) = (Itv‘𝐺)
4 isleag.g . . . . . 6 (𝜑𝐺 ∈ TarskiG)
54ad2antrr 723 . . . . 5 (((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → 𝐺 ∈ TarskiG)
6 isleag.a . . . . . 6 (𝜑𝐴𝑃)
76ad2antrr 723 . . . . 5 (((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → 𝐴𝑃)
8 isleag.b . . . . . 6 (𝜑𝐵𝑃)
98ad2antrr 723 . . . . 5 (((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → 𝐵𝑃)
10 cgrg3col4.x . . . . . 6 (𝜑𝑋𝑃)
1110ad2antrr 723 . . . . 5 (((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → 𝑋𝑃)
12 eqid 2736 . . . . 5 (cgrG‘𝐺) = (cgrG‘𝐺)
13 isleag.d . . . . . 6 (𝜑𝐷𝑃)
1413ad2antrr 723 . . . . 5 (((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → 𝐷𝑃)
15 isleag.e . . . . . 6 (𝜑𝐸𝑃)
1615ad2antrr 723 . . . . 5 (((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → 𝐸𝑃)
17 eqid 2736 . . . . 5 (dist‘𝐺) = (dist‘𝐺)
18 simpr 485 . . . . 5 (((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋))
19 isleag.c . . . . . . 7 (𝜑𝐶𝑃)
20 isleag.f . . . . . . 7 (𝜑𝐹𝑃)
21 cgrg3col4.1 . . . . . . 7 (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩)
221, 17, 3, 12, 4, 6, 8, 19, 13, 15, 20, 21cgr3simp1 27170 . . . . . 6 (𝜑 → (𝐴(dist‘𝐺)𝐵) = (𝐷(dist‘𝐺)𝐸))
2322ad2antrr 723 . . . . 5 (((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → (𝐴(dist‘𝐺)𝐵) = (𝐷(dist‘𝐺)𝐸))
241, 2, 3, 5, 7, 9, 11, 12, 14, 16, 17, 18, 23lnext 27217 . . . 4 (((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → ∃𝑦𝑃 ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩)
2521ad4antr 729 . . . . . . 7 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩)
265ad2antrr 723 . . . . . . . . 9 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐺 ∈ TarskiG)
2711ad2antrr 723 . . . . . . . . 9 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝑋𝑃)
287ad2antrr 723 . . . . . . . . 9 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐴𝑃)
29 simplr 766 . . . . . . . . 9 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝑦𝑃)
3014ad2antrr 723 . . . . . . . . 9 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐷𝑃)
319ad2antrr 723 . . . . . . . . . 10 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐵𝑃)
3216ad2antrr 723 . . . . . . . . . 10 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐸𝑃)
33 simpr 485 . . . . . . . . . 10 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩)
341, 17, 3, 12, 26, 28, 31, 27, 30, 32, 29, 33cgr3simp3 27172 . . . . . . . . 9 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝑋(dist‘𝐺)𝐴) = (𝑦(dist‘𝐺)𝐷))
351, 17, 3, 26, 27, 28, 29, 30, 34tgcgrcomlr 27130 . . . . . . . 8 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝐴(dist‘𝐺)𝑋) = (𝐷(dist‘𝐺)𝑦))
361, 17, 3, 12, 26, 28, 31, 27, 30, 32, 29, 33cgr3simp2 27171 . . . . . . . 8 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝐵(dist‘𝐺)𝑋) = (𝐸(dist‘𝐺)𝑦))
3719ad4antr 729 . . . . . . . . 9 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐶𝑃)
3820ad4antr 729 . . . . . . . . 9 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐹𝑃)
39 simpr 485 . . . . . . . . . . . 12 ((𝜑𝐴 = 𝐶) → 𝐴 = 𝐶)
4039ad3antrrr 727 . . . . . . . . . . 11 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐴 = 𝐶)
4140oveq2d 7353 . . . . . . . . . 10 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝑋(dist‘𝐺)𝐴) = (𝑋(dist‘𝐺)𝐶))
424adantr 481 . . . . . . . . . . . . 13 ((𝜑𝐴 = 𝐶) → 𝐺 ∈ TarskiG)
436adantr 481 . . . . . . . . . . . . 13 ((𝜑𝐴 = 𝐶) → 𝐴𝑃)
4419adantr 481 . . . . . . . . . . . . 13 ((𝜑𝐴 = 𝐶) → 𝐶𝑃)
4513adantr 481 . . . . . . . . . . . . 13 ((𝜑𝐴 = 𝐶) → 𝐷𝑃)
4620adantr 481 . . . . . . . . . . . . 13 ((𝜑𝐴 = 𝐶) → 𝐹𝑃)
471, 17, 3, 12, 4, 6, 8, 19, 13, 15, 20, 21cgr3simp3 27172 . . . . . . . . . . . . . . 15 (𝜑 → (𝐶(dist‘𝐺)𝐴) = (𝐹(dist‘𝐺)𝐷))
481, 17, 3, 4, 19, 6, 20, 13, 47tgcgrcomlr 27130 . . . . . . . . . . . . . 14 (𝜑 → (𝐴(dist‘𝐺)𝐶) = (𝐷(dist‘𝐺)𝐹))
4948adantr 481 . . . . . . . . . . . . 13 ((𝜑𝐴 = 𝐶) → (𝐴(dist‘𝐺)𝐶) = (𝐷(dist‘𝐺)𝐹))
501, 17, 3, 42, 43, 44, 45, 46, 49, 39tgcgreq 27132 . . . . . . . . . . . 12 ((𝜑𝐴 = 𝐶) → 𝐷 = 𝐹)
5150ad3antrrr 727 . . . . . . . . . . 11 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐷 = 𝐹)
5251oveq2d 7353 . . . . . . . . . 10 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝑦(dist‘𝐺)𝐷) = (𝑦(dist‘𝐺)𝐹))
5334, 41, 523eqtr3d 2784 . . . . . . . . 9 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝑋(dist‘𝐺)𝐶) = (𝑦(dist‘𝐺)𝐹))
541, 17, 3, 26, 27, 37, 29, 38, 53tgcgrcomlr 27130 . . . . . . . 8 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝐶(dist‘𝐺)𝑋) = (𝐹(dist‘𝐺)𝑦))
5535, 36, 543jca 1127 . . . . . . 7 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → ((𝐴(dist‘𝐺)𝑋) = (𝐷(dist‘𝐺)𝑦) ∧ (𝐵(dist‘𝐺)𝑋) = (𝐸(dist‘𝐺)𝑦) ∧ (𝐶(dist‘𝐺)𝑋) = (𝐹(dist‘𝐺)𝑦)))
561, 17, 3, 12, 26, 28, 31, 37, 27, 30, 32, 38, 29tgcgr4 27181 . . . . . . 7 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩ ↔ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩ ∧ ((𝐴(dist‘𝐺)𝑋) = (𝐷(dist‘𝐺)𝑦) ∧ (𝐵(dist‘𝐺)𝑋) = (𝐸(dist‘𝐺)𝑦) ∧ (𝐶(dist‘𝐺)𝑋) = (𝐹(dist‘𝐺)𝑦)))))
5725, 55, 56mpbir2and 710 . . . . . 6 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → ⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩)
5857ex 413 . . . . 5 ((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) → (⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩ → ⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩))
5958reximdva 3161 . . . 4 (((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → (∃𝑦𝑃 ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩ → ∃𝑦𝑃 ⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩))
6024, 59mpd 15 . . 3 (((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → ∃𝑦𝑃 ⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩)
61 eqid 2736 . . . . . 6 (hlG‘𝐺) = (hlG‘𝐺)
624ad2antrr 723 . . . . . . 7 (((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → 𝐺 ∈ TarskiG)
6362ad2antrr 723 . . . . . 6 (((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) → 𝐺 ∈ TarskiG)
648ad2antrr 723 . . . . . . 7 (((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → 𝐵𝑃)
6564ad2antrr 723 . . . . . 6 (((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) → 𝐵𝑃)
666ad2antrr 723 . . . . . . 7 (((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → 𝐴𝑃)
6766ad2antrr 723 . . . . . 6 (((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) → 𝐴𝑃)
6810ad2antrr 723 . . . . . . 7 (((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → 𝑋𝑃)
6968ad2antrr 723 . . . . . 6 (((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) → 𝑋𝑃)
7015ad2antrr 723 . . . . . . 7 (((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → 𝐸𝑃)
7170ad2antrr 723 . . . . . 6 (((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) → 𝐸𝑃)
7213ad2antrr 723 . . . . . . 7 (((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → 𝐷𝑃)
7372ad2antrr 723 . . . . . 6 (((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) → 𝐷𝑃)
74 simplr 766 . . . . . 6 (((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) → 𝑥𝑃)
75 simpllr 773 . . . . . 6 (((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) → ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋))
76 simpr 485 . . . . . . . . 9 (((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) → ¬ 𝑥 ∈ (𝐷𝐿𝐸))
7722ad2antrr 723 . . . . . . . . . . . 12 (((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → (𝐴(dist‘𝐺)𝐵) = (𝐷(dist‘𝐺)𝐸))
78 simpr 485 . . . . . . . . . . . . . 14 (((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋))
791, 3, 2, 62, 64, 66, 68, 78ncolne1 27275 . . . . . . . . . . . . 13 (((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → 𝐵𝐴)
8079necomd 2996 . . . . . . . . . . . 12 (((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → 𝐴𝐵)
811, 17, 3, 62, 66, 64, 72, 70, 77, 80tgcgrneq 27133 . . . . . . . . . . 11 (((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → 𝐷𝐸)
8281ad2antrr 723 . . . . . . . . . 10 (((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) → 𝐷𝐸)
8382neneqd 2945 . . . . . . . . 9 (((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) → ¬ 𝐷 = 𝐸)
84 ioran 981 . . . . . . . . 9 (¬ (𝑥 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸) ↔ (¬ 𝑥 ∈ (𝐷𝐿𝐸) ∧ ¬ 𝐷 = 𝐸))
8576, 83, 84sylanbrc 583 . . . . . . . 8 (((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) → ¬ (𝑥 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸))
861, 2, 3, 63, 73, 71, 74, 85ncolcom 27211 . . . . . . 7 (((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) → ¬ (𝑥 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷))
871, 2, 3, 63, 71, 73, 74, 86ncolrot1 27212 . . . . . 6 (((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) → ¬ (𝐸 ∈ (𝐷𝐿𝑥) ∨ 𝐷 = 𝑥))
881, 17, 3, 4, 6, 8, 13, 15, 22tgcgrcomlr 27130 . . . . . . 7 (𝜑 → (𝐵(dist‘𝐺)𝐴) = (𝐸(dist‘𝐺)𝐷))
8988ad4antr 729 . . . . . 6 (((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) → (𝐵(dist‘𝐺)𝐴) = (𝐸(dist‘𝐺)𝐷))
901, 17, 3, 2, 61, 63, 65, 67, 69, 71, 73, 74, 75, 87, 89trgcopy 27454 . . . . 5 (((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) → ∃𝑦𝑃 (⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩ ∧ 𝑦((hpG‘𝐺)‘(𝐸𝐿𝐷))𝑥))
9121ad6antr 733 . . . . . . . . 9 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩)
9263ad2antrr 723 . . . . . . . . . . 11 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → 𝐺 ∈ TarskiG)
9365ad2antrr 723 . . . . . . . . . . 11 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → 𝐵𝑃)
9467ad2antrr 723 . . . . . . . . . . 11 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → 𝐴𝑃)
9569ad2antrr 723 . . . . . . . . . . 11 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → 𝑋𝑃)
9671ad2antrr 723 . . . . . . . . . . 11 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → 𝐸𝑃)
9773ad2antrr 723 . . . . . . . . . . 11 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → 𝐷𝑃)
98 simplr 766 . . . . . . . . . . 11 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → 𝑦𝑃)
99 simpr 485 . . . . . . . . . . 11 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩)
1001, 17, 3, 12, 92, 93, 94, 95, 96, 97, 98, 99cgr3simp2 27171 . . . . . . . . . 10 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → (𝐴(dist‘𝐺)𝑋) = (𝐷(dist‘𝐺)𝑦))
1011, 17, 3, 12, 92, 93, 94, 95, 96, 97, 98, 99cgr3simp3 27172 . . . . . . . . . . 11 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → (𝑋(dist‘𝐺)𝐵) = (𝑦(dist‘𝐺)𝐸))
1021, 17, 3, 92, 95, 93, 98, 96, 101tgcgrcomlr 27130 . . . . . . . . . 10 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → (𝐵(dist‘𝐺)𝑋) = (𝐸(dist‘𝐺)𝑦))
10344ad5antr 731 . . . . . . . . . . 11 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → 𝐶𝑃)
10446ad5antr 731 . . . . . . . . . . 11 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → 𝐹𝑃)
1051, 17, 3, 92, 94, 95, 97, 98, 100tgcgrcomlr 27130 . . . . . . . . . . . 12 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → (𝑋(dist‘𝐺)𝐴) = (𝑦(dist‘𝐺)𝐷))
106 simp-6r 785 . . . . . . . . . . . . 13 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → 𝐴 = 𝐶)
107106oveq2d 7353 . . . . . . . . . . . 12 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → (𝑋(dist‘𝐺)𝐴) = (𝑋(dist‘𝐺)𝐶))
10850ad5antr 731 . . . . . . . . . . . . 13 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → 𝐷 = 𝐹)
109108oveq2d 7353 . . . . . . . . . . . 12 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → (𝑦(dist‘𝐺)𝐷) = (𝑦(dist‘𝐺)𝐹))
110105, 107, 1093eqtr3d 2784 . . . . . . . . . . 11 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → (𝑋(dist‘𝐺)𝐶) = (𝑦(dist‘𝐺)𝐹))
1111, 17, 3, 92, 95, 103, 98, 104, 110tgcgrcomlr 27130 . . . . . . . . . 10 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → (𝐶(dist‘𝐺)𝑋) = (𝐹(dist‘𝐺)𝑦))
112100, 102, 1113jca 1127 . . . . . . . . 9 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → ((𝐴(dist‘𝐺)𝑋) = (𝐷(dist‘𝐺)𝑦) ∧ (𝐵(dist‘𝐺)𝑋) = (𝐸(dist‘𝐺)𝑦) ∧ (𝐶(dist‘𝐺)𝑋) = (𝐹(dist‘𝐺)𝑦)))
1131, 17, 3, 12, 92, 94, 93, 103, 95, 97, 96, 104, 98tgcgr4 27181 . . . . . . . . 9 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → (⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩ ↔ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩ ∧ ((𝐴(dist‘𝐺)𝑋) = (𝐷(dist‘𝐺)𝑦) ∧ (𝐵(dist‘𝐺)𝑋) = (𝐸(dist‘𝐺)𝑦) ∧ (𝐶(dist‘𝐺)𝑋) = (𝐹(dist‘𝐺)𝑦)))))
11491, 112, 113mpbir2and 710 . . . . . . . 8 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → ⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩)
115114ex 413 . . . . . . 7 ((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) → (⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩ → ⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩))
116115adantrd 492 . . . . . 6 ((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) → ((⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩ ∧ 𝑦((hpG‘𝐺)‘(𝐸𝐿𝐷))𝑥) → ⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩))
117116reximdva 3161 . . . . 5 (((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) → (∃𝑦𝑃 (⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩ ∧ 𝑦((hpG‘𝐺)‘(𝐸𝐿𝐷))𝑥) → ∃𝑦𝑃 ⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩))
11890, 117mpd 15 . . . 4 (((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) → ∃𝑦𝑃 ⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩)
1191, 2, 3, 62, 66, 68, 64, 78ncoltgdim2 27215 . . . . 5 (((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → 𝐺DimTarskiG≥2)
1201, 3, 2, 62, 119, 72, 70, 81tglowdim2ln 27301 . . . 4 (((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → ∃𝑥𝑃 ¬ 𝑥 ∈ (𝐷𝐿𝐸))
121118, 120r19.29a 3155 . . 3 (((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → ∃𝑦𝑃 ⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩)
12260, 121pm2.61dan 810 . 2 ((𝜑𝐴 = 𝐶) → ∃𝑦𝑃 ⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩)
123 cgrg3col4.2 . . . . . . 7 (𝜑 → (𝑋 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
1241, 2, 3, 4, 6, 19, 10, 123colcom 27208 . . . . . 6 (𝜑 → (𝑋 ∈ (𝐶𝐿𝐴) ∨ 𝐶 = 𝐴))
1251, 2, 3, 4, 19, 6, 10, 124colrot1 27209 . . . . 5 (𝜑 → (𝐶 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋))
1261, 2, 3, 4, 6, 19, 10, 12, 13, 20, 17, 125, 48lnext 27217 . . . 4 (𝜑 → ∃𝑦𝑃 ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩)
127126adantr 481 . . 3 ((𝜑𝐴𝐶) → ∃𝑦𝑃 ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩)
12821ad3antrrr 727 . . . . . 6 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩)
1294ad3antrrr 727 . . . . . . . 8 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → 𝐺 ∈ TarskiG)
13010ad3antrrr 727 . . . . . . . 8 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → 𝑋𝑃)
1316ad3antrrr 727 . . . . . . . 8 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → 𝐴𝑃)
132 simplr 766 . . . . . . . 8 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → 𝑦𝑃)
13313ad3antrrr 727 . . . . . . . 8 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → 𝐷𝑃)
13419ad3antrrr 727 . . . . . . . . 9 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → 𝐶𝑃)
13520ad3antrrr 727 . . . . . . . . 9 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → 𝐹𝑃)
136 simpr 485 . . . . . . . . 9 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩)
1371, 17, 3, 12, 129, 131, 134, 130, 133, 135, 132, 136cgr3simp3 27172 . . . . . . . 8 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → (𝑋(dist‘𝐺)𝐴) = (𝑦(dist‘𝐺)𝐷))
1381, 17, 3, 129, 130, 131, 132, 133, 137tgcgrcomlr 27130 . . . . . . 7 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → (𝐴(dist‘𝐺)𝑋) = (𝐷(dist‘𝐺)𝑦))
1398ad3antrrr 727 . . . . . . . 8 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → 𝐵𝑃)
14015ad3antrrr 727 . . . . . . . 8 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → 𝐸𝑃)
141125ad3antrrr 727 . . . . . . . . 9 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → (𝐶 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋))
14222ad3antrrr 727 . . . . . . . . 9 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → (𝐴(dist‘𝐺)𝐵) = (𝐷(dist‘𝐺)𝐸))
1431, 17, 3, 12, 4, 6, 8, 19, 13, 15, 20, 21cgr3simp2 27171 . . . . . . . . . . 11 (𝜑 → (𝐵(dist‘𝐺)𝐶) = (𝐸(dist‘𝐺)𝐹))
1441, 17, 3, 4, 8, 19, 15, 20, 143tgcgrcomlr 27130 . . . . . . . . . 10 (𝜑 → (𝐶(dist‘𝐺)𝐵) = (𝐹(dist‘𝐺)𝐸))
145144ad3antrrr 727 . . . . . . . . 9 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → (𝐶(dist‘𝐺)𝐵) = (𝐹(dist‘𝐺)𝐸))
146 simpllr 773 . . . . . . . . 9 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → 𝐴𝐶)
1471, 2, 3, 129, 131, 134, 130, 12, 133, 135, 17, 139, 132, 140, 141, 136, 142, 145, 146tgfscgr 27218 . . . . . . . 8 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → (𝑋(dist‘𝐺)𝐵) = (𝑦(dist‘𝐺)𝐸))
1481, 17, 3, 129, 130, 139, 132, 140, 147tgcgrcomlr 27130 . . . . . . 7 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → (𝐵(dist‘𝐺)𝑋) = (𝐸(dist‘𝐺)𝑦))
1491, 17, 3, 12, 129, 131, 134, 130, 133, 135, 132, 136cgr3simp2 27171 . . . . . . 7 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → (𝐶(dist‘𝐺)𝑋) = (𝐹(dist‘𝐺)𝑦))
150138, 148, 1493jca 1127 . . . . . 6 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → ((𝐴(dist‘𝐺)𝑋) = (𝐷(dist‘𝐺)𝑦) ∧ (𝐵(dist‘𝐺)𝑋) = (𝐸(dist‘𝐺)𝑦) ∧ (𝐶(dist‘𝐺)𝑋) = (𝐹(dist‘𝐺)𝑦)))
1511, 17, 3, 12, 129, 131, 139, 134, 130, 133, 140, 135, 132tgcgr4 27181 . . . . . 6 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → (⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩ ↔ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩ ∧ ((𝐴(dist‘𝐺)𝑋) = (𝐷(dist‘𝐺)𝑦) ∧ (𝐵(dist‘𝐺)𝑋) = (𝐸(dist‘𝐺)𝑦) ∧ (𝐶(dist‘𝐺)𝑋) = (𝐹(dist‘𝐺)𝑦)))))
152128, 150, 151mpbir2and 710 . . . . 5 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → ⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩)
153152ex 413 . . . 4 (((𝜑𝐴𝐶) ∧ 𝑦𝑃) → (⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩ → ⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩))
154153reximdva 3161 . . 3 ((𝜑𝐴𝐶) → (∃𝑦𝑃 ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩ → ∃𝑦𝑃 ⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩))
155127, 154mpd 15 . 2 ((𝜑𝐴𝐶) → ∃𝑦𝑃 ⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩)
156122, 155pm2.61dane 3029 1 (𝜑 → ∃𝑦𝑃 ⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  wo 844  w3a 1086   = wceq 1540  wcel 2105  wne 2940  wrex 3070   class class class wbr 5092  cfv 6479  (class class class)co 7337  ⟨“cs3 14654  ⟨“cs4 14655  Basecbs 17009  distcds 17068  TarskiGcstrkg 27077  Itvcitv 27083  LineGclng 27084  cgrGccgrg 27160  hlGchlg 27250  hpGchpg 27407
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5229  ax-sep 5243  ax-nul 5250  ax-pow 5308  ax-pr 5372  ax-un 7650  ax-cnex 11028  ax-resscn 11029  ax-1cn 11030  ax-icn 11031  ax-addcl 11032  ax-addrcl 11033  ax-mulcl 11034  ax-mulrcl 11035  ax-mulcom 11036  ax-addass 11037  ax-mulass 11038  ax-distr 11039  ax-i2m1 11040  ax-1ne0 11041  ax-1rid 11042  ax-rnegex 11043  ax-rrecex 11044  ax-cnre 11045  ax-pre-lttri 11046  ax-pre-lttrn 11047  ax-pre-ltadd 11048  ax-pre-mulgt0 11049
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3917  df-nul 4270  df-if 4474  df-pw 4549  df-sn 4574  df-pr 4576  df-tp 4578  df-op 4580  df-uni 4853  df-int 4895  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5176  df-tr 5210  df-id 5518  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5575  df-we 5577  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-pred 6238  df-ord 6305  df-on 6306  df-lim 6307  df-suc 6308  df-iota 6431  df-fun 6481  df-fn 6482  df-f 6483  df-f1 6484  df-fo 6485  df-f1o 6486  df-fv 6487  df-riota 7293  df-ov 7340  df-oprab 7341  df-mpo 7342  df-om 7781  df-1st 7899  df-2nd 7900  df-frecs 8167  df-wrecs 8198  df-recs 8272  df-rdg 8311  df-1o 8367  df-oadd 8371  df-er 8569  df-map 8688  df-pm 8689  df-en 8805  df-dom 8806  df-sdom 8807  df-fin 8808  df-dju 9758  df-card 9796  df-pnf 11112  df-mnf 11113  df-xr 11114  df-ltxr 11115  df-le 11116  df-sub 11308  df-neg 11309  df-nn 12075  df-2 12137  df-3 12138  df-4 12139  df-n0 12335  df-xnn0 12407  df-z 12421  df-uz 12684  df-fz 13341  df-fzo 13484  df-hash 14146  df-word 14318  df-concat 14374  df-s1 14400  df-s2 14660  df-s3 14661  df-s4 14662  df-trkgc 27098  df-trkgb 27099  df-trkgcb 27100  df-trkgld 27102  df-trkg 27103  df-cgrg 27161  df-ismt 27183  df-leg 27233  df-hlg 27251  df-mir 27303  df-rag 27344  df-perpg 27346  df-hpg 27408  df-mid 27424  df-lmi 27425
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator