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

Theorem lnopp2hpgb 27879
Description: Theorem 9.8 of [Schwabhauser] p. 71. (Contributed by Thierry Arnoux, 4-Mar-2020.)
Hypotheses
Ref Expression
ishpg.p 𝑃 = (Base‘𝐺)
ishpg.i 𝐼 = (Itv‘𝐺)
ishpg.l 𝐿 = (LineG‘𝐺)
ishpg.o 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃𝐷) ∧ 𝑏 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝑎𝐼𝑏))}
ishpg.g (𝜑𝐺 ∈ TarskiG)
ishpg.d (𝜑𝐷 ∈ ran 𝐿)
hpgbr.a (𝜑𝐴𝑃)
hpgbr.b (𝜑𝐵𝑃)
lnopp2hpgb.c (𝜑𝐶𝑃)
lnopp2hpgb.1 (𝜑𝐴𝑂𝐶)
Assertion
Ref Expression
lnopp2hpgb (𝜑 → (𝐵𝑂𝐶𝐴((hpG‘𝐺)‘𝐷)𝐵))
Distinct variable groups:   𝑡,𝐴   𝑡,𝐵   𝐶,𝑎,𝑏,𝑡   𝐷,𝑎,𝑏,𝑡   𝐺,𝑎,𝑏,𝑡   𝐼,𝑎,𝑏,𝑡   𝐿,𝑎,𝑏,𝑡   𝑂,𝑎,𝑏,𝑡   𝑃,𝑎,𝑏,𝑡   𝜑,𝑡
Allowed substitution hints:   𝜑(𝑎,𝑏)   𝐴(𝑎,𝑏)   𝐵(𝑎,𝑏)

Proof of Theorem lnopp2hpgb
Dummy variables 𝑑 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lnopp2hpgb.c . . . . 5 (𝜑𝐶𝑃)
21adantr 481 . . . 4 ((𝜑𝐵𝑂𝐶) → 𝐶𝑃)
3 lnopp2hpgb.1 . . . . 5 (𝜑𝐴𝑂𝐶)
43adantr 481 . . . 4 ((𝜑𝐵𝑂𝐶) → 𝐴𝑂𝐶)
5 simpr 485 . . . 4 ((𝜑𝐵𝑂𝐶) → 𝐵𝑂𝐶)
6 breq2 5145 . . . . . 6 (𝑑 = 𝐶 → (𝐴𝑂𝑑𝐴𝑂𝐶))
7 breq2 5145 . . . . . 6 (𝑑 = 𝐶 → (𝐵𝑂𝑑𝐵𝑂𝐶))
86, 7anbi12d 631 . . . . 5 (𝑑 = 𝐶 → ((𝐴𝑂𝑑𝐵𝑂𝑑) ↔ (𝐴𝑂𝐶𝐵𝑂𝐶)))
98rspcev 3609 . . . 4 ((𝐶𝑃 ∧ (𝐴𝑂𝐶𝐵𝑂𝐶)) → ∃𝑑𝑃 (𝐴𝑂𝑑𝐵𝑂𝑑))
102, 4, 5, 9syl12anc 835 . . 3 ((𝜑𝐵𝑂𝐶) → ∃𝑑𝑃 (𝐴𝑂𝑑𝐵𝑂𝑑))
11 ishpg.p . . . . 5 𝑃 = (Base‘𝐺)
12 ishpg.i . . . . 5 𝐼 = (Itv‘𝐺)
13 ishpg.l . . . . 5 𝐿 = (LineG‘𝐺)
14 ishpg.o . . . . 5 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃𝐷) ∧ 𝑏 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝑎𝐼𝑏))}
15 ishpg.g . . . . 5 (𝜑𝐺 ∈ TarskiG)
16 ishpg.d . . . . 5 (𝜑𝐷 ∈ ran 𝐿)
17 hpgbr.a . . . . 5 (𝜑𝐴𝑃)
18 hpgbr.b . . . . 5 (𝜑𝐵𝑃)
1911, 12, 13, 14, 15, 16, 17, 18hpgbr 27876 . . . 4 (𝜑 → (𝐴((hpG‘𝐺)‘𝐷)𝐵 ↔ ∃𝑑𝑃 (𝐴𝑂𝑑𝐵𝑂𝑑)))
2019adantr 481 . . 3 ((𝜑𝐵𝑂𝐶) → (𝐴((hpG‘𝐺)‘𝐷)𝐵 ↔ ∃𝑑𝑃 (𝐴𝑂𝑑𝐵𝑂𝑑)))
2110, 20mpbird 256 . 2 ((𝜑𝐵𝑂𝐶) → 𝐴((hpG‘𝐺)‘𝐷)𝐵)
22 eqid 2731 . . . . . . . 8 (dist‘𝐺) = (dist‘𝐺)
2316ad7antr 736 . . . . . . . . 9 ((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) → 𝐷 ∈ ran 𝐿)
2423ad3antrrr 728 . . . . . . . 8 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝐷 ∈ ran 𝐿)
2515ad7antr 736 . . . . . . . . 9 ((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) → 𝐺 ∈ TarskiG)
2625ad3antrrr 728 . . . . . . . 8 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝐺 ∈ TarskiG)
27 eqid 2731 . . . . . . . 8 (hlG‘𝐺) = (hlG‘𝐺)
2817ad3antrrr 728 . . . . . . . . . 10 ((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) → 𝐴𝑃)
2928ad4antr 730 . . . . . . . . 9 ((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) → 𝐴𝑃)
3029ad3antrrr 728 . . . . . . . 8 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝐴𝑃)
3118ad3antrrr 728 . . . . . . . . . 10 ((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) → 𝐵𝑃)
3231ad4antr 730 . . . . . . . . 9 ((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) → 𝐵𝑃)
3332ad3antrrr 728 . . . . . . . 8 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝐵𝑃)
341ad10antr 742 . . . . . . . 8 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝐶𝑃)
353ad10antr 742 . . . . . . . 8 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝐴𝑂𝐶)
36 simpr 485 . . . . . . . 8 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝑧𝐷)
37 simplr 767 . . . . . . . . . . . . . . 15 ((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) → 𝑦𝐷)
3811, 13, 12, 25, 23, 37tglnpt 27665 . . . . . . . . . . . . . 14 ((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) → 𝑦𝑃)
3938ad3antrrr 728 . . . . . . . . . . . . 13 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝑦𝑃)
40 simp-5r 784 . . . . . . . . . . . . . 14 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝑦𝐷)
4111, 22, 12, 14, 13, 24, 26, 30, 34, 35oppne1 27857 . . . . . . . . . . . . . 14 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → ¬ 𝐴𝐷)
42 nelne2 3039 . . . . . . . . . . . . . 14 ((𝑦𝐷 ∧ ¬ 𝐴𝐷) → 𝑦𝐴)
4340, 41, 42syl2anc 584 . . . . . . . . . . . . 13 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝑦𝐴)
4411, 12, 13, 26, 39, 30, 43tgelrnln 27746 . . . . . . . . . . . 12 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → (𝑦𝐿𝐴) ∈ ran 𝐿)
4511, 12, 13, 26, 39, 30, 43tglinerflx2 27750 . . . . . . . . . . . . . 14 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝐴 ∈ (𝑦𝐿𝐴))
46 nelne1 3038 . . . . . . . . . . . . . 14 ((𝐴 ∈ (𝑦𝐿𝐴) ∧ ¬ 𝐴𝐷) → (𝑦𝐿𝐴) ≠ 𝐷)
4745, 41, 46syl2anc 584 . . . . . . . . . . . . 13 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → (𝑦𝐿𝐴) ≠ 𝐷)
4847necomd 2995 . . . . . . . . . . . 12 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝐷 ≠ (𝑦𝐿𝐴))
49 simpllr 774 . . . . . . . . . . . . . 14 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝑧𝑃)
50 simplrr 776 . . . . . . . . . . . . . 14 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝑧 ∈ (𝑦𝐼𝐴))
5111, 12, 13, 26, 39, 30, 49, 43, 50btwnlng1 27735 . . . . . . . . . . . . 13 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝑧 ∈ (𝑦𝐿𝐴))
5236, 51elind 4190 . . . . . . . . . . . 12 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝑧 ∈ (𝐷 ∩ (𝑦𝐿𝐴)))
5311, 12, 13, 26, 39, 30, 43tglinerflx1 27749 . . . . . . . . . . . . 13 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝑦 ∈ (𝑦𝐿𝐴))
5440, 53elind 4190 . . . . . . . . . . . 12 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝑦 ∈ (𝐷 ∩ (𝑦𝐿𝐴)))
5511, 12, 13, 26, 24, 44, 48, 52, 54tglineineq 27759 . . . . . . . . . . 11 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝑧 = 𝑦)
5655, 43eqnetrd 3007 . . . . . . . . . 10 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝑧𝐴)
5756necomd 2995 . . . . . . . . 9 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝐴𝑧)
58 simp-4r 782 . . . . . . . . . . . . . . 15 ((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) → 𝑥𝐷)
5911, 13, 12, 25, 23, 58tglnpt 27665 . . . . . . . . . . . . . 14 ((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) → 𝑥𝑃)
6059ad3antrrr 728 . . . . . . . . . . . . 13 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝑥𝑃)
61 simp-7r 788 . . . . . . . . . . . . . 14 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝑥𝐷)
62 simplr 767 . . . . . . . . . . . . . . . . 17 ((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) → 𝑑𝑃)
6362ad4antr 730 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) → 𝑑𝑃)
6463ad3antrrr 728 . . . . . . . . . . . . . . 15 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝑑𝑃)
65 simprr 771 . . . . . . . . . . . . . . . 16 ((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) → 𝐵𝑂𝑑)
6665ad7antr 736 . . . . . . . . . . . . . . 15 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝐵𝑂𝑑)
6711, 22, 12, 14, 13, 24, 26, 33, 64, 66oppne1 27857 . . . . . . . . . . . . . 14 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → ¬ 𝐵𝐷)
68 nelne2 3039 . . . . . . . . . . . . . 14 ((𝑥𝐷 ∧ ¬ 𝐵𝐷) → 𝑥𝐵)
6961, 67, 68syl2anc 584 . . . . . . . . . . . . 13 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝑥𝐵)
7011, 12, 13, 26, 60, 33, 69tgelrnln 27746 . . . . . . . . . . . 12 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → (𝑥𝐿𝐵) ∈ ran 𝐿)
7111, 12, 13, 26, 60, 33, 69tglinerflx2 27750 . . . . . . . . . . . . . 14 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝐵 ∈ (𝑥𝐿𝐵))
72 nelne1 3038 . . . . . . . . . . . . . 14 ((𝐵 ∈ (𝑥𝐿𝐵) ∧ ¬ 𝐵𝐷) → (𝑥𝐿𝐵) ≠ 𝐷)
7371, 67, 72syl2anc 584 . . . . . . . . . . . . 13 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → (𝑥𝐿𝐵) ≠ 𝐷)
7473necomd 2995 . . . . . . . . . . . 12 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝐷 ≠ (𝑥𝐿𝐵))
75 simplrl 775 . . . . . . . . . . . . . 14 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝑧 ∈ (𝑥𝐼𝐵))
7611, 12, 13, 26, 60, 33, 49, 69, 75btwnlng1 27735 . . . . . . . . . . . . 13 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝑧 ∈ (𝑥𝐿𝐵))
7736, 76elind 4190 . . . . . . . . . . . 12 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝑧 ∈ (𝐷 ∩ (𝑥𝐿𝐵)))
7811, 12, 13, 26, 60, 33, 69tglinerflx1 27749 . . . . . . . . . . . . 13 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝑥 ∈ (𝑥𝐿𝐵))
7961, 78elind 4190 . . . . . . . . . . . 12 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝑥 ∈ (𝐷 ∩ (𝑥𝐿𝐵)))
8011, 12, 13, 26, 24, 70, 74, 77, 79tglineineq 27759 . . . . . . . . . . 11 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝑧 = 𝑥)
8180, 69eqnetrd 3007 . . . . . . . . . 10 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝑧𝐵)
8281necomd 2995 . . . . . . . . 9 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝐵𝑧)
83 simprl 769 . . . . . . . . . . . . . 14 ((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) → 𝐴𝑂𝑑)
8483ad7antr 736 . . . . . . . . . . . . 13 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝐴𝑂𝑑)
8511, 22, 12, 14, 13, 24, 26, 30, 64, 84oppne2 27858 . . . . . . . . . . . 12 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → ¬ 𝑑𝐷)
86 nelne2 3039 . . . . . . . . . . . 12 ((𝑧𝐷 ∧ ¬ 𝑑𝐷) → 𝑧𝑑)
8736, 85, 86syl2anc 584 . . . . . . . . . . 11 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝑧𝑑)
8887necomd 2995 . . . . . . . . . 10 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝑑𝑧)
89 simpllr 774 . . . . . . . . . . . . 13 ((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) → 𝑥 ∈ (𝐴𝐼𝑑))
9089ad3antrrr 728 . . . . . . . . . . . 12 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝑥 ∈ (𝐴𝐼𝑑))
9111, 22, 12, 26, 30, 60, 64, 90tgbtwncom 27604 . . . . . . . . . . 11 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝑥 ∈ (𝑑𝐼𝐴))
9280, 91eqeltrd 2832 . . . . . . . . . 10 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝑧 ∈ (𝑑𝐼𝐴))
93 simp-4r 782 . . . . . . . . . . . 12 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝑦 ∈ (𝐵𝐼𝑑))
9411, 22, 12, 26, 33, 39, 64, 93tgbtwncom 27604 . . . . . . . . . . 11 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝑦 ∈ (𝑑𝐼𝐵))
9555, 94eqeltrd 2832 . . . . . . . . . 10 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝑧 ∈ (𝑑𝐼𝐵))
9611, 12, 26, 64, 49, 30, 33, 88, 92, 95tgbtwnconn2 27692 . . . . . . . . 9 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → (𝐴 ∈ (𝑧𝐼𝐵) ∨ 𝐵 ∈ (𝑧𝐼𝐴)))
9711, 12, 27, 30, 33, 49, 26ishlg 27718 . . . . . . . . 9 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → (𝐴((hlG‘𝐺)‘𝑧)𝐵 ↔ (𝐴𝑧𝐵𝑧 ∧ (𝐴 ∈ (𝑧𝐼𝐵) ∨ 𝐵 ∈ (𝑧𝐼𝐴)))))
9857, 82, 96, 97mpbir3and 1342 . . . . . . . 8 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝐴((hlG‘𝐺)‘𝑧)𝐵)
9911, 22, 12, 14, 13, 24, 26, 27, 30, 33, 34, 35, 36, 98opphl 27870 . . . . . . 7 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧𝐷) → 𝐵𝑂𝐶)
10023ad3antrrr 728 . . . . . . . 8 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧𝐷) → 𝐷 ∈ ran 𝐿)
10125ad3antrrr 728 . . . . . . . 8 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧𝐷) → 𝐺 ∈ TarskiG)
102 simpllr 774 . . . . . . . 8 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧𝐷) → 𝑧𝑃)
10332ad3antrrr 728 . . . . . . . 8 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧𝐷) → 𝐵𝑃)
1041ad10antr 742 . . . . . . . 8 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧𝐷) → 𝐶𝑃)
10529ad3antrrr 728 . . . . . . . . 9 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧𝐷) → 𝐴𝑃)
1063ad10antr 742 . . . . . . . . 9 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧𝐷) → 𝐴𝑂𝐶)
107 simp-5r 784 . . . . . . . . 9 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧𝐷) → 𝑦𝐷)
10838ad3antrrr 728 . . . . . . . . . 10 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧𝐷) → 𝑦𝑃)
109 simplrr 776 . . . . . . . . . . 11 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧𝐷) → 𝑧 ∈ (𝑦𝐼𝐴))
110 simpr 485 . . . . . . . . . . . . . 14 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧𝐷) → ¬ 𝑧𝐷)
111 nelne2 3039 . . . . . . . . . . . . . 14 ((𝑦𝐷 ∧ ¬ 𝑧𝐷) → 𝑦𝑧)
112107, 110, 111syl2anc 584 . . . . . . . . . . . . 13 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧𝐷) → 𝑦𝑧)
113112necomd 2995 . . . . . . . . . . . 12 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧𝐷) → 𝑧𝑦)
11411, 22, 12, 101, 108, 102, 105, 109, 113tgbtwnne 27606 . . . . . . . . . . 11 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧𝐷) → 𝑦𝐴)
11511, 12, 27, 108, 105, 102, 101, 105, 109, 114, 113btwnhl1 27728 . . . . . . . . . 10 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧𝐷) → 𝑧((hlG‘𝐺)‘𝑦)𝐴)
11611, 12, 27, 102, 105, 108, 101, 115hlcomd 27720 . . . . . . . . 9 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧𝐷) → 𝐴((hlG‘𝐺)‘𝑦)𝑧)
11711, 22, 12, 14, 13, 100, 101, 27, 105, 102, 104, 106, 107, 116opphl 27870 . . . . . . . 8 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧𝐷) → 𝑧𝑂𝐶)
11858ad3antrrr 728 . . . . . . . 8 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧𝐷) → 𝑥𝐷)
11959ad3antrrr 728 . . . . . . . . 9 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧𝐷) → 𝑥𝑃)
120 simplrl 775 . . . . . . . . 9 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧𝐷) → 𝑧 ∈ (𝑥𝐼𝐵))
121 nelne2 3039 . . . . . . . . . . . 12 ((𝑥𝐷 ∧ ¬ 𝑧𝐷) → 𝑥𝑧)
122118, 110, 121syl2anc 584 . . . . . . . . . . 11 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧𝐷) → 𝑥𝑧)
123122necomd 2995 . . . . . . . . . 10 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧𝐷) → 𝑧𝑥)
12411, 22, 12, 101, 119, 102, 103, 120, 123tgbtwnne 27606 . . . . . . . . 9 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧𝐷) → 𝑥𝐵)
12511, 12, 27, 119, 103, 102, 101, 105, 120, 124, 123btwnhl1 27728 . . . . . . . 8 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧𝐷) → 𝑧((hlG‘𝐺)‘𝑥)𝐵)
12611, 22, 12, 14, 13, 100, 101, 27, 102, 103, 104, 117, 118, 125opphl 27870 . . . . . . 7 (((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧𝐷) → 𝐵𝑂𝐶)
12799, 126pm2.61dan 811 . . . . . 6 ((((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) → 𝐵𝑂𝐶)
128 simpr 485 . . . . . . 7 ((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) → 𝑦 ∈ (𝐵𝐼𝑑))
12911, 22, 12, 25, 29, 32, 63, 59, 38, 89, 128axtgpasch 27583 . . . . . 6 ((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) → ∃𝑧𝑃 (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴)))
130127, 129r19.29a 3161 . . . . 5 ((((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) → 𝐵𝑂𝐶)
13111, 22, 12, 14, 31, 62islnopp 27855 . . . . . . . . 9 ((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) → (𝐵𝑂𝑑 ↔ ((¬ 𝐵𝐷 ∧ ¬ 𝑑𝐷) ∧ ∃𝑡𝐷 𝑡 ∈ (𝐵𝐼𝑑))))
13265, 131mpbid 231 . . . . . . . 8 ((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) → ((¬ 𝐵𝐷 ∧ ¬ 𝑑𝐷) ∧ ∃𝑡𝐷 𝑡 ∈ (𝐵𝐼𝑑)))
133132simprd 496 . . . . . . 7 ((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) → ∃𝑡𝐷 𝑡 ∈ (𝐵𝐼𝑑))
134 eleq1w 2815 . . . . . . . 8 (𝑡 = 𝑦 → (𝑡 ∈ (𝐵𝐼𝑑) ↔ 𝑦 ∈ (𝐵𝐼𝑑)))
135134cbvrexvw 3234 . . . . . . 7 (∃𝑡𝐷 𝑡 ∈ (𝐵𝐼𝑑) ↔ ∃𝑦𝐷 𝑦 ∈ (𝐵𝐼𝑑))
136133, 135sylib 217 . . . . . 6 ((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) → ∃𝑦𝐷 𝑦 ∈ (𝐵𝐼𝑑))
137136ad2antrr 724 . . . . 5 ((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) → ∃𝑦𝐷 𝑦 ∈ (𝐵𝐼𝑑))
138130, 137r19.29a 3161 . . . 4 ((((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) ∧ 𝑥𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) → 𝐵𝑂𝐶)
13911, 22, 12, 14, 28, 62islnopp 27855 . . . . . . 7 ((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) → (𝐴𝑂𝑑 ↔ ((¬ 𝐴𝐷 ∧ ¬ 𝑑𝐷) ∧ ∃𝑡𝐷 𝑡 ∈ (𝐴𝐼𝑑))))
14083, 139mpbid 231 . . . . . 6 ((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) → ((¬ 𝐴𝐷 ∧ ¬ 𝑑𝐷) ∧ ∃𝑡𝐷 𝑡 ∈ (𝐴𝐼𝑑)))
141140simprd 496 . . . . 5 ((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) → ∃𝑡𝐷 𝑡 ∈ (𝐴𝐼𝑑))
142 eleq1w 2815 . . . . . 6 (𝑡 = 𝑥 → (𝑡 ∈ (𝐴𝐼𝑑) ↔ 𝑥 ∈ (𝐴𝐼𝑑)))
143142cbvrexvw 3234 . . . . 5 (∃𝑡𝐷 𝑡 ∈ (𝐴𝐼𝑑) ↔ ∃𝑥𝐷 𝑥 ∈ (𝐴𝐼𝑑))
144141, 143sylib 217 . . . 4 ((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) → ∃𝑥𝐷 𝑥 ∈ (𝐴𝐼𝑑))
145138, 144r19.29a 3161 . . 3 ((((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑𝑃) ∧ (𝐴𝑂𝑑𝐵𝑂𝑑)) → 𝐵𝑂𝐶)
14619biimpa 477 . . 3 ((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) → ∃𝑑𝑃 (𝐴𝑂𝑑𝐵𝑂𝑑))
147145, 146r19.29a 3161 . 2 ((𝜑𝐴((hpG‘𝐺)‘𝐷)𝐵) → 𝐵𝑂𝐶)
14821, 147impbida 799 1 (𝜑 → (𝐵𝑂𝐶𝐴((hpG‘𝐺)‘𝐷)𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845   = wceq 1541  wcel 2106  wne 2939  wrex 3069  cdif 3941   class class class wbr 5141  {copab 5203  ran crn 5670  cfv 6532  (class class class)co 7393  Basecbs 17126  distcds 17188  TarskiGcstrkg 27543  Itvcitv 27549  LineGclng 27550  hlGchlg 27716  hpGchpg 27873
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 2702  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7708  ax-cnex 11148  ax-resscn 11149  ax-1cn 11150  ax-icn 11151  ax-addcl 11152  ax-addrcl 11153  ax-mulcl 11154  ax-mulrcl 11155  ax-mulcom 11156  ax-addass 11157  ax-mulass 11158  ax-distr 11159  ax-i2m1 11160  ax-1ne0 11161  ax-1rid 11162  ax-rnegex 11163  ax-rrecex 11164  ax-cnre 11165  ax-pre-lttri 11166  ax-pre-lttrn 11167  ax-pre-ltadd 11168  ax-pre-mulgt0 11169
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 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4523  df-pw 4598  df-sn 4623  df-pr 4625  df-tp 4627  df-op 4629  df-uni 4902  df-int 4944  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6289  df-ord 6356  df-on 6357  df-lim 6358  df-suc 6359  df-iota 6484  df-fun 6534  df-fn 6535  df-f 6536  df-f1 6537  df-fo 6538  df-f1o 6539  df-fv 6540  df-riota 7349  df-ov 7396  df-oprab 7397  df-mpo 7398  df-om 7839  df-1st 7957  df-2nd 7958  df-frecs 8248  df-wrecs 8279  df-recs 8353  df-rdg 8392  df-1o 8448  df-oadd 8452  df-er 8686  df-map 8805  df-pm 8806  df-en 8923  df-dom 8924  df-sdom 8925  df-fin 8926  df-dju 9878  df-card 9916  df-pnf 11232  df-mnf 11233  df-xr 11234  df-ltxr 11235  df-le 11236  df-sub 11428  df-neg 11429  df-nn 12195  df-2 12257  df-3 12258  df-n0 12455  df-xnn0 12527  df-z 12541  df-uz 12805  df-fz 13467  df-fzo 13610  df-hash 14273  df-word 14447  df-concat 14503  df-s1 14528  df-s2 14781  df-s3 14782  df-trkgc 27564  df-trkgb 27565  df-trkgcb 27566  df-trkgld 27568  df-trkg 27569  df-cgrg 27627  df-leg 27699  df-hlg 27717  df-mir 27769  df-rag 27810  df-perpg 27812  df-hpg 27874
This theorem is referenced by:  lnoppnhpg  27880  hpgtr  27884  colhp  27886  lnperpex  27919  trgcopyeulem  27921
  Copyright terms: Public domain W3C validator