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

Theorem tgcgrcomlr 22934
Description: Congruence commutes on both sides. Theorem 2.5 of [Schwabhauser] p. 27. (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 22923 . 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 22923 . 2  |-  ( ph  ->  ( C  .-  D
)  =  ( D 
.-  C ) )
121, 8, 113eqtr3d 2483 1  |-  ( ph  ->  ( B  .-  A
)  =  ( D 
.-  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    e. wcel 1756   ` cfv 5418  (class class class)co 6091   Basecbs 14174   distcds 14247  TarskiGcstrkg 22889  Itvcitv 22897
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-nul 4421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-rab 2724  df-v 2974  df-sbc 3187  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-br 4293  df-iota 5381  df-fv 5426  df-ov 6094  df-trkgc 22909  df-trkg 22916
This theorem is referenced by:  tgcgrextend  22939  tgifscgr  22961  tgcgrsub  22962  trgcgrg  22967  tgcgrxfr  22970  cgr3swap12  22975  cgr3swap23  22976  tgbtwnxfr  22979  lnext  22999  tgbtwnconn1lem1  23004  tgbtwnconn1lem2  23005  tgbtwnconn1lem3  23006  tgbtwnconn1  23007  legov2  23017  legtri3  23021  legbtwn  23025  miriso  23073  miduniq  23079  colmid  23082  symquadlem  23083  krippenlem  23084  midexlem  23086  ragcom  23092  ragflat  23098  ragcgr  23101  footex  23109  colperplem1  23112
  Copyright terms: Public domain W3C validator