Metamath Proof Explorer


Theorem mircgr

Description: Property of the image by the point inversion function. Definition 7.5 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 𝑀 = ( 𝑆𝐴 )
mirfv.b ( 𝜑𝐵𝑃 )
Assertion mircgr ( 𝜑 → ( 𝐴 ( 𝑀𝐵 ) ) = ( 𝐴 𝐵 ) )

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 mirfv.b ( 𝜑𝐵𝑃 )
10 1 2 3 4 5 6 7 8 9 mirfv ( 𝜑 → ( 𝑀𝐵 ) = ( 𝑧𝑃 ( ( 𝐴 𝑧 ) = ( 𝐴 𝐵 ) ∧ 𝐴 ∈ ( 𝑧 𝐼 𝐵 ) ) ) )
11 1 2 3 6 9 7 mirreu3 ( 𝜑 → ∃! 𝑧𝑃 ( ( 𝐴 𝑧 ) = ( 𝐴 𝐵 ) ∧ 𝐴 ∈ ( 𝑧 𝐼 𝐵 ) ) )
12 riotacl2 ( ∃! 𝑧𝑃 ( ( 𝐴 𝑧 ) = ( 𝐴 𝐵 ) ∧ 𝐴 ∈ ( 𝑧 𝐼 𝐵 ) ) → ( 𝑧𝑃 ( ( 𝐴 𝑧 ) = ( 𝐴 𝐵 ) ∧ 𝐴 ∈ ( 𝑧 𝐼 𝐵 ) ) ) ∈ { 𝑧𝑃 ∣ ( ( 𝐴 𝑧 ) = ( 𝐴 𝐵 ) ∧ 𝐴 ∈ ( 𝑧 𝐼 𝐵 ) ) } )
13 11 12 syl ( 𝜑 → ( 𝑧𝑃 ( ( 𝐴 𝑧 ) = ( 𝐴 𝐵 ) ∧ 𝐴 ∈ ( 𝑧 𝐼 𝐵 ) ) ) ∈ { 𝑧𝑃 ∣ ( ( 𝐴 𝑧 ) = ( 𝐴 𝐵 ) ∧ 𝐴 ∈ ( 𝑧 𝐼 𝐵 ) ) } )
14 10 13 eqeltrd ( 𝜑 → ( 𝑀𝐵 ) ∈ { 𝑧𝑃 ∣ ( ( 𝐴 𝑧 ) = ( 𝐴 𝐵 ) ∧ 𝐴 ∈ ( 𝑧 𝐼 𝐵 ) ) } )
15 oveq2 ( 𝑧 = ( 𝑀𝐵 ) → ( 𝐴 𝑧 ) = ( 𝐴 ( 𝑀𝐵 ) ) )
16 15 eqeq1d ( 𝑧 = ( 𝑀𝐵 ) → ( ( 𝐴 𝑧 ) = ( 𝐴 𝐵 ) ↔ ( 𝐴 ( 𝑀𝐵 ) ) = ( 𝐴 𝐵 ) ) )
17 oveq1 ( 𝑧 = ( 𝑀𝐵 ) → ( 𝑧 𝐼 𝐵 ) = ( ( 𝑀𝐵 ) 𝐼 𝐵 ) )
18 17 eleq2d ( 𝑧 = ( 𝑀𝐵 ) → ( 𝐴 ∈ ( 𝑧 𝐼 𝐵 ) ↔ 𝐴 ∈ ( ( 𝑀𝐵 ) 𝐼 𝐵 ) ) )
19 16 18 anbi12d ( 𝑧 = ( 𝑀𝐵 ) → ( ( ( 𝐴 𝑧 ) = ( 𝐴 𝐵 ) ∧ 𝐴 ∈ ( 𝑧 𝐼 𝐵 ) ) ↔ ( ( 𝐴 ( 𝑀𝐵 ) ) = ( 𝐴 𝐵 ) ∧ 𝐴 ∈ ( ( 𝑀𝐵 ) 𝐼 𝐵 ) ) ) )
20 19 elrab ( ( 𝑀𝐵 ) ∈ { 𝑧𝑃 ∣ ( ( 𝐴 𝑧 ) = ( 𝐴 𝐵 ) ∧ 𝐴 ∈ ( 𝑧 𝐼 𝐵 ) ) } ↔ ( ( 𝑀𝐵 ) ∈ 𝑃 ∧ ( ( 𝐴 ( 𝑀𝐵 ) ) = ( 𝐴 𝐵 ) ∧ 𝐴 ∈ ( ( 𝑀𝐵 ) 𝐼 𝐵 ) ) ) )
21 14 20 sylib ( 𝜑 → ( ( 𝑀𝐵 ) ∈ 𝑃 ∧ ( ( 𝐴 ( 𝑀𝐵 ) ) = ( 𝐴 𝐵 ) ∧ 𝐴 ∈ ( ( 𝑀𝐵 ) 𝐼 𝐵 ) ) ) )
22 21 simprld ( 𝜑 → ( 𝐴 ( 𝑀𝐵 ) ) = ( 𝐴 𝐵 ) )