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

Theorem islnopp 26453
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 2900 . . . . . 6 (𝑢 = 𝐴 → (𝑢 ∈ (𝑃𝐷) ↔ 𝐴 ∈ (𝑃𝐷)))
43anbi1d 629 . . . . 5 (𝑢 = 𝐴 → ((𝑢 ∈ (𝑃𝐷) ∧ 𝑣 ∈ (𝑃𝐷)) ↔ (𝐴 ∈ (𝑃𝐷) ∧ 𝑣 ∈ (𝑃𝐷))))
5 oveq1 7152 . . . . . . 7 (𝑢 = 𝐴 → (𝑢𝐼𝑣) = (𝐴𝐼𝑣))
65eleq2d 2898 . . . . . 6 (𝑢 = 𝐴 → (𝑡 ∈ (𝑢𝐼𝑣) ↔ 𝑡 ∈ (𝐴𝐼𝑣)))
76rexbidv 3297 . . . . 5 (𝑢 = 𝐴 → (∃𝑡𝐷 𝑡 ∈ (𝑢𝐼𝑣) ↔ ∃𝑡𝐷 𝑡 ∈ (𝐴𝐼𝑣)))
84, 7anbi12d 630 . . . 4 (𝑢 = 𝐴 → (((𝑢 ∈ (𝑃𝐷) ∧ 𝑣 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝑢𝐼𝑣)) ↔ ((𝐴 ∈ (𝑃𝐷) ∧ 𝑣 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝐴𝐼𝑣))))
9 eleq1 2900 . . . . . 6 (𝑣 = 𝐵 → (𝑣 ∈ (𝑃𝐷) ↔ 𝐵 ∈ (𝑃𝐷)))
109anbi2d 628 . . . . 5 (𝑣 = 𝐵 → ((𝐴 ∈ (𝑃𝐷) ∧ 𝑣 ∈ (𝑃𝐷)) ↔ (𝐴 ∈ (𝑃𝐷) ∧ 𝐵 ∈ (𝑃𝐷))))
11 oveq2 7153 . . . . . . 7 (𝑣 = 𝐵 → (𝐴𝐼𝑣) = (𝐴𝐼𝐵))
1211eleq2d 2898 . . . . . 6 (𝑣 = 𝐵 → (𝑡 ∈ (𝐴𝐼𝑣) ↔ 𝑡 ∈ (𝐴𝐼𝐵)))
1312rexbidv 3297 . . . . 5 (𝑣 = 𝐵 → (∃𝑡𝐷 𝑡 ∈ (𝐴𝐼𝑣) ↔ ∃𝑡𝐷 𝑡 ∈ (𝐴𝐼𝐵)))
1410, 13anbi12d 630 . . . 4 (𝑣 = 𝐵 → (((𝐴 ∈ (𝑃𝐷) ∧ 𝑣 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝐴𝐼𝑣)) ↔ ((𝐴 ∈ (𝑃𝐷) ∧ 𝐵 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝐴𝐼𝐵))))
15 hpg.o . . . . 5 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃𝐷) ∧ 𝑏 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝑎𝐼𝑏))}
16 simpl 483 . . . . . . . . 9 ((𝑎 = 𝑢𝑏 = 𝑣) → 𝑎 = 𝑢)
1716eleq1d 2897 . . . . . . . 8 ((𝑎 = 𝑢𝑏 = 𝑣) → (𝑎 ∈ (𝑃𝐷) ↔ 𝑢 ∈ (𝑃𝐷)))
18 simpr 485 . . . . . . . . 9 ((𝑎 = 𝑢𝑏 = 𝑣) → 𝑏 = 𝑣)
1918eleq1d 2897 . . . . . . . 8 ((𝑎 = 𝑢𝑏 = 𝑣) → (𝑏 ∈ (𝑃𝐷) ↔ 𝑣 ∈ (𝑃𝐷)))
2017, 19anbi12d 630 . . . . . . 7 ((𝑎 = 𝑢𝑏 = 𝑣) → ((𝑎 ∈ (𝑃𝐷) ∧ 𝑏 ∈ (𝑃𝐷)) ↔ (𝑢 ∈ (𝑃𝐷) ∧ 𝑣 ∈ (𝑃𝐷))))
21 oveq12 7154 . . . . . . . . 9 ((𝑎 = 𝑢𝑏 = 𝑣) → (𝑎𝐼𝑏) = (𝑢𝐼𝑣))
2221eleq2d 2898 . . . . . . . 8 ((𝑎 = 𝑢𝑏 = 𝑣) → (𝑡 ∈ (𝑎𝐼𝑏) ↔ 𝑡 ∈ (𝑢𝐼𝑣)))
2322rexbidv 3297 . . . . . . 7 ((𝑎 = 𝑢𝑏 = 𝑣) → (∃𝑡𝐷 𝑡 ∈ (𝑎𝐼𝑏) ↔ ∃𝑡𝐷 𝑡 ∈ (𝑢𝐼𝑣)))
2420, 23anbi12d 630 . . . . . 6 ((𝑎 = 𝑢𝑏 = 𝑣) → (((𝑎 ∈ (𝑃𝐷) ∧ 𝑏 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝑎𝐼𝑏)) ↔ ((𝑢 ∈ (𝑃𝐷) ∧ 𝑣 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝑢𝐼𝑣))))
2524cbvopabv 5130 . . . . 5 {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃𝐷) ∧ 𝑏 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝑎𝐼𝑏))} = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ (𝑃𝐷) ∧ 𝑣 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝑢𝐼𝑣))}
2615, 25eqtri 2844 . . . 4 𝑂 = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ (𝑃𝐷) ∧ 𝑣 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝑢𝐼𝑣))}
278, 14, 26brabg 5418 . . 3 ((𝐴𝑃𝐵𝑃) → (𝐴𝑂𝐵 ↔ ((𝐴 ∈ (𝑃𝐷) ∧ 𝐵 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝐴𝐼𝐵))))
281, 2, 27syl2anc 584 . 2 (𝜑 → (𝐴𝑂𝐵 ↔ ((𝐴 ∈ (𝑃𝐷) ∧ 𝐵 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝐴𝐼𝐵))))
291biantrurd 533 . . . . 5 (𝜑 → (¬ 𝐴𝐷 ↔ (𝐴𝑃 ∧ ¬ 𝐴𝐷)))
30 eldif 3945 . . . . 5 (𝐴 ∈ (𝑃𝐷) ↔ (𝐴𝑃 ∧ ¬ 𝐴𝐷))
3129, 30syl6bbr 290 . . . 4 (𝜑 → (¬ 𝐴𝐷𝐴 ∈ (𝑃𝐷)))
322biantrurd 533 . . . . 5 (𝜑 → (¬ 𝐵𝐷 ↔ (𝐵𝑃 ∧ ¬ 𝐵𝐷)))
33 eldif 3945 . . . . 5 (𝐵 ∈ (𝑃𝐷) ↔ (𝐵𝑃 ∧ ¬ 𝐵𝐷))
3432, 33syl6bbr 290 . . . 4 (𝜑 → (¬ 𝐵𝐷𝐵 ∈ (𝑃𝐷)))
3531, 34anbi12d 630 . . 3 (𝜑 → ((¬ 𝐴𝐷 ∧ ¬ 𝐵𝐷) ↔ (𝐴 ∈ (𝑃𝐷) ∧ 𝐵 ∈ (𝑃𝐷))))
3635anbi1d 629 . 2 (𝜑 → (((¬ 𝐴𝐷 ∧ ¬ 𝐵𝐷) ∧ ∃𝑡𝐷 𝑡 ∈ (𝐴𝐼𝐵)) ↔ ((𝐴 ∈ (𝑃𝐷) ∧ 𝐵 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝐴𝐼𝐵))))
3728, 36bitr4d 283 1 (𝜑 → (𝐴𝑂𝐵 ↔ ((¬ 𝐴𝐷 ∧ ¬ 𝐵𝐷) ∧ ∃𝑡𝐷 𝑡 ∈ (𝐴𝐼𝐵))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396   = wceq 1528  wcel 2105  wrex 3139  cdif 3932   class class class wbr 5058  {copab 5120  cfv 6349  (class class class)co 7145  Basecbs 16473  distcds 16564  Itvcitv 26150
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pr 5321
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rex 3144  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-opab 5121  df-iota 6308  df-fv 6357  df-ov 7148
This theorem is referenced by:  islnoppd  26454  oppne1  26455  oppne2  26456  oppne3  26457  oppcom  26458  oppnid  26460  opphllem1  26461  opphllem3  26463  opphllem5  26465  opphllem6  26466  oppperpex  26467  outpasch  26469  lnopp2hpgb  26477  hpgerlem  26479  colopp  26483  colhp  26484  trgcopyeulem  26519
  Copyright terms: Public domain W3C validator