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

Theorem axtgsegcon 24375
Description: Axiom of segment construction, Axiom A4 of [Schwabhauser] p. 11. As discussed in Axiom 4 of [Tarski1999] p. 178, "The intuitive content [is that] given any line segment  A B, one can construct a line segment congruent to it, starting at any point  Y and going in the direction of any ray containing  Y. The ray is determined by the point  Y and a second point  X, the endpoint of the ray. The other endpoint of the line segment to be constructed is just the point  z whose existence is asserted." (Contributed by Thierry Arnoux, 15-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 )
axtgsegcon.1  |-  ( ph  ->  X  e.  P )
axtgsegcon.2  |-  ( ph  ->  Y  e.  P )
axtgsegcon.3  |-  ( ph  ->  A  e.  P )
axtgsegcon.4  |-  ( ph  ->  B  e.  P )
Assertion
Ref Expression
axtgsegcon  |-  ( ph  ->  E. z  e.  P  ( Y  e.  ( X I z )  /\  ( Y  .-  z )  =  ( A  .-  B ) ) )
Distinct variable groups:    z, A    z, B    z, I    z, P    z, X    z, Y    z, 
.-
Allowed substitution hints:    ph( z)    G( z)

Proof of Theorem axtgsegcon
Dummy variables  f 
i  p  x  y  a  b  c  v  u are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-trkg 24364 . . . . . 6  |- 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 inss2 3689 . . . . . . 7  |-  ( (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_  (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 ) ) } ) } )
3 inss1 3688 . . . . . . 7  |-  (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_ TarskiGCB
42, 3sstri 3479 . . . . . 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_ TarskiGCB
51, 4eqsstri 3500 . . . . 5  |- TarskiG  C_ TarskiGCB
6 axtrkg.g . . . . 5  |-  ( ph  ->  G  e. TarskiG )
75, 6sseldi 3468 . . . 4  |-  ( ph  ->  G  e. TarskiGCB )
8 axtrkg.p . . . . . . 7  |-  P  =  ( Base `  G
)
9 axtrkg.d . . . . . . 7  |-  .-  =  ( dist `  G )
10 axtrkg.i . . . . . . 7  |-  I  =  (Itv `  G )
118, 9, 10istrkgcb 24367 . . . . . 6  |-  ( G  e. TarskiGCB  <->  ( G  e.  _V  /\  ( A. x  e.  P  A. y  e.  P  A. z  e.  P  A. u  e.  P  A. a  e.  P  A. b  e.  P  A. c  e.  P  A. v  e.  P  ( ( ( x  =/=  y  /\  y  e.  ( x I z )  /\  b  e.  ( a I c ) )  /\  (
( ( x  .-  y )  =  ( a  .-  b )  /\  ( y  .-  z )  =  ( b  .-  c ) )  /\  ( ( x  .-  u )  =  ( a  .-  v )  /\  (
y  .-  u )  =  ( b  .-  v ) ) ) )  ->  ( z  .-  u )  =  ( c  .-  v ) )  /\  A. x  e.  P  A. y  e.  P  A. a  e.  P  A. b  e.  P  E. z  e.  P  ( y  e.  ( x I z )  /\  ( y 
.-  z )  =  ( a  .-  b
) ) ) ) )
1211simprbi 465 . . . . 5  |-  ( G  e. TarskiGCB 
->  ( A. x  e.  P  A. y  e.  P  A. z  e.  P  A. u  e.  P  A. a  e.  P  A. b  e.  P  A. c  e.  P  A. v  e.  P  ( ( ( x  =/=  y  /\  y  e.  ( x I z )  /\  b  e.  ( a
I c ) )  /\  ( ( ( x  .-  y )  =  ( a  .-  b )  /\  (
y  .-  z )  =  ( b  .-  c ) )  /\  ( ( x  .-  u )  =  ( a  .-  v )  /\  ( y  .-  u )  =  ( b  .-  v ) ) ) )  -> 
( z  .-  u
)  =  ( c 
.-  v ) )  /\  A. x  e.  P  A. y  e.  P  A. a  e.  P  A. b  e.  P  E. z  e.  P  ( y  e.  ( x I z )  /\  ( y 
.-  z )  =  ( a  .-  b
) ) ) )
1312simprd 464 . . . 4  |-  ( G  e. TarskiGCB 
->  A. x  e.  P  A. y  e.  P  A. a  e.  P  A. b  e.  P  E. z  e.  P  ( y  e.  ( x I z )  /\  ( y  .-  z )  =  ( a  .-  b ) ) )
147, 13syl 17 . . 3  |-  ( ph  ->  A. x  e.  P  A. y  e.  P  A. a  e.  P  A. b  e.  P  E. z  e.  P  ( y  e.  ( x I z )  /\  ( y  .-  z )  =  ( a  .-  b ) ) )
15 axtgsegcon.1 . . . 4  |-  ( ph  ->  X  e.  P )
16 axtgsegcon.2 . . . 4  |-  ( ph  ->  Y  e.  P )
17 oveq1 6312 . . . . . . . . 9  |-  ( x  =  X  ->  (
x I z )  =  ( X I z ) )
1817eleq2d 2499 . . . . . . . 8  |-  ( x  =  X  ->  (
y  e.  ( x I z )  <->  y  e.  ( X I z ) ) )
1918anbi1d 709 . . . . . . 7  |-  ( x  =  X  ->  (
( y  e.  ( x I z )  /\  ( y  .-  z )  =  ( a  .-  b ) )  <->  ( y  e.  ( X I z )  /\  ( y 
.-  z )  =  ( a  .-  b
) ) ) )
2019rexbidv 2946 . . . . . 6  |-  ( x  =  X  ->  ( E. z  e.  P  ( y  e.  ( x I z )  /\  ( y  .-  z )  =  ( a  .-  b ) )  <->  E. z  e.  P  ( y  e.  ( X I z )  /\  ( y  .-  z )  =  ( a  .-  b ) ) ) )
21202ralbidv 2876 . . . . 5  |-  ( x  =  X  ->  ( A. a  e.  P  A. b  e.  P  E. z  e.  P  ( y  e.  ( x I z )  /\  ( y  .-  z )  =  ( a  .-  b ) )  <->  A. a  e.  P  A. b  e.  P  E. z  e.  P  ( y  e.  ( X I z )  /\  ( y  .-  z )  =  ( a  .-  b ) ) ) )
22 eleq1 2501 . . . . . . . 8  |-  ( y  =  Y  ->  (
y  e.  ( X I z )  <->  Y  e.  ( X I z ) ) )
23 oveq1 6312 . . . . . . . . 9  |-  ( y  =  Y  ->  (
y  .-  z )  =  ( Y  .-  z ) )
2423eqeq1d 2431 . . . . . . . 8  |-  ( y  =  Y  ->  (
( y  .-  z
)  =  ( a 
.-  b )  <->  ( Y  .-  z )  =  ( a  .-  b ) ) )
2522, 24anbi12d 715 . . . . . . 7  |-  ( y  =  Y  ->  (
( y  e.  ( X I z )  /\  ( y  .-  z )  =  ( a  .-  b ) )  <->  ( Y  e.  ( X I z )  /\  ( Y 
.-  z )  =  ( a  .-  b
) ) ) )
2625rexbidv 2946 . . . . . 6  |-  ( y  =  Y  ->  ( E. z  e.  P  ( y  e.  ( X I z )  /\  ( y  .-  z )  =  ( a  .-  b ) )  <->  E. z  e.  P  ( Y  e.  ( X I z )  /\  ( Y  .-  z )  =  ( a  .-  b ) ) ) )
27262ralbidv 2876 . . . . 5  |-  ( y  =  Y  ->  ( A. a  e.  P  A. b  e.  P  E. z  e.  P  ( y  e.  ( X I z )  /\  ( y  .-  z )  =  ( a  .-  b ) )  <->  A. a  e.  P  A. b  e.  P  E. z  e.  P  ( Y  e.  ( X I z )  /\  ( Y  .-  z )  =  ( a  .-  b ) ) ) )
2821, 27rspc2v 3197 . . . 4  |-  ( ( X  e.  P  /\  Y  e.  P )  ->  ( A. x  e.  P  A. y  e.  P  A. a  e.  P  A. b  e.  P  E. z  e.  P  ( y  e.  ( x I z )  /\  ( y 
.-  z )  =  ( a  .-  b
) )  ->  A. a  e.  P  A. b  e.  P  E. z  e.  P  ( Y  e.  ( X I z )  /\  ( Y 
.-  z )  =  ( a  .-  b
) ) ) )
2915, 16, 28syl2anc 665 . . 3  |-  ( ph  ->  ( A. x  e.  P  A. y  e.  P  A. a  e.  P  A. b  e.  P  E. z  e.  P  ( y  e.  ( x I z )  /\  ( y 
.-  z )  =  ( a  .-  b
) )  ->  A. a  e.  P  A. b  e.  P  E. z  e.  P  ( Y  e.  ( X I z )  /\  ( Y 
.-  z )  =  ( a  .-  b
) ) ) )
3014, 29mpd 15 . 2  |-  ( ph  ->  A. a  e.  P  A. b  e.  P  E. z  e.  P  ( Y  e.  ( X I z )  /\  ( Y  .-  z )  =  ( a  .-  b ) ) )
31 axtgsegcon.3 . . 3  |-  ( ph  ->  A  e.  P )
32 axtgsegcon.4 . . 3  |-  ( ph  ->  B  e.  P )
33 oveq1 6312 . . . . . . 7  |-  ( a  =  A  ->  (
a  .-  b )  =  ( A  .-  b ) )
3433eqeq2d 2443 . . . . . 6  |-  ( a  =  A  ->  (
( Y  .-  z
)  =  ( a 
.-  b )  <->  ( Y  .-  z )  =  ( A  .-  b ) ) )
3534anbi2d 708 . . . . 5  |-  ( a  =  A  ->  (
( Y  e.  ( X I z )  /\  ( Y  .-  z )  =  ( a  .-  b ) )  <->  ( Y  e.  ( X I z )  /\  ( Y 
.-  z )  =  ( A  .-  b
) ) ) )
3635rexbidv 2946 . . . 4  |-  ( a  =  A  ->  ( E. z  e.  P  ( Y  e.  ( X I z )  /\  ( Y  .-  z )  =  ( a  .-  b ) )  <->  E. z  e.  P  ( Y  e.  ( X I z )  /\  ( Y  .-  z )  =  ( A  .-  b ) ) ) )
37 oveq2 6313 . . . . . . 7  |-  ( b  =  B  ->  ( A  .-  b )  =  ( A  .-  B
) )
3837eqeq2d 2443 . . . . . 6  |-  ( b  =  B  ->  (
( Y  .-  z
)  =  ( A 
.-  b )  <->  ( Y  .-  z )  =  ( A  .-  B ) ) )
3938anbi2d 708 . . . . 5  |-  ( b  =  B  ->  (
( Y  e.  ( X I z )  /\  ( Y  .-  z )  =  ( A  .-  b ) )  <->  ( Y  e.  ( X I z )  /\  ( Y 
.-  z )  =  ( A  .-  B
) ) ) )
4039rexbidv 2946 . . . 4  |-  ( b  =  B  ->  ( E. z  e.  P  ( Y  e.  ( X I z )  /\  ( Y  .-  z )  =  ( A  .-  b ) )  <->  E. z  e.  P  ( Y  e.  ( X I z )  /\  ( Y  .-  z )  =  ( A  .-  B ) ) ) )
4136, 40rspc2v 3197 . . 3  |-  ( ( A  e.  P  /\  B  e.  P )  ->  ( A. a  e.  P  A. b  e.  P  E. z  e.  P  ( Y  e.  ( X I z )  /\  ( Y 
.-  z )  =  ( a  .-  b
) )  ->  E. z  e.  P  ( Y  e.  ( X I z )  /\  ( Y 
.-  z )  =  ( A  .-  B
) ) ) )
4231, 32, 41syl2anc 665 . 2  |-  ( ph  ->  ( A. a  e.  P  A. b  e.  P  E. z  e.  P  ( Y  e.  ( X I z )  /\  ( Y 
.-  z )  =  ( a  .-  b
) )  ->  E. z  e.  P  ( Y  e.  ( X I z )  /\  ( Y 
.-  z )  =  ( A  .-  B
) ) ) )
4330, 42mpd 15 1  |-  ( ph  ->  E. z  e.  P  ( Y  e.  ( X I z )  /\  ( Y  .-  z )  =  ( A  .-  B ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    \/ w3o 981    /\ w3a 982    = wceq 1437    e. wcel 1870   {cab 2414    =/= wne 2625   A.wral 2782   E.wrex 2783   {crab 2786   _Vcvv 3087   [.wsbc 3305    \ cdif 3439    i^i cin 3441   {csn 4002   ` cfv 5601  (class class class)co 6305    |-> cmpt2 6307   Basecbs 15084   distcds 15161  TarskiGcstrkg 24341  TarskiGCcstrkgc 24342  TarskiGBcstrkgb 24343  TarskiGCBcstrkgcb 24344  Itvcitv 24347  LineGclng 24348
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-nul 4556
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-sbc 3306  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-iota 5565  df-fv 5609  df-ov 6308  df-trkgcb 24361  df-trkg 24364
This theorem is referenced by:  tgcgrtriv  24391  tgbtwntriv2  24394  tgbtwnouttr2  24402  tgbtwndiff  24413  tgifscgr  24416  tgcgrxfr  24425  lnext  24472  tgbtwnconn1lem3  24479  tgbtwnconn1  24480  legtrid  24496  hlcgrex  24520  mirreu3  24559  miriso  24574  midexlem  24594  footex  24620  opphllem  24634  dfcgra2  24726  f1otrg  24747
  Copyright terms: Public domain W3C validator