Metamath Proof Explorer

Theorem outsidele

Description: Relate OutsideOf to Seg<_ . Theorem 6.13 of Schwabhauser p. 45. (Contributed by Scott Fenton, 24-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion outsidele 
|- ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( P OutsideOf <. A , B >. -> ( <. P , A >. Seg<_ <. P , B >. <-> A Btwn <. P , B >. ) ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> N e. NN )
2 simpr1 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> P e. ( EE ` N ) )
3 simpr2 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
4 simpr3 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
5 brsegle2 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( P e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( <. P , A >. Seg<_ <. P , B >. <-> E. y e. ( EE ` N ) ( A Btwn <. P , y >. /\ <. P , y >. Cgr <. P , B >. ) ) )
6 1 2 3 2 4 5 syl122anc 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( <. P , A >. Seg<_ <. P , B >. <-> E. y e. ( EE ` N ) ( A Btwn <. P , y >. /\ <. P , y >. Cgr <. P , B >. ) ) )
7 6 adantr 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ P OutsideOf <. A , B >. ) -> ( <. P , A >. Seg<_ <. P , B >. <-> E. y e. ( EE ` N ) ( A Btwn <. P , y >. /\ <. P , y >. Cgr <. P , B >. ) ) )
8 simprl 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( P OutsideOf <. A , B >. /\ ( A Btwn <. P , y >. /\ <. P , y >. Cgr <. P , B >. ) ) ) -> P OutsideOf <. A , B >. )
9 outsideofcom 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( P OutsideOf <. A , B >. <-> P OutsideOf <. B , A >. ) )
10 9 ad2antrr 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( P OutsideOf <. A , B >. /\ ( A Btwn <. P , y >. /\ <. P , y >. Cgr <. P , B >. ) ) ) -> ( P OutsideOf <. A , B >. <-> P OutsideOf <. B , A >. ) )
11 8 10 mpbid 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( P OutsideOf <. A , B >. /\ ( A Btwn <. P , y >. /\ <. P , y >. Cgr <. P , B >. ) ) ) -> P OutsideOf <. B , A >. )
12 simpll 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) -> N e. NN )
13 simplr1 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) -> P e. ( EE ` N ) )
14 simplr3 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) -> B e. ( EE ` N ) )
15 12 13 14 cgrrflxd 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) -> <. P , B >. Cgr <. P , B >. )
16 15 adantr 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( P OutsideOf <. A , B >. /\ ( A Btwn <. P , y >. /\ <. P , y >. Cgr <. P , B >. ) ) ) -> <. P , B >. Cgr <. P , B >. )
17 11 16 jca 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( P OutsideOf <. A , B >. /\ ( A Btwn <. P , y >. /\ <. P , y >. Cgr <. P , B >. ) ) ) -> ( P OutsideOf <. B , A >. /\ <. P , B >. Cgr <. P , B >. ) )
18 simprrl 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( P OutsideOf <. A , B >. /\ ( A Btwn <. P , y >. /\ <. P , y >. Cgr <. P , B >. ) ) ) -> A Btwn <. P , y >. )
19 simpr 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) -> y e. ( EE ` N ) )
20 simplr2 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) -> A e. ( EE ` N ) )
21 btwncolinear1 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ y e. ( EE ` N ) /\ A e. ( EE ` N ) ) ) -> ( A Btwn <. P , y >. -> P Colinear <. y , A >. ) )
22 12 13 19 20 21 syl13anc 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) -> ( A Btwn <. P , y >. -> P Colinear <. y , A >. ) )
23 22 adantr 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( P OutsideOf <. A , B >. /\ ( A Btwn <. P , y >. /\ <. P , y >. Cgr <. P , B >. ) ) ) -> ( A Btwn <. P , y >. -> P Colinear <. y , A >. ) )
24 18 23 mpd 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( P OutsideOf <. A , B >. /\ ( A Btwn <. P , y >. /\ <. P , y >. Cgr <. P , B >. ) ) ) -> P Colinear <. y , A >. )
25 outsidene1 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( P OutsideOf <. A , B >. -> A =/= P ) )
26 25 ad2antrr 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( P OutsideOf <. A , B >. /\ ( A Btwn <. P , y >. /\ <. P , y >. Cgr <. P , B >. ) ) ) -> ( P OutsideOf <. A , B >. -> A =/= P ) )
27 8 26 mpd 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( P OutsideOf <. A , B >. /\ ( A Btwn <. P , y >. /\ <. P , y >. Cgr <. P , B >. ) ) ) -> A =/= P )
28 27 neneqd 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( P OutsideOf <. A , B >. /\ ( A Btwn <. P , y >. /\ <. P , y >. Cgr <. P , B >. ) ) ) -> -. A = P )
29 df-3an 
 |-  ( ( P OutsideOf <. A , B >. /\ ( A Btwn <. P , y >. /\ <. P , y >. Cgr <. P , B >. ) /\ P Btwn <. y , A >. ) <-> ( ( P OutsideOf <. A , B >. /\ ( A Btwn <. P , y >. /\ <. P , y >. Cgr <. P , B >. ) ) /\ P Btwn <. y , A >. ) )
30 simpr2l 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( P OutsideOf <. A , B >. /\ ( A Btwn <. P , y >. /\ <. P , y >. Cgr <. P , B >. ) /\ P Btwn <. y , A >. ) ) -> A Btwn <. P , y >. )
31 12 20 13 19 30 btwncomand 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( P OutsideOf <. A , B >. /\ ( A Btwn <. P , y >. /\ <. P , y >. Cgr <. P , B >. ) /\ P Btwn <. y , A >. ) ) -> A Btwn <. y , P >. )
32 simpr3 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( P OutsideOf <. A , B >. /\ ( A Btwn <. P , y >. /\ <. P , y >. Cgr <. P , B >. ) /\ P Btwn <. y , A >. ) ) -> P Btwn <. y , A >. )
33 btwnswapid2 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ y e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> ( ( A Btwn <. y , P >. /\ P Btwn <. y , A >. ) -> A = P ) )
34 12 20 19 13 33 syl13anc 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) -> ( ( A Btwn <. y , P >. /\ P Btwn <. y , A >. ) -> A = P ) )
35 34 adantr 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( P OutsideOf <. A , B >. /\ ( A Btwn <. P , y >. /\ <. P , y >. Cgr <. P , B >. ) /\ P Btwn <. y , A >. ) ) -> ( ( A Btwn <. y , P >. /\ P Btwn <. y , A >. ) -> A = P ) )
36 31 32 35 mp2and 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( P OutsideOf <. A , B >. /\ ( A Btwn <. P , y >. /\ <. P , y >. Cgr <. P , B >. ) /\ P Btwn <. y , A >. ) ) -> A = P )
37 29 36 sylan2br 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( ( P OutsideOf <. A , B >. /\ ( A Btwn <. P , y >. /\ <. P , y >. Cgr <. P , B >. ) ) /\ P Btwn <. y , A >. ) ) -> A = P )
38 37 expr 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( P OutsideOf <. A , B >. /\ ( A Btwn <. P , y >. /\ <. P , y >. Cgr <. P , B >. ) ) ) -> ( P Btwn <. y , A >. -> A = P ) )
39 28 38 mtod 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( P OutsideOf <. A , B >. /\ ( A Btwn <. P , y >. /\ <. P , y >. Cgr <. P , B >. ) ) ) -> -. P Btwn <. y , A >. )
40 broutsideof 
 |-  ( P OutsideOf <. y , A >. <-> ( P Colinear <. y , A >. /\ -. P Btwn <. y , A >. ) )
41 24 39 40 sylanbrc 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( P OutsideOf <. A , B >. /\ ( A Btwn <. P , y >. /\ <. P , y >. Cgr <. P , B >. ) ) ) -> P OutsideOf <. y , A >. )
42 simprrr 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( P OutsideOf <. A , B >. /\ ( A Btwn <. P , y >. /\ <. P , y >. Cgr <. P , B >. ) ) ) -> <. P , y >. Cgr <. P , B >. )
43 41 42 jca 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( P OutsideOf <. A , B >. /\ ( A Btwn <. P , y >. /\ <. P , y >. Cgr <. P , B >. ) ) ) -> ( P OutsideOf <. y , A >. /\ <. P , y >. Cgr <. P , B >. ) )
44 outsideofeq 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ P e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ B e. ( EE ` N ) /\ y e. ( EE ` N ) ) ) -> ( ( ( P OutsideOf <. B , A >. /\ <. P , B >. Cgr <. P , B >. ) /\ ( P OutsideOf <. y , A >. /\ <. P , y >. Cgr <. P , B >. ) ) -> B = y ) )
45 12 13 20 13 14 14 19 44 syl133anc 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) -> ( ( ( P OutsideOf <. B , A >. /\ <. P , B >. Cgr <. P , B >. ) /\ ( P OutsideOf <. y , A >. /\ <. P , y >. Cgr <. P , B >. ) ) -> B = y ) )
46 45 adantr 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( P OutsideOf <. A , B >. /\ ( A Btwn <. P , y >. /\ <. P , y >. Cgr <. P , B >. ) ) ) -> ( ( ( P OutsideOf <. B , A >. /\ <. P , B >. Cgr <. P , B >. ) /\ ( P OutsideOf <. y , A >. /\ <. P , y >. Cgr <. P , B >. ) ) -> B = y ) )
47 17 43 46 mp2and 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( P OutsideOf <. A , B >. /\ ( A Btwn <. P , y >. /\ <. P , y >. Cgr <. P , B >. ) ) ) -> B = y )
48 opeq2 
 |-  ( B = y -> <. P , B >. = <. P , y >. )
49 48 breq2d 
 |-  ( B = y -> ( A Btwn <. P , B >. <-> A Btwn <. P , y >. ) )
50 18 49 syl5ibrcom 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( P OutsideOf <. A , B >. /\ ( A Btwn <. P , y >. /\ <. P , y >. Cgr <. P , B >. ) ) ) -> ( B = y -> A Btwn <. P , B >. ) )
51 47 50 mpd 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( P OutsideOf <. A , B >. /\ ( A Btwn <. P , y >. /\ <. P , y >. Cgr <. P , B >. ) ) ) -> A Btwn <. P , B >. )
52 51 an4s 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ P OutsideOf <. A , B >. ) /\ ( y e. ( EE ` N ) /\ ( A Btwn <. P , y >. /\ <. P , y >. Cgr <. P , B >. ) ) ) -> A Btwn <. P , B >. )
53 52 rexlimdvaa 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ P OutsideOf <. A , B >. ) -> ( E. y e. ( EE ` N ) ( A Btwn <. P , y >. /\ <. P , y >. Cgr <. P , B >. ) -> A Btwn <. P , B >. ) )
54 7 53 sylbid 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ P OutsideOf <. A , B >. ) -> ( <. P , A >. Seg<_ <. P , B >. -> A Btwn <. P , B >. ) )
55 btwnsegle 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( A Btwn <. P , B >. -> <. P , A >. Seg<_ <. P , B >. ) )
56 55 adantr 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ P OutsideOf <. A , B >. ) -> ( A Btwn <. P , B >. -> <. P , A >. Seg<_ <. P , B >. ) )
57 54 56 impbid 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) /\ P OutsideOf <. A , B >. ) -> ( <. P , A >. Seg<_ <. P , B >. <-> A Btwn <. P , B >. ) )
58 57 ex 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( P OutsideOf <. A , B >. -> ( <. P , A >. Seg<_ <. P , B >. <-> A Btwn <. P , B >. ) ) )