Metamath Proof Explorer

Theorem miriso

Description: The point inversion function is an isometry, i.e. it is conserves congruence. Because it is also a bijection, it is also a motion. Theorem 7.13 of Schwabhauser p. 50. (Contributed by Thierry Arnoux, 6-Jun-2019)

Ref Expression
Hypotheses mirval.p 
|- P = ( Base ` G )
mirval.d 
|- .- = ( dist ` G )
mirval.i 
|- I = ( Itv ` G )
mirval.l 
|- L = ( LineG ` G )
mirval.s 
|- S = ( pInvG ` G )
mirval.g 
|- ( ph -> G e. TarskiG )
mirval.a 
|- ( ph -> A e. P )
mirfv.m 
|- M = ( S ` A )
miriso.1 
|- ( ph -> X e. P )
miriso.2 
|- ( ph -> Y e. P )
Assertion miriso 
|- ( ph -> ( ( M ` X ) .- ( M ` Y ) ) = ( X .- Y ) )

Proof

Step Hyp Ref Expression
1 mirval.p 
 |-  P = ( Base ` G )
2 mirval.d 
 |-  .- = ( dist ` G )
3 mirval.i 
 |-  I = ( Itv ` G )
4 mirval.l 
 |-  L = ( LineG ` G )
5 mirval.s 
 |-  S = ( pInvG ` G )
6 mirval.g 
 |-  ( ph -> G e. TarskiG )
7 mirval.a 
 |-  ( ph -> A e. P )
8 mirfv.m 
 |-  M = ( S ` A )
9 miriso.1 
 |-  ( ph -> X e. P )
10 miriso.2 
 |-  ( ph -> Y e. P )
11 simpr 
 |-  ( ( ph /\ X = A ) -> X = A )
12 11 oveq1d 
 |-  ( ( ph /\ X = A ) -> ( X .- Y ) = ( A .- Y ) )
13 6 adantr 
 |-  ( ( ph /\ X = A ) -> G e. TarskiG )
14 7 adantr 
 |-  ( ( ph /\ X = A ) -> A e. P )
15 10 adantr 
 |-  ( ( ph /\ X = A ) -> Y e. P )
16 1 2 3 4 5 13 14 8 15 mircgr 
 |-  ( ( ph /\ X = A ) -> ( A .- ( M ` Y ) ) = ( A .- Y ) )
17 9 adantr 
 |-  ( ( ph /\ X = A ) -> X e. P )
18 11 eqcomd 
 |-  ( ( ph /\ X = A ) -> A = X )
19 18 oveq2d 
 |-  ( ( ph /\ X = A ) -> ( A .- A ) = ( A .- X ) )
20 1 2 3 13 14 17 tgbtwntriv1 
 |-  ( ( ph /\ X = A ) -> A e. ( A I X ) )
21 1 2 3 4 5 13 14 8 17 14 19 20 ismir 
 |-  ( ( ph /\ X = A ) -> A = ( M ` X ) )
22 21 oveq1d 
 |-  ( ( ph /\ X = A ) -> ( A .- ( M ` Y ) ) = ( ( M ` X ) .- ( M ` Y ) ) )
23 12 16 22 3eqtr2rd 
 |-  ( ( ph /\ X = A ) -> ( ( M ` X ) .- ( M ` Y ) ) = ( X .- Y ) )
24 6 adantr 
 |-  ( ( ph /\ X =/= A ) -> G e. TarskiG )
25 24 ad2antrr 
 |-  ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) -> G e. TarskiG )
26 25 ad6antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> G e. TarskiG )
27 simplr 
 |-  ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) -> x e. P )
28 27 ad6antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> x e. P )
29 9 adantr 
 |-  ( ( ph /\ X =/= A ) -> X e. P )
30 29 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> X e. P )
31 7 adantr 
 |-  ( ( ph /\ X =/= A ) -> A e. P )
32 31 ad2antrr 
 |-  ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) -> A e. P )
33 32 ad6antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> A e. P )
34 10 adantr 
 |-  ( ( ph /\ X =/= A ) -> Y e. P )
35 34 ad2antrr 
 |-  ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) -> Y e. P )
36 35 ad6antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> Y e. P )
37 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> z e. P )
38 1 2 3 4 5 24 31 8 29 mircl 
 |-  ( ( ph /\ X =/= A ) -> ( M ` X ) e. P )
39 38 ad2antrr 
 |-  ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) -> ( M ` X ) e. P )
40 39 ad6antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( M ` X ) e. P )
41 1 2 3 4 5 24 31 8 34 mircl 
 |-  ( ( ph /\ X =/= A ) -> ( M ` Y ) e. P )
42 41 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( M ` Y ) e. P )
43 1 2 3 4 5 26 33 8 30 mirbtwn 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> A e. ( ( M ` X ) I X ) )
44 simp-7r 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) )
45 44 simpld 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> X e. ( ( M ` X ) I x ) )
46 1 2 3 26 40 33 30 28 43 45 tgbtwnexch3 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> X e. ( A I x ) )
47 1 2 3 26 33 30 28 46 tgbtwncom 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> X e. ( x I A ) )
48 1 2 3 26 40 30 28 45 tgbtwncom 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> X e. ( x I ( M ` X ) ) )
49 1 2 3 26 40 33 30 43 tgbtwncom 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> A e. ( X I ( M ` X ) ) )
50 1 2 3 26 28 30 33 40 48 49 tgbtwnexch2 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> A e. ( x I ( M ` X ) ) )
51 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) )
52 51 simpld 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( M ` X ) e. ( x I z ) )
53 1 2 3 26 28 33 40 37 50 52 tgbtwnexch3 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( M ` X ) e. ( A I z ) )
54 1 2 3 26 33 40 37 53 tgbtwncom 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( M ` X ) e. ( z I A ) )
55 simp-4r 
 |-  ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) -> y e. P )
56 55 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> y e. P )
57 1 2 3 4 5 26 33 8 36 mirbtwn 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> A e. ( ( M ` Y ) I Y ) )
58 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) )
59 58 simpld 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> Y e. ( ( M ` Y ) I y ) )
60 1 2 3 26 42 33 36 56 57 59 tgbtwnexch3 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> Y e. ( A I y ) )
61 1 2 3 26 33 36 56 60 tgbtwncom 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> Y e. ( y I A ) )
62 1 2 3 4 5 26 33 8 30 mircgr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( A .- ( M ` X ) ) = ( A .- X ) )
63 58 simprd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( Y .- y ) = ( X .- A ) )
64 1 2 3 26 36 56 30 33 63 tgcgrcomlr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( y .- Y ) = ( A .- X ) )
65 62 64 eqtr4d 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( A .- ( M ` X ) ) = ( y .- Y ) )
66 51 simprd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( ( M ` X ) .- z ) = ( Y .- A ) )
67 1 2 3 26 33 40 37 56 36 33 53 61 65 66 tgcgrextend 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( A .- z ) = ( y .- A ) )
68 44 simprd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( X .- x ) = ( Y .- A ) )
69 68 eqcomd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( Y .- A ) = ( X .- x ) )
70 1 2 3 26 56 36 33 33 30 28 61 46 64 69 tgcgrextend 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( y .- A ) = ( A .- x ) )
71 67 70 eqtr2d 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( A .- x ) = ( A .- z ) )
72 1 2 3 26 33 28 33 37 71 tgcgrcomlr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( x .- A ) = ( z .- A ) )
73 62 eqcomd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( A .- X ) = ( A .- ( M ` X ) ) )
74 1 2 3 26 33 30 33 40 73 tgcgrcomlr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( X .- A ) = ( ( M ` X ) .- A ) )
75 simplr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> t e. P )
76 1 2 3 26 42 36 56 59 tgbtwncom 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> Y e. ( y I ( M ` Y ) ) )
77 1 2 3 26 42 33 36 57 tgbtwncom 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> A e. ( Y I ( M ` Y ) ) )
78 1 2 3 26 56 36 33 42 76 77 tgbtwnexch2 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> A e. ( y I ( M ` Y ) ) )
79 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) )
80 79 simpld 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( M ` Y ) e. ( y I t ) )
81 1 2 3 26 56 33 42 75 78 80 tgbtwnexch3 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( M ` Y ) e. ( A I t ) )
82 1 2 3 26 33 42 75 81 tgbtwncom 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( M ` Y ) e. ( t I A ) )
83 1 2 3 26 30 28 36 33 68 tgcgrcomlr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( x .- X ) = ( A .- Y ) )
84 1 2 3 4 5 26 33 8 36 mircgr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( A .- ( M ` Y ) ) = ( A .- Y ) )
85 83 84 eqtr4d 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( x .- X ) = ( A .- ( M ` Y ) ) )
86 79 simprd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( ( M ` Y ) .- t ) = ( X .- A ) )
87 86 eqcomd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( X .- A ) = ( ( M ` Y ) .- t ) )
88 1 2 3 26 28 30 33 33 42 75 47 81 85 87 tgcgrextend 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( x .- A ) = ( A .- t ) )
89 1 2 3 26 33 75 axtgcgrrflx 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( A .- t ) = ( t .- A ) )
90 88 89 eqtrd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( x .- A ) = ( t .- A ) )
91 1 2 3 26 28 33 75 33 90 tgcgrcomlr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( A .- x ) = ( A .- t ) )
92 70 91 89 3eqtrd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( y .- A ) = ( t .- A ) )
93 1 2 3 26 33 42 33 36 84 tgcgrcomlr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( ( M ` Y ) .- A ) = ( Y .- A ) )
94 93 eqcomd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( Y .- A ) = ( ( M ` Y ) .- A ) )
95 1 2 3 26 75 37 axtgcgrrflx 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( t .- z ) = ( z .- t ) )
96 simp-9r 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> X =/= A )
97 96 neneqd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> -. X = A )
98 26 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) /\ x = A ) -> G e. TarskiG )
99 33 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) /\ x = A ) -> A e. P )
100 30 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) /\ x = A ) -> X e. P )
101 46 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) /\ x = A ) -> X e. ( A I x ) )
102 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) /\ x = A ) -> x = A )
103 102 oveq2d 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) /\ x = A ) -> ( A I x ) = ( A I A ) )
104 101 103 eleqtrd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) /\ x = A ) -> X e. ( A I A ) )
105 1 2 3 98 99 100 104 axtgbtwnid 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) /\ x = A ) -> A = X )
106 105 eqcomd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) /\ x = A ) -> X = A )
107 97 106 mtand 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> -. x = A )
108 107 neqned 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> x =/= A )
109 1 2 3 26 28 33 40 37 50 52 tgbtwnexch 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> A e. ( x I z ) )
110 1 2 3 26 56 33 42 75 78 80 tgbtwnexch 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> A e. ( y I t ) )
111 1 2 3 26 56 33 75 110 tgbtwncom 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> A e. ( t I y ) )
112 1 2 3 26 56 33 axtgcgrrflx 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( y .- A ) = ( A .- y ) )
113 67 112 eqtrd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( A .- z ) = ( A .- y ) )
114 1 2 3 26 28 75 axtgcgrrflx 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( x .- t ) = ( t .- x ) )
115 91 eqcomd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( A .- t ) = ( A .- x ) )
116 1 2 3 26 28 33 37 75 33 56 75 28 108 109 111 90 113 114 115 axtg5seg 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( z .- t ) = ( y .- x ) )
117 95 116 eqtr2d 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( y .- x ) = ( t .- z ) )
118 1 2 3 26 56 36 33 28 75 42 33 37 61 82 92 94 117 71 tgifscgr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( Y .- x ) = ( ( M ` Y ) .- z ) )
119 1 2 3 26 36 28 42 37 118 tgcgrcomlr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( x .- Y ) = ( z .- ( M ` Y ) ) )
120 84 eqcomd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( A .- Y ) = ( A .- ( M ` Y ) ) )
121 1 2 3 26 28 30 33 36 37 40 33 42 47 54 72 74 119 120 tgifscgr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( X .- Y ) = ( ( M ` X ) .- ( M ` Y ) ) )
122 121 eqcomd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) /\ t e. P ) /\ ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) ) -> ( ( M ` X ) .- ( M ` Y ) ) = ( X .- Y ) )
123 simp-6l 
 |-  ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) -> ( ph /\ X =/= A ) )
124 simpllr 
 |-  ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) -> ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) )
125 24 ad2antrr 
 |-  ( ( ( ( ph /\ X =/= A ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) -> G e. TarskiG )
126 simplr 
 |-  ( ( ( ( ph /\ X =/= A ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) -> y e. P )
127 41 ad2antrr 
 |-  ( ( ( ( ph /\ X =/= A ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) -> ( M ` Y ) e. P )
128 29 ad2antrr 
 |-  ( ( ( ( ph /\ X =/= A ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) -> X e. P )
129 31 ad2antrr 
 |-  ( ( ( ( ph /\ X =/= A ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) -> A e. P )
130 1 2 3 125 126 127 128 129 axtgsegcon 
 |-  ( ( ( ( ph /\ X =/= A ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) -> E. t e. P ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) )
131 123 55 124 130 syl21anc 
 |-  ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) -> E. t e. P ( ( M ` Y ) e. ( y I t ) /\ ( ( M ` Y ) .- t ) = ( X .- A ) ) )
132 122 131 r19.29a 
 |-  ( ( ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) /\ z e. P ) /\ ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) ) -> ( ( M ` X ) .- ( M ` Y ) ) = ( X .- Y ) )
133 1 2 3 25 27 39 35 32 axtgsegcon 
 |-  ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) -> E. z e. P ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) )
134 133 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) -> E. z e. P ( ( M ` X ) e. ( x I z ) /\ ( ( M ` X ) .- z ) = ( Y .- A ) ) )
135 132 134 r19.29a 
 |-  ( ( ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) /\ y e. P ) /\ ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) ) -> ( ( M ` X ) .- ( M ` Y ) ) = ( X .- Y ) )
136 1 2 3 24 41 34 29 31 axtgsegcon 
 |-  ( ( ph /\ X =/= A ) -> E. y e. P ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) )
137 136 ad2antrr 
 |-  ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) -> E. y e. P ( Y e. ( ( M ` Y ) I y ) /\ ( Y .- y ) = ( X .- A ) ) )
138 135 137 r19.29a 
 |-  ( ( ( ( ph /\ X =/= A ) /\ x e. P ) /\ ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) ) -> ( ( M ` X ) .- ( M ` Y ) ) = ( X .- Y ) )
139 1 2 3 24 38 29 34 31 axtgsegcon 
 |-  ( ( ph /\ X =/= A ) -> E. x e. P ( X e. ( ( M ` X ) I x ) /\ ( X .- x ) = ( Y .- A ) ) )
140 138 139 r19.29a 
 |-  ( ( ph /\ X =/= A ) -> ( ( M ` X ) .- ( M ` Y ) ) = ( X .- Y ) )
141 23 140 pm2.61dane 
 |-  ( ph -> ( ( M ` X ) .- ( M ` Y ) ) = ( X .- Y ) )