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 𝑃 = ( Base ‘ 𝐺 )
mirval.d = ( dist ‘ 𝐺 )
mirval.i 𝐼 = ( Itv ‘ 𝐺 )
mirval.l 𝐿 = ( LineG ‘ 𝐺 )
mirval.s 𝑆 = ( pInvG ‘ 𝐺 )
mirval.g ( 𝜑𝐺 ∈ TarskiG )
mirval.a ( 𝜑𝐴𝑃 )
mirfv.m 𝑀 = ( 𝑆𝐴 )
mirmir.b ( 𝜑𝐵𝑃 )
Assertion mirmir ( 𝜑 → ( 𝑀 ‘ ( 𝑀𝐵 ) ) = 𝐵 )

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 mirmir.b ( 𝜑𝐵𝑃 )
10 1 2 3 4 5 6 7 8 9 mircl ( 𝜑 → ( 𝑀𝐵 ) ∈ 𝑃 )
11 1 2 3 4 5 6 7 8 9 mircgr ( 𝜑 → ( 𝐴 ( 𝑀𝐵 ) ) = ( 𝐴 𝐵 ) )
12 11 eqcomd ( 𝜑 → ( 𝐴 𝐵 ) = ( 𝐴 ( 𝑀𝐵 ) ) )
13 1 2 3 4 5 6 7 8 9 mirbtwn ( 𝜑𝐴 ∈ ( ( 𝑀𝐵 ) 𝐼 𝐵 ) )
14 1 2 3 6 10 7 9 13 tgbtwncom ( 𝜑𝐴 ∈ ( 𝐵 𝐼 ( 𝑀𝐵 ) ) )
15 1 2 3 4 5 6 7 8 10 9 12 14 ismir ( 𝜑𝐵 = ( 𝑀 ‘ ( 𝑀𝐵 ) ) )
16 15 eqcomd ( 𝜑 → ( 𝑀 ‘ ( 𝑀𝐵 ) ) = 𝐵 )