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

Theorem hlpasch 25890
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 2774 . . . 4 (LineG‘𝐺) = (LineG‘𝐺)
4 hlpasch.g . . . . 5 (𝜑𝐺 ∈ TarskiG)
54adantr 467 . . . 4 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → 𝐺 ∈ TarskiG)
6 hlpasch.5 . . . . 5 (𝜑𝐷𝑃)
76adantr 467 . . . 4 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → 𝐷𝑃)
8 hlpasch.4 . . . . 5 (𝜑𝑋𝑃)
98adantr 467 . . . 4 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → 𝑋𝑃)
10 hlpasch.3 . . . . 5 (𝜑𝐶𝑃)
1110adantr 467 . . . 4 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → 𝐶𝑃)
12 hlpasch.2 . . . . 5 (𝜑𝐵𝑃)
1312adantr 467 . . . 4 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → 𝐵𝑃)
14 hlpasch.1 . . . . 5 (𝜑𝐴𝑃)
1514adantr 467 . . . 4 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → 𝐴𝑃)
16 eqid 2774 . . . . 5 (dist‘𝐺) = (dist‘𝐺)
17 simpr 472 . . . . 5 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → 𝐶 ∈ (𝐵𝐼𝐷))
181, 16, 2, 5, 13, 11, 7, 17tgbtwncom 25625 . . . 4 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → 𝐶 ∈ (𝐷𝐼𝐵))
19 hlpasch.8 . . . . 5 (𝜑𝐴 ∈ (𝑋𝐼𝐶))
2019adantr 467 . . . 4 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → 𝐴 ∈ (𝑋𝐼𝐶))
211, 2, 3, 5, 7, 9, 11, 13, 15, 18, 20outpasch 25889 . . 3 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → ∃𝑒𝑃 (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒)))
22 hlpasch.k . . . . . . 7 𝐾 = (hlG‘𝐺)
23 simplr 774 . . . . . . 7 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑒𝑃)
2413ad2antrr 706 . . . . . . 7 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐵𝑃)
2515ad2antrr 706 . . . . . . 7 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴𝑃)
265ad2antrr 706 . . . . . . 7 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐺 ∈ TarskiG)
27 simprr 778 . . . . . . . 8 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴 ∈ (𝐵𝐼𝑒))
281, 16, 2, 26, 24, 25, 23, 27tgbtwncom 25625 . . . . . . 7 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴 ∈ (𝑒𝐼𝐵))
2926adantr 467 . . . . . . . . . . 11 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐺 ∈ TarskiG)
3024adantr 467 . . . . . . . . . . 11 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐵𝑃)
3125adantr 467 . . . . . . . . . . 11 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴𝑃)
3227adantr 467 . . . . . . . . . . . 12 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴 ∈ (𝐵𝐼𝑒))
33 simpr 472 . . . . . . . . . . . . 13 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝑒 = 𝐵)
3433oveq2d 6828 . . . . . . . . . . . 12 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → (𝐵𝐼𝑒) = (𝐵𝐼𝐵))
3532, 34eleqtrd 2855 . . . . . . . . . . 11 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴 ∈ (𝐵𝐼𝐵))
361, 16, 2, 29, 30, 31, 35axtgbtwnid 25607 . . . . . . . . . 10 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐵 = 𝐴)
3736eqcomd 2780 . . . . . . . . 9 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴 = 𝐵)
38 hlpasch.6 . . . . . . . . . . . 12 (𝜑𝐴𝐵)
3938ad3antrrr 710 . . . . . . . . . . 11 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴𝐵)
4039adantr 467 . . . . . . . . . 10 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴𝐵)
4140neneqd 2951 . . . . . . . . 9 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → ¬ 𝐴 = 𝐵)
4237, 41pm2.65da 840 . . . . . . . 8 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → ¬ 𝑒 = 𝐵)
4342neqned 2953 . . . . . . 7 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑒𝐵)
441, 2, 22, 23, 24, 25, 26, 25, 28, 43, 39btwnhl2 25750 . . . . . 6 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴(𝐾𝐵)𝑒)
457ad2antrr 706 . . . . . . 7 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐷𝑃)
469ad2antrr 706 . . . . . . 7 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑋𝑃)
47 simprl 776 . . . . . . 7 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑒 ∈ (𝐷𝐼𝑋))
481, 16, 2, 26, 45, 23, 46, 47tgbtwncom 25625 . . . . . 6 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑒 ∈ (𝑋𝐼𝐷))
4944, 48jca 502 . . . . 5 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
5049ex 398 . . . 4 (((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) → ((𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒)) → (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷))))
5150reximdva 3168 . . 3 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → (∃𝑒𝑃 (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒)) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷))))
5221, 51mpd 15 . 2 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
536ad2antrr 706 . . . . . 6 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐷𝑃)
5453adantr 467 . . . . 5 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐷𝑃)
55 simpr 472 . . . . . . 7 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) ∧ 𝑒 = 𝐷) → 𝑒 = 𝐷)
5655breq2d 4809 . . . . . 6 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) ∧ 𝑒 = 𝐷) → (𝐴(𝐾𝐵)𝑒𝐴(𝐾𝐵)𝐷))
5755eleq1d 2838 . . . . . 6 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) ∧ 𝑒 = 𝐷) → (𝑒 ∈ (𝑋𝐼𝐷) ↔ 𝐷 ∈ (𝑋𝐼𝐷)))
5856, 57anbi12d 617 . . . . 5 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) ∧ 𝑒 = 𝐷) → ((𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)) ↔ (𝐴(𝐾𝐵)𝐷𝐷 ∈ (𝑋𝐼𝐷))))
5914ad2antrr 706 . . . . . . . 8 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐴𝑃)
6059adantr 467 . . . . . . 7 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴𝑃)
6112ad2antrr 706 . . . . . . . 8 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐵𝑃)
6261adantr 467 . . . . . . 7 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐵𝑃)
634ad2antrr 706 . . . . . . . 8 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐺 ∈ TarskiG)
6463adantr 467 . . . . . . 7 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐺 ∈ TarskiG)
65 hlpasch.7 . . . . . . . . . 10 (𝜑𝐶(𝐾𝐵)𝐷)
661, 2, 22, 10, 6, 12, 4, 65hlcomd 25741 . . . . . . . . 9 (𝜑𝐷(𝐾𝐵)𝐶)
6766ad3antrrr 710 . . . . . . . 8 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐷(𝐾𝐵)𝐶)
6810adantr 467 . . . . . . . . . 10 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → 𝐶𝑃)
6968ad2antrr 706 . . . . . . . . 9 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐶𝑃)
7019adantr 467 . . . . . . . . . . 11 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → 𝐴 ∈ (𝑋𝐼𝐶))
7170ad2antrr 706 . . . . . . . . . 10 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴 ∈ (𝑋𝐼𝐶))
72 simpr 472 . . . . . . . . . . 11 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝑋 = 𝐵)
7372oveq1d 6827 . . . . . . . . . 10 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → (𝑋𝐼𝐶) = (𝐵𝐼𝐶))
7471, 73eleqtrd 2855 . . . . . . . . 9 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴 ∈ (𝐵𝐼𝐶))
751, 2, 22, 10, 6, 12, 4ishlg 25739 . . . . . . . . . . . 12 (𝜑 → (𝐶(𝐾𝐵)𝐷 ↔ (𝐶𝐵𝐷𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐶)))))
7665, 75mpbid 223 . . . . . . . . . . 11 (𝜑 → (𝐶𝐵𝐷𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐶))))
7776simp1d 1163 . . . . . . . . . 10 (𝜑𝐶𝐵)
7877ad3antrrr 710 . . . . . . . . 9 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐶𝐵)
7938ad2antrr 706 . . . . . . . . . 10 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐴𝐵)
8079adantr 467 . . . . . . . . 9 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴𝐵)
811, 2, 22, 54, 69, 62, 64, 60, 74, 78, 80hlbtwn 25748 . . . . . . . 8 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → (𝐷(𝐾𝐵)𝐶𝐷(𝐾𝐵)𝐴))
8267, 81mpbid 223 . . . . . . 7 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐷(𝐾𝐵)𝐴)
831, 2, 22, 54, 60, 62, 64, 82hlcomd 25741 . . . . . 6 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴(𝐾𝐵)𝐷)
848ad2antrr 706 . . . . . . . 8 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝑋𝑃)
8584adantr 467 . . . . . . 7 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝑋𝑃)
861, 16, 2, 64, 85, 54tgbtwntriv2 25624 . . . . . 6 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐷 ∈ (𝑋𝐼𝐷))
8783, 86jca 502 . . . . 5 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → (𝐴(𝐾𝐵)𝐷𝐷 ∈ (𝑋𝐼𝐷)))
8854, 58, 87rspcedvd 3472 . . . 4 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
8984ad2antrr 706 . . . . . 6 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐴(𝐾𝐵)𝑋) → 𝑋𝑃)
90 simpr 472 . . . . . . . . 9 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 = 𝑋) → 𝑒 = 𝑋)
9190breq2d 4809 . . . . . . . 8 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 = 𝑋) → (𝐴(𝐾𝐵)𝑒𝐴(𝐾𝐵)𝑋))
9290eleq1d 2838 . . . . . . . 8 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 = 𝑋) → (𝑒 ∈ (𝑋𝐼𝐷) ↔ 𝑋 ∈ (𝑋𝐼𝐷)))
9391, 92anbi12d 617 . . . . . . 7 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 = 𝑋) → ((𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)) ↔ (𝐴(𝐾𝐵)𝑋𝑋 ∈ (𝑋𝐼𝐷))))
9493ad4ant14 748 . . . . . 6 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐴(𝐾𝐵)𝑋) ∧ 𝑒 = 𝑋) → ((𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)) ↔ (𝐴(𝐾𝐵)𝑋𝑋 ∈ (𝑋𝐼𝐷))))
95 simpr 472 . . . . . . 7 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐴(𝐾𝐵)𝑋) → 𝐴(𝐾𝐵)𝑋)
961, 16, 2, 63, 84, 53tgbtwntriv1 25628 . . . . . . . 8 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝑋 ∈ (𝑋𝐼𝐷))
9796ad2antrr 706 . . . . . . 7 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐴(𝐾𝐵)𝑋) → 𝑋 ∈ (𝑋𝐼𝐷))
9895, 97jca 502 . . . . . 6 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐴(𝐾𝐵)𝑋) → (𝐴(𝐾𝐵)𝑋𝑋 ∈ (𝑋𝐼𝐷)))
9989, 94, 98rspcedvd 3472 . . . . 5 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐴(𝐾𝐵)𝑋) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
10053ad2antrr 706 . . . . . 6 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐷𝑃)
101 simpr 472 . . . . . . . 8 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) ∧ 𝑒 = 𝐷) → 𝑒 = 𝐷)
102101breq2d 4809 . . . . . . 7 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) ∧ 𝑒 = 𝐷) → (𝐴(𝐾𝐵)𝑒𝐴(𝐾𝐵)𝐷))
103101eleq1d 2838 . . . . . . 7 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) ∧ 𝑒 = 𝐷) → (𝑒 ∈ (𝑋𝐼𝐷) ↔ 𝐷 ∈ (𝑋𝐼𝐷)))
104102, 103anbi12d 617 . . . . . 6 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) ∧ 𝑒 = 𝐷) → ((𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)) ↔ (𝐴(𝐾𝐵)𝐷𝐷 ∈ (𝑋𝐼𝐷))))
10579ad2antrr 706 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴𝐵)
1061, 2, 22, 10, 6, 12, 4, 65hlne2 25743 . . . . . . . . . 10 (𝜑𝐷𝐵)
107106ad4antr 713 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐷𝐵)
10863ad2antrr 706 . . . . . . . . . 10 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐺 ∈ TarskiG)
10961ad2antrr 706 . . . . . . . . . 10 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐵𝑃)
11059ad2antrr 706 . . . . . . . . . 10 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴𝑃)
11168ad2antrr 706 . . . . . . . . . . 11 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐶𝑃)
112111adantr 467 . . . . . . . . . 10 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐶𝑃)
11384ad2antrr 706 . . . . . . . . . . 11 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝑋𝑃)
114 simpr 472 . . . . . . . . . . 11 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐵 ∈ (𝑋𝐼𝐴))
11570ad2antrr 706 . . . . . . . . . . . 12 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐴 ∈ (𝑋𝐼𝐶))
116115adantr 467 . . . . . . . . . . 11 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴 ∈ (𝑋𝐼𝐶))
1171, 16, 2, 108, 113, 109, 110, 112, 114, 116tgbtwnexch3 25631 . . . . . . . . . 10 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴 ∈ (𝐵𝐼𝐶))
118 simp-4r 792 . . . . . . . . . 10 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐷 ∈ (𝐵𝐼𝐶))
1191, 2, 108, 109, 110, 100, 112, 117, 118tgbtwnconn3 25714 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → (𝐴 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐴)))
120105, 107, 1193jca 1149 . . . . . . . 8 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → (𝐴𝐵𝐷𝐵 ∧ (𝐴 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐴))))
1211, 2, 22, 14, 6, 12, 4ishlg 25739 . . . . . . . . 9 (𝜑 → (𝐴(𝐾𝐵)𝐷 ↔ (𝐴𝐵𝐷𝐵 ∧ (𝐴 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐴)))))
122121ad4antr 713 . . . . . . . 8 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → (𝐴(𝐾𝐵)𝐷 ↔ (𝐴𝐵𝐷𝐵 ∧ (𝐴 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐴)))))
123120, 122mpbird 248 . . . . . . 7 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴(𝐾𝐵)𝐷)
1241, 16, 2, 108, 113, 100tgbtwntriv2 25624 . . . . . . 7 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐷 ∈ (𝑋𝐼𝐷))
125123, 124jca 502 . . . . . 6 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → (𝐴(𝐾𝐵)𝐷𝐷 ∈ (𝑋𝐼𝐷)))
126100, 104, 125rspcedvd 3472 . . . . 5 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
1278ad3antrrr 710 . . . . . 6 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝑋𝑃)
12812ad3antrrr 710 . . . . . 6 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐵𝑃)
12914ad3antrrr 710 . . . . . 6 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐴𝑃)
1304ad3antrrr 710 . . . . . 6 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐺 ∈ TarskiG)
131 simpr 472 . . . . . . . 8 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝑋𝐵)
132131neneqd 2951 . . . . . . 7 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → ¬ 𝑋 = 𝐵)
13363adantr 467 . . . . . . . . . 10 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐺 ∈ TarskiG)
134133adantr 467 . . . . . . . . . . . . . 14 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋 = 𝐶) → 𝐺 ∈ TarskiG)
135127adantr 467 . . . . . . . . . . . . . 14 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋 = 𝐶) → 𝑋𝑃)
136129adantr 467 . . . . . . . . . . . . . 14 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋 = 𝐶) → 𝐴𝑃)
137115adantr 467 . . . . . . . . . . . . . . 15 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋 = 𝐶) → 𝐴 ∈ (𝑋𝐼𝐶))
138 simpr 472 . . . . . . . . . . . . . . . 16 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋 = 𝐶) → 𝑋 = 𝐶)
139138oveq2d 6828 . . . . . . . . . . . . . . 15 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋 = 𝐶) → (𝑋𝐼𝑋) = (𝑋𝐼𝐶))
140137, 139eleqtrrd 2856 . . . . . . . . . . . . . 14 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋 = 𝐶) → 𝐴 ∈ (𝑋𝐼𝑋))
1411, 16, 2, 134, 135, 136, 140axtgbtwnid 25607 . . . . . . . . . . . . 13 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋 = 𝐶) → 𝑋 = 𝐴)
142141olcd 890 . . . . . . . . . . . 12 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋 = 𝐶) → (𝐵 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
143133adantr 467 . . . . . . . . . . . . 13 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → 𝐺 ∈ TarskiG)
144128adantr 467 . . . . . . . . . . . . 13 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → 𝐵𝑃)
145111adantr 467 . . . . . . . . . . . . 13 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → 𝐶𝑃)
146127adantr 467 . . . . . . . . . . . . 13 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → 𝑋𝑃)
147129adantr 467 . . . . . . . . . . . . 13 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → 𝐴𝑃)
148 simpr 472 . . . . . . . . . . . . . . . 16 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → 𝑋𝐶)
149148necomd 3001 . . . . . . . . . . . . . . 15 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → 𝐶𝑋)
150149neneqd 2951 . . . . . . . . . . . . . 14 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → ¬ 𝐶 = 𝑋)
15153adantr 467 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐷𝑃)
152106ad3antrrr 710 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐷𝐵)
153 simplr 774 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷))
1541, 2, 3, 133, 151, 128, 127, 152, 153lncom 25759 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝑋 ∈ (𝐷(LineG‘𝐺)𝐵))
15577necomd 3001 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐵𝐶)
156155ad3antrrr 710 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐵𝐶)
15766ad3antrrr 710 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐷(𝐾𝐵)𝐶)
1581, 2, 22, 151, 111, 128, 133, 3, 157hlln 25744 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐷 ∈ (𝐶(LineG‘𝐺)𝐵))
1591, 2, 3, 133, 128, 111, 151, 156, 158lncom 25759 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐷 ∈ (𝐵(LineG‘𝐺)𝐶))
160159orcd 889 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝐷 ∈ (𝐵(LineG‘𝐺)𝐶) ∨ 𝐵 = 𝐶))
1611, 2, 3, 133, 127, 151, 128, 111, 154, 160coltr 25784 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝑋 ∈ (𝐵(LineG‘𝐺)𝐶) ∨ 𝐵 = 𝐶))
1621, 3, 2, 133, 128, 111, 127, 161colrot1 25696 . . . . . . . . . . . . . . . . 17 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝐵 ∈ (𝐶(LineG‘𝐺)𝑋) ∨ 𝐶 = 𝑋))
163162orcomd 887 . . . . . . . . . . . . . . . 16 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝐶 = 𝑋𝐵 ∈ (𝐶(LineG‘𝐺)𝑋)))
164163adantr 467 . . . . . . . . . . . . . . 15 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → (𝐶 = 𝑋𝐵 ∈ (𝐶(LineG‘𝐺)𝑋)))
165164ord 880 . . . . . . . . . . . . . 14 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → (¬ 𝐶 = 𝑋𝐵 ∈ (𝐶(LineG‘𝐺)𝑋)))
166150, 165mpd 15 . . . . . . . . . . . . 13 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → 𝐵 ∈ (𝐶(LineG‘𝐺)𝑋))
1671, 3, 2, 133, 127, 129, 111, 115btwncolg3 25694 . . . . . . . . . . . . . 14 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝐶 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
168167adantr 467 . . . . . . . . . . . . 13 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → (𝐶 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
1691, 2, 3, 143, 144, 145, 146, 147, 166, 168coltr 25784 . . . . . . . . . . . 12 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → (𝐵 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
170142, 169pm2.61dane 3033 . . . . . . . . . . 11 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝐵 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
1711, 3, 2, 133, 127, 129, 128, 170colrot2 25697 . . . . . . . . . 10 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝐴 ∈ (𝐵(LineG‘𝐺)𝑋) ∨ 𝐵 = 𝑋))
1721, 3, 2, 133, 128, 127, 129, 171colcom 25695 . . . . . . . . 9 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝐴 ∈ (𝑋(LineG‘𝐺)𝐵) ∨ 𝑋 = 𝐵))
173172orcomd 887 . . . . . . . 8 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝑋 = 𝐵𝐴 ∈ (𝑋(LineG‘𝐺)𝐵)))
174173ord 880 . . . . . . 7 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (¬ 𝑋 = 𝐵𝐴 ∈ (𝑋(LineG‘𝐺)𝐵)))
175132, 174mpd 15 . . . . . 6 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐴 ∈ (𝑋(LineG‘𝐺)𝐵))
1761, 2, 22, 127, 128, 129, 130, 129, 3, 175lnhl 25752 . . . . 5 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝐴(𝐾𝐵)𝑋𝐵 ∈ (𝑋𝐼𝐴)))
17799, 126, 176mpjaodan 970 . . . 4 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
17888, 177pm2.61dane 3033 . . 3 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
1794adantr 467 . . . . . 6 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → 𝐺 ∈ TarskiG)
1808adantr 467 . . . . . 6 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → 𝑋𝑃)
18112adantr 467 . . . . . 6 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → 𝐵𝑃)
18214adantr 467 . . . . . 6 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → 𝐴𝑃)
1836adantr 467 . . . . . 6 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → 𝐷𝑃)
184 simpr 472 . . . . . 6 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → 𝐷 ∈ (𝐵𝐼𝐶))
1851, 16, 2, 179, 180, 181, 68, 182, 183, 70, 184axtgpasch 25608 . . . . 5 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → ∃𝑒𝑃 (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋)))
186185adantr 467 . . . 4 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → ∃𝑒𝑃 (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋)))
187 simplr 774 . . . . . . . 8 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒𝑃)
188182ad3antrrr 710 . . . . . . . 8 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐴𝑃)
189181ad3antrrr 710 . . . . . . . 8 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐵𝑃)
190179ad3antrrr 710 . . . . . . . 8 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐺 ∈ TarskiG)
191 simprl 776 . . . . . . . . . 10 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒 ∈ (𝐴𝐼𝐵))
1921, 16, 2, 190, 188, 187, 189, 191tgbtwncom 25625 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒 ∈ (𝐵𝐼𝐴))
19338necomd 3001 . . . . . . . . . 10 (𝜑𝐵𝐴)
194193ad4antr 713 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐵𝐴)
195190adantr 467 . . . . . . . . . . . . 13 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐺 ∈ TarskiG)
1966ad5antr 717 . . . . . . . . . . . . 13 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷𝑃)
1978ad5antr 717 . . . . . . . . . . . . 13 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑋𝑃)
198189adantr 467 . . . . . . . . . . . . 13 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵𝑃)
199 simp-4r 792 . . . . . . . . . . . . . . . 16 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷))
200106necomd 3001 . . . . . . . . . . . . . . . . . 18 (𝜑𝐵𝐷)
201200ad5antr 717 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵𝐷)
202201neneqd 2951 . . . . . . . . . . . . . . . 16 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → ¬ 𝐵 = 𝐷)
203199, 202jca 502 . . . . . . . . . . . . . . 15 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → (¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷) ∧ ¬ 𝐵 = 𝐷))
204 ioran 995 . . . . . . . . . . . . . . 15 (¬ (𝑋 ∈ (𝐵(LineG‘𝐺)𝐷) ∨ 𝐵 = 𝐷) ↔ (¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷) ∧ ¬ 𝐵 = 𝐷))
205203, 204sylibr 225 . . . . . . . . . . . . . 14 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → ¬ (𝑋 ∈ (𝐵(LineG‘𝐺)𝐷) ∨ 𝐵 = 𝐷))
2061, 3, 2, 195, 198, 196, 197, 205ncolrot2 25700 . . . . . . . . . . . . 13 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → ¬ (𝐷 ∈ (𝑋(LineG‘𝐺)𝐵) ∨ 𝑋 = 𝐵))
207 simpr 472 . . . . . . . . . . . . . 14 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑒 = 𝐵)
208187adantr 467 . . . . . . . . . . . . . . 15 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑒𝑃)
2091, 2, 3, 195, 196, 197, 198, 206ncolne1 25762 . . . . . . . . . . . . . . 15 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷𝑋)
210 simplrr 785 . . . . . . . . . . . . . . 15 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑒 ∈ (𝐷𝐼𝑋))
2111, 2, 3, 195, 196, 197, 208, 209, 210btwnlng1 25756 . . . . . . . . . . . . . 14 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑒 ∈ (𝐷(LineG‘𝐺)𝑋))
212207, 211eqeltrrd 2854 . . . . . . . . . . . . 13 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 ∈ (𝐷(LineG‘𝐺)𝑋))
2131, 3, 2, 195, 196, 197, 212tglngne 25687 . . . . . . . . . . . . . 14 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷𝑋)
2141, 2, 3, 195, 196, 197, 213tglinerflx1 25770 . . . . . . . . . . . . 13 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷 ∈ (𝐷(LineG‘𝐺)𝑋))
215106ad5antr 717 . . . . . . . . . . . . . . 15 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷𝐵)
216215necomd 3001 . . . . . . . . . . . . . 14 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵𝐷)
2171, 2, 3, 195, 198, 196, 216tglinerflx1 25770 . . . . . . . . . . . . 13 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 ∈ (𝐵(LineG‘𝐺)𝐷))
2181, 2, 3, 195, 198, 196, 216tglinerflx2 25771 . . . . . . . . . . . . 13 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷 ∈ (𝐵(LineG‘𝐺)𝐷))
2191, 2, 3, 195, 196, 197, 198, 196, 206, 212, 214, 217, 218tglineinteq 25782 . . . . . . . . . . . 12 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 = 𝐷)
220219eqcomd 2780 . . . . . . . . . . 11 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷 = 𝐵)
221215neneqd 2951 . . . . . . . . . . 11 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → ¬ 𝐷 = 𝐵)
222220, 221pm2.65da 840 . . . . . . . . . 10 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → ¬ 𝑒 = 𝐵)
223222neqned 2953 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒𝐵)
2241, 2, 22, 189, 188, 187, 190, 188, 192, 194, 223btwnhl1 25749 . . . . . . . 8 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒(𝐾𝐵)𝐴)
2251, 2, 22, 187, 188, 189, 190, 224hlcomd 25741 . . . . . . 7 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐴(𝐾𝐵)𝑒)
226179ad3antrrr 710 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝐺 ∈ TarskiG)
227183ad3antrrr 710 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝐷𝑃)
228 simplr 774 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝑒𝑃)
229180ad3antrrr 710 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝑋𝑃)
230 simpr 472 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝑒 ∈ (𝐷𝐼𝑋))
2311, 16, 2, 226, 227, 228, 229, 230tgbtwncom 25625 . . . . . . . 8 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝑒 ∈ (𝑋𝐼𝐷))
232231adantrl 696 . . . . . . 7 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒 ∈ (𝑋𝐼𝐷))
233225, 232jca 502 . . . . . 6 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
234233ex 398 . . . . 5 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) → ((𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷))))
235234reximdva 3168 . . . 4 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → (∃𝑒𝑃 (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷))))
236186, 235mpd 15 . . 3 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
237178, 236pm2.61dan 836 . 2 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
23876simp3d 1165 . 2 (𝜑 → (𝐶 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐶)))
23952, 237, 238mpjaodan 970 1 (𝜑 → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 383  wo 863  w3a 1098   = wceq 1634  wcel 2148  wne 2946  wrex 3065   class class class wbr 4797  cfv 6042  (class class class)co 6812  Basecbs 16084  distcds 16178  TarskiGcstrkg 25571  Itvcitv 25577  LineGclng 25578  hlGchlg 25737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-8 2150  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754  ax-rep 4917  ax-sep 4928  ax-nul 4936  ax-pow 4988  ax-pr 5048  ax-un 7117  ax-cnex 10215  ax-resscn 10216  ax-1cn 10217  ax-icn 10218  ax-addcl 10219  ax-addrcl 10220  ax-mulcl 10221  ax-mulrcl 10222  ax-mulcom 10223  ax-addass 10224  ax-mulass 10225  ax-distr 10226  ax-i2m1 10227  ax-1ne0 10228  ax-1rid 10229  ax-rnegex 10230  ax-rrecex 10231  ax-cnre 10232  ax-pre-lttri 10233  ax-pre-lttrn 10234  ax-pre-ltadd 10235  ax-pre-mulgt0 10236
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-3or 1099  df-3an 1100  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-eu 2625  df-mo 2626  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-ne 2947  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3071  df-rmo 3072  df-rab 3073  df-v 3357  df-sbc 3594  df-csb 3689  df-dif 3732  df-un 3734  df-in 3736  df-ss 3743  df-pss 3745  df-nul 4074  df-if 4236  df-pw 4309  df-sn 4327  df-pr 4329  df-tp 4331  df-op 4333  df-uni 4586  df-int 4623  df-iun 4667  df-br 4798  df-opab 4860  df-mpt 4877  df-tr 4900  df-id 5171  df-eprel 5176  df-po 5184  df-so 5185  df-fr 5222  df-we 5224  df-xp 5269  df-rel 5270  df-cnv 5271  df-co 5272  df-dm 5273  df-rn 5274  df-res 5275  df-ima 5276  df-pred 5834  df-ord 5880  df-on 5881  df-lim 5882  df-suc 5883  df-iota 6005  df-fun 6044  df-fn 6045  df-f 6046  df-f1 6047  df-fo 6048  df-f1o 6049  df-fv 6050  df-riota 6773  df-ov 6815  df-oprab 6816  df-mpt2 6817  df-om 7234  df-1st 7336  df-2nd 7337  df-wrecs 7580  df-recs 7642  df-rdg 7680  df-1o 7734  df-oadd 7738  df-er 7917  df-map 8032  df-pm 8033  df-en 8131  df-dom 8132  df-sdom 8133  df-fin 8134  df-card 8986  df-cda 9213  df-pnf 10299  df-mnf 10300  df-xr 10301  df-ltxr 10302  df-le 10303  df-sub 10491  df-neg 10492  df-nn 11244  df-2 11302  df-3 11303  df-n0 11517  df-xnn0 11588  df-z 11602  df-uz 11911  df-fz 12556  df-fzo 12696  df-hash 13344  df-word 13517  df-concat 13519  df-s1 13520  df-s2 13824  df-s3 13825  df-trkgc 25589  df-trkgb 25590  df-trkgcb 25591  df-trkgld 25593  df-trkg 25594  df-cgrg 25648  df-leg 25720  df-hlg 25738  df-mir 25790  df-rag 25831  df-perpg 25833
This theorem is referenced by:  inaghl  25973
  Copyright terms: Public domain W3C validator