Description: Congruence commutes on the LHS. 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 | tgcgrcoml | |- ( ph -> ( B .- A ) = ( C .- D ) ) |
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 5 6 | axtgcgrrflx | |- ( ph -> ( A .- B ) = ( B .- A ) ) |
11 | 10 9 | eqtr3d | |- ( ph -> ( B .- A ) = ( C .- D ) ) |