Metamath Proof Explorer

Theorem mideulem2

Description: Lemma for opphllem , which is itself used for mideu . (Contributed by Thierry Arnoux, 19-Feb-2020)

Ref Expression
Hypotheses colperpex.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
colperpex.d ⊢ − = ( dist ‘ 𝐺 )
colperpex.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
colperpex.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
colperpex.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
mideu.s ⊢ 𝑆 = ( pInvG ‘ 𝐺 )
mideu.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
mideu.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
mideulem.1 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
mideulem.2 ⊢ ( 𝜑 → 𝑄 ∈ 𝑃 )
mideulem.3 ⊢ ( 𝜑 → 𝑂 ∈ 𝑃 )
mideulem.4 ⊢ ( 𝜑 → 𝑇 ∈ 𝑃 )
mideulem.5 ⊢ ( 𝜑 → ( 𝐴 𝐿 𝐵 ) ( ⟂G ‘ 𝐺 ) ( 𝑄 𝐿 𝐵 ) )
mideulem.6 ⊢ ( 𝜑 → ( 𝐴 𝐿 𝐵 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑂 ) )
mideulem.7 ⊢ ( 𝜑 → 𝑇 ∈ ( 𝐴 𝐿 𝐵 ) )
mideulem.8 ⊢ ( 𝜑 → 𝑇 ∈ ( 𝑄 𝐼 𝑂 ) )
opphllem.1 ⊢ ( 𝜑 → 𝑅 ∈ 𝑃 )
opphllem.2 ⊢ ( 𝜑 → 𝑅 ∈ ( 𝐵 𝐼 𝑄 ) )
opphllem.3 ⊢ ( 𝜑 → ( 𝐴 − 𝑂 ) = ( 𝐵 − 𝑅 ) )
mideulem2.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
mideulem2.2 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑇 𝐼 𝐵 ) )
mideulem2.3 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑅 𝐼 𝑂 ) )
mideulem2.4 ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
mideulem2.5 ⊢ ( 𝜑 → 𝑋 ∈ ( ( ( 𝑆 ‘ 𝐴 ) ‘ 𝑂 ) 𝐼 𝑍 ) )
mideulem2.6 ⊢ ( 𝜑 → ( 𝑋 − 𝑍 ) = ( 𝑋 − 𝑅 ) )
mideulem2.7 ⊢ ( 𝜑 → 𝑀 ∈ 𝑃 )
mideulem2.8 ⊢ ( 𝜑 → 𝑅 = ( ( 𝑆 ‘ 𝑀 ) ‘ 𝑍 ) )
Assertion mideulem2 ( 𝜑 → 𝐵 = 𝑀 )

Proof

Step Hyp Ref Expression
1 colperpex.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 colperpex.d ⊢ − = ( dist ‘ 𝐺 )
3 colperpex.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 colperpex.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
5 colperpex.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6 mideu.s ⊢ 𝑆 = ( pInvG ‘ 𝐺 )
7 mideu.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
8 mideu.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
9 mideulem.1 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
10 mideulem.2 ⊢ ( 𝜑 → 𝑄 ∈ 𝑃 )
11 mideulem.3 ⊢ ( 𝜑 → 𝑂 ∈ 𝑃 )
12 mideulem.4 ⊢ ( 𝜑 → 𝑇 ∈ 𝑃 )
13 mideulem.5 ⊢ ( 𝜑 → ( 𝐴 𝐿 𝐵 ) ( ⟂G ‘ 𝐺 ) ( 𝑄 𝐿 𝐵 ) )
14 mideulem.6 ⊢ ( 𝜑 → ( 𝐴 𝐿 𝐵 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑂 ) )
15 mideulem.7 ⊢ ( 𝜑 → 𝑇 ∈ ( 𝐴 𝐿 𝐵 ) )
16 mideulem.8 ⊢ ( 𝜑 → 𝑇 ∈ ( 𝑄 𝐼 𝑂 ) )
17 opphllem.1 ⊢ ( 𝜑 → 𝑅 ∈ 𝑃 )
18 opphllem.2 ⊢ ( 𝜑 → 𝑅 ∈ ( 𝐵 𝐼 𝑄 ) )
19 opphllem.3 ⊢ ( 𝜑 → ( 𝐴 − 𝑂 ) = ( 𝐵 − 𝑅 ) )
20 mideulem2.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
21 mideulem2.2 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑇 𝐼 𝐵 ) )
22 mideulem2.3 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑅 𝐼 𝑂 ) )
23 mideulem2.4 ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
24 mideulem2.5 ⊢ ( 𝜑 → 𝑋 ∈ ( ( ( 𝑆 ‘ 𝐴 ) ‘ 𝑂 ) 𝐼 𝑍 ) )
25 mideulem2.6 ⊢ ( 𝜑 → ( 𝑋 − 𝑍 ) = ( 𝑋 − 𝑅 ) )
26 mideulem2.7 ⊢ ( 𝜑 → 𝑀 ∈ 𝑃 )
27 mideulem2.8 ⊢ ( 𝜑 → 𝑅 = ( ( 𝑆 ‘ 𝑀 ) ‘ 𝑍 ) )
28 oveq2 ⊢ ( 𝑦 = 𝐵 → ( 𝑅 𝐿 𝑦 ) = ( 𝑅 𝐿 𝐵 ) )
29 28 breq1d ⊢ ( 𝑦 = 𝐵 → ( ( 𝑅 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ↔ ( 𝑅 𝐿 𝐵 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) )
30 oveq2 ⊢ ( 𝑦 = 𝑀 → ( 𝑅 𝐿 𝑦 ) = ( 𝑅 𝐿 𝑀 ) )
31 30 breq1d ⊢ ( 𝑦 = 𝑀 → ( ( 𝑅 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ↔ ( 𝑅 𝐿 𝑀 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) )
32 1 3 4 5 7 8 9 tgelrnln ⊢ ( 𝜑 → ( 𝐴 𝐿 𝐵 ) ∈ ran 𝐿 )
33 9 adantr ⊢ ( ( 𝜑 ∧ 𝑅 ∈ ( 𝐴 𝐿 𝐵 ) ) → 𝐴 ≠ 𝐵 )
34 33 neneqd ⊢ ( ( 𝜑 ∧ 𝑅 ∈ ( 𝐴 𝐿 𝐵 ) ) → ¬ 𝐴 = 𝐵 )
35 4 5 14 perpln2 ⊢ ( 𝜑 → ( 𝐴 𝐿 𝑂 ) ∈ ran 𝐿 )
36 1 3 4 5 7 11 35 tglnne ⊢ ( 𝜑 → 𝐴 ≠ 𝑂 )
37 1 2 3 5 7 11 8 17 19 36 tgcgrneq ⊢ ( 𝜑 → 𝐵 ≠ 𝑅 )
38 37 adantr ⊢ ( ( 𝜑 ∧ 𝑅 ∈ ( 𝐴 𝐿 𝐵 ) ) → 𝐵 ≠ 𝑅 )
39 38 necomd ⊢ ( ( 𝜑 ∧ 𝑅 ∈ ( 𝐴 𝐿 𝐵 ) ) → 𝑅 ≠ 𝐵 )
40 39 neneqd ⊢ ( ( 𝜑 ∧ 𝑅 ∈ ( 𝐴 𝐿 𝐵 ) ) → ¬ 𝑅 = 𝐵 )
41 34 40 jca ⊢ ( ( 𝜑 ∧ 𝑅 ∈ ( 𝐴 𝐿 𝐵 ) ) → ( ¬ 𝐴 = 𝐵 ∧ ¬ 𝑅 = 𝐵 ) )
42 5 adantr ⊢ ( ( 𝜑 ∧ 𝑅 ∈ ( 𝐴 𝐿 𝐵 ) ) → 𝐺 ∈ TarskiG )
43 7 adantr ⊢ ( ( 𝜑 ∧ 𝑅 ∈ ( 𝐴 𝐿 𝐵 ) ) → 𝐴 ∈ 𝑃 )
44 8 adantr ⊢ ( ( 𝜑 ∧ 𝑅 ∈ ( 𝐴 𝐿 𝐵 ) ) → 𝐵 ∈ 𝑃 )
45 17 adantr ⊢ ( ( 𝜑 ∧ 𝑅 ∈ ( 𝐴 𝐿 𝐵 ) ) → 𝑅 ∈ 𝑃 )
46 4 5 13 perpln2 ⊢ ( 𝜑 → ( 𝑄 𝐿 𝐵 ) ∈ ran 𝐿 )
47 1 3 4 5 10 8 46 tglnne ⊢ ( 𝜑 → 𝑄 ≠ 𝐵 )
48 1 3 4 5 10 8 47 tglinerflx2 ⊢ ( 𝜑 → 𝐵 ∈ ( 𝑄 𝐿 𝐵 ) )
49 1 2 3 4 5 32 46 13 perpcom ⊢ ( 𝜑 → ( 𝑄 𝐿 𝐵 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) )
50 1 3 4 5 7 8 9 tglinecom ⊢ ( 𝜑 → ( 𝐴 𝐿 𝐵 ) = ( 𝐵 𝐿 𝐴 ) )
51 49 50 breqtrd ⊢ ( 𝜑 → ( 𝑄 𝐿 𝐵 ) ( ⟂G ‘ 𝐺 ) ( 𝐵 𝐿 𝐴 ) )
52 1 2 3 4 5 10 8 48 7 51 perprag ⊢ ( 𝜑 → ⟨“ 𝑄 𝐵 𝐴 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
53 1 4 3 5 8 17 10 18 btwncolg3 ⊢ ( 𝜑 → ( 𝑄 ∈ ( 𝐵 𝐿 𝑅 ) ∨ 𝐵 = 𝑅 ) )
54 1 2 3 4 6 5 10 8 7 17 52 47 53 ragcol ⊢ ( 𝜑 → ⟨“ 𝑅 𝐵 𝐴 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
55 1 2 3 4 6 5 17 8 7 54 ragcom ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝑅 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
56 55 adantr ⊢ ( ( 𝜑 ∧ 𝑅 ∈ ( 𝐴 𝐿 𝐵 ) ) → ⟨“ 𝐴 𝐵 𝑅 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
57 animorrl ⊢ ( ( 𝜑 ∧ 𝑅 ∈ ( 𝐴 𝐿 𝐵 ) ) → ( 𝑅 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
58 1 2 3 4 6 42 43 44 45 56 57 ragflat3 ⊢ ( ( 𝜑 ∧ 𝑅 ∈ ( 𝐴 𝐿 𝐵 ) ) → ( 𝐴 = 𝐵 ∨ 𝑅 = 𝐵 ) )
59 oran ⊢ ( ( 𝐴 = 𝐵 ∨ 𝑅 = 𝐵 ) ↔ ¬ ( ¬ 𝐴 = 𝐵 ∧ ¬ 𝑅 = 𝐵 ) )
60 58 59 sylib ⊢ ( ( 𝜑 ∧ 𝑅 ∈ ( 𝐴 𝐿 𝐵 ) ) → ¬ ( ¬ 𝐴 = 𝐵 ∧ ¬ 𝑅 = 𝐵 ) )
61 41 60 pm2.65da ⊢ ( 𝜑 → ¬ 𝑅 ∈ ( 𝐴 𝐿 𝐵 ) )
62 1 2 3 4 5 32 17 61 foot ⊢ ( 𝜑 → ∃! 𝑦 ∈ ( 𝐴 𝐿 𝐵 ) ( 𝑅 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) )
63 1 3 4 5 7 8 9 tglinerflx2 ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐿 𝐵 ) )
64 9 neneqd ⊢ ( 𝜑 → ¬ 𝐴 = 𝐵 )
65 oveq2 ⊢ ( 𝑦 = 𝐴 → ( 𝑅 𝐿 𝑦 ) = ( 𝑅 𝐿 𝐴 ) )
66 65 breq1d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑅 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ↔ ( 𝑅 𝐿 𝐴 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) )
67 62 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐴 ) → ∃! 𝑦 ∈ ( 𝐴 𝐿 𝐵 ) ( 𝑅 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) )
68 1 3 4 5 7 8 9 tglinerflx1 ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐴 𝐿 𝐵 ) )
69 68 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐴 ) → 𝐴 ∈ ( 𝐴 𝐿 𝐵 ) )
70 63 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐴 ) → 𝐵 ∈ ( 𝐴 𝐿 𝐵 ) )
71 5 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐴 ) → 𝐺 ∈ TarskiG )
72 17 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐴 ) → 𝑅 ∈ 𝑃 )
73 7 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐴 ) → 𝐴 ∈ 𝑃 )
74 61 64 jca ⊢ ( 𝜑 → ( ¬ 𝑅 ∈ ( 𝐴 𝐿 𝐵 ) ∧ ¬ 𝐴 = 𝐵 ) )
75 pm4.56 ⊢ ( ( ¬ 𝑅 ∈ ( 𝐴 𝐿 𝐵 ) ∧ ¬ 𝐴 = 𝐵 ) ↔ ¬ ( 𝑅 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
76 74 75 sylib ⊢ ( 𝜑 → ¬ ( 𝑅 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
77 1 3 4 5 17 7 8 76 ncolne1 ⊢ ( 𝜑 → 𝑅 ≠ 𝐴 )
78 77 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐴 ) → 𝑅 ≠ 𝐴 )
79 1 3 4 71 72 73 78 tglinecom ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐴 ) → ( 𝑅 𝐿 𝐴 ) = ( 𝐴 𝐿 𝑅 ) )
80 78 necomd ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐴 ) → 𝐴 ≠ 𝑅 )
81 11 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐴 ) → 𝑂 ∈ 𝑃 )
82 36 necomd ⊢ ( 𝜑 → 𝑂 ≠ 𝐴 )
83 82 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐴 ) → 𝑂 ≠ 𝐴 )
84 20 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐴 ) → 𝑋 ∈ 𝑃 )
85 simpr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐴 ) → 𝑋 = 𝐴 )
86 85 80 eqnetrd ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐴 ) → 𝑋 ≠ 𝑅 )
87 1 2 3 5 17 20 11 22 tgbtwncom ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑂 𝐼 𝑅 ) )
88 1 3 4 5 12 7 8 20 15 21 coltr3 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 𝐿 𝐵 ) )
89 9 necomd ⊢ ( 𝜑 → 𝐵 ≠ 𝐴 )
90 89 neneqd ⊢ ( 𝜑 → ¬ 𝐵 = 𝐴 )
91 90 adantr ⊢ ( ( 𝜑 ∧ 𝑂 ∈ ( 𝐵 𝐿 𝐴 ) ) → ¬ 𝐵 = 𝐴 )
92 82 neneqd ⊢ ( 𝜑 → ¬ 𝑂 = 𝐴 )
93 92 adantr ⊢ ( ( 𝜑 ∧ 𝑂 ∈ ( 𝐵 𝐿 𝐴 ) ) → ¬ 𝑂 = 𝐴 )
94 91 93 jca ⊢ ( ( 𝜑 ∧ 𝑂 ∈ ( 𝐵 𝐿 𝐴 ) ) → ( ¬ 𝐵 = 𝐴 ∧ ¬ 𝑂 = 𝐴 ) )
95 5 adantr ⊢ ( ( 𝜑 ∧ 𝑂 ∈ ( 𝐵 𝐿 𝐴 ) ) → 𝐺 ∈ TarskiG )
96 8 adantr ⊢ ( ( 𝜑 ∧ 𝑂 ∈ ( 𝐵 𝐿 𝐴 ) ) → 𝐵 ∈ 𝑃 )
97 7 adantr ⊢ ( ( 𝜑 ∧ 𝑂 ∈ ( 𝐵 𝐿 𝐴 ) ) → 𝐴 ∈ 𝑃 )
98 11 adantr ⊢ ( ( 𝜑 ∧ 𝑂 ∈ ( 𝐵 𝐿 𝐴 ) ) → 𝑂 ∈ 𝑃 )
99 1 3 4 5 8 7 89 tglinerflx2 ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐵 𝐿 𝐴 ) )
100 50 14 eqbrtrrd ⊢ ( 𝜑 → ( 𝐵 𝐿 𝐴 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑂 ) )
101 1 2 3 4 5 8 7 99 11 100 perprag ⊢ ( 𝜑 → ⟨“ 𝐵 𝐴 𝑂 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
102 101 adantr ⊢ ( ( 𝜑 ∧ 𝑂 ∈ ( 𝐵 𝐿 𝐴 ) ) → ⟨“ 𝐵 𝐴 𝑂 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
103 animorrl ⊢ ( ( 𝜑 ∧ 𝑂 ∈ ( 𝐵 𝐿 𝐴 ) ) → ( 𝑂 ∈ ( 𝐵 𝐿 𝐴 ) ∨ 𝐵 = 𝐴 ) )
104 1 2 3 4 6 95 96 97 98 102 103 ragflat3 ⊢ ( ( 𝜑 ∧ 𝑂 ∈ ( 𝐵 𝐿 𝐴 ) ) → ( 𝐵 = 𝐴 ∨ 𝑂 = 𝐴 ) )
105 oran ⊢ ( ( 𝐵 = 𝐴 ∨ 𝑂 = 𝐴 ) ↔ ¬ ( ¬ 𝐵 = 𝐴 ∧ ¬ 𝑂 = 𝐴 ) )
106 104 105 sylib ⊢ ( ( 𝜑 ∧ 𝑂 ∈ ( 𝐵 𝐿 𝐴 ) ) → ¬ ( ¬ 𝐵 = 𝐴 ∧ ¬ 𝑂 = 𝐴 ) )
107 94 106 pm2.65da ⊢ ( 𝜑 → ¬ 𝑂 ∈ ( 𝐵 𝐿 𝐴 ) )
108 107 50 neleqtrrd ⊢ ( 𝜑 → ¬ 𝑂 ∈ ( 𝐴 𝐿 𝐵 ) )
109 nelne2 ⊢ ( ( 𝑋 ∈ ( 𝐴 𝐿 𝐵 ) ∧ ¬ 𝑂 ∈ ( 𝐴 𝐿 𝐵 ) ) → 𝑋 ≠ 𝑂 )
110 88 108 109 syl2anc ⊢ ( 𝜑 → 𝑋 ≠ 𝑂 )
111 1 2 3 5 11 20 17 87 110 tgbtwnne ⊢ ( 𝜑 → 𝑂 ≠ 𝑅 )
112 111 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐴 ) → 𝑂 ≠ 𝑅 )
113 112 necomd ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐴 ) → 𝑅 ≠ 𝑂 )
114 22 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐴 ) → 𝑋 ∈ ( 𝑅 𝐼 𝑂 ) )
115 1 3 4 71 72 81 84 113 114 btwnlng1 ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐴 ) → 𝑋 ∈ ( 𝑅 𝐿 𝑂 ) )
116 1 3 4 71 84 72 81 86 115 113 lnrot2 ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐴 ) → 𝑂 ∈ ( 𝑋 𝐿 𝑅 ) )
117 85 oveq1d ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐴 ) → ( 𝑋 𝐿 𝑅 ) = ( 𝐴 𝐿 𝑅 ) )
118 116 117 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐴 ) → 𝑂 ∈ ( 𝐴 𝐿 𝑅 ) )
119 1 3 4 71 73 72 80 81 83 118 tglineelsb2 ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐴 ) → ( 𝐴 𝐿 𝑅 ) = ( 𝐴 𝐿 𝑂 ) )
120 79 119 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐴 ) → ( 𝑅 𝐿 𝐴 ) = ( 𝐴 𝐿 𝑂 ) )
121 1 2 3 4 5 32 35 14 perpcom ⊢ ( 𝜑 → ( 𝐴 𝐿 𝑂 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) )
122 121 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐴 ) → ( 𝐴 𝐿 𝑂 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) )
123 120 122 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐴 ) → ( 𝑅 𝐿 𝐴 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) )
124 32 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐴 ) → ( 𝐴 𝐿 𝐵 ) ∈ ran 𝐿 )
125 37 necomd ⊢ ( 𝜑 → 𝑅 ≠ 𝐵 )
126 1 3 4 5 17 8 125 tgelrnln ⊢ ( 𝜑 → ( 𝑅 𝐿 𝐵 ) ∈ ran 𝐿 )
127 126 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐴 ) → ( 𝑅 𝐿 𝐵 ) ∈ ran 𝐿 )
128 1 3 4 5 17 8 125 tglinerflx2 ⊢ ( 𝜑 → 𝐵 ∈ ( 𝑅 𝐿 𝐵 ) )
129 63 128 elind ⊢ ( 𝜑 → 𝐵 ∈ ( ( 𝐴 𝐿 𝐵 ) ∩ ( 𝑅 𝐿 𝐵 ) ) )
130 1 3 4 5 17 8 125 tglinerflx1 ⊢ ( 𝜑 → 𝑅 ∈ ( 𝑅 𝐿 𝐵 ) )
131 1 2 3 4 5 32 126 129 68 130 9 125 55 ragperp ⊢ ( 𝜑 → ( 𝐴 𝐿 𝐵 ) ( ⟂G ‘ 𝐺 ) ( 𝑅 𝐿 𝐵 ) )
132 131 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐴 ) → ( 𝐴 𝐿 𝐵 ) ( ⟂G ‘ 𝐺 ) ( 𝑅 𝐿 𝐵 ) )
133 1 2 3 4 71 124 127 132 perpcom ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐴 ) → ( 𝑅 𝐿 𝐵 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) )
134 66 29 67 69 70 123 133 reu2eqd ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐴 ) → 𝐴 = 𝐵 )
135 64 134 mtand ⊢ ( 𝜑 → ¬ 𝑋 = 𝐴 )
136 135 neqned ⊢ ( 𝜑 → 𝑋 ≠ 𝐴 )
137 136 necomd ⊢ ( 𝜑 → 𝐴 ≠ 𝑋 )
138 eqid ⊢ ( 𝑆 ‘ 𝐴 ) = ( 𝑆 ‘ 𝐴 )
139 eqid ⊢ ( 𝑆 ‘ 𝑀 ) = ( 𝑆 ‘ 𝑀 )
140 1 2 3 4 6 5 7 138 11 mircl ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐴 ) ‘ 𝑂 ) ∈ 𝑃 )
141 88 orcd ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
142 1 4 3 5 7 8 20 141 colcom ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐵 𝐿 𝐴 ) ∨ 𝐵 = 𝐴 ) )
143 1 4 3 5 8 7 20 142 colrot1 ⊢ ( 𝜑 → ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) )
144 1 2 3 4 6 5 8 7 11 20 101 89 143 ragcol ⊢ ( 𝜑 → ⟨“ 𝑋 𝐴 𝑂 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
145 1 2 3 4 6 5 20 7 11 israg ⊢ ( 𝜑 → ( ⟨“ 𝑋 𝐴 𝑂 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ( 𝑋 − 𝑂 ) = ( 𝑋 − ( ( 𝑆 ‘ 𝐴 ) ‘ 𝑂 ) ) ) )
146 144 145 mpbid ⊢ ( 𝜑 → ( 𝑋 − 𝑂 ) = ( 𝑋 − ( ( 𝑆 ‘ 𝐴 ) ‘ 𝑂 ) ) )
147 25 eqcomd ⊢ ( 𝜑 → ( 𝑋 − 𝑅 ) = ( 𝑋 − 𝑍 ) )
148 eqidd ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐴 ) ‘ 𝑂 ) = ( ( 𝑆 ‘ 𝐴 ) ‘ 𝑂 ) )
149 27 eqcomd ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑀 ) ‘ 𝑍 ) = 𝑅 )
150 1 2 3 4 6 5 26 139 23 149 mircom ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑀 ) ‘ 𝑅 ) = 𝑍 )
151 150 eqcomd ⊢ ( 𝜑 → 𝑍 = ( ( 𝑆 ‘ 𝑀 ) ‘ 𝑅 ) )
152 1 2 3 4 6 5 138 139 11 140 20 17 23 7 26 87 24 146 147 148 151 krippen ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 𝐼 𝑀 ) )
153 1 3 4 5 7 20 26 137 152 btwnlng3 ⊢ ( 𝜑 → 𝑀 ∈ ( 𝐴 𝐿 𝑋 ) )
154 1 3 4 5 7 8 9 20 136 88 26 153 tglineeltr ⊢ ( 𝜑 → 𝑀 ∈ ( 𝐴 𝐿 𝐵 ) )
155 1 2 3 4 5 32 126 131 perpcom ⊢ ( 𝜑 → ( 𝑅 𝐿 𝐵 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) )
156 nelne2 ⊢ ( ( 𝑀 ∈ ( 𝐴 𝐿 𝐵 ) ∧ ¬ 𝑅 ∈ ( 𝐴 𝐿 𝐵 ) ) → 𝑀 ≠ 𝑅 )
157 154 61 156 syl2anc ⊢ ( 𝜑 → 𝑀 ≠ 𝑅 )
158 157 necomd ⊢ ( 𝜑 → 𝑅 ≠ 𝑀 )
159 1 3 4 5 17 26 158 tgelrnln ⊢ ( 𝜑 → ( 𝑅 𝐿 𝑀 ) ∈ ran 𝐿 )
160 1 3 4 5 17 26 158 tglinerflx2 ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑅 𝐿 𝑀 ) )
161 154 160 elind ⊢ ( 𝜑 → 𝑀 ∈ ( ( 𝐴 𝐿 𝐵 ) ∩ ( 𝑅 𝐿 𝑀 ) ) )
162 1 3 4 5 17 26 158 tglinerflx1 ⊢ ( 𝜑 → 𝑅 ∈ ( 𝑅 𝐿 𝑀 ) )
163 simpr ⊢ ( ( 𝜑 ∧ 𝑀 = 𝑋 ) → 𝑀 = 𝑋 )
164 5 adantr ⊢ ( ( 𝜑 ∧ 𝑀 = 𝑋 ) → 𝐺 ∈ TarskiG )
165 26 adantr ⊢ ( ( 𝜑 ∧ 𝑀 = 𝑋 ) → 𝑀 ∈ 𝑃 )
166 7 adantr ⊢ ( ( 𝜑 ∧ 𝑀 = 𝑋 ) → 𝐴 ∈ 𝑃 )
167 11 adantr ⊢ ( ( 𝜑 ∧ 𝑀 = 𝑋 ) → 𝑂 ∈ 𝑃 )
168 140 adantr ⊢ ( ( 𝜑 ∧ 𝑀 = 𝑋 ) → ( ( 𝑆 ‘ 𝐴 ) ‘ 𝑂 ) ∈ 𝑃 )
169 146 adantr ⊢ ( ( 𝜑 ∧ 𝑀 = 𝑋 ) → ( 𝑋 − 𝑂 ) = ( 𝑋 − ( ( 𝑆 ‘ 𝐴 ) ‘ 𝑂 ) ) )
170 163 oveq1d ⊢ ( ( 𝜑 ∧ 𝑀 = 𝑋 ) → ( 𝑀 − 𝑂 ) = ( 𝑋 − 𝑂 ) )
171 163 oveq1d ⊢ ( ( 𝜑 ∧ 𝑀 = 𝑋 ) → ( 𝑀 − ( ( 𝑆 ‘ 𝐴 ) ‘ 𝑂 ) ) = ( 𝑋 − ( ( 𝑆 ‘ 𝐴 ) ‘ 𝑂 ) ) )
172 169 170 171 3eqtr4rd ⊢ ( ( 𝜑 ∧ 𝑀 = 𝑋 ) → ( 𝑀 − ( ( 𝑆 ‘ 𝐴 ) ‘ 𝑂 ) ) = ( 𝑀 − 𝑂 ) )
173 23 adantr ⊢ ( ( 𝜑 ∧ 𝑀 = 𝑋 ) → 𝑍 ∈ 𝑃 )
174 17 adantr ⊢ ( ( 𝜑 ∧ 𝑀 = 𝑋 ) → 𝑅 ∈ 𝑃 )
175 27 adantr ⊢ ( ( 𝜑 ∧ 𝑀 = 𝑋 ) → 𝑅 = ( ( 𝑆 ‘ 𝑀 ) ‘ 𝑍 ) )
176 175 oveq2d ⊢ ( ( 𝜑 ∧ 𝑀 = 𝑋 ) → ( 𝑀 − 𝑅 ) = ( 𝑀 − ( ( 𝑆 ‘ 𝑀 ) ‘ 𝑍 ) ) )
177 1 2 3 4 6 164 165 139 173 mircgr ⊢ ( ( 𝜑 ∧ 𝑀 = 𝑋 ) → ( 𝑀 − ( ( 𝑆 ‘ 𝑀 ) ‘ 𝑍 ) ) = ( 𝑀 − 𝑍 ) )
178 176 177 eqtrd ⊢ ( ( 𝜑 ∧ 𝑀 = 𝑋 ) → ( 𝑀 − 𝑅 ) = ( 𝑀 − 𝑍 ) )
179 1 2 3 164 165 174 165 173 178 tgcgrcomlr ⊢ ( ( 𝜑 ∧ 𝑀 = 𝑋 ) → ( 𝑅 − 𝑀 ) = ( 𝑍 − 𝑀 ) )
180 88 adantr ⊢ ( ( 𝜑 ∧ 𝑀 = 𝑋 ) → 𝑋 ∈ ( 𝐴 𝐿 𝐵 ) )
181 163 180 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑀 = 𝑋 ) → 𝑀 ∈ ( 𝐴 𝐿 𝐵 ) )
182 61 adantr ⊢ ( ( 𝜑 ∧ 𝑀 = 𝑋 ) → ¬ 𝑅 ∈ ( 𝐴 𝐿 𝐵 ) )
183 181 182 156 syl2anc ⊢ ( ( 𝜑 ∧ 𝑀 = 𝑋 ) → 𝑀 ≠ 𝑅 )
184 183 necomd ⊢ ( ( 𝜑 ∧ 𝑀 = 𝑋 ) → 𝑅 ≠ 𝑀 )
185 1 2 3 164 174 165 173 165 179 184 tgcgrneq ⊢ ( ( 𝜑 ∧ 𝑀 = 𝑋 ) → 𝑍 ≠ 𝑀 )
186 1 2 3 4 6 5 26 139 23 mirbtwn ⊢ ( 𝜑 → 𝑀 ∈ ( ( ( 𝑆 ‘ 𝑀 ) ‘ 𝑍 ) 𝐼 𝑍 ) )
187 27 oveq1d ⊢ ( 𝜑 → ( 𝑅 𝐼 𝑍 ) = ( ( ( 𝑆 ‘ 𝑀 ) ‘ 𝑍 ) 𝐼 𝑍 ) )
188 186 187 eleqtrrd ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑅 𝐼 𝑍 ) )
189 188 adantr ⊢ ( ( 𝜑 ∧ 𝑀 = 𝑋 ) → 𝑀 ∈ ( 𝑅 𝐼 𝑍 ) )
190 1 2 3 164 174 165 173 189 tgbtwncom ⊢ ( ( 𝜑 ∧ 𝑀 = 𝑋 ) → 𝑀 ∈ ( 𝑍 𝐼 𝑅 ) )
191 24 adantr ⊢ ( ( 𝜑 ∧ 𝑀 = 𝑋 ) → 𝑋 ∈ ( ( ( 𝑆 ‘ 𝐴 ) ‘ 𝑂 ) 𝐼 𝑍 ) )
192 163 191 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑀 = 𝑋 ) → 𝑀 ∈ ( ( ( 𝑆 ‘ 𝐴 ) ‘ 𝑂 ) 𝐼 𝑍 ) )
193 1 2 3 164 168 165 173 192 tgbtwncom ⊢ ( ( 𝜑 ∧ 𝑀 = 𝑋 ) → 𝑀 ∈ ( 𝑍 𝐼 ( ( 𝑆 ‘ 𝐴 ) ‘ 𝑂 ) ) )
194 22 adantr ⊢ ( ( 𝜑 ∧ 𝑀 = 𝑋 ) → 𝑋 ∈ ( 𝑅 𝐼 𝑂 ) )
195 163 194 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑀 = 𝑋 ) → 𝑀 ∈ ( 𝑅 𝐼 𝑂 ) )
196 1 3 164 173 165 174 168 167 185 184 190 193 195 tgbtwnconn22 ⊢ ( ( 𝜑 ∧ 𝑀 = 𝑋 ) → 𝑀 ∈ ( ( ( 𝑆 ‘ 𝐴 ) ‘ 𝑂 ) 𝐼 𝑂 ) )
197 1 2 3 4 6 164 165 139 167 168 172 196 ismir ⊢ ( ( 𝜑 ∧ 𝑀 = 𝑋 ) → ( ( 𝑆 ‘ 𝐴 ) ‘ 𝑂 ) = ( ( 𝑆 ‘ 𝑀 ) ‘ 𝑂 ) )
198 197 eqcomd ⊢ ( ( 𝜑 ∧ 𝑀 = 𝑋 ) → ( ( 𝑆 ‘ 𝑀 ) ‘ 𝑂 ) = ( ( 𝑆 ‘ 𝐴 ) ‘ 𝑂 ) )
199 1 2 3 4 6 164 165 166 167 198 miduniq1 ⊢ ( ( 𝜑 ∧ 𝑀 = 𝑋 ) → 𝑀 = 𝐴 )
200 163 199 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑀 = 𝑋 ) → 𝑋 = 𝐴 )
201 135 200 mtand ⊢ ( 𝜑 → ¬ 𝑀 = 𝑋 )
202 201 neqned ⊢ ( 𝜑 → 𝑀 ≠ 𝑋 )
203 202 necomd ⊢ ( 𝜑 → 𝑋 ≠ 𝑀 )
204 150 oveq2d ⊢ ( 𝜑 → ( 𝑋 − ( ( 𝑆 ‘ 𝑀 ) ‘ 𝑅 ) ) = ( 𝑋 − 𝑍 ) )
205 204 25 eqtr2d ⊢ ( 𝜑 → ( 𝑋 − 𝑅 ) = ( 𝑋 − ( ( 𝑆 ‘ 𝑀 ) ‘ 𝑅 ) ) )
206 1 2 3 4 6 5 20 26 17 israg ⊢ ( 𝜑 → ( ⟨“ 𝑋 𝑀 𝑅 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ( 𝑋 − 𝑅 ) = ( 𝑋 − ( ( 𝑆 ‘ 𝑀 ) ‘ 𝑅 ) ) ) )
207 205 206 mpbird ⊢ ( 𝜑 → ⟨“ 𝑋 𝑀 𝑅 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
208 1 2 3 4 5 32 159 161 88 162 203 158 207 ragperp ⊢ ( 𝜑 → ( 𝐴 𝐿 𝐵 ) ( ⟂G ‘ 𝐺 ) ( 𝑅 𝐿 𝑀 ) )
209 1 2 3 4 5 32 159 208 perpcom ⊢ ( 𝜑 → ( 𝑅 𝐿 𝑀 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) )
210 29 31 62 63 154 155 209 reu2eqd ⊢ ( 𝜑 → 𝐵 = 𝑀 )