MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tgcgrcomlr Structured version   Unicode version

Theorem tgcgrcomlr 24072
Description: Congruence commutes on both sides. (Contributed by Thierry Arnoux, 23-Mar-2019.)
Hypotheses
Ref Expression
tkgeom.p  |-  P  =  ( Base `  G
)
tkgeom.d  |-  .-  =  ( dist `  G )
tkgeom.i  |-  I  =  (Itv `  G )
tkgeom.g  |-  ( ph  ->  G  e. TarskiG )
tgcgrcomlr.a  |-  ( ph  ->  A  e.  P )
tgcgrcomlr.b  |-  ( ph  ->  B  e.  P )
tgcgrcomlr.c  |-  ( ph  ->  C  e.  P )
tgcgrcomlr.d  |-  ( ph  ->  D  e.  P )
tgcgrcomlr.6  |-  ( ph  ->  ( A  .-  B
)  =  ( C 
.-  D ) )
Assertion
Ref Expression
tgcgrcomlr  |-  ( ph  ->  ( B  .-  A
)  =  ( D 
.-  C ) )

Proof of Theorem tgcgrcomlr
StepHypRef Expression
1 tgcgrcomlr.6 . 2  |-  ( ph  ->  ( A  .-  B
)  =  ( C 
.-  D ) )
2 tkgeom.p . . 3  |-  P  =  ( Base `  G
)
3 tkgeom.d . . 3  |-  .-  =  ( dist `  G )
4 tkgeom.i . . 3  |-  I  =  (Itv `  G )
5 tkgeom.g . . 3  |-  ( ph  ->  G  e. TarskiG )
6 tgcgrcomlr.a . . 3  |-  ( ph  ->  A  e.  P )
7 tgcgrcomlr.b . . 3  |-  ( ph  ->  B  e.  P )
82, 3, 4, 5, 6, 7axtgcgrrflx 24057 . 2  |-  ( ph  ->  ( A  .-  B
)  =  ( B 
.-  A ) )
9 tgcgrcomlr.c . . 3  |-  ( ph  ->  C  e.  P )
10 tgcgrcomlr.d . . 3  |-  ( ph  ->  D  e.  P )
112, 3, 4, 5, 9, 10axtgcgrrflx 24057 . 2  |-  ( ph  ->  ( C  .-  D
)  =  ( D 
.-  C ) )
121, 8, 113eqtr3d 2503 1  |-  ( ph  ->  ( B  .-  A
)  =  ( D 
.-  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1398    e. wcel 1823   ` cfv 5570  (class class class)co 6270   Basecbs 14716   distcds 14793  TarskiGcstrkg 24023  Itvcitv 24030
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-nul 4568
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-iota 5534  df-fv 5578  df-ov 6273  df-trkgc 24042  df-trkg 24048
This theorem is referenced by:  tgcgrextend  24077  tgifscgr  24101  tgcgrsub  24102  trgcgrg  24107  tgcgrxfr  24110  cgr3swap12  24115  cgr3swap23  24116  tgbtwnxfr  24119  lnext  24155  tgbtwnconn1lem1  24160  tgbtwnconn1lem2  24161  tgbtwnconn1lem3  24162  tgbtwnconn1  24163  legov2  24174  legtri3  24178  legbtwn  24182  miriso  24251  miduniq  24263  colmid  24266  symquadlem  24267  krippenlem  24268  midexlem  24270  ragcom  24276  ragflat  24282  ragcgr  24285  footex  24296  colperpexlem1  24305  mideulem2  24309  opphllem  24310  opphllem3  24322  lmiisolem  24362  hypcgrlem1  24365
  Copyright terms: Public domain W3C validator