Theorem tgcgrcomlr 28943

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 28925	. 2 ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐵 − 𝐴))
9		tgcgrcomlr.c	. . 3 ⊢ (𝜑 → 𝐶 ∈ 𝑃)
10		tgcgrcomlr.d	. . 3 ⊢ (𝜑 → 𝐷 ∈ 𝑃)
11	2, 3, 4, 5, 9, 10	axtgcgrrflx 28925	. 2 ⊢ (𝜑 → (𝐶 − 𝐷) = (𝐷 − 𝐶))
12	1, 8, 11	3eqtr3d 2803	1 ⊢ (𝜑 → (𝐵 − 𝐴) = (𝐷 − 𝐶))

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  ‘cfv 6538  (class class class)co 7420  Basecbs 17388  distcds 17438  TarskiGcstrkg 28890  Itvcitv 28896

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  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 1572  df-fal 1582  df-ex 1812  df-sb 2099  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-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423  df-trkgc 28911  df-trkg 28916

This theorem is used by:  tgcgrextend  28948  tgifscgr  28972  tgcgrsub  28973  iscgrglt  28978  trgcgrg  28979  tgcgrxfr  28982  cgr3swap12  28987  cgr3swap23  28988  tgbtwnxfr  28994  lnext  29031  tgbtwnconn1lem1  29036  tgbtwnconn1lem2  29037  tgbtwnconn1lem3  29038  tgbtwnconn1  29039  legov2  29050  legtri3  29054  legbtwn  29058  tgcgrsub2  29059  miriso  29143  mircgrextend  29155  mirtrcgr  29156  miduniq  29158  colmid  29161  symquadlem  29162  krippenlem  29163  midexlem  29165  ragcom  29174  ragflat  29180  ragcgr  29183  footexALT  29194  footexlem1  29195  footexlem2  29196  colperpexlem1  29207  mideulem2  29211  opphllem  29212  opphllem3  29226  lmiisolem  29302  symquadmid  29305  hypcgrlem1  29306  trgcopy  29312  trgcopyeulem  29313  iscgra1  29318  cgracgr  29326  cgraswap  29328  cgrcgra  29329  cgracom  29330  cgratr  29331  zerocgra  29332  flatcgra  29333  dfcgra2  29339  acopy  29342  acopyeu  29343  ragcgra  29344  ragsupplcgra  29346  tgaaddcpbllem1  29350  cgrg3col4  29373  angmgmaddeu1  29380  tgsas1  29400  tgsas3  29403  tgasa1  29404  symquadprlng  29441  tgaltai  29446  cgrahlb  33048  iscgrag  33053  cgrgptxfr  33054