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

Theorem axtgsegcon 22925
Description: Axiom of segment construction, Axiom A4 of [Schwabhauser] p. 11. (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 22916 . . . . . 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 3571 . . . . . . 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 3570 . . . . . . 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 3365 . . . . . 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 3386 . . . . 5  |- TarskiG  C_ TarskiGCB
6 axtrkg.g . . . . 5  |-  ( ph  ->  G  e. TarskiG )
75, 6sseldi 3354 . . . 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 22919 . . . . . 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 464 . . . . 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 463 . . . 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 16 . . 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 6098 . . . . . . . . 9  |-  ( x  =  X  ->  (
x I z )  =  ( X I z ) )
1817eleq2d 2510 . . . . . . . 8  |-  ( x  =  X  ->  (
y  e.  ( x I z )  <->  y  e.  ( X I z ) ) )
1918anbi1d 704 . . . . . . 7  |-  ( x  =  X  ->  (
( y  e.  ( x I z )  /\  ( y  .-  z )  =  ( a  .-  b ) )  <->  ( y  e.  ( X I z )  /\  ( y 
.-  z )  =  ( a  .-  b
) ) ) )
2019rexbidv 2736 . . . . . 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 2757 . . . . 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 2503 . . . . . . . 8  |-  ( y  =  Y  ->  (
y  e.  ( X I z )  <->  Y  e.  ( X I z ) ) )
23 oveq1 6098 . . . . . . . . 9  |-  ( y  =  Y  ->  (
y  .-  z )  =  ( Y  .-  z ) )
2423eqeq1d 2451 . . . . . . . 8  |-  ( y  =  Y  ->  (
( y  .-  z
)  =  ( a 
.-  b )  <->  ( Y  .-  z )  =  ( a  .-  b ) ) )
2522, 24anbi12d 710 . . . . . . 7  |-  ( y  =  Y  ->  (
( y  e.  ( X I z )  /\  ( y  .-  z )  =  ( a  .-  b ) )  <->  ( Y  e.  ( X I z )  /\  ( Y 
.-  z )  =  ( a  .-  b
) ) ) )
2625rexbidv 2736 . . . . . 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 2757 . . . . 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 3079 . . . 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 661 . . 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 6098 . . . . . . 7  |-  ( a  =  A  ->  (
a  .-  b )  =  ( A  .-  b ) )
3433eqeq2d 2454 . . . . . 6  |-  ( a  =  A  ->  (
( Y  .-  z
)  =  ( a 
.-  b )  <->  ( Y  .-  z )  =  ( A  .-  b ) ) )
3534anbi2d 703 . . . . 5  |-  ( a  =  A  ->  (
( Y  e.  ( X I z )  /\  ( Y  .-  z )  =  ( a  .-  b ) )  <->  ( Y  e.  ( X I z )  /\  ( Y 
.-  z )  =  ( A  .-  b
) ) ) )
3635rexbidv 2736 . . . 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 6099 . . . . . . 7  |-  ( b  =  B  ->  ( A  .-  b )  =  ( A  .-  B
) )
3837eqeq2d 2454 . . . . . 6  |-  ( b  =  B  ->  (
( Y  .-  z
)  =  ( A 
.-  b )  <->  ( Y  .-  z )  =  ( A  .-  B ) ) )
3938anbi2d 703 . . . . 5  |-  ( b  =  B  ->  (
( Y  e.  ( X I z )  /\  ( Y  .-  z )  =  ( A  .-  b ) )  <->  ( Y  e.  ( X I z )  /\  ( Y 
.-  z )  =  ( A  .-  B
) ) ) )
4039rexbidv 2736 . . . 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 3079 . . 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 661 . 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 369    \/ w3o 964    /\ w3a 965    = wceq 1369    e. wcel 1756   {cab 2429    =/= wne 2606   A.wral 2715   E.wrex 2716   {crab 2719   _Vcvv 2972   [.wsbc 3186    \ cdif 3325    i^i cin 3327   {csn 3877   ` cfv 5418  (class class class)co 6091    e. cmpt2 6093   Basecbs 14174   distcds 14247  TarskiGcstrkg 22889  TarskiGCcstrkgc 22890  TarskiGBcstrkgb 22891  TarskiGCBcstrkgcb 22892  Itvcitv 22897  LineGclng 22898
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-trkgcb 22911  df-trkg 22916
This theorem is referenced by:  tgcgrtriv  22938  tgbtwntriv2  22941  tgbtwnouttr2  22948  tgbtwndiff  22959  tgifscgr  22961  tgcgrxfr  22970  lnext  22999  tgbtwnconn1lem3  23006  tgbtwnconn1  23007  legtrid  23022  mirreu3  23058  miriso  23073  midexlem  23086  footex  23109  f1otrg  23117
  Copyright terms: Public domain W3C validator