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

Theorem islnopp 28663
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 2814 . . . . . 6 (𝑢 = 𝐴 → (𝑢 ∈ (𝑃𝐷) ↔ 𝐴 ∈ (𝑃𝐷)))
43anbi1d 629 . . . . 5 (𝑢 = 𝐴 → ((𝑢 ∈ (𝑃𝐷) ∧ 𝑣 ∈ (𝑃𝐷)) ↔ (𝐴 ∈ (𝑃𝐷) ∧ 𝑣 ∈ (𝑃𝐷))))
5 oveq1 7423 . . . . . . 7 (𝑢 = 𝐴 → (𝑢𝐼𝑣) = (𝐴𝐼𝑣))
65eleq2d 2812 . . . . . 6 (𝑢 = 𝐴 → (𝑡 ∈ (𝑢𝐼𝑣) ↔ 𝑡 ∈ (𝐴𝐼𝑣)))
76rexbidv 3169 . . . . 5 (𝑢 = 𝐴 → (∃𝑡𝐷 𝑡 ∈ (𝑢𝐼𝑣) ↔ ∃𝑡𝐷 𝑡 ∈ (𝐴𝐼𝑣)))
84, 7anbi12d 630 . . . 4 (𝑢 = 𝐴 → (((𝑢 ∈ (𝑃𝐷) ∧ 𝑣 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝑢𝐼𝑣)) ↔ ((𝐴 ∈ (𝑃𝐷) ∧ 𝑣 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝐴𝐼𝑣))))
9 eleq1 2814 . . . . . 6 (𝑣 = 𝐵 → (𝑣 ∈ (𝑃𝐷) ↔ 𝐵 ∈ (𝑃𝐷)))
109anbi2d 628 . . . . 5 (𝑣 = 𝐵 → ((𝐴 ∈ (𝑃𝐷) ∧ 𝑣 ∈ (𝑃𝐷)) ↔ (𝐴 ∈ (𝑃𝐷) ∧ 𝐵 ∈ (𝑃𝐷))))
11 oveq2 7424 . . . . . . 7 (𝑣 = 𝐵 → (𝐴𝐼𝑣) = (𝐴𝐼𝐵))
1211eleq2d 2812 . . . . . 6 (𝑣 = 𝐵 → (𝑡 ∈ (𝐴𝐼𝑣) ↔ 𝑡 ∈ (𝐴𝐼𝐵)))
1312rexbidv 3169 . . . . 5 (𝑣 = 𝐵 → (∃𝑡𝐷 𝑡 ∈ (𝐴𝐼𝑣) ↔ ∃𝑡𝐷 𝑡 ∈ (𝐴𝐼𝐵)))
1410, 13anbi12d 630 . . . 4 (𝑣 = 𝐵 → (((𝐴 ∈ (𝑃𝐷) ∧ 𝑣 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝐴𝐼𝑣)) ↔ ((𝐴 ∈ (𝑃𝐷) ∧ 𝐵 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝐴𝐼𝐵))))
15 hpg.o . . . . 5 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃𝐷) ∧ 𝑏 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝑎𝐼𝑏))}
16 simpl 481 . . . . . . . . 9 ((𝑎 = 𝑢𝑏 = 𝑣) → 𝑎 = 𝑢)
1716eleq1d 2811 . . . . . . . 8 ((𝑎 = 𝑢𝑏 = 𝑣) → (𝑎 ∈ (𝑃𝐷) ↔ 𝑢 ∈ (𝑃𝐷)))
18 simpr 483 . . . . . . . . 9 ((𝑎 = 𝑢𝑏 = 𝑣) → 𝑏 = 𝑣)
1918eleq1d 2811 . . . . . . . 8 ((𝑎 = 𝑢𝑏 = 𝑣) → (𝑏 ∈ (𝑃𝐷) ↔ 𝑣 ∈ (𝑃𝐷)))
2017, 19anbi12d 630 . . . . . . 7 ((𝑎 = 𝑢𝑏 = 𝑣) → ((𝑎 ∈ (𝑃𝐷) ∧ 𝑏 ∈ (𝑃𝐷)) ↔ (𝑢 ∈ (𝑃𝐷) ∧ 𝑣 ∈ (𝑃𝐷))))
21 oveq12 7425 . . . . . . . . 9 ((𝑎 = 𝑢𝑏 = 𝑣) → (𝑎𝐼𝑏) = (𝑢𝐼𝑣))
2221eleq2d 2812 . . . . . . . 8 ((𝑎 = 𝑢𝑏 = 𝑣) → (𝑡 ∈ (𝑎𝐼𝑏) ↔ 𝑡 ∈ (𝑢𝐼𝑣)))
2322rexbidv 3169 . . . . . . 7 ((𝑎 = 𝑢𝑏 = 𝑣) → (∃𝑡𝐷 𝑡 ∈ (𝑎𝐼𝑏) ↔ ∃𝑡𝐷 𝑡 ∈ (𝑢𝐼𝑣)))
2420, 23anbi12d 630 . . . . . 6 ((𝑎 = 𝑢𝑏 = 𝑣) → (((𝑎 ∈ (𝑃𝐷) ∧ 𝑏 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝑎𝐼𝑏)) ↔ ((𝑢 ∈ (𝑃𝐷) ∧ 𝑣 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝑢𝐼𝑣))))
2524cbvopabv 5218 . . . . 5 {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃𝐷) ∧ 𝑏 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝑎𝐼𝑏))} = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ (𝑃𝐷) ∧ 𝑣 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝑢𝐼𝑣))}
2615, 25eqtri 2754 . . . 4 𝑂 = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ (𝑃𝐷) ∧ 𝑣 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝑢𝐼𝑣))}
278, 14, 26brabg 5537 . . 3 ((𝐴𝑃𝐵𝑃) → (𝐴𝑂𝐵 ↔ ((𝐴 ∈ (𝑃𝐷) ∧ 𝐵 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝐴𝐼𝐵))))
281, 2, 27syl2anc 582 . 2 (𝜑 → (𝐴𝑂𝐵 ↔ ((𝐴 ∈ (𝑃𝐷) ∧ 𝐵 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝐴𝐼𝐵))))
291biantrurd 531 . . . . 5 (𝜑 → (¬ 𝐴𝐷 ↔ (𝐴𝑃 ∧ ¬ 𝐴𝐷)))
30 eldif 3956 . . . . 5 (𝐴 ∈ (𝑃𝐷) ↔ (𝐴𝑃 ∧ ¬ 𝐴𝐷))
3129, 30bitr4di 288 . . . 4 (𝜑 → (¬ 𝐴𝐷𝐴 ∈ (𝑃𝐷)))
322biantrurd 531 . . . . 5 (𝜑 → (¬ 𝐵𝐷 ↔ (𝐵𝑃 ∧ ¬ 𝐵𝐷)))
33 eldif 3956 . . . . 5 (𝐵 ∈ (𝑃𝐷) ↔ (𝐵𝑃 ∧ ¬ 𝐵𝐷))
3432, 33bitr4di 288 . . . 4 (𝜑 → (¬ 𝐵𝐷𝐵 ∈ (𝑃𝐷)))
3531, 34anbi12d 630 . . 3 (𝜑 → ((¬ 𝐴𝐷 ∧ ¬ 𝐵𝐷) ↔ (𝐴 ∈ (𝑃𝐷) ∧ 𝐵 ∈ (𝑃𝐷))))
3635anbi1d 629 . 2 (𝜑 → (((¬ 𝐴𝐷 ∧ ¬ 𝐵𝐷) ∧ ∃𝑡𝐷 𝑡 ∈ (𝐴𝐼𝐵)) ↔ ((𝐴 ∈ (𝑃𝐷) ∧ 𝐵 ∈ (𝑃𝐷)) ∧ ∃𝑡𝐷 𝑡 ∈ (𝐴𝐼𝐵))))
3728, 36bitr4d 281 1 (𝜑 → (𝐴𝑂𝐵 ↔ ((¬ 𝐴𝐷 ∧ ¬ 𝐵𝐷) ∧ ∃𝑡𝐷 𝑡 ∈ (𝐴𝐼𝐵))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394   = wceq 1534  wcel 2099  wrex 3060  cdif 3943   class class class wbr 5145  {copab 5207  cfv 6546  (class class class)co 7416  Basecbs 17208  distcds 17270  Itvcitv 28357
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-sep 5296  ax-nul 5303  ax-pr 5425
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rex 3061  df-rab 3420  df-v 3464  df-dif 3949  df-un 3951  df-ss 3963  df-nul 4323  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4906  df-br 5146  df-opab 5208  df-iota 6498  df-fv 6554  df-ov 7419
This theorem is referenced by:  islnoppd  28664  oppne1  28665  oppne2  28666  oppne3  28667  oppcom  28668  oppnid  28670  opphllem1  28671  opphllem3  28673  opphllem5  28675  opphllem6  28676  oppperpex  28677  outpasch  28679  lnopp2hpgb  28687  hpgerlem  28689  colopp  28693  colhp  28694  trgcopyeulem  28729
  Copyright terms: Public domain W3C validator