Theorem islnopp 27681

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.

Step	Hyp	Ref	Expression
1		islnopp.a	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
2		islnopp.b	. . 3 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
3		eleq1 2825	. . . . . 6 ⊢ (𝑢 = 𝐴 → (𝑢 ∈ (𝑃 ∖ 𝐷) ↔ 𝐴 ∈ (𝑃 ∖ 𝐷)))
4	3	anbi1d 630	. . . . 5 ⊢ (𝑢 = 𝐴 → ((𝑢 ∈ (𝑃 ∖ 𝐷) ∧ 𝑣 ∈ (𝑃 ∖ 𝐷)) ↔ (𝐴 ∈ (𝑃 ∖ 𝐷) ∧ 𝑣 ∈ (𝑃 ∖ 𝐷))))
5		oveq1 7364	. . . . . . 7 ⊢ (𝑢 = 𝐴 → (𝑢𝐼𝑣) = (𝐴𝐼𝑣))
6	5	eleq2d 2823	. . . . . 6 ⊢ (𝑢 = 𝐴 → (𝑡 ∈ (𝑢𝐼𝑣) ↔ 𝑡 ∈ (𝐴𝐼𝑣)))
7	6	rexbidv 3175	. . . . 5 ⊢ (𝑢 = 𝐴 → (∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑢𝐼𝑣) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝑣)))
8	4, 7	anbi12d 631	. . . 4 ⊢ (𝑢 = 𝐴 → (((𝑢 ∈ (𝑃 ∖ 𝐷) ∧ 𝑣 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑢𝐼𝑣)) ↔ ((𝐴 ∈ (𝑃 ∖ 𝐷) ∧ 𝑣 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝑣))))
9		eleq1 2825	. . . . . 6 ⊢ (𝑣 = 𝐵 → (𝑣 ∈ (𝑃 ∖ 𝐷) ↔ 𝐵 ∈ (𝑃 ∖ 𝐷)))
10	9	anbi2d 629	. . . . 5 ⊢ (𝑣 = 𝐵 → ((𝐴 ∈ (𝑃 ∖ 𝐷) ∧ 𝑣 ∈ (𝑃 ∖ 𝐷)) ↔ (𝐴 ∈ (𝑃 ∖ 𝐷) ∧ 𝐵 ∈ (𝑃 ∖ 𝐷))))
11		oveq2 7365	. . . . . . 7 ⊢ (𝑣 = 𝐵 → (𝐴𝐼𝑣) = (𝐴𝐼𝐵))
12	11	eleq2d 2823	. . . . . 6 ⊢ (𝑣 = 𝐵 → (𝑡 ∈ (𝐴𝐼𝑣) ↔ 𝑡 ∈ (𝐴𝐼𝐵)))
13	12	rexbidv 3175	. . . . 5 ⊢ (𝑣 = 𝐵 → (∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝑣) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝐵)))
14	10, 13	anbi12d 631	. . . 4 ⊢ (𝑣 = 𝐵 → (((𝐴 ∈ (𝑃 ∖ 𝐷) ∧ 𝑣 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝑣)) ↔ ((𝐴 ∈ (𝑃 ∖ 𝐷) ∧ 𝐵 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝐵))))
15		hpg.o	. . . . 5 ⊢ 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))}
16		simpl 483	. . . . . . . . 9 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → 𝑎 = 𝑢)
17	16	eleq1d 2822	. . . . . . . 8 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → (𝑎 ∈ (𝑃 ∖ 𝐷) ↔ 𝑢 ∈ (𝑃 ∖ 𝐷)))
18		simpr 485	. . . . . . . . 9 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → 𝑏 = 𝑣)
19	18	eleq1d 2822	. . . . . . . 8 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → (𝑏 ∈ (𝑃 ∖ 𝐷) ↔ 𝑣 ∈ (𝑃 ∖ 𝐷)))
20	17, 19	anbi12d 631	. . . . . . 7 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ↔ (𝑢 ∈ (𝑃 ∖ 𝐷) ∧ 𝑣 ∈ (𝑃 ∖ 𝐷))))
21		oveq12 7366	. . . . . . . . 9 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → (𝑎𝐼𝑏) = (𝑢𝐼𝑣))
22	21	eleq2d 2823	. . . . . . . 8 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → (𝑡 ∈ (𝑎𝐼𝑏) ↔ 𝑡 ∈ (𝑢𝐼𝑣)))
23	22	rexbidv 3175	. . . . . . 7 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → (∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑢𝐼𝑣)))
24	20, 23	anbi12d 631	. . . . . 6 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏)) ↔ ((𝑢 ∈ (𝑃 ∖ 𝐷) ∧ 𝑣 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑢𝐼𝑣))))
25	24	cbvopabv 5178	. . . . 5 ⊢ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ (𝑃 ∖ 𝐷) ∧ 𝑣 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑢𝐼𝑣))}
26	15, 25	eqtri 2764	. . . 4 ⊢ 𝑂 = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ (𝑃 ∖ 𝐷) ∧ 𝑣 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑢𝐼𝑣))}
27	8, 14, 26	brabg 5496	. . 3 ⊢ ((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) → (𝐴𝑂𝐵 ↔ ((𝐴 ∈ (𝑃 ∖ 𝐷) ∧ 𝐵 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝐵))))
28	1, 2, 27	syl2anc 584	. 2 ⊢ (𝜑 → (𝐴𝑂𝐵 ↔ ((𝐴 ∈ (𝑃 ∖ 𝐷) ∧ 𝐵 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝐵))))
29	1	biantrurd 533	. . . . 5 ⊢ (𝜑 → (¬ 𝐴 ∈ 𝐷 ↔ (𝐴 ∈ 𝑃 ∧ ¬ 𝐴 ∈ 𝐷)))
30		eldif 3920	. . . . 5 ⊢ (𝐴 ∈ (𝑃 ∖ 𝐷) ↔ (𝐴 ∈ 𝑃 ∧ ¬ 𝐴 ∈ 𝐷))
31	29, 30	bitr4di 288	. . . 4 ⊢ (𝜑 → (¬ 𝐴 ∈ 𝐷 ↔ 𝐴 ∈ (𝑃 ∖ 𝐷)))
32	2	biantrurd 533	. . . . 5 ⊢ (𝜑 → (¬ 𝐵 ∈ 𝐷 ↔ (𝐵 ∈ 𝑃 ∧ ¬ 𝐵 ∈ 𝐷)))
33		eldif 3920	. . . . 5 ⊢ (𝐵 ∈ (𝑃 ∖ 𝐷) ↔ (𝐵 ∈ 𝑃 ∧ ¬ 𝐵 ∈ 𝐷))
34	32, 33	bitr4di 288	. . . 4 ⊢ (𝜑 → (¬ 𝐵 ∈ 𝐷 ↔ 𝐵 ∈ (𝑃 ∖ 𝐷)))
35	31, 34	anbi12d 631	. . 3 ⊢ (𝜑 → ((¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷) ↔ (𝐴 ∈ (𝑃 ∖ 𝐷) ∧ 𝐵 ∈ (𝑃 ∖ 𝐷))))
36	35	anbi1d 630	. 2 ⊢ (𝜑 → (((¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝐵)) ↔ ((𝐴 ∈ (𝑃 ∖ 𝐷) ∧ 𝐵 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝐵))))
37	28, 36	bitr4d 281	1 ⊢ (𝜑 → (𝐴𝑂𝐵 ↔ ((¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝐵))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ∃wrex 3073   ∖ cdif 3907   class class class wbr 5105  {copab 5167  ‘cfv 6496  (class class class)co 7357  Basecbs 17083  distcds 17142  Itvcitv 27375

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-rex 3074  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-iota 6448  df-fv 6504  df-ov 7360

This theorem is referenced by:  islnoppd  27682  oppne1  27683  oppne2  27684  oppne3  27685  oppcom  27686  oppnid  27688  opphllem1  27689  opphllem3  27691  opphllem5  27693  opphllem6  27694  oppperpex  27695  outpasch  27697  lnopp2hpgb  27705  hpgerlem  27707  colopp  27711  colhp  27712  trgcopyeulem  27747