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

Theorem islnopp 28257
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 2819 . . . . . 6 (𝑒 = 𝐴 β†’ (𝑒 ∈ (𝑃 βˆ– 𝐷) ↔ 𝐴 ∈ (𝑃 βˆ– 𝐷)))
43anbi1d 628 . . . . 5 (𝑒 = 𝐴 β†’ ((𝑒 ∈ (𝑃 βˆ– 𝐷) ∧ 𝑣 ∈ (𝑃 βˆ– 𝐷)) ↔ (𝐴 ∈ (𝑃 βˆ– 𝐷) ∧ 𝑣 ∈ (𝑃 βˆ– 𝐷))))
5 oveq1 7418 . . . . . . 7 (𝑒 = 𝐴 β†’ (𝑒𝐼𝑣) = (𝐴𝐼𝑣))
65eleq2d 2817 . . . . . 6 (𝑒 = 𝐴 β†’ (𝑑 ∈ (𝑒𝐼𝑣) ↔ 𝑑 ∈ (𝐴𝐼𝑣)))
76rexbidv 3176 . . . . 5 (𝑒 = 𝐴 β†’ (βˆƒπ‘‘ ∈ 𝐷 𝑑 ∈ (𝑒𝐼𝑣) ↔ βˆƒπ‘‘ ∈ 𝐷 𝑑 ∈ (𝐴𝐼𝑣)))
84, 7anbi12d 629 . . . 4 (𝑒 = 𝐴 β†’ (((𝑒 ∈ (𝑃 βˆ– 𝐷) ∧ 𝑣 ∈ (𝑃 βˆ– 𝐷)) ∧ βˆƒπ‘‘ ∈ 𝐷 𝑑 ∈ (𝑒𝐼𝑣)) ↔ ((𝐴 ∈ (𝑃 βˆ– 𝐷) ∧ 𝑣 ∈ (𝑃 βˆ– 𝐷)) ∧ βˆƒπ‘‘ ∈ 𝐷 𝑑 ∈ (𝐴𝐼𝑣))))
9 eleq1 2819 . . . . . 6 (𝑣 = 𝐡 β†’ (𝑣 ∈ (𝑃 βˆ– 𝐷) ↔ 𝐡 ∈ (𝑃 βˆ– 𝐷)))
109anbi2d 627 . . . . 5 (𝑣 = 𝐡 β†’ ((𝐴 ∈ (𝑃 βˆ– 𝐷) ∧ 𝑣 ∈ (𝑃 βˆ– 𝐷)) ↔ (𝐴 ∈ (𝑃 βˆ– 𝐷) ∧ 𝐡 ∈ (𝑃 βˆ– 𝐷))))
11 oveq2 7419 . . . . . . 7 (𝑣 = 𝐡 β†’ (𝐴𝐼𝑣) = (𝐴𝐼𝐡))
1211eleq2d 2817 . . . . . 6 (𝑣 = 𝐡 β†’ (𝑑 ∈ (𝐴𝐼𝑣) ↔ 𝑑 ∈ (𝐴𝐼𝐡)))
1312rexbidv 3176 . . . . 5 (𝑣 = 𝐡 β†’ (βˆƒπ‘‘ ∈ 𝐷 𝑑 ∈ (𝐴𝐼𝑣) ↔ βˆƒπ‘‘ ∈ 𝐷 𝑑 ∈ (𝐴𝐼𝐡)))
1410, 13anbi12d 629 . . . 4 (𝑣 = 𝐡 β†’ (((𝐴 ∈ (𝑃 βˆ– 𝐷) ∧ 𝑣 ∈ (𝑃 βˆ– 𝐷)) ∧ βˆƒπ‘‘ ∈ 𝐷 𝑑 ∈ (𝐴𝐼𝑣)) ↔ ((𝐴 ∈ (𝑃 βˆ– 𝐷) ∧ 𝐡 ∈ (𝑃 βˆ– 𝐷)) ∧ βˆƒπ‘‘ ∈ 𝐷 𝑑 ∈ (𝐴𝐼𝐡))))
15 hpg.o . . . . 5 𝑂 = {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ (𝑃 βˆ– 𝐷) ∧ 𝑏 ∈ (𝑃 βˆ– 𝐷)) ∧ βˆƒπ‘‘ ∈ 𝐷 𝑑 ∈ (π‘ŽπΌπ‘))}
16 simpl 481 . . . . . . . . 9 ((π‘Ž = 𝑒 ∧ 𝑏 = 𝑣) β†’ π‘Ž = 𝑒)
1716eleq1d 2816 . . . . . . . 8 ((π‘Ž = 𝑒 ∧ 𝑏 = 𝑣) β†’ (π‘Ž ∈ (𝑃 βˆ– 𝐷) ↔ 𝑒 ∈ (𝑃 βˆ– 𝐷)))
18 simpr 483 . . . . . . . . 9 ((π‘Ž = 𝑒 ∧ 𝑏 = 𝑣) β†’ 𝑏 = 𝑣)
1918eleq1d 2816 . . . . . . . 8 ((π‘Ž = 𝑒 ∧ 𝑏 = 𝑣) β†’ (𝑏 ∈ (𝑃 βˆ– 𝐷) ↔ 𝑣 ∈ (𝑃 βˆ– 𝐷)))
2017, 19anbi12d 629 . . . . . . 7 ((π‘Ž = 𝑒 ∧ 𝑏 = 𝑣) β†’ ((π‘Ž ∈ (𝑃 βˆ– 𝐷) ∧ 𝑏 ∈ (𝑃 βˆ– 𝐷)) ↔ (𝑒 ∈ (𝑃 βˆ– 𝐷) ∧ 𝑣 ∈ (𝑃 βˆ– 𝐷))))
21 oveq12 7420 . . . . . . . . 9 ((π‘Ž = 𝑒 ∧ 𝑏 = 𝑣) β†’ (π‘ŽπΌπ‘) = (𝑒𝐼𝑣))
2221eleq2d 2817 . . . . . . . 8 ((π‘Ž = 𝑒 ∧ 𝑏 = 𝑣) β†’ (𝑑 ∈ (π‘ŽπΌπ‘) ↔ 𝑑 ∈ (𝑒𝐼𝑣)))
2322rexbidv 3176 . . . . . . 7 ((π‘Ž = 𝑒 ∧ 𝑏 = 𝑣) β†’ (βˆƒπ‘‘ ∈ 𝐷 𝑑 ∈ (π‘ŽπΌπ‘) ↔ βˆƒπ‘‘ ∈ 𝐷 𝑑 ∈ (𝑒𝐼𝑣)))
2420, 23anbi12d 629 . . . . . 6 ((π‘Ž = 𝑒 ∧ 𝑏 = 𝑣) β†’ (((π‘Ž ∈ (𝑃 βˆ– 𝐷) ∧ 𝑏 ∈ (𝑃 βˆ– 𝐷)) ∧ βˆƒπ‘‘ ∈ 𝐷 𝑑 ∈ (π‘ŽπΌπ‘)) ↔ ((𝑒 ∈ (𝑃 βˆ– 𝐷) ∧ 𝑣 ∈ (𝑃 βˆ– 𝐷)) ∧ βˆƒπ‘‘ ∈ 𝐷 𝑑 ∈ (𝑒𝐼𝑣))))
2524cbvopabv 5220 . . . . 5 {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ (𝑃 βˆ– 𝐷) ∧ 𝑏 ∈ (𝑃 βˆ– 𝐷)) ∧ βˆƒπ‘‘ ∈ 𝐷 𝑑 ∈ (π‘ŽπΌπ‘))} = {βŸ¨π‘’, π‘£βŸ© ∣ ((𝑒 ∈ (𝑃 βˆ– 𝐷) ∧ 𝑣 ∈ (𝑃 βˆ– 𝐷)) ∧ βˆƒπ‘‘ ∈ 𝐷 𝑑 ∈ (𝑒𝐼𝑣))}
2615, 25eqtri 2758 . . . 4 𝑂 = {βŸ¨π‘’, π‘£βŸ© ∣ ((𝑒 ∈ (𝑃 βˆ– 𝐷) ∧ 𝑣 ∈ (𝑃 βˆ– 𝐷)) ∧ βˆƒπ‘‘ ∈ 𝐷 𝑑 ∈ (𝑒𝐼𝑣))}
278, 14, 26brabg 5538 . . 3 ((𝐴 ∈ 𝑃 ∧ 𝐡 ∈ 𝑃) β†’ (𝐴𝑂𝐡 ↔ ((𝐴 ∈ (𝑃 βˆ– 𝐷) ∧ 𝐡 ∈ (𝑃 βˆ– 𝐷)) ∧ βˆƒπ‘‘ ∈ 𝐷 𝑑 ∈ (𝐴𝐼𝐡))))
281, 2, 27syl2anc 582 . 2 (πœ‘ β†’ (𝐴𝑂𝐡 ↔ ((𝐴 ∈ (𝑃 βˆ– 𝐷) ∧ 𝐡 ∈ (𝑃 βˆ– 𝐷)) ∧ βˆƒπ‘‘ ∈ 𝐷 𝑑 ∈ (𝐴𝐼𝐡))))
291biantrurd 531 . . . . 5 (πœ‘ β†’ (Β¬ 𝐴 ∈ 𝐷 ↔ (𝐴 ∈ 𝑃 ∧ Β¬ 𝐴 ∈ 𝐷)))
30 eldif 3957 . . . . 5 (𝐴 ∈ (𝑃 βˆ– 𝐷) ↔ (𝐴 ∈ 𝑃 ∧ Β¬ 𝐴 ∈ 𝐷))
3129, 30bitr4di 288 . . . 4 (πœ‘ β†’ (Β¬ 𝐴 ∈ 𝐷 ↔ 𝐴 ∈ (𝑃 βˆ– 𝐷)))
322biantrurd 531 . . . . 5 (πœ‘ β†’ (Β¬ 𝐡 ∈ 𝐷 ↔ (𝐡 ∈ 𝑃 ∧ Β¬ 𝐡 ∈ 𝐷)))
33 eldif 3957 . . . . 5 (𝐡 ∈ (𝑃 βˆ– 𝐷) ↔ (𝐡 ∈ 𝑃 ∧ Β¬ 𝐡 ∈ 𝐷))
3432, 33bitr4di 288 . . . 4 (πœ‘ β†’ (Β¬ 𝐡 ∈ 𝐷 ↔ 𝐡 ∈ (𝑃 βˆ– 𝐷)))
3531, 34anbi12d 629 . . 3 (πœ‘ β†’ ((Β¬ 𝐴 ∈ 𝐷 ∧ Β¬ 𝐡 ∈ 𝐷) ↔ (𝐴 ∈ (𝑃 βˆ– 𝐷) ∧ 𝐡 ∈ (𝑃 βˆ– 𝐷))))
3635anbi1d 628 . 2 (πœ‘ β†’ (((Β¬ 𝐴 ∈ 𝐷 ∧ Β¬ 𝐡 ∈ 𝐷) ∧ βˆƒπ‘‘ ∈ 𝐷 𝑑 ∈ (𝐴𝐼𝐡)) ↔ ((𝐴 ∈ (𝑃 βˆ– 𝐷) ∧ 𝐡 ∈ (𝑃 βˆ– 𝐷)) ∧ βˆƒπ‘‘ ∈ 𝐷 𝑑 ∈ (𝐴𝐼𝐡))))
3728, 36bitr4d 281 1 (πœ‘ β†’ (𝐴𝑂𝐡 ↔ ((Β¬ 𝐴 ∈ 𝐷 ∧ Β¬ 𝐡 ∈ 𝐷) ∧ βˆƒπ‘‘ ∈ 𝐷 𝑑 ∈ (𝐴𝐼𝐡))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 394   = wceq 1539   ∈ wcel 2104  βˆƒwrex 3068   βˆ– cdif 3944   class class class wbr 5147  {copab 5209  β€˜cfv 6542  (class class class)co 7411  Basecbs 17148  distcds 17210  Itvcitv 27951
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-iota 6494  df-fv 6550  df-ov 7414
This theorem is referenced by:  islnoppd  28258  oppne1  28259  oppne2  28260  oppne3  28261  oppcom  28262  oppnid  28264  opphllem1  28265  opphllem3  28267  opphllem5  28269  opphllem6  28270  oppperpex  28271  outpasch  28273  lnopp2hpgb  28281  hpgerlem  28283  colopp  28287  colhp  28288  trgcopyeulem  28323
  Copyright terms: Public domain W3C validator