Metamath Proof Explorer


Theorem mirinv

Description: The only invariant point of a point inversion Theorem 7.3 of Schwabhauser p. 49, Theorem 7.10 of Schwabhauser p. 50. (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 𝑀 = ( 𝑆𝐴 )
mirinv.b ( 𝜑𝐵𝑃 )
Assertion mirinv ( 𝜑 → ( ( 𝑀𝐵 ) = 𝐵𝐴 = 𝐵 ) )

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 mirinv.b ( 𝜑𝐵𝑃 )
10 6 adantr ( ( 𝜑 ∧ ( 𝑀𝐵 ) = 𝐵 ) → 𝐺 ∈ TarskiG )
11 9 adantr ( ( 𝜑 ∧ ( 𝑀𝐵 ) = 𝐵 ) → 𝐵𝑃 )
12 7 adantr ( ( 𝜑 ∧ ( 𝑀𝐵 ) = 𝐵 ) → 𝐴𝑃 )
13 1 2 3 4 5 10 12 8 11 mirbtwn ( ( 𝜑 ∧ ( 𝑀𝐵 ) = 𝐵 ) → 𝐴 ∈ ( ( 𝑀𝐵 ) 𝐼 𝐵 ) )
14 simpr ( ( 𝜑 ∧ ( 𝑀𝐵 ) = 𝐵 ) → ( 𝑀𝐵 ) = 𝐵 )
15 14 oveq1d ( ( 𝜑 ∧ ( 𝑀𝐵 ) = 𝐵 ) → ( ( 𝑀𝐵 ) 𝐼 𝐵 ) = ( 𝐵 𝐼 𝐵 ) )
16 13 15 eleqtrd ( ( 𝜑 ∧ ( 𝑀𝐵 ) = 𝐵 ) → 𝐴 ∈ ( 𝐵 𝐼 𝐵 ) )
17 1 2 3 10 11 12 16 axtgbtwnid ( ( 𝜑 ∧ ( 𝑀𝐵 ) = 𝐵 ) → 𝐵 = 𝐴 )
18 17 eqcomd ( ( 𝜑 ∧ ( 𝑀𝐵 ) = 𝐵 ) → 𝐴 = 𝐵 )
19 6 adantr ( ( 𝜑𝐴 = 𝐵 ) → 𝐺 ∈ TarskiG )
20 7 adantr ( ( 𝜑𝐴 = 𝐵 ) → 𝐴𝑃 )
21 9 adantr ( ( 𝜑𝐴 = 𝐵 ) → 𝐵𝑃 )
22 eqidd ( ( 𝜑𝐴 = 𝐵 ) → ( 𝐴 𝐵 ) = ( 𝐴 𝐵 ) )
23 simpr ( ( 𝜑𝐴 = 𝐵 ) → 𝐴 = 𝐵 )
24 1 2 3 19 21 21 tgbtwntriv1 ( ( 𝜑𝐴 = 𝐵 ) → 𝐵 ∈ ( 𝐵 𝐼 𝐵 ) )
25 23 24 eqeltrd ( ( 𝜑𝐴 = 𝐵 ) → 𝐴 ∈ ( 𝐵 𝐼 𝐵 ) )
26 1 2 3 4 5 19 20 8 21 21 22 25 ismir ( ( 𝜑𝐴 = 𝐵 ) → 𝐵 = ( 𝑀𝐵 ) )
27 26 eqcomd ( ( 𝜑𝐴 = 𝐵 ) → ( 𝑀𝐵 ) = 𝐵 )
28 18 27 impbida ( 𝜑 → ( ( 𝑀𝐵 ) = 𝐵𝐴 = 𝐵 ) )