Metamath Proof Explorer


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 P = Base G
hpg.d - ˙ = dist G
hpg.i I = Itv G
hpg.o O = a b | a P D b P D t D t a I b
islnopp.a φ A P
islnopp.b φ B P
Assertion islnopp φ A O B ¬ A D ¬ B D t D t A I B

Proof

Step Hyp Ref Expression
1 hpg.p P = Base G
2 hpg.d - ˙ = dist G
3 hpg.i I = Itv G
4 hpg.o O = a b | a P D b P D t D t a I b
5 islnopp.a φ A P
6 islnopp.b φ B P
7 eleq1 u = A u P D A P D
8 7 anbi1d u = A u P D v P D A P D v P D
9 oveq1 u = A u I v = A I v
10 9 eleq2d u = A t u I v t A I v
11 10 rexbidv u = A t D t u I v t D t A I v
12 8 11 anbi12d u = A u P D v P D t D t u I v A P D v P D t D t A I v
13 eleq1 v = B v P D B P D
14 13 anbi2d v = B A P D v P D A P D B P D
15 oveq2 v = B A I v = A I B
16 15 eleq2d v = B t A I v t A I B
17 16 rexbidv v = B t D t A I v t D t A I B
18 14 17 anbi12d v = B A P D v P D t D t A I v A P D B P D t D t A I B
19 simpl a = u b = v a = u
20 19 eleq1d a = u b = v a P D u P D
21 simpr a = u b = v b = v
22 21 eleq1d a = u b = v b P D v P D
23 20 22 anbi12d a = u b = v a P D b P D u P D v P D
24 oveq12 a = u b = v a I b = u I v
25 24 eleq2d a = u b = v t a I b t u I v
26 25 rexbidv a = u b = v t D t a I b t D t u I v
27 23 26 anbi12d a = u b = v a P D b P D t D t a I b u P D v P D t D t u I v
28 27 cbvopabv a b | a P D b P D t D t a I b = u v | u P D v P D t D t u I v
29 4 28 eqtri O = u v | u P D v P D t D t u I v
30 12 18 29 brabg A P B P A O B A P D B P D t D t A I B
31 5 6 30 syl2anc φ A O B A P D B P D t D t A I B
32 5 biantrurd φ ¬ A D A P ¬ A D
33 eldif A P D A P ¬ A D
34 32 33 bitr4di φ ¬ A D A P D
35 6 biantrurd φ ¬ B D B P ¬ B D
36 eldif B P D B P ¬ B D
37 35 36 bitr4di φ ¬ B D B P D
38 34 37 anbi12d φ ¬ A D ¬ B D A P D B P D
39 38 anbi1d φ ¬ A D ¬ B D t D t A I B A P D B P D t D t A I B
40 31 39 bitr4d φ A O B ¬ A D ¬ B D t D t A I B