Metamath Proof Explorer


Theorem lineelsb2

Description: If S lies on P Q , then P Q = P S . Theorem 6.16 of Schwabhauser p. 45. (Contributed by Scott Fenton, 27-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion lineelsb2 N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S S P Line Q P Line Q = P Line S

Proof

Step Hyp Ref Expression
1 simpl1 N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N N
2 simpl3l N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S 𝔼 N
3 simpl21 N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P 𝔼 N
4 simpl22 N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q 𝔼 N
5 brcolinear N S 𝔼 N P 𝔼 N Q 𝔼 N S Colinear P Q S Btwn P Q P Btwn Q S Q Btwn S P
6 1 2 3 4 5 syl13anc N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Colinear P Q S Btwn P Q P Btwn Q S Q Btwn S P
7 6 biimpa N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Colinear P Q S Btwn P Q P Btwn Q S Q Btwn S P
8 simpr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N x 𝔼 N
9 brcolinear N x 𝔼 N P 𝔼 N Q 𝔼 N x Colinear P Q x Btwn P Q P Btwn Q x Q Btwn x P
10 1 8 3 4 9 syl13anc N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N x Colinear P Q x Btwn P Q P Btwn Q x Q Btwn x P
11 10 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q x Colinear P Q x Btwn P Q P Btwn Q x Q Btwn x P
12 btwnconn3 N P 𝔼 N S 𝔼 N x 𝔼 N Q 𝔼 N S Btwn P Q x Btwn P Q S Btwn P x x Btwn P S
13 1 3 2 8 4 12 syl122anc N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q x Btwn P Q S Btwn P x x Btwn P S
14 13 imp N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q x Btwn P Q S Btwn P x x Btwn P S
15 btwncolinear3 N P 𝔼 N x 𝔼 N S 𝔼 N S Btwn P x x Colinear P S
16 1 3 8 2 15 syl13anc N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P x x Colinear P S
17 btwncolinear5 N P 𝔼 N S 𝔼 N x 𝔼 N x Btwn P S x Colinear P S
18 1 3 2 8 17 syl13anc N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N x Btwn P S x Colinear P S
19 16 18 jaod N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P x x Btwn P S x Colinear P S
20 19 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q x Btwn P Q S Btwn P x x Btwn P S x Colinear P S
21 14 20 mpd N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q x Btwn P Q x Colinear P S
22 21 expr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q x Btwn P Q x Colinear P S
23 simprl N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q P Btwn Q x S Btwn P Q
24 1 2 3 4 23 btwncomand N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q P Btwn Q x S Btwn Q P
25 simprr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q P Btwn Q x P Btwn Q x
26 1 4 2 3 8 24 25 btwnexch3and N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q P Btwn Q x P Btwn S x
27 btwncolinear4 N S 𝔼 N x 𝔼 N P 𝔼 N P Btwn S x x Colinear P S
28 1 2 8 3 27 syl13anc N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn S x x Colinear P S
29 28 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q P Btwn Q x P Btwn S x x Colinear P S
30 26 29 mpd N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q P Btwn Q x x Colinear P S
31 30 expr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q P Btwn Q x x Colinear P S
32 simprl N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q Q Btwn x P S Btwn P Q
33 simprr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q Q Btwn x P Q Btwn x P
34 1 4 8 3 33 btwncomand N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q Q Btwn x P Q Btwn P x
35 1 3 2 4 8 32 34 btwnexchand N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q Q Btwn x P S Btwn P x
36 16 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q Q Btwn x P S Btwn P x x Colinear P S
37 35 36 mpd N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q Q Btwn x P x Colinear P S
38 37 expr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q Q Btwn x P x Colinear P S
39 22 31 38 3jaod N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q x Btwn P Q P Btwn Q x Q Btwn x P x Colinear P S
40 11 39 sylbid N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q x Colinear P Q x Colinear P S
41 brcolinear N x 𝔼 N P 𝔼 N S 𝔼 N x Colinear P S x Btwn P S P Btwn S x S Btwn x P
42 1 8 3 2 41 syl13anc N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N x Colinear P S x Btwn P S P Btwn S x S Btwn x P
43 42 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q x Colinear P S x Btwn P S P Btwn S x S Btwn x P
44 simprr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q x Btwn P S x Btwn P S
45 simprl N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q x Btwn P S S Btwn P Q
46 1 3 8 2 4 44 45 btwnexchand N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q x Btwn P S x Btwn P Q
47 btwncolinear5 N P 𝔼 N Q 𝔼 N x 𝔼 N x Btwn P Q x Colinear P Q
48 1 3 4 8 47 syl13anc N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N x Btwn P Q x Colinear P Q
49 48 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q x Btwn P S x Btwn P Q x Colinear P Q
50 46 49 mpd N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q x Btwn P S x Colinear P Q
51 50 expr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q x Btwn P S x Colinear P Q
52 simpl3r N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P S
53 52 necomd N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S P
54 53 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q P Btwn S x S P
55 simprl N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q P Btwn S x S Btwn P Q
56 1 2 3 4 55 btwncomand N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q P Btwn S x S Btwn Q P
57 simprr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q P Btwn S x P Btwn S x
58 btwnouttr2 N Q 𝔼 N S 𝔼 N P 𝔼 N x 𝔼 N S P S Btwn Q P P Btwn S x P Btwn Q x
59 1 4 2 3 8 58 syl122anc N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S P S Btwn Q P P Btwn S x P Btwn Q x
60 59 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q P Btwn S x S P S Btwn Q P P Btwn S x P Btwn Q x
61 54 56 57 60 mp3and N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q P Btwn S x P Btwn Q x
62 btwncolinear4 N Q 𝔼 N x 𝔼 N P 𝔼 N P Btwn Q x x Colinear P Q
63 1 4 8 3 62 syl13anc N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q x x Colinear P Q
64 63 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q P Btwn S x P Btwn Q x x Colinear P Q
65 61 64 mpd N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q P Btwn S x x Colinear P Q
66 65 expr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q P Btwn S x x Colinear P Q
67 52 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q S Btwn x P P S
68 simprl N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q S Btwn x P S Btwn P Q
69 simprr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q S Btwn x P S Btwn x P
70 1 2 8 3 69 btwncomand N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q S Btwn x P S Btwn P x
71 btwnconn1 N P 𝔼 N S 𝔼 N Q 𝔼 N x 𝔼 N P S S Btwn P Q S Btwn P x Q Btwn P x x Btwn P Q
72 1 3 2 4 8 71 syl122anc N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P S S Btwn P Q S Btwn P x Q Btwn P x x Btwn P Q
73 72 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q S Btwn x P P S S Btwn P Q S Btwn P x Q Btwn P x x Btwn P Q
74 67 68 70 73 mp3and N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q S Btwn x P Q Btwn P x x Btwn P Q
75 btwncolinear3 N P 𝔼 N x 𝔼 N Q 𝔼 N Q Btwn P x x Colinear P Q
76 1 3 8 4 75 syl13anc N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn P x x Colinear P Q
77 76 48 jaod N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn P x x Btwn P Q x Colinear P Q
78 77 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q S Btwn x P Q Btwn P x x Btwn P Q x Colinear P Q
79 74 78 mpd N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q S Btwn x P x Colinear P Q
80 79 expr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q S Btwn x P x Colinear P Q
81 51 66 80 3jaod N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q x Btwn P S P Btwn S x S Btwn x P x Colinear P Q
82 43 81 sylbid N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q x Colinear P S x Colinear P Q
83 40 82 impbid N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q x Colinear P Q x Colinear P S
84 10 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S x Colinear P Q x Btwn P Q P Btwn Q x Q Btwn x P
85 simprr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S x Btwn P Q x Btwn P Q
86 1 8 3 4 85 btwncomand N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S x Btwn P Q x Btwn Q P
87 simprl N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S x Btwn P Q P Btwn Q S
88 1 4 8 3 2 86 87 btwnexch3and N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S x Btwn P Q P Btwn x S
89 btwncolinear2 N x 𝔼 N S 𝔼 N P 𝔼 N P Btwn x S x Colinear P S
90 1 8 2 3 89 syl13anc N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn x S x Colinear P S
91 90 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S x Btwn P Q P Btwn x S x Colinear P S
92 88 91 mpd N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S x Btwn P Q x Colinear P S
93 92 expr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S x Btwn P Q x Colinear P S
94 simpl23 N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Q
95 94 necomd N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q P
96 95 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S P Btwn Q x Q P
97 simprl N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S P Btwn Q x P Btwn Q S
98 simprr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S P Btwn Q x P Btwn Q x
99 btwnconn2 N Q 𝔼 N P 𝔼 N S 𝔼 N x 𝔼 N Q P P Btwn Q S P Btwn Q x S Btwn P x x Btwn P S
100 1 4 3 2 8 99 syl122anc N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q P P Btwn Q S P Btwn Q x S Btwn P x x Btwn P S
101 100 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S P Btwn Q x Q P P Btwn Q S P Btwn Q x S Btwn P x x Btwn P S
102 96 97 98 101 mp3and N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S P Btwn Q x S Btwn P x x Btwn P S
103 19 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S P Btwn Q x S Btwn P x x Btwn P S x Colinear P S
104 102 103 mpd N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S P Btwn Q x x Colinear P S
105 104 expr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S P Btwn Q x x Colinear P S
106 94 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S Q Btwn x P P Q
107 simprl N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S Q Btwn x P P Btwn Q S
108 1 3 4 2 107 btwncomand N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S Q Btwn x P P Btwn S Q
109 simprr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S Q Btwn x P Q Btwn x P
110 1 4 8 3 109 btwncomand N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S Q Btwn x P Q Btwn P x
111 btwnouttr N S 𝔼 N P 𝔼 N Q 𝔼 N x 𝔼 N P Q P Btwn S Q Q Btwn P x P Btwn S x
112 1 2 3 4 8 111 syl122anc N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Q P Btwn S Q Q Btwn P x P Btwn S x
113 112 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S Q Btwn x P P Q P Btwn S Q Q Btwn P x P Btwn S x
114 106 108 110 113 mp3and N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S Q Btwn x P P Btwn S x
115 28 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S Q Btwn x P P Btwn S x x Colinear P S
116 114 115 mpd N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S Q Btwn x P x Colinear P S
117 116 expr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S Q Btwn x P x Colinear P S
118 93 105 117 3jaod N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S x Btwn P Q P Btwn Q x Q Btwn x P x Colinear P S
119 84 118 sylbid N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S x Colinear P Q x Colinear P S
120 42 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S x Colinear P S x Btwn P S P Btwn S x S Btwn x P
121 simprr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S x Btwn P S x Btwn P S
122 1 8 3 2 121 btwncomand N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S x Btwn P S x Btwn S P
123 simprl N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S x Btwn P S P Btwn Q S
124 1 3 4 2 123 btwncomand N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S x Btwn P S P Btwn S Q
125 1 2 8 3 4 122 124 btwnexch3and N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S x Btwn P S P Btwn x Q
126 btwncolinear2 N x 𝔼 N Q 𝔼 N P 𝔼 N P Btwn x Q x Colinear P Q
127 1 8 4 3 126 syl13anc N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn x Q x Colinear P Q
128 127 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S x Btwn P S P Btwn x Q x Colinear P Q
129 125 128 mpd N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S x Btwn P S x Colinear P Q
130 129 expr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S x Btwn P S x Colinear P Q
131 53 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S P Btwn S x S P
132 simprl N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S P Btwn S x P Btwn Q S
133 1 3 4 2 132 btwncomand N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S P Btwn S x P Btwn S Q
134 simprr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S P Btwn S x P Btwn S x
135 btwnconn2 N S 𝔼 N P 𝔼 N Q 𝔼 N x 𝔼 N S P P Btwn S Q P Btwn S x Q Btwn P x x Btwn P Q
136 1 2 3 4 8 135 syl122anc N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S P P Btwn S Q P Btwn S x Q Btwn P x x Btwn P Q
137 136 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S P Btwn S x S P P Btwn S Q P Btwn S x Q Btwn P x x Btwn P Q
138 131 133 134 137 mp3and N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S P Btwn S x Q Btwn P x x Btwn P Q
139 77 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S P Btwn S x Q Btwn P x x Btwn P Q x Colinear P Q
140 138 139 mpd N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S P Btwn S x x Colinear P Q
141 140 expr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S P Btwn S x x Colinear P Q
142 52 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S S Btwn x P P S
143 simprl N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S S Btwn x P P Btwn Q S
144 simprr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S S Btwn x P S Btwn x P
145 1 2 8 3 144 btwncomand N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S S Btwn x P S Btwn P x
146 btwnouttr N Q 𝔼 N P 𝔼 N S 𝔼 N x 𝔼 N P S P Btwn Q S S Btwn P x P Btwn Q x
147 1 4 3 2 8 146 syl122anc N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P S P Btwn Q S S Btwn P x P Btwn Q x
148 147 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S S Btwn x P P S P Btwn Q S S Btwn P x P Btwn Q x
149 142 143 145 148 mp3and N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S S Btwn x P P Btwn Q x
150 63 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S S Btwn x P P Btwn Q x x Colinear P Q
151 149 150 mpd N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S S Btwn x P x Colinear P Q
152 151 expr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S S Btwn x P x Colinear P Q
153 130 141 152 3jaod N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S x Btwn P S P Btwn S x S Btwn x P x Colinear P Q
154 120 153 sylbid N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S x Colinear P S x Colinear P Q
155 119 154 impbid N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Btwn Q S x Colinear P Q x Colinear P S
156 10 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P x Colinear P Q x Btwn P Q P Btwn Q x Q Btwn x P
157 simprr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P x Btwn P Q x Btwn P Q
158 simprl N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P x Btwn P Q Q Btwn S P
159 1 4 2 3 158 btwncomand N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P x Btwn P Q Q Btwn P S
160 1 3 8 4 2 157 159 btwnexchand N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P x Btwn P Q x Btwn P S
161 18 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P x Btwn P Q x Btwn P S x Colinear P S
162 160 161 mpd N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P x Btwn P Q x Colinear P S
163 162 expr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P x Btwn P Q x Colinear P S
164 95 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P P Btwn Q x Q P
165 simprl N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P P Btwn Q x Q Btwn S P
166 simprr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P P Btwn Q x P Btwn Q x
167 btwnouttr2 N S 𝔼 N Q 𝔼 N P 𝔼 N x 𝔼 N Q P Q Btwn S P P Btwn Q x P Btwn S x
168 1 2 4 3 8 167 syl122anc N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q P Q Btwn S P P Btwn Q x P Btwn S x
169 168 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P P Btwn Q x Q P Q Btwn S P P Btwn Q x P Btwn S x
170 164 165 166 169 mp3and N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P P Btwn Q x P Btwn S x
171 28 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P P Btwn Q x P Btwn S x x Colinear P S
172 170 171 mpd N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P P Btwn Q x x Colinear P S
173 172 expr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P P Btwn Q x x Colinear P S
174 94 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P Q Btwn x P P Q
175 simprl N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P Q Btwn x P Q Btwn S P
176 1 4 2 3 175 btwncomand N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P Q Btwn x P Q Btwn P S
177 simprr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P Q Btwn x P Q Btwn x P
178 1 4 8 3 177 btwncomand N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P Q Btwn x P Q Btwn P x
179 btwnconn1 N P 𝔼 N Q 𝔼 N S 𝔼 N x 𝔼 N P Q Q Btwn P S Q Btwn P x S Btwn P x x Btwn P S
180 1 3 4 2 8 179 syl122anc N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N P Q Q Btwn P S Q Btwn P x S Btwn P x x Btwn P S
181 180 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P Q Btwn x P P Q Q Btwn P S Q Btwn P x S Btwn P x x Btwn P S
182 174 176 178 181 mp3and N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P Q Btwn x P S Btwn P x x Btwn P S
183 19 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P Q Btwn x P S Btwn P x x Btwn P S x Colinear P S
184 182 183 mpd N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P Q Btwn x P x Colinear P S
185 184 expr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P Q Btwn x P x Colinear P S
186 163 173 185 3jaod N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P x Btwn P Q P Btwn Q x Q Btwn x P x Colinear P S
187 156 186 sylbid N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P x Colinear P Q x Colinear P S
188 42 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P x Colinear P S x Btwn P S P Btwn S x S Btwn x P
189 simprl N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P x Btwn P S Q Btwn S P
190 1 4 2 3 189 btwncomand N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P x Btwn P S Q Btwn P S
191 simprr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P x Btwn P S x Btwn P S
192 btwnconn3 N P 𝔼 N Q 𝔼 N x 𝔼 N S 𝔼 N Q Btwn P S x Btwn P S Q Btwn P x x Btwn P Q
193 1 3 4 8 2 192 syl122anc N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn P S x Btwn P S Q Btwn P x x Btwn P Q
194 193 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P x Btwn P S Q Btwn P S x Btwn P S Q Btwn P x x Btwn P Q
195 190 191 194 mp2and N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P x Btwn P S Q Btwn P x x Btwn P Q
196 77 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P x Btwn P S Q Btwn P x x Btwn P Q x Colinear P Q
197 195 196 mpd N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P x Btwn P S x Colinear P Q
198 197 expr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P x Btwn P S x Colinear P Q
199 simprl N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P P Btwn S x Q Btwn S P
200 simprr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P P Btwn S x P Btwn S x
201 1 2 4 3 8 199 200 btwnexch3and N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P P Btwn S x P Btwn Q x
202 63 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P P Btwn S x P Btwn Q x x Colinear P Q
203 201 202 mpd N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P P Btwn S x x Colinear P Q
204 203 expr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P P Btwn S x x Colinear P Q
205 simprl N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P S Btwn x P Q Btwn S P
206 1 4 2 3 205 btwncomand N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P S Btwn x P Q Btwn P S
207 simprr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P S Btwn x P S Btwn x P
208 1 2 8 3 207 btwncomand N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P S Btwn x P S Btwn P x
209 1 3 4 2 8 206 208 btwnexchand N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P S Btwn x P Q Btwn P x
210 76 adantr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P S Btwn x P Q Btwn P x x Colinear P Q
211 209 210 mpd N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P S Btwn x P x Colinear P Q
212 211 expr N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P S Btwn x P x Colinear P Q
213 198 204 212 3jaod N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P x Btwn P S P Btwn S x S Btwn x P x Colinear P Q
214 188 213 sylbid N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P x Colinear P S x Colinear P Q
215 187 214 impbid N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N Q Btwn S P x Colinear P Q x Colinear P S
216 83 155 215 3jaodan N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Btwn P Q P Btwn Q S Q Btwn S P x Colinear P Q x Colinear P S
217 7 216 syldan N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S Colinear P Q x Colinear P Q x Colinear P S
218 217 adantrl N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S x 𝔼 N S 𝔼 N S Colinear P Q x Colinear P Q x Colinear P S
219 218 an32s N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S S 𝔼 N S Colinear P Q x 𝔼 N x Colinear P Q x Colinear P S
220 219 rabbidva N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S S 𝔼 N S Colinear P Q x 𝔼 N | x Colinear P Q = x 𝔼 N | x Colinear P S
221 220 ex N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S S 𝔼 N S Colinear P Q x 𝔼 N | x Colinear P Q = x 𝔼 N | x Colinear P S
222 fvline2 N P 𝔼 N Q 𝔼 N P Q P Line Q = x 𝔼 N | x Colinear P Q
223 222 3adant3 N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S P Line Q = x 𝔼 N | x Colinear P Q
224 223 eleq2d N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S S P Line Q S x 𝔼 N | x Colinear P Q
225 breq1 x = S x Colinear P Q S Colinear P Q
226 225 elrab S x 𝔼 N | x Colinear P Q S 𝔼 N S Colinear P Q
227 224 226 bitrdi N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S S P Line Q S 𝔼 N S Colinear P Q
228 simp1 N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S N
229 simp21 N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S P 𝔼 N
230 simp3l N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S S 𝔼 N
231 simp3r N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S P S
232 fvline2 N P 𝔼 N S 𝔼 N P S P Line S = x 𝔼 N | x Colinear P S
233 228 229 230 231 232 syl13anc N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S P Line S = x 𝔼 N | x Colinear P S
234 223 233 eqeq12d N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S P Line Q = P Line S x 𝔼 N | x Colinear P Q = x 𝔼 N | x Colinear P S
235 221 227 234 3imtr4d N P 𝔼 N Q 𝔼 N P Q S 𝔼 N P S S P Line Q P Line Q = P Line S