Metamath Proof Explorer

Theorem morleylemrneab

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

Ref Expression
Hypotheses morley.s ⊢ 𝑆 = ( Base ‘ 𝐺 )
morley.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
morley.e ⊢ ∼ = ( cgrA ‘ 𝐺 )
morley.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
morley.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
morley.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
morley.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑆 )
morley.p ⊢ ( 𝜑 → 𝑃 ∈ 𝑆 )
morley.q ⊢ ( 𝜑 → 𝑄 ∈ 𝑆 )
morley.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑆 )
morley.0 ⊢ ( 𝜑 → ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
morley.1 ⊢ ( 𝜑 → ⟨“ 𝐶 𝐴 𝑄 ”⟩ ∼ ⟨“ 𝑄 𝐴 𝑅 ”⟩ )
morley.2 ⊢ ( 𝜑 → ⟨“ 𝑅 𝐴 𝐵 ”⟩ ∼ ⟨“ 𝑄 𝐴 𝑅 ”⟩ )
morley.3 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝑅 ”⟩ ∼ ⟨“ 𝑅 𝐵 𝑃 ”⟩ )
morley.4 ⊢ ( 𝜑 → ⟨“ 𝑃 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝑅 𝐵 𝑃 ”⟩ )
morley.5 ⊢ ( 𝜑 → ⟨“ 𝐵 𝐶 𝑃 ”⟩ ∼ ⟨“ 𝑃 𝐶 𝑄 ”⟩ )
morley.6 ⊢ ( 𝜑 → ⟨“ 𝑄 𝐶 𝐴 ”⟩ ∼ ⟨“ 𝑃 𝐶 𝑄 ”⟩ )
Assertion morleylemrneab ( 𝜑 → ¬ 𝑅 ∈ ( 𝐴 𝐿 𝐵 ) )

Proof

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