Description: Congruence commutes on the RHS. Variant of Theorem 2.5 of Schwabhauser p. 27, but in a convenient form for a common case. (Contributed by David A. Wheeler, 29-Jun-2020)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | tkgeom.p | |- P = ( Base ` G ) |
|
| tkgeom.d | |- .- = ( dist ` G ) |
||
| tkgeom.i | |- I = ( Itv ` G ) |
||
| tkgeom.g | |- ( ph -> G e. TarskiG ) |
||
| tgcgrcomr.a | |- ( ph -> A e. P ) |
||
| tgcgrcomr.b | |- ( ph -> B e. P ) |
||
| tgcgrcomr.c | |- ( ph -> C e. P ) |
||
| tgcgrcomr.d | |- ( ph -> D e. P ) |
||
| tgcgrcomr.6 | |- ( ph -> ( A .- B ) = ( C .- D ) ) |
||
| Assertion | tgcgrcomr | |- ( ph -> ( A .- B ) = ( D .- C ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | tkgeom.p | |- P = ( Base ` G ) |
|
| 2 | tkgeom.d | |- .- = ( dist ` G ) |
|
| 3 | tkgeom.i | |- I = ( Itv ` G ) |
|
| 4 | tkgeom.g | |- ( ph -> G e. TarskiG ) |
|
| 5 | tgcgrcomr.a | |- ( ph -> A e. P ) |
|
| 6 | tgcgrcomr.b | |- ( ph -> B e. P ) |
|
| 7 | tgcgrcomr.c | |- ( ph -> C e. P ) |
|
| 8 | tgcgrcomr.d | |- ( ph -> D e. P ) |
|
| 9 | tgcgrcomr.6 | |- ( ph -> ( A .- B ) = ( C .- D ) ) |
|
| 10 | 1 2 3 4 7 8 | axtgcgrrflx | |- ( ph -> ( C .- D ) = ( D .- C ) ) |
| 11 | 9 10 | eqtrd | |- ( ph -> ( A .- B ) = ( D .- C ) ) |