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

Theorem axtgpasch 23990
Description: Axiom of (Inner) Pasch, Axiom A7 of [Schwabhauser] p. 12. Given triangle  X Y Z, point  U in segment  X Z, and point  V in segment  Y Z, there exists a point  a on both the segment  U Y and the segment  V X. This axiom is essentially a subset of the general Pasch axiom. The general Pasch axiom asserts that on a plane "a line intersecting a triangle in one of its sides, and not intersecting any of the vertices, must intersect one of the other two sides" (per the discussion about Axiom 7 of [Tarski1999] p. 179). The (general) Pasch axiom was used implicitly by Euclid, but never stated; Moritz Pasch discovered its omission in 1882. As noted in the Metamath book, this means that the omission of Pasch's axiom from Euclid went unnoticed for 2000 years. Only the inner Pasch algorithm is included as an axiom; the "outer" form of the Pasch axiom can be proved using the inner form (see theorem 9.6 of [Schwabhauser] p. 69 and the brief discussion in axiom 7.1 of [Tarski1999] p. 180). (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 )
axtgpasch.1  |-  ( ph  ->  X  e.  P )
axtgpasch.2  |-  ( ph  ->  Y  e.  P )
axtgpasch.3  |-  ( ph  ->  Z  e.  P )
axtgpasch.4  |-  ( ph  ->  U  e.  P )
axtgpasch.5  |-  ( ph  ->  V  e.  P )
axtgpasch.6  |-  ( ph  ->  U  e.  ( X I Z ) )
axtgpasch.7  |-  ( ph  ->  V  e.  ( Y I Z ) )
Assertion
Ref Expression
axtgpasch  |-  ( ph  ->  E. a  e.  P  ( a  e.  ( U I Y )  /\  a  e.  ( V I X ) ) )
Distinct variable groups:    I, a    P, a    U, a    X, a    Y, a    Z, a    V, a    .- , a
Allowed substitution hints:    ph( a)    G( a)

Proof of Theorem axtgpasch
Dummy variables  f 
i  p  x  y  z  b  v  s  t  u are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 axtgpasch.6 . 2  |-  ( ph  ->  U  e.  ( X I Z ) )
2 axtgpasch.7 . 2  |-  ( ph  ->  V  e.  ( Y I Z ) )
3 df-trkg 23976 . . . . . . 7  |- 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 ) ) } ) } ) )
4 inss1 3714 . . . . . . . 8  |-  ( (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 )
5 inss2 3715 . . . . . . . 8  |-  (TarskiGC  i^i TarskiGB )  C_ TarskiGB
64, 5sstri 3508 . . . . . . 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_ TarskiGB
73, 6eqsstri 3529 . . . . . 6  |- TarskiG  C_ TarskiGB
8 axtrkg.g . . . . . 6  |-  ( ph  ->  G  e. TarskiG )
97, 8sseldi 3497 . . . . 5  |-  ( ph  ->  G  e. TarskiGB )
10 axtrkg.p . . . . . . . 8  |-  P  =  ( Base `  G
)
11 axtrkg.d . . . . . . . 8  |-  .-  =  ( dist `  G )
12 axtrkg.i . . . . . . . 8  |-  I  =  (Itv `  G )
1310, 11, 12istrkgb 23978 . . . . . . 7  |-  ( G  e. TarskiGB  <->  ( G  e.  _V  /\  ( A. x  e.  P  A. y  e.  P  ( y  e.  ( x I x )  ->  x  =  y )  /\  A. x  e.  P  A. y  e.  P  A. z  e.  P  A. u  e.  P  A. v  e.  P  ( (
u  e.  ( x I z )  /\  v  e.  ( y
I z ) )  ->  E. a  e.  P  ( a  e.  ( u I y )  /\  a  e.  ( v I x ) ) )  /\  A. s  e.  ~P  P A. t  e.  ~P  P ( E. a  e.  P  A. x  e.  s  A. y  e.  t  x  e.  ( a I y )  ->  E. b  e.  P  A. x  e.  s  A. y  e.  t  b  e.  ( x I y ) ) ) ) )
1413simprbi 464 . . . . . 6  |-  ( G  e. TarskiGB 
->  ( A. x  e.  P  A. y  e.  P  ( y  e.  ( x I x )  ->  x  =  y )  /\  A. x  e.  P  A. y  e.  P  A. z  e.  P  A. u  e.  P  A. v  e.  P  (
( u  e.  ( x I z )  /\  v  e.  ( y I z ) )  ->  E. a  e.  P  ( a  e.  ( u I y )  /\  a  e.  ( v I x ) ) )  /\  A. s  e.  ~P  P A. t  e.  ~P  P ( E. a  e.  P  A. x  e.  s  A. y  e.  t  x  e.  ( a I y )  ->  E. b  e.  P  A. x  e.  s  A. y  e.  t  b  e.  ( x I y ) ) ) )
1514simp2d 1009 . . . . 5  |-  ( G  e. TarskiGB 
->  A. x  e.  P  A. y  e.  P  A. z  e.  P  A. u  e.  P  A. v  e.  P  ( ( u  e.  ( x I z )  /\  v  e.  ( y I z ) )  ->  E. a  e.  P  ( a  e.  ( u I y )  /\  a  e.  ( v I x ) ) ) )
169, 15syl 16 . . . 4  |-  ( ph  ->  A. x  e.  P  A. y  e.  P  A. z  e.  P  A. u  e.  P  A. v  e.  P  ( ( u  e.  ( x I z )  /\  v  e.  ( y I z ) )  ->  E. a  e.  P  ( a  e.  ( u I y )  /\  a  e.  ( v I x ) ) ) )
17 axtgpasch.1 . . . . 5  |-  ( ph  ->  X  e.  P )
18 axtgpasch.2 . . . . 5  |-  ( ph  ->  Y  e.  P )
19 axtgpasch.3 . . . . 5  |-  ( ph  ->  Z  e.  P )
20 oveq1 6303 . . . . . . . . . 10  |-  ( x  =  X  ->  (
x I z )  =  ( X I z ) )
2120eleq2d 2527 . . . . . . . . 9  |-  ( x  =  X  ->  (
u  e.  ( x I z )  <->  u  e.  ( X I z ) ) )
2221anbi1d 704 . . . . . . . 8  |-  ( x  =  X  ->  (
( u  e.  ( x I z )  /\  v  e.  ( y I z ) )  <->  ( u  e.  ( X I z )  /\  v  e.  ( y I z ) ) ) )
23 oveq2 6304 . . . . . . . . . . 11  |-  ( x  =  X  ->  (
v I x )  =  ( v I X ) )
2423eleq2d 2527 . . . . . . . . . 10  |-  ( x  =  X  ->  (
a  e.  ( v I x )  <->  a  e.  ( v I X ) ) )
2524anbi2d 703 . . . . . . . . 9  |-  ( x  =  X  ->  (
( a  e.  ( u I y )  /\  a  e.  ( v I x ) )  <->  ( a  e.  ( u I y )  /\  a  e.  ( v I X ) ) ) )
2625rexbidv 2968 . . . . . . . 8  |-  ( x  =  X  ->  ( E. a  e.  P  ( a  e.  ( u I y )  /\  a  e.  ( v I x ) )  <->  E. a  e.  P  ( a  e.  ( u I y )  /\  a  e.  ( v I X ) ) ) )
2722, 26imbi12d 320 . . . . . . 7  |-  ( x  =  X  ->  (
( ( u  e.  ( x I z )  /\  v  e.  ( y I z ) )  ->  E. a  e.  P  ( a  e.  ( u I y )  /\  a  e.  ( v I x ) ) )  <->  ( (
u  e.  ( X I z )  /\  v  e.  ( y
I z ) )  ->  E. a  e.  P  ( a  e.  ( u I y )  /\  a  e.  ( v I X ) ) ) ) )
28272ralbidv 2901 . . . . . 6  |-  ( x  =  X  ->  ( A. u  e.  P  A. v  e.  P  ( ( u  e.  ( x I z )  /\  v  e.  ( y I z ) )  ->  E. a  e.  P  ( a  e.  ( u I y )  /\  a  e.  ( v I x ) ) )  <->  A. u  e.  P  A. v  e.  P  ( (
u  e.  ( X I z )  /\  v  e.  ( y
I z ) )  ->  E. a  e.  P  ( a  e.  ( u I y )  /\  a  e.  ( v I X ) ) ) ) )
29 oveq1 6303 . . . . . . . . . 10  |-  ( y  =  Y  ->  (
y I z )  =  ( Y I z ) )
3029eleq2d 2527 . . . . . . . . 9  |-  ( y  =  Y  ->  (
v  e.  ( y I z )  <->  v  e.  ( Y I z ) ) )
3130anbi2d 703 . . . . . . . 8  |-  ( y  =  Y  ->  (
( u  e.  ( X I z )  /\  v  e.  ( y I z ) )  <->  ( u  e.  ( X I z )  /\  v  e.  ( Y I z ) ) ) )
32 oveq2 6304 . . . . . . . . . . 11  |-  ( y  =  Y  ->  (
u I y )  =  ( u I Y ) )
3332eleq2d 2527 . . . . . . . . . 10  |-  ( y  =  Y  ->  (
a  e.  ( u I y )  <->  a  e.  ( u I Y ) ) )
3433anbi1d 704 . . . . . . . . 9  |-  ( y  =  Y  ->  (
( a  e.  ( u I y )  /\  a  e.  ( v I X ) )  <->  ( a  e.  ( u I Y )  /\  a  e.  ( v I X ) ) ) )
3534rexbidv 2968 . . . . . . . 8  |-  ( y  =  Y  ->  ( E. a  e.  P  ( a  e.  ( u I y )  /\  a  e.  ( v I X ) )  <->  E. a  e.  P  ( a  e.  ( u I Y )  /\  a  e.  ( v I X ) ) ) )
3631, 35imbi12d 320 . . . . . . 7  |-  ( y  =  Y  ->  (
( ( u  e.  ( X I z )  /\  v  e.  ( y I z ) )  ->  E. a  e.  P  ( a  e.  ( u I y )  /\  a  e.  ( v I X ) ) )  <->  ( (
u  e.  ( X I z )  /\  v  e.  ( Y I z ) )  ->  E. a  e.  P  ( a  e.  ( u I Y )  /\  a  e.  ( v I X ) ) ) ) )
37362ralbidv 2901 . . . . . 6  |-  ( y  =  Y  ->  ( A. u  e.  P  A. v  e.  P  ( ( u  e.  ( X I z )  /\  v  e.  ( y I z ) )  ->  E. a  e.  P  ( a  e.  ( u I y )  /\  a  e.  ( v I X ) ) )  <->  A. u  e.  P  A. v  e.  P  ( (
u  e.  ( X I z )  /\  v  e.  ( Y I z ) )  ->  E. a  e.  P  ( a  e.  ( u I Y )  /\  a  e.  ( v I X ) ) ) ) )
38 oveq2 6304 . . . . . . . . . 10  |-  ( z  =  Z  ->  ( X I z )  =  ( X I Z ) )
3938eleq2d 2527 . . . . . . . . 9  |-  ( z  =  Z  ->  (
u  e.  ( X I z )  <->  u  e.  ( X I Z ) ) )
40 oveq2 6304 . . . . . . . . . 10  |-  ( z  =  Z  ->  ( Y I z )  =  ( Y I Z ) )
4140eleq2d 2527 . . . . . . . . 9  |-  ( z  =  Z  ->  (
v  e.  ( Y I z )  <->  v  e.  ( Y I Z ) ) )
4239, 41anbi12d 710 . . . . . . . 8  |-  ( z  =  Z  ->  (
( u  e.  ( X I z )  /\  v  e.  ( Y I z ) )  <->  ( u  e.  ( X I Z )  /\  v  e.  ( Y I Z ) ) ) )
4342imbi1d 317 . . . . . . 7  |-  ( z  =  Z  ->  (
( ( u  e.  ( X I z )  /\  v  e.  ( Y I z ) )  ->  E. a  e.  P  ( a  e.  ( u I Y )  /\  a  e.  ( v I X ) ) )  <->  ( (
u  e.  ( X I Z )  /\  v  e.  ( Y I Z ) )  ->  E. a  e.  P  ( a  e.  ( u I Y )  /\  a  e.  ( v I X ) ) ) ) )
44432ralbidv 2901 . . . . . 6  |-  ( z  =  Z  ->  ( A. u  e.  P  A. v  e.  P  ( ( u  e.  ( X I z )  /\  v  e.  ( Y I z ) )  ->  E. a  e.  P  ( a  e.  ( u I Y )  /\  a  e.  ( v I X ) ) )  <->  A. u  e.  P  A. v  e.  P  ( (
u  e.  ( X I Z )  /\  v  e.  ( Y I Z ) )  ->  E. a  e.  P  ( a  e.  ( u I Y )  /\  a  e.  ( v I X ) ) ) ) )
4528, 37, 44rspc3v 3222 . . . . 5  |-  ( ( X  e.  P  /\  Y  e.  P  /\  Z  e.  P )  ->  ( A. x  e.  P  A. y  e.  P  A. z  e.  P  A. u  e.  P  A. v  e.  P  ( ( u  e.  ( x I z )  /\  v  e.  ( y I z ) )  ->  E. a  e.  P  ( a  e.  ( u I y )  /\  a  e.  ( v I x ) ) )  ->  A. u  e.  P  A. v  e.  P  ( ( u  e.  ( X I Z )  /\  v  e.  ( Y I Z ) )  ->  E. a  e.  P  ( a  e.  ( u I Y )  /\  a  e.  ( v I X ) ) ) ) )
4617, 18, 19, 45syl3anc 1228 . . . 4  |-  ( ph  ->  ( A. x  e.  P  A. y  e.  P  A. z  e.  P  A. u  e.  P  A. v  e.  P  ( ( u  e.  ( x I z )  /\  v  e.  ( y I z ) )  ->  E. a  e.  P  ( a  e.  ( u I y )  /\  a  e.  ( v I x ) ) )  ->  A. u  e.  P  A. v  e.  P  ( ( u  e.  ( X I Z )  /\  v  e.  ( Y I Z ) )  ->  E. a  e.  P  ( a  e.  ( u I Y )  /\  a  e.  ( v I X ) ) ) ) )
4716, 46mpd 15 . . 3  |-  ( ph  ->  A. u  e.  P  A. v  e.  P  ( ( u  e.  ( X I Z )  /\  v  e.  ( Y I Z ) )  ->  E. a  e.  P  ( a  e.  ( u I Y )  /\  a  e.  ( v I X ) ) ) )
48 axtgpasch.4 . . . 4  |-  ( ph  ->  U  e.  P )
49 axtgpasch.5 . . . 4  |-  ( ph  ->  V  e.  P )
50 eleq1 2529 . . . . . . 7  |-  ( u  =  U  ->  (
u  e.  ( X I Z )  <->  U  e.  ( X I Z ) ) )
5150anbi1d 704 . . . . . 6  |-  ( u  =  U  ->  (
( u  e.  ( X I Z )  /\  v  e.  ( Y I Z ) )  <->  ( U  e.  ( X I Z )  /\  v  e.  ( Y I Z ) ) ) )
52 oveq1 6303 . . . . . . . . 9  |-  ( u  =  U  ->  (
u I Y )  =  ( U I Y ) )
5352eleq2d 2527 . . . . . . . 8  |-  ( u  =  U  ->  (
a  e.  ( u I Y )  <->  a  e.  ( U I Y ) ) )
5453anbi1d 704 . . . . . . 7  |-  ( u  =  U  ->  (
( a  e.  ( u I Y )  /\  a  e.  ( v I X ) )  <->  ( a  e.  ( U I Y )  /\  a  e.  ( v I X ) ) ) )
5554rexbidv 2968 . . . . . 6  |-  ( u  =  U  ->  ( E. a  e.  P  ( a  e.  ( u I Y )  /\  a  e.  ( v I X ) )  <->  E. a  e.  P  ( a  e.  ( U I Y )  /\  a  e.  ( v I X ) ) ) )
5651, 55imbi12d 320 . . . . 5  |-  ( u  =  U  ->  (
( ( u  e.  ( X I Z )  /\  v  e.  ( Y I Z ) )  ->  E. a  e.  P  ( a  e.  ( u I Y )  /\  a  e.  ( v I X ) ) )  <->  ( ( U  e.  ( X I Z )  /\  v  e.  ( Y I Z ) )  ->  E. a  e.  P  ( a  e.  ( U I Y )  /\  a  e.  ( v I X ) ) ) ) )
57 eleq1 2529 . . . . . . 7  |-  ( v  =  V  ->  (
v  e.  ( Y I Z )  <->  V  e.  ( Y I Z ) ) )
5857anbi2d 703 . . . . . 6  |-  ( v  =  V  ->  (
( U  e.  ( X I Z )  /\  v  e.  ( Y I Z ) )  <->  ( U  e.  ( X I Z )  /\  V  e.  ( Y I Z ) ) ) )
59 oveq1 6303 . . . . . . . . 9  |-  ( v  =  V  ->  (
v I X )  =  ( V I X ) )
6059eleq2d 2527 . . . . . . . 8  |-  ( v  =  V  ->  (
a  e.  ( v I X )  <->  a  e.  ( V I X ) ) )
6160anbi2d 703 . . . . . . 7  |-  ( v  =  V  ->  (
( a  e.  ( U I Y )  /\  a  e.  ( v I X ) )  <->  ( a  e.  ( U I Y )  /\  a  e.  ( V I X ) ) ) )
6261rexbidv 2968 . . . . . 6  |-  ( v  =  V  ->  ( E. a  e.  P  ( a  e.  ( U I Y )  /\  a  e.  ( v I X ) )  <->  E. a  e.  P  ( a  e.  ( U I Y )  /\  a  e.  ( V I X ) ) ) )
6358, 62imbi12d 320 . . . . 5  |-  ( v  =  V  ->  (
( ( U  e.  ( X I Z )  /\  v  e.  ( Y I Z ) )  ->  E. a  e.  P  ( a  e.  ( U I Y )  /\  a  e.  ( v I X ) ) )  <->  ( ( U  e.  ( X I Z )  /\  V  e.  ( Y I Z ) )  ->  E. a  e.  P  ( a  e.  ( U I Y )  /\  a  e.  ( V I X ) ) ) ) )
6456, 63rspc2v 3219 . . . 4  |-  ( ( U  e.  P  /\  V  e.  P )  ->  ( A. u  e.  P  A. v  e.  P  ( ( u  e.  ( X I Z )  /\  v  e.  ( Y I Z ) )  ->  E. a  e.  P  ( a  e.  ( u I Y )  /\  a  e.  ( v I X ) ) )  -> 
( ( U  e.  ( X I Z )  /\  V  e.  ( Y I Z ) )  ->  E. a  e.  P  ( a  e.  ( U I Y )  /\  a  e.  ( V I X ) ) ) ) )
6548, 49, 64syl2anc 661 . . 3  |-  ( ph  ->  ( A. u  e.  P  A. v  e.  P  ( ( u  e.  ( X I Z )  /\  v  e.  ( Y I Z ) )  ->  E. a  e.  P  ( a  e.  ( u I Y )  /\  a  e.  ( v I X ) ) )  -> 
( ( U  e.  ( X I Z )  /\  V  e.  ( Y I Z ) )  ->  E. a  e.  P  ( a  e.  ( U I Y )  /\  a  e.  ( V I X ) ) ) ) )
6647, 65mpd 15 . 2  |-  ( ph  ->  ( ( U  e.  ( X I Z )  /\  V  e.  ( Y I Z ) )  ->  E. a  e.  P  ( a  e.  ( U I Y )  /\  a  e.  ( V I X ) ) ) )
671, 2, 66mp2and 679 1  |-  ( ph  ->  E. a  e.  P  ( a  e.  ( U I Y )  /\  a  e.  ( V I X ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    \/ w3o 972    /\ w3a 973    = wceq 1395    e. wcel 1819   {cab 2442   A.wral 2807   E.wrex 2808   {crab 2811   _Vcvv 3109   [.wsbc 3327    \ cdif 3468    i^i cin 3470   ~Pcpw 4015   {csn 4032   ` cfv 5594  (class class class)co 6296    |-> cmpt2 6298   Basecbs 14644   distcds 14721  TarskiGcstrkg 23951  TarskiGCcstrkgc 23952  TarskiGBcstrkgb 23953  TarskiGCBcstrkgcb 23954  Itvcitv 23958  LineGclng 23959
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-nul 4586
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4252  df-br 4457  df-iota 5557  df-fv 5602  df-ov 6299  df-trkgb 23971  df-trkg 23976
This theorem is referenced by:  tgbtwncom  24005  tgbtwnswapid  24009  tgbtwnintr  24010  tgtrisegint  24016  tgbtwnconn1  24088  midexlem  24195  opphllem  24235  opphllem1  24245  lnopp2hpgb  24258  f1otrg  24301
  Copyright terms: Public domain W3C validator