Metamath Proof Explorer

Theorem morleylemrneab

Description: Lemma for morley . (Contributed by TA and SS, 4-Jun-2026)

Ref Expression
Hypotheses morley.s 
|- S = ( Base ` G )
morley.l 
|- L = ( LineG ` G )
morley.e 
|- .~ = ( cgrA ` G )
morley.g 
|- ( ph -> G e. TarskiG )
morley.a 
|- ( ph -> A e. S )
morley.b 
|- ( ph -> B e. S )
morley.c 
|- ( ph -> C e. S )
morley.p 
|- ( ph -> P e. S )
morley.q 
|- ( ph -> Q e. S )
morley.r 
|- ( ph -> R e. S )
morley.0 
|- ( ph -> -. ( C e. ( A L B ) \/ A = B ) )
morley.1 
|- ( ph -> <" C A Q "> .~ <" Q A R "> )
morley.2 
|- ( ph -> <" R A B "> .~ <" Q A R "> )
morley.3 
|- ( ph -> <" A B R "> .~ <" R B P "> )
morley.4 
|- ( ph -> <" P B C "> .~ <" R B P "> )
morley.5 
|- ( ph -> <" B C P "> .~ <" P C Q "> )
morley.6 
|- ( ph -> <" Q C A "> .~ <" P C Q "> )
Assertion morleylemrneab 
|- ( ph -> -. R e. ( A L B ) )

Proof

Step Hyp Ref Expression
1 morley.s 
 |-  S = ( Base ` G )
2 morley.l 
 |-  L = ( LineG ` G )
3 morley.e 
 |-  .~ = ( cgrA ` G )
4 morley.g 
 |-  ( ph -> G e. TarskiG )
5 morley.a 
 |-  ( ph -> A e. S )
6 morley.b 
 |-  ( ph -> B e. S )
7 morley.c 
 |-  ( ph -> C e. S )
8 morley.p 
 |-  ( ph -> P e. S )
9 morley.q 
 |-  ( ph -> Q e. S )
10 morley.r 
 |-  ( ph -> R e. S )
11 morley.0 
 |-  ( ph -> -. ( C e. ( A L B ) \/ A = B ) )
12 morley.1 
 |-  ( ph -> <" C A Q "> .~ <" Q A R "> )
13 morley.2 
 |-  ( ph -> <" R A B "> .~ <" Q A R "> )
14 morley.3 
 |-  ( ph -> <" A B R "> .~ <" R B P "> )
15 morley.4 
 |-  ( ph -> <" P B C "> .~ <" R B P "> )
16 morley.5 
 |-  ( ph -> <" B C P "> .~ <" P C Q "> )
17 morley.6 
 |-  ( ph -> <" Q C A "> .~ <" P C Q "> )
18 ioran 
 |-  ( -. ( C e. ( A L B ) \/ A = B ) <-> ( -. C e. ( A L B ) /\ -. A = B ) )
19 11 18 sylib 
 |-  ( ph -> ( -. C e. ( A L B ) /\ -. A = B ) )
20 19 simpld 
 |-  ( ph -> -. C e. ( A L B ) )
21 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
22 4 ad2antrr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ R e. ( A ( Itv ` G ) B ) ) -> G e. TarskiG )
23 5 ad2antrr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ R e. ( A ( Itv ` G ) B ) ) -> A e. S )
24 6 ad2antrr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ R e. ( A ( Itv ` G ) B ) ) -> B e. S )
25 19 simprd 
 |-  ( ph -> -. A = B )
26 25 adantr 
 |-  ( ( ph /\ R e. ( A L B ) ) -> -. A = B )
27 26 neqned 
 |-  ( ( ph /\ R e. ( A L B ) ) -> A =/= B )
28 27 adantr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ R e. ( A ( Itv ` G ) B ) ) -> A =/= B )
29 9 ad2antrr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ R e. ( A ( Itv ` G ) B ) ) -> Q e. S )
30 eqid 
 |-  ( hlG ` G ) = ( hlG ` G )
31 10 ad2antrr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ R e. ( A ( Itv ` G ) B ) ) -> R e. S )
32 13 adantr 
 |-  ( ( ph /\ R e. ( A L B ) ) -> <" R A B "> .~ <" Q A R "> )
33 3 breqi 
 |-  ( <" R A B "> .~ <" Q A R "> <-> <" R A B "> ( cgrA ` G ) <" Q A R "> )
34 32 33 sylib 
 |-  ( ( ph /\ R e. ( A L B ) ) -> <" R A B "> ( cgrA ` G ) <" Q A R "> )
35 34 adantr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ R e. ( A ( Itv ` G ) B ) ) -> <" R A B "> ( cgrA ` G ) <" Q A R "> )
36 1 21 30 22 31 23 24 29 23 31 35 cgrane3 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ R e. ( A ( Itv ` G ) B ) ) -> A =/= Q )
37 36 necomd 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ R e. ( A ( Itv ` G ) B ) ) -> Q =/= A )
38 1 21 30 22 31 23 24 29 23 31 35 cgrane4 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ R e. ( A ( Itv ` G ) B ) ) -> A =/= R )
39 simpr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ R e. ( A ( Itv ` G ) B ) ) -> R e. ( A ( Itv ` G ) B ) )
40 1 21 22 31 23 24 29 23 31 35 39 cgranbtwn 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ R e. ( A ( Itv ` G ) B ) ) -> ( Q e. ( A ( Itv ` G ) R ) \/ R e. ( A ( Itv ` G ) Q ) ) )
41 1 21 2 22 23 31 29 38 40 btwnlng13 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ R e. ( A ( Itv ` G ) B ) ) -> Q e. ( A L R ) )
42 28 necomd 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ R e. ( A ( Itv ` G ) B ) ) -> B =/= A )
43 1 21 2 22 23 31 24 38 39 btwnlng3 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ R e. ( A ( Itv ` G ) B ) ) -> B e. ( A L R ) )
44 1 21 2 22 23 31 38 24 42 43 tglineelsb2 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ R e. ( A ( Itv ` G ) B ) ) -> ( A L R ) = ( A L B ) )
45 41 44 eleqtrd 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ R e. ( A ( Itv ` G ) B ) ) -> Q e. ( A L B ) )
46 7 ad2antrr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ R e. ( A ( Itv ` G ) B ) ) -> C e. S )
47 4 adantr 
 |-  ( ( ph /\ R e. ( A L B ) ) -> G e. TarskiG )
48 7 adantr 
 |-  ( ( ph /\ R e. ( A L B ) ) -> C e. S )
49 5 adantr 
 |-  ( ( ph /\ R e. ( A L B ) ) -> A e. S )
50 9 adantr 
 |-  ( ( ph /\ R e. ( A L B ) ) -> Q e. S )
51 10 adantr 
 |-  ( ( ph /\ R e. ( A L B ) ) -> R e. S )
52 6 adantr 
 |-  ( ( ph /\ R e. ( A L B ) ) -> B e. S )
53 12 adantr 
 |-  ( ( ph /\ R e. ( A L B ) ) -> <" C A Q "> .~ <" Q A R "> )
54 3 breqi 
 |-  ( <" C A Q "> .~ <" Q A R "> <-> <" C A Q "> ( cgrA ` G ) <" Q A R "> )
55 53 54 sylib 
 |-  ( ( ph /\ R e. ( A L B ) ) -> <" C A Q "> ( cgrA ` G ) <" Q A R "> )
56 1 21 47 30 51 49 52 50 49 51 34 cgracom 
 |-  ( ( ph /\ R e. ( A L B ) ) -> <" Q A R "> ( cgrA ` G ) <" R A B "> )
57 1 21 47 30 48 49 50 50 49 51 55 51 49 52 56 cgratr 
 |-  ( ( ph /\ R e. ( A L B ) ) -> <" C A Q "> ( cgrA ` G ) <" R A B "> )
58 1 21 47 30 48 49 50 51 49 52 57 cgracom 
 |-  ( ( ph /\ R e. ( A L B ) ) -> <" R A B "> ( cgrA ` G ) <" C A Q "> )
59 58 adantr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ R e. ( A ( Itv ` G ) B ) ) -> <" R A B "> ( cgrA ` G ) <" C A Q "> )
60 1 21 22 31 23 24 46 23 29 59 39 cgranbtwn 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ R e. ( A ( Itv ` G ) B ) ) -> ( C e. ( A ( Itv ` G ) Q ) \/ Q e. ( A ( Itv ` G ) C ) ) )
61 1 21 2 22 23 29 46 36 60 btwnlng13 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ R e. ( A ( Itv ` G ) B ) ) -> C e. ( A L Q ) )
62 1 21 2 22 23 24 28 29 37 45 46 61 tglineeltr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ R e. ( A ( Itv ` G ) B ) ) -> C e. ( A L B ) )
63 4 ad2antrr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ A e. ( R ( Itv ` G ) B ) ) -> G e. TarskiG )
64 5 ad2antrr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ A e. ( R ( Itv ` G ) B ) ) -> A e. S )
65 6 ad2antrr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ A e. ( R ( Itv ` G ) B ) ) -> B e. S )
66 27 adantr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ A e. ( R ( Itv ` G ) B ) ) -> A =/= B )
67 9 ad2antrr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ A e. ( R ( Itv ` G ) B ) ) -> Q e. S )
68 1 21 30 47 48 49 50 50 49 51 55 cgrane2 
 |-  ( ( ph /\ R e. ( A L B ) ) -> A =/= Q )
69 68 adantr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ A e. ( R ( Itv ` G ) B ) ) -> A =/= Q )
70 69 necomd 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ A e. ( R ( Itv ` G ) B ) ) -> Q =/= A )
71 10 ad2antrr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ A e. ( R ( Itv ` G ) B ) ) -> R e. S )
72 1 21 30 47 51 49 52 50 49 51 34 cgrane4 
 |-  ( ( ph /\ R e. ( A L B ) ) -> A =/= R )
73 72 adantr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ A e. ( R ( Itv ` G ) B ) ) -> A =/= R )
74 eqid 
 |-  ( dist ` G ) = ( dist ` G )
75 34 adantr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ A e. ( R ( Itv ` G ) B ) ) -> <" R A B "> ( cgrA ` G ) <" Q A R "> )
76 simpr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ A e. ( R ( Itv ` G ) B ) ) -> A e. ( R ( Itv ` G ) B ) )
77 1 21 74 63 71 64 65 67 64 71 75 76 cgrabtwn 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ A e. ( R ( Itv ` G ) B ) ) -> A e. ( Q ( Itv ` G ) R ) )
78 1 21 2 63 64 71 67 73 77 btwnlng2 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ A e. ( R ( Itv ` G ) B ) ) -> Q e. ( A L R ) )
79 72 necomd 
 |-  ( ( ph /\ R e. ( A L B ) ) -> R =/= A )
80 simpr 
 |-  ( ( ph /\ R e. ( A L B ) ) -> R e. ( A L B ) )
81 1 21 2 47 49 52 27 51 79 80 tglineelsb2 
 |-  ( ( ph /\ R e. ( A L B ) ) -> ( A L B ) = ( A L R ) )
82 81 adantr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ A e. ( R ( Itv ` G ) B ) ) -> ( A L B ) = ( A L R ) )
83 78 82 eleqtrrd 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ A e. ( R ( Itv ` G ) B ) ) -> Q e. ( A L B ) )
84 7 ad2antrr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ A e. ( R ( Itv ` G ) B ) ) -> C e. S )
85 58 adantr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ A e. ( R ( Itv ` G ) B ) ) -> <" R A B "> ( cgrA ` G ) <" C A Q "> )
86 1 21 74 63 71 64 65 84 64 67 85 76 cgrabtwn 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ A e. ( R ( Itv ` G ) B ) ) -> A e. ( C ( Itv ` G ) Q ) )
87 1 21 2 63 64 67 84 69 86 btwnlng2 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ A e. ( R ( Itv ` G ) B ) ) -> C e. ( A L Q ) )
88 1 21 2 63 64 65 66 67 70 83 84 87 tglineeltr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ A e. ( R ( Itv ` G ) B ) ) -> C e. ( A L B ) )
89 4 ad2antrr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ B e. ( A ( Itv ` G ) R ) ) -> G e. TarskiG )
90 5 ad2antrr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ B e. ( A ( Itv ` G ) R ) ) -> A e. S )
91 6 ad2antrr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ B e. ( A ( Itv ` G ) R ) ) -> B e. S )
92 27 adantr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ B e. ( A ( Itv ` G ) R ) ) -> A =/= B )
93 9 ad2antrr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ B e. ( A ( Itv ` G ) R ) ) -> Q e. S )
94 68 adantr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ B e. ( A ( Itv ` G ) R ) ) -> A =/= Q )
95 94 necomd 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ B e. ( A ( Itv ` G ) R ) ) -> Q =/= A )
96 10 ad2antrr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ B e. ( A ( Itv ` G ) R ) ) -> R e. S )
97 72 adantr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ B e. ( A ( Itv ` G ) R ) ) -> A =/= R )
98 92 necomd 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ B e. ( A ( Itv ` G ) R ) ) -> B =/= A )
99 1 21 89 30 91 90 96 98 97 cgraswap 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ B e. ( A ( Itv ` G ) R ) ) -> <" B A R "> ( cgrA ` G ) <" R A B "> )
100 34 adantr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ B e. ( A ( Itv ` G ) R ) ) -> <" R A B "> ( cgrA ` G ) <" Q A R "> )
101 1 21 89 30 91 90 96 96 90 91 99 93 90 96 100 cgratr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ B e. ( A ( Itv ` G ) R ) ) -> <" B A R "> ( cgrA ` G ) <" Q A R "> )
102 simpr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ B e. ( A ( Itv ` G ) R ) ) -> B e. ( A ( Itv ` G ) R ) )
103 1 21 89 91 90 96 93 90 96 101 102 cgranbtwn 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ B e. ( A ( Itv ` G ) R ) ) -> ( Q e. ( A ( Itv ` G ) R ) \/ R e. ( A ( Itv ` G ) Q ) ) )
104 1 21 2 89 90 96 93 97 103 btwnlng13 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ B e. ( A ( Itv ` G ) R ) ) -> Q e. ( A L R ) )
105 81 adantr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ B e. ( A ( Itv ` G ) R ) ) -> ( A L B ) = ( A L R ) )
106 104 105 eleqtrrd 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ B e. ( A ( Itv ` G ) R ) ) -> Q e. ( A L B ) )
107 7 ad2antrr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ B e. ( A ( Itv ` G ) R ) ) -> C e. S )
108 58 adantr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ B e. ( A ( Itv ` G ) R ) ) -> <" R A B "> ( cgrA ` G ) <" C A Q "> )
109 1 21 89 30 91 90 96 96 90 91 99 107 90 93 108 cgratr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ B e. ( A ( Itv ` G ) R ) ) -> <" B A R "> ( cgrA ` G ) <" C A Q "> )
110 1 21 89 91 90 96 107 90 93 109 102 cgranbtwn 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ B e. ( A ( Itv ` G ) R ) ) -> ( C e. ( A ( Itv ` G ) Q ) \/ Q e. ( A ( Itv ` G ) C ) ) )
111 1 21 2 89 90 93 107 94 110 btwnlng13 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ B e. ( A ( Itv ` G ) R ) ) -> C e. ( A L Q ) )
112 1 21 2 89 90 91 92 93 95 106 107 111 tglineeltr 
 |-  ( ( ( ph /\ R e. ( A L B ) ) /\ B e. ( A ( Itv ` G ) R ) ) -> C e. ( A L B ) )
113 1 2 21 47 49 52 27 51 tgellng 
 |-  ( ( ph /\ R e. ( A L B ) ) -> ( R e. ( A L B ) <-> ( R e. ( A ( Itv ` G ) B ) \/ A e. ( R ( Itv ` G ) B ) \/ B e. ( A ( Itv ` G ) R ) ) ) )
114 80 113 mpbid 
 |-  ( ( ph /\ R e. ( A L B ) ) -> ( R e. ( A ( Itv ` G ) B ) \/ A e. ( R ( Itv ` G ) B ) \/ B e. ( A ( Itv ` G ) R ) ) )
115 62 88 112 114 mpjao3dan 
 |-  ( ( ph /\ R e. ( A L B ) ) -> C e. ( A L B ) )
116 20 115 mtand 
 |-  ( ph -> -. R e. ( A L B ) )