Theorem islnopp

Description: The property for two points A and B to lie on the opposite sides of a set D Definition 9.1 of Schwabhauser p. 67. (Contributed by Thierry Arnoux, 19-Dec-2019)

	Ref	Expression
Hypotheses	hpg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	hpg.d	⊢ − = ( dist ‘ 𝐺 )
	hpg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	hpg.o	⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
	islnopp.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	islnopp.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
Assertion	islnopp	⊢ ( 𝜑 → ( 𝐴 𝑂 𝐵 ↔ ( ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		hpg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		hpg.d	⊢ − = ( dist ‘ 𝐺 )
3		hpg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		hpg.o	⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
5		islnopp.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6		islnopp.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7		eleq1	⊢ ( 𝑢 = 𝐴 → ( 𝑢 ∈ ( 𝑃 ∖ 𝐷 ) ↔ 𝐴 ∈ ( 𝑃 ∖ 𝐷 ) ) )
8	7	anbi1d	⊢ ( 𝑢 = 𝐴 → ( ( 𝑢 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑣 ∈ ( 𝑃 ∖ 𝐷 ) ) ↔ ( 𝐴 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑣 ∈ ( 𝑃 ∖ 𝐷 ) ) ) )
9		oveq1	⊢ ( 𝑢 = 𝐴 → ( 𝑢 𝐼 𝑣 ) = ( 𝐴 𝐼 𝑣 ) )
10	9	eleq2d	⊢ ( 𝑢 = 𝐴 → ( 𝑡 ∈ ( 𝑢 𝐼 𝑣 ) ↔ 𝑡 ∈ ( 𝐴 𝐼 𝑣 ) ) )
11	10	rexbidv	⊢ ( 𝑢 = 𝐴 → ( ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑢 𝐼 𝑣 ) ↔ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝑣 ) ) )
12	8 11	anbi12d	⊢ ( 𝑢 = 𝐴 → ( ( ( 𝑢 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑣 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑢 𝐼 𝑣 ) ) ↔ ( ( 𝐴 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑣 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝑣 ) ) ) )
13		eleq1	⊢ ( 𝑣 = 𝐵 → ( 𝑣 ∈ ( 𝑃 ∖ 𝐷 ) ↔ 𝐵 ∈ ( 𝑃 ∖ 𝐷 ) ) )
14	13	anbi2d	⊢ ( 𝑣 = 𝐵 → ( ( 𝐴 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑣 ∈ ( 𝑃 ∖ 𝐷 ) ) ↔ ( 𝐴 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝐵 ∈ ( 𝑃 ∖ 𝐷 ) ) ) )
15		oveq2	⊢ ( 𝑣 = 𝐵 → ( 𝐴 𝐼 𝑣 ) = ( 𝐴 𝐼 𝐵 ) )
16	15	eleq2d	⊢ ( 𝑣 = 𝐵 → ( 𝑡 ∈ ( 𝐴 𝐼 𝑣 ) ↔ 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ) )
17	16	rexbidv	⊢ ( 𝑣 = 𝐵 → ( ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝑣 ) ↔ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ) )
18	14 17	anbi12d	⊢ ( 𝑣 = 𝐵 → ( ( ( 𝐴 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑣 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝑣 ) ) ↔ ( ( 𝐴 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝐵 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ) ) )
19		simpl	⊢ ( ( 𝑎 = 𝑢 ∧ 𝑏 = 𝑣 ) → 𝑎 = 𝑢 )
20	19	eleq1d	⊢ ( ( 𝑎 = 𝑢 ∧ 𝑏 = 𝑣 ) → ( 𝑎 ∈ ( 𝑃 ∖ 𝐷 ) ↔ 𝑢 ∈ ( 𝑃 ∖ 𝐷 ) ) )
21		simpr	⊢ ( ( 𝑎 = 𝑢 ∧ 𝑏 = 𝑣 ) → 𝑏 = 𝑣 )
22	21	eleq1d	⊢ ( ( 𝑎 = 𝑢 ∧ 𝑏 = 𝑣 ) → ( 𝑏 ∈ ( 𝑃 ∖ 𝐷 ) ↔ 𝑣 ∈ ( 𝑃 ∖ 𝐷 ) ) )
23	20 22	anbi12d	⊢ ( ( 𝑎 = 𝑢 ∧ 𝑏 = 𝑣 ) → ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐷 ) ) ↔ ( 𝑢 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑣 ∈ ( 𝑃 ∖ 𝐷 ) ) ) )
24		oveq12	⊢ ( ( 𝑎 = 𝑢 ∧ 𝑏 = 𝑣 ) → ( 𝑎 𝐼 𝑏 ) = ( 𝑢 𝐼 𝑣 ) )
25	24	eleq2d	⊢ ( ( 𝑎 = 𝑢 ∧ 𝑏 = 𝑣 ) → ( 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ↔ 𝑡 ∈ ( 𝑢 𝐼 𝑣 ) ) )
26	25	rexbidv	⊢ ( ( 𝑎 = 𝑢 ∧ 𝑏 = 𝑣 ) → ( ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ↔ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑢 𝐼 𝑣 ) ) )
27	23 26	anbi12d	⊢ ( ( 𝑎 = 𝑢 ∧ 𝑏 = 𝑣 ) → ( ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) ↔ ( ( 𝑢 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑣 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑢 𝐼 𝑣 ) ) ) )
28	27	cbvopabv	⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) } = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑣 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑢 𝐼 𝑣 ) ) }
29	4 28	eqtri	⊢ 𝑂 = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑣 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑢 𝐼 𝑣 ) ) }
30	12 18 29	brabg	⊢ ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ) → ( 𝐴 𝑂 𝐵 ↔ ( ( 𝐴 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝐵 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ) ) )
31	5 6 30	syl2anc	⊢ ( 𝜑 → ( 𝐴 𝑂 𝐵 ↔ ( ( 𝐴 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝐵 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ) ) )
32	5	biantrurd	⊢ ( 𝜑 → ( ¬ 𝐴 ∈ 𝐷 ↔ ( 𝐴 ∈ 𝑃 ∧ ¬ 𝐴 ∈ 𝐷 ) ) )
33		eldif	⊢ ( 𝐴 ∈ ( 𝑃 ∖ 𝐷 ) ↔ ( 𝐴 ∈ 𝑃 ∧ ¬ 𝐴 ∈ 𝐷 ) )
34	32 33	bitr4di	⊢ ( 𝜑 → ( ¬ 𝐴 ∈ 𝐷 ↔ 𝐴 ∈ ( 𝑃 ∖ 𝐷 ) ) )
35	6	biantrurd	⊢ ( 𝜑 → ( ¬ 𝐵 ∈ 𝐷 ↔ ( 𝐵 ∈ 𝑃 ∧ ¬ 𝐵 ∈ 𝐷 ) ) )
36		eldif	⊢ ( 𝐵 ∈ ( 𝑃 ∖ 𝐷 ) ↔ ( 𝐵 ∈ 𝑃 ∧ ¬ 𝐵 ∈ 𝐷 ) )
37	35 36	bitr4di	⊢ ( 𝜑 → ( ¬ 𝐵 ∈ 𝐷 ↔ 𝐵 ∈ ( 𝑃 ∖ 𝐷 ) ) )
38	34 37	anbi12d	⊢ ( 𝜑 → ( ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ↔ ( 𝐴 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝐵 ∈ ( 𝑃 ∖ 𝐷 ) ) ) )
39	38	anbi1d	⊢ ( 𝜑 → ( ( ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ) ↔ ( ( 𝐴 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝐵 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ) ) )
40	31 39	bitr4d	⊢ ( 𝜑 → ( 𝐴 𝑂 𝐵 ↔ ( ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ) ) )