Theorem tgcgrcomlr 26886

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2104  ‘cfv 6458  (class class class)co 7307  Basecbs 16957  distcds 17016  TarskiGcstrkg 26833  Itvcitv 26839

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707  ax-nul 5239

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2942  df-ral 3063  df-rab 3287  df-v 3439  df-sbc 3722  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-br 5082  df-iota 6410  df-fv 6466  df-ov 7310  df-trkgc 26854  df-trkg 26859

This theorem is referenced by:  tgcgrextend  26891  tgifscgr  26914  tgcgrsub  26915  iscgrglt  26920  trgcgrg  26921  tgcgrxfr  26924  cgr3swap12  26929  cgr3swap23  26930  tgbtwnxfr  26936  lnext  26973  tgbtwnconn1lem1  26978  tgbtwnconn1lem2  26979  tgbtwnconn1lem3  26980  tgbtwnconn1  26981  legov2  26992  legtri3  26996  legbtwn  27000  tgcgrsub2  27001  miriso  27076  mircgrextend  27088  mirtrcgr  27089  miduniq  27091  colmid  27094  symquadlem  27095  krippenlem  27096  midexlem  27098  ragcom  27104  ragflat  27110  ragcgr  27113  footexALT  27124  footexlem1  27125  footexlem2  27126  colperpexlem1  27136  mideulem2  27140  opphllem  27141  opphllem3  27155  lmiisolem  27202  hypcgrlem1  27205  trgcopy  27210  trgcopyeulem  27211  iscgra1  27216  cgracgr  27224  cgraswap  27226  cgrcgra  27227  cgracom  27228  cgratr  27229  flatcgra  27230  dfcgra2  27236  acopy  27239  acopyeu  27240  cgrg3col4  27259  tgsas1  27260  tgsas3  27263  tgasa1  27264