Metamath Proof Explorer

Theorem outpasch

Description: Axiom of Pasch, outer form. This was proven by Gupta from other axioms and is therefore presented as Theorem 9.6 in Schwabhauser p. 70. (Contributed by Thierry Arnoux, 16-Aug-2020)

Ref Expression
Hypotheses outpasch.p 
|- P = ( Base ` G )
outpasch.i 
|- I = ( Itv ` G )
outpasch.l 
|- L = ( LineG ` G )
outpasch.g 
|- ( ph -> G e. TarskiG )
outpasch.a 
|- ( ph -> A e. P )
outpasch.b 
|- ( ph -> B e. P )
outpasch.c 
|- ( ph -> C e. P )
outpasch.r 
|- ( ph -> R e. P )
outpasch.q 
|- ( ph -> Q e. P )
outpasch.1 
|- ( ph -> C e. ( A I R ) )
outpasch.2 
|- ( ph -> Q e. ( B I C ) )
Assertion outpasch 
|- ( ph -> E. x e. P ( x e. ( A I B ) /\ Q e. ( R I x ) ) )

Proof

Step Hyp Ref Expression
1 outpasch.p 
 |-  P = ( Base ` G )
2 outpasch.i 
 |-  I = ( Itv ` G )
3 outpasch.l 
 |-  L = ( LineG ` G )
4 outpasch.g 
 |-  ( ph -> G e. TarskiG )
5 outpasch.a 
 |-  ( ph -> A e. P )
6 outpasch.b 
 |-  ( ph -> B e. P )
7 outpasch.c 
 |-  ( ph -> C e. P )
8 outpasch.r 
 |-  ( ph -> R e. P )
9 outpasch.q 
 |-  ( ph -> Q e. P )
10 outpasch.1 
 |-  ( ph -> C e. ( A I R ) )
11 outpasch.2 
 |-  ( ph -> Q e. ( B I C ) )
12 5 adantr 
 |-  ( ( ph /\ Q e. ( R I C ) ) -> A e. P )
13 simpr 
 |-  ( ( ( ph /\ Q e. ( R I C ) ) /\ x = A ) -> x = A )
14 13 eleq1d 
 |-  ( ( ( ph /\ Q e. ( R I C ) ) /\ x = A ) -> ( x e. ( A I B ) <-> A e. ( A I B ) ) )
15 13 oveq2d 
 |-  ( ( ( ph /\ Q e. ( R I C ) ) /\ x = A ) -> ( R I x ) = ( R I A ) )
16 15 eleq2d 
 |-  ( ( ( ph /\ Q e. ( R I C ) ) /\ x = A ) -> ( Q e. ( R I x ) <-> Q e. ( R I A ) ) )
17 14 16 anbi12d 
 |-  ( ( ( ph /\ Q e. ( R I C ) ) /\ x = A ) -> ( ( x e. ( A I B ) /\ Q e. ( R I x ) ) <-> ( A e. ( A I B ) /\ Q e. ( R I A ) ) ) )
18 eqid 
 |-  ( dist ` G ) = ( dist ` G )
19 1 18 2 4 5 6 tgbtwntriv1 
 |-  ( ph -> A e. ( A I B ) )
20 19 adantr 
 |-  ( ( ph /\ Q e. ( R I C ) ) -> A e. ( A I B ) )
21 4 adantr 
 |-  ( ( ph /\ Q e. ( R I C ) ) -> G e. TarskiG )
22 8 adantr 
 |-  ( ( ph /\ Q e. ( R I C ) ) -> R e. P )
23 9 adantr 
 |-  ( ( ph /\ Q e. ( R I C ) ) -> Q e. P )
24 7 adantr 
 |-  ( ( ph /\ Q e. ( R I C ) ) -> C e. P )
25 simpr 
 |-  ( ( ph /\ Q e. ( R I C ) ) -> Q e. ( R I C ) )
26 1 18 2 4 5 7 8 10 tgbtwncom 
 |-  ( ph -> C e. ( R I A ) )
27 26 adantr 
 |-  ( ( ph /\ Q e. ( R I C ) ) -> C e. ( R I A ) )
28 1 18 2 21 22 23 24 12 25 27 tgbtwnexch 
 |-  ( ( ph /\ Q e. ( R I C ) ) -> Q e. ( R I A ) )
29 20 28 jca 
 |-  ( ( ph /\ Q e. ( R I C ) ) -> ( A e. ( A I B ) /\ Q e. ( R I A ) ) )
30 12 17 29 rspcedvd 
 |-  ( ( ph /\ Q e. ( R I C ) ) -> E. x e. P ( x e. ( A I B ) /\ Q e. ( R I x ) ) )
31 30 adantlr 
 |-  ( ( ( ph /\ ( R e. ( Q L C ) \/ Q = C ) ) /\ Q e. ( R I C ) ) -> E. x e. P ( x e. ( A I B ) /\ Q e. ( R I x ) ) )
32 6 ad2antrr 
 |-  ( ( ( ph /\ ( R e. ( Q L C ) \/ Q = C ) ) /\ -. Q e. ( R I C ) ) -> B e. P )
33 eleq1 
 |-  ( x = B -> ( x e. ( A I B ) <-> B e. ( A I B ) ) )
34 oveq2 
 |-  ( x = B -> ( R I x ) = ( R I B ) )
35 34 eleq2d 
 |-  ( x = B -> ( Q e. ( R I x ) <-> Q e. ( R I B ) ) )
36 33 35 anbi12d 
 |-  ( x = B -> ( ( x e. ( A I B ) /\ Q e. ( R I x ) ) <-> ( B e. ( A I B ) /\ Q e. ( R I B ) ) ) )
37 36 adantl 
 |-  ( ( ( ( ph /\ ( R e. ( Q L C ) \/ Q = C ) ) /\ -. Q e. ( R I C ) ) /\ x = B ) -> ( ( x e. ( A I B ) /\ Q e. ( R I x ) ) <-> ( B e. ( A I B ) /\ Q e. ( R I B ) ) ) )
38 1 18 2 4 5 6 tgbtwntriv2 
 |-  ( ph -> B e. ( A I B ) )
39 38 ad2antrr 
 |-  ( ( ( ph /\ ( R e. ( Q L C ) \/ Q = C ) ) /\ -. Q e. ( R I C ) ) -> B e. ( A I B ) )
40 4 ad3antrrr 
 |-  ( ( ( ( ph /\ ( R e. ( Q L C ) \/ Q = C ) ) /\ -. Q e. ( R I C ) ) /\ R e. ( Q I C ) ) -> G e. TarskiG )
41 7 ad3antrrr 
 |-  ( ( ( ( ph /\ ( R e. ( Q L C ) \/ Q = C ) ) /\ -. Q e. ( R I C ) ) /\ R e. ( Q I C ) ) -> C e. P )
42 8 ad3antrrr 
 |-  ( ( ( ( ph /\ ( R e. ( Q L C ) \/ Q = C ) ) /\ -. Q e. ( R I C ) ) /\ R e. ( Q I C ) ) -> R e. P )
43 9 ad3antrrr 
 |-  ( ( ( ( ph /\ ( R e. ( Q L C ) \/ Q = C ) ) /\ -. Q e. ( R I C ) ) /\ R e. ( Q I C ) ) -> Q e. P )
44 6 ad3antrrr 
 |-  ( ( ( ( ph /\ ( R e. ( Q L C ) \/ Q = C ) ) /\ -. Q e. ( R I C ) ) /\ R e. ( Q I C ) ) -> B e. P )
45 simpr 
 |-  ( ( ( ( ph /\ ( R e. ( Q L C ) \/ Q = C ) ) /\ -. Q e. ( R I C ) ) /\ R e. ( Q I C ) ) -> R e. ( Q I C ) )
46 1 18 2 40 43 42 41 45 tgbtwncom 
 |-  ( ( ( ( ph /\ ( R e. ( Q L C ) \/ Q = C ) ) /\ -. Q e. ( R I C ) ) /\ R e. ( Q I C ) ) -> R e. ( C I Q ) )
47 1 18 2 4 6 9 7 11 tgbtwncom 
 |-  ( ph -> Q e. ( C I B ) )
48 47 ad3antrrr 
 |-  ( ( ( ( ph /\ ( R e. ( Q L C ) \/ Q = C ) ) /\ -. Q e. ( R I C ) ) /\ R e. ( Q I C ) ) -> Q e. ( C I B ) )
49 1 18 2 40 41 42 43 44 46 48 tgbtwnexch3 
 |-  ( ( ( ( ph /\ ( R e. ( Q L C ) \/ Q = C ) ) /\ -. Q e. ( R I C ) ) /\ R e. ( Q I C ) ) -> Q e. ( R I B ) )
50 4 ad3antrrr 
 |-  ( ( ( ( ph /\ ( R e. ( Q L C ) \/ Q = C ) ) /\ -. Q e. ( R I C ) ) /\ C e. ( Q I R ) ) -> G e. TarskiG )
51 6 ad3antrrr 
 |-  ( ( ( ( ph /\ ( R e. ( Q L C ) \/ Q = C ) ) /\ -. Q e. ( R I C ) ) /\ C e. ( Q I R ) ) -> B e. P )
52 9 ad3antrrr 
 |-  ( ( ( ( ph /\ ( R e. ( Q L C ) \/ Q = C ) ) /\ -. Q e. ( R I C ) ) /\ C e. ( Q I R ) ) -> Q e. P )
53 8 ad3antrrr 
 |-  ( ( ( ( ph /\ ( R e. ( Q L C ) \/ Q = C ) ) /\ -. Q e. ( R I C ) ) /\ C e. ( Q I R ) ) -> R e. P )
54 7 ad3antrrr 
 |-  ( ( ( ( ph /\ ( R e. ( Q L C ) \/ Q = C ) ) /\ -. Q e. ( R I C ) ) /\ C e. ( Q I R ) ) -> C e. P )
55 simpr 
 |-  ( ( ( ( ( ph /\ ( R e. ( Q L C ) \/ Q = C ) ) /\ -. Q e. ( R I C ) ) /\ C e. ( Q I R ) ) /\ Q = C ) -> Q = C )
56 1 18 2 4 8 7 tgbtwntriv2 
 |-  ( ph -> C e. ( R I C ) )
57 56 ad4antr 
 |-  ( ( ( ( ( ph /\ ( R e. ( Q L C ) \/ Q = C ) ) /\ -. Q e. ( R I C ) ) /\ C e. ( Q I R ) ) /\ Q = C ) -> C e. ( R I C ) )
58 55 57 eqeltrd 
 |-  ( ( ( ( ( ph /\ ( R e. ( Q L C ) \/ Q = C ) ) /\ -. Q e. ( R I C ) ) /\ C e. ( Q I R ) ) /\ Q = C ) -> Q e. ( R I C ) )
59 simpllr 
 |-  ( ( ( ( ( ph /\ ( R e. ( Q L C ) \/ Q = C ) ) /\ -. Q e. ( R I C ) ) /\ C e. ( Q I R ) ) /\ Q = C ) -> -. Q e. ( R I C ) )
60 58 59 pm2.65da 
 |-  ( ( ( ( ph /\ ( R e. ( Q L C ) \/ Q = C ) ) /\ -. Q e. ( R I C ) ) /\ C e. ( Q I R ) ) -> -. Q = C )
61 60 neqned 
 |-  ( ( ( ( ph /\ ( R e. ( Q L C ) \/ Q = C ) ) /\ -. Q e. ( R I C ) ) /\ C e. ( Q I R ) ) -> Q =/= C )
62 11 ad3antrrr 
 |-  ( ( ( ( ph /\ ( R e. ( Q L C ) \/ Q = C ) ) /\ -. Q e. ( R I C ) ) /\ C e. ( Q I R ) ) -> Q e. ( B I C ) )
63 simpr 
 |-  ( ( ( ( ph /\ ( R e. ( Q L C ) \/ Q = C ) ) /\ -. Q e. ( R I C ) ) /\ C e. ( Q I R ) ) -> C e. ( Q I R ) )
64 1 18 2 50 51 52 54 53 61 62 63 tgbtwnouttr 
 |-  ( ( ( ( ph /\ ( R e. ( Q L C ) \/ Q = C ) ) /\ -. Q e. ( R I C ) ) /\ C e. ( Q I R ) ) -> Q e. ( B I R ) )
65 1 18 2 50 51 52 53 64 tgbtwncom 
 |-  ( ( ( ( ph /\ ( R e. ( Q L C ) \/ Q = C ) ) /\ -. Q e. ( R I C ) ) /\ C e. ( Q I R ) ) -> Q e. ( R I B ) )
66 1 3 2 4 9 7 8 tgcolg 
 |-  ( ph -> ( ( R e. ( Q L C ) \/ Q = C ) <-> ( R e. ( Q I C ) \/ Q e. ( R I C ) \/ C e. ( Q I R ) ) ) )
67 66 biimpa 
 |-  ( ( ph /\ ( R e. ( Q L C ) \/ Q = C ) ) -> ( R e. ( Q I C ) \/ Q e. ( R I C ) \/ C e. ( Q I R ) ) )
68 3orcoma 
 |-  ( ( Q e. ( R I C ) \/ R e. ( Q I C ) \/ C e. ( Q I R ) ) <-> ( R e. ( Q I C ) \/ Q e. ( R I C ) \/ C e. ( Q I R ) ) )
69 3orass 
 |-  ( ( Q e. ( R I C ) \/ R e. ( Q I C ) \/ C e. ( Q I R ) ) <-> ( Q e. ( R I C ) \/ ( R e. ( Q I C ) \/ C e. ( Q I R ) ) ) )
70 68 69 bitr3i 
 |-  ( ( R e. ( Q I C ) \/ Q e. ( R I C ) \/ C e. ( Q I R ) ) <-> ( Q e. ( R I C ) \/ ( R e. ( Q I C ) \/ C e. ( Q I R ) ) ) )
71 67 70 sylib 
 |-  ( ( ph /\ ( R e. ( Q L C ) \/ Q = C ) ) -> ( Q e. ( R I C ) \/ ( R e. ( Q I C ) \/ C e. ( Q I R ) ) ) )
72 71 orcanai 
 |-  ( ( ( ph /\ ( R e. ( Q L C ) \/ Q = C ) ) /\ -. Q e. ( R I C ) ) -> ( R e. ( Q I C ) \/ C e. ( Q I R ) ) )
73 49 65 72 mpjaodan 
 |-  ( ( ( ph /\ ( R e. ( Q L C ) \/ Q = C ) ) /\ -. Q e. ( R I C ) ) -> Q e. ( R I B ) )
74 39 73 jca 
 |-  ( ( ( ph /\ ( R e. ( Q L C ) \/ Q = C ) ) /\ -. Q e. ( R I C ) ) -> ( B e. ( A I B ) /\ Q e. ( R I B ) ) )
75 32 37 74 rspcedvd 
 |-  ( ( ( ph /\ ( R e. ( Q L C ) \/ Q = C ) ) /\ -. Q e. ( R I C ) ) -> E. x e. P ( x e. ( A I B ) /\ Q e. ( R I x ) ) )
76 31 75 pm2.61dan 
 |-  ( ( ph /\ ( R e. ( Q L C ) \/ Q = C ) ) -> E. x e. P ( x e. ( A I B ) /\ Q e. ( R I x ) ) )
77 6 ad2antrr 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ B e. ( R L Q ) ) -> B e. P )
78 36 adantl 
 |-  ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ B e. ( R L Q ) ) /\ x = B ) -> ( ( x e. ( A I B ) /\ Q e. ( R I x ) ) <-> ( B e. ( A I B ) /\ Q e. ( R I B ) ) ) )
79 38 ad2antrr 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ B e. ( R L Q ) ) -> B e. ( A I B ) )
80 4 ad2antrr 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ B e. ( R L Q ) ) -> G e. TarskiG )
81 8 ad2antrr 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ B e. ( R L Q ) ) -> R e. P )
82 9 ad2antrr 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ B e. ( R L Q ) ) -> Q e. P )
83 7 ad2antrr 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ B e. ( R L Q ) ) -> C e. P )
84 simplr 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ B e. ( R L Q ) ) -> -. ( R e. ( Q L C ) \/ Q = C ) )
85 simpr 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ B e. ( R L Q ) ) -> B e. ( R L Q ) )
86 4 adantr 
 |-  ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) -> G e. TarskiG )
87 8 adantr 
 |-  ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) -> R e. P )
88 9 adantr 
 |-  ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) -> Q e. P )
89 7 adantr 
 |-  ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) -> C e. P )
90 simpr 
 |-  ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) -> -. ( R e. ( Q L C ) \/ Q = C ) )
91 1 2 3 86 87 88 89 90 ncolne1 
 |-  ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) -> R =/= Q )
92 1 2 3 86 87 88 91 tglinerflx2 
 |-  ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) -> Q e. ( R L Q ) )
93 92 adantr 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ B e. ( R L Q ) ) -> Q e. ( R L Q ) )
94 1 3 2 86 88 89 87 90 ncolcom 
 |-  ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) -> -. ( R e. ( C L Q ) \/ C = Q ) )
95 1 3 2 86 89 88 87 94 ncolrot1 
 |-  ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) -> -. ( C e. ( Q L R ) \/ Q = R ) )
96 1 2 3 86 89 88 87 95 ncolne1 
 |-  ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) -> C =/= Q )
97 96 adantr 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ B e. ( R L Q ) ) -> C =/= Q )
98 47 ad2antrr 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ B e. ( R L Q ) ) -> Q e. ( C I B ) )
99 1 2 3 80 83 82 77 97 98 btwnlng3 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ B e. ( R L Q ) ) -> B e. ( C L Q ) )
100 1 2 3 80 83 82 97 tglinerflx2 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ B e. ( R L Q ) ) -> Q e. ( C L Q ) )
101 1 2 3 80 81 82 83 82 84 85 93 99 100 tglineinteq 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ B e. ( R L Q ) ) -> B = Q )
102 1 18 2 4 8 6 tgbtwntriv2 
 |-  ( ph -> B e. ( R I B ) )
103 102 ad2antrr 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ B e. ( R L Q ) ) -> B e. ( R I B ) )
104 101 103 eqeltrrd 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ B e. ( R L Q ) ) -> Q e. ( R I B ) )
105 79 104 jca 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ B e. ( R L Q ) ) -> ( B e. ( A I B ) /\ Q e. ( R I B ) ) )
106 77 78 105 rspcedvd 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ B e. ( R L Q ) ) -> E. x e. P ( x e. ( A I B ) /\ Q e. ( R I x ) ) )
107 eleq1 
 |-  ( t = x -> ( t e. ( a I b ) <-> x e. ( a I b ) ) )
108 107 cbvrexvw 
 |-  ( E. t e. ( R L Q ) t e. ( a I b ) <-> E. x e. ( R L Q ) x e. ( a I b ) )
109 108 anbi2i 
 |-  ( ( ( a e. ( P \ ( R L Q ) ) /\ b e. ( P \ ( R L Q ) ) ) /\ E. t e. ( R L Q ) t e. ( a I b ) ) <-> ( ( a e. ( P \ ( R L Q ) ) /\ b e. ( P \ ( R L Q ) ) ) /\ E. x e. ( R L Q ) x e. ( a I b ) ) )
110 109 opabbii 
 |-  { <. a , b >. | ( ( a e. ( P \ ( R L Q ) ) /\ b e. ( P \ ( R L Q ) ) ) /\ E. t e. ( R L Q ) t e. ( a I b ) ) } = { <. a , b >. | ( ( a e. ( P \ ( R L Q ) ) /\ b e. ( P \ ( R L Q ) ) ) /\ E. x e. ( R L Q ) x e. ( a I b ) ) }
111 4 ad2antrr 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) -> G e. TarskiG )
112 8 ad2antrr 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) -> R e. P )
113 9 ad2antrr 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) -> Q e. P )
114 91 adantr 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) -> R =/= Q )
115 1 2 3 111 112 113 114 tgelrnln 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) -> ( R L Q ) e. ran L )
116 eqid 
 |-  ( hlG ` G ) = ( hlG ` G )
117 7 ad2antrr 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) -> C e. P )
118 5 ad2antrr 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) -> A e. P )
119 6 ad2antrr 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) -> B e. P )
120 92 adantr 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) -> Q e. ( R L Q ) )
121 1 3 2 86 88 89 87 90 ncolrot2 
 |-  ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) -> -. ( C e. ( R L Q ) \/ R = Q ) )
122 pm2.45 
 |-  ( -. ( C e. ( R L Q ) \/ R = Q ) -> -. C e. ( R L Q ) )
123 121 122 syl 
 |-  ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) -> -. C e. ( R L Q ) )
124 123 adantr 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) -> -. C e. ( R L Q ) )
125 simpr 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) -> -. B e. ( R L Q ) )
126 47 ad2antrr 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) -> Q e. ( C I B ) )
127 1 18 2 110 117 119 120 124 125 126 islnoppd 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) -> C { <. a , b >. | ( ( a e. ( P \ ( R L Q ) ) /\ b e. ( P \ ( R L Q ) ) ) /\ E. t e. ( R L Q ) t e. ( a I b ) ) } B )
128 1 2 3 86 87 88 91 tglinerflx1 
 |-  ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) -> R e. ( R L Q ) )
129 128 adantr 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) -> R e. ( R L Q ) )
130 26 ad2antrr 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) -> C e. ( R I A ) )
131 1 2 3 86 89 87 88 121 ncolne1 
 |-  ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) -> C =/= R )
132 131 adantr 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) -> C =/= R )
133 1 18 2 111 112 117 118 130 132 tgbtwnne 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) -> R =/= A )
134 1 2 116 112 118 117 111 118 130 133 132 btwnhl1 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) -> C ( ( hlG ` G ) ` R ) A )
135 1 18 2 110 3 115 111 116 117 118 119 127 129 134 opphl 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) -> A { <. a , b >. | ( ( a e. ( P \ ( R L Q ) ) /\ b e. ( P \ ( R L Q ) ) ) /\ E. t e. ( R L Q ) t e. ( a I b ) ) } B )
136 1 18 2 110 118 119 islnopp 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) -> ( A { <. a , b >. | ( ( a e. ( P \ ( R L Q ) ) /\ b e. ( P \ ( R L Q ) ) ) /\ E. t e. ( R L Q ) t e. ( a I b ) ) } B <-> ( ( -. A e. ( R L Q ) /\ -. B e. ( R L Q ) ) /\ E. x e. ( R L Q ) x e. ( A I B ) ) ) )
137 135 136 mpbid 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) -> ( ( -. A e. ( R L Q ) /\ -. B e. ( R L Q ) ) /\ E. x e. ( R L Q ) x e. ( A I B ) ) )
138 137 simprd 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) -> E. x e. ( R L Q ) x e. ( A I B ) )
139 111 ad2antrr 
 |-  ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) -> G e. TarskiG )
140 115 ad2antrr 
 |-  ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) -> ( R L Q ) e. ran L )
141 simplr 
 |-  ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) -> x e. ( R L Q ) )
142 1 3 2 139 140 141 tglnpt 
 |-  ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) -> x e. P )
143 simpr 
 |-  ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) -> x e. ( A I B ) )
144 139 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) /\ t e. P ) /\ ( t e. ( x I R ) /\ t e. ( C I B ) ) ) -> G e. TarskiG )
145 87 ad3antrrr 
 |-  ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) -> R e. P )
146 145 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) /\ t e. P ) /\ ( t e. ( x I R ) /\ t e. ( C I B ) ) ) -> R e. P )
147 88 ad5antr 
 |-  ( ( ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) /\ t e. P ) /\ ( t e. ( x I R ) /\ t e. ( C I B ) ) ) -> Q e. P )
148 117 ad2antrr 
 |-  ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) -> C e. P )
149 148 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) /\ t e. P ) /\ ( t e. ( x I R ) /\ t e. ( C I B ) ) ) -> C e. P )
150 90 ad5antr 
 |-  ( ( ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) /\ t e. P ) /\ ( t e. ( x I R ) /\ t e. ( C I B ) ) ) -> -. ( R e. ( Q L C ) \/ Q = C ) )
151 simplr 
 |-  ( ( ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) /\ t e. P ) /\ ( t e. ( x I R ) /\ t e. ( C I B ) ) ) -> t e. P )
152 114 ad4antr 
 |-  ( ( ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) /\ t e. P ) /\ ( t e. ( x I R ) /\ t e. ( C I B ) ) ) -> R =/= Q )
153 142 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) /\ t e. P ) /\ ( t e. ( x I R ) /\ t e. ( C I B ) ) ) -> x e. P )
154 91 necomd 
 |-  ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) -> Q =/= R )
155 154 ad5antr 
 |-  ( ( ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) /\ t e. P ) /\ ( t e. ( x I R ) /\ t e. ( C I B ) ) ) -> Q =/= R )
156 141 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) /\ t e. P ) /\ ( t e. ( x I R ) /\ t e. ( C I B ) ) ) -> x e. ( R L Q ) )
157 1 2 3 144 147 146 153 155 156 lncom 
 |-  ( ( ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) /\ t e. P ) /\ ( t e. ( x I R ) /\ t e. ( C I B ) ) ) -> x e. ( Q L R ) )
158 simprl 
 |-  ( ( ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) /\ t e. P ) /\ ( t e. ( x I R ) /\ t e. ( C I B ) ) ) -> t e. ( x I R ) )
159 1 2 3 144 153 147 146 151 157 158 coltr3 
 |-  ( ( ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) /\ t e. P ) /\ ( t e. ( x I R ) /\ t e. ( C I B ) ) ) -> t e. ( Q L R ) )
160 1 2 3 144 146 147 151 152 159 lncom 
 |-  ( ( ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) /\ t e. P ) /\ ( t e. ( x I R ) /\ t e. ( C I B ) ) ) -> t e. ( R L Q ) )
161 92 ad5antr 
 |-  ( ( ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) /\ t e. P ) /\ ( t e. ( x I R ) /\ t e. ( C I B ) ) ) -> Q e. ( R L Q ) )
162 96 ad5antr 
 |-  ( ( ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) /\ t e. P ) /\ ( t e. ( x I R ) /\ t e. ( C I B ) ) ) -> C =/= Q )
163 119 ad2antrr 
 |-  ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) -> B e. P )
164 163 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) /\ t e. P ) /\ ( t e. ( x I R ) /\ t e. ( C I B ) ) ) -> B e. P )
165 6 adantr 
 |-  ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) -> B e. P )
166 96 necomd 
 |-  ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) -> Q =/= C )
167 11 adantr 
 |-  ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) -> Q e. ( B I C ) )
168 1 2 3 86 88 89 165 166 167 btwnlng2 
 |-  ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) -> B e. ( Q L C ) )
169 168 ad5antr 
 |-  ( ( ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) /\ t e. P ) /\ ( t e. ( x I R ) /\ t e. ( C I B ) ) ) -> B e. ( Q L C ) )
170 simprr 
 |-  ( ( ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) /\ t e. P ) /\ ( t e. ( x I R ) /\ t e. ( C I B ) ) ) -> t e. ( C I B ) )
171 1 18 2 144 149 151 164 170 tgbtwncom 
 |-  ( ( ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) /\ t e. P ) /\ ( t e. ( x I R ) /\ t e. ( C I B ) ) ) -> t e. ( B I C ) )
172 1 2 3 144 164 147 149 151 169 171 coltr3 
 |-  ( ( ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) /\ t e. P ) /\ ( t e. ( x I R ) /\ t e. ( C I B ) ) ) -> t e. ( Q L C ) )
173 1 2 3 144 149 147 151 162 172 lncom 
 |-  ( ( ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) /\ t e. P ) /\ ( t e. ( x I R ) /\ t e. ( C I B ) ) ) -> t e. ( C L Q ) )
174 1 2 3 86 89 88 96 tglinerflx2 
 |-  ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) -> Q e. ( C L Q ) )
175 174 ad5antr 
 |-  ( ( ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) /\ t e. P ) /\ ( t e. ( x I R ) /\ t e. ( C I B ) ) ) -> Q e. ( C L Q ) )
176 1 2 3 144 146 147 149 147 150 160 161 173 175 tglineinteq 
 |-  ( ( ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) /\ t e. P ) /\ ( t e. ( x I R ) /\ t e. ( C I B ) ) ) -> t = Q )
177 1 18 2 144 153 151 146 158 tgbtwncom 
 |-  ( ( ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) /\ t e. P ) /\ ( t e. ( x I R ) /\ t e. ( C I B ) ) ) -> t e. ( R I x ) )
178 176 177 eqeltrrd 
 |-  ( ( ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) /\ t e. P ) /\ ( t e. ( x I R ) /\ t e. ( C I B ) ) ) -> Q e. ( R I x ) )
179 118 ad2antrr 
 |-  ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) -> A e. P )
180 1 18 2 139 179 142 163 143 tgbtwncom 
 |-  ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) -> x e. ( B I A ) )
181 26 ad4antr 
 |-  ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) -> C e. ( R I A ) )
182 1 18 2 139 163 145 179 142 148 180 181 axtgpasch 
 |-  ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) -> E. t e. P ( t e. ( x I R ) /\ t e. ( C I B ) ) )
183 178 182 r19.29a 
 |-  ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) -> Q e. ( R I x ) )
184 142 143 183 jca32 
 |-  ( ( ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) /\ x e. ( R L Q ) ) /\ x e. ( A I B ) ) -> ( x e. P /\ ( x e. ( A I B ) /\ Q e. ( R I x ) ) ) )
185 184 expl 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) -> ( ( x e. ( R L Q ) /\ x e. ( A I B ) ) -> ( x e. P /\ ( x e. ( A I B ) /\ Q e. ( R I x ) ) ) ) )
186 185 reximdv2 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) -> ( E. x e. ( R L Q ) x e. ( A I B ) -> E. x e. P ( x e. ( A I B ) /\ Q e. ( R I x ) ) ) )
187 138 186 mpd 
 |-  ( ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) /\ -. B e. ( R L Q ) ) -> E. x e. P ( x e. ( A I B ) /\ Q e. ( R I x ) ) )
188 106 187 pm2.61dan 
 |-  ( ( ph /\ -. ( R e. ( Q L C ) \/ Q = C ) ) -> E. x e. P ( x e. ( A I B ) /\ Q e. ( R I x ) ) )
189 76 188 pm2.61dan 
 |-  ( ph -> E. x e. P ( x e. ( A I B ) /\ Q e. ( R I x ) ) )