Theorem tgcgrcomlr 28972

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  ‘cfv 6558  (class class class)co 7443  Basecbs 17416  distcds 17466  TarskiGcstrkg 28919  Itvcitv 28925

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-nul 5263

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6512  df-fv 6566  df-ov 7446  df-trkgc 28940  df-trkg 28945

This theorem is used by:  tgcgrextend  28977  tgifscgr  29001  tgcgrsub  29002  iscgrglt  29007  trgcgrg  29008  tgcgrxfr  29011  cgr3swap12  29016  cgr3swap23  29017  tgbtwnxfr  29023  lnext  29060  tgbtwnconn1lem1  29065  tgbtwnconn1lem2  29066  tgbtwnconn1lem3  29067  tgbtwnconn1  29068  legov2  29079  legtri3  29083  legbtwn  29087  tgcgrsub2  29088  miriso  29172  mircgrextend  29184  mirtrcgr  29185  miduniq  29187  colmid  29190  symquadlem  29191  krippenlem  29192  midexlem  29194  ragcom  29203  ragflat  29209  ragcgr  29212  footexALT  29223  footexlem1  29224  footexlem2  29225  colperpexlem1  29236  mideulem2  29240  opphllem  29241  opphllem3  29255  lmiisolem  29331  symquadmid  29334  hypcgrlem1  29335  trgcopy  29341  trgcopyeulem  29342  iscgra1  29347  cgracgr  29355  cgraswap  29357  cgrcgra  29358  cgracom  29359  cgratr  29360  zerocgra  29361  flatcgra  29362  dfcgra2  29368  acopy  29371  acopyeu  29372  ragcgra  29373  ragsupplcgra  29375  tgaaddcpbllem1  29379  cgrg3col4  29402  angmgmaddeu1  29409  tgsas1  29429  tgsas3  29432  tgasa1  29433  symquadprlng  29470  tgaltai  29475  cgrahlb  33077  iscgrag  33082  cgrgptxfr  33083