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=BaseG
tkgeom.d -˙=distG
tkgeom.i I=ItvG
tkgeom.g φG𝒢Tarski
tgcgrcomr.a φAP
tgcgrcomr.b φBP
tgcgrcomr.c φCP
tgcgrcomr.d φDP
tgcgrcomr.6 φA-˙B=C-˙D
Assertion tgcgrcoml φB-˙A=C-˙D

Proof

Step Hyp Ref Expression
1 tkgeom.p P=BaseG
2 tkgeom.d -˙=distG
3 tkgeom.i I=ItvG
4 tkgeom.g φG𝒢Tarski
5 tgcgrcomr.a φAP
6 tgcgrcomr.b φBP
7 tgcgrcomr.c φCP
8 tgcgrcomr.d φDP
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