Metamath Proof Explorer

Theorem lmiisolem

Description: Lemma for lmiiso . (Contributed by Thierry Arnoux, 14-Dec-2019)

Ref Expression
Hypotheses ismid.p 
|- P = ( Base ` G )
ismid.d 
|- .- = ( dist ` G )
ismid.i 
|- I = ( Itv ` G )
ismid.g 
|- ( ph -> G e. TarskiG )
ismid.1 
|- ( ph -> G TarskiGDim>= 2 )
lmif.m 
|- M = ( ( lInvG ` G ) ` D )
lmif.l 
|- L = ( LineG ` G )
lmif.d 
|- ( ph -> D e. ran L )
lmiiso.1 
|- ( ph -> A e. P )
lmiiso.2 
|- ( ph -> B e. P )
lmiisolem.s 
|- S = ( ( pInvG ` G ) ` Z )
lmiisolem.z 
|- Z = ( ( A ( midG ` G ) ( M ` A ) ) ( midG ` G ) ( B ( midG ` G ) ( M ` B ) ) )
Assertion lmiisolem 
|- ( ph -> ( ( M ` A ) .- ( M ` B ) ) = ( A .- B ) )

Proof

Step Hyp Ref Expression
1 ismid.p 
 |-  P = ( Base ` G )
2 ismid.d 
 |-  .- = ( dist ` G )
3 ismid.i 
 |-  I = ( Itv ` G )
4 ismid.g 
 |-  ( ph -> G e. TarskiG )
5 ismid.1 
 |-  ( ph -> G TarskiGDim>= 2 )
6 lmif.m 
 |-  M = ( ( lInvG ` G ) ` D )
7 lmif.l 
 |-  L = ( LineG ` G )
8 lmif.d 
 |-  ( ph -> D e. ran L )
9 lmiiso.1 
 |-  ( ph -> A e. P )
10 lmiiso.2 
 |-  ( ph -> B e. P )
11 lmiisolem.s 
 |-  S = ( ( pInvG ` G ) ` Z )
12 lmiisolem.z 
 |-  Z = ( ( A ( midG ` G ) ( M ` A ) ) ( midG ` G ) ( B ( midG ` G ) ( M ` B ) ) )
13 4 adantr 
 |-  ( ( ph /\ ( S ` A ) = Z ) -> G e. TarskiG )
14 1 2 3 4 5 6 7 8 9 lmicl 
 |-  ( ph -> ( M ` A ) e. P )
15 1 2 3 4 5 9 14 midcl 
 |-  ( ph -> ( A ( midG ` G ) ( M ` A ) ) e. P )
16 1 2 3 4 5 6 7 8 10 lmicl 
 |-  ( ph -> ( M ` B ) e. P )
17 1 2 3 4 5 10 16 midcl 
 |-  ( ph -> ( B ( midG ` G ) ( M ` B ) ) e. P )
18 1 2 3 4 5 15 17 midcl 
 |-  ( ph -> ( ( A ( midG ` G ) ( M ` A ) ) ( midG ` G ) ( B ( midG ` G ) ( M ` B ) ) ) e. P )
19 12 18 eqeltrid 
 |-  ( ph -> Z e. P )
20 19 adantr 
 |-  ( ( ph /\ ( S ` A ) = Z ) -> Z e. P )
21 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
22 1 2 3 7 21 4 19 11 9 mircl 
 |-  ( ph -> ( S ` A ) e. P )
23 22 adantr 
 |-  ( ( ph /\ ( S ` A ) = Z ) -> ( S ` A ) e. P )
24 9 adantr 
 |-  ( ( ph /\ ( S ` A ) = Z ) -> A e. P )
25 1 2 3 7 21 13 20 11 24 mircgr 
 |-  ( ( ph /\ ( S ` A ) = Z ) -> ( Z .- ( S ` A ) ) = ( Z .- A ) )
26 simpr 
 |-  ( ( ph /\ ( S ` A ) = Z ) -> ( S ` A ) = Z )
27 26 eqcomd 
 |-  ( ( ph /\ ( S ` A ) = Z ) -> Z = ( S ` A ) )
28 1 2 3 13 20 23 20 24 25 27 tgcgreq 
 |-  ( ( ph /\ ( S ` A ) = Z ) -> Z = A )
29 simpr 
 |-  ( ( ph /\ ( A ( midG ` G ) ( M ` A ) ) = ( B ( midG ` G ) ( M ` B ) ) ) -> ( A ( midG ` G ) ( M ` A ) ) = ( B ( midG ` G ) ( M ` B ) ) )
30 29 oveq2d 
 |-  ( ( ph /\ ( A ( midG ` G ) ( M ` A ) ) = ( B ( midG ` G ) ( M ` B ) ) ) -> ( ( A ( midG ` G ) ( M ` A ) ) ( midG ` G ) ( A ( midG ` G ) ( M ` A ) ) ) = ( ( A ( midG ` G ) ( M ` A ) ) ( midG ` G ) ( B ( midG ` G ) ( M ` B ) ) ) )
31 12 30 eqtr4id 
 |-  ( ( ph /\ ( A ( midG ` G ) ( M ` A ) ) = ( B ( midG ` G ) ( M ` B ) ) ) -> Z = ( ( A ( midG ` G ) ( M ` A ) ) ( midG ` G ) ( A ( midG ` G ) ( M ` A ) ) ) )
32 4 adantr 
 |-  ( ( ph /\ ( A ( midG ` G ) ( M ` A ) ) = ( B ( midG ` G ) ( M ` B ) ) ) -> G e. TarskiG )
33 5 adantr 
 |-  ( ( ph /\ ( A ( midG ` G ) ( M ` A ) ) = ( B ( midG ` G ) ( M ` B ) ) ) -> G TarskiGDim>= 2 )
34 15 adantr 
 |-  ( ( ph /\ ( A ( midG ` G ) ( M ` A ) ) = ( B ( midG ` G ) ( M ` B ) ) ) -> ( A ( midG ` G ) ( M ` A ) ) e. P )
35 1 2 3 32 33 34 34 midid 
 |-  ( ( ph /\ ( A ( midG ` G ) ( M ` A ) ) = ( B ( midG ` G ) ( M ` B ) ) ) -> ( ( A ( midG ` G ) ( M ` A ) ) ( midG ` G ) ( A ( midG ` G ) ( M ` A ) ) ) = ( A ( midG ` G ) ( M ` A ) ) )
36 31 35 eqtrd 
 |-  ( ( ph /\ ( A ( midG ` G ) ( M ` A ) ) = ( B ( midG ` G ) ( M ` B ) ) ) -> Z = ( A ( midG ` G ) ( M ` A ) ) )
37 eqidd 
 |-  ( ph -> ( M ` A ) = ( M ` A ) )
38 1 2 3 4 5 6 7 8 9 14 islmib 
 |-  ( ph -> ( ( M ` A ) = ( M ` A ) <-> ( ( A ( midG ` G ) ( M ` A ) ) e. D /\ ( D ( perpG ` G ) ( A L ( M ` A ) ) \/ A = ( M ` A ) ) ) ) )
39 37 38 mpbid 
 |-  ( ph -> ( ( A ( midG ` G ) ( M ` A ) ) e. D /\ ( D ( perpG ` G ) ( A L ( M ` A ) ) \/ A = ( M ` A ) ) ) )
40 39 simpld 
 |-  ( ph -> ( A ( midG ` G ) ( M ` A ) ) e. D )
41 40 adantr 
 |-  ( ( ph /\ ( A ( midG ` G ) ( M ` A ) ) = ( B ( midG ` G ) ( M ` B ) ) ) -> ( A ( midG ` G ) ( M ` A ) ) e. D )
42 36 41 eqeltrd 
 |-  ( ( ph /\ ( A ( midG ` G ) ( M ` A ) ) = ( B ( midG ` G ) ( M ` B ) ) ) -> Z e. D )
43 4 adantr 
 |-  ( ( ph /\ ( A ( midG ` G ) ( M ` A ) ) =/= ( B ( midG ` G ) ( M ` B ) ) ) -> G e. TarskiG )
44 15 adantr 
 |-  ( ( ph /\ ( A ( midG ` G ) ( M ` A ) ) =/= ( B ( midG ` G ) ( M ` B ) ) ) -> ( A ( midG ` G ) ( M ` A ) ) e. P )
45 17 adantr 
 |-  ( ( ph /\ ( A ( midG ` G ) ( M ` A ) ) =/= ( B ( midG ` G ) ( M ` B ) ) ) -> ( B ( midG ` G ) ( M ` B ) ) e. P )
46 19 adantr 
 |-  ( ( ph /\ ( A ( midG ` G ) ( M ` A ) ) =/= ( B ( midG ` G ) ( M ` B ) ) ) -> Z e. P )
47 simpr 
 |-  ( ( ph /\ ( A ( midG ` G ) ( M ` A ) ) =/= ( B ( midG ` G ) ( M ` B ) ) ) -> ( A ( midG ` G ) ( M ` A ) ) =/= ( B ( midG ` G ) ( M ` B ) ) )
48 1 2 3 4 5 15 17 midbtwn 
 |-  ( ph -> ( ( A ( midG ` G ) ( M ` A ) ) ( midG ` G ) ( B ( midG ` G ) ( M ` B ) ) ) e. ( ( A ( midG ` G ) ( M ` A ) ) I ( B ( midG ` G ) ( M ` B ) ) ) )
49 12 48 eqeltrid 
 |-  ( ph -> Z e. ( ( A ( midG ` G ) ( M ` A ) ) I ( B ( midG ` G ) ( M ` B ) ) ) )
50 49 adantr 
 |-  ( ( ph /\ ( A ( midG ` G ) ( M ` A ) ) =/= ( B ( midG ` G ) ( M ` B ) ) ) -> Z e. ( ( A ( midG ` G ) ( M ` A ) ) I ( B ( midG ` G ) ( M ` B ) ) ) )
51 1 3 7 43 44 45 46 47 50 btwnlng1 
 |-  ( ( ph /\ ( A ( midG ` G ) ( M ` A ) ) =/= ( B ( midG ` G ) ( M ` B ) ) ) -> Z e. ( ( A ( midG ` G ) ( M ` A ) ) L ( B ( midG ` G ) ( M ` B ) ) ) )
52 8 adantr 
 |-  ( ( ph /\ ( A ( midG ` G ) ( M ` A ) ) =/= ( B ( midG ` G ) ( M ` B ) ) ) -> D e. ran L )
53 40 adantr 
 |-  ( ( ph /\ ( A ( midG ` G ) ( M ` A ) ) =/= ( B ( midG ` G ) ( M ` B ) ) ) -> ( A ( midG ` G ) ( M ` A ) ) e. D )
54 eqidd 
 |-  ( ph -> ( M ` B ) = ( M ` B ) )
55 1 2 3 4 5 6 7 8 10 16 islmib 
 |-  ( ph -> ( ( M ` B ) = ( M ` B ) <-> ( ( B ( midG ` G ) ( M ` B ) ) e. D /\ ( D ( perpG ` G ) ( B L ( M ` B ) ) \/ B = ( M ` B ) ) ) ) )
56 54 55 mpbid 
 |-  ( ph -> ( ( B ( midG ` G ) ( M ` B ) ) e. D /\ ( D ( perpG ` G ) ( B L ( M ` B ) ) \/ B = ( M ` B ) ) ) )
57 56 simpld 
 |-  ( ph -> ( B ( midG ` G ) ( M ` B ) ) e. D )
58 57 adantr 
 |-  ( ( ph /\ ( A ( midG ` G ) ( M ` A ) ) =/= ( B ( midG ` G ) ( M ` B ) ) ) -> ( B ( midG ` G ) ( M ` B ) ) e. D )
59 1 3 7 43 44 45 47 47 52 53 58 tglinethru 
 |-  ( ( ph /\ ( A ( midG ` G ) ( M ` A ) ) =/= ( B ( midG ` G ) ( M ` B ) ) ) -> D = ( ( A ( midG ` G ) ( M ` A ) ) L ( B ( midG ` G ) ( M ` B ) ) ) )
60 51 59 eleqtrrd 
 |-  ( ( ph /\ ( A ( midG ` G ) ( M ` A ) ) =/= ( B ( midG ` G ) ( M ` B ) ) ) -> Z e. D )
61 42 60 pm2.61dane 
 |-  ( ph -> Z e. D )
62 61 adantr 
 |-  ( ( ph /\ ( S ` A ) = Z ) -> Z e. D )
63 28 62 eqeltrrd 
 |-  ( ( ph /\ ( S ` A ) = Z ) -> A e. D )
64 1 2 3 4 5 6 7 8 9 lmiinv 
 |-  ( ph -> ( ( M ` A ) = A <-> A e. D ) )
65 64 biimpar 
 |-  ( ( ph /\ A e. D ) -> ( M ` A ) = A )
66 63 65 syldan 
 |-  ( ( ph /\ ( S ` A ) = Z ) -> ( M ` A ) = A )
67 66 28 eqtr4d 
 |-  ( ( ph /\ ( S ` A ) = Z ) -> ( M ` A ) = Z )
68 67 oveq1d 
 |-  ( ( ph /\ ( S ` A ) = Z ) -> ( ( M ` A ) .- ( M ` B ) ) = ( Z .- ( M ` B ) ) )
69 eqidd 
 |-  ( ( ph /\ B = ( M ` B ) ) -> Z = Z )
70 4 adantr 
 |-  ( ( ph /\ B = ( M ` B ) ) -> G e. TarskiG )
71 10 adantr 
 |-  ( ( ph /\ B = ( M ` B ) ) -> B e. P )
72 17 adantr 
 |-  ( ( ph /\ B = ( M ` B ) ) -> ( B ( midG ` G ) ( M ` B ) ) e. P )
73 1 2 3 4 5 10 16 midbtwn 
 |-  ( ph -> ( B ( midG ` G ) ( M ` B ) ) e. ( B I ( M ` B ) ) )
74 73 adantr 
 |-  ( ( ph /\ B = ( M ` B ) ) -> ( B ( midG ` G ) ( M ` B ) ) e. ( B I ( M ` B ) ) )
75 simpr 
 |-  ( ( ph /\ B = ( M ` B ) ) -> B = ( M ` B ) )
76 75 oveq2d 
 |-  ( ( ph /\ B = ( M ` B ) ) -> ( B I B ) = ( B I ( M ` B ) ) )
77 74 76 eleqtrrd 
 |-  ( ( ph /\ B = ( M ` B ) ) -> ( B ( midG ` G ) ( M ` B ) ) e. ( B I B ) )
78 1 2 3 70 71 72 77 axtgbtwnid 
 |-  ( ( ph /\ B = ( M ` B ) ) -> B = ( B ( midG ` G ) ( M ` B ) ) )
79 eqidd 
 |-  ( ( ph /\ B = ( M ` B ) ) -> B = B )
80 69 78 79 s3eqd 
 |-  ( ( ph /\ B = ( M ` B ) ) -> <" Z B B "> = <" Z ( B ( midG ` G ) ( M ` B ) ) B "> )
81 1 2 3 7 21 4 19 10 10 ragtrivb 
 |-  ( ph -> <" Z B B "> e. ( raG ` G ) )
82 81 adantr 
 |-  ( ( ph /\ B = ( M ` B ) ) -> <" Z B B "> e. ( raG ` G ) )
83 80 82 eqeltrrd 
 |-  ( ( ph /\ B = ( M ` B ) ) -> <" Z ( B ( midG ` G ) ( M ` B ) ) B "> e. ( raG ` G ) )
84 4 adantr 
 |-  ( ( ph /\ B =/= ( M ` B ) ) -> G e. TarskiG )
85 61 adantr 
 |-  ( ( ph /\ B =/= ( M ` B ) ) -> Z e. D )
86 57 adantr 
 |-  ( ( ph /\ B =/= ( M ` B ) ) -> ( B ( midG ` G ) ( M ` B ) ) e. D )
87 10 adantr 
 |-  ( ( ph /\ B =/= ( M ` B ) ) -> B e. P )
88 df-ne 
 |-  ( B =/= ( M ` B ) <-> -. B = ( M ` B ) )
89 56 simprd 
 |-  ( ph -> ( D ( perpG ` G ) ( B L ( M ` B ) ) \/ B = ( M ` B ) ) )
90 89 orcomd 
 |-  ( ph -> ( B = ( M ` B ) \/ D ( perpG ` G ) ( B L ( M ` B ) ) ) )
91 90 orcanai 
 |-  ( ( ph /\ -. B = ( M ` B ) ) -> D ( perpG ` G ) ( B L ( M ` B ) ) )
92 88 91 sylan2b 
 |-  ( ( ph /\ B =/= ( M ` B ) ) -> D ( perpG ` G ) ( B L ( M ` B ) ) )
93 16 adantr 
 |-  ( ( ph /\ B =/= ( M ` B ) ) -> ( M ` B ) e. P )
94 simpr 
 |-  ( ( ph /\ B =/= ( M ` B ) ) -> B =/= ( M ` B ) )
95 17 adantr 
 |-  ( ( ph /\ B =/= ( M ` B ) ) -> ( B ( midG ` G ) ( M ` B ) ) e. P )
96 4 adantr 
 |-  ( ( ph /\ ( B ( midG ` G ) ( M ` B ) ) = B ) -> G e. TarskiG )
97 10 adantr 
 |-  ( ( ph /\ ( B ( midG ` G ) ( M ` B ) ) = B ) -> B e. P )
98 16 adantr 
 |-  ( ( ph /\ ( B ( midG ` G ) ( M ` B ) ) = B ) -> ( M ` B ) e. P )
99 5 adantr 
 |-  ( ( ph /\ ( B ( midG ` G ) ( M ` B ) ) = B ) -> G TarskiGDim>= 2 )
100 simpr 
 |-  ( ( ph /\ ( B ( midG ` G ) ( M ` B ) ) = B ) -> ( B ( midG ` G ) ( M ` B ) ) = B )
101 1 2 3 96 99 97 98 100 midcgr 
 |-  ( ( ph /\ ( B ( midG ` G ) ( M ` B ) ) = B ) -> ( B .- B ) = ( B .- ( M ` B ) ) )
102 101 eqcomd 
 |-  ( ( ph /\ ( B ( midG ` G ) ( M ` B ) ) = B ) -> ( B .- ( M ` B ) ) = ( B .- B ) )
103 1 2 3 96 97 98 97 102 axtgcgrid 
 |-  ( ( ph /\ ( B ( midG ` G ) ( M ` B ) ) = B ) -> B = ( M ` B ) )
104 103 ex 
 |-  ( ph -> ( ( B ( midG ` G ) ( M ` B ) ) = B -> B = ( M ` B ) ) )
105 104 necon3d 
 |-  ( ph -> ( B =/= ( M ` B ) -> ( B ( midG ` G ) ( M ` B ) ) =/= B ) )
106 105 imp 
 |-  ( ( ph /\ B =/= ( M ` B ) ) -> ( B ( midG ` G ) ( M ` B ) ) =/= B )
107 73 adantr 
 |-  ( ( ph /\ B =/= ( M ` B ) ) -> ( B ( midG ` G ) ( M ` B ) ) e. ( B I ( M ` B ) ) )
108 1 3 7 84 87 93 95 94 107 btwnlng1 
 |-  ( ( ph /\ B =/= ( M ` B ) ) -> ( B ( midG ` G ) ( M ` B ) ) e. ( B L ( M ` B ) ) )
109 1 3 7 84 87 93 94 95 106 108 tglineelsb2 
 |-  ( ( ph /\ B =/= ( M ` B ) ) -> ( B L ( M ` B ) ) = ( B L ( B ( midG ` G ) ( M ` B ) ) ) )
110 1 3 7 84 95 87 106 tglinecom 
 |-  ( ( ph /\ B =/= ( M ` B ) ) -> ( ( B ( midG ` G ) ( M ` B ) ) L B ) = ( B L ( B ( midG ` G ) ( M ` B ) ) ) )
111 109 110 eqtr4d 
 |-  ( ( ph /\ B =/= ( M ` B ) ) -> ( B L ( M ` B ) ) = ( ( B ( midG ` G ) ( M ` B ) ) L B ) )
112 92 111 breqtrd 
 |-  ( ( ph /\ B =/= ( M ` B ) ) -> D ( perpG ` G ) ( ( B ( midG ` G ) ( M ` B ) ) L B ) )
113 1 2 3 7 84 85 86 87 112 perpdrag 
 |-  ( ( ph /\ B =/= ( M ` B ) ) -> <" Z ( B ( midG ` G ) ( M ` B ) ) B "> e. ( raG ` G ) )
114 83 113 pm2.61dane 
 |-  ( ph -> <" Z ( B ( midG ` G ) ( M ` B ) ) B "> e. ( raG ` G ) )
115 1 2 3 7 21 4 19 17 10 israg 
 |-  ( ph -> ( <" Z ( B ( midG ` G ) ( M ` B ) ) B "> e. ( raG ` G ) <-> ( Z .- B ) = ( Z .- ( ( ( pInvG ` G ) ` ( B ( midG ` G ) ( M ` B ) ) ) ` B ) ) ) )
116 114 115 mpbid 
 |-  ( ph -> ( Z .- B ) = ( Z .- ( ( ( pInvG ` G ) ` ( B ( midG ` G ) ( M ` B ) ) ) ` B ) ) )
117 eqidd 
 |-  ( ph -> ( B ( midG ` G ) ( M ` B ) ) = ( B ( midG ` G ) ( M ` B ) ) )
118 1 2 3 4 5 10 16 21 17 ismidb 
 |-  ( ph -> ( ( M ` B ) = ( ( ( pInvG ` G ) ` ( B ( midG ` G ) ( M ` B ) ) ) ` B ) <-> ( B ( midG ` G ) ( M ` B ) ) = ( B ( midG ` G ) ( M ` B ) ) ) )
119 117 118 mpbird 
 |-  ( ph -> ( M ` B ) = ( ( ( pInvG ` G ) ` ( B ( midG ` G ) ( M ` B ) ) ) ` B ) )
120 119 oveq2d 
 |-  ( ph -> ( Z .- ( M ` B ) ) = ( Z .- ( ( ( pInvG ` G ) ` ( B ( midG ` G ) ( M ` B ) ) ) ` B ) ) )
121 116 120 eqtr4d 
 |-  ( ph -> ( Z .- B ) = ( Z .- ( M ` B ) ) )
122 121 adantr 
 |-  ( ( ph /\ ( S ` A ) = Z ) -> ( Z .- B ) = ( Z .- ( M ` B ) ) )
123 28 oveq1d 
 |-  ( ( ph /\ ( S ` A ) = Z ) -> ( Z .- B ) = ( A .- B ) )
124 68 122 123 3eqtr2d 
 |-  ( ( ph /\ ( S ` A ) = Z ) -> ( ( M ` A ) .- ( M ` B ) ) = ( A .- B ) )
125 4 adantr 
 |-  ( ( ph /\ ( S ` A ) =/= Z ) -> G e. TarskiG )
126 22 adantr 
 |-  ( ( ph /\ ( S ` A ) =/= Z ) -> ( S ` A ) e. P )
127 19 adantr 
 |-  ( ( ph /\ ( S ` A ) =/= Z ) -> Z e. P )
128 9 adantr 
 |-  ( ( ph /\ ( S ` A ) =/= Z ) -> A e. P )
129 1 2 3 7 21 4 19 11 14 mircl 
 |-  ( ph -> ( S ` ( M ` A ) ) e. P )
130 129 adantr 
 |-  ( ( ph /\ ( S ` A ) =/= Z ) -> ( S ` ( M ` A ) ) e. P )
131 14 adantr 
 |-  ( ( ph /\ ( S ` A ) =/= Z ) -> ( M ` A ) e. P )
132 10 adantr 
 |-  ( ( ph /\ ( S ` A ) =/= Z ) -> B e. P )
133 16 adantr 
 |-  ( ( ph /\ ( S ` A ) =/= Z ) -> ( M ` B ) e. P )
134 simpr 
 |-  ( ( ph /\ ( S ` A ) =/= Z ) -> ( S ` A ) =/= Z )
135 1 2 3 7 21 125 127 11 128 mirbtwn 
 |-  ( ( ph /\ ( S ` A ) =/= Z ) -> Z e. ( ( S ` A ) I A ) )
136 1 2 3 7 21 125 127 11 131 mirbtwn 
 |-  ( ( ph /\ ( S ` A ) =/= Z ) -> Z e. ( ( S ` ( M ` A ) ) I ( M ` A ) ) )
137 eqidd 
 |-  ( ( ph /\ A = ( M ` A ) ) -> Z = Z )
138 4 adantr 
 |-  ( ( ph /\ A = ( M ` A ) ) -> G e. TarskiG )
139 9 adantr 
 |-  ( ( ph /\ A = ( M ` A ) ) -> A e. P )
140 15 adantr 
 |-  ( ( ph /\ A = ( M ` A ) ) -> ( A ( midG ` G ) ( M ` A ) ) e. P )
141 1 2 3 4 5 9 14 midbtwn 
 |-  ( ph -> ( A ( midG ` G ) ( M ` A ) ) e. ( A I ( M ` A ) ) )
142 141 adantr 
 |-  ( ( ph /\ A = ( M ` A ) ) -> ( A ( midG ` G ) ( M ` A ) ) e. ( A I ( M ` A ) ) )
143 simpr 
 |-  ( ( ph /\ A = ( M ` A ) ) -> A = ( M ` A ) )
144 143 oveq2d 
 |-  ( ( ph /\ A = ( M ` A ) ) -> ( A I A ) = ( A I ( M ` A ) ) )
145 142 144 eleqtrrd 
 |-  ( ( ph /\ A = ( M ` A ) ) -> ( A ( midG ` G ) ( M ` A ) ) e. ( A I A ) )
146 1 2 3 138 139 140 145 axtgbtwnid 
 |-  ( ( ph /\ A = ( M ` A ) ) -> A = ( A ( midG ` G ) ( M ` A ) ) )
147 eqidd 
 |-  ( ( ph /\ A = ( M ` A ) ) -> A = A )
148 137 146 147 s3eqd 
 |-  ( ( ph /\ A = ( M ` A ) ) -> <" Z A A "> = <" Z ( A ( midG ` G ) ( M ` A ) ) A "> )
149 1 2 3 7 21 4 19 9 9 ragtrivb 
 |-  ( ph -> <" Z A A "> e. ( raG ` G ) )
150 149 adantr 
 |-  ( ( ph /\ A = ( M ` A ) ) -> <" Z A A "> e. ( raG ` G ) )
151 148 150 eqeltrrd 
 |-  ( ( ph /\ A = ( M ` A ) ) -> <" Z ( A ( midG ` G ) ( M ` A ) ) A "> e. ( raG ` G ) )
152 4 adantr 
 |-  ( ( ph /\ A =/= ( M ` A ) ) -> G e. TarskiG )
153 61 adantr 
 |-  ( ( ph /\ A =/= ( M ` A ) ) -> Z e. D )
154 40 adantr 
 |-  ( ( ph /\ A =/= ( M ` A ) ) -> ( A ( midG ` G ) ( M ` A ) ) e. D )
155 9 adantr 
 |-  ( ( ph /\ A =/= ( M ` A ) ) -> A e. P )
156 df-ne 
 |-  ( A =/= ( M ` A ) <-> -. A = ( M ` A ) )
157 39 simprd 
 |-  ( ph -> ( D ( perpG ` G ) ( A L ( M ` A ) ) \/ A = ( M ` A ) ) )
158 157 orcomd 
 |-  ( ph -> ( A = ( M ` A ) \/ D ( perpG ` G ) ( A L ( M ` A ) ) ) )
159 158 orcanai 
 |-  ( ( ph /\ -. A = ( M ` A ) ) -> D ( perpG ` G ) ( A L ( M ` A ) ) )
160 156 159 sylan2b 
 |-  ( ( ph /\ A =/= ( M ` A ) ) -> D ( perpG ` G ) ( A L ( M ` A ) ) )
161 14 adantr 
 |-  ( ( ph /\ A =/= ( M ` A ) ) -> ( M ` A ) e. P )
162 simpr 
 |-  ( ( ph /\ A =/= ( M ` A ) ) -> A =/= ( M ` A ) )
163 15 adantr 
 |-  ( ( ph /\ A =/= ( M ` A ) ) -> ( A ( midG ` G ) ( M ` A ) ) e. P )
164 4 adantr 
 |-  ( ( ph /\ ( A ( midG ` G ) ( M ` A ) ) = A ) -> G e. TarskiG )
165 9 adantr 
 |-  ( ( ph /\ ( A ( midG ` G ) ( M ` A ) ) = A ) -> A e. P )
166 14 adantr 
 |-  ( ( ph /\ ( A ( midG ` G ) ( M ` A ) ) = A ) -> ( M ` A ) e. P )
167 5 adantr 
 |-  ( ( ph /\ ( A ( midG ` G ) ( M ` A ) ) = A ) -> G TarskiGDim>= 2 )
168 simpr 
 |-  ( ( ph /\ ( A ( midG ` G ) ( M ` A ) ) = A ) -> ( A ( midG ` G ) ( M ` A ) ) = A )
169 1 2 3 164 167 165 166 168 midcgr 
 |-  ( ( ph /\ ( A ( midG ` G ) ( M ` A ) ) = A ) -> ( A .- A ) = ( A .- ( M ` A ) ) )
170 169 eqcomd 
 |-  ( ( ph /\ ( A ( midG ` G ) ( M ` A ) ) = A ) -> ( A .- ( M ` A ) ) = ( A .- A ) )
171 1 2 3 164 165 166 165 170 axtgcgrid 
 |-  ( ( ph /\ ( A ( midG ` G ) ( M ` A ) ) = A ) -> A = ( M ` A ) )
172 171 ex 
 |-  ( ph -> ( ( A ( midG ` G ) ( M ` A ) ) = A -> A = ( M ` A ) ) )
173 172 necon3d 
 |-  ( ph -> ( A =/= ( M ` A ) -> ( A ( midG ` G ) ( M ` A ) ) =/= A ) )
174 173 imp 
 |-  ( ( ph /\ A =/= ( M ` A ) ) -> ( A ( midG ` G ) ( M ` A ) ) =/= A )
175 141 adantr 
 |-  ( ( ph /\ A =/= ( M ` A ) ) -> ( A ( midG ` G ) ( M ` A ) ) e. ( A I ( M ` A ) ) )
176 1 3 7 152 155 161 163 162 175 btwnlng1 
 |-  ( ( ph /\ A =/= ( M ` A ) ) -> ( A ( midG ` G ) ( M ` A ) ) e. ( A L ( M ` A ) ) )
177 1 3 7 152 155 161 162 163 174 176 tglineelsb2 
 |-  ( ( ph /\ A =/= ( M ` A ) ) -> ( A L ( M ` A ) ) = ( A L ( A ( midG ` G ) ( M ` A ) ) ) )
178 1 3 7 152 163 155 174 tglinecom 
 |-  ( ( ph /\ A =/= ( M ` A ) ) -> ( ( A ( midG ` G ) ( M ` A ) ) L A ) = ( A L ( A ( midG ` G ) ( M ` A ) ) ) )
179 177 178 eqtr4d 
 |-  ( ( ph /\ A =/= ( M ` A ) ) -> ( A L ( M ` A ) ) = ( ( A ( midG ` G ) ( M ` A ) ) L A ) )
180 160 179 breqtrd 
 |-  ( ( ph /\ A =/= ( M ` A ) ) -> D ( perpG ` G ) ( ( A ( midG ` G ) ( M ` A ) ) L A ) )
181 1 2 3 7 152 153 154 155 180 perpdrag 
 |-  ( ( ph /\ A =/= ( M ` A ) ) -> <" Z ( A ( midG ` G ) ( M ` A ) ) A "> e. ( raG ` G ) )
182 151 181 pm2.61dane 
 |-  ( ph -> <" Z ( A ( midG ` G ) ( M ` A ) ) A "> e. ( raG ` G ) )
183 1 2 3 7 21 4 19 15 9 israg 
 |-  ( ph -> ( <" Z ( A ( midG ` G ) ( M ` A ) ) A "> e. ( raG ` G ) <-> ( Z .- A ) = ( Z .- ( ( ( pInvG ` G ) ` ( A ( midG ` G ) ( M ` A ) ) ) ` A ) ) ) )
184 182 183 mpbid 
 |-  ( ph -> ( Z .- A ) = ( Z .- ( ( ( pInvG ` G ) ` ( A ( midG ` G ) ( M ` A ) ) ) ` A ) ) )
185 eqidd 
 |-  ( ph -> ( A ( midG ` G ) ( M ` A ) ) = ( A ( midG ` G ) ( M ` A ) ) )
186 1 2 3 4 5 9 14 21 15 ismidb 
 |-  ( ph -> ( ( M ` A ) = ( ( ( pInvG ` G ) ` ( A ( midG ` G ) ( M ` A ) ) ) ` A ) <-> ( A ( midG ` G ) ( M ` A ) ) = ( A ( midG ` G ) ( M ` A ) ) ) )
187 185 186 mpbird 
 |-  ( ph -> ( M ` A ) = ( ( ( pInvG ` G ) ` ( A ( midG ` G ) ( M ` A ) ) ) ` A ) )
188 187 oveq2d 
 |-  ( ph -> ( Z .- ( M ` A ) ) = ( Z .- ( ( ( pInvG ` G ) ` ( A ( midG ` G ) ( M ` A ) ) ) ` A ) ) )
189 184 188 eqtr4d 
 |-  ( ph -> ( Z .- A ) = ( Z .- ( M ` A ) ) )
190 1 2 3 7 21 4 19 11 9 mircgr 
 |-  ( ph -> ( Z .- ( S ` A ) ) = ( Z .- A ) )
191 1 2 3 7 21 4 19 11 14 mircgr 
 |-  ( ph -> ( Z .- ( S ` ( M ` A ) ) ) = ( Z .- ( M ` A ) ) )
192 189 190 191 3eqtr4d 
 |-  ( ph -> ( Z .- ( S ` A ) ) = ( Z .- ( S ` ( M ` A ) ) ) )
193 192 adantr 
 |-  ( ( ph /\ ( S ` A ) =/= Z ) -> ( Z .- ( S ` A ) ) = ( Z .- ( S ` ( M ` A ) ) ) )
194 1 2 3 125 127 126 127 130 193 tgcgrcomlr 
 |-  ( ( ph /\ ( S ` A ) =/= Z ) -> ( ( S ` A ) .- Z ) = ( ( S ` ( M ` A ) ) .- Z ) )
195 189 adantr 
 |-  ( ( ph /\ ( S ` A ) =/= Z ) -> ( Z .- A ) = ( Z .- ( M ` A ) ) )
196 11 fveq1i 
 |-  ( S ` ( A ( midG ` G ) ( M ` A ) ) ) = ( ( ( pInvG ` G ) ` Z ) ` ( A ( midG ` G ) ( M ` A ) ) )
197 1 2 3 4 5 9 14 11 19 mirmid 
 |-  ( ph -> ( ( S ` A ) ( midG ` G ) ( S ` ( M ` A ) ) ) = ( S ` ( A ( midG ` G ) ( M ` A ) ) ) )
198 12 eqcomi 
 |-  ( ( A ( midG ` G ) ( M ` A ) ) ( midG ` G ) ( B ( midG ` G ) ( M ` B ) ) ) = Z
199 1 2 3 4 5 15 17 21 19 ismidb 
 |-  ( ph -> ( ( B ( midG ` G ) ( M ` B ) ) = ( ( ( pInvG ` G ) ` Z ) ` ( A ( midG ` G ) ( M ` A ) ) ) <-> ( ( A ( midG ` G ) ( M ` A ) ) ( midG ` G ) ( B ( midG ` G ) ( M ` B ) ) ) = Z ) )
200 198 199 mpbiri 
 |-  ( ph -> ( B ( midG ` G ) ( M ` B ) ) = ( ( ( pInvG ` G ) ` Z ) ` ( A ( midG ` G ) ( M ` A ) ) ) )
201 196 197 200 3eqtr4a 
 |-  ( ph -> ( ( S ` A ) ( midG ` G ) ( S ` ( M ` A ) ) ) = ( B ( midG ` G ) ( M ` B ) ) )
202 1 2 3 4 5 22 129 21 17 ismidb 
 |-  ( ph -> ( ( S ` ( M ` A ) ) = ( ( ( pInvG ` G ) ` ( B ( midG ` G ) ( M ` B ) ) ) ` ( S ` A ) ) <-> ( ( S ` A ) ( midG ` G ) ( S ` ( M ` A ) ) ) = ( B ( midG ` G ) ( M ` B ) ) ) )
203 201 202 mpbird 
 |-  ( ph -> ( S ` ( M ` A ) ) = ( ( ( pInvG ` G ) ` ( B ( midG ` G ) ( M ` B ) ) ) ` ( S ` A ) ) )
204 119 203 oveq12d 
 |-  ( ph -> ( ( M ` B ) .- ( S ` ( M ` A ) ) ) = ( ( ( ( pInvG ` G ) ` ( B ( midG ` G ) ( M ` B ) ) ) ` B ) .- ( ( ( pInvG ` G ) ` ( B ( midG ` G ) ( M ` B ) ) ) ` ( S ` A ) ) ) )
205 eqid 
 |-  ( ( pInvG ` G ) ` ( B ( midG ` G ) ( M ` B ) ) ) = ( ( pInvG ` G ) ` ( B ( midG ` G ) ( M ` B ) ) )
206 1 2 3 7 21 4 17 205 10 22 miriso 
 |-  ( ph -> ( ( ( ( pInvG ` G ) ` ( B ( midG ` G ) ( M ` B ) ) ) ` B ) .- ( ( ( pInvG ` G ) ` ( B ( midG ` G ) ( M ` B ) ) ) ` ( S ` A ) ) ) = ( B .- ( S ` A ) ) )
207 204 206 eqtr2d 
 |-  ( ph -> ( B .- ( S ` A ) ) = ( ( M ` B ) .- ( S ` ( M ` A ) ) ) )
208 207 adantr 
 |-  ( ( ph /\ ( S ` A ) =/= Z ) -> ( B .- ( S ` A ) ) = ( ( M ` B ) .- ( S ` ( M ` A ) ) ) )
209 1 2 3 125 132 126 133 130 208 tgcgrcomlr 
 |-  ( ( ph /\ ( S ` A ) =/= Z ) -> ( ( S ` A ) .- B ) = ( ( S ` ( M ` A ) ) .- ( M ` B ) ) )
210 121 adantr 
 |-  ( ( ph /\ ( S ` A ) =/= Z ) -> ( Z .- B ) = ( Z .- ( M ` B ) ) )
211 1 2 3 125 126 127 128 130 127 131 132 133 134 135 136 194 195 209 210 axtg5seg 
 |-  ( ( ph /\ ( S ` A ) =/= Z ) -> ( A .- B ) = ( ( M ` A ) .- ( M ` B ) ) )
212 211 eqcomd 
 |-  ( ( ph /\ ( S ` A ) =/= Z ) -> ( ( M ` A ) .- ( M ` B ) ) = ( A .- B ) )
213 124 212 pm2.61dane 
 |-  ( ph -> ( ( M ` A ) .- ( M ` B ) ) = ( A .- B ) )