Description: Point inversion preserves congruence. Theorem 7.16 of Schwabhauser p. 51. (Contributed by Thierry Arnoux, 30-Jul-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mirval.p | |- P = ( Base ` G ) |
|
mirval.d | |- .- = ( dist ` G ) |
||
mirval.i | |- I = ( Itv ` G ) |
||
mirval.l | |- L = ( LineG ` G ) |
||
mirval.s | |- S = ( pInvG ` G ) |
||
mirval.g | |- ( ph -> G e. TarskiG ) |
||
mirval.a | |- ( ph -> A e. P ) |
||
mirfv.m | |- M = ( S ` A ) |
||
miriso.1 | |- ( ph -> X e. P ) |
||
miriso.2 | |- ( ph -> Y e. P ) |
||
mircgrs.z | |- ( ph -> Z e. P ) |
||
mircgrs.t | |- ( ph -> T e. P ) |
||
mircgrs.e | |- ( ph -> ( X .- Y ) = ( Z .- T ) ) |
||
Assertion | mircgrs | |- ( ph -> ( ( M ` X ) .- ( M ` Y ) ) = ( ( M ` Z ) .- ( M ` T ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mirval.p | |- P = ( Base ` G ) |
|
2 | mirval.d | |- .- = ( dist ` G ) |
|
3 | mirval.i | |- I = ( Itv ` G ) |
|
4 | mirval.l | |- L = ( LineG ` G ) |
|
5 | mirval.s | |- S = ( pInvG ` G ) |
|
6 | mirval.g | |- ( ph -> G e. TarskiG ) |
|
7 | mirval.a | |- ( ph -> A e. P ) |
|
8 | mirfv.m | |- M = ( S ` A ) |
|
9 | miriso.1 | |- ( ph -> X e. P ) |
|
10 | miriso.2 | |- ( ph -> Y e. P ) |
|
11 | mircgrs.z | |- ( ph -> Z e. P ) |
|
12 | mircgrs.t | |- ( ph -> T e. P ) |
|
13 | mircgrs.e | |- ( ph -> ( X .- Y ) = ( Z .- T ) ) |
|
14 | 1 2 3 4 5 6 7 8 9 10 | miriso | |- ( ph -> ( ( M ` X ) .- ( M ` Y ) ) = ( X .- Y ) ) |
15 | 1 2 3 4 5 6 7 8 11 12 | miriso | |- ( ph -> ( ( M ` Z ) .- ( M ` T ) ) = ( Z .- T ) ) |
16 | 13 14 15 | 3eqtr4d | |- ( ph -> ( ( M ` X ) .- ( M ` Y ) ) = ( ( M ` Z ) .- ( M ` T ) ) ) |