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=BaseG
mirval.d -˙=distG
mirval.i I=ItvG
mirval.l L=Line𝒢G
mirval.s S=pInv𝒢G
mirval.g φG𝒢Tarski
mirval.a φAP
mirfv.m M=SA
miriso.1 φXP
miriso.2 φYP
Assertion miriso φMX-˙MY=X-˙Y

Proof

Step Hyp Ref Expression
1 mirval.p P=BaseG
2 mirval.d -˙=distG
3 mirval.i I=ItvG
4 mirval.l L=Line𝒢G
5 mirval.s S=pInv𝒢G
6 mirval.g φG𝒢Tarski
7 mirval.a φAP
8 mirfv.m M=SA
9 miriso.1 φXP
10 miriso.2 φYP
11 simpr φX=AX=A
12 11 oveq1d φX=AX-˙Y=A-˙Y
13 6 adantr φX=AG𝒢Tarski
14 7 adantr φX=AAP
15 10 adantr φX=AYP
16 1 2 3 4 5 13 14 8 15 mircgr φX=AA-˙MY=A-˙Y
17 9 adantr φX=AXP
18 11 eqcomd φX=AA=X
19 18 oveq2d φX=AA-˙A=A-˙X
20 1 2 3 13 14 17 tgbtwntriv1 φX=AAAIX
21 1 2 3 4 5 13 14 8 17 14 19 20 ismir φX=AA=MX
22 21 oveq1d φX=AA-˙MY=MX-˙MY
23 12 16 22 3eqtr2rd φX=AMX-˙MY=X-˙Y
24 6 adantr φXAG𝒢Tarski
25 24 ad2antrr φXAxPXMXIxX-˙x=Y-˙AG𝒢Tarski
26 25 ad6antr φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AG𝒢Tarski
27 simplr φXAxPXMXIxX-˙x=Y-˙AxP
28 27 ad6antr φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AxP
29 9 adantr φXAXP
30 29 ad8antr φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AXP
31 7 adantr φXAAP
32 31 ad2antrr φXAxPXMXIxX-˙x=Y-˙AAP
33 32 ad6antr φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AAP
34 10 adantr φXAYP
35 34 ad2antrr φXAxPXMXIxX-˙x=Y-˙AYP
36 35 ad6antr φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AYP
37 simp-4r φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AzP
38 1 2 3 4 5 24 31 8 29 mircl φXAMXP
39 38 ad2antrr φXAxPXMXIxX-˙x=Y-˙AMXP
40 39 ad6antr φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AMXP
41 1 2 3 4 5 24 31 8 34 mircl φXAMYP
42 41 ad8antr φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AMYP
43 1 2 3 4 5 26 33 8 30 mirbtwn φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AAMXIX
44 simp-7r φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AXMXIxX-˙x=Y-˙A
45 44 simpld φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AXMXIx
46 1 2 3 26 40 33 30 28 43 45 tgbtwnexch3 φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AXAIx
47 1 2 3 26 33 30 28 46 tgbtwncom φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AXxIA
48 1 2 3 26 40 30 28 45 tgbtwncom φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AXxIMX
49 1 2 3 26 40 33 30 43 tgbtwncom φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AAXIMX
50 1 2 3 26 28 30 33 40 48 49 tgbtwnexch2 φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AAxIMX
51 simpllr φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AMXxIzMX-˙z=Y-˙A
52 51 simpld φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AMXxIz
53 1 2 3 26 28 33 40 37 50 52 tgbtwnexch3 φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AMXAIz
54 1 2 3 26 33 40 37 53 tgbtwncom φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AMXzIA
55 simp-4r φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AyP
56 55 ad2antrr φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AyP
57 1 2 3 4 5 26 33 8 36 mirbtwn φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AAMYIY
58 simp-5r φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AYMYIyY-˙y=X-˙A
59 58 simpld φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AYMYIy
60 1 2 3 26 42 33 36 56 57 59 tgbtwnexch3 φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AYAIy
61 1 2 3 26 33 36 56 60 tgbtwncom φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AYyIA
62 1 2 3 4 5 26 33 8 30 mircgr φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AA-˙MX=A-˙X
63 58 simprd φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AY-˙y=X-˙A
64 1 2 3 26 36 56 30 33 63 tgcgrcomlr φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙Ay-˙Y=A-˙X
65 62 64 eqtr4d φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AA-˙MX=y-˙Y
66 51 simprd φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AMX-˙z=Y-˙A
67 1 2 3 26 33 40 37 56 36 33 53 61 65 66 tgcgrextend φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AA-˙z=y-˙A
68 44 simprd φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AX-˙x=Y-˙A
69 68 eqcomd φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AY-˙A=X-˙x
70 1 2 3 26 56 36 33 33 30 28 61 46 64 69 tgcgrextend φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙Ay-˙A=A-˙x
71 67 70 eqtr2d φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AA-˙x=A-˙z
72 1 2 3 26 33 28 33 37 71 tgcgrcomlr φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙Ax-˙A=z-˙A
73 62 eqcomd φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AA-˙X=A-˙MX
74 1 2 3 26 33 30 33 40 73 tgcgrcomlr φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AX-˙A=MX-˙A
75 simplr φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AtP
76 1 2 3 26 42 36 56 59 tgbtwncom φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AYyIMY
77 1 2 3 26 42 33 36 57 tgbtwncom φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AAYIMY
78 1 2 3 26 56 36 33 42 76 77 tgbtwnexch2 φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AAyIMY
79 simpr φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AMYyItMY-˙t=X-˙A
80 79 simpld φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AMYyIt
81 1 2 3 26 56 33 42 75 78 80 tgbtwnexch3 φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AMYAIt
82 1 2 3 26 33 42 75 81 tgbtwncom φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AMYtIA
83 1 2 3 26 30 28 36 33 68 tgcgrcomlr φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙Ax-˙X=A-˙Y
84 1 2 3 4 5 26 33 8 36 mircgr φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AA-˙MY=A-˙Y
85 83 84 eqtr4d φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙Ax-˙X=A-˙MY
86 79 simprd φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AMY-˙t=X-˙A
87 86 eqcomd φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AX-˙A=MY-˙t
88 1 2 3 26 28 30 33 33 42 75 47 81 85 87 tgcgrextend φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙Ax-˙A=A-˙t
89 1 2 3 26 33 75 axtgcgrrflx φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AA-˙t=t-˙A
90 88 89 eqtrd φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙Ax-˙A=t-˙A
91 1 2 3 26 28 33 75 33 90 tgcgrcomlr φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AA-˙x=A-˙t
92 70 91 89 3eqtrd φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙Ay-˙A=t-˙A
93 1 2 3 26 33 42 33 36 84 tgcgrcomlr φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AMY-˙A=Y-˙A
94 93 eqcomd φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AY-˙A=MY-˙A
95 1 2 3 26 75 37 axtgcgrrflx φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙At-˙z=z-˙t
96 simp-9r φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AXA
97 96 neneqd φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙A¬X=A
98 26 adantr φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙Ax=AG𝒢Tarski
99 33 adantr φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙Ax=AAP
100 30 adantr φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙Ax=AXP
101 46 adantr φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙Ax=AXAIx
102 simpr φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙Ax=Ax=A
103 102 oveq2d φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙Ax=AAIx=AIA
104 101 103 eleqtrd φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙Ax=AXAIA
105 1 2 3 98 99 100 104 axtgbtwnid φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙Ax=AA=X
106 105 eqcomd φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙Ax=AX=A
107 97 106 mtand φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙A¬x=A
108 107 neqned φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AxA
109 1 2 3 26 28 33 40 37 50 52 tgbtwnexch φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AAxIz
110 1 2 3 26 56 33 42 75 78 80 tgbtwnexch φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AAyIt
111 1 2 3 26 56 33 75 110 tgbtwncom φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AAtIy
112 1 2 3 26 56 33 axtgcgrrflx φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙Ay-˙A=A-˙y
113 67 112 eqtrd φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AA-˙z=A-˙y
114 1 2 3 26 28 75 axtgcgrrflx φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙Ax-˙t=t-˙x
115 91 eqcomd φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AA-˙t=A-˙x
116 1 2 3 26 28 33 37 75 33 56 75 28 108 109 111 90 113 114 115 axtg5seg φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙Az-˙t=y-˙x
117 95 116 eqtr2d φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙Ay-˙x=t-˙z
118 1 2 3 26 56 36 33 28 75 42 33 37 61 82 92 94 117 71 tgifscgr φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AY-˙x=MY-˙z
119 1 2 3 26 36 28 42 37 118 tgcgrcomlr φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙Ax-˙Y=z-˙MY
120 84 eqcomd φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AA-˙Y=A-˙MY
121 1 2 3 26 28 30 33 36 37 40 33 42 47 54 72 74 119 120 tgifscgr φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AX-˙Y=MX-˙MY
122 121 eqcomd φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙AMX-˙MY=X-˙Y
123 simp-6l φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AφXA
124 simpllr φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AYMYIyY-˙y=X-˙A
125 24 ad2antrr φXAyPYMYIyY-˙y=X-˙AG𝒢Tarski
126 simplr φXAyPYMYIyY-˙y=X-˙AyP
127 41 ad2antrr φXAyPYMYIyY-˙y=X-˙AMYP
128 29 ad2antrr φXAyPYMYIyY-˙y=X-˙AXP
129 31 ad2antrr φXAyPYMYIyY-˙y=X-˙AAP
130 1 2 3 125 126 127 128 129 axtgsegcon φXAyPYMYIyY-˙y=X-˙AtPMYyItMY-˙t=X-˙A
131 123 55 124 130 syl21anc φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AtPMYyItMY-˙t=X-˙A
132 122 131 r19.29a φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙AMX-˙MY=X-˙Y
133 1 2 3 25 27 39 35 32 axtgsegcon φXAxPXMXIxX-˙x=Y-˙AzPMXxIzMX-˙z=Y-˙A
134 133 ad2antrr φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AzPMXxIzMX-˙z=Y-˙A
135 132 134 r19.29a φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙AMX-˙MY=X-˙Y
136 1 2 3 24 41 34 29 31 axtgsegcon φXAyPYMYIyY-˙y=X-˙A
137 136 ad2antrr φXAxPXMXIxX-˙x=Y-˙AyPYMYIyY-˙y=X-˙A
138 135 137 r19.29a φXAxPXMXIxX-˙x=Y-˙AMX-˙MY=X-˙Y
139 1 2 3 24 38 29 34 31 axtgsegcon φXAxPXMXIxX-˙x=Y-˙A
140 138 139 r19.29a φXAMX-˙MY=X-˙Y
141 23 140 pm2.61dane φMX-˙MY=X-˙Y