Metamath Proof Explorer

Theorem mireq

Description: Equality deduction for point inversion. Theorem 7.9 of Schwabhauser p. 50. (Contributed by Thierry Arnoux, 30-May-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 ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
mireq.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
mireq.d ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐵 ) = ( 𝑀 ‘ 𝐶 ) )
Assertion mireq ( 𝜑 → 𝐵 = 𝐶 )

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 mireq.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
11 mireq.d ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐵 ) = ( 𝑀 ‘ 𝐶 ) )
12 1 2 3 4 5 6 7 8 10 mircl ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐶 ) ∈ 𝑃 )
13 1 2 3 4 5 6 7 8 9 mirfv ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐵 ) = ( ℩ 𝑧 ∈ 𝑃 ( ( 𝐴 − 𝑧 ) = ( 𝐴 − 𝐵 ) ∧ 𝐴 ∈ ( 𝑧 𝐼 𝐵 ) ) ) )
14 13 11 eqtr3d ⊢ ( 𝜑 → ( ℩ 𝑧 ∈ 𝑃 ( ( 𝐴 − 𝑧 ) = ( 𝐴 − 𝐵 ) ∧ 𝐴 ∈ ( 𝑧 𝐼 𝐵 ) ) ) = ( 𝑀 ‘ 𝐶 ) )
15 1 2 3 6 9 7 mirreu3 ⊢ ( 𝜑 → ∃! 𝑧 ∈ 𝑃 ( ( 𝐴 − 𝑧 ) = ( 𝐴 − 𝐵 ) ∧ 𝐴 ∈ ( 𝑧 𝐼 𝐵 ) ) )
16 oveq2 ⊢ ( 𝑧 = ( 𝑀 ‘ 𝐶 ) → ( 𝐴 − 𝑧 ) = ( 𝐴 − ( 𝑀 ‘ 𝐶 ) ) )
17 16 eqeq1d ⊢ ( 𝑧 = ( 𝑀 ‘ 𝐶 ) → ( ( 𝐴 − 𝑧 ) = ( 𝐴 − 𝐵 ) ↔ ( 𝐴 − ( 𝑀 ‘ 𝐶 ) ) = ( 𝐴 − 𝐵 ) ) )
18 oveq1 ⊢ ( 𝑧 = ( 𝑀 ‘ 𝐶 ) → ( 𝑧 𝐼 𝐵 ) = ( ( 𝑀 ‘ 𝐶 ) 𝐼 𝐵 ) )
19 18 eleq2d ⊢ ( 𝑧 = ( 𝑀 ‘ 𝐶 ) → ( 𝐴 ∈ ( 𝑧 𝐼 𝐵 ) ↔ 𝐴 ∈ ( ( 𝑀 ‘ 𝐶 ) 𝐼 𝐵 ) ) )
20 17 19 anbi12d ⊢ ( 𝑧 = ( 𝑀 ‘ 𝐶 ) → ( ( ( 𝐴 − 𝑧 ) = ( 𝐴 − 𝐵 ) ∧ 𝐴 ∈ ( 𝑧 𝐼 𝐵 ) ) ↔ ( ( 𝐴 − ( 𝑀 ‘ 𝐶 ) ) = ( 𝐴 − 𝐵 ) ∧ 𝐴 ∈ ( ( 𝑀 ‘ 𝐶 ) 𝐼 𝐵 ) ) ) )
21 20 riota2 ⊢ ( ( ( 𝑀 ‘ 𝐶 ) ∈ 𝑃 ∧ ∃! 𝑧 ∈ 𝑃 ( ( 𝐴 − 𝑧 ) = ( 𝐴 − 𝐵 ) ∧ 𝐴 ∈ ( 𝑧 𝐼 𝐵 ) ) ) → ( ( ( 𝐴 − ( 𝑀 ‘ 𝐶 ) ) = ( 𝐴 − 𝐵 ) ∧ 𝐴 ∈ ( ( 𝑀 ‘ 𝐶 ) 𝐼 𝐵 ) ) ↔ ( ℩ 𝑧 ∈ 𝑃 ( ( 𝐴 − 𝑧 ) = ( 𝐴 − 𝐵 ) ∧ 𝐴 ∈ ( 𝑧 𝐼 𝐵 ) ) ) = ( 𝑀 ‘ 𝐶 ) ) )
22 12 15 21 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐴 − ( 𝑀 ‘ 𝐶 ) ) = ( 𝐴 − 𝐵 ) ∧ 𝐴 ∈ ( ( 𝑀 ‘ 𝐶 ) 𝐼 𝐵 ) ) ↔ ( ℩ 𝑧 ∈ 𝑃 ( ( 𝐴 − 𝑧 ) = ( 𝐴 − 𝐵 ) ∧ 𝐴 ∈ ( 𝑧 𝐼 𝐵 ) ) ) = ( 𝑀 ‘ 𝐶 ) ) )
23 14 22 mpbird ⊢ ( 𝜑 → ( ( 𝐴 − ( 𝑀 ‘ 𝐶 ) ) = ( 𝐴 − 𝐵 ) ∧ 𝐴 ∈ ( ( 𝑀 ‘ 𝐶 ) 𝐼 𝐵 ) ) )
24 23 simpld ⊢ ( 𝜑 → ( 𝐴 − ( 𝑀 ‘ 𝐶 ) ) = ( 𝐴 − 𝐵 ) )
25 24 eqcomd ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐴 − ( 𝑀 ‘ 𝐶 ) ) )
26 23 simprd ⊢ ( 𝜑 → 𝐴 ∈ ( ( 𝑀 ‘ 𝐶 ) 𝐼 𝐵 ) )
27 1 2 3 6 12 7 9 26 tgbtwncom ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐵 𝐼 ( 𝑀 ‘ 𝐶 ) ) )
28 1 2 3 4 5 6 7 8 12 9 25 27 ismir ⊢ ( 𝜑 → 𝐵 = ( 𝑀 ‘ ( 𝑀 ‘ 𝐶 ) ) )
29 1 2 3 4 5 6 7 8 10 mirmir ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑀 ‘ 𝐶 ) ) = 𝐶 )
30 28 29 eqtrd ⊢ ( 𝜑 → 𝐵 = 𝐶 )