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

Theorem hlpasch 27698
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 2736 . . . 4 (LineG‘𝐺) = (LineG‘𝐺)
4 hlpasch.g . . . . 5 (𝜑𝐺 ∈ TarskiG)
54adantr 481 . . . 4 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → 𝐺 ∈ TarskiG)
6 hlpasch.5 . . . . 5 (𝜑𝐷𝑃)
76adantr 481 . . . 4 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → 𝐷𝑃)
8 hlpasch.4 . . . . 5 (𝜑𝑋𝑃)
98adantr 481 . . . 4 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → 𝑋𝑃)
10 hlpasch.3 . . . . 5 (𝜑𝐶𝑃)
1110adantr 481 . . . 4 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → 𝐶𝑃)
12 hlpasch.2 . . . . 5 (𝜑𝐵𝑃)
1312adantr 481 . . . 4 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → 𝐵𝑃)
14 hlpasch.1 . . . . 5 (𝜑𝐴𝑃)
1514adantr 481 . . . 4 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → 𝐴𝑃)
16 eqid 2736 . . . . 5 (dist‘𝐺) = (dist‘𝐺)
17 simpr 485 . . . . 5 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → 𝐶 ∈ (𝐵𝐼𝐷))
181, 16, 2, 5, 13, 11, 7, 17tgbtwncom 27430 . . . 4 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → 𝐶 ∈ (𝐷𝐼𝐵))
19 hlpasch.8 . . . . 5 (𝜑𝐴 ∈ (𝑋𝐼𝐶))
2019adantr 481 . . . 4 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → 𝐴 ∈ (𝑋𝐼𝐶))
211, 2, 3, 5, 7, 9, 11, 13, 15, 18, 20outpasch 27697 . . 3 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → ∃𝑒𝑃 (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒)))
22 hlpasch.k . . . . . . 7 𝐾 = (hlG‘𝐺)
23 simplr 767 . . . . . . 7 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑒𝑃)
2413ad2antrr 724 . . . . . . 7 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐵𝑃)
2515ad2antrr 724 . . . . . . 7 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴𝑃)
265ad2antrr 724 . . . . . . 7 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐺 ∈ TarskiG)
27 simprr 771 . . . . . . . 8 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴 ∈ (𝐵𝐼𝑒))
281, 16, 2, 26, 24, 25, 23, 27tgbtwncom 27430 . . . . . . 7 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴 ∈ (𝑒𝐼𝐵))
2926adantr 481 . . . . . . . . . . 11 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐺 ∈ TarskiG)
3024adantr 481 . . . . . . . . . . 11 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐵𝑃)
3125adantr 481 . . . . . . . . . . 11 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴𝑃)
32 simplrr 776 . . . . . . . . . . . 12 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴 ∈ (𝐵𝐼𝑒))
33 simpr 485 . . . . . . . . . . . . 13 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝑒 = 𝐵)
3433oveq2d 7373 . . . . . . . . . . . 12 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → (𝐵𝐼𝑒) = (𝐵𝐼𝐵))
3532, 34eleqtrd 2840 . . . . . . . . . . 11 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴 ∈ (𝐵𝐼𝐵))
361, 16, 2, 29, 30, 31, 35axtgbtwnid 27408 . . . . . . . . . 10 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐵 = 𝐴)
3736eqcomd 2742 . . . . . . . . 9 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴 = 𝐵)
38 hlpasch.6 . . . . . . . . . . . 12 (𝜑𝐴𝐵)
3938ad3antrrr 728 . . . . . . . . . . 11 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴𝐵)
4039adantr 481 . . . . . . . . . 10 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴𝐵)
4140neneqd 2948 . . . . . . . . 9 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → ¬ 𝐴 = 𝐵)
4237, 41pm2.65da 815 . . . . . . . 8 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → ¬ 𝑒 = 𝐵)
4342neqned 2950 . . . . . . 7 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑒𝐵)
441, 2, 22, 23, 24, 25, 26, 25, 28, 43, 39btwnhl2 27555 . . . . . 6 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴(𝐾𝐵)𝑒)
457ad2antrr 724 . . . . . . 7 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐷𝑃)
469ad2antrr 724 . . . . . . 7 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑋𝑃)
47 simprl 769 . . . . . . 7 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑒 ∈ (𝐷𝐼𝑋))
481, 16, 2, 26, 45, 23, 46, 47tgbtwncom 27430 . . . . . 6 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑒 ∈ (𝑋𝐼𝐷))
4944, 48jca 512 . . . . 5 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
5049ex 413 . . . 4 (((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) → ((𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒)) → (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷))))
5150reximdva 3165 . . 3 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → (∃𝑒𝑃 (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒)) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷))))
5221, 51mpd 15 . 2 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
536ad2antrr 724 . . . . . 6 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐷𝑃)
5453adantr 481 . . . . 5 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐷𝑃)
55 simpr 485 . . . . . . 7 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) ∧ 𝑒 = 𝐷) → 𝑒 = 𝐷)
5655breq2d 5117 . . . . . 6 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) ∧ 𝑒 = 𝐷) → (𝐴(𝐾𝐵)𝑒𝐴(𝐾𝐵)𝐷))
5755eleq1d 2822 . . . . . 6 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) ∧ 𝑒 = 𝐷) → (𝑒 ∈ (𝑋𝐼𝐷) ↔ 𝐷 ∈ (𝑋𝐼𝐷)))
5856, 57anbi12d 631 . . . . 5 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) ∧ 𝑒 = 𝐷) → ((𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)) ↔ (𝐴(𝐾𝐵)𝐷𝐷 ∈ (𝑋𝐼𝐷))))
5914ad2antrr 724 . . . . . . . 8 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐴𝑃)
6059adantr 481 . . . . . . 7 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴𝑃)
6112ad2antrr 724 . . . . . . . 8 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐵𝑃)
6261adantr 481 . . . . . . 7 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐵𝑃)
634ad2antrr 724 . . . . . . . 8 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐺 ∈ TarskiG)
6463adantr 481 . . . . . . 7 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐺 ∈ TarskiG)
65 hlpasch.7 . . . . . . . . . 10 (𝜑𝐶(𝐾𝐵)𝐷)
661, 2, 22, 10, 6, 12, 4, 65hlcomd 27546 . . . . . . . . 9 (𝜑𝐷(𝐾𝐵)𝐶)
6766ad3antrrr 728 . . . . . . . 8 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐷(𝐾𝐵)𝐶)
6810adantr 481 . . . . . . . . . 10 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → 𝐶𝑃)
6968ad2antrr 724 . . . . . . . . 9 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐶𝑃)
7019adantr 481 . . . . . . . . . . 11 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → 𝐴 ∈ (𝑋𝐼𝐶))
7170ad2antrr 724 . . . . . . . . . 10 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴 ∈ (𝑋𝐼𝐶))
72 simpr 485 . . . . . . . . . . 11 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝑋 = 𝐵)
7372oveq1d 7372 . . . . . . . . . 10 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → (𝑋𝐼𝐶) = (𝐵𝐼𝐶))
7471, 73eleqtrd 2840 . . . . . . . . 9 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴 ∈ (𝐵𝐼𝐶))
751, 2, 22, 10, 6, 12, 4ishlg 27544 . . . . . . . . . . . 12 (𝜑 → (𝐶(𝐾𝐵)𝐷 ↔ (𝐶𝐵𝐷𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐶)))))
7665, 75mpbid 231 . . . . . . . . . . 11 (𝜑 → (𝐶𝐵𝐷𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐶))))
7776simp1d 1142 . . . . . . . . . 10 (𝜑𝐶𝐵)
7877ad3antrrr 728 . . . . . . . . 9 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐶𝐵)
7938ad2antrr 724 . . . . . . . . . 10 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐴𝐵)
8079adantr 481 . . . . . . . . 9 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴𝐵)
811, 2, 22, 54, 69, 62, 64, 60, 74, 78, 80hlbtwn 27553 . . . . . . . 8 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → (𝐷(𝐾𝐵)𝐶𝐷(𝐾𝐵)𝐴))
8267, 81mpbid 231 . . . . . . 7 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐷(𝐾𝐵)𝐴)
831, 2, 22, 54, 60, 62, 64, 82hlcomd 27546 . . . . . 6 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴(𝐾𝐵)𝐷)
848ad2antrr 724 . . . . . . . 8 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝑋𝑃)
8584adantr 481 . . . . . . 7 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝑋𝑃)
861, 16, 2, 64, 85, 54tgbtwntriv2 27429 . . . . . 6 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐷 ∈ (𝑋𝐼𝐷))
8783, 86jca 512 . . . . 5 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → (𝐴(𝐾𝐵)𝐷𝐷 ∈ (𝑋𝐼𝐷)))
8854, 58, 87rspcedvd 3583 . . . 4 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
8984ad2antrr 724 . . . . . 6 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐴(𝐾𝐵)𝑋) → 𝑋𝑃)
90 simpr 485 . . . . . . . . 9 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 = 𝑋) → 𝑒 = 𝑋)
9190breq2d 5117 . . . . . . . 8 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 = 𝑋) → (𝐴(𝐾𝐵)𝑒𝐴(𝐾𝐵)𝑋))
9290eleq1d 2822 . . . . . . . 8 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 = 𝑋) → (𝑒 ∈ (𝑋𝐼𝐷) ↔ 𝑋 ∈ (𝑋𝐼𝐷)))
9391, 92anbi12d 631 . . . . . . 7 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 = 𝑋) → ((𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)) ↔ (𝐴(𝐾𝐵)𝑋𝑋 ∈ (𝑋𝐼𝐷))))
9493ad4ant14 750 . . . . . 6 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐴(𝐾𝐵)𝑋) ∧ 𝑒 = 𝑋) → ((𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)) ↔ (𝐴(𝐾𝐵)𝑋𝑋 ∈ (𝑋𝐼𝐷))))
95 simpr 485 . . . . . . 7 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐴(𝐾𝐵)𝑋) → 𝐴(𝐾𝐵)𝑋)
961, 16, 2, 63, 84, 53tgbtwntriv1 27433 . . . . . . . 8 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝑋 ∈ (𝑋𝐼𝐷))
9796ad2antrr 724 . . . . . . 7 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐴(𝐾𝐵)𝑋) → 𝑋 ∈ (𝑋𝐼𝐷))
9895, 97jca 512 . . . . . 6 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐴(𝐾𝐵)𝑋) → (𝐴(𝐾𝐵)𝑋𝑋 ∈ (𝑋𝐼𝐷)))
9989, 94, 98rspcedvd 3583 . . . . 5 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐴(𝐾𝐵)𝑋) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
10053ad2antrr 724 . . . . . 6 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐷𝑃)
101 simpr 485 . . . . . . . 8 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) ∧ 𝑒 = 𝐷) → 𝑒 = 𝐷)
102101breq2d 5117 . . . . . . 7 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) ∧ 𝑒 = 𝐷) → (𝐴(𝐾𝐵)𝑒𝐴(𝐾𝐵)𝐷))
103101eleq1d 2822 . . . . . . 7 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) ∧ 𝑒 = 𝐷) → (𝑒 ∈ (𝑋𝐼𝐷) ↔ 𝐷 ∈ (𝑋𝐼𝐷)))
104102, 103anbi12d 631 . . . . . 6 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) ∧ 𝑒 = 𝐷) → ((𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)) ↔ (𝐴(𝐾𝐵)𝐷𝐷 ∈ (𝑋𝐼𝐷))))
10579ad2antrr 724 . . . . . . . 8 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴𝐵)
1061, 2, 22, 10, 6, 12, 4, 65hlne2 27548 . . . . . . . . 9 (𝜑𝐷𝐵)
107106ad4antr 730 . . . . . . . 8 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐷𝐵)
10863ad2antrr 724 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐺 ∈ TarskiG)
10961ad2antrr 724 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐵𝑃)
11059ad2antrr 724 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴𝑃)
11168ad2antrr 724 . . . . . . . . . 10 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐶𝑃)
112111adantr 481 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐶𝑃)
11384ad2antrr 724 . . . . . . . . . 10 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝑋𝑃)
114 simpr 485 . . . . . . . . . 10 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐵 ∈ (𝑋𝐼𝐴))
11570ad2antrr 724 . . . . . . . . . . 11 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐴 ∈ (𝑋𝐼𝐶))
116115adantr 481 . . . . . . . . . 10 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴 ∈ (𝑋𝐼𝐶))
1171, 16, 2, 108, 113, 109, 110, 112, 114, 116tgbtwnexch3 27436 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴 ∈ (𝐵𝐼𝐶))
118 simp-4r 782 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐷 ∈ (𝐵𝐼𝐶))
1191, 2, 108, 109, 110, 100, 112, 117, 118tgbtwnconn3 27519 . . . . . . . 8 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → (𝐴 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐴)))
1201, 2, 22, 14, 6, 12, 4ishlg 27544 . . . . . . . . 9 (𝜑 → (𝐴(𝐾𝐵)𝐷 ↔ (𝐴𝐵𝐷𝐵 ∧ (𝐴 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐴)))))
121120ad4antr 730 . . . . . . . 8 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → (𝐴(𝐾𝐵)𝐷 ↔ (𝐴𝐵𝐷𝐵 ∧ (𝐴 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐴)))))
122105, 107, 119, 121mpbir3and 1342 . . . . . . 7 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴(𝐾𝐵)𝐷)
1231, 16, 2, 108, 113, 100tgbtwntriv2 27429 . . . . . . 7 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐷 ∈ (𝑋𝐼𝐷))
124122, 123jca 512 . . . . . 6 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → (𝐴(𝐾𝐵)𝐷𝐷 ∈ (𝑋𝐼𝐷)))
125100, 104, 124rspcedvd 3583 . . . . 5 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
1268ad3antrrr 728 . . . . . 6 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝑋𝑃)
12712ad3antrrr 728 . . . . . 6 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐵𝑃)
12814ad3antrrr 728 . . . . . 6 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐴𝑃)
1294ad3antrrr 728 . . . . . 6 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐺 ∈ TarskiG)
130 simpr 485 . . . . . . . 8 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝑋𝐵)
131130neneqd 2948 . . . . . . 7 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → ¬ 𝑋 = 𝐵)
13263adantr 481 . . . . . . . . . 10 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐺 ∈ TarskiG)
133132adantr 481 . . . . . . . . . . . . . 14 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋 = 𝐶) → 𝐺 ∈ TarskiG)
134126adantr 481 . . . . . . . . . . . . . 14 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋 = 𝐶) → 𝑋𝑃)
135128adantr 481 . . . . . . . . . . . . . 14 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋 = 𝐶) → 𝐴𝑃)
136115adantr 481 . . . . . . . . . . . . . . 15 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋 = 𝐶) → 𝐴 ∈ (𝑋𝐼𝐶))
137 simpr 485 . . . . . . . . . . . . . . . 16 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋 = 𝐶) → 𝑋 = 𝐶)
138137oveq2d 7373 . . . . . . . . . . . . . . 15 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋 = 𝐶) → (𝑋𝐼𝑋) = (𝑋𝐼𝐶))
139136, 138eleqtrrd 2841 . . . . . . . . . . . . . 14 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋 = 𝐶) → 𝐴 ∈ (𝑋𝐼𝑋))
1401, 16, 2, 133, 134, 135, 139axtgbtwnid 27408 . . . . . . . . . . . . 13 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋 = 𝐶) → 𝑋 = 𝐴)
141140olcd 872 . . . . . . . . . . . 12 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋 = 𝐶) → (𝐵 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
142132adantr 481 . . . . . . . . . . . . 13 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → 𝐺 ∈ TarskiG)
143127adantr 481 . . . . . . . . . . . . 13 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → 𝐵𝑃)
144111adantr 481 . . . . . . . . . . . . 13 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → 𝐶𝑃)
145126adantr 481 . . . . . . . . . . . . 13 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → 𝑋𝑃)
146128adantr 481 . . . . . . . . . . . . 13 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → 𝐴𝑃)
147 simpr 485 . . . . . . . . . . . . . . . 16 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → 𝑋𝐶)
148147necomd 2999 . . . . . . . . . . . . . . 15 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → 𝐶𝑋)
149148neneqd 2948 . . . . . . . . . . . . . 14 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → ¬ 𝐶 = 𝑋)
15053adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐷𝑃)
151106ad3antrrr 728 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐷𝐵)
152 simplr 767 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷))
1531, 2, 3, 132, 150, 127, 126, 151, 152lncom 27564 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝑋 ∈ (𝐷(LineG‘𝐺)𝐵))
15477necomd 2999 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐵𝐶)
155154ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐵𝐶)
15666ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐷(𝐾𝐵)𝐶)
1571, 2, 22, 150, 111, 127, 132, 3, 156hlln 27549 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐷 ∈ (𝐶(LineG‘𝐺)𝐵))
1581, 2, 3, 132, 127, 111, 150, 155, 157lncom 27564 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐷 ∈ (𝐵(LineG‘𝐺)𝐶))
159158orcd 871 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝐷 ∈ (𝐵(LineG‘𝐺)𝐶) ∨ 𝐵 = 𝐶))
1601, 2, 3, 132, 126, 150, 127, 111, 153, 159coltr 27589 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝑋 ∈ (𝐵(LineG‘𝐺)𝐶) ∨ 𝐵 = 𝐶))
1611, 3, 2, 132, 127, 111, 126, 160colrot1 27501 . . . . . . . . . . . . . . . . 17 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝐵 ∈ (𝐶(LineG‘𝐺)𝑋) ∨ 𝐶 = 𝑋))
162161orcomd 869 . . . . . . . . . . . . . . . 16 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝐶 = 𝑋𝐵 ∈ (𝐶(LineG‘𝐺)𝑋)))
163162adantr 481 . . . . . . . . . . . . . . 15 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → (𝐶 = 𝑋𝐵 ∈ (𝐶(LineG‘𝐺)𝑋)))
164163ord 862 . . . . . . . . . . . . . 14 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → (¬ 𝐶 = 𝑋𝐵 ∈ (𝐶(LineG‘𝐺)𝑋)))
165149, 164mpd 15 . . . . . . . . . . . . 13 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → 𝐵 ∈ (𝐶(LineG‘𝐺)𝑋))
1661, 3, 2, 132, 126, 128, 111, 115btwncolg3 27499 . . . . . . . . . . . . . 14 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝐶 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
167166adantr 481 . . . . . . . . . . . . 13 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → (𝐶 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
1681, 2, 3, 142, 143, 144, 145, 146, 165, 167coltr 27589 . . . . . . . . . . . 12 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → (𝐵 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
169141, 168pm2.61dane 3032 . . . . . . . . . . 11 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝐵 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
1701, 3, 2, 132, 126, 128, 127, 169colrot2 27502 . . . . . . . . . 10 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝐴 ∈ (𝐵(LineG‘𝐺)𝑋) ∨ 𝐵 = 𝑋))
1711, 3, 2, 132, 127, 126, 128, 170colcom 27500 . . . . . . . . 9 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝐴 ∈ (𝑋(LineG‘𝐺)𝐵) ∨ 𝑋 = 𝐵))
172171orcomd 869 . . . . . . . 8 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝑋 = 𝐵𝐴 ∈ (𝑋(LineG‘𝐺)𝐵)))
173172ord 862 . . . . . . 7 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (¬ 𝑋 = 𝐵𝐴 ∈ (𝑋(LineG‘𝐺)𝐵)))
174131, 173mpd 15 . . . . . 6 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐴 ∈ (𝑋(LineG‘𝐺)𝐵))
1751, 2, 22, 126, 127, 128, 129, 128, 3, 174lnhl 27557 . . . . 5 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝐴(𝐾𝐵)𝑋𝐵 ∈ (𝑋𝐼𝐴)))
17699, 125, 175mpjaodan 957 . . . 4 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
17788, 176pm2.61dane 3032 . . 3 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
1784adantr 481 . . . . . 6 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → 𝐺 ∈ TarskiG)
1798adantr 481 . . . . . 6 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → 𝑋𝑃)
18012adantr 481 . . . . . 6 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → 𝐵𝑃)
18114adantr 481 . . . . . 6 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → 𝐴𝑃)
1826adantr 481 . . . . . 6 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → 𝐷𝑃)
183 simpr 485 . . . . . 6 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → 𝐷 ∈ (𝐵𝐼𝐶))
1841, 16, 2, 178, 179, 180, 68, 181, 182, 70, 183axtgpasch 27409 . . . . 5 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → ∃𝑒𝑃 (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋)))
185184adantr 481 . . . 4 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → ∃𝑒𝑃 (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋)))
186 simplr 767 . . . . . . . 8 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒𝑃)
187181ad3antrrr 728 . . . . . . . 8 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐴𝑃)
188180ad3antrrr 728 . . . . . . . 8 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐵𝑃)
189178ad3antrrr 728 . . . . . . . 8 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐺 ∈ TarskiG)
190 simprl 769 . . . . . . . . . 10 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒 ∈ (𝐴𝐼𝐵))
1911, 16, 2, 189, 187, 186, 188, 190tgbtwncom 27430 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒 ∈ (𝐵𝐼𝐴))
19238necomd 2999 . . . . . . . . . 10 (𝜑𝐵𝐴)
193192ad4antr 730 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐵𝐴)
194189adantr 481 . . . . . . . . . . . 12 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐺 ∈ TarskiG)
1956ad5antr 732 . . . . . . . . . . . 12 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷𝑃)
1968ad5antr 732 . . . . . . . . . . . 12 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑋𝑃)
197188adantr 481 . . . . . . . . . . . 12 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵𝑃)
198 simp-4r 782 . . . . . . . . . . . . . 14 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷))
199106necomd 2999 . . . . . . . . . . . . . . . 16 (𝜑𝐵𝐷)
200199ad5antr 732 . . . . . . . . . . . . . . 15 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵𝐷)
201200neneqd 2948 . . . . . . . . . . . . . 14 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → ¬ 𝐵 = 𝐷)
202 ioran 982 . . . . . . . . . . . . . 14 (¬ (𝑋 ∈ (𝐵(LineG‘𝐺)𝐷) ∨ 𝐵 = 𝐷) ↔ (¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷) ∧ ¬ 𝐵 = 𝐷))
203198, 201, 202sylanbrc 583 . . . . . . . . . . . . 13 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → ¬ (𝑋 ∈ (𝐵(LineG‘𝐺)𝐷) ∨ 𝐵 = 𝐷))
2041, 3, 2, 194, 197, 195, 196, 203ncolrot2 27505 . . . . . . . . . . . 12 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → ¬ (𝐷 ∈ (𝑋(LineG‘𝐺)𝐵) ∨ 𝑋 = 𝐵))
205 simpr 485 . . . . . . . . . . . . 13 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑒 = 𝐵)
206186adantr 481 . . . . . . . . . . . . . 14 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑒𝑃)
2071, 2, 3, 194, 195, 196, 197, 204ncolne1 27567 . . . . . . . . . . . . . 14 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷𝑋)
208 simplrr 776 . . . . . . . . . . . . . 14 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑒 ∈ (𝐷𝐼𝑋))
2091, 2, 3, 194, 195, 196, 206, 207, 208btwnlng1 27561 . . . . . . . . . . . . 13 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑒 ∈ (𝐷(LineG‘𝐺)𝑋))
210205, 209eqeltrrd 2839 . . . . . . . . . . . 12 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 ∈ (𝐷(LineG‘𝐺)𝑋))
2111, 2, 3, 194, 195, 196, 207tglinerflx1 27575 . . . . . . . . . . . 12 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷 ∈ (𝐷(LineG‘𝐺)𝑋))
212106ad5antr 732 . . . . . . . . . . . . . 14 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷𝐵)
213212necomd 2999 . . . . . . . . . . . . 13 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵𝐷)
2141, 2, 3, 194, 197, 195, 213tglinerflx1 27575 . . . . . . . . . . . 12 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 ∈ (𝐵(LineG‘𝐺)𝐷))
2151, 2, 3, 194, 197, 195, 213tglinerflx2 27576 . . . . . . . . . . . 12 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷 ∈ (𝐵(LineG‘𝐺)𝐷))
2161, 2, 3, 194, 195, 196, 197, 195, 204, 210, 211, 214, 215tglineinteq 27587 . . . . . . . . . . 11 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 = 𝐷)
217216, 201pm2.65da 815 . . . . . . . . . 10 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → ¬ 𝑒 = 𝐵)
218217neqned 2950 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒𝐵)
2191, 2, 22, 188, 187, 186, 189, 187, 191, 193, 218btwnhl1 27554 . . . . . . . 8 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒(𝐾𝐵)𝐴)
2201, 2, 22, 186, 187, 188, 189, 219hlcomd 27546 . . . . . . 7 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐴(𝐾𝐵)𝑒)
221178ad3antrrr 728 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝐺 ∈ TarskiG)
222182ad3antrrr 728 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝐷𝑃)
223 simplr 767 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝑒𝑃)
224179ad3antrrr 728 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝑋𝑃)
225 simpr 485 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝑒 ∈ (𝐷𝐼𝑋))
2261, 16, 2, 221, 222, 223, 224, 225tgbtwncom 27430 . . . . . . . 8 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝑒 ∈ (𝑋𝐼𝐷))
227226adantrl 714 . . . . . . 7 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒 ∈ (𝑋𝐼𝐷))
228220, 227jca 512 . . . . . 6 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
229228ex 413 . . . . 5 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) → ((𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷))))
230229reximdva 3165 . . . 4 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → (∃𝑒𝑃 (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷))))
231185, 230mpd 15 . . 3 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
232177, 231pm2.61dan 811 . 2 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
23376simp3d 1144 . 2 (𝜑 → (𝐶 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐶)))
23452, 232, 233mpjaodan 957 1 (𝜑 → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845  w3a 1087   = wceq 1541  wcel 2106  wne 2943  wrex 3073   class class class wbr 5105  cfv 6496  (class class class)co 7357  Basecbs 17083  distcds 17142  TarskiGcstrkg 27369  Itvcitv 27375  LineGclng 27376  hlGchlg 27542
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-oadd 8416  df-er 8648  df-map 8767  df-pm 8768  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-dju 9837  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-nn 12154  df-2 12216  df-3 12217  df-n0 12414  df-xnn0 12486  df-z 12500  df-uz 12764  df-fz 13425  df-fzo 13568  df-hash 14231  df-word 14403  df-concat 14459  df-s1 14484  df-s2 14737  df-s3 14738  df-trkgc 27390  df-trkgb 27391  df-trkgcb 27392  df-trkgld 27394  df-trkg 27395  df-cgrg 27453  df-leg 27525  df-hlg 27543  df-mir 27595  df-rag 27636  df-perpg 27638
This theorem is referenced by:  inaghl  27787
  Copyright terms: Public domain W3C validator