Metamath Proof Explorer

Theorem lnopp2hpgb

Description: Theorem 9.8 of Schwabhauser p. 71. (Contributed by Thierry Arnoux, 4-Mar-2020)

Ref Expression
Hypotheses 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 lnopp2hpgb ( 𝜑 → ( 𝐵 𝑂 𝐶 ↔ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ishpg.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 ishpg.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 ishpg.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
4 ishpg.o ⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
5 ishpg.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6 ishpg.d ⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 )
7 hpgbr.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
8 hpgbr.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
9 lnopp2hpgb.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
10 lnopp2hpgb.1 ⊢ ( 𝜑 → 𝐴 𝑂 𝐶 )
11 9 adantr ⊢ ( ( 𝜑 ∧ 𝐵 𝑂 𝐶 ) → 𝐶 ∈ 𝑃 )
12 10 adantr ⊢ ( ( 𝜑 ∧ 𝐵 𝑂 𝐶 ) → 𝐴 𝑂 𝐶 )
13 simpr ⊢ ( ( 𝜑 ∧ 𝐵 𝑂 𝐶 ) → 𝐵 𝑂 𝐶 )
14 breq2 ⊢ ( 𝑑 = 𝐶 → ( 𝐴 𝑂 𝑑 ↔ 𝐴 𝑂 𝐶 ) )
15 breq2 ⊢ ( 𝑑 = 𝐶 → ( 𝐵 𝑂 𝑑 ↔ 𝐵 𝑂 𝐶 ) )
16 14 15 anbi12d ⊢ ( 𝑑 = 𝐶 → ( ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ↔ ( 𝐴 𝑂 𝐶 ∧ 𝐵 𝑂 𝐶 ) ) )
17 16 rspcev ⊢ ( ( 𝐶 ∈ 𝑃 ∧ ( 𝐴 𝑂 𝐶 ∧ 𝐵 𝑂 𝐶 ) ) → ∃ 𝑑 ∈ 𝑃 ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) )
18 11 12 13 17 syl12anc ⊢ ( ( 𝜑 ∧ 𝐵 𝑂 𝐶 ) → ∃ 𝑑 ∈ 𝑃 ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) )
19 1 2 3 4 5 6 7 8 hpgbr ⊢ ( 𝜑 → ( 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ↔ ∃ 𝑑 ∈ 𝑃 ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝐵 𝑂 𝐶 ) → ( 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ↔ ∃ 𝑑 ∈ 𝑃 ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) )
21 18 20 mpbird ⊢ ( ( 𝜑 ∧ 𝐵 𝑂 𝐶 ) → 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 )
22 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
23 6 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) → 𝐷 ∈ ran 𝐿 )
24 23 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝐷 ∈ ran 𝐿 )
25 5 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) → 𝐺 ∈ TarskiG )
26 25 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝐺 ∈ TarskiG )
27 eqid ⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
28 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) → 𝐴 ∈ 𝑃 )
29 28 ad4antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) → 𝐴 ∈ 𝑃 )
30 29 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝐴 ∈ 𝑃 )
31 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) → 𝐵 ∈ 𝑃 )
32 31 ad4antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) → 𝐵 ∈ 𝑃 )
33 32 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝐵 ∈ 𝑃 )
34 9 ad10antr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝐶 ∈ 𝑃 )
35 10 ad10antr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝐴 𝑂 𝐶 )
36 simpr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝑧 ∈ 𝐷 )
37 simplr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) → 𝑦 ∈ 𝐷 )
38 1 3 2 25 23 37 tglnpt ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) → 𝑦 ∈ 𝑃 )
39 38 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝑦 ∈ 𝑃 )
40 simp-5r ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝑦 ∈ 𝐷 )
41 1 22 2 4 3 24 26 30 34 35 oppne1 ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → ¬ 𝐴 ∈ 𝐷 )
42 nelne2 ⊢ ( ( 𝑦 ∈ 𝐷 ∧ ¬ 𝐴 ∈ 𝐷 ) → 𝑦 ≠ 𝐴 )
43 40 41 42 syl2anc ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝑦 ≠ 𝐴 )
44 1 2 3 26 39 30 43 tgelrnln ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → ( 𝑦 𝐿 𝐴 ) ∈ ran 𝐿 )
45 1 2 3 26 39 30 43 tglinerflx2 ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝐴 ∈ ( 𝑦 𝐿 𝐴 ) )
46 nelne1 ⊢ ( ( 𝐴 ∈ ( 𝑦 𝐿 𝐴 ) ∧ ¬ 𝐴 ∈ 𝐷 ) → ( 𝑦 𝐿 𝐴 ) ≠ 𝐷 )
47 45 41 46 syl2anc ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → ( 𝑦 𝐿 𝐴 ) ≠ 𝐷 )
48 47 necomd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝐷 ≠ ( 𝑦 𝐿 𝐴 ) )
49 simpllr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝑧 ∈ 𝑃 )
50 simplrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) )
51 1 2 3 26 39 30 49 43 50 btwnlng1 ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝑧 ∈ ( 𝑦 𝐿 𝐴 ) )
52 36 51 elind ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝑧 ∈ ( 𝐷 ∩ ( 𝑦 𝐿 𝐴 ) ) )
53 1 2 3 26 39 30 43 tglinerflx1 ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝑦 ∈ ( 𝑦 𝐿 𝐴 ) )
54 40 53 elind ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝑦 ∈ ( 𝐷 ∩ ( 𝑦 𝐿 𝐴 ) ) )
55 1 2 3 26 24 44 48 52 54 tglineineq ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝑧 = 𝑦 )
56 55 43 eqnetrd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝑧 ≠ 𝐴 )
57 56 necomd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝐴 ≠ 𝑧 )
58 simp-4r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) → 𝑥 ∈ 𝐷 )
59 1 3 2 25 23 58 tglnpt ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) → 𝑥 ∈ 𝑃 )
60 59 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝑥 ∈ 𝑃 )
61 simp-7r ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝑥 ∈ 𝐷 )
62 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) → 𝑑 ∈ 𝑃 )
63 62 ad4antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) → 𝑑 ∈ 𝑃 )
64 63 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝑑 ∈ 𝑃 )
65 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) → 𝐵 𝑂 𝑑 )
66 65 ad7antr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝐵 𝑂 𝑑 )
67 1 22 2 4 3 24 26 33 64 66 oppne1 ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → ¬ 𝐵 ∈ 𝐷 )
68 nelne2 ⊢ ( ( 𝑥 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) → 𝑥 ≠ 𝐵 )
69 61 67 68 syl2anc ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝑥 ≠ 𝐵 )
70 1 2 3 26 60 33 69 tgelrnln ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → ( 𝑥 𝐿 𝐵 ) ∈ ran 𝐿 )
71 1 2 3 26 60 33 69 tglinerflx2 ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝐵 ∈ ( 𝑥 𝐿 𝐵 ) )
72 nelne1 ⊢ ( ( 𝐵 ∈ ( 𝑥 𝐿 𝐵 ) ∧ ¬ 𝐵 ∈ 𝐷 ) → ( 𝑥 𝐿 𝐵 ) ≠ 𝐷 )
73 71 67 72 syl2anc ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → ( 𝑥 𝐿 𝐵 ) ≠ 𝐷 )
74 73 necomd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝐷 ≠ ( 𝑥 𝐿 𝐵 ) )
75 simplrl ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) )
76 1 2 3 26 60 33 49 69 75 btwnlng1 ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝑧 ∈ ( 𝑥 𝐿 𝐵 ) )
77 36 76 elind ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝑧 ∈ ( 𝐷 ∩ ( 𝑥 𝐿 𝐵 ) ) )
78 1 2 3 26 60 33 69 tglinerflx1 ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝑥 ∈ ( 𝑥 𝐿 𝐵 ) )
79 61 78 elind ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝑥 ∈ ( 𝐷 ∩ ( 𝑥 𝐿 𝐵 ) ) )
80 1 2 3 26 24 70 74 77 79 tglineineq ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝑧 = 𝑥 )
81 80 69 eqnetrd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝑧 ≠ 𝐵 )
82 81 necomd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝐵 ≠ 𝑧 )
83 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) → 𝐴 𝑂 𝑑 )
84 83 ad7antr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝐴 𝑂 𝑑 )
85 1 22 2 4 3 24 26 30 64 84 oppne2 ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → ¬ 𝑑 ∈ 𝐷 )
86 nelne2 ⊢ ( ( 𝑧 ∈ 𝐷 ∧ ¬ 𝑑 ∈ 𝐷 ) → 𝑧 ≠ 𝑑 )
87 36 85 86 syl2anc ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝑧 ≠ 𝑑 )
88 87 necomd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝑑 ≠ 𝑧 )
89 simpllr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) → 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) )
90 89 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) )
91 1 22 2 26 30 60 64 90 tgbtwncom ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝑥 ∈ ( 𝑑 𝐼 𝐴 ) )
92 80 91 eqeltrd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝑧 ∈ ( 𝑑 𝐼 𝐴 ) )
93 simp-4r ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) )
94 1 22 2 26 33 39 64 93 tgbtwncom ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝑦 ∈ ( 𝑑 𝐼 𝐵 ) )
95 55 94 eqeltrd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝑧 ∈ ( 𝑑 𝐼 𝐵 ) )
96 1 2 26 64 49 30 33 88 92 95 tgbtwnconn2 ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → ( 𝐴 ∈ ( 𝑧 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝑧 𝐼 𝐴 ) ) )
97 1 2 27 30 33 49 26 ishlg ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → ( 𝐴 ( ( hlG ‘ 𝐺 ) ‘ 𝑧 ) 𝐵 ↔ ( 𝐴 ≠ 𝑧 ∧ 𝐵 ≠ 𝑧 ∧ ( 𝐴 ∈ ( 𝑧 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝑧 𝐼 𝐴 ) ) ) ) )
98 57 82 96 97 mpbir3and ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝐴 ( ( hlG ‘ 𝐺 ) ‘ 𝑧 ) 𝐵 )
99 1 22 2 4 3 24 26 27 30 33 34 35 36 98 opphl ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝐵 𝑂 𝐶 )
100 23 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ ¬ 𝑧 ∈ 𝐷 ) → 𝐷 ∈ ran 𝐿 )
101 25 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ ¬ 𝑧 ∈ 𝐷 ) → 𝐺 ∈ TarskiG )
102 simpllr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ ¬ 𝑧 ∈ 𝐷 ) → 𝑧 ∈ 𝑃 )
103 32 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ ¬ 𝑧 ∈ 𝐷 ) → 𝐵 ∈ 𝑃 )
104 9 ad10antr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ ¬ 𝑧 ∈ 𝐷 ) → 𝐶 ∈ 𝑃 )
105 29 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ ¬ 𝑧 ∈ 𝐷 ) → 𝐴 ∈ 𝑃 )
106 10 ad10antr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ ¬ 𝑧 ∈ 𝐷 ) → 𝐴 𝑂 𝐶 )
107 simp-5r ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ ¬ 𝑧 ∈ 𝐷 ) → 𝑦 ∈ 𝐷 )
108 38 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ ¬ 𝑧 ∈ 𝐷 ) → 𝑦 ∈ 𝑃 )
109 simplrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ ¬ 𝑧 ∈ 𝐷 ) → 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) )
110 simpr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ ¬ 𝑧 ∈ 𝐷 ) → ¬ 𝑧 ∈ 𝐷 )
111 nelne2 ⊢ ( ( 𝑦 ∈ 𝐷 ∧ ¬ 𝑧 ∈ 𝐷 ) → 𝑦 ≠ 𝑧 )
112 107 110 111 syl2anc ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ ¬ 𝑧 ∈ 𝐷 ) → 𝑦 ≠ 𝑧 )
113 112 necomd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ ¬ 𝑧 ∈ 𝐷 ) → 𝑧 ≠ 𝑦 )
114 1 22 2 101 108 102 105 109 113 tgbtwnne ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ ¬ 𝑧 ∈ 𝐷 ) → 𝑦 ≠ 𝐴 )
115 1 2 27 108 105 102 101 105 109 114 113 btwnhl1 ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ ¬ 𝑧 ∈ 𝐷 ) → 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑦 ) 𝐴 )
116 1 2 27 102 105 108 101 115 hlcomd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ ¬ 𝑧 ∈ 𝐷 ) → 𝐴 ( ( hlG ‘ 𝐺 ) ‘ 𝑦 ) 𝑧 )
117 1 22 2 4 3 100 101 27 105 102 104 106 107 116 opphl ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ ¬ 𝑧 ∈ 𝐷 ) → 𝑧 𝑂 𝐶 )
118 58 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ ¬ 𝑧 ∈ 𝐷 ) → 𝑥 ∈ 𝐷 )
119 59 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ ¬ 𝑧 ∈ 𝐷 ) → 𝑥 ∈ 𝑃 )
120 simplrl ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ ¬ 𝑧 ∈ 𝐷 ) → 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) )
121 nelne2 ⊢ ( ( 𝑥 ∈ 𝐷 ∧ ¬ 𝑧 ∈ 𝐷 ) → 𝑥 ≠ 𝑧 )
122 118 110 121 syl2anc ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ ¬ 𝑧 ∈ 𝐷 ) → 𝑥 ≠ 𝑧 )
123 122 necomd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ ¬ 𝑧 ∈ 𝐷 ) → 𝑧 ≠ 𝑥 )
124 1 22 2 101 119 102 103 120 123 tgbtwnne ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ ¬ 𝑧 ∈ 𝐷 ) → 𝑥 ≠ 𝐵 )
125 1 2 27 119 103 102 101 105 120 124 123 btwnhl1 ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ ¬ 𝑧 ∈ 𝐷 ) → 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑥 ) 𝐵 )
126 1 22 2 4 3 100 101 27 102 103 104 117 118 125 opphl ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) ∧ ¬ 𝑧 ∈ 𝐷 ) → 𝐵 𝑂 𝐶 )
127 99 126 pm2.61dan ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) ) → 𝐵 𝑂 𝐶 )
128 simpr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) → 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) )
129 1 22 2 25 29 32 63 59 38 89 128 axtgpasch ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) → ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝐵 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝐴 ) ) )
130 127 129 r19.29a ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) → 𝐵 𝑂 𝐶 )
131 1 22 2 4 31 62 islnopp ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) → ( 𝐵 𝑂 𝑑 ↔ ( ( ¬ 𝐵 ∈ 𝐷 ∧ ¬ 𝑑 ∈ 𝐷 ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐵 𝐼 𝑑 ) ) ) )
132 65 131 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) → ( ( ¬ 𝐵 ∈ 𝐷 ∧ ¬ 𝑑 ∈ 𝐷 ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐵 𝐼 𝑑 ) ) )
133 132 simprd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) → ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐵 𝐼 𝑑 ) )
134 eleq1w ⊢ ( 𝑡 = 𝑦 → ( 𝑡 ∈ ( 𝐵 𝐼 𝑑 ) ↔ 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) ) )
135 134 cbvrexvw ⊢ ( ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐵 𝐼 𝑑 ) ↔ ∃ 𝑦 ∈ 𝐷 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) )
136 133 135 sylib ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) → ∃ 𝑦 ∈ 𝐷 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) )
137 136 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) → ∃ 𝑦 ∈ 𝐷 𝑦 ∈ ( 𝐵 𝐼 𝑑 ) )
138 130 137 r19.29a ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) → 𝐵 𝑂 𝐶 )
139 1 22 2 4 28 62 islnopp ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) → ( 𝐴 𝑂 𝑑 ↔ ( ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝑑 ∈ 𝐷 ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝑑 ) ) ) )
140 83 139 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) → ( ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝑑 ∈ 𝐷 ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝑑 ) ) )
141 140 simprd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) → ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝑑 ) )
142 eleq1w ⊢ ( 𝑡 = 𝑥 → ( 𝑡 ∈ ( 𝐴 𝐼 𝑑 ) ↔ 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) ) )
143 142 cbvrexvw ⊢ ( ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝑑 ) ↔ ∃ 𝑥 ∈ 𝐷 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) )
144 141 143 sylib ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) → ∃ 𝑥 ∈ 𝐷 𝑥 ∈ ( 𝐴 𝐼 𝑑 ) )
145 138 144 r19.29a ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) ) → 𝐵 𝑂 𝐶 )
146 19 biimpa ⊢ ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) → ∃ 𝑑 ∈ 𝑃 ( 𝐴 𝑂 𝑑 ∧ 𝐵 𝑂 𝑑 ) )
147 145 146 r19.29a ⊢ ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) → 𝐵 𝑂 𝐶 )
148 21 147 impbida ⊢ ( 𝜑 → ( 𝐵 𝑂 𝐶 ↔ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) )