Metamath Proof Explorer


Theorem mircgrs

Description: Point inversion preserves congruence. Theorem 7.16 of Schwabhauser p. 51. (Contributed by Thierry Arnoux, 30-Jul-2019)

Ref Expression
Hypotheses mirval.p 𝑃 = ( Base ‘ 𝐺 )
mirval.d = ( dist ‘ 𝐺 )
mirval.i 𝐼 = ( Itv ‘ 𝐺 )
mirval.l 𝐿 = ( LineG ‘ 𝐺 )
mirval.s 𝑆 = ( pInvG ‘ 𝐺 )
mirval.g ( 𝜑𝐺 ∈ TarskiG )
mirval.a ( 𝜑𝐴𝑃 )
mirfv.m 𝑀 = ( 𝑆𝐴 )
miriso.1 ( 𝜑𝑋𝑃 )
miriso.2 ( 𝜑𝑌𝑃 )
mircgrs.z ( 𝜑𝑍𝑃 )
mircgrs.t ( 𝜑𝑇𝑃 )
mircgrs.e ( 𝜑 → ( 𝑋 𝑌 ) = ( 𝑍 𝑇 ) )
Assertion mircgrs ( 𝜑 → ( ( 𝑀𝑋 ) ( 𝑀𝑌 ) ) = ( ( 𝑀𝑍 ) ( 𝑀𝑇 ) ) )

Proof

Step Hyp Ref Expression
1 mirval.p 𝑃 = ( Base ‘ 𝐺 )
2 mirval.d = ( dist ‘ 𝐺 )
3 mirval.i 𝐼 = ( Itv ‘ 𝐺 )
4 mirval.l 𝐿 = ( LineG ‘ 𝐺 )
5 mirval.s 𝑆 = ( pInvG ‘ 𝐺 )
6 mirval.g ( 𝜑𝐺 ∈ TarskiG )
7 mirval.a ( 𝜑𝐴𝑃 )
8 mirfv.m 𝑀 = ( 𝑆𝐴 )
9 miriso.1 ( 𝜑𝑋𝑃 )
10 miriso.2 ( 𝜑𝑌𝑃 )
11 mircgrs.z ( 𝜑𝑍𝑃 )
12 mircgrs.t ( 𝜑𝑇𝑃 )
13 mircgrs.e ( 𝜑 → ( 𝑋 𝑌 ) = ( 𝑍 𝑇 ) )
14 1 2 3 4 5 6 7 8 9 10 miriso ( 𝜑 → ( ( 𝑀𝑋 ) ( 𝑀𝑌 ) ) = ( 𝑋 𝑌 ) )
15 1 2 3 4 5 6 7 8 11 12 miriso ( 𝜑 → ( ( 𝑀𝑍 ) ( 𝑀𝑇 ) ) = ( 𝑍 𝑇 ) )
16 13 14 15 3eqtr4d ( 𝜑 → ( ( 𝑀𝑋 ) ( 𝑀𝑌 ) ) = ( ( 𝑀𝑍 ) ( 𝑀𝑇 ) ) )