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

Theorem hlpasch 28547
Description: An application of the axiom of Pasch for half-lines. (Contributed by Thierry Arnoux, 15-Sep-2020.)
Hypotheses
Ref Expression
hlpasch.p 𝑃 = (Base‘𝐺)
hlpasch.i 𝐼 = (Itv‘𝐺)
hlpasch.k 𝐾 = (hlG‘𝐺)
hlpasch.g (𝜑𝐺 ∈ TarskiG)
hlpasch.1 (𝜑𝐴𝑃)
hlpasch.2 (𝜑𝐵𝑃)
hlpasch.3 (𝜑𝐶𝑃)
hlpasch.4 (𝜑𝑋𝑃)
hlpasch.5 (𝜑𝐷𝑃)
hlpasch.6 (𝜑𝐴𝐵)
hlpasch.7 (𝜑𝐶(𝐾𝐵)𝐷)
hlpasch.8 (𝜑𝐴 ∈ (𝑋𝐼𝐶))
Assertion
Ref Expression
hlpasch (𝜑 → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
Distinct variable groups:   𝐴,𝑒   𝐵,𝑒   𝐶,𝑒   𝐷,𝑒   𝑒,𝐺   𝑒,𝐼   𝑒,𝐾   𝑃,𝑒   𝑒,𝑋   𝜑,𝑒

Proof of Theorem hlpasch
StepHypRef Expression
1 hlpasch.p . . . 4 𝑃 = (Base‘𝐺)
2 hlpasch.i . . . 4 𝐼 = (Itv‘𝐺)
3 eqid 2727 . . . 4 (LineG‘𝐺) = (LineG‘𝐺)
4 hlpasch.g . . . . 5 (𝜑𝐺 ∈ TarskiG)
54adantr 480 . . . 4 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → 𝐺 ∈ TarskiG)
6 hlpasch.5 . . . . 5 (𝜑𝐷𝑃)
76adantr 480 . . . 4 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → 𝐷𝑃)
8 hlpasch.4 . . . . 5 (𝜑𝑋𝑃)
98adantr 480 . . . 4 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → 𝑋𝑃)
10 hlpasch.3 . . . . 5 (𝜑𝐶𝑃)
1110adantr 480 . . . 4 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → 𝐶𝑃)
12 hlpasch.2 . . . . 5 (𝜑𝐵𝑃)
1312adantr 480 . . . 4 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → 𝐵𝑃)
14 hlpasch.1 . . . . 5 (𝜑𝐴𝑃)
1514adantr 480 . . . 4 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → 𝐴𝑃)
16 eqid 2727 . . . . 5 (dist‘𝐺) = (dist‘𝐺)
17 simpr 484 . . . . 5 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → 𝐶 ∈ (𝐵𝐼𝐷))
181, 16, 2, 5, 13, 11, 7, 17tgbtwncom 28279 . . . 4 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → 𝐶 ∈ (𝐷𝐼𝐵))
19 hlpasch.8 . . . . 5 (𝜑𝐴 ∈ (𝑋𝐼𝐶))
2019adantr 480 . . . 4 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → 𝐴 ∈ (𝑋𝐼𝐶))
211, 2, 3, 5, 7, 9, 11, 13, 15, 18, 20outpasch 28546 . . 3 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → ∃𝑒𝑃 (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒)))
22 hlpasch.k . . . . . . 7 𝐾 = (hlG‘𝐺)
23 simplr 768 . . . . . . 7 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑒𝑃)
2413ad2antrr 725 . . . . . . 7 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐵𝑃)
2515ad2antrr 725 . . . . . . 7 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴𝑃)
265ad2antrr 725 . . . . . . 7 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐺 ∈ TarskiG)
27 simprr 772 . . . . . . . 8 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴 ∈ (𝐵𝐼𝑒))
281, 16, 2, 26, 24, 25, 23, 27tgbtwncom 28279 . . . . . . 7 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴 ∈ (𝑒𝐼𝐵))
2926adantr 480 . . . . . . . . . . 11 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐺 ∈ TarskiG)
3024adantr 480 . . . . . . . . . . 11 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐵𝑃)
3125adantr 480 . . . . . . . . . . 11 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴𝑃)
32 simplrr 777 . . . . . . . . . . . 12 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴 ∈ (𝐵𝐼𝑒))
33 simpr 484 . . . . . . . . . . . . 13 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝑒 = 𝐵)
3433oveq2d 7430 . . . . . . . . . . . 12 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → (𝐵𝐼𝑒) = (𝐵𝐼𝐵))
3532, 34eleqtrd 2830 . . . . . . . . . . 11 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴 ∈ (𝐵𝐼𝐵))
361, 16, 2, 29, 30, 31, 35axtgbtwnid 28257 . . . . . . . . . 10 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐵 = 𝐴)
3736eqcomd 2733 . . . . . . . . 9 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴 = 𝐵)
38 hlpasch.6 . . . . . . . . . . . 12 (𝜑𝐴𝐵)
3938ad3antrrr 729 . . . . . . . . . . 11 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴𝐵)
4039adantr 480 . . . . . . . . . 10 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴𝐵)
4140neneqd 2940 . . . . . . . . 9 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → ¬ 𝐴 = 𝐵)
4237, 41pm2.65da 816 . . . . . . . 8 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → ¬ 𝑒 = 𝐵)
4342neqned 2942 . . . . . . 7 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑒𝐵)
441, 2, 22, 23, 24, 25, 26, 25, 28, 43, 39btwnhl2 28404 . . . . . 6 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴(𝐾𝐵)𝑒)
457ad2antrr 725 . . . . . . 7 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐷𝑃)
469ad2antrr 725 . . . . . . 7 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑋𝑃)
47 simprl 770 . . . . . . 7 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑒 ∈ (𝐷𝐼𝑋))
481, 16, 2, 26, 45, 23, 46, 47tgbtwncom 28279 . . . . . 6 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑒 ∈ (𝑋𝐼𝐷))
4944, 48jca 511 . . . . 5 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
5049ex 412 . . . 4 (((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) → ((𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒)) → (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷))))
5150reximdva 3163 . . 3 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → (∃𝑒𝑃 (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒)) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷))))
5221, 51mpd 15 . 2 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
536ad2antrr 725 . . . . . 6 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐷𝑃)
5453adantr 480 . . . . 5 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐷𝑃)
55 simpr 484 . . . . . . 7 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) ∧ 𝑒 = 𝐷) → 𝑒 = 𝐷)
5655breq2d 5154 . . . . . 6 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) ∧ 𝑒 = 𝐷) → (𝐴(𝐾𝐵)𝑒𝐴(𝐾𝐵)𝐷))
5755eleq1d 2813 . . . . . 6 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) ∧ 𝑒 = 𝐷) → (𝑒 ∈ (𝑋𝐼𝐷) ↔ 𝐷 ∈ (𝑋𝐼𝐷)))
5856, 57anbi12d 630 . . . . 5 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) ∧ 𝑒 = 𝐷) → ((𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)) ↔ (𝐴(𝐾𝐵)𝐷𝐷 ∈ (𝑋𝐼𝐷))))
5914ad2antrr 725 . . . . . . . 8 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐴𝑃)
6059adantr 480 . . . . . . 7 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴𝑃)
6112ad2antrr 725 . . . . . . . 8 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐵𝑃)
6261adantr 480 . . . . . . 7 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐵𝑃)
634ad2antrr 725 . . . . . . . 8 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐺 ∈ TarskiG)
6463adantr 480 . . . . . . 7 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐺 ∈ TarskiG)
65 hlpasch.7 . . . . . . . . . 10 (𝜑𝐶(𝐾𝐵)𝐷)
661, 2, 22, 10, 6, 12, 4, 65hlcomd 28395 . . . . . . . . 9 (𝜑𝐷(𝐾𝐵)𝐶)
6766ad3antrrr 729 . . . . . . . 8 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐷(𝐾𝐵)𝐶)
6810adantr 480 . . . . . . . . . 10 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → 𝐶𝑃)
6968ad2antrr 725 . . . . . . . . 9 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐶𝑃)
7019adantr 480 . . . . . . . . . . 11 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → 𝐴 ∈ (𝑋𝐼𝐶))
7170ad2antrr 725 . . . . . . . . . 10 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴 ∈ (𝑋𝐼𝐶))
72 simpr 484 . . . . . . . . . . 11 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝑋 = 𝐵)
7372oveq1d 7429 . . . . . . . . . 10 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → (𝑋𝐼𝐶) = (𝐵𝐼𝐶))
7471, 73eleqtrd 2830 . . . . . . . . 9 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴 ∈ (𝐵𝐼𝐶))
751, 2, 22, 10, 6, 12, 4ishlg 28393 . . . . . . . . . . . 12 (𝜑 → (𝐶(𝐾𝐵)𝐷 ↔ (𝐶𝐵𝐷𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐶)))))
7665, 75mpbid 231 . . . . . . . . . . 11 (𝜑 → (𝐶𝐵𝐷𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐶))))
7776simp1d 1140 . . . . . . . . . 10 (𝜑𝐶𝐵)
7877ad3antrrr 729 . . . . . . . . 9 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐶𝐵)
7938ad2antrr 725 . . . . . . . . . 10 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐴𝐵)
8079adantr 480 . . . . . . . . 9 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴𝐵)
811, 2, 22, 54, 69, 62, 64, 60, 74, 78, 80hlbtwn 28402 . . . . . . . 8 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → (𝐷(𝐾𝐵)𝐶𝐷(𝐾𝐵)𝐴))
8267, 81mpbid 231 . . . . . . 7 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐷(𝐾𝐵)𝐴)
831, 2, 22, 54, 60, 62, 64, 82hlcomd 28395 . . . . . 6 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴(𝐾𝐵)𝐷)
848ad2antrr 725 . . . . . . . 8 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝑋𝑃)
8584adantr 480 . . . . . . 7 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝑋𝑃)
861, 16, 2, 64, 85, 54tgbtwntriv2 28278 . . . . . 6 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐷 ∈ (𝑋𝐼𝐷))
8783, 86jca 511 . . . . 5 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → (𝐴(𝐾𝐵)𝐷𝐷 ∈ (𝑋𝐼𝐷)))
8854, 58, 87rspcedvd 3609 . . . 4 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
8984ad2antrr 725 . . . . . 6 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐴(𝐾𝐵)𝑋) → 𝑋𝑃)
90 simpr 484 . . . . . . . . 9 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 = 𝑋) → 𝑒 = 𝑋)
9190breq2d 5154 . . . . . . . 8 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 = 𝑋) → (𝐴(𝐾𝐵)𝑒𝐴(𝐾𝐵)𝑋))
9290eleq1d 2813 . . . . . . . 8 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 = 𝑋) → (𝑒 ∈ (𝑋𝐼𝐷) ↔ 𝑋 ∈ (𝑋𝐼𝐷)))
9391, 92anbi12d 630 . . . . . . 7 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 = 𝑋) → ((𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)) ↔ (𝐴(𝐾𝐵)𝑋𝑋 ∈ (𝑋𝐼𝐷))))
9493ad4ant14 751 . . . . . 6 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐴(𝐾𝐵)𝑋) ∧ 𝑒 = 𝑋) → ((𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)) ↔ (𝐴(𝐾𝐵)𝑋𝑋 ∈ (𝑋𝐼𝐷))))
95 simpr 484 . . . . . . 7 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐴(𝐾𝐵)𝑋) → 𝐴(𝐾𝐵)𝑋)
961, 16, 2, 63, 84, 53tgbtwntriv1 28282 . . . . . . . 8 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝑋 ∈ (𝑋𝐼𝐷))
9796ad2antrr 725 . . . . . . 7 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐴(𝐾𝐵)𝑋) → 𝑋 ∈ (𝑋𝐼𝐷))
9895, 97jca 511 . . . . . 6 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐴(𝐾𝐵)𝑋) → (𝐴(𝐾𝐵)𝑋𝑋 ∈ (𝑋𝐼𝐷)))
9989, 94, 98rspcedvd 3609 . . . . 5 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐴(𝐾𝐵)𝑋) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
10053ad2antrr 725 . . . . . 6 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐷𝑃)
101 simpr 484 . . . . . . . 8 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) ∧ 𝑒 = 𝐷) → 𝑒 = 𝐷)
102101breq2d 5154 . . . . . . 7 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) ∧ 𝑒 = 𝐷) → (𝐴(𝐾𝐵)𝑒𝐴(𝐾𝐵)𝐷))
103101eleq1d 2813 . . . . . . 7 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) ∧ 𝑒 = 𝐷) → (𝑒 ∈ (𝑋𝐼𝐷) ↔ 𝐷 ∈ (𝑋𝐼𝐷)))
104102, 103anbi12d 630 . . . . . 6 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) ∧ 𝑒 = 𝐷) → ((𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)) ↔ (𝐴(𝐾𝐵)𝐷𝐷 ∈ (𝑋𝐼𝐷))))
10579ad2antrr 725 . . . . . . . 8 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴𝐵)
1061, 2, 22, 10, 6, 12, 4, 65hlne2 28397 . . . . . . . . 9 (𝜑𝐷𝐵)
107106ad4antr 731 . . . . . . . 8 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐷𝐵)
10863ad2antrr 725 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐺 ∈ TarskiG)
10961ad2antrr 725 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐵𝑃)
11059ad2antrr 725 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴𝑃)
11168ad2antrr 725 . . . . . . . . . 10 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐶𝑃)
112111adantr 480 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐶𝑃)
11384ad2antrr 725 . . . . . . . . . 10 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝑋𝑃)
114 simpr 484 . . . . . . . . . 10 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐵 ∈ (𝑋𝐼𝐴))
11570ad2antrr 725 . . . . . . . . . . 11 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐴 ∈ (𝑋𝐼𝐶))
116115adantr 480 . . . . . . . . . 10 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴 ∈ (𝑋𝐼𝐶))
1171, 16, 2, 108, 113, 109, 110, 112, 114, 116tgbtwnexch3 28285 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴 ∈ (𝐵𝐼𝐶))
118 simp-4r 783 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐷 ∈ (𝐵𝐼𝐶))
1191, 2, 108, 109, 110, 100, 112, 117, 118tgbtwnconn3 28368 . . . . . . . 8 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → (𝐴 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐴)))
1201, 2, 22, 14, 6, 12, 4ishlg 28393 . . . . . . . . 9 (𝜑 → (𝐴(𝐾𝐵)𝐷 ↔ (𝐴𝐵𝐷𝐵 ∧ (𝐴 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐴)))))
121120ad4antr 731 . . . . . . . 8 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → (𝐴(𝐾𝐵)𝐷 ↔ (𝐴𝐵𝐷𝐵 ∧ (𝐴 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐴)))))
122105, 107, 119, 121mpbir3and 1340 . . . . . . 7 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴(𝐾𝐵)𝐷)
1231, 16, 2, 108, 113, 100tgbtwntriv2 28278 . . . . . . 7 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐷 ∈ (𝑋𝐼𝐷))
124122, 123jca 511 . . . . . 6 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → (𝐴(𝐾𝐵)𝐷𝐷 ∈ (𝑋𝐼𝐷)))
125100, 104, 124rspcedvd 3609 . . . . 5 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
1268ad3antrrr 729 . . . . . 6 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝑋𝑃)
12712ad3antrrr 729 . . . . . 6 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐵𝑃)
12814ad3antrrr 729 . . . . . 6 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐴𝑃)
1294ad3antrrr 729 . . . . . 6 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐺 ∈ TarskiG)
130 simpr 484 . . . . . . . 8 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝑋𝐵)
131130neneqd 2940 . . . . . . 7 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → ¬ 𝑋 = 𝐵)
13263adantr 480 . . . . . . . . . 10 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐺 ∈ TarskiG)
133132adantr 480 . . . . . . . . . . . . . 14 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋 = 𝐶) → 𝐺 ∈ TarskiG)
134126adantr 480 . . . . . . . . . . . . . 14 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋 = 𝐶) → 𝑋𝑃)
135128adantr 480 . . . . . . . . . . . . . 14 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋 = 𝐶) → 𝐴𝑃)
136115adantr 480 . . . . . . . . . . . . . . 15 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋 = 𝐶) → 𝐴 ∈ (𝑋𝐼𝐶))
137 simpr 484 . . . . . . . . . . . . . . . 16 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋 = 𝐶) → 𝑋 = 𝐶)
138137oveq2d 7430 . . . . . . . . . . . . . . 15 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋 = 𝐶) → (𝑋𝐼𝑋) = (𝑋𝐼𝐶))
139136, 138eleqtrrd 2831 . . . . . . . . . . . . . 14 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋 = 𝐶) → 𝐴 ∈ (𝑋𝐼𝑋))
1401, 16, 2, 133, 134, 135, 139axtgbtwnid 28257 . . . . . . . . . . . . 13 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋 = 𝐶) → 𝑋 = 𝐴)
141140olcd 873 . . . . . . . . . . . 12 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋 = 𝐶) → (𝐵 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
142132adantr 480 . . . . . . . . . . . . 13 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → 𝐺 ∈ TarskiG)
143127adantr 480 . . . . . . . . . . . . 13 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → 𝐵𝑃)
144111adantr 480 . . . . . . . . . . . . 13 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → 𝐶𝑃)
145126adantr 480 . . . . . . . . . . . . 13 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → 𝑋𝑃)
146128adantr 480 . . . . . . . . . . . . 13 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → 𝐴𝑃)
147 simpr 484 . . . . . . . . . . . . . . . 16 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → 𝑋𝐶)
148147necomd 2991 . . . . . . . . . . . . . . 15 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → 𝐶𝑋)
149148neneqd 2940 . . . . . . . . . . . . . 14 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → ¬ 𝐶 = 𝑋)
15053adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐷𝑃)
151106ad3antrrr 729 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐷𝐵)
152 simplr 768 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷))
1531, 2, 3, 132, 150, 127, 126, 151, 152lncom 28413 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝑋 ∈ (𝐷(LineG‘𝐺)𝐵))
15477necomd 2991 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐵𝐶)
155154ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐵𝐶)
15666ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐷(𝐾𝐵)𝐶)
1571, 2, 22, 150, 111, 127, 132, 3, 156hlln 28398 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐷 ∈ (𝐶(LineG‘𝐺)𝐵))
1581, 2, 3, 132, 127, 111, 150, 155, 157lncom 28413 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐷 ∈ (𝐵(LineG‘𝐺)𝐶))
159158orcd 872 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝐷 ∈ (𝐵(LineG‘𝐺)𝐶) ∨ 𝐵 = 𝐶))
1601, 2, 3, 132, 126, 150, 127, 111, 153, 159coltr 28438 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝑋 ∈ (𝐵(LineG‘𝐺)𝐶) ∨ 𝐵 = 𝐶))
1611, 3, 2, 132, 127, 111, 126, 160colrot1 28350 . . . . . . . . . . . . . . . . 17 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝐵 ∈ (𝐶(LineG‘𝐺)𝑋) ∨ 𝐶 = 𝑋))
162161orcomd 870 . . . . . . . . . . . . . . . 16 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝐶 = 𝑋𝐵 ∈ (𝐶(LineG‘𝐺)𝑋)))
163162adantr 480 . . . . . . . . . . . . . . 15 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → (𝐶 = 𝑋𝐵 ∈ (𝐶(LineG‘𝐺)𝑋)))
164163ord 863 . . . . . . . . . . . . . 14 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → (¬ 𝐶 = 𝑋𝐵 ∈ (𝐶(LineG‘𝐺)𝑋)))
165149, 164mpd 15 . . . . . . . . . . . . 13 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → 𝐵 ∈ (𝐶(LineG‘𝐺)𝑋))
1661, 3, 2, 132, 126, 128, 111, 115btwncolg3 28348 . . . . . . . . . . . . . 14 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝐶 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
167166adantr 480 . . . . . . . . . . . . 13 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → (𝐶 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
1681, 2, 3, 142, 143, 144, 145, 146, 165, 167coltr 28438 . . . . . . . . . . . 12 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → (𝐵 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
169141, 168pm2.61dane 3024 . . . . . . . . . . 11 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝐵 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
1701, 3, 2, 132, 126, 128, 127, 169colrot2 28351 . . . . . . . . . 10 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝐴 ∈ (𝐵(LineG‘𝐺)𝑋) ∨ 𝐵 = 𝑋))
1711, 3, 2, 132, 127, 126, 128, 170colcom 28349 . . . . . . . . 9 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝐴 ∈ (𝑋(LineG‘𝐺)𝐵) ∨ 𝑋 = 𝐵))
172171orcomd 870 . . . . . . . 8 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝑋 = 𝐵𝐴 ∈ (𝑋(LineG‘𝐺)𝐵)))
173172ord 863 . . . . . . 7 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (¬ 𝑋 = 𝐵𝐴 ∈ (𝑋(LineG‘𝐺)𝐵)))
174131, 173mpd 15 . . . . . 6 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐴 ∈ (𝑋(LineG‘𝐺)𝐵))
1751, 2, 22, 126, 127, 128, 129, 128, 3, 174lnhl 28406 . . . . 5 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝐴(𝐾𝐵)𝑋𝐵 ∈ (𝑋𝐼𝐴)))
17699, 125, 175mpjaodan 957 . . . 4 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
17788, 176pm2.61dane 3024 . . 3 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
1784adantr 480 . . . . . 6 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → 𝐺 ∈ TarskiG)
1798adantr 480 . . . . . 6 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → 𝑋𝑃)
18012adantr 480 . . . . . 6 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → 𝐵𝑃)
18114adantr 480 . . . . . 6 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → 𝐴𝑃)
1826adantr 480 . . . . . 6 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → 𝐷𝑃)
183 simpr 484 . . . . . 6 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → 𝐷 ∈ (𝐵𝐼𝐶))
1841, 16, 2, 178, 179, 180, 68, 181, 182, 70, 183axtgpasch 28258 . . . . 5 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → ∃𝑒𝑃 (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋)))
185184adantr 480 . . . 4 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → ∃𝑒𝑃 (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋)))
186 simplr 768 . . . . . . . 8 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒𝑃)
187181ad3antrrr 729 . . . . . . . 8 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐴𝑃)
188180ad3antrrr 729 . . . . . . . 8 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐵𝑃)
189178ad3antrrr 729 . . . . . . . 8 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐺 ∈ TarskiG)
190 simprl 770 . . . . . . . . . 10 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒 ∈ (𝐴𝐼𝐵))
1911, 16, 2, 189, 187, 186, 188, 190tgbtwncom 28279 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒 ∈ (𝐵𝐼𝐴))
19238necomd 2991 . . . . . . . . . 10 (𝜑𝐵𝐴)
193192ad4antr 731 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐵𝐴)
194189adantr 480 . . . . . . . . . . . 12 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐺 ∈ TarskiG)
1956ad5antr 733 . . . . . . . . . . . 12 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷𝑃)
1968ad5antr 733 . . . . . . . . . . . 12 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑋𝑃)
197188adantr 480 . . . . . . . . . . . 12 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵𝑃)
198 simp-4r 783 . . . . . . . . . . . . . 14 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷))
199106necomd 2991 . . . . . . . . . . . . . . . 16 (𝜑𝐵𝐷)
200199ad5antr 733 . . . . . . . . . . . . . . 15 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵𝐷)
201200neneqd 2940 . . . . . . . . . . . . . 14 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → ¬ 𝐵 = 𝐷)
202 ioran 982 . . . . . . . . . . . . . 14 (¬ (𝑋 ∈ (𝐵(LineG‘𝐺)𝐷) ∨ 𝐵 = 𝐷) ↔ (¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷) ∧ ¬ 𝐵 = 𝐷))
203198, 201, 202sylanbrc 582 . . . . . . . . . . . . 13 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → ¬ (𝑋 ∈ (𝐵(LineG‘𝐺)𝐷) ∨ 𝐵 = 𝐷))
2041, 3, 2, 194, 197, 195, 196, 203ncolrot2 28354 . . . . . . . . . . . 12 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → ¬ (𝐷 ∈ (𝑋(LineG‘𝐺)𝐵) ∨ 𝑋 = 𝐵))
205 simpr 484 . . . . . . . . . . . . 13 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑒 = 𝐵)
206186adantr 480 . . . . . . . . . . . . . 14 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑒𝑃)
2071, 2, 3, 194, 195, 196, 197, 204ncolne1 28416 . . . . . . . . . . . . . 14 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷𝑋)
208 simplrr 777 . . . . . . . . . . . . . 14 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑒 ∈ (𝐷𝐼𝑋))
2091, 2, 3, 194, 195, 196, 206, 207, 208btwnlng1 28410 . . . . . . . . . . . . 13 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑒 ∈ (𝐷(LineG‘𝐺)𝑋))
210205, 209eqeltrrd 2829 . . . . . . . . . . . 12 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 ∈ (𝐷(LineG‘𝐺)𝑋))
2111, 2, 3, 194, 195, 196, 207tglinerflx1 28424 . . . . . . . . . . . 12 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷 ∈ (𝐷(LineG‘𝐺)𝑋))
212106ad5antr 733 . . . . . . . . . . . . . 14 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷𝐵)
213212necomd 2991 . . . . . . . . . . . . 13 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵𝐷)
2141, 2, 3, 194, 197, 195, 213tglinerflx1 28424 . . . . . . . . . . . 12 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 ∈ (𝐵(LineG‘𝐺)𝐷))
2151, 2, 3, 194, 197, 195, 213tglinerflx2 28425 . . . . . . . . . . . 12 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷 ∈ (𝐵(LineG‘𝐺)𝐷))
2161, 2, 3, 194, 195, 196, 197, 195, 204, 210, 211, 214, 215tglineinteq 28436 . . . . . . . . . . 11 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 = 𝐷)
217216, 201pm2.65da 816 . . . . . . . . . 10 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → ¬ 𝑒 = 𝐵)
218217neqned 2942 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒𝐵)
2191, 2, 22, 188, 187, 186, 189, 187, 191, 193, 218btwnhl1 28403 . . . . . . . 8 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒(𝐾𝐵)𝐴)
2201, 2, 22, 186, 187, 188, 189, 219hlcomd 28395 . . . . . . 7 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐴(𝐾𝐵)𝑒)
221178ad3antrrr 729 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝐺 ∈ TarskiG)
222182ad3antrrr 729 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝐷𝑃)
223 simplr 768 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝑒𝑃)
224179ad3antrrr 729 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝑋𝑃)
225 simpr 484 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝑒 ∈ (𝐷𝐼𝑋))
2261, 16, 2, 221, 222, 223, 224, 225tgbtwncom 28279 . . . . . . . 8 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝑒 ∈ (𝑋𝐼𝐷))
227226adantrl 715 . . . . . . 7 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒 ∈ (𝑋𝐼𝐷))
228220, 227jca 511 . . . . . 6 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
229228ex 412 . . . . 5 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) → ((𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷))))
230229reximdva 3163 . . . 4 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → (∃𝑒𝑃 (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷))))
231185, 230mpd 15 . . 3 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
232177, 231pm2.61dan 812 . 2 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
23376simp3d 1142 . 2 (𝜑 → (𝐶 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐶)))
23452, 232, 233mpjaodan 957 1 (𝜑 → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  wo 846  w3a 1085   = wceq 1534  wcel 2099  wne 2935  wrex 3065   class class class wbr 5142  cfv 6542  (class class class)co 7414  Basecbs 17171  distcds 17233  TarskiGcstrkg 28218  Itvcitv 28224  LineGclng 28225  hlGchlg 28391
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-cnex 11186  ax-resscn 11187  ax-1cn 11188  ax-icn 11189  ax-addcl 11190  ax-addrcl 11191  ax-mulcl 11192  ax-mulrcl 11193  ax-mulcom 11194  ax-addass 11195  ax-mulass 11196  ax-distr 11197  ax-i2m1 11198  ax-1ne0 11199  ax-1rid 11200  ax-rnegex 11201  ax-rrecex 11202  ax-cnre 11203  ax-pre-lttri 11204  ax-pre-lttrn 11205  ax-pre-ltadd 11206  ax-pre-mulgt0 11207
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-tp 4629  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7865  df-1st 7987  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-oadd 8484  df-er 8718  df-map 8838  df-pm 8839  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-dju 9916  df-card 9954  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11468  df-neg 11469  df-nn 12235  df-2 12297  df-3 12298  df-n0 12495  df-xnn0 12567  df-z 12581  df-uz 12845  df-fz 13509  df-fzo 13652  df-hash 14314  df-word 14489  df-concat 14545  df-s1 14570  df-s2 14823  df-s3 14824  df-trkgc 28239  df-trkgb 28240  df-trkgcb 28241  df-trkgld 28243  df-trkg 28244  df-cgrg 28302  df-leg 28374  df-hlg 28392  df-mir 28444  df-rag 28485  df-perpg 28487
This theorem is referenced by:  inaghl  28636
  Copyright terms: Public domain W3C validator