Metamath Proof Explorer


Theorem mirmir

Description: The point inversion function is an involution. Theorem 7.7 of Schwabhauser p. 49. (Contributed by Thierry Arnoux, 3-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 )
mirmir.b
|- ( ph -> B e. P )
Assertion mirmir
|- ( ph -> ( M ` ( M ` B ) ) = B )

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 mirmir.b
 |-  ( ph -> B e. P )
10 1 2 3 4 5 6 7 8 9 mircl
 |-  ( ph -> ( M ` B ) e. P )
11 1 2 3 4 5 6 7 8 9 mircgr
 |-  ( ph -> ( A .- ( M ` B ) ) = ( A .- B ) )
12 11 eqcomd
 |-  ( ph -> ( A .- B ) = ( A .- ( M ` B ) ) )
13 1 2 3 4 5 6 7 8 9 mirbtwn
 |-  ( ph -> A e. ( ( M ` B ) I B ) )
14 1 2 3 6 10 7 9 13 tgbtwncom
 |-  ( ph -> A e. ( B I ( M ` B ) ) )
15 1 2 3 4 5 6 7 8 10 9 12 14 ismir
 |-  ( ph -> B = ( M ` ( M ` B ) ) )
16 15 eqcomd
 |-  ( ph -> ( M ` ( M ` B ) ) = B )