Description: Point inversion preserves congruence. Theorem 7.16 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 ) | ||
mirval.a | ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 ) | ||
mirfv.m | ⊢ 𝑀 = ( 𝑆 ‘ 𝐴 ) | ||
miriso.1 | ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 ) | ||
miriso.2 | ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 ) | ||
mircgrs.z | ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 ) | ||
mircgrs.t | ⊢ ( 𝜑 → 𝑇 ∈ 𝑃 ) | ||
mircgrs.e | ⊢ ( 𝜑 → ( 𝑋 − 𝑌 ) = ( 𝑍 − 𝑇 ) ) | ||
Assertion | mircgrs | ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑋 ) − ( 𝑀 ‘ 𝑌 ) ) = ( ( 𝑀 ‘ 𝑍 ) − ( 𝑀 ‘ 𝑇 ) ) ) |
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 | miriso.1 | ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 ) | |
10 | miriso.2 | ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 ) | |
11 | mircgrs.z | ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 ) | |
12 | mircgrs.t | ⊢ ( 𝜑 → 𝑇 ∈ 𝑃 ) | |
13 | mircgrs.e | ⊢ ( 𝜑 → ( 𝑋 − 𝑌 ) = ( 𝑍 − 𝑇 ) ) | |
14 | 1 2 3 4 5 6 7 8 9 10 | miriso | ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑋 ) − ( 𝑀 ‘ 𝑌 ) ) = ( 𝑋 − 𝑌 ) ) |
15 | 1 2 3 4 5 6 7 8 11 12 | miriso | ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑍 ) − ( 𝑀 ‘ 𝑇 ) ) = ( 𝑍 − 𝑇 ) ) |
16 | 13 14 15 | 3eqtr4d | ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑋 ) − ( 𝑀 ‘ 𝑌 ) ) = ( ( 𝑀 ‘ 𝑍 ) − ( 𝑀 ‘ 𝑇 ) ) ) |