Metamath Proof Explorer

Theorem oppperpex

Description: Restating colperpex using the "opposite side of a line" relation. (Contributed by Thierry Arnoux, 2-Aug-2020)

Ref Expression
Hypotheses hpg.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
hpg.d ⊢ − = ( dist ‘ 𝐺 )
hpg.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
hpg.o ⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
opphl.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
opphl.d ⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 )
opphl.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
opphl.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
oppperpex.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
oppperpex.2 ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
oppperpex.3 ⊢ ( 𝜑 → ¬ 𝐶 ∈ 𝐷 )
oppperpex.4 ⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
Assertion oppperpex ( 𝜑 → ∃ 𝑝 ∈ 𝑃 ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) 𝐷 ∧ 𝐶 𝑂 𝑝 ) )

Proof

Step Hyp Ref Expression
1 hpg.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 hpg.d ⊢ − = ( dist ‘ 𝐺 )
3 hpg.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 hpg.o ⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
5 opphl.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
6 opphl.d ⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 )
7 opphl.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
8 opphl.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
9 oppperpex.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
10 oppperpex.2 ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
11 oppperpex.3 ⊢ ( 𝜑 → ¬ 𝐶 ∈ 𝐷 )
12 oppperpex.4 ⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
13 simprrl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) ∧ ( 𝑝 ∈ 𝑃 ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑥 ) ∧ ∃ 𝑡 ∈ 𝑃 ( ( 𝑡 ∈ ( 𝐴 𝐿 𝑥 ) ∨ 𝐴 = 𝑥 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) ) ) → ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑥 ) )
14 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) → 𝐺 ∈ TarskiG )
15 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) → 𝐷 ∈ ran 𝐿 )
16 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) → 𝐴 ∈ 𝐷 )
17 1 5 3 14 15 16 tglnpt ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) → 𝐴 ∈ 𝑃 )
18 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) → 𝑥 ∈ 𝐷 )
19 1 5 3 14 15 18 tglnpt ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) → 𝑥 ∈ 𝑃 )
20 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) → 𝐴 ≠ 𝑥 )
21 1 3 5 14 17 19 20 20 15 16 18 tglinethru ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) → 𝐷 = ( 𝐴 𝐿 𝑥 ) )
22 21 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) ∧ ( 𝑝 ∈ 𝑃 ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑥 ) ∧ ∃ 𝑡 ∈ 𝑃 ( ( 𝑡 ∈ ( 𝐴 𝐿 𝑥 ) ∨ 𝐴 = 𝑥 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) ) ) → 𝐷 = ( 𝐴 𝐿 𝑥 ) )
23 13 22 breqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) ∧ ( 𝑝 ∈ 𝑃 ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑥 ) ∧ ∃ 𝑡 ∈ 𝑃 ( ( 𝑡 ∈ ( 𝐴 𝐿 𝑥 ) ∨ 𝐴 = 𝑥 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) ) ) → ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) 𝐷 )
24 11 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) ∧ ( 𝑝 ∈ 𝑃 ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑥 ) ∧ ∃ 𝑡 ∈ 𝑃 ( ( 𝑡 ∈ ( 𝐴 𝐿 𝑥 ) ∨ 𝐴 = 𝑥 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) ) ) → ¬ 𝐶 ∈ 𝐷 )
25 14 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) ∧ ( 𝑝 ∈ 𝑃 ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑥 ) ∧ ∃ 𝑡 ∈ 𝑃 ( ( 𝑡 ∈ ( 𝐴 𝐿 𝑥 ) ∨ 𝐴 = 𝑥 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) ) ) → 𝐺 ∈ TarskiG )
26 15 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) ∧ ( 𝑝 ∈ 𝑃 ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑥 ) ∧ ∃ 𝑡 ∈ 𝑃 ( ( 𝑡 ∈ ( 𝐴 𝐿 𝑥 ) ∨ 𝐴 = 𝑥 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) ) ) → 𝐷 ∈ ran 𝐿 )
27 16 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) ∧ ( 𝑝 ∈ 𝑃 ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑥 ) ∧ ∃ 𝑡 ∈ 𝑃 ( ( 𝑡 ∈ ( 𝐴 𝐿 𝑥 ) ∨ 𝐴 = 𝑥 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) ) ) → 𝐴 ∈ 𝐷 )
28 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) ∧ ( 𝑝 ∈ 𝑃 ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑥 ) ∧ ∃ 𝑡 ∈ 𝑃 ( ( 𝑡 ∈ ( 𝐴 𝐿 𝑥 ) ∨ 𝐴 = 𝑥 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) ) ) → 𝑝 ∈ 𝑃 )
29 1 2 3 5 25 26 27 28 23 footne ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) ∧ ( 𝑝 ∈ 𝑃 ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑥 ) ∧ ∃ 𝑡 ∈ 𝑃 ( ( 𝑡 ∈ ( 𝐴 𝐿 𝑥 ) ∨ 𝐴 = 𝑥 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) ) ) → ¬ 𝑝 ∈ 𝐷 )
30 20 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑥 ) ) ∧ ( 𝑡 ∈ 𝑃 ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝑥 ) ∨ 𝐴 = 𝑥 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) ) → 𝐴 ≠ 𝑥 )
31 30 neneqd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑥 ) ) ∧ ( 𝑡 ∈ 𝑃 ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝑥 ) ∨ 𝐴 = 𝑥 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) ) → ¬ 𝐴 = 𝑥 )
32 simprrl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑥 ) ) ∧ ( 𝑡 ∈ 𝑃 ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝑥 ) ∨ 𝐴 = 𝑥 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) ) → ( 𝑡 ∈ ( 𝐴 𝐿 𝑥 ) ∨ 𝐴 = 𝑥 ) )
33 32 orcomd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑥 ) ) ∧ ( 𝑡 ∈ 𝑃 ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝑥 ) ∨ 𝐴 = 𝑥 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) ) → ( 𝐴 = 𝑥 ∨ 𝑡 ∈ ( 𝐴 𝐿 𝑥 ) ) )
34 33 ord ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑥 ) ) ∧ ( 𝑡 ∈ 𝑃 ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝑥 ) ∨ 𝐴 = 𝑥 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) ) → ( ¬ 𝐴 = 𝑥 → 𝑡 ∈ ( 𝐴 𝐿 𝑥 ) ) )
35 31 34 mpd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑥 ) ) ∧ ( 𝑡 ∈ 𝑃 ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝑥 ) ∨ 𝐴 = 𝑥 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) ) → 𝑡 ∈ ( 𝐴 𝐿 𝑥 ) )
36 21 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑥 ) ) ∧ ( 𝑡 ∈ 𝑃 ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝑥 ) ∨ 𝐴 = 𝑥 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) ) → 𝐷 = ( 𝐴 𝐿 𝑥 ) )
37 35 36 eleqtrrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑥 ) ) ∧ ( 𝑡 ∈ 𝑃 ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝑥 ) ∨ 𝐴 = 𝑥 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) ) → 𝑡 ∈ 𝐷 )
38 simprrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑥 ) ) ∧ ( 𝑡 ∈ 𝑃 ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝑥 ) ∨ 𝐴 = 𝑥 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) ) → 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) )
39 37 38 jca ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑥 ) ) ∧ ( 𝑡 ∈ 𝑃 ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝑥 ) ∨ 𝐴 = 𝑥 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) ) → ( 𝑡 ∈ 𝐷 ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) )
40 39 ex ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑥 ) ) → ( ( 𝑡 ∈ 𝑃 ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝑥 ) ∨ 𝐴 = 𝑥 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) → ( 𝑡 ∈ 𝐷 ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) )
41 40 reximdv2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑥 ) ) → ( ∃ 𝑡 ∈ 𝑃 ( ( 𝑡 ∈ ( 𝐴 𝐿 𝑥 ) ∨ 𝐴 = 𝑥 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) → ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) )
42 41 impr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑥 ) ∧ ∃ 𝑡 ∈ 𝑃 ( ( 𝑡 ∈ ( 𝐴 𝐿 𝑥 ) ∨ 𝐴 = 𝑥 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) ) → ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) )
43 42 anasss ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) ∧ ( 𝑝 ∈ 𝑃 ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑥 ) ∧ ∃ 𝑡 ∈ 𝑃 ( ( 𝑡 ∈ ( 𝐴 𝐿 𝑥 ) ∨ 𝐴 = 𝑥 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) ) ) → ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) )
44 24 29 43 jca31 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) ∧ ( 𝑝 ∈ 𝑃 ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑥 ) ∧ ∃ 𝑡 ∈ 𝑃 ( ( 𝑡 ∈ ( 𝐴 𝐿 𝑥 ) ∨ 𝐴 = 𝑥 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) ) ) → ( ( ¬ 𝐶 ∈ 𝐷 ∧ ¬ 𝑝 ∈ 𝐷 ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) )
45 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) → 𝐶 ∈ 𝑃 )
46 45 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑥 ) ) → 𝐶 ∈ 𝑃 )
47 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑥 ) ) → 𝑝 ∈ 𝑃 )
48 1 2 3 4 46 47 islnopp ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑥 ) ) → ( 𝐶 𝑂 𝑝 ↔ ( ( ¬ 𝐶 ∈ 𝐷 ∧ ¬ 𝑝 ∈ 𝐷 ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) )
49 48 adantrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑥 ) ∧ ∃ 𝑡 ∈ 𝑃 ( ( 𝑡 ∈ ( 𝐴 𝐿 𝑥 ) ∨ 𝐴 = 𝑥 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) ) → ( 𝐶 𝑂 𝑝 ↔ ( ( ¬ 𝐶 ∈ 𝐷 ∧ ¬ 𝑝 ∈ 𝐷 ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) )
50 49 anasss ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) ∧ ( 𝑝 ∈ 𝑃 ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑥 ) ∧ ∃ 𝑡 ∈ 𝑃 ( ( 𝑡 ∈ ( 𝐴 𝐿 𝑥 ) ∨ 𝐴 = 𝑥 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) ) ) → ( 𝐶 𝑂 𝑝 ↔ ( ( ¬ 𝐶 ∈ 𝐷 ∧ ¬ 𝑝 ∈ 𝐷 ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) )
51 44 50 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) ∧ ( 𝑝 ∈ 𝑃 ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑥 ) ∧ ∃ 𝑡 ∈ 𝑃 ( ( 𝑡 ∈ ( 𝐴 𝐿 𝑥 ) ∨ 𝐴 = 𝑥 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) ) ) → 𝐶 𝑂 𝑝 )
52 23 51 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) ∧ ( 𝑝 ∈ 𝑃 ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑥 ) ∧ ∃ 𝑡 ∈ 𝑃 ( ( 𝑡 ∈ ( 𝐴 𝐿 𝑥 ) ∨ 𝐴 = 𝑥 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) ) ) → ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) 𝐷 ∧ 𝐶 𝑂 𝑝 ) )
53 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) → 𝐺 DimTarskiG≥ 2 )
54 1 2 3 5 14 17 19 45 20 53 colperpex ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) → ∃ 𝑝 ∈ 𝑃 ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑥 ) ∧ ∃ 𝑡 ∈ 𝑃 ( ( 𝑡 ∈ ( 𝐴 𝐿 𝑥 ) ∨ 𝐴 = 𝑥 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) )
55 52 54 reximddv ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝐴 ≠ 𝑥 ) → ∃ 𝑝 ∈ 𝑃 ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) 𝐷 ∧ 𝐶 𝑂 𝑝 ) )
56 1 3 5 7 6 9 tglnpt2 ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐷 𝐴 ≠ 𝑥 )
57 55 56 r19.29a ⊢ ( 𝜑 → ∃ 𝑝 ∈ 𝑃 ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) 𝐷 ∧ 𝐶 𝑂 𝑝 ) )