Metamath Proof Explorer

Theorem miduniq

Description: Uniqueness of the middle point, expressed with point inversion. Theorem 7.17 of Schwabhauser p. 51. (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 )
miduniq.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
miduniq.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
miduniq.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
miduniq.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
miduniq.e ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐴 ) ‘ 𝑋 ) = 𝑌 )
miduniq.f ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐵 ) ‘ 𝑋 ) = 𝑌 )
Assertion miduniq ( 𝜑 → 𝐴 = 𝐵 )

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 miduniq.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
8 miduniq.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
9 miduniq.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
10 miduniq.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
11 miduniq.e ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐴 ) ‘ 𝑋 ) = 𝑌 )
12 miduniq.f ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐵 ) ‘ 𝑋 ) = 𝑌 )
13 eqid ⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
14 eqid ⊢ ( 𝑆 ‘ 𝐴 ) = ( 𝑆 ‘ 𝐴 )
15 1 2 3 4 5 6 7 14 8 mircl ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐴 ) ‘ 𝐵 ) ∈ 𝑃 )
16 eqid ⊢ ( 𝑆 ‘ 𝐵 ) = ( 𝑆 ‘ 𝐵 )
17 1 2 3 4 5 6 8 16 9 mirbtwn ⊢ ( 𝜑 → 𝐵 ∈ ( ( ( 𝑆 ‘ 𝐵 ) ‘ 𝑋 ) 𝐼 𝑋 ) )
18 12 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝐵 ) ‘ 𝑋 ) 𝐼 𝑋 ) = ( 𝑌 𝐼 𝑋 ) )
19 17 18 eleqtrd ⊢ ( 𝜑 → 𝐵 ∈ ( 𝑌 𝐼 𝑋 ) )
20 1 2 3 6 10 8 9 19 tgbtwncom ⊢ ( 𝜑 → 𝐵 ∈ ( 𝑋 𝐼 𝑌 ) )
21 1 2 3 4 5 6 7 14 10 8 miriso ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝐴 ) ‘ 𝑌 ) − ( ( 𝑆 ‘ 𝐴 ) ‘ 𝐵 ) ) = ( 𝑌 − 𝐵 ) )
22 1 2 3 4 5 6 7 14 9 11 mircom ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐴 ) ‘ 𝑌 ) = 𝑋 )
23 22 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝐴 ) ‘ 𝑌 ) − ( ( 𝑆 ‘ 𝐴 ) ‘ 𝐵 ) ) = ( 𝑋 − ( ( 𝑆 ‘ 𝐴 ) ‘ 𝐵 ) ) )
24 1 2 3 4 5 6 8 16 9 mircgr ⊢ ( 𝜑 → ( 𝐵 − ( ( 𝑆 ‘ 𝐵 ) ‘ 𝑋 ) ) = ( 𝐵 − 𝑋 ) )
25 12 oveq2d ⊢ ( 𝜑 → ( 𝐵 − ( ( 𝑆 ‘ 𝐵 ) ‘ 𝑋 ) ) = ( 𝐵 − 𝑌 ) )
26 24 25 eqtr3d ⊢ ( 𝜑 → ( 𝐵 − 𝑋 ) = ( 𝐵 − 𝑌 ) )
27 26 eqcomd ⊢ ( 𝜑 → ( 𝐵 − 𝑌 ) = ( 𝐵 − 𝑋 ) )
28 1 2 3 6 8 10 8 9 27 tgcgrcomlr ⊢ ( 𝜑 → ( 𝑌 − 𝐵 ) = ( 𝑋 − 𝐵 ) )
29 21 23 28 3eqtr3rd ⊢ ( 𝜑 → ( 𝑋 − 𝐵 ) = ( 𝑋 − ( ( 𝑆 ‘ 𝐴 ) ‘ 𝐵 ) ) )
30 1 2 3 4 5 6 7 14 9 8 miriso ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝐴 ) ‘ 𝑋 ) − ( ( 𝑆 ‘ 𝐴 ) ‘ 𝐵 ) ) = ( 𝑋 − 𝐵 ) )
31 11 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝐴 ) ‘ 𝑋 ) − ( ( 𝑆 ‘ 𝐴 ) ‘ 𝐵 ) ) = ( 𝑌 − ( ( 𝑆 ‘ 𝐴 ) ‘ 𝐵 ) ) )
32 1 2 3 6 8 9 8 10 26 tgcgrcomlr ⊢ ( 𝜑 → ( 𝑋 − 𝐵 ) = ( 𝑌 − 𝐵 ) )
33 30 31 32 3eqtr3rd ⊢ ( 𝜑 → ( 𝑌 − 𝐵 ) = ( 𝑌 − ( ( 𝑆 ‘ 𝐴 ) ‘ 𝐵 ) ) )
34 1 4 3 6 9 10 8 13 15 7 2 20 29 33 tgidinside ⊢ ( 𝜑 → 𝐵 = ( ( 𝑆 ‘ 𝐴 ) ‘ 𝐵 ) )
35 34 eqcomd ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐴 ) ‘ 𝐵 ) = 𝐵 )
36 1 2 3 4 5 6 7 14 8 mirinv ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝐴 ) ‘ 𝐵 ) = 𝐵 ↔ 𝐴 = 𝐵 ) )
37 35 36 mpbid ⊢ ( 𝜑 → 𝐴 = 𝐵 )