Metamath Proof Explorer

Theorem mirreu

Description: Any point has a unique antecedent through point inversion. Theorem 7.8 of Schwabhauser p. 50. (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 mirreu ( 𝜑 → ∃! 𝑎 ∈ 𝑃 ( 𝑀 ‘ 𝑎 ) = 𝐵 )

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 mirmir ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑀 ‘ 𝐵 ) ) = 𝐵 )
12 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ ( 𝑀 ‘ 𝑎 ) = 𝐵 ) → 𝐺 ∈ TarskiG )
13 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ ( 𝑀 ‘ 𝑎 ) = 𝐵 ) → 𝐴 ∈ 𝑃 )
14 simplr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ ( 𝑀 ‘ 𝑎 ) = 𝐵 ) → 𝑎 ∈ 𝑃 )
15 1 2 3 4 5 12 13 8 14 mirmir ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ ( 𝑀 ‘ 𝑎 ) = 𝐵 ) → ( 𝑀 ‘ ( 𝑀 ‘ 𝑎 ) ) = 𝑎 )
16 simpr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ ( 𝑀 ‘ 𝑎 ) = 𝐵 ) → ( 𝑀 ‘ 𝑎 ) = 𝐵 )
17 16 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ ( 𝑀 ‘ 𝑎 ) = 𝐵 ) → ( 𝑀 ‘ ( 𝑀 ‘ 𝑎 ) ) = ( 𝑀 ‘ 𝐵 ) )
18 15 17 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ ( 𝑀 ‘ 𝑎 ) = 𝐵 ) → 𝑎 = ( 𝑀 ‘ 𝐵 ) )
19 18 ex ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) → ( ( 𝑀 ‘ 𝑎 ) = 𝐵 → 𝑎 = ( 𝑀 ‘ 𝐵 ) ) )
20 19 ralrimiva ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑃 ( ( 𝑀 ‘ 𝑎 ) = 𝐵 → 𝑎 = ( 𝑀 ‘ 𝐵 ) ) )
21 fveqeq2 ⊢ ( 𝑎 = ( 𝑀 ‘ 𝐵 ) → ( ( 𝑀 ‘ 𝑎 ) = 𝐵 ↔ ( 𝑀 ‘ ( 𝑀 ‘ 𝐵 ) ) = 𝐵 ) )
22 21 eqreu ⊢ ( ( ( 𝑀 ‘ 𝐵 ) ∈ 𝑃 ∧ ( 𝑀 ‘ ( 𝑀 ‘ 𝐵 ) ) = 𝐵 ∧ ∀ 𝑎 ∈ 𝑃 ( ( 𝑀 ‘ 𝑎 ) = 𝐵 → 𝑎 = ( 𝑀 ‘ 𝐵 ) ) ) → ∃! 𝑎 ∈ 𝑃 ( 𝑀 ‘ 𝑎 ) = 𝐵 )
23 10 11 20 22 syl3anc ⊢ ( 𝜑 → ∃! 𝑎 ∈ 𝑃 ( 𝑀 ‘ 𝑎 ) = 𝐵 )