Theorem tgcgrcomlr 28876

Description: Congruence commutes on both sides. (Contributed by Thierry Arnoux, 23-Mar-2019.)

Hypotheses

Ref	Expression
tkgeom.p	⊢ 𝑃 = (Base‘𝐺)
tkgeom.d	⊢ − = (dist‘𝐺)
tkgeom.i	⊢ 𝐼 = (Itv‘𝐺)
tkgeom.g	⊢ (𝜑 → 𝐺 ∈ TarskiG)
tgcgrcomlr.a	⊢ (𝜑 → 𝐴 ∈ 𝑃)
tgcgrcomlr.b	⊢ (𝜑 → 𝐵 ∈ 𝑃)
tgcgrcomlr.c	⊢ (𝜑 → 𝐶 ∈ 𝑃)
tgcgrcomlr.d	⊢ (𝜑 → 𝐷 ∈ 𝑃)
tgcgrcomlr.6	⊢ (𝜑 → (𝐴 − 𝐵) = (𝐶 − 𝐷))

Assertion

Ref	Expression
tgcgrcomlr	⊢ (𝜑 → (𝐵 − 𝐴) = (𝐷 − 𝐶))

Proof of Theorem tgcgrcomlr

Step	Hyp	Ref	Expression
1		tgcgrcomlr.6	. 2 ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐶 − 𝐷))
2		tkgeom.p	. . 3 ⊢ 𝑃 = (Base‘𝐺)
3		tkgeom.d	. . 3 ⊢ − = (dist‘𝐺)
4		tkgeom.i	. . 3 ⊢ 𝐼 = (Itv‘𝐺)
5		tkgeom.g	. . 3 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
6		tgcgrcomlr.a	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
7		tgcgrcomlr.b	. . 3 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
8	2, 3, 4, 5, 6, 7	axtgcgrrflx 28858	. 2 ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐵 − 𝐴))
9		tgcgrcomlr.c	. . 3 ⊢ (𝜑 → 𝐶 ∈ 𝑃)
10		tgcgrcomlr.d	. . 3 ⊢ (𝜑 → 𝐷 ∈ 𝑃)
11	2, 3, 4, 5, 9, 10	axtgcgrrflx 28858	. 2 ⊢ (𝜑 → (𝐶 − 𝐷) = (𝐷 − 𝐶))
12	1, 8, 11	3eqtr3d 2803	1 ⊢ (𝜑 → (𝐵 − 𝐴) = (𝐷 − 𝐶))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ‘cfv 6527  (class class class)co 7408  Basecbs 17349  distcds 17399  TarskiGcstrkg 28823  Itvcitv 28829

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-nul 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rab 3413  df-v 3452  df-sbc 3739  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-iota 6483  df-fv 6535  df-ov 7411  df-trkgc 28844  df-trkg 28849

This theorem is used by:  tgcgrextend  28881  tgifscgr  28905  tgcgrsub  28906  iscgrglt  28911  trgcgrg  28912  tgcgrxfr  28915  cgr3swap12  28920  cgr3swap23  28921  tgbtwnxfr  28927  lnext  28964  tgbtwnconn1lem1  28969  tgbtwnconn1lem2  28970  tgbtwnconn1lem3  28971  tgbtwnconn1  28972  legov2  28983  legtri3  28987  legbtwn  28991  tgcgrsub2  28992  miriso  29076  mircgrextend  29088  mirtrcgr  29089  miduniq  29091  colmid  29094  symquadlem  29095  krippenlem  29096  midexlem  29098  ragcom  29107  ragflat  29113  ragcgr  29116  footexALT  29127  footexlem1  29128  footexlem2  29129  colperpexlem1  29140  mideulem2  29144  opphllem  29145  opphllem3  29159  lmiisolem  29235  symquadmid  29238  hypcgrlem1  29239  trgcopy  29245  trgcopyeulem  29246  iscgra1  29251  cgracgr  29259  cgraswap  29261  cgrcgra  29262  cgracom  29263  cgratr  29264  zerocgra  29265  flatcgra  29266  dfcgra2  29272  acopy  29275  acopyeu  29276  ragcgra  29277  ragsupplcgra  29279  tgaaddcpbllem1  29283  cgrg3col4  29306  angmgmaddeu1  29313  tgsas1  29333  tgsas3  29336  tgasa1  29337  symquadprlng  29374  tgaltai  29379