Theorem islnopp 26087

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 2847	. . . . . 6 ⊢ (𝑢 = 𝐴 → (𝑢 ∈ (𝑃 ∖ 𝐷) ↔ 𝐴 ∈ (𝑃 ∖ 𝐷)))
4	3	anbi1d 623	. . . . 5 ⊢ (𝑢 = 𝐴 → ((𝑢 ∈ (𝑃 ∖ 𝐷) ∧ 𝑣 ∈ (𝑃 ∖ 𝐷)) ↔ (𝐴 ∈ (𝑃 ∖ 𝐷) ∧ 𝑣 ∈ (𝑃 ∖ 𝐷))))
5		id 22	. . . . . . . 8 ⊢ (𝑢 = 𝐴 → 𝑢 = 𝐴)
6	5	oveq1d 6937	. . . . . . 7 ⊢ (𝑢 = 𝐴 → (𝑢𝐼𝑣) = (𝐴𝐼𝑣))
7	6	eleq2d 2845	. . . . . 6 ⊢ (𝑢 = 𝐴 → (𝑡 ∈ (𝑢𝐼𝑣) ↔ 𝑡 ∈ (𝐴𝐼𝑣)))
8	7	rexbidv 3237	. . . . 5 ⊢ (𝑢 = 𝐴 → (∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑢𝐼𝑣) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝑣)))
9	4, 8	anbi12d 624	. . . 4 ⊢ (𝑢 = 𝐴 → (((𝑢 ∈ (𝑃 ∖ 𝐷) ∧ 𝑣 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑢𝐼𝑣)) ↔ ((𝐴 ∈ (𝑃 ∖ 𝐷) ∧ 𝑣 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝑣))))
10		eleq1 2847	. . . . . 6 ⊢ (𝑣 = 𝐵 → (𝑣 ∈ (𝑃 ∖ 𝐷) ↔ 𝐵 ∈ (𝑃 ∖ 𝐷)))
11	10	anbi2d 622	. . . . 5 ⊢ (𝑣 = 𝐵 → ((𝐴 ∈ (𝑃 ∖ 𝐷) ∧ 𝑣 ∈ (𝑃 ∖ 𝐷)) ↔ (𝐴 ∈ (𝑃 ∖ 𝐷) ∧ 𝐵 ∈ (𝑃 ∖ 𝐷))))
12		oveq2 6930	. . . . . . 7 ⊢ (𝑣 = 𝐵 → (𝐴𝐼𝑣) = (𝐴𝐼𝐵))
13	12	eleq2d 2845	. . . . . 6 ⊢ (𝑣 = 𝐵 → (𝑡 ∈ (𝐴𝐼𝑣) ↔ 𝑡 ∈ (𝐴𝐼𝐵)))
14	13	rexbidv 3237	. . . . 5 ⊢ (𝑣 = 𝐵 → (∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝑣) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝐵)))
15	11, 14	anbi12d 624	. . . 4 ⊢ (𝑣 = 𝐵 → (((𝐴 ∈ (𝑃 ∖ 𝐷) ∧ 𝑣 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝑣)) ↔ ((𝐴 ∈ (𝑃 ∖ 𝐷) ∧ 𝐵 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝐵))))
16		hpg.o	. . . . 5 ⊢ 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))}
17		simpl 476	. . . . . . . . 9 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → 𝑎 = 𝑢)
18		eqidd 2779	. . . . . . . . 9 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → (𝑃 ∖ 𝐷) = (𝑃 ∖ 𝐷))
19	17, 18	eleq12d 2853	. . . . . . . 8 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → (𝑎 ∈ (𝑃 ∖ 𝐷) ↔ 𝑢 ∈ (𝑃 ∖ 𝐷)))
20		simpr 479	. . . . . . . . 9 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → 𝑏 = 𝑣)
21	20, 18	eleq12d 2853	. . . . . . . 8 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → (𝑏 ∈ (𝑃 ∖ 𝐷) ↔ 𝑣 ∈ (𝑃 ∖ 𝐷)))
22	19, 21	anbi12d 624	. . . . . . 7 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ↔ (𝑢 ∈ (𝑃 ∖ 𝐷) ∧ 𝑣 ∈ (𝑃 ∖ 𝐷))))
23		oveq12 6931	. . . . . . . . 9 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → (𝑎𝐼𝑏) = (𝑢𝐼𝑣))
24	23	eleq2d 2845	. . . . . . . 8 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → (𝑡 ∈ (𝑎𝐼𝑏) ↔ 𝑡 ∈ (𝑢𝐼𝑣)))
25	24	rexbidv 3237	. . . . . . 7 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → (∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑢𝐼𝑣)))
26	22, 25	anbi12d 624	. . . . . 6 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏)) ↔ ((𝑢 ∈ (𝑃 ∖ 𝐷) ∧ 𝑣 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑢𝐼𝑣))))
27	26	cbvopabv 4958	. . . . 5 ⊢ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ (𝑃 ∖ 𝐷) ∧ 𝑣 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑢𝐼𝑣))}
28	16, 27	eqtri 2802	. . . 4 ⊢ 𝑂 = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ (𝑃 ∖ 𝐷) ∧ 𝑣 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑢𝐼𝑣))}
29	9, 15, 28	brabg 5231	. . 3 ⊢ ((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) → (𝐴𝑂𝐵 ↔ ((𝐴 ∈ (𝑃 ∖ 𝐷) ∧ 𝐵 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝐵))))
30	1, 2, 29	syl2anc 579	. 2 ⊢ (𝜑 → (𝐴𝑂𝐵 ↔ ((𝐴 ∈ (𝑃 ∖ 𝐷) ∧ 𝐵 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝐵))))
31	1	biantrurd 528	. . . . 5 ⊢ (𝜑 → (¬ 𝐴 ∈ 𝐷 ↔ (𝐴 ∈ 𝑃 ∧ ¬ 𝐴 ∈ 𝐷)))
32		eldif 3802	. . . . 5 ⊢ (𝐴 ∈ (𝑃 ∖ 𝐷) ↔ (𝐴 ∈ 𝑃 ∧ ¬ 𝐴 ∈ 𝐷))
33	31, 32	syl6bbr 281	. . . 4 ⊢ (𝜑 → (¬ 𝐴 ∈ 𝐷 ↔ 𝐴 ∈ (𝑃 ∖ 𝐷)))
34	2	biantrurd 528	. . . . 5 ⊢ (𝜑 → (¬ 𝐵 ∈ 𝐷 ↔ (𝐵 ∈ 𝑃 ∧ ¬ 𝐵 ∈ 𝐷)))
35		eldif 3802	. . . . 5 ⊢ (𝐵 ∈ (𝑃 ∖ 𝐷) ↔ (𝐵 ∈ 𝑃 ∧ ¬ 𝐵 ∈ 𝐷))
36	34, 35	syl6bbr 281	. . . 4 ⊢ (𝜑 → (¬ 𝐵 ∈ 𝐷 ↔ 𝐵 ∈ (𝑃 ∖ 𝐷)))
37	33, 36	anbi12d 624	. . 3 ⊢ (𝜑 → ((¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷) ↔ (𝐴 ∈ (𝑃 ∖ 𝐷) ∧ 𝐵 ∈ (𝑃 ∖ 𝐷))))
38	37	anbi1d 623	. 2 ⊢ (𝜑 → (((¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝐵)) ↔ ((𝐴 ∈ (𝑃 ∖ 𝐷) ∧ 𝐵 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝐵))))
39	30, 38	bitr4d 274	1 ⊢ (𝜑 → (𝐴𝑂𝐵 ↔ ((¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝐵))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 386   = wceq 1601   ∈ wcel 2107  ∃wrex 3091   ∖ cdif 3789   class class class wbr 4886  {copab 4948  ‘cfv 6135  (class class class)co 6922  Basecbs 16255  distcds 16347  Itvcitv 25787

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5017  ax-nul 5025  ax-pr 5138

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rex 3096  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4672  df-br 4887  df-opab 4949  df-iota 6099  df-fv 6143  df-ov 6925

This theorem is referenced by:  islnoppd  26088  oppne1  26089  oppne2  26090  oppne3  26091  oppcom  26092  oppnid  26094  opphllem1  26095  opphllem3  26097  opphllem4  26098  opphllem5  26099  opphllem6  26100  oppperpex  26101  outpasch  26103  lnopp2hpgb  26111  hpgerlem  26113  colopp  26117  colhp  26118  lmiopp  26150  trgcopyeulem  26153