Metamath Proof Explorer


Theorem miduniq1

Description: Uniqueness of the middle point, expressed with point inversion. Theorem 7.18 of Schwabhauser p. 52. (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 )
miduniq1.a ( 𝜑𝐴𝑃 )
miduniq1.b ( 𝜑𝐵𝑃 )
miduniq1.x ( 𝜑𝑋𝑃 )
miduniq1.e ( 𝜑 → ( ( 𝑆𝐴 ) ‘ 𝑋 ) = ( ( 𝑆𝐵 ) ‘ 𝑋 ) )
Assertion miduniq1 ( 𝜑𝐴 = 𝐵 )

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 miduniq1.a ( 𝜑𝐴𝑃 )
8 miduniq1.b ( 𝜑𝐵𝑃 )
9 miduniq1.x ( 𝜑𝑋𝑃 )
10 miduniq1.e ( 𝜑 → ( ( 𝑆𝐴 ) ‘ 𝑋 ) = ( ( 𝑆𝐵 ) ‘ 𝑋 ) )
11 eqid ( 𝑆𝐴 ) = ( 𝑆𝐴 )
12 1 2 3 4 5 6 7 11 9 mircl ( 𝜑 → ( ( 𝑆𝐴 ) ‘ 𝑋 ) ∈ 𝑃 )
13 eqidd ( 𝜑 → ( ( 𝑆𝐴 ) ‘ 𝑋 ) = ( ( 𝑆𝐴 ) ‘ 𝑋 ) )
14 10 eqcomd ( 𝜑 → ( ( 𝑆𝐵 ) ‘ 𝑋 ) = ( ( 𝑆𝐴 ) ‘ 𝑋 ) )
15 1 2 3 4 5 6 7 8 9 12 13 14 miduniq ( 𝜑𝐴 = 𝐵 )