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

Theorem hlpasch 25548
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 2621 . . . 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 2621 . . . . 5 (dist‘𝐺) = (dist‘𝐺)
17 simpr 477 . . . . 5 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → 𝐶 ∈ (𝐵𝐼𝐷))
181, 16, 2, 5, 13, 11, 7, 17tgbtwncom 25283 . . . 4 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → 𝐶 ∈ (𝐷𝐼𝐵))
19 hlpasch.8 . . . . 5 (𝜑𝐴 ∈ (𝑋𝐼𝐶))
2019adantr 481 . . . 4 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → 𝐴 ∈ (𝑋𝐼𝐶))
211, 2, 3, 5, 7, 9, 11, 13, 15, 18, 20outpasch 25547 . . 3 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → ∃𝑒𝑃 (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒)))
22 hlpasch.k . . . . . . 7 𝐾 = (hlG‘𝐺)
23 simplr 791 . . . . . . 7 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑒𝑃)
2413ad2antrr 761 . . . . . . 7 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐵𝑃)
2515ad2antrr 761 . . . . . . 7 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴𝑃)
265ad2antrr 761 . . . . . . 7 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐺 ∈ TarskiG)
27 simprr 795 . . . . . . . 8 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴 ∈ (𝐵𝐼𝑒))
281, 16, 2, 26, 24, 25, 23, 27tgbtwncom 25283 . . . . . . 7 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴 ∈ (𝑒𝐼𝐵))
2926adantr 481 . . . . . . . . . . 11 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐺 ∈ TarskiG)
3024adantr 481 . . . . . . . . . . 11 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐵𝑃)
3125adantr 481 . . . . . . . . . . 11 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴𝑃)
3227adantr 481 . . . . . . . . . . . 12 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴 ∈ (𝐵𝐼𝑒))
33 simpr 477 . . . . . . . . . . . . 13 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝑒 = 𝐵)
3433oveq2d 6620 . . . . . . . . . . . 12 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → (𝐵𝐼𝑒) = (𝐵𝐼𝐵))
3532, 34eleqtrd 2700 . . . . . . . . . . 11 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴 ∈ (𝐵𝐼𝐵))
361, 16, 2, 29, 30, 31, 35axtgbtwnid 25265 . . . . . . . . . 10 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐵 = 𝐴)
3736eqcomd 2627 . . . . . . . . 9 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴 = 𝐵)
38 hlpasch.6 . . . . . . . . . . . 12 (𝜑𝐴𝐵)
3938ad3antrrr 765 . . . . . . . . . . 11 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴𝐵)
4039adantr 481 . . . . . . . . . 10 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴𝐵)
4140neneqd 2795 . . . . . . . . 9 (((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → ¬ 𝐴 = 𝐵)
4237, 41pm2.65da 599 . . . . . . . 8 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → ¬ 𝑒 = 𝐵)
4342neqned 2797 . . . . . . 7 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑒𝐵)
441, 2, 22, 23, 24, 25, 26, 25, 28, 43, 39btwnhl2 25408 . . . . . 6 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴(𝐾𝐵)𝑒)
457ad2antrr 761 . . . . . . 7 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐷𝑃)
469ad2antrr 761 . . . . . . 7 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑋𝑃)
47 simprl 793 . . . . . . 7 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑒 ∈ (𝐷𝐼𝑋))
481, 16, 2, 26, 45, 23, 46, 47tgbtwncom 25283 . . . . . 6 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑒 ∈ (𝑋𝐼𝐷))
4944, 48jca 554 . . . . 5 ((((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
5049ex 450 . . . 4 (((𝜑𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒𝑃) → ((𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒)) → (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷))))
5150reximdva 3011 . . 3 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → (∃𝑒𝑃 (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒)) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷))))
5221, 51mpd 15 . 2 ((𝜑𝐶 ∈ (𝐵𝐼𝐷)) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
536ad2antrr 761 . . . . . 6 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐷𝑃)
5453adantr 481 . . . . 5 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐷𝑃)
55 simpr 477 . . . . . . 7 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) ∧ 𝑒 = 𝐷) → 𝑒 = 𝐷)
5655breq2d 4625 . . . . . 6 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) ∧ 𝑒 = 𝐷) → (𝐴(𝐾𝐵)𝑒𝐴(𝐾𝐵)𝐷))
5755eleq1d 2683 . . . . . 6 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) ∧ 𝑒 = 𝐷) → (𝑒 ∈ (𝑋𝐼𝐷) ↔ 𝐷 ∈ (𝑋𝐼𝐷)))
5856, 57anbi12d 746 . . . . 5 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) ∧ 𝑒 = 𝐷) → ((𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)) ↔ (𝐴(𝐾𝐵)𝐷𝐷 ∈ (𝑋𝐼𝐷))))
5914ad2antrr 761 . . . . . . . 8 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐴𝑃)
6059adantr 481 . . . . . . 7 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴𝑃)
6112ad2antrr 761 . . . . . . . 8 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐵𝑃)
6261adantr 481 . . . . . . 7 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐵𝑃)
634ad2antrr 761 . . . . . . . 8 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐺 ∈ TarskiG)
6463adantr 481 . . . . . . 7 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐺 ∈ TarskiG)
65 hlpasch.7 . . . . . . . . . 10 (𝜑𝐶(𝐾𝐵)𝐷)
661, 2, 22, 10, 6, 12, 4, 65hlcomd 25399 . . . . . . . . 9 (𝜑𝐷(𝐾𝐵)𝐶)
6766ad3antrrr 765 . . . . . . . 8 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐷(𝐾𝐵)𝐶)
6810adantr 481 . . . . . . . . . 10 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → 𝐶𝑃)
6968ad2antrr 761 . . . . . . . . 9 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐶𝑃)
7019adantr 481 . . . . . . . . . . 11 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → 𝐴 ∈ (𝑋𝐼𝐶))
7170ad2antrr 761 . . . . . . . . . 10 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴 ∈ (𝑋𝐼𝐶))
72 simpr 477 . . . . . . . . . . 11 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝑋 = 𝐵)
7372oveq1d 6619 . . . . . . . . . 10 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → (𝑋𝐼𝐶) = (𝐵𝐼𝐶))
7471, 73eleqtrd 2700 . . . . . . . . 9 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴 ∈ (𝐵𝐼𝐶))
751, 2, 22, 10, 6, 12, 4ishlg 25397 . . . . . . . . . . . 12 (𝜑 → (𝐶(𝐾𝐵)𝐷 ↔ (𝐶𝐵𝐷𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐶)))))
7665, 75mpbid 222 . . . . . . . . . . 11 (𝜑 → (𝐶𝐵𝐷𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐶))))
7776simp1d 1071 . . . . . . . . . 10 (𝜑𝐶𝐵)
7877ad3antrrr 765 . . . . . . . . 9 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐶𝐵)
7938ad2antrr 761 . . . . . . . . . 10 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐴𝐵)
8079adantr 481 . . . . . . . . 9 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴𝐵)
811, 2, 22, 54, 69, 62, 64, 60, 74, 78, 80hlbtwn 25406 . . . . . . . 8 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → (𝐷(𝐾𝐵)𝐶𝐷(𝐾𝐵)𝐴))
8267, 81mpbid 222 . . . . . . 7 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐷(𝐾𝐵)𝐴)
831, 2, 22, 54, 60, 62, 64, 82hlcomd 25399 . . . . . 6 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴(𝐾𝐵)𝐷)
848ad2antrr 761 . . . . . . . 8 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝑋𝑃)
8584adantr 481 . . . . . . 7 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝑋𝑃)
861, 16, 2, 64, 85, 54tgbtwntriv2 25282 . . . . . 6 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐷 ∈ (𝑋𝐼𝐷))
8783, 86jca 554 . . . . 5 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → (𝐴(𝐾𝐵)𝐷𝐷 ∈ (𝑋𝐼𝐷)))
8854, 58, 87rspcedvd 3302 . . . 4 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
8984ad2antrr 761 . . . . . 6 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐴(𝐾𝐵)𝑋) → 𝑋𝑃)
90 simpr 477 . . . . . . . . 9 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 = 𝑋) → 𝑒 = 𝑋)
9190breq2d 4625 . . . . . . . 8 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 = 𝑋) → (𝐴(𝐾𝐵)𝑒𝐴(𝐾𝐵)𝑋))
9290eleq1d 2683 . . . . . . . 8 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 = 𝑋) → (𝑒 ∈ (𝑋𝐼𝐷) ↔ 𝑋 ∈ (𝑋𝐼𝐷)))
9391, 92anbi12d 746 . . . . . . 7 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 = 𝑋) → ((𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)) ↔ (𝐴(𝐾𝐵)𝑋𝑋 ∈ (𝑋𝐼𝐷))))
9493ad4ant14 1290 . . . . . 6 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐴(𝐾𝐵)𝑋) ∧ 𝑒 = 𝑋) → ((𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)) ↔ (𝐴(𝐾𝐵)𝑋𝑋 ∈ (𝑋𝐼𝐷))))
95 simpr 477 . . . . . . 7 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐴(𝐾𝐵)𝑋) → 𝐴(𝐾𝐵)𝑋)
961, 16, 2, 63, 84, 53tgbtwntriv1 25286 . . . . . . . 8 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝑋 ∈ (𝑋𝐼𝐷))
9796ad2antrr 761 . . . . . . 7 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐴(𝐾𝐵)𝑋) → 𝑋 ∈ (𝑋𝐼𝐷))
9895, 97jca 554 . . . . . 6 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐴(𝐾𝐵)𝑋) → (𝐴(𝐾𝐵)𝑋𝑋 ∈ (𝑋𝐼𝐷)))
9989, 94, 98rspcedvd 3302 . . . . 5 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐴(𝐾𝐵)𝑋) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
10053ad2antrr 761 . . . . . 6 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐷𝑃)
101 simpr 477 . . . . . . . 8 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) ∧ 𝑒 = 𝐷) → 𝑒 = 𝐷)
102101breq2d 4625 . . . . . . 7 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) ∧ 𝑒 = 𝐷) → (𝐴(𝐾𝐵)𝑒𝐴(𝐾𝐵)𝐷))
103101eleq1d 2683 . . . . . . 7 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) ∧ 𝑒 = 𝐷) → (𝑒 ∈ (𝑋𝐼𝐷) ↔ 𝐷 ∈ (𝑋𝐼𝐷)))
104102, 103anbi12d 746 . . . . . 6 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) ∧ 𝑒 = 𝐷) → ((𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)) ↔ (𝐴(𝐾𝐵)𝐷𝐷 ∈ (𝑋𝐼𝐷))))
10579ad2antrr 761 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴𝐵)
1061, 2, 22, 10, 6, 12, 4, 65hlne2 25401 . . . . . . . . . 10 (𝜑𝐷𝐵)
107106ad4antr 767 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐷𝐵)
10863ad2antrr 761 . . . . . . . . . 10 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐺 ∈ TarskiG)
10961ad2antrr 761 . . . . . . . . . 10 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐵𝑃)
11059ad2antrr 761 . . . . . . . . . 10 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴𝑃)
11168ad2antrr 761 . . . . . . . . . . 11 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐶𝑃)
112111adantr 481 . . . . . . . . . 10 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐶𝑃)
11384ad2antrr 761 . . . . . . . . . . 11 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝑋𝑃)
114 simpr 477 . . . . . . . . . . 11 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐵 ∈ (𝑋𝐼𝐴))
11570ad2antrr 761 . . . . . . . . . . . 12 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐴 ∈ (𝑋𝐼𝐶))
116115adantr 481 . . . . . . . . . . 11 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴 ∈ (𝑋𝐼𝐶))
1171, 16, 2, 108, 113, 109, 110, 112, 114, 116tgbtwnexch3 25289 . . . . . . . . . 10 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴 ∈ (𝐵𝐼𝐶))
118 simp-4r 806 . . . . . . . . . 10 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐷 ∈ (𝐵𝐼𝐶))
1191, 2, 108, 109, 110, 100, 112, 117, 118tgbtwnconn3 25372 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → (𝐴 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐴)))
120105, 107, 1193jca 1240 . . . . . . . 8 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → (𝐴𝐵𝐷𝐵 ∧ (𝐴 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐴))))
1211, 2, 22, 14, 6, 12, 4ishlg 25397 . . . . . . . . 9 (𝜑 → (𝐴(𝐾𝐵)𝐷 ↔ (𝐴𝐵𝐷𝐵 ∧ (𝐴 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐴)))))
122121ad4antr 767 . . . . . . . 8 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → (𝐴(𝐾𝐵)𝐷 ↔ (𝐴𝐵𝐷𝐵 ∧ (𝐴 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐴)))))
123120, 122mpbird 247 . . . . . . 7 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴(𝐾𝐵)𝐷)
1241, 16, 2, 108, 113, 100tgbtwntriv2 25282 . . . . . . 7 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐷 ∈ (𝑋𝐼𝐷))
125123, 124jca 554 . . . . . 6 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → (𝐴(𝐾𝐵)𝐷𝐷 ∈ (𝑋𝐼𝐷)))
126100, 104, 125rspcedvd 3302 . . . . 5 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
1278ad3antrrr 765 . . . . . 6 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝑋𝑃)
12812ad3antrrr 765 . . . . . 6 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐵𝑃)
12914ad3antrrr 765 . . . . . 6 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐴𝑃)
1304ad3antrrr 765 . . . . . 6 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐺 ∈ TarskiG)
131 simpr 477 . . . . . . . 8 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝑋𝐵)
132131neneqd 2795 . . . . . . 7 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → ¬ 𝑋 = 𝐵)
13363adantr 481 . . . . . . . . . 10 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐺 ∈ TarskiG)
134133adantr 481 . . . . . . . . . . . . . 14 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋 = 𝐶) → 𝐺 ∈ TarskiG)
135127adantr 481 . . . . . . . . . . . . . 14 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋 = 𝐶) → 𝑋𝑃)
136129adantr 481 . . . . . . . . . . . . . 14 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋 = 𝐶) → 𝐴𝑃)
137115adantr 481 . . . . . . . . . . . . . . 15 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋 = 𝐶) → 𝐴 ∈ (𝑋𝐼𝐶))
138 simpr 477 . . . . . . . . . . . . . . . 16 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋 = 𝐶) → 𝑋 = 𝐶)
139138oveq2d 6620 . . . . . . . . . . . . . . 15 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋 = 𝐶) → (𝑋𝐼𝑋) = (𝑋𝐼𝐶))
140137, 139eleqtrrd 2701 . . . . . . . . . . . . . 14 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋 = 𝐶) → 𝐴 ∈ (𝑋𝐼𝑋))
1411, 16, 2, 134, 135, 136, 140axtgbtwnid 25265 . . . . . . . . . . . . 13 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋 = 𝐶) → 𝑋 = 𝐴)
142141olcd 408 . . . . . . . . . . . 12 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋 = 𝐶) → (𝐵 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
143133adantr 481 . . . . . . . . . . . . 13 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → 𝐺 ∈ TarskiG)
144128adantr 481 . . . . . . . . . . . . 13 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → 𝐵𝑃)
145111adantr 481 . . . . . . . . . . . . 13 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → 𝐶𝑃)
146127adantr 481 . . . . . . . . . . . . 13 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → 𝑋𝑃)
147129adantr 481 . . . . . . . . . . . . 13 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → 𝐴𝑃)
148 simpr 477 . . . . . . . . . . . . . . . 16 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → 𝑋𝐶)
149148necomd 2845 . . . . . . . . . . . . . . 15 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → 𝐶𝑋)
150149neneqd 2795 . . . . . . . . . . . . . 14 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → ¬ 𝐶 = 𝑋)
15153adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐷𝑃)
152106ad3antrrr 765 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐷𝐵)
153 simplr 791 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷))
1541, 2, 3, 133, 151, 128, 127, 152, 153lncom 25417 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝑋 ∈ (𝐷(LineG‘𝐺)𝐵))
15577necomd 2845 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐵𝐶)
156155ad3antrrr 765 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐵𝐶)
15766ad3antrrr 765 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐷(𝐾𝐵)𝐶)
1581, 2, 22, 151, 111, 128, 133, 3, 157hlln 25402 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐷 ∈ (𝐶(LineG‘𝐺)𝐵))
1591, 2, 3, 133, 128, 111, 151, 156, 158lncom 25417 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐷 ∈ (𝐵(LineG‘𝐺)𝐶))
160159orcd 407 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝐷 ∈ (𝐵(LineG‘𝐺)𝐶) ∨ 𝐵 = 𝐶))
1611, 2, 3, 133, 127, 151, 128, 111, 154, 160coltr 25442 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝑋 ∈ (𝐵(LineG‘𝐺)𝐶) ∨ 𝐵 = 𝐶))
1621, 3, 2, 133, 128, 111, 127, 161colrot1 25354 . . . . . . . . . . . . . . . . 17 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝐵 ∈ (𝐶(LineG‘𝐺)𝑋) ∨ 𝐶 = 𝑋))
163162orcomd 403 . . . . . . . . . . . . . . . 16 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝐶 = 𝑋𝐵 ∈ (𝐶(LineG‘𝐺)𝑋)))
164163adantr 481 . . . . . . . . . . . . . . 15 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → (𝐶 = 𝑋𝐵 ∈ (𝐶(LineG‘𝐺)𝑋)))
165164ord 392 . . . . . . . . . . . . . 14 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → (¬ 𝐶 = 𝑋𝐵 ∈ (𝐶(LineG‘𝐺)𝑋)))
166150, 165mpd 15 . . . . . . . . . . . . 13 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → 𝐵 ∈ (𝐶(LineG‘𝐺)𝑋))
1671, 3, 2, 133, 127, 129, 111, 115btwncolg3 25352 . . . . . . . . . . . . . 14 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝐶 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
168167adantr 481 . . . . . . . . . . . . 13 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → (𝐶 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
1691, 2, 3, 143, 144, 145, 146, 147, 166, 168coltr 25442 . . . . . . . . . . . 12 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) ∧ 𝑋𝐶) → (𝐵 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
170142, 169pm2.61dane 2877 . . . . . . . . . . 11 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝐵 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
1711, 3, 2, 133, 127, 129, 128, 170colrot2 25355 . . . . . . . . . 10 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝐴 ∈ (𝐵(LineG‘𝐺)𝑋) ∨ 𝐵 = 𝑋))
1721, 3, 2, 133, 128, 127, 129, 171colcom 25353 . . . . . . . . 9 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝐴 ∈ (𝑋(LineG‘𝐺)𝐵) ∨ 𝑋 = 𝐵))
173172orcomd 403 . . . . . . . 8 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝑋 = 𝐵𝐴 ∈ (𝑋(LineG‘𝐺)𝐵)))
174173ord 392 . . . . . . 7 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (¬ 𝑋 = 𝐵𝐴 ∈ (𝑋(LineG‘𝐺)𝐵)))
175132, 174mpd 15 . . . . . 6 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → 𝐴 ∈ (𝑋(LineG‘𝐺)𝐵))
1761, 2, 22, 127, 128, 129, 130, 129, 3, 175lnhl 25410 . . . . 5 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → (𝐴(𝐾𝐵)𝑋𝐵 ∈ (𝑋𝐼𝐴)))
17799, 126, 176mpjaodan 826 . . . 4 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋𝐵) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
17888, 177pm2.61dane 2877 . . 3 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
1794adantr 481 . . . . . 6 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → 𝐺 ∈ TarskiG)
1808adantr 481 . . . . . 6 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → 𝑋𝑃)
18112adantr 481 . . . . . 6 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → 𝐵𝑃)
18214adantr 481 . . . . . 6 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → 𝐴𝑃)
1836adantr 481 . . . . . 6 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → 𝐷𝑃)
184 simpr 477 . . . . . 6 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → 𝐷 ∈ (𝐵𝐼𝐶))
1851, 16, 2, 179, 180, 181, 68, 182, 183, 70, 184axtgpasch 25266 . . . . 5 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → ∃𝑒𝑃 (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋)))
186185adantr 481 . . . 4 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → ∃𝑒𝑃 (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋)))
187 simplr 791 . . . . . . . 8 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒𝑃)
188182ad3antrrr 765 . . . . . . . 8 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐴𝑃)
189181ad3antrrr 765 . . . . . . . 8 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐵𝑃)
190179ad3antrrr 765 . . . . . . . 8 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐺 ∈ TarskiG)
191 simprl 793 . . . . . . . . . 10 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒 ∈ (𝐴𝐼𝐵))
1921, 16, 2, 190, 188, 187, 189, 191tgbtwncom 25283 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒 ∈ (𝐵𝐼𝐴))
19338necomd 2845 . . . . . . . . . 10 (𝜑𝐵𝐴)
194193ad4antr 767 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐵𝐴)
195190adantr 481 . . . . . . . . . . . . 13 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐺 ∈ TarskiG)
1966ad5antr 769 . . . . . . . . . . . . 13 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷𝑃)
1978ad5antr 769 . . . . . . . . . . . . 13 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑋𝑃)
198189adantr 481 . . . . . . . . . . . . 13 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵𝑃)
199 simp-4r 806 . . . . . . . . . . . . . . . 16 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷))
200106necomd 2845 . . . . . . . . . . . . . . . . . 18 (𝜑𝐵𝐷)
201200ad5antr 769 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵𝐷)
202201neneqd 2795 . . . . . . . . . . . . . . . 16 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → ¬ 𝐵 = 𝐷)
203199, 202jca 554 . . . . . . . . . . . . . . 15 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → (¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷) ∧ ¬ 𝐵 = 𝐷))
204 ioran 511 . . . . . . . . . . . . . . 15 (¬ (𝑋 ∈ (𝐵(LineG‘𝐺)𝐷) ∨ 𝐵 = 𝐷) ↔ (¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷) ∧ ¬ 𝐵 = 𝐷))
205203, 204sylibr 224 . . . . . . . . . . . . . 14 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → ¬ (𝑋 ∈ (𝐵(LineG‘𝐺)𝐷) ∨ 𝐵 = 𝐷))
2061, 3, 2, 195, 198, 196, 197, 205ncolrot2 25358 . . . . . . . . . . . . 13 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → ¬ (𝐷 ∈ (𝑋(LineG‘𝐺)𝐵) ∨ 𝑋 = 𝐵))
207 simpr 477 . . . . . . . . . . . . . 14 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑒 = 𝐵)
208187adantr 481 . . . . . . . . . . . . . . 15 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑒𝑃)
2091, 2, 3, 195, 196, 197, 198, 206ncolne1 25420 . . . . . . . . . . . . . . 15 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷𝑋)
210 simplrr 800 . . . . . . . . . . . . . . 15 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑒 ∈ (𝐷𝐼𝑋))
2111, 2, 3, 195, 196, 197, 208, 209, 210btwnlng1 25414 . . . . . . . . . . . . . 14 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑒 ∈ (𝐷(LineG‘𝐺)𝑋))
212207, 211eqeltrrd 2699 . . . . . . . . . . . . 13 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 ∈ (𝐷(LineG‘𝐺)𝑋))
2131, 3, 2, 195, 196, 197, 212tglngne 25345 . . . . . . . . . . . . . 14 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷𝑋)
2141, 2, 3, 195, 196, 197, 213tglinerflx1 25428 . . . . . . . . . . . . 13 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷 ∈ (𝐷(LineG‘𝐺)𝑋))
215106ad5antr 769 . . . . . . . . . . . . . . 15 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷𝐵)
216215necomd 2845 . . . . . . . . . . . . . 14 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵𝐷)
2171, 2, 3, 195, 198, 196, 216tglinerflx1 25428 . . . . . . . . . . . . 13 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 ∈ (𝐵(LineG‘𝐺)𝐷))
2181, 2, 3, 195, 198, 196, 216tglinerflx2 25429 . . . . . . . . . . . . 13 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷 ∈ (𝐵(LineG‘𝐺)𝐷))
2191, 2, 3, 195, 196, 197, 198, 196, 206, 212, 214, 217, 218tglineinteq 25440 . . . . . . . . . . . 12 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 = 𝐷)
220219eqcomd 2627 . . . . . . . . . . 11 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷 = 𝐵)
221215neneqd 2795 . . . . . . . . . . 11 ((((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → ¬ 𝐷 = 𝐵)
222220, 221pm2.65da 599 . . . . . . . . . 10 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → ¬ 𝑒 = 𝐵)
223222neqned 2797 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒𝐵)
2241, 2, 22, 189, 188, 187, 190, 188, 192, 194, 223btwnhl1 25407 . . . . . . . 8 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒(𝐾𝐵)𝐴)
2251, 2, 22, 187, 188, 189, 190, 224hlcomd 25399 . . . . . . 7 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐴(𝐾𝐵)𝑒)
226179ad3antrrr 765 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝐺 ∈ TarskiG)
227183ad3antrrr 765 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝐷𝑃)
228 simplr 791 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝑒𝑃)
229180ad3antrrr 765 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝑋𝑃)
230 simpr 477 . . . . . . . . 9 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝑒 ∈ (𝐷𝐼𝑋))
2311, 16, 2, 226, 227, 228, 229, 230tgbtwncom 25283 . . . . . . . 8 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝑒 ∈ (𝑋𝐼𝐷))
232231adantrl 751 . . . . . . 7 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒 ∈ (𝑋𝐼𝐷))
233225, 232jca 554 . . . . . 6 (((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
234233ex 450 . . . . 5 ((((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒𝑃) → ((𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷))))
235234reximdva 3011 . . . 4 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → (∃𝑒𝑃 (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷))))
236186, 235mpd 15 . . 3 (((𝜑𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
237178, 236pm2.61dan 831 . 2 ((𝜑𝐷 ∈ (𝐵𝐼𝐶)) → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
23876simp3d 1073 . 2 (𝜑 → (𝐶 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐶)))
23952, 237, 238mpjaodan 826 1 (𝜑 → ∃𝑒𝑃 (𝐴(𝐾𝐵)𝑒𝑒 ∈ (𝑋𝐼𝐷)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384  w3a 1036   = wceq 1480  wcel 1987  wne 2790  wrex 2908   class class class wbr 4613  cfv 5847  (class class class)co 6604  Basecbs 15781  distcds 15871  TarskiGcstrkg 25229  Itvcitv 25235  LineGclng 25236  hlGchlg 25395
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-cnex 9936  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956  ax-pre-mulgt0 9957
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-om 7013  df-1st 7113  df-2nd 7114  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-oadd 7509  df-er 7687  df-map 7804  df-pm 7805  df-en 7900  df-dom 7901  df-sdom 7902  df-fin 7903  df-card 8709  df-cda 8934  df-pnf 10020  df-mnf 10021  df-xr 10022  df-ltxr 10023  df-le 10024  df-sub 10212  df-neg 10213  df-nn 10965  df-2 11023  df-3 11024  df-n0 11237  df-xnn0 11308  df-z 11322  df-uz 11632  df-fz 12269  df-fzo 12407  df-hash 13058  df-word 13238  df-concat 13240  df-s1 13241  df-s2 13530  df-s3 13531  df-trkgc 25247  df-trkgb 25248  df-trkgcb 25249  df-trkgld 25251  df-trkg 25252  df-cgrg 25306  df-leg 25378  df-hlg 25396  df-mir 25448  df-rag 25489  df-perpg 25491
This theorem is referenced by:  inaghl  25631
  Copyright terms: Public domain W3C validator