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

Theorem axtgcgrrflx 22945
Description: Axiom of reflexivity of congruence, Axiom A1 of [Schwabhauser] p. 10. (Contributed by Thierry Arnoux, 14-Mar-2019.)
Hypotheses
Ref Expression
axtrkg.p  |-  P  =  ( Base `  G
)
axtrkg.d  |-  .-  =  ( dist `  G )
axtrkg.i  |-  I  =  (Itv `  G )
axtrkg.g  |-  ( ph  ->  G  e. TarskiG )
axtgcgrrflx.1  |-  ( ph  ->  X  e.  P )
axtgcgrrflx.2  |-  ( ph  ->  Y  e.  P )
Assertion
Ref Expression
axtgcgrrflx  |-  ( ph  ->  ( X  .-  Y
)  =  ( Y 
.-  X ) )

Proof of Theorem axtgcgrrflx
Dummy variables  f 
i  p  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-trkg 22938 . . . . 5  |- TarskiG  =  ( (TarskiGC  i^i TarskiGB )  i^i  (TarskiGCB  i^i  {
f  |  [. ( Base `  f )  /  p ]. [. (Itv `  f )  /  i ]. (LineG `  f )  =  ( x  e.  p ,  y  e.  ( p  \  {
x } )  |->  { z  e.  p  |  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) } ) } ) )
2 inss1 3591 . . . . . 6  |-  ( (TarskiGC  i^i TarskiGB )  i^i  (TarskiGCB  i^i  { f  | 
[. ( Base `  f
)  /  p ]. [. (Itv `  f )  /  i ]. (LineG `  f )  =  ( x  e.  p ,  y  e.  ( p 
\  { x }
)  |->  { z  e.  p  |  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) } ) } ) )  C_  (TarskiGC  i^i TarskiGB )
3 inss1 3591 . . . . . 6  |-  (TarskiGC  i^i TarskiGB )  C_ TarskiGC
42, 3sstri 3386 . . . . 5  |-  ( (TarskiGC  i^i TarskiGB )  i^i  (TarskiGCB  i^i  { f  | 
[. ( Base `  f
)  /  p ]. [. (Itv `  f )  /  i ]. (LineG `  f )  =  ( x  e.  p ,  y  e.  ( p 
\  { x }
)  |->  { z  e.  p  |  ( z  e.  ( x i y )  \/  x  e.  ( z i y )  \/  y  e.  ( x i z ) ) } ) } ) )  C_ TarskiGC
51, 4eqsstri 3407 . . . 4  |- TarskiG  C_ TarskiGC
6 axtrkg.g . . . 4  |-  ( ph  ->  G  e. TarskiG )
75, 6sseldi 3375 . . 3  |-  ( ph  ->  G  e. TarskiGC )
8 axtrkg.p . . . . . 6  |-  P  =  ( Base `  G
)
9 axtrkg.d . . . . . 6  |-  .-  =  ( dist `  G )
10 axtrkg.i . . . . . 6  |-  I  =  (Itv `  G )
118, 9, 10istrkgc 22939 . . . . 5  |-  ( G  e. TarskiGC  <->  ( G  e.  _V  /\  ( A. x  e.  P  A. y  e.  P  ( x  .-  y )  =  ( y  .-  x )  /\  A. x  e.  P  A. y  e.  P  A. z  e.  P  (
( x  .-  y
)  =  ( z 
.-  z )  ->  x  =  y )
) ) )
1211simprbi 464 . . . 4  |-  ( G  e. TarskiGC 
->  ( A. x  e.  P  A. y  e.  P  ( x  .-  y )  =  ( y  .-  x )  /\  A. x  e.  P  A. y  e.  P  A. z  e.  P  ( ( x 
.-  y )  =  ( z  .-  z
)  ->  x  =  y ) ) )
1312simpld 459 . . 3  |-  ( G  e. TarskiGC 
->  A. x  e.  P  A. y  e.  P  ( x  .-  y )  =  ( y  .-  x ) )
147, 13syl 16 . 2  |-  ( ph  ->  A. x  e.  P  A. y  e.  P  ( x  .-  y )  =  ( y  .-  x ) )
15 axtgcgrrflx.1 . . 3  |-  ( ph  ->  X  e.  P )
16 axtgcgrrflx.2 . . 3  |-  ( ph  ->  Y  e.  P )
17 oveq1 6119 . . . . 5  |-  ( x  =  X  ->  (
x  .-  y )  =  ( X  .-  y ) )
18 oveq2 6120 . . . . 5  |-  ( x  =  X  ->  (
y  .-  x )  =  ( y  .-  X ) )
1917, 18eqeq12d 2457 . . . 4  |-  ( x  =  X  ->  (
( x  .-  y
)  =  ( y 
.-  x )  <->  ( X  .-  y )  =  ( y  .-  X ) ) )
20 oveq2 6120 . . . . 5  |-  ( y  =  Y  ->  ( X  .-  y )  =  ( X  .-  Y
) )
21 oveq1 6119 . . . . 5  |-  ( y  =  Y  ->  (
y  .-  X )  =  ( Y  .-  X ) )
2220, 21eqeq12d 2457 . . . 4  |-  ( y  =  Y  ->  (
( X  .-  y
)  =  ( y 
.-  X )  <->  ( X  .-  Y )  =  ( Y  .-  X ) ) )
2319, 22rspc2v 3100 . . 3  |-  ( ( X  e.  P  /\  Y  e.  P )  ->  ( A. x  e.  P  A. y  e.  P  ( x  .-  y )  =  ( y  .-  x )  ->  ( X  .-  Y )  =  ( Y  .-  X ) ) )
2415, 16, 23syl2anc 661 . 2  |-  ( ph  ->  ( A. x  e.  P  A. y  e.  P  ( x  .-  y )  =  ( y  .-  x )  ->  ( X  .-  Y )  =  ( Y  .-  X ) ) )
2514, 24mpd 15 1  |-  ( ph  ->  ( X  .-  Y
)  =  ( Y 
.-  X ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    \/ w3o 964    = wceq 1369    e. wcel 1756   {cab 2429   A.wral 2736   {crab 2740   _Vcvv 2993   [.wsbc 3207    \ cdif 3346    i^i cin 3348   {csn 3898   ` cfv 5439  (class class class)co 6112    e. cmpt2 6114   Basecbs 14195   distcds 14268  TarskiGcstrkg 22911  TarskiGCcstrkgc 22912  TarskiGBcstrkgb 22913  TarskiGCBcstrkgcb 22914  Itvcitv 22919  LineGclng 22920
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 4442
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 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-rab 2745  df-v 2995  df-sbc 3208  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-sn 3899  df-pr 3901  df-op 3905  df-uni 4113  df-br 4314  df-iota 5402  df-fv 5447  df-ov 6115  df-trkgc 22931  df-trkg 22938
This theorem is referenced by:  tgcgrcomlr  22956  tgbtwnconn1lem1  23026  tgbtwnconn1lem2  23027  tgbtwnconn1lem3  23028  miriso  23095  symquadlem  23105  midexlem  23108  footex  23131  colperplem1  23134  f1otrg  23139
  Copyright terms: Public domain W3C validator