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 e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }
	islnopp.a	|- ( ph -> A e. P )
	islnopp.b	|- ( ph -> B e. P )
Assertion	islnopp	|- ( ph -> ( A O B <-> ( ( -. A e. D /\ -. B e. D ) /\ E. t e. D t e. ( 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 e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }
5		islnopp.a	|- ( ph -> A e. P )
6		islnopp.b	|- ( ph -> B e. P )
7		eleq1	|- ( u = A -> ( u e. ( P \ D ) <-> A e. ( P \ D ) ) )
8	7	anbi1d	|- ( u = A -> ( ( u e. ( P \ D ) /\ v e. ( P \ D ) ) <-> ( A e. ( P \ D ) /\ v e. ( P \ D ) ) ) )
9		oveq1	|- ( u = A -> ( u I v ) = ( A I v ) )
10	9	eleq2d	|- ( u = A -> ( t e. ( u I v ) <-> t e. ( A I v ) ) )
11	10	rexbidv	|- ( u = A -> ( E. t e. D t e. ( u I v ) <-> E. t e. D t e. ( A I v ) ) )
12	8 11	anbi12d	|- ( u = A -> ( ( ( u e. ( P \ D ) /\ v e. ( P \ D ) ) /\ E. t e. D t e. ( u I v ) ) <-> ( ( A e. ( P \ D ) /\ v e. ( P \ D ) ) /\ E. t e. D t e. ( A I v ) ) ) )
13		eleq1	|- ( v = B -> ( v e. ( P \ D ) <-> B e. ( P \ D ) ) )
14	13	anbi2d	|- ( v = B -> ( ( A e. ( P \ D ) /\ v e. ( P \ D ) ) <-> ( A e. ( P \ D ) /\ B e. ( P \ D ) ) ) )
15		oveq2	|- ( v = B -> ( A I v ) = ( A I B ) )
16	15	eleq2d	|- ( v = B -> ( t e. ( A I v ) <-> t e. ( A I B ) ) )
17	16	rexbidv	|- ( v = B -> ( E. t e. D t e. ( A I v ) <-> E. t e. D t e. ( A I B ) ) )
18	14 17	anbi12d	|- ( v = B -> ( ( ( A e. ( P \ D ) /\ v e. ( P \ D ) ) /\ E. t e. D t e. ( A I v ) ) <-> ( ( A e. ( P \ D ) /\ B e. ( P \ D ) ) /\ E. t e. D t e. ( A I B ) ) ) )
19		simpl	|- ( ( a = u /\ b = v ) -> a = u )
20	19	eleq1d	|- ( ( a = u /\ b = v ) -> ( a e. ( P \ D ) <-> u e. ( P \ D ) ) )
21		simpr	|- ( ( a = u /\ b = v ) -> b = v )
22	21	eleq1d	|- ( ( a = u /\ b = v ) -> ( b e. ( P \ D ) <-> v e. ( P \ D ) ) )
23	20 22	anbi12d	|- ( ( a = u /\ b = v ) -> ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) <-> ( u e. ( P \ D ) /\ v e. ( P \ D ) ) ) )
24		oveq12	|- ( ( a = u /\ b = v ) -> ( a I b ) = ( u I v ) )
25	24	eleq2d	|- ( ( a = u /\ b = v ) -> ( t e. ( a I b ) <-> t e. ( u I v ) ) )
26	25	rexbidv	|- ( ( a = u /\ b = v ) -> ( E. t e. D t e. ( a I b ) <-> E. t e. D t e. ( u I v ) ) )
27	23 26	anbi12d	|- ( ( a = u /\ b = v ) -> ( ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) <-> ( ( u e. ( P \ D ) /\ v e. ( P \ D ) ) /\ E. t e. D t e. ( u I v ) ) ) )
28	27	cbvopabv	|- { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) } = { <. u , v >. | ( ( u e. ( P \ D ) /\ v e. ( P \ D ) ) /\ E. t e. D t e. ( u I v ) ) }
29	4 28	eqtri	|- O = { <. u , v >. | ( ( u e. ( P \ D ) /\ v e. ( P \ D ) ) /\ E. t e. D t e. ( u I v ) ) }
30	12 18 29	brabg	|- ( ( A e. P /\ B e. P ) -> ( A O B <-> ( ( A e. ( P \ D ) /\ B e. ( P \ D ) ) /\ E. t e. D t e. ( A I B ) ) ) )
31	5 6 30	syl2anc	|- ( ph -> ( A O B <-> ( ( A e. ( P \ D ) /\ B e. ( P \ D ) ) /\ E. t e. D t e. ( A I B ) ) ) )
32	5	biantrurd	|- ( ph -> ( -. A e. D <-> ( A e. P /\ -. A e. D ) ) )
33		eldif	|- ( A e. ( P \ D ) <-> ( A e. P /\ -. A e. D ) )
34	32 33	bitr4di	|- ( ph -> ( -. A e. D <-> A e. ( P \ D ) ) )
35	6	biantrurd	|- ( ph -> ( -. B e. D <-> ( B e. P /\ -. B e. D ) ) )
36		eldif	|- ( B e. ( P \ D ) <-> ( B e. P /\ -. B e. D ) )
37	35 36	bitr4di	|- ( ph -> ( -. B e. D <-> B e. ( P \ D ) ) )
38	34 37	anbi12d	|- ( ph -> ( ( -. A e. D /\ -. B e. D ) <-> ( A e. ( P \ D ) /\ B e. ( P \ D ) ) ) )
39	38	anbi1d	|- ( ph -> ( ( ( -. A e. D /\ -. B e. D ) /\ E. t e. D t e. ( A I B ) ) <-> ( ( A e. ( P \ D ) /\ B e. ( P \ D ) ) /\ E. t e. D t e. ( A I B ) ) ) )
40	31 39	bitr4d	|- ( ph -> ( A O B <-> ( ( -. A e. D /\ -. B e. D ) /\ E. t e. D t e. ( A I B ) ) ) )