Metamath Proof Explorer

Theorem tglineeltr

Description: Transitivity law for lines, one half of tglineelsb2 . (Contributed by Thierry Arnoux, 25-May-2019)

Ref Expression
Hypotheses tglineelsb2.p 
|- B = ( Base ` G )
tglineelsb2.i 
|- I = ( Itv ` G )
tglineelsb2.l 
|- L = ( LineG ` G )
tglineelsb2.g 
|- ( ph -> G e. TarskiG )
tglineelsb2.1 
|- ( ph -> P e. B )
tglineelsb2.2 
|- ( ph -> Q e. B )
tglineelsb2.4 
|- ( ph -> P =/= Q )
tglineelsb2.3 
|- ( ph -> S e. B )
tglineelsb2.5 
|- ( ph -> S =/= P )
tglineelsb2.6 
|- ( ph -> S e. ( P L Q ) )
tglineeltr.7 
|- ( ph -> R e. B )
tglineeltr.8 
|- ( ph -> R e. ( P L S ) )
Assertion tglineeltr 
|- ( ph -> R e. ( P L Q ) )

Proof

Step Hyp Ref Expression
1 tglineelsb2.p 
 |-  B = ( Base ` G )
2 tglineelsb2.i 
 |-  I = ( Itv ` G )
3 tglineelsb2.l 
 |-  L = ( LineG ` G )
4 tglineelsb2.g 
 |-  ( ph -> G e. TarskiG )
5 tglineelsb2.1 
 |-  ( ph -> P e. B )
6 tglineelsb2.2 
 |-  ( ph -> Q e. B )
7 tglineelsb2.4 
 |-  ( ph -> P =/= Q )
8 tglineelsb2.3 
 |-  ( ph -> S e. B )
9 tglineelsb2.5 
 |-  ( ph -> S =/= P )
10 tglineelsb2.6 
 |-  ( ph -> S e. ( P L Q ) )
11 tglineeltr.7 
 |-  ( ph -> R e. B )
12 tglineeltr.8 
 |-  ( ph -> R e. ( P L S ) )
13 4 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ R e. ( P I S ) ) /\ S e. ( P I Q ) ) -> G e. TarskiG )
14 5 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ R e. ( P I S ) ) /\ S e. ( P I Q ) ) -> P e. B )
15 6 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ R e. ( P I S ) ) /\ S e. ( P I Q ) ) -> Q e. B )
16 simpllr 
 |-  ( ( ( ( ph /\ R e. B ) /\ R e. ( P I S ) ) /\ S e. ( P I Q ) ) -> R e. B )
17 eqid 
 |-  ( dist ` G ) = ( dist ` G )
18 8 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ R e. ( P I S ) ) /\ S e. ( P I Q ) ) -> S e. B )
19 simplr 
 |-  ( ( ( ( ph /\ R e. B ) /\ R e. ( P I S ) ) /\ S e. ( P I Q ) ) -> R e. ( P I S ) )
20 simpr 
 |-  ( ( ( ( ph /\ R e. B ) /\ R e. ( P I S ) ) /\ S e. ( P I Q ) ) -> S e. ( P I Q ) )
21 1 17 2 13 14 16 18 15 19 20 tgbtwnexch 
 |-  ( ( ( ( ph /\ R e. B ) /\ R e. ( P I S ) ) /\ S e. ( P I Q ) ) -> R e. ( P I Q ) )
22 1 3 2 13 14 15 16 21 btwncolg1 
 |-  ( ( ( ( ph /\ R e. B ) /\ R e. ( P I S ) ) /\ S e. ( P I Q ) ) -> ( R e. ( P L Q ) \/ P = Q ) )
23 4 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ R e. ( P I S ) ) /\ P e. ( S I Q ) ) -> G e. TarskiG )
24 5 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ R e. ( P I S ) ) /\ P e. ( S I Q ) ) -> P e. B )
25 6 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ R e. ( P I S ) ) /\ P e. ( S I Q ) ) -> Q e. B )
26 simpllr 
 |-  ( ( ( ( ph /\ R e. B ) /\ R e. ( P I S ) ) /\ P e. ( S I Q ) ) -> R e. B )
27 8 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ R e. ( P I S ) ) /\ P e. ( S I Q ) ) -> S e. B )
28 simplr 
 |-  ( ( ( ( ph /\ R e. B ) /\ R e. ( P I S ) ) /\ P e. ( S I Q ) ) -> R e. ( P I S ) )
29 1 17 2 23 24 26 27 28 tgbtwncom 
 |-  ( ( ( ( ph /\ R e. B ) /\ R e. ( P I S ) ) /\ P e. ( S I Q ) ) -> R e. ( S I P ) )
30 simpr 
 |-  ( ( ( ( ph /\ R e. B ) /\ R e. ( P I S ) ) /\ P e. ( S I Q ) ) -> P e. ( S I Q ) )
31 1 17 2 23 27 26 24 25 29 30 tgbtwnexch3 
 |-  ( ( ( ( ph /\ R e. B ) /\ R e. ( P I S ) ) /\ P e. ( S I Q ) ) -> P e. ( R I Q ) )
32 1 3 2 23 24 25 26 31 btwncolg2 
 |-  ( ( ( ( ph /\ R e. B ) /\ R e. ( P I S ) ) /\ P e. ( S I Q ) ) -> ( R e. ( P L Q ) \/ P = Q ) )
33 4 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ R e. ( P I S ) ) /\ Q e. ( P I S ) ) -> G e. TarskiG )
34 5 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ R e. ( P I S ) ) /\ Q e. ( P I S ) ) -> P e. B )
35 simpllr 
 |-  ( ( ( ( ph /\ R e. B ) /\ R e. ( P I S ) ) /\ Q e. ( P I S ) ) -> R e. B )
36 6 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ R e. ( P I S ) ) /\ Q e. ( P I S ) ) -> Q e. B )
37 8 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ R e. ( P I S ) ) /\ Q e. ( P I S ) ) -> S e. B )
38 simplr 
 |-  ( ( ( ( ph /\ R e. B ) /\ R e. ( P I S ) ) /\ Q e. ( P I S ) ) -> R e. ( P I S ) )
39 simpr 
 |-  ( ( ( ( ph /\ R e. B ) /\ R e. ( P I S ) ) /\ Q e. ( P I S ) ) -> Q e. ( P I S ) )
40 1 2 33 34 35 36 37 38 39 3 tgbtwnconnln3 
 |-  ( ( ( ( ph /\ R e. B ) /\ R e. ( P I S ) ) /\ Q e. ( P I S ) ) -> ( R e. ( P L Q ) \/ P = Q ) )
41 1 3 2 4 5 6 7 8 tgellng 
 |-  ( ph -> ( S e. ( P L Q ) <-> ( S e. ( P I Q ) \/ P e. ( S I Q ) \/ Q e. ( P I S ) ) ) )
42 10 41 mpbid 
 |-  ( ph -> ( S e. ( P I Q ) \/ P e. ( S I Q ) \/ Q e. ( P I S ) ) )
43 42 ad2antrr 
 |-  ( ( ( ph /\ R e. B ) /\ R e. ( P I S ) ) -> ( S e. ( P I Q ) \/ P e. ( S I Q ) \/ Q e. ( P I S ) ) )
44 22 32 40 43 mpjao3dan 
 |-  ( ( ( ph /\ R e. B ) /\ R e. ( P I S ) ) -> ( R e. ( P L Q ) \/ P = Q ) )
45 44 an32s 
 |-  ( ( ( ph /\ R e. ( P I S ) ) /\ R e. B ) -> ( R e. ( P L Q ) \/ P = Q ) )
46 11 45 mpidan 
 |-  ( ( ph /\ R e. ( P I S ) ) -> ( R e. ( P L Q ) \/ P = Q ) )
47 4 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ P e. ( R I S ) ) /\ S e. ( P I Q ) ) -> G e. TarskiG )
48 5 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ P e. ( R I S ) ) /\ S e. ( P I Q ) ) -> P e. B )
49 6 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ P e. ( R I S ) ) /\ S e. ( P I Q ) ) -> Q e. B )
50 simpllr 
 |-  ( ( ( ( ph /\ R e. B ) /\ P e. ( R I S ) ) /\ S e. ( P I Q ) ) -> R e. B )
51 8 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ P e. ( R I S ) ) /\ S e. ( P I Q ) ) -> S e. B )
52 9 necomd 
 |-  ( ph -> P =/= S )
53 52 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ P e. ( R I S ) ) /\ S e. ( P I Q ) ) -> P =/= S )
54 simplr 
 |-  ( ( ( ( ph /\ R e. B ) /\ P e. ( R I S ) ) /\ S e. ( P I Q ) ) -> P e. ( R I S ) )
55 simpr 
 |-  ( ( ( ( ph /\ R e. B ) /\ P e. ( R I S ) ) /\ S e. ( P I Q ) ) -> S e. ( P I Q ) )
56 1 17 2 47 50 48 51 49 53 54 55 tgbtwnouttr 
 |-  ( ( ( ( ph /\ R e. B ) /\ P e. ( R I S ) ) /\ S e. ( P I Q ) ) -> P e. ( R I Q ) )
57 1 3 2 47 48 49 50 56 btwncolg2 
 |-  ( ( ( ( ph /\ R e. B ) /\ P e. ( R I S ) ) /\ S e. ( P I Q ) ) -> ( R e. ( P L Q ) \/ P = Q ) )
58 4 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ P e. ( R I S ) ) /\ P e. ( S I Q ) ) -> G e. TarskiG )
59 6 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ P e. ( R I S ) ) /\ P e. ( S I Q ) ) -> Q e. B )
60 simpllr 
 |-  ( ( ( ( ph /\ R e. B ) /\ P e. ( R I S ) ) /\ P e. ( S I Q ) ) -> R e. B )
61 5 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ P e. ( R I S ) ) /\ P e. ( S I Q ) ) -> P e. B )
62 8 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ P e. ( R I S ) ) /\ P e. ( S I Q ) ) -> S e. B )
63 9 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ P e. ( R I S ) ) /\ P e. ( S I Q ) ) -> S =/= P )
64 simpr 
 |-  ( ( ( ( ph /\ R e. B ) /\ P e. ( R I S ) ) /\ P e. ( S I Q ) ) -> P e. ( S I Q ) )
65 simplr 
 |-  ( ( ( ( ph /\ R e. B ) /\ P e. ( R I S ) ) /\ P e. ( S I Q ) ) -> P e. ( R I S ) )
66 1 17 2 58 60 61 62 65 tgbtwncom 
 |-  ( ( ( ( ph /\ R e. B ) /\ P e. ( R I S ) ) /\ P e. ( S I Q ) ) -> P e. ( S I R ) )
67 1 2 58 62 61 59 60 3 63 64 66 tgbtwnconnln2 
 |-  ( ( ( ( ph /\ R e. B ) /\ P e. ( R I S ) ) /\ P e. ( S I Q ) ) -> ( P e. ( Q L R ) \/ Q = R ) )
68 1 3 2 58 59 60 61 67 colrot2 
 |-  ( ( ( ( ph /\ R e. B ) /\ P e. ( R I S ) ) /\ P e. ( S I Q ) ) -> ( R e. ( P L Q ) \/ P = Q ) )
69 4 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ P e. ( R I S ) ) /\ Q e. ( P I S ) ) -> G e. TarskiG )
70 6 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ P e. ( R I S ) ) /\ Q e. ( P I S ) ) -> Q e. B )
71 5 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ P e. ( R I S ) ) /\ Q e. ( P I S ) ) -> P e. B )
72 simpllr 
 |-  ( ( ( ( ph /\ R e. B ) /\ P e. ( R I S ) ) /\ Q e. ( P I S ) ) -> R e. B )
73 8 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ P e. ( R I S ) ) /\ Q e. ( P I S ) ) -> S e. B )
74 simpr 
 |-  ( ( ( ( ph /\ R e. B ) /\ P e. ( R I S ) ) /\ Q e. ( P I S ) ) -> Q e. ( P I S ) )
75 simplr 
 |-  ( ( ( ( ph /\ R e. B ) /\ P e. ( R I S ) ) /\ Q e. ( P I S ) ) -> P e. ( R I S ) )
76 1 17 2 69 70 71 72 73 74 75 tgbtwnintr 
 |-  ( ( ( ( ph /\ R e. B ) /\ P e. ( R I S ) ) /\ Q e. ( P I S ) ) -> P e. ( Q I R ) )
77 1 3 2 69 70 71 72 76 btwncolg3 
 |-  ( ( ( ( ph /\ R e. B ) /\ P e. ( R I S ) ) /\ Q e. ( P I S ) ) -> ( R e. ( Q L P ) \/ Q = P ) )
78 1 3 2 69 70 71 72 77 colcom 
 |-  ( ( ( ( ph /\ R e. B ) /\ P e. ( R I S ) ) /\ Q e. ( P I S ) ) -> ( R e. ( P L Q ) \/ P = Q ) )
79 42 ad2antrr 
 |-  ( ( ( ph /\ R e. B ) /\ P e. ( R I S ) ) -> ( S e. ( P I Q ) \/ P e. ( S I Q ) \/ Q e. ( P I S ) ) )
80 57 68 78 79 mpjao3dan 
 |-  ( ( ( ph /\ R e. B ) /\ P e. ( R I S ) ) -> ( R e. ( P L Q ) \/ P = Q ) )
81 80 an32s 
 |-  ( ( ( ph /\ P e. ( R I S ) ) /\ R e. B ) -> ( R e. ( P L Q ) \/ P = Q ) )
82 11 81 mpidan 
 |-  ( ( ph /\ P e. ( R I S ) ) -> ( R e. ( P L Q ) \/ P = Q ) )
83 4 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ S e. ( P I R ) ) /\ S e. ( P I Q ) ) -> G e. TarskiG )
84 6 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ S e. ( P I R ) ) /\ S e. ( P I Q ) ) -> Q e. B )
85 simpllr 
 |-  ( ( ( ( ph /\ R e. B ) /\ S e. ( P I R ) ) /\ S e. ( P I Q ) ) -> R e. B )
86 5 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ S e. ( P I R ) ) /\ S e. ( P I Q ) ) -> P e. B )
87 8 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ S e. ( P I R ) ) /\ S e. ( P I Q ) ) -> S e. B )
88 52 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ S e. ( P I R ) ) /\ S e. ( P I Q ) ) -> P =/= S )
89 simpr 
 |-  ( ( ( ( ph /\ R e. B ) /\ S e. ( P I R ) ) /\ S e. ( P I Q ) ) -> S e. ( P I Q ) )
90 simplr 
 |-  ( ( ( ( ph /\ R e. B ) /\ S e. ( P I R ) ) /\ S e. ( P I Q ) ) -> S e. ( P I R ) )
91 1 2 83 86 87 84 85 3 88 89 90 tgbtwnconnln1 
 |-  ( ( ( ( ph /\ R e. B ) /\ S e. ( P I R ) ) /\ S e. ( P I Q ) ) -> ( P e. ( Q L R ) \/ Q = R ) )
92 1 3 2 83 84 85 86 91 colrot2 
 |-  ( ( ( ( ph /\ R e. B ) /\ S e. ( P I R ) ) /\ S e. ( P I Q ) ) -> ( R e. ( P L Q ) \/ P = Q ) )
93 4 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ S e. ( P I R ) ) /\ P e. ( S I Q ) ) -> G e. TarskiG )
94 5 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ S e. ( P I R ) ) /\ P e. ( S I Q ) ) -> P e. B )
95 6 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ S e. ( P I R ) ) /\ P e. ( S I Q ) ) -> Q e. B )
96 simpllr 
 |-  ( ( ( ( ph /\ R e. B ) /\ S e. ( P I R ) ) /\ P e. ( S I Q ) ) -> R e. B )
97 8 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ S e. ( P I R ) ) /\ P e. ( S I Q ) ) -> S e. B )
98 9 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ S e. ( P I R ) ) /\ P e. ( S I Q ) ) -> S =/= P )
99 simplr 
 |-  ( ( ( ( ph /\ R e. B ) /\ S e. ( P I R ) ) /\ P e. ( S I Q ) ) -> S e. ( P I R ) )
100 1 17 2 93 94 97 96 99 tgbtwncom 
 |-  ( ( ( ( ph /\ R e. B ) /\ S e. ( P I R ) ) /\ P e. ( S I Q ) ) -> S e. ( R I P ) )
101 simpr 
 |-  ( ( ( ( ph /\ R e. B ) /\ S e. ( P I R ) ) /\ P e. ( S I Q ) ) -> P e. ( S I Q ) )
102 1 17 2 93 96 97 94 95 98 100 101 tgbtwnouttr2 
 |-  ( ( ( ( ph /\ R e. B ) /\ S e. ( P I R ) ) /\ P e. ( S I Q ) ) -> P e. ( R I Q ) )
103 1 3 2 93 94 95 96 102 btwncolg2 
 |-  ( ( ( ( ph /\ R e. B ) /\ S e. ( P I R ) ) /\ P e. ( S I Q ) ) -> ( R e. ( P L Q ) \/ P = Q ) )
104 4 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ S e. ( P I R ) ) /\ Q e. ( P I S ) ) -> G e. TarskiG )
105 5 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ S e. ( P I R ) ) /\ Q e. ( P I S ) ) -> P e. B )
106 6 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ S e. ( P I R ) ) /\ Q e. ( P I S ) ) -> Q e. B )
107 simpllr 
 |-  ( ( ( ( ph /\ R e. B ) /\ S e. ( P I R ) ) /\ Q e. ( P I S ) ) -> R e. B )
108 8 ad3antrrr 
 |-  ( ( ( ( ph /\ R e. B ) /\ S e. ( P I R ) ) /\ Q e. ( P I S ) ) -> S e. B )
109 simpr 
 |-  ( ( ( ( ph /\ R e. B ) /\ S e. ( P I R ) ) /\ Q e. ( P I S ) ) -> Q e. ( P I S ) )
110 simplr 
 |-  ( ( ( ( ph /\ R e. B ) /\ S e. ( P I R ) ) /\ Q e. ( P I S ) ) -> S e. ( P I R ) )
111 1 17 2 104 105 106 108 107 109 110 tgbtwnexch 
 |-  ( ( ( ( ph /\ R e. B ) /\ S e. ( P I R ) ) /\ Q e. ( P I S ) ) -> Q e. ( P I R ) )
112 1 3 2 104 105 106 107 111 btwncolg3 
 |-  ( ( ( ( ph /\ R e. B ) /\ S e. ( P I R ) ) /\ Q e. ( P I S ) ) -> ( R e. ( P L Q ) \/ P = Q ) )
113 42 ad2antrr 
 |-  ( ( ( ph /\ R e. B ) /\ S e. ( P I R ) ) -> ( S e. ( P I Q ) \/ P e. ( S I Q ) \/ Q e. ( P I S ) ) )
114 92 103 112 113 mpjao3dan 
 |-  ( ( ( ph /\ R e. B ) /\ S e. ( P I R ) ) -> ( R e. ( P L Q ) \/ P = Q ) )
115 114 an32s 
 |-  ( ( ( ph /\ S e. ( P I R ) ) /\ R e. B ) -> ( R e. ( P L Q ) \/ P = Q ) )
116 11 115 mpidan 
 |-  ( ( ph /\ S e. ( P I R ) ) -> ( R e. ( P L Q ) \/ P = Q ) )
117 id 
 |-  ( ph -> ph )
118 4 adantr 
 |-  ( ( ph /\ R e. B ) -> G e. TarskiG )
119 5 adantr 
 |-  ( ( ph /\ R e. B ) -> P e. B )
120 8 adantr 
 |-  ( ( ph /\ R e. B ) -> S e. B )
121 52 adantr 
 |-  ( ( ph /\ R e. B ) -> P =/= S )
122 simpr 
 |-  ( ( ph /\ R e. B ) -> R e. B )
123 1 3 2 118 119 120 121 122 tgellng 
 |-  ( ( ph /\ R e. B ) -> ( R e. ( P L S ) <-> ( R e. ( P I S ) \/ P e. ( R I S ) \/ S e. ( P I R ) ) ) )
124 123 biimpa 
 |-  ( ( ( ph /\ R e. B ) /\ R e. ( P L S ) ) -> ( R e. ( P I S ) \/ P e. ( R I S ) \/ S e. ( P I R ) ) )
125 117 11 12 124 syl21anc 
 |-  ( ph -> ( R e. ( P I S ) \/ P e. ( R I S ) \/ S e. ( P I R ) ) )
126 46 82 116 125 mpjao3dan 
 |-  ( ph -> ( R e. ( P L Q ) \/ P = Q ) )
127 7 neneqd 
 |-  ( ph -> -. P = Q )
128 pm5.61 
 |-  ( ( ( R e. ( P L Q ) \/ P = Q ) /\ -. P = Q ) <-> ( R e. ( P L Q ) /\ -. P = Q ) )
129 128 simplbi 
 |-  ( ( ( R e. ( P L Q ) \/ P = Q ) /\ -. P = Q ) -> R e. ( P L Q ) )
130 126 127 129 syl2anc 
 |-  ( ph -> R e. ( P L Q ) )