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 
|- P = ( Base ` G )
colperpex.d 
|- .- = ( dist ` G )
colperpex.i 
|- I = ( Itv ` G )
colperpex.l 
|- L = ( LineG ` G )
colperpex.g 
|- ( ph -> G e. TarskiG )
mideu.s 
|- S = ( pInvG ` G )
mideu.1 
|- ( ph -> A e. P )
mideu.2 
|- ( ph -> B e. P )
mideulem.1 
|- ( ph -> A =/= B )
mideulem.2 
|- ( ph -> Q e. P )
mideulem.3 
|- ( ph -> O e. P )
mideulem.4 
|- ( ph -> T e. P )
mideulem.5 
|- ( ph -> ( A L B ) ( perpG ` G ) ( Q L B ) )
mideulem.6 
|- ( ph -> ( A L B ) ( perpG ` G ) ( A L O ) )
mideulem.7 
|- ( ph -> T e. ( A L B ) )
mideulem.8 
|- ( ph -> T e. ( Q I O ) )
opphllem.1 
|- ( ph -> R e. P )
opphllem.2 
|- ( ph -> R e. ( B I Q ) )
opphllem.3 
|- ( ph -> ( A .- O ) = ( B .- R ) )
mideulem2.1 
|- ( ph -> X e. P )
mideulem2.2 
|- ( ph -> X e. ( T I B ) )
mideulem2.3 
|- ( ph -> X e. ( R I O ) )
mideulem2.4 
|- ( ph -> Z e. P )
mideulem2.5 
|- ( ph -> X e. ( ( ( S ` A ) ` O ) I Z ) )
mideulem2.6 
|- ( ph -> ( X .- Z ) = ( X .- R ) )
mideulem2.7 
|- ( ph -> M e. P )
mideulem2.8 
|- ( ph -> R = ( ( S ` M ) ` Z ) )
Assertion mideulem2 
|- ( ph -> B = M )

Proof

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