Theorem islnoppd

Description: Deduce that A and B lie on opposite sides of line L . (Contributed by Thierry Arnoux, 16-Aug-2020)

	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 ) ) }
	islnoppd.a	|- ( ph -> A e. P )
	islnoppd.b	|- ( ph -> B e. P )
	islnoppd.c	|- ( ph -> C e. D )
	islnoppd.1	|- ( ph -> -. A e. D )
	islnoppd.2	|- ( ph -> -. B e. D )
	islnoppd.3	|- ( ph -> C e. ( A I B ) )
Assertion	islnoppd	|- ( ph -> A O 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		islnoppd.a	|- ( ph -> A e. P )
6		islnoppd.b	|- ( ph -> B e. P )
7		islnoppd.c	|- ( ph -> C e. D )
8		islnoppd.1	|- ( ph -> -. A e. D )
9		islnoppd.2	|- ( ph -> -. B e. D )
10		islnoppd.3	|- ( ph -> C e. ( A I B ) )
11		simpr	|- ( ( ph /\ t = C ) -> t = C )
12	11	eleq1d	|- ( ( ph /\ t = C ) -> ( t e. ( A I B ) <-> C e. ( A I B ) ) )
13	7 12 10	rspcedvd	|- ( ph -> E. t e. D t e. ( A I B ) )
14	8 9 13	jca31	|- ( ph -> ( ( -. A e. D /\ -. B e. D ) /\ E. t e. D t e. ( A I B ) ) )
15	1 2 3 4 5 6	islnopp	|- ( ph -> ( A O B <-> ( ( -. A e. D /\ -. B e. D ) /\ E. t e. D t e. ( A I B ) ) ) )
16	14 15	mpbird	|- ( ph -> A O B )