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 φ G 𝒢 Tarski
tgcgrcomr.a φ A P
tgcgrcomr.b φ B P
tgcgrcomr.c φ C P
tgcgrcomr.d φ D P
tgcgrcomr.6 φ A - ˙ B = C - ˙ D
Assertion tgcgrcoml φ 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 φ G 𝒢 Tarski
5 tgcgrcomr.a φ A P
6 tgcgrcomr.b φ B P
7 tgcgrcomr.c φ C P
8 tgcgrcomr.d φ D P
9 tgcgrcomr.6 φ A - ˙ B = C - ˙ D
10 1 2 3 4 5 6 axtgcgrrflx φ A - ˙ B = B - ˙ A
11 10 9 eqtr3d φ B - ˙ A = C - ˙ D