Metamath Proof Explorer

Theorem lineunray

Description: A line is composed of a point and the two rays emerging from it. Theorem 6.15 of Schwabhauser p. 45. (Contributed by Scott Fenton, 26-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion lineunray 
|- ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) -> ( P Btwn <. Q , R >. -> ( P Line Q ) = ( ( ( P Ray Q ) u. { P } ) u. ( P Ray R ) ) ) )

Proof

Step Hyp Ref Expression
1 simpl1 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) -> N e. NN )
2 simpr 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) -> x e. ( EE ` N ) )
3 simpl21 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) -> P e. ( EE ` N ) )
4 simpl22 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) -> Q e. ( EE ` N ) )
5 brcolinear 
 |-  ( ( N e. NN /\ ( x e. ( EE ` N ) /\ P e. ( EE ` N ) /\ Q e. ( EE ` N ) ) ) -> ( x Colinear <. P , Q >. <-> ( x Btwn <. P , Q >. \/ P Btwn <. Q , x >. \/ Q Btwn <. x , P >. ) ) )
6 1 2 3 4 5 syl13anc 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) -> ( x Colinear <. P , Q >. <-> ( x Btwn <. P , Q >. \/ P Btwn <. Q , x >. \/ Q Btwn <. x , P >. ) ) )
7 6 adantr 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ P Btwn <. Q , R >. ) -> ( x Colinear <. P , Q >. <-> ( x Btwn <. P , Q >. \/ P Btwn <. Q , x >. \/ Q Btwn <. x , P >. ) ) )
8 olc 
 |-  ( x Btwn <. P , Q >. -> ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) )
9 8 orcd 
 |-  ( x Btwn <. P , Q >. -> ( ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) \/ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) )
10 9 a1i 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ P Btwn <. Q , R >. ) -> ( x Btwn <. P , Q >. -> ( ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) \/ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) ) )
11 simpl3l 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) -> P =/= Q )
12 11 necomd 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) -> Q =/= P )
13 12 adantr 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ ( P Btwn <. Q , R >. /\ P Btwn <. Q , x >. ) ) -> Q =/= P )
14 simprl 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ ( P Btwn <. Q , R >. /\ P Btwn <. Q , x >. ) ) -> P Btwn <. Q , R >. )
15 simprr 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ ( P Btwn <. Q , R >. /\ P Btwn <. Q , x >. ) ) -> P Btwn <. Q , x >. )
16 13 14 15 3jca 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ ( P Btwn <. Q , R >. /\ P Btwn <. Q , x >. ) ) -> ( Q =/= P /\ P Btwn <. Q , R >. /\ P Btwn <. Q , x >. ) )
17 simpl23 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) -> R e. ( EE ` N ) )
18 btwnconn2 
 |-  ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ P e. ( EE ` N ) ) /\ ( R e. ( EE ` N ) /\ x e. ( EE ` N ) ) ) -> ( ( Q =/= P /\ P Btwn <. Q , R >. /\ P Btwn <. Q , x >. ) -> ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) )
19 1 4 3 17 2 18 syl122anc 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) -> ( ( Q =/= P /\ P Btwn <. Q , R >. /\ P Btwn <. Q , x >. ) -> ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) )
20 19 adantr 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ ( P Btwn <. Q , R >. /\ P Btwn <. Q , x >. ) ) -> ( ( Q =/= P /\ P Btwn <. Q , R >. /\ P Btwn <. Q , x >. ) -> ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) )
21 16 20 mpd 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ ( P Btwn <. Q , R >. /\ P Btwn <. Q , x >. ) ) -> ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) )
22 21 olcd 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ ( P Btwn <. Q , R >. /\ P Btwn <. Q , x >. ) ) -> ( ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) \/ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) )
23 22 expr 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ P Btwn <. Q , R >. ) -> ( P Btwn <. Q , x >. -> ( ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) \/ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) ) )
24 btwncom 
 |-  ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ x e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> ( Q Btwn <. x , P >. <-> Q Btwn <. P , x >. ) )
25 1 4 2 3 24 syl13anc 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) -> ( Q Btwn <. x , P >. <-> Q Btwn <. P , x >. ) )
26 orc 
 |-  ( Q Btwn <. P , x >. -> ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) )
27 26 orcd 
 |-  ( Q Btwn <. P , x >. -> ( ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) \/ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) )
28 25 27 syl6bi 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) -> ( Q Btwn <. x , P >. -> ( ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) \/ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) ) )
29 28 adantr 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ P Btwn <. Q , R >. ) -> ( Q Btwn <. x , P >. -> ( ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) \/ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) ) )
30 10 23 29 3jaod 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ P Btwn <. Q , R >. ) -> ( ( x Btwn <. P , Q >. \/ P Btwn <. Q , x >. \/ Q Btwn <. x , P >. ) -> ( ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) \/ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) ) )
31 7 30 sylbid 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ P Btwn <. Q , R >. ) -> ( x Colinear <. P , Q >. -> ( ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) \/ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) ) )
32 olc 
 |-  ( ( ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) \/ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) -> ( x = P \/ ( ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) \/ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) ) )
33 31 32 syl6 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ P Btwn <. Q , R >. ) -> ( x Colinear <. P , Q >. -> ( x = P \/ ( ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) \/ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) ) ) )
34 colineartriv1 
 |-  ( ( N e. NN /\ P e. ( EE ` N ) /\ Q e. ( EE ` N ) ) -> P Colinear <. P , Q >. )
35 1 3 4 34 syl3anc 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) -> P Colinear <. P , Q >. )
36 breq1 
 |-  ( x = P -> ( x Colinear <. P , Q >. <-> P Colinear <. P , Q >. ) )
37 35 36 syl5ibrcom 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) -> ( x = P -> x Colinear <. P , Q >. ) )
38 37 adantr 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ P Btwn <. Q , R >. ) -> ( x = P -> x Colinear <. P , Q >. ) )
39 btwncolinear3 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ x e. ( EE ` N ) /\ Q e. ( EE ` N ) ) ) -> ( Q Btwn <. P , x >. -> x Colinear <. P , Q >. ) )
40 1 3 2 4 39 syl13anc 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) -> ( Q Btwn <. P , x >. -> x Colinear <. P , Q >. ) )
41 btwncolinear5 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ x e. ( EE ` N ) ) ) -> ( x Btwn <. P , Q >. -> x Colinear <. P , Q >. ) )
42 1 3 4 2 41 syl13anc 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) -> ( x Btwn <. P , Q >. -> x Colinear <. P , Q >. ) )
43 40 42 jaod 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) -> ( ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) -> x Colinear <. P , Q >. ) )
44 43 adantr 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ P Btwn <. Q , R >. ) -> ( ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) -> x Colinear <. P , Q >. ) )
45 simpl3r 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) -> P =/= R )
46 45 adantr 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ ( P Btwn <. Q , R >. /\ R Btwn <. P , x >. ) ) -> P =/= R )
47 simprl 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ ( P Btwn <. Q , R >. /\ R Btwn <. P , x >. ) ) -> P Btwn <. Q , R >. )
48 simprr 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ ( P Btwn <. Q , R >. /\ R Btwn <. P , x >. ) ) -> R Btwn <. P , x >. )
49 46 47 48 3jca 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ ( P Btwn <. Q , R >. /\ R Btwn <. P , x >. ) ) -> ( P =/= R /\ P Btwn <. Q , R >. /\ R Btwn <. P , x >. ) )
50 btwnouttr 
 |-  ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ P e. ( EE ` N ) ) /\ ( R e. ( EE ` N ) /\ x e. ( EE ` N ) ) ) -> ( ( P =/= R /\ P Btwn <. Q , R >. /\ R Btwn <. P , x >. ) -> P Btwn <. Q , x >. ) )
51 1 4 3 17 2 50 syl122anc 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) -> ( ( P =/= R /\ P Btwn <. Q , R >. /\ R Btwn <. P , x >. ) -> P Btwn <. Q , x >. ) )
52 51 adantr 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ ( P Btwn <. Q , R >. /\ R Btwn <. P , x >. ) ) -> ( ( P =/= R /\ P Btwn <. Q , R >. /\ R Btwn <. P , x >. ) -> P Btwn <. Q , x >. ) )
53 49 52 mpd 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ ( P Btwn <. Q , R >. /\ R Btwn <. P , x >. ) ) -> P Btwn <. Q , x >. )
54 btwncolinear4 
 |-  ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ x e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> ( P Btwn <. Q , x >. -> x Colinear <. P , Q >. ) )
55 1 4 2 3 54 syl13anc 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) -> ( P Btwn <. Q , x >. -> x Colinear <. P , Q >. ) )
56 55 adantr 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ ( P Btwn <. Q , R >. /\ R Btwn <. P , x >. ) ) -> ( P Btwn <. Q , x >. -> x Colinear <. P , Q >. ) )
57 53 56 mpd 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ ( P Btwn <. Q , R >. /\ R Btwn <. P , x >. ) ) -> x Colinear <. P , Q >. )
58 57 expr 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ P Btwn <. Q , R >. ) -> ( R Btwn <. P , x >. -> x Colinear <. P , Q >. ) )
59 simprr 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ ( P Btwn <. Q , R >. /\ x Btwn <. P , R >. ) ) -> x Btwn <. P , R >. )
60 1 2 3 17 59 btwncomand 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ ( P Btwn <. Q , R >. /\ x Btwn <. P , R >. ) ) -> x Btwn <. R , P >. )
61 simprl 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ ( P Btwn <. Q , R >. /\ x Btwn <. P , R >. ) ) -> P Btwn <. Q , R >. )
62 1 3 4 17 61 btwncomand 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ ( P Btwn <. Q , R >. /\ x Btwn <. P , R >. ) ) -> P Btwn <. R , Q >. )
63 1 17 2 3 4 60 62 btwnexch3and 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ ( P Btwn <. Q , R >. /\ x Btwn <. P , R >. ) ) -> P Btwn <. x , Q >. )
64 btwncolinear2 
 |-  ( ( N e. NN /\ ( x e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> ( P Btwn <. x , Q >. -> x Colinear <. P , Q >. ) )
65 1 2 4 3 64 syl13anc 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) -> ( P Btwn <. x , Q >. -> x Colinear <. P , Q >. ) )
66 65 adantr 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ ( P Btwn <. Q , R >. /\ x Btwn <. P , R >. ) ) -> ( P Btwn <. x , Q >. -> x Colinear <. P , Q >. ) )
67 63 66 mpd 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ ( P Btwn <. Q , R >. /\ x Btwn <. P , R >. ) ) -> x Colinear <. P , Q >. )
68 67 expr 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ P Btwn <. Q , R >. ) -> ( x Btwn <. P , R >. -> x Colinear <. P , Q >. ) )
69 58 68 jaod 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ P Btwn <. Q , R >. ) -> ( ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) -> x Colinear <. P , Q >. ) )
70 44 69 jaod 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ P Btwn <. Q , R >. ) -> ( ( ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) \/ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) -> x Colinear <. P , Q >. ) )
71 38 70 jaod 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ P Btwn <. Q , R >. ) -> ( ( x = P \/ ( ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) \/ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) ) -> x Colinear <. P , Q >. ) )
72 33 71 impbid 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ P Btwn <. Q , R >. ) -> ( x Colinear <. P , Q >. <-> ( x = P \/ ( ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) \/ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) ) ) )
73 pm5.63 
 |-  ( ( x = P \/ ( ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) \/ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) ) <-> ( x = P \/ ( -. x = P /\ ( ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) \/ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) ) ) )
74 df-ne 
 |-  ( x =/= P <-> -. x = P )
75 74 anbi1i 
 |-  ( ( x =/= P /\ ( ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) \/ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) ) <-> ( -. x = P /\ ( ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) \/ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) ) )
76 andi 
 |-  ( ( x =/= P /\ ( ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) \/ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) ) <-> ( ( x =/= P /\ ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) ) \/ ( x =/= P /\ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) ) )
77 75 76 bitr3i 
 |-  ( ( -. x = P /\ ( ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) \/ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) ) <-> ( ( x =/= P /\ ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) ) \/ ( x =/= P /\ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) ) )
78 77 orbi2i 
 |-  ( ( x = P \/ ( -. x = P /\ ( ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) \/ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) ) ) <-> ( x = P \/ ( ( x =/= P /\ ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) ) \/ ( x =/= P /\ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) ) ) )
79 73 78 bitri 
 |-  ( ( x = P \/ ( ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) \/ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) ) <-> ( x = P \/ ( ( x =/= P /\ ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) ) \/ ( x =/= P /\ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) ) ) )
80 72 79 bitrdi 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ P Btwn <. Q , R >. ) -> ( x Colinear <. P , Q >. <-> ( x = P \/ ( ( x =/= P /\ ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) ) \/ ( x =/= P /\ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) ) ) ) )
81 broutsideof2 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ x e. ( EE ` N ) ) ) -> ( P OutsideOf <. Q , x >. <-> ( Q =/= P /\ x =/= P /\ ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) ) ) )
82 1 3 4 2 81 syl13anc 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) -> ( P OutsideOf <. Q , x >. <-> ( Q =/= P /\ x =/= P /\ ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) ) ) )
83 3simpc 
 |-  ( ( Q =/= P /\ x =/= P /\ ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) ) -> ( x =/= P /\ ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) ) )
84 simpl3l 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ ( x e. ( EE ` N ) /\ ( x =/= P /\ ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) ) ) ) -> P =/= Q )
85 84 necomd 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ ( x e. ( EE ` N ) /\ ( x =/= P /\ ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) ) ) ) -> Q =/= P )
86 simprrl 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ ( x e. ( EE ` N ) /\ ( x =/= P /\ ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) ) ) ) -> x =/= P )
87 simprrr 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ ( x e. ( EE ` N ) /\ ( x =/= P /\ ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) ) ) ) -> ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) )
88 85 86 87 3jca 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ ( x e. ( EE ` N ) /\ ( x =/= P /\ ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) ) ) ) -> ( Q =/= P /\ x =/= P /\ ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) ) )
89 88 expr 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) -> ( ( x =/= P /\ ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) ) -> ( Q =/= P /\ x =/= P /\ ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) ) ) )
90 83 89 impbid2 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) -> ( ( Q =/= P /\ x =/= P /\ ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) ) <-> ( x =/= P /\ ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) ) ) )
91 82 90 bitrd 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) -> ( P OutsideOf <. Q , x >. <-> ( x =/= P /\ ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) ) ) )
92 broutsideof2 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ R e. ( EE ` N ) /\ x e. ( EE ` N ) ) ) -> ( P OutsideOf <. R , x >. <-> ( R =/= P /\ x =/= P /\ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) ) )
93 1 3 17 2 92 syl13anc 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) -> ( P OutsideOf <. R , x >. <-> ( R =/= P /\ x =/= P /\ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) ) )
94 3simpc 
 |-  ( ( R =/= P /\ x =/= P /\ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) -> ( x =/= P /\ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) )
95 simpl3r 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ ( x e. ( EE ` N ) /\ ( x =/= P /\ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) ) ) -> P =/= R )
96 95 necomd 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ ( x e. ( EE ` N ) /\ ( x =/= P /\ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) ) ) -> R =/= P )
97 simprrl 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ ( x e. ( EE ` N ) /\ ( x =/= P /\ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) ) ) -> x =/= P )
98 simprrr 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ ( x e. ( EE ` N ) /\ ( x =/= P /\ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) ) ) -> ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) )
99 96 97 98 3jca 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ ( x e. ( EE ` N ) /\ ( x =/= P /\ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) ) ) -> ( R =/= P /\ x =/= P /\ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) )
100 99 expr 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) -> ( ( x =/= P /\ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) -> ( R =/= P /\ x =/= P /\ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) ) )
101 94 100 impbid2 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) -> ( ( R =/= P /\ x =/= P /\ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) <-> ( x =/= P /\ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) ) )
102 93 101 bitrd 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) -> ( P OutsideOf <. R , x >. <-> ( x =/= P /\ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) ) )
103 91 102 orbi12d 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) -> ( ( P OutsideOf <. Q , x >. \/ P OutsideOf <. R , x >. ) <-> ( ( x =/= P /\ ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) ) \/ ( x =/= P /\ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) ) ) )
104 103 adantr 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ P Btwn <. Q , R >. ) -> ( ( P OutsideOf <. Q , x >. \/ P OutsideOf <. R , x >. ) <-> ( ( x =/= P /\ ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) ) \/ ( x =/= P /\ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) ) ) )
105 104 orbi2d 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ P Btwn <. Q , R >. ) -> ( ( x = P \/ ( P OutsideOf <. Q , x >. \/ P OutsideOf <. R , x >. ) ) <-> ( x = P \/ ( ( x =/= P /\ ( Q Btwn <. P , x >. \/ x Btwn <. P , Q >. ) ) \/ ( x =/= P /\ ( R Btwn <. P , x >. \/ x Btwn <. P , R >. ) ) ) ) ) )
106 80 105 bitr4d 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ P Btwn <. Q , R >. ) -> ( x Colinear <. P , Q >. <-> ( x = P \/ ( P OutsideOf <. Q , x >. \/ P OutsideOf <. R , x >. ) ) ) )
107 orcom 
 |-  ( ( x = P \/ ( P OutsideOf <. Q , x >. \/ P OutsideOf <. R , x >. ) ) <-> ( ( P OutsideOf <. Q , x >. \/ P OutsideOf <. R , x >. ) \/ x = P ) )
108 or32 
 |-  ( ( ( P OutsideOf <. Q , x >. \/ P OutsideOf <. R , x >. ) \/ x = P ) <-> ( ( P OutsideOf <. Q , x >. \/ x = P ) \/ P OutsideOf <. R , x >. ) )
109 107 108 bitri 
 |-  ( ( x = P \/ ( P OutsideOf <. Q , x >. \/ P OutsideOf <. R , x >. ) ) <-> ( ( P OutsideOf <. Q , x >. \/ x = P ) \/ P OutsideOf <. R , x >. ) )
110 106 109 bitrdi 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ x e. ( EE ` N ) ) /\ P Btwn <. Q , R >. ) -> ( x Colinear <. P , Q >. <-> ( ( P OutsideOf <. Q , x >. \/ x = P ) \/ P OutsideOf <. R , x >. ) ) )
111 110 an32s 
 |-  ( ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ P Btwn <. Q , R >. ) /\ x e. ( EE ` N ) ) -> ( x Colinear <. P , Q >. <-> ( ( P OutsideOf <. Q , x >. \/ x = P ) \/ P OutsideOf <. R , x >. ) ) )
112 111 rabbidva 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ P Btwn <. Q , R >. ) -> { x e. ( EE ` N ) | x Colinear <. P , Q >. } = { x e. ( EE ` N ) | ( ( P OutsideOf <. Q , x >. \/ x = P ) \/ P OutsideOf <. R , x >. ) } )
113 simp1 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) -> N e. NN )
114 simp21 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) -> P e. ( EE ` N ) )
115 simp22 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) -> Q e. ( EE ` N ) )
116 simp3l 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) -> P =/= Q )
117 fvline2 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) ) -> ( P Line Q ) = { x e. ( EE ` N ) | x Colinear <. P , Q >. } )
118 113 114 115 116 117 syl13anc 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) -> ( P Line Q ) = { x e. ( EE ` N ) | x Colinear <. P , Q >. } )
119 118 adantr 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ P Btwn <. Q , R >. ) -> ( P Line Q ) = { x e. ( EE ` N ) | x Colinear <. P , Q >. } )
120 fvray 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) ) -> ( P Ray Q ) = { x e. ( EE ` N ) | P OutsideOf <. Q , x >. } )
121 113 114 115 116 120 syl13anc 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) -> ( P Ray Q ) = { x e. ( EE ` N ) | P OutsideOf <. Q , x >. } )
122 rabsn 
 |-  ( P e. ( EE ` N ) -> { x e. ( EE ` N ) | x = P } = { P } )
123 114 122 syl 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) -> { x e. ( EE ` N ) | x = P } = { P } )
124 123 eqcomd 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) -> { P } = { x e. ( EE ` N ) | x = P } )
125 121 124 uneq12d 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) -> ( ( P Ray Q ) u. { P } ) = ( { x e. ( EE ` N ) | P OutsideOf <. Q , x >. } u. { x e. ( EE ` N ) | x = P } ) )
126 simp23 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) -> R e. ( EE ` N ) )
127 simp3r 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) -> P =/= R )
128 fvray 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ R e. ( EE ` N ) /\ P =/= R ) ) -> ( P Ray R ) = { x e. ( EE ` N ) | P OutsideOf <. R , x >. } )
129 113 114 126 127 128 syl13anc 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) -> ( P Ray R ) = { x e. ( EE ` N ) | P OutsideOf <. R , x >. } )
130 125 129 uneq12d 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) -> ( ( ( P Ray Q ) u. { P } ) u. ( P Ray R ) ) = ( ( { x e. ( EE ` N ) | P OutsideOf <. Q , x >. } u. { x e. ( EE ` N ) | x = P } ) u. { x e. ( EE ` N ) | P OutsideOf <. R , x >. } ) )
131 130 adantr 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ P Btwn <. Q , R >. ) -> ( ( ( P Ray Q ) u. { P } ) u. ( P Ray R ) ) = ( ( { x e. ( EE ` N ) | P OutsideOf <. Q , x >. } u. { x e. ( EE ` N ) | x = P } ) u. { x e. ( EE ` N ) | P OutsideOf <. R , x >. } ) )
132 unrab 
 |-  ( { x e. ( EE ` N ) | P OutsideOf <. Q , x >. } u. { x e. ( EE ` N ) | x = P } ) = { x e. ( EE ` N ) | ( P OutsideOf <. Q , x >. \/ x = P ) }
133 132 uneq1i 
 |-  ( ( { x e. ( EE ` N ) | P OutsideOf <. Q , x >. } u. { x e. ( EE ` N ) | x = P } ) u. { x e. ( EE ` N ) | P OutsideOf <. R , x >. } ) = ( { x e. ( EE ` N ) | ( P OutsideOf <. Q , x >. \/ x = P ) } u. { x e. ( EE ` N ) | P OutsideOf <. R , x >. } )
134 unrab 
 |-  ( { x e. ( EE ` N ) | ( P OutsideOf <. Q , x >. \/ x = P ) } u. { x e. ( EE ` N ) | P OutsideOf <. R , x >. } ) = { x e. ( EE ` N ) | ( ( P OutsideOf <. Q , x >. \/ x = P ) \/ P OutsideOf <. R , x >. ) }
135 133 134 eqtri 
 |-  ( ( { x e. ( EE ` N ) | P OutsideOf <. Q , x >. } u. { x e. ( EE ` N ) | x = P } ) u. { x e. ( EE ` N ) | P OutsideOf <. R , x >. } ) = { x e. ( EE ` N ) | ( ( P OutsideOf <. Q , x >. \/ x = P ) \/ P OutsideOf <. R , x >. ) }
136 131 135 eqtrdi 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ P Btwn <. Q , R >. ) -> ( ( ( P Ray Q ) u. { P } ) u. ( P Ray R ) ) = { x e. ( EE ` N ) | ( ( P OutsideOf <. Q , x >. \/ x = P ) \/ P OutsideOf <. R , x >. ) } )
137 112 119 136 3eqtr4d 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) /\ P Btwn <. Q , R >. ) -> ( P Line Q ) = ( ( ( P Ray Q ) u. { P } ) u. ( P Ray R ) ) )
138 137 ex 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( P =/= Q /\ P =/= R ) ) -> ( P Btwn <. Q , R >. -> ( P Line Q ) = ( ( ( P Ray Q ) u. { P } ) u. ( P Ray R ) ) ) )