Metamath Proof Explorer


Theorem tgcgrcoml

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 ) )

Proof

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 ) )