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

Theorem cgrg3col4 25534
 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 2610 . . . . 5 (Itv‘𝐺) = (Itv‘𝐺)
4 isleag.g . . . . . 6 (𝜑𝐺 ∈ TarskiG)
54ad2antrr 758 . . . . 5 (((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → 𝐺 ∈ TarskiG)
6 isleag.a . . . . . 6 (𝜑𝐴𝑃)
76ad2antrr 758 . . . . 5 (((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → 𝐴𝑃)
8 isleag.b . . . . . 6 (𝜑𝐵𝑃)
98ad2antrr 758 . . . . 5 (((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → 𝐵𝑃)
10 cgrg3col4.x . . . . . 6 (𝜑𝑋𝑃)
1110ad2antrr 758 . . . . 5 (((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → 𝑋𝑃)
12 eqid 2610 . . . . 5 (cgrG‘𝐺) = (cgrG‘𝐺)
13 isleag.d . . . . . 6 (𝜑𝐷𝑃)
1413ad2antrr 758 . . . . 5 (((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → 𝐷𝑃)
15 isleag.e . . . . . 6 (𝜑𝐸𝑃)
1615ad2antrr 758 . . . . 5 (((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → 𝐸𝑃)
17 eqid 2610 . . . . 5 (dist‘𝐺) = (dist‘𝐺)
18 simpr 476 . . . . 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 25215 . . . . . 6 (𝜑 → (𝐴(dist‘𝐺)𝐵) = (𝐷(dist‘𝐺)𝐸))
2322ad2antrr 758 . . . . 5 (((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → (𝐴(dist‘𝐺)𝐵) = (𝐷(dist‘𝐺)𝐸))
241, 2, 3, 5, 7, 9, 11, 12, 14, 16, 17, 18, 23lnext 25262 . . . 4 (((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → ∃𝑦𝑃 ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩)
2521ad4antr 764 . . . . . . . 8 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩)
265ad2antrr 758 . . . . . . . . . 10 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐺 ∈ TarskiG)
2711ad2antrr 758 . . . . . . . . . 10 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝑋𝑃)
287ad2antrr 758 . . . . . . . . . 10 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐴𝑃)
29 simplr 788 . . . . . . . . . 10 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝑦𝑃)
3014ad2antrr 758 . . . . . . . . . 10 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐷𝑃)
319ad2antrr 758 . . . . . . . . . . 11 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐵𝑃)
3216ad2antrr 758 . . . . . . . . . . 11 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐸𝑃)
33 simpr 476 . . . . . . . . . . 11 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩)
341, 17, 3, 12, 26, 28, 31, 27, 30, 32, 29, 33cgr3simp3 25217 . . . . . . . . . 10 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝑋(dist‘𝐺)𝐴) = (𝑦(dist‘𝐺)𝐷))
351, 17, 3, 26, 27, 28, 29, 30, 34tgcgrcomlr 25175 . . . . . . . . 9 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝐴(dist‘𝐺)𝑋) = (𝐷(dist‘𝐺)𝑦))
361, 17, 3, 12, 26, 28, 31, 27, 30, 32, 29, 33cgr3simp2 25216 . . . . . . . . 9 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝐵(dist‘𝐺)𝑋) = (𝐸(dist‘𝐺)𝑦))
3719ad4antr 764 . . . . . . . . . 10 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐶𝑃)
3820ad4antr 764 . . . . . . . . . 10 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐹𝑃)
39 simpr 476 . . . . . . . . . . . . 13 ((𝜑𝐴 = 𝐶) → 𝐴 = 𝐶)
4039ad3antrrr 762 . . . . . . . . . . . 12 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐴 = 𝐶)
4140oveq2d 6565 . . . . . . . . . . 11 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝑋(dist‘𝐺)𝐴) = (𝑋(dist‘𝐺)𝐶))
424adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝐴 = 𝐶) → 𝐺 ∈ TarskiG)
436adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝐴 = 𝐶) → 𝐴𝑃)
4419adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝐴 = 𝐶) → 𝐶𝑃)
4513adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝐴 = 𝐶) → 𝐷𝑃)
4620adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝐴 = 𝐶) → 𝐹𝑃)
471, 17, 3, 12, 4, 6, 8, 19, 13, 15, 20, 21cgr3simp3 25217 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐶(dist‘𝐺)𝐴) = (𝐹(dist‘𝐺)𝐷))
481, 17, 3, 4, 19, 6, 20, 13, 47tgcgrcomlr 25175 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴(dist‘𝐺)𝐶) = (𝐷(dist‘𝐺)𝐹))
4948adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝐴 = 𝐶) → (𝐴(dist‘𝐺)𝐶) = (𝐷(dist‘𝐺)𝐹))
501, 17, 3, 42, 43, 44, 45, 46, 49, 39tgcgreq 25177 . . . . . . . . . . . . 13 ((𝜑𝐴 = 𝐶) → 𝐷 = 𝐹)
5150ad3antrrr 762 . . . . . . . . . . . 12 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐷 = 𝐹)
5251oveq2d 6565 . . . . . . . . . . 11 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝑦(dist‘𝐺)𝐷) = (𝑦(dist‘𝐺)𝐹))
5334, 41, 523eqtr3d 2652 . . . . . . . . . 10 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝑋(dist‘𝐺)𝐶) = (𝑦(dist‘𝐺)𝐹))
541, 17, 3, 26, 27, 37, 29, 38, 53tgcgrcomlr 25175 . . . . . . . . 9 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝐶(dist‘𝐺)𝑋) = (𝐹(dist‘𝐺)𝑦))
5535, 36, 543jca 1235 . . . . . . . 8 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → ((𝐴(dist‘𝐺)𝑋) = (𝐷(dist‘𝐺)𝑦) ∧ (𝐵(dist‘𝐺)𝑋) = (𝐸(dist‘𝐺)𝑦) ∧ (𝐶(dist‘𝐺)𝑋) = (𝐹(dist‘𝐺)𝑦)))
5625, 55jca 553 . . . . . . 7 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩ ∧ ((𝐴(dist‘𝐺)𝑋) = (𝐷(dist‘𝐺)𝑦) ∧ (𝐵(dist‘𝐺)𝑋) = (𝐸(dist‘𝐺)𝑦) ∧ (𝐶(dist‘𝐺)𝑋) = (𝐹(dist‘𝐺)𝑦))))
571, 17, 3, 12, 26, 28, 31, 37, 27, 30, 32, 38, 29tgcgr4 25226 . . . . . . 7 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩ ↔ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩ ∧ ((𝐴(dist‘𝐺)𝑋) = (𝐷(dist‘𝐺)𝑦) ∧ (𝐵(dist‘𝐺)𝑋) = (𝐸(dist‘𝐺)𝑦) ∧ (𝐶(dist‘𝐺)𝑋) = (𝐹(dist‘𝐺)𝑦)))))
5856, 57mpbird 246 . . . . . 6 (((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → ⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩)
5958ex 449 . . . . 5 ((((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑦𝑃) → (⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩ → ⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩))
6059reximdva 3000 . . . 4 (((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → (∃𝑦𝑃 ⟨“𝐴𝐵𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩ → ∃𝑦𝑃 ⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩))
6124, 60mpd 15 . . 3 (((𝜑𝐴 = 𝐶) ∧ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → ∃𝑦𝑃 ⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩)
62 eqid 2610 . . . . . 6 (hlG‘𝐺) = (hlG‘𝐺)
6342adantr 480 . . . . . . 7 (((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → 𝐺 ∈ TarskiG)
6463ad2antrr 758 . . . . . 6 (((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) → 𝐺 ∈ TarskiG)
658ad2antrr 758 . . . . . . 7 (((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → 𝐵𝑃)
6665ad2antrr 758 . . . . . 6 (((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) → 𝐵𝑃)
6743adantr 480 . . . . . . 7 (((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → 𝐴𝑃)
6867ad2antrr 758 . . . . . 6 (((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) → 𝐴𝑃)
6910ad2antrr 758 . . . . . . 7 (((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → 𝑋𝑃)
7069ad2antrr 758 . . . . . 6 (((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) → 𝑋𝑃)
7115ad2antrr 758 . . . . . . 7 (((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → 𝐸𝑃)
7271ad2antrr 758 . . . . . 6 (((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) → 𝐸𝑃)
7345adantr 480 . . . . . . 7 (((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → 𝐷𝑃)
7473ad2antrr 758 . . . . . 6 (((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) → 𝐷𝑃)
75 simplr 788 . . . . . 6 (((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) → 𝑥𝑃)
76 simpr 476 . . . . . . 7 (((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋))
7776ad2antrr 758 . . . . . 6 (((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) → ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋))
78 simpr 476 . . . . . . . . . 10 (((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) → ¬ 𝑥 ∈ (𝐷𝐿𝐸))
7922ad2antrr 758 . . . . . . . . . . . . 13 (((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → (𝐴(dist‘𝐺)𝐵) = (𝐷(dist‘𝐺)𝐸))
801, 3, 2, 63, 65, 67, 69, 76ncolne1 25320 . . . . . . . . . . . . . 14 (((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → 𝐵𝐴)
8180necomd 2837 . . . . . . . . . . . . 13 (((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → 𝐴𝐵)
821, 17, 3, 63, 67, 65, 73, 71, 79, 81tgcgrneq 25178 . . . . . . . . . . . 12 (((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → 𝐷𝐸)
8382ad2antrr 758 . . . . . . . . . . 11 (((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) → 𝐷𝐸)
8483neneqd 2787 . . . . . . . . . 10 (((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) → ¬ 𝐷 = 𝐸)
8578, 84jca 553 . . . . . . . . 9 (((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) → (¬ 𝑥 ∈ (𝐷𝐿𝐸) ∧ ¬ 𝐷 = 𝐸))
86 ioran 510 . . . . . . . . 9 (¬ (𝑥 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸) ↔ (¬ 𝑥 ∈ (𝐷𝐿𝐸) ∧ ¬ 𝐷 = 𝐸))
8785, 86sylibr 223 . . . . . . . 8 (((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) → ¬ (𝑥 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸))
881, 2, 3, 64, 74, 72, 75, 87ncolcom 25256 . . . . . . 7 (((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) → ¬ (𝑥 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷))
891, 2, 3, 64, 72, 74, 75, 88ncolrot1 25257 . . . . . 6 (((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) → ¬ (𝐸 ∈ (𝐷𝐿𝑥) ∨ 𝐷 = 𝑥))
901, 17, 3, 4, 6, 8, 13, 15, 22tgcgrcomlr 25175 . . . . . . 7 (𝜑 → (𝐵(dist‘𝐺)𝐴) = (𝐸(dist‘𝐺)𝐷))
9190ad4antr 764 . . . . . 6 (((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) → (𝐵(dist‘𝐺)𝐴) = (𝐸(dist‘𝐺)𝐷))
921, 17, 3, 2, 62, 64, 66, 68, 70, 72, 74, 75, 77, 89, 91trgcopy 25496 . . . . 5 (((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) → ∃𝑦𝑃 (⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩ ∧ 𝑦((hpG‘𝐺)‘(𝐸𝐿𝐷))𝑥))
9321ad6antr 768 . . . . . . . . . 10 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩)
9464ad2antrr 758 . . . . . . . . . . . 12 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → 𝐺 ∈ TarskiG)
9566ad2antrr 758 . . . . . . . . . . . 12 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → 𝐵𝑃)
9668ad2antrr 758 . . . . . . . . . . . 12 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → 𝐴𝑃)
9770ad2antrr 758 . . . . . . . . . . . 12 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → 𝑋𝑃)
9872ad2antrr 758 . . . . . . . . . . . 12 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → 𝐸𝑃)
9974ad2antrr 758 . . . . . . . . . . . 12 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → 𝐷𝑃)
100 simplr 788 . . . . . . . . . . . 12 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → 𝑦𝑃)
101 simpr 476 . . . . . . . . . . . 12 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩)
1021, 17, 3, 12, 94, 95, 96, 97, 98, 99, 100, 101cgr3simp2 25216 . . . . . . . . . . 11 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → (𝐴(dist‘𝐺)𝑋) = (𝐷(dist‘𝐺)𝑦))
1031, 17, 3, 12, 94, 95, 96, 97, 98, 99, 100, 101cgr3simp3 25217 . . . . . . . . . . . 12 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → (𝑋(dist‘𝐺)𝐵) = (𝑦(dist‘𝐺)𝐸))
1041, 17, 3, 94, 97, 95, 100, 98, 103tgcgrcomlr 25175 . . . . . . . . . . 11 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → (𝐵(dist‘𝐺)𝑋) = (𝐸(dist‘𝐺)𝑦))
10544ad5antr 766 . . . . . . . . . . . 12 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → 𝐶𝑃)
10646ad5antr 766 . . . . . . . . . . . 12 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → 𝐹𝑃)
1071, 17, 3, 94, 96, 97, 99, 100, 102tgcgrcomlr 25175 . . . . . . . . . . . . 13 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → (𝑋(dist‘𝐺)𝐴) = (𝑦(dist‘𝐺)𝐷))
108 simp-6r 807 . . . . . . . . . . . . . 14 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → 𝐴 = 𝐶)
109108oveq2d 6565 . . . . . . . . . . . . 13 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → (𝑋(dist‘𝐺)𝐴) = (𝑋(dist‘𝐺)𝐶))
11050ad5antr 766 . . . . . . . . . . . . . 14 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → 𝐷 = 𝐹)
111110oveq2d 6565 . . . . . . . . . . . . 13 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → (𝑦(dist‘𝐺)𝐷) = (𝑦(dist‘𝐺)𝐹))
112107, 109, 1113eqtr3d 2652 . . . . . . . . . . . 12 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → (𝑋(dist‘𝐺)𝐶) = (𝑦(dist‘𝐺)𝐹))
1131, 17, 3, 94, 97, 105, 100, 106, 112tgcgrcomlr 25175 . . . . . . . . . . 11 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → (𝐶(dist‘𝐺)𝑋) = (𝐹(dist‘𝐺)𝑦))
114102, 104, 1133jca 1235 . . . . . . . . . 10 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → ((𝐴(dist‘𝐺)𝑋) = (𝐷(dist‘𝐺)𝑦) ∧ (𝐵(dist‘𝐺)𝑋) = (𝐸(dist‘𝐺)𝑦) ∧ (𝐶(dist‘𝐺)𝑋) = (𝐹(dist‘𝐺)𝑦)))
11593, 114jca 553 . . . . . . . . 9 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩ ∧ ((𝐴(dist‘𝐺)𝑋) = (𝐷(dist‘𝐺)𝑦) ∧ (𝐵(dist‘𝐺)𝑋) = (𝐸(dist‘𝐺)𝑦) ∧ (𝐶(dist‘𝐺)𝑋) = (𝐹(dist‘𝐺)𝑦))))
1161, 17, 3, 12, 94, 96, 95, 105, 97, 99, 98, 106, 100tgcgr4 25226 . . . . . . . . 9 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → (⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩ ↔ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩ ∧ ((𝐴(dist‘𝐺)𝑋) = (𝐷(dist‘𝐺)𝑦) ∧ (𝐵(dist‘𝐺)𝑋) = (𝐸(dist‘𝐺)𝑦) ∧ (𝐶(dist‘𝐺)𝑋) = (𝐹(dist‘𝐺)𝑦)))))
117115, 116mpbird 246 . . . . . . . 8 (((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) ∧ ⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩) → ⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩)
118117ex 449 . . . . . . 7 ((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) → (⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩ → ⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩))
119118adantrd 483 . . . . . 6 ((((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) ∧ 𝑦𝑃) → ((⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩ ∧ 𝑦((hpG‘𝐺)‘(𝐸𝐿𝐷))𝑥) → ⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩))
120119reximdva 3000 . . . . 5 (((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) → (∃𝑦𝑃 (⟨“𝐵𝐴𝑋”⟩(cgrG‘𝐺)⟨“𝐸𝐷𝑦”⟩ ∧ 𝑦((hpG‘𝐺)‘(𝐸𝐿𝐷))𝑥) → ∃𝑦𝑃 ⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩))
12192, 120mpd 15 . . . 4 (((((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) ∧ 𝑥𝑃) ∧ ¬ 𝑥 ∈ (𝐷𝐿𝐸)) → ∃𝑦𝑃 ⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩)
1221, 2, 3, 63, 67, 69, 65, 76ncoltgdim2 25260 . . . . 5 (((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → 𝐺DimTarskiG≥2)
1231, 3, 2, 63, 122, 73, 71, 82tglowdim2ln 25346 . . . 4 (((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → ∃𝑥𝑃 ¬ 𝑥 ∈ (𝐷𝐿𝐸))
124121, 123r19.29a 3060 . . 3 (((𝜑𝐴 = 𝐶) ∧ ¬ (𝐵 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋)) → ∃𝑦𝑃 ⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩)
12561, 124pm2.61dan 828 . 2 ((𝜑𝐴 = 𝐶) → ∃𝑦𝑃 ⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩)
126 cgrg3col4.2 . . . . . . 7 (𝜑 → (𝑋 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
1271, 2, 3, 4, 6, 19, 10, 126colcom 25253 . . . . . 6 (𝜑 → (𝑋 ∈ (𝐶𝐿𝐴) ∨ 𝐶 = 𝐴))
1281, 2, 3, 4, 19, 6, 10, 127colrot1 25254 . . . . 5 (𝜑 → (𝐶 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋))
1291, 2, 3, 4, 6, 19, 10, 12, 13, 20, 17, 128, 48lnext 25262 . . . 4 (𝜑 → ∃𝑦𝑃 ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩)
130129adantr 480 . . 3 ((𝜑𝐴𝐶) → ∃𝑦𝑃 ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩)
13121ad3antrrr 762 . . . . . . 7 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩)
1324ad3antrrr 762 . . . . . . . . 9 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → 𝐺 ∈ TarskiG)
13310ad3antrrr 762 . . . . . . . . 9 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → 𝑋𝑃)
1346ad3antrrr 762 . . . . . . . . 9 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → 𝐴𝑃)
135 simplr 788 . . . . . . . . 9 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → 𝑦𝑃)
13613ad3antrrr 762 . . . . . . . . 9 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → 𝐷𝑃)
13719ad3antrrr 762 . . . . . . . . . 10 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → 𝐶𝑃)
13820ad3antrrr 762 . . . . . . . . . 10 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → 𝐹𝑃)
139 simpr 476 . . . . . . . . . 10 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩)
1401, 17, 3, 12, 132, 134, 137, 133, 136, 138, 135, 139cgr3simp3 25217 . . . . . . . . 9 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → (𝑋(dist‘𝐺)𝐴) = (𝑦(dist‘𝐺)𝐷))
1411, 17, 3, 132, 133, 134, 135, 136, 140tgcgrcomlr 25175 . . . . . . . 8 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → (𝐴(dist‘𝐺)𝑋) = (𝐷(dist‘𝐺)𝑦))
1428ad3antrrr 762 . . . . . . . . 9 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → 𝐵𝑃)
14315ad3antrrr 762 . . . . . . . . 9 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → 𝐸𝑃)
144128ad3antrrr 762 . . . . . . . . . 10 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → (𝐶 ∈ (𝐴𝐿𝑋) ∨ 𝐴 = 𝑋))
14522ad3antrrr 762 . . . . . . . . . 10 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → (𝐴(dist‘𝐺)𝐵) = (𝐷(dist‘𝐺)𝐸))
1461, 17, 3, 12, 4, 6, 8, 19, 13, 15, 20, 21cgr3simp2 25216 . . . . . . . . . . . 12 (𝜑 → (𝐵(dist‘𝐺)𝐶) = (𝐸(dist‘𝐺)𝐹))
1471, 17, 3, 4, 8, 19, 15, 20, 146tgcgrcomlr 25175 . . . . . . . . . . 11 (𝜑 → (𝐶(dist‘𝐺)𝐵) = (𝐹(dist‘𝐺)𝐸))
148147ad3antrrr 762 . . . . . . . . . 10 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → (𝐶(dist‘𝐺)𝐵) = (𝐹(dist‘𝐺)𝐸))
149 simpllr 795 . . . . . . . . . 10 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → 𝐴𝐶)
1501, 2, 3, 132, 134, 137, 133, 12, 136, 138, 17, 142, 135, 143, 144, 139, 145, 148, 149tgfscgr 25263 . . . . . . . . 9 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → (𝑋(dist‘𝐺)𝐵) = (𝑦(dist‘𝐺)𝐸))
1511, 17, 3, 132, 133, 142, 135, 143, 150tgcgrcomlr 25175 . . . . . . . 8 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → (𝐵(dist‘𝐺)𝑋) = (𝐸(dist‘𝐺)𝑦))
1521, 17, 3, 12, 132, 134, 137, 133, 136, 138, 135, 139cgr3simp2 25216 . . . . . . . 8 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → (𝐶(dist‘𝐺)𝑋) = (𝐹(dist‘𝐺)𝑦))
153141, 151, 1523jca 1235 . . . . . . 7 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → ((𝐴(dist‘𝐺)𝑋) = (𝐷(dist‘𝐺)𝑦) ∧ (𝐵(dist‘𝐺)𝑋) = (𝐸(dist‘𝐺)𝑦) ∧ (𝐶(dist‘𝐺)𝑋) = (𝐹(dist‘𝐺)𝑦)))
154131, 153jca 553 . . . . . 6 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩ ∧ ((𝐴(dist‘𝐺)𝑋) = (𝐷(dist‘𝐺)𝑦) ∧ (𝐵(dist‘𝐺)𝑋) = (𝐸(dist‘𝐺)𝑦) ∧ (𝐶(dist‘𝐺)𝑋) = (𝐹(dist‘𝐺)𝑦))))
1551, 17, 3, 12, 132, 134, 142, 137, 133, 136, 143, 138, 135tgcgr4 25226 . . . . . 6 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → (⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩ ↔ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩ ∧ ((𝐴(dist‘𝐺)𝑋) = (𝐷(dist‘𝐺)𝑦) ∧ (𝐵(dist‘𝐺)𝑋) = (𝐸(dist‘𝐺)𝑦) ∧ (𝐶(dist‘𝐺)𝑋) = (𝐹(dist‘𝐺)𝑦)))))
156154, 155mpbird 246 . . . . 5 ((((𝜑𝐴𝐶) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩) → ⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩)
157156ex 449 . . . 4 (((𝜑𝐴𝐶) ∧ 𝑦𝑃) → (⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩ → ⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩))
158157reximdva 3000 . . 3 ((𝜑𝐴𝐶) → (∃𝑦𝑃 ⟨“𝐴𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐹𝑦”⟩ → ∃𝑦𝑃 ⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩))
159130, 158mpd 15 . 2 ((𝜑𝐴𝐶) → ∃𝑦𝑃 ⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩)
160125, 159pm2.61dane 2869 1 (𝜑 → ∃𝑦𝑃 ⟨“𝐴𝐵𝐶𝑋”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹𝑦”⟩)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 382   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∃wrex 2897   class class class wbr 4583  ‘cfv 5804  (class class class)co 6549  ⟨“cs3 13438  ⟨“cs4 13439  Basecbs 15695  distcds 15777  TarskiGcstrkg 25129  Itvcitv 25135  LineGclng 25136  cgrGccgrg 25205  hlGchlg 25295  hpGchpg 25449 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-n0 11170  df-xnn0 11241  df-z 11255  df-uz 11564  df-fz 12198  df-fzo 12335  df-hash 12980  df-word 13154  df-concat 13156  df-s1 13157  df-s2 13444  df-s3 13445  df-s4 13446  df-trkgc 25147  df-trkgb 25148  df-trkgcb 25149  df-trkgld 25151  df-trkg 25152  df-cgrg 25206  df-ismt 25228  df-leg 25278  df-hlg 25296  df-mir 25348  df-rag 25389  df-perpg 25391  df-hpg 25450  df-mid 25466  df-lmi 25467 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator