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

Theorem islnopp 26531
Description: The property for two points 𝐴 and 𝐵 to lie on the opposite sides of a set 𝐷 Definition 9.1 of [Schwabhauser] p. 67. (Contributed by Thierry Arnoux, 19-Dec-2019.)
Hypotheses
Ref Expression
hpg.p 𝑃 = (Base‘𝐺)
hpg.d = (dist‘𝐺)
hpg.i 𝐼 = (Itv‘𝐺)
hpg.o 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃𝐷) ∧ 𝑏 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝑎𝐼𝑏))}
islnopp.a (𝜑𝐴𝑃)
islnopp.b (𝜑𝐵𝑃)
Assertion
Ref Expression
islnopp (𝜑 → (𝐴𝑂𝐵 ↔ ((¬ 𝐴𝐷 ∧ ¬ 𝐵𝐷) ∧ ∃𝑡𝐷 𝑡 ∈ (𝐴𝐼𝐵))))
Distinct variable groups:   𝐷,𝑎,𝑏   𝐼,𝑎,𝑏   𝑃,𝑎,𝑏   𝑡,𝐴   𝑡,𝐵   𝑡,𝑎,𝑏
Allowed substitution hints:   𝜑(𝑡,𝑎,𝑏)   𝐴(𝑎,𝑏)   𝐵(𝑎,𝑏)   𝐷(𝑡)   𝑃(𝑡)   𝐺(𝑡,𝑎,𝑏)   𝐼(𝑡)   (𝑡,𝑎,𝑏)   𝑂(𝑡,𝑎,𝑏)

Proof of Theorem islnopp
Dummy variables 𝑢 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 islnopp.a . . 3 (𝜑𝐴𝑃)
2 islnopp.b . . 3 (𝜑𝐵𝑃)
3 eleq1 2901 . . . . . 6 (𝑢 = 𝐴 → (𝑢 ∈ (𝑃𝐷) ↔ 𝐴 ∈ (𝑃𝐷)))
43anbi1d 632 . . . . 5 (𝑢 = 𝐴 → ((𝑢 ∈ (𝑃𝐷) ∧ 𝑣 ∈ (𝑃𝐷)) ↔ (𝐴 ∈ (𝑃𝐷) ∧ 𝑣 ∈ (𝑃𝐷))))
5 oveq1 7147 . . . . . . 7 (𝑢 = 𝐴 → (𝑢𝐼𝑣) = (𝐴𝐼𝑣))
65eleq2d 2899 . . . . . 6 (𝑢 = 𝐴 → (𝑡 ∈ (𝑢𝐼𝑣) ↔ 𝑡 ∈ (𝐴𝐼𝑣)))
76rexbidv 3283 . . . . 5 (𝑢 = 𝐴 → (∃𝑡𝐷 𝑡 ∈ (𝑢𝐼𝑣) ↔ ∃𝑡𝐷 𝑡 ∈ (𝐴𝐼𝑣)))
84, 7anbi12d 633 . . . 4 (𝑢 = 𝐴 → (((𝑢 ∈ (𝑃𝐷) ∧ 𝑣 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝑢𝐼𝑣)) ↔ ((𝐴 ∈ (𝑃𝐷) ∧ 𝑣 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝐴𝐼𝑣))))
9 eleq1 2901 . . . . . 6 (𝑣 = 𝐵 → (𝑣 ∈ (𝑃𝐷) ↔ 𝐵 ∈ (𝑃𝐷)))
109anbi2d 631 . . . . 5 (𝑣 = 𝐵 → ((𝐴 ∈ (𝑃𝐷) ∧ 𝑣 ∈ (𝑃𝐷)) ↔ (𝐴 ∈ (𝑃𝐷) ∧ 𝐵 ∈ (𝑃𝐷))))
11 oveq2 7148 . . . . . . 7 (𝑣 = 𝐵 → (𝐴𝐼𝑣) = (𝐴𝐼𝐵))
1211eleq2d 2899 . . . . . 6 (𝑣 = 𝐵 → (𝑡 ∈ (𝐴𝐼𝑣) ↔ 𝑡 ∈ (𝐴𝐼𝐵)))
1312rexbidv 3283 . . . . 5 (𝑣 = 𝐵 → (∃𝑡𝐷 𝑡 ∈ (𝐴𝐼𝑣) ↔ ∃𝑡𝐷 𝑡 ∈ (𝐴𝐼𝐵)))
1410, 13anbi12d 633 . . . 4 (𝑣 = 𝐵 → (((𝐴 ∈ (𝑃𝐷) ∧ 𝑣 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝐴𝐼𝑣)) ↔ ((𝐴 ∈ (𝑃𝐷) ∧ 𝐵 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝐴𝐼𝐵))))
15 hpg.o . . . . 5 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃𝐷) ∧ 𝑏 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝑎𝐼𝑏))}
16 simpl 486 . . . . . . . . 9 ((𝑎 = 𝑢𝑏 = 𝑣) → 𝑎 = 𝑢)
1716eleq1d 2898 . . . . . . . 8 ((𝑎 = 𝑢𝑏 = 𝑣) → (𝑎 ∈ (𝑃𝐷) ↔ 𝑢 ∈ (𝑃𝐷)))
18 simpr 488 . . . . . . . . 9 ((𝑎 = 𝑢𝑏 = 𝑣) → 𝑏 = 𝑣)
1918eleq1d 2898 . . . . . . . 8 ((𝑎 = 𝑢𝑏 = 𝑣) → (𝑏 ∈ (𝑃𝐷) ↔ 𝑣 ∈ (𝑃𝐷)))
2017, 19anbi12d 633 . . . . . . 7 ((𝑎 = 𝑢𝑏 = 𝑣) → ((𝑎 ∈ (𝑃𝐷) ∧ 𝑏 ∈ (𝑃𝐷)) ↔ (𝑢 ∈ (𝑃𝐷) ∧ 𝑣 ∈ (𝑃𝐷))))
21 oveq12 7149 . . . . . . . . 9 ((𝑎 = 𝑢𝑏 = 𝑣) → (𝑎𝐼𝑏) = (𝑢𝐼𝑣))
2221eleq2d 2899 . . . . . . . 8 ((𝑎 = 𝑢𝑏 = 𝑣) → (𝑡 ∈ (𝑎𝐼𝑏) ↔ 𝑡 ∈ (𝑢𝐼𝑣)))
2322rexbidv 3283 . . . . . . 7 ((𝑎 = 𝑢𝑏 = 𝑣) → (∃𝑡𝐷 𝑡 ∈ (𝑎𝐼𝑏) ↔ ∃𝑡𝐷 𝑡 ∈ (𝑢𝐼𝑣)))
2420, 23anbi12d 633 . . . . . 6 ((𝑎 = 𝑢𝑏 = 𝑣) → (((𝑎 ∈ (𝑃𝐷) ∧ 𝑏 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝑎𝐼𝑏)) ↔ ((𝑢 ∈ (𝑃𝐷) ∧ 𝑣 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝑢𝐼𝑣))))
2524cbvopabv 5114 . . . . 5 {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃𝐷) ∧ 𝑏 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝑎𝐼𝑏))} = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ (𝑃𝐷) ∧ 𝑣 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝑢𝐼𝑣))}
2615, 25eqtri 2845 . . . 4 𝑂 = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ (𝑃𝐷) ∧ 𝑣 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝑢𝐼𝑣))}
278, 14, 26brabg 5403 . . 3 ((𝐴𝑃𝐵𝑃) → (𝐴𝑂𝐵 ↔ ((𝐴 ∈ (𝑃𝐷) ∧ 𝐵 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝐴𝐼𝐵))))
281, 2, 27syl2anc 587 . 2 (𝜑 → (𝐴𝑂𝐵 ↔ ((𝐴 ∈ (𝑃𝐷) ∧ 𝐵 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝐴𝐼𝐵))))
291biantrurd 536 . . . . 5 (𝜑 → (¬ 𝐴𝐷 ↔ (𝐴𝑃 ∧ ¬ 𝐴𝐷)))
30 eldif 3918 . . . . 5 (𝐴 ∈ (𝑃𝐷) ↔ (𝐴𝑃 ∧ ¬ 𝐴𝐷))
3129, 30syl6bbr 292 . . . 4 (𝜑 → (¬ 𝐴𝐷𝐴 ∈ (𝑃𝐷)))
322biantrurd 536 . . . . 5 (𝜑 → (¬ 𝐵𝐷 ↔ (𝐵𝑃 ∧ ¬ 𝐵𝐷)))
33 eldif 3918 . . . . 5 (𝐵 ∈ (𝑃𝐷) ↔ (𝐵𝑃 ∧ ¬ 𝐵𝐷))
3432, 33syl6bbr 292 . . . 4 (𝜑 → (¬ 𝐵𝐷𝐵 ∈ (𝑃𝐷)))
3531, 34anbi12d 633 . . 3 (𝜑 → ((¬ 𝐴𝐷 ∧ ¬ 𝐵𝐷) ↔ (𝐴 ∈ (𝑃𝐷) ∧ 𝐵 ∈ (𝑃𝐷))))
3635anbi1d 632 . 2 (𝜑 → (((¬ 𝐴𝐷 ∧ ¬ 𝐵𝐷) ∧ ∃𝑡𝐷 𝑡 ∈ (𝐴𝐼𝐵)) ↔ ((𝐴 ∈ (𝑃𝐷) ∧ 𝐵 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝐴𝐼𝐵))))
3728, 36bitr4d 285 1 (𝜑 → (𝐴𝑂𝐵 ↔ ((¬ 𝐴𝐷 ∧ ¬ 𝐵𝐷) ∧ ∃𝑡𝐷 𝑡 ∈ (𝐴𝐼𝐵))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399   = wceq 1538  wcel 2114  wrex 3131  cdif 3905   class class class wbr 5042  {copab 5104  cfv 6334  (class class class)co 7140  Basecbs 16474  distcds 16565  Itvcitv 26228
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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179  ax-nul 5186  ax-pr 5307
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-rex 3136  df-v 3471  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4266  df-if 4440  df-sn 4540  df-pr 4542  df-op 4546  df-uni 4814  df-br 5043  df-opab 5105  df-iota 6293  df-fv 6342  df-ov 7143
This theorem is referenced by:  islnoppd  26532  oppne1  26533  oppne2  26534  oppne3  26535  oppcom  26536  oppnid  26538  opphllem1  26539  opphllem3  26541  opphllem5  26543  opphllem6  26544  oppperpex  26545  outpasch  26547  lnopp2hpgb  26555  hpgerlem  26557  colopp  26561  colhp  26562  trgcopyeulem  26597
  Copyright terms: Public domain W3C validator