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

Theorem axtgcgrid 22946
Description: Axiom of identity of congruence, Axiom A3 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 )
axtgcgrid.1  |-  ( ph  ->  X  e.  P )
axtgcgrid.2  |-  ( ph  ->  Y  e.  P )
axtgcgrid.3  |-  ( ph  ->  Z  e.  P )
axtgcgrid.4  |-  ( ph  ->  ( X  .-  Y
)  =  ( Z 
.-  Z ) )
Assertion
Ref Expression
axtgcgrid  |-  ( ph  ->  X  =  Y )

Proof of Theorem axtgcgrid
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 ) ) )
1312simprd 463 . . 3  |-  ( G  e. TarskiGC 
->  A. x  e.  P  A. y  e.  P  A. z  e.  P  ( ( x  .-  y )  =  ( z  .-  z )  ->  x  =  y ) )
147, 13syl 16 . 2  |-  ( ph  ->  A. x  e.  P  A. y  e.  P  A. z  e.  P  ( ( x  .-  y )  =  ( z  .-  z )  ->  x  =  y ) )
15 axtgcgrid.4 . 2  |-  ( ph  ->  ( X  .-  Y
)  =  ( Z 
.-  Z ) )
16 axtgcgrid.1 . . 3  |-  ( ph  ->  X  e.  P )
17 axtgcgrid.2 . . 3  |-  ( ph  ->  Y  e.  P )
18 axtgcgrid.3 . . 3  |-  ( ph  ->  Z  e.  P )
19 oveq1 6119 . . . . . 6  |-  ( x  =  X  ->  (
x  .-  y )  =  ( X  .-  y ) )
2019eqeq1d 2451 . . . . 5  |-  ( x  =  X  ->  (
( x  .-  y
)  =  ( z 
.-  z )  <->  ( X  .-  y )  =  ( z  .-  z ) ) )
21 eqeq1 2449 . . . . 5  |-  ( x  =  X  ->  (
x  =  y  <->  X  =  y ) )
2220, 21imbi12d 320 . . . 4  |-  ( x  =  X  ->  (
( ( x  .-  y )  =  ( z  .-  z )  ->  x  =  y )  <->  ( ( X 
.-  y )  =  ( z  .-  z
)  ->  X  =  y ) ) )
23 oveq2 6120 . . . . . 6  |-  ( y  =  Y  ->  ( X  .-  y )  =  ( X  .-  Y
) )
2423eqeq1d 2451 . . . . 5  |-  ( y  =  Y  ->  (
( X  .-  y
)  =  ( z 
.-  z )  <->  ( X  .-  Y )  =  ( z  .-  z ) ) )
25 eqeq2 2452 . . . . 5  |-  ( y  =  Y  ->  ( X  =  y  <->  X  =  Y ) )
2624, 25imbi12d 320 . . . 4  |-  ( y  =  Y  ->  (
( ( X  .-  y )  =  ( z  .-  z )  ->  X  =  y )  <->  ( ( X 
.-  Y )  =  ( z  .-  z
)  ->  X  =  Y ) ) )
27 id 22 . . . . . . 7  |-  ( z  =  Z  ->  z  =  Z )
2827, 27oveq12d 6130 . . . . . 6  |-  ( z  =  Z  ->  (
z  .-  z )  =  ( Z  .-  Z ) )
2928eqeq2d 2454 . . . . 5  |-  ( z  =  Z  ->  (
( X  .-  Y
)  =  ( z 
.-  z )  <->  ( X  .-  Y )  =  ( Z  .-  Z ) ) )
3029imbi1d 317 . . . 4  |-  ( z  =  Z  ->  (
( ( X  .-  Y )  =  ( z  .-  z )  ->  X  =  Y )  <->  ( ( X 
.-  Y )  =  ( Z  .-  Z
)  ->  X  =  Y ) ) )
3122, 26, 30rspc3v 3103 . . 3  |-  ( ( X  e.  P  /\  Y  e.  P  /\  Z  e.  P )  ->  ( A. x  e.  P  A. y  e.  P  A. z  e.  P  ( ( x 
.-  y )  =  ( z  .-  z
)  ->  x  =  y )  ->  (
( X  .-  Y
)  =  ( Z 
.-  Z )  ->  X  =  Y )
) )
3216, 17, 18, 31syl3anc 1218 . 2  |-  ( ph  ->  ( A. x  e.  P  A. y  e.  P  A. z  e.  P  ( ( x 
.-  y )  =  ( z  .-  z
)  ->  x  =  y )  ->  (
( X  .-  Y
)  =  ( Z 
.-  Z )  ->  X  =  Y )
) )
3314, 15, 32mp2d 45 1  |-  ( ph  ->  X  =  Y )
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:  tgcgreqb  22957  tgcgrtriv  22960  tgcgrextend  22961  tgsegconeq  22962  tgbtwntriv2  22963  tgbtwndiff  22981  tgifscgr  22983  tgbtwnxfr  23001  lnid  23024  tgidinside  23025  tgbtwnconn1lem2  23027  tgbtwnconn1lem3  23028  legtri3  23043  legeq  23046  legbtwn  23047  mirreu3  23080  colmid  23104  krippenlem  23106  f1otrg  23139
  Copyright terms: Public domain W3C validator