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

Theorem axtgeucl 24383
Description: Euclid's Axiom. Axiom A10 of [Schwabhauser] p. 13. This is equivalent to Euclid's parallel postulate when combined with other axioms. (Contributed by Thierry Arnoux, 16-Mar-2019.)
Hypotheses
Ref Expression
axtrkge.p  |-  P  =  ( Base `  G
)
axtrkge.d  |-  .-  =  ( dist `  G )
axtrkge.i  |-  I  =  (Itv `  G )
axtgeucl.g  |-  ( ph  ->  G  e. TarskiGE )
axtgeucl.1  |-  ( ph  ->  X  e.  P )
axtgeucl.2  |-  ( ph  ->  Y  e.  P )
axtgeucl.3  |-  ( ph  ->  Z  e.  P )
axtgeucl.4  |-  ( ph  ->  U  e.  P )
axtgeucl.5  |-  ( ph  ->  V  e.  P )
axtgeucl.6  |-  ( ph  ->  U  e.  ( X I V ) )
axtgeucl.7  |-  ( ph  ->  U  e.  ( Y I Z ) )
axtgeucl.8  |-  ( ph  ->  X  =/=  U )
Assertion
Ref Expression
axtgeucl  |-  ( ph  ->  E. a  e.  P  E. b  e.  P  ( Y  e.  ( X I a )  /\  Z  e.  ( X I b )  /\  V  e.  ( a I b ) ) )
Distinct variable groups:    a, b, I    P, a, b    V, a, b    U, a, b    X, a, b    Y, a, b    Z, a, b    .- , a,
b
Allowed substitution hints:    ph( a, b)    G( a, b)

Proof of Theorem axtgeucl
Dummy variables  v  u  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 axtgeucl.6 . 2  |-  ( ph  ->  U  e.  ( X I V ) )
2 axtgeucl.7 . 2  |-  ( ph  ->  U  e.  ( Y I Z ) )
3 axtgeucl.8 . 2  |-  ( ph  ->  X  =/=  U )
4 axtgeucl.g . . . . . 6  |-  ( ph  ->  G  e. TarskiGE )
5 axtrkge.p . . . . . . 7  |-  P  =  ( Base `  G
)
6 axtrkge.d . . . . . . 7  |-  .-  =  ( dist `  G )
7 axtrkge.i . . . . . . 7  |-  I  =  (Itv `  G )
85, 6, 7istrkge 24368 . . . . . 6  |-  ( G  e. TarskiGE  <->  ( G  e.  _V  /\  A. x  e.  P  A. y  e.  P  A. z  e.  P  A. u  e.  P  A. v  e.  P  (
( u  e.  ( x I v )  /\  u  e.  ( y I z )  /\  x  =/=  u
)  ->  E. a  e.  P  E. b  e.  P  ( y  e.  ( x I a )  /\  z  e.  ( x I b )  /\  v  e.  ( a I b ) ) ) ) )
94, 8sylib 199 . . . . 5  |-  ( ph  ->  ( G  e.  _V  /\ 
A. x  e.  P  A. y  e.  P  A. z  e.  P  A. u  e.  P  A. v  e.  P  ( ( u  e.  ( x I v )  /\  u  e.  ( y I z )  /\  x  =/=  u )  ->  E. a  e.  P  E. b  e.  P  ( y  e.  ( x I a )  /\  z  e.  ( x I b )  /\  v  e.  ( a I b ) ) ) ) )
109simprd 464 . . . 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 v )  /\  u  e.  ( y I z )  /\  x  =/=  u )  ->  E. a  e.  P  E. b  e.  P  ( y  e.  ( x I a )  /\  z  e.  ( x I b )  /\  v  e.  ( a I b ) ) ) )
11 axtgeucl.1 . . . . 5  |-  ( ph  ->  X  e.  P )
12 axtgeucl.2 . . . . 5  |-  ( ph  ->  Y  e.  P )
13 axtgeucl.3 . . . . 5  |-  ( ph  ->  Z  e.  P )
14 oveq1 6312 . . . . . . . . . 10  |-  ( x  =  X  ->  (
x I v )  =  ( X I v ) )
1514eleq2d 2499 . . . . . . . . 9  |-  ( x  =  X  ->  (
u  e.  ( x I v )  <->  u  e.  ( X I v ) ) )
16 neeq1 2712 . . . . . . . . 9  |-  ( x  =  X  ->  (
x  =/=  u  <->  X  =/=  u ) )
1715, 163anbi13d 1337 . . . . . . . 8  |-  ( x  =  X  ->  (
( u  e.  ( x I v )  /\  u  e.  ( y I z )  /\  x  =/=  u
)  <->  ( u  e.  ( X I v )  /\  u  e.  ( y I z )  /\  X  =/=  u ) ) )
18 oveq1 6312 . . . . . . . . . . 11  |-  ( x  =  X  ->  (
x I a )  =  ( X I a ) )
1918eleq2d 2499 . . . . . . . . . 10  |-  ( x  =  X  ->  (
y  e.  ( x I a )  <->  y  e.  ( X I a ) ) )
20 oveq1 6312 . . . . . . . . . . 11  |-  ( x  =  X  ->  (
x I b )  =  ( X I b ) )
2120eleq2d 2499 . . . . . . . . . 10  |-  ( x  =  X  ->  (
z  e.  ( x I b )  <->  z  e.  ( X I b ) ) )
2219, 213anbi12d 1336 . . . . . . . . 9  |-  ( x  =  X  ->  (
( y  e.  ( x I a )  /\  z  e.  ( x I b )  /\  v  e.  ( a I b ) )  <->  ( y  e.  ( X I a )  /\  z  e.  ( X I b )  /\  v  e.  ( a I b ) ) ) )
23222rexbidv 2953 . . . . . . . 8  |-  ( x  =  X  ->  ( E. a  e.  P  E. b  e.  P  ( y  e.  ( x I a )  /\  z  e.  ( x I b )  /\  v  e.  ( a I b ) )  <->  E. a  e.  P  E. b  e.  P  ( y  e.  ( X I a )  /\  z  e.  ( X I b )  /\  v  e.  ( a I b ) ) ) )
2417, 23imbi12d 321 . . . . . . 7  |-  ( x  =  X  ->  (
( ( u  e.  ( x I v )  /\  u  e.  ( y I z )  /\  x  =/=  u )  ->  E. a  e.  P  E. b  e.  P  ( y  e.  ( x I a )  /\  z  e.  ( x I b )  /\  v  e.  ( a I b ) ) )  <->  ( (
u  e.  ( X I v )  /\  u  e.  ( y
I z )  /\  X  =/=  u )  ->  E. a  e.  P  E. b  e.  P  ( y  e.  ( X I a )  /\  z  e.  ( X I b )  /\  v  e.  ( a I b ) ) ) ) )
25242ralbidv 2876 . . . . . 6  |-  ( x  =  X  ->  ( A. u  e.  P  A. v  e.  P  ( ( u  e.  ( x I v )  /\  u  e.  ( y I z )  /\  x  =/=  u )  ->  E. a  e.  P  E. b  e.  P  ( y  e.  ( x I a )  /\  z  e.  ( x I b )  /\  v  e.  ( a I b ) ) )  <->  A. u  e.  P  A. v  e.  P  ( (
u  e.  ( X I v )  /\  u  e.  ( y
I z )  /\  X  =/=  u )  ->  E. a  e.  P  E. b  e.  P  ( y  e.  ( X I a )  /\  z  e.  ( X I b )  /\  v  e.  ( a I b ) ) ) ) )
26 oveq1 6312 . . . . . . . . . 10  |-  ( y  =  Y  ->  (
y I z )  =  ( Y I z ) )
2726eleq2d 2499 . . . . . . . . 9  |-  ( y  =  Y  ->  (
u  e.  ( y I z )  <->  u  e.  ( Y I z ) ) )
28273anbi2d 1340 . . . . . . . 8  |-  ( y  =  Y  ->  (
( u  e.  ( X I v )  /\  u  e.  ( y I z )  /\  X  =/=  u
)  <->  ( u  e.  ( X I v )  /\  u  e.  ( Y I z )  /\  X  =/=  u ) ) )
29 eleq1 2501 . . . . . . . . . 10  |-  ( y  =  Y  ->  (
y  e.  ( X I a )  <->  Y  e.  ( X I a ) ) )
30293anbi1d 1339 . . . . . . . . 9  |-  ( y  =  Y  ->  (
( y  e.  ( X I a )  /\  z  e.  ( X I b )  /\  v  e.  ( a I b ) )  <->  ( Y  e.  ( X I a )  /\  z  e.  ( X I b )  /\  v  e.  ( a I b ) ) ) )
31302rexbidv 2953 . . . . . . . 8  |-  ( y  =  Y  ->  ( E. a  e.  P  E. b  e.  P  ( y  e.  ( X I a )  /\  z  e.  ( X I b )  /\  v  e.  ( a I b ) )  <->  E. a  e.  P  E. b  e.  P  ( Y  e.  ( X I a )  /\  z  e.  ( X I b )  /\  v  e.  ( a I b ) ) ) )
3228, 31imbi12d 321 . . . . . . 7  |-  ( y  =  Y  ->  (
( ( u  e.  ( X I v )  /\  u  e.  ( y I z )  /\  X  =/=  u )  ->  E. a  e.  P  E. b  e.  P  ( y  e.  ( X I a )  /\  z  e.  ( X I b )  /\  v  e.  ( a I b ) ) )  <->  ( (
u  e.  ( X I v )  /\  u  e.  ( Y I z )  /\  X  =/=  u )  ->  E. a  e.  P  E. b  e.  P  ( Y  e.  ( X I a )  /\  z  e.  ( X I b )  /\  v  e.  ( a I b ) ) ) ) )
33322ralbidv 2876 . . . . . 6  |-  ( y  =  Y  ->  ( A. u  e.  P  A. v  e.  P  ( ( u  e.  ( X I v )  /\  u  e.  ( y I z )  /\  X  =/=  u )  ->  E. a  e.  P  E. b  e.  P  ( y  e.  ( X I a )  /\  z  e.  ( X I b )  /\  v  e.  ( a I b ) ) )  <->  A. u  e.  P  A. v  e.  P  ( (
u  e.  ( X I v )  /\  u  e.  ( Y I z )  /\  X  =/=  u )  ->  E. a  e.  P  E. b  e.  P  ( Y  e.  ( X I a )  /\  z  e.  ( X I b )  /\  v  e.  ( a I b ) ) ) ) )
34 oveq2 6313 . . . . . . . . . 10  |-  ( z  =  Z  ->  ( Y I z )  =  ( Y I Z ) )
3534eleq2d 2499 . . . . . . . . 9  |-  ( z  =  Z  ->  (
u  e.  ( Y I z )  <->  u  e.  ( Y I Z ) ) )
36353anbi2d 1340 . . . . . . . 8  |-  ( z  =  Z  ->  (
( u  e.  ( X I v )  /\  u  e.  ( Y I z )  /\  X  =/=  u
)  <->  ( u  e.  ( X I v )  /\  u  e.  ( Y I Z )  /\  X  =/=  u ) ) )
37 eleq1 2501 . . . . . . . . . 10  |-  ( z  =  Z  ->  (
z  e.  ( X I b )  <->  Z  e.  ( X I b ) ) )
38373anbi2d 1340 . . . . . . . . 9  |-  ( z  =  Z  ->  (
( Y  e.  ( X I a )  /\  z  e.  ( X I b )  /\  v  e.  ( a I b ) )  <->  ( Y  e.  ( X I a )  /\  Z  e.  ( X I b )  /\  v  e.  ( a I b ) ) ) )
39382rexbidv 2953 . . . . . . . 8  |-  ( z  =  Z  ->  ( E. a  e.  P  E. b  e.  P  ( Y  e.  ( X I a )  /\  z  e.  ( X I b )  /\  v  e.  ( a I b ) )  <->  E. a  e.  P  E. b  e.  P  ( Y  e.  ( X I a )  /\  Z  e.  ( X I b )  /\  v  e.  ( a I b ) ) ) )
4036, 39imbi12d 321 . . . . . . 7  |-  ( z  =  Z  ->  (
( ( u  e.  ( X I v )  /\  u  e.  ( Y I z )  /\  X  =/=  u )  ->  E. a  e.  P  E. b  e.  P  ( Y  e.  ( X I a )  /\  z  e.  ( X I b )  /\  v  e.  ( a I b ) ) )  <->  ( (
u  e.  ( X I v )  /\  u  e.  ( Y I Z )  /\  X  =/=  u )  ->  E. a  e.  P  E. b  e.  P  ( Y  e.  ( X I a )  /\  Z  e.  ( X I b )  /\  v  e.  ( a I b ) ) ) ) )
41402ralbidv 2876 . . . . . 6  |-  ( z  =  Z  ->  ( A. u  e.  P  A. v  e.  P  ( ( u  e.  ( X I v )  /\  u  e.  ( Y I z )  /\  X  =/=  u )  ->  E. a  e.  P  E. b  e.  P  ( Y  e.  ( X I a )  /\  z  e.  ( X I b )  /\  v  e.  ( a I b ) ) )  <->  A. u  e.  P  A. v  e.  P  ( (
u  e.  ( X I v )  /\  u  e.  ( Y I Z )  /\  X  =/=  u )  ->  E. a  e.  P  E. b  e.  P  ( Y  e.  ( X I a )  /\  Z  e.  ( X I b )  /\  v  e.  ( a I b ) ) ) ) )
4225, 33, 41rspc3v 3200 . . . . 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 v )  /\  u  e.  ( y I z )  /\  x  =/=  u )  ->  E. a  e.  P  E. b  e.  P  ( y  e.  ( x I a )  /\  z  e.  ( x I b )  /\  v  e.  ( a I b ) ) )  ->  A. u  e.  P  A. v  e.  P  ( ( u  e.  ( X I v )  /\  u  e.  ( Y I Z )  /\  X  =/=  u )  ->  E. a  e.  P  E. b  e.  P  ( Y  e.  ( X I a )  /\  Z  e.  ( X I b )  /\  v  e.  ( a I b ) ) ) ) )
4311, 12, 13, 42syl3anc 1264 . . . 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 v )  /\  u  e.  ( y I z )  /\  x  =/=  u )  ->  E. a  e.  P  E. b  e.  P  ( y  e.  ( x I a )  /\  z  e.  ( x I b )  /\  v  e.  ( a I b ) ) )  ->  A. u  e.  P  A. v  e.  P  ( ( u  e.  ( X I v )  /\  u  e.  ( Y I Z )  /\  X  =/=  u )  ->  E. a  e.  P  E. b  e.  P  ( Y  e.  ( X I a )  /\  Z  e.  ( X I b )  /\  v  e.  ( a I b ) ) ) ) )
4410, 43mpd 15 . . 3  |-  ( ph  ->  A. u  e.  P  A. v  e.  P  ( ( u  e.  ( X I v )  /\  u  e.  ( Y I Z )  /\  X  =/=  u )  ->  E. a  e.  P  E. b  e.  P  ( Y  e.  ( X I a )  /\  Z  e.  ( X I b )  /\  v  e.  ( a I b ) ) ) )
45 axtgeucl.4 . . . 4  |-  ( ph  ->  U  e.  P )
46 axtgeucl.5 . . . 4  |-  ( ph  ->  V  e.  P )
47 eleq1 2501 . . . . . . 7  |-  ( u  =  U  ->  (
u  e.  ( X I v )  <->  U  e.  ( X I v ) ) )
48 eleq1 2501 . . . . . . 7  |-  ( u  =  U  ->  (
u  e.  ( Y I Z )  <->  U  e.  ( Y I Z ) ) )
49 neeq2 2714 . . . . . . 7  |-  ( u  =  U  ->  ( X  =/=  u  <->  X  =/=  U ) )
5047, 48, 493anbi123d 1335 . . . . . 6  |-  ( u  =  U  ->  (
( u  e.  ( X I v )  /\  u  e.  ( Y I Z )  /\  X  =/=  u
)  <->  ( U  e.  ( X I v )  /\  U  e.  ( Y I Z )  /\  X  =/= 
U ) ) )
5150imbi1d 318 . . . . 5  |-  ( u  =  U  ->  (
( ( u  e.  ( X I v )  /\  u  e.  ( Y I Z )  /\  X  =/=  u )  ->  E. a  e.  P  E. b  e.  P  ( Y  e.  ( X I a )  /\  Z  e.  ( X I b )  /\  v  e.  ( a I b ) ) )  <->  ( ( U  e.  ( X I v )  /\  U  e.  ( Y I Z )  /\  X  =/=  U )  ->  E. a  e.  P  E. b  e.  P  ( Y  e.  ( X I a )  /\  Z  e.  ( X I b )  /\  v  e.  ( a I b ) ) ) ) )
52 oveq2 6313 . . . . . . . 8  |-  ( v  =  V  ->  ( X I v )  =  ( X I V ) )
5352eleq2d 2499 . . . . . . 7  |-  ( v  =  V  ->  ( U  e.  ( X I v )  <->  U  e.  ( X I V ) ) )
54533anbi1d 1339 . . . . . 6  |-  ( v  =  V  ->  (
( U  e.  ( X I v )  /\  U  e.  ( Y I Z )  /\  X  =/=  U
)  <->  ( U  e.  ( X I V )  /\  U  e.  ( Y I Z )  /\  X  =/= 
U ) ) )
55 eleq1 2501 . . . . . . . 8  |-  ( v  =  V  ->  (
v  e.  ( a I b )  <->  V  e.  ( a I b ) ) )
56553anbi3d 1341 . . . . . . 7  |-  ( v  =  V  ->  (
( Y  e.  ( X I a )  /\  Z  e.  ( X I b )  /\  v  e.  ( a I b ) )  <->  ( Y  e.  ( X I a )  /\  Z  e.  ( X I b )  /\  V  e.  ( a I b ) ) ) )
57562rexbidv 2953 . . . . . 6  |-  ( v  =  V  ->  ( E. a  e.  P  E. b  e.  P  ( Y  e.  ( X I a )  /\  Z  e.  ( X I b )  /\  v  e.  ( a I b ) )  <->  E. a  e.  P  E. b  e.  P  ( Y  e.  ( X I a )  /\  Z  e.  ( X I b )  /\  V  e.  ( a I b ) ) ) )
5854, 57imbi12d 321 . . . . 5  |-  ( v  =  V  ->  (
( ( U  e.  ( X I v )  /\  U  e.  ( Y I Z )  /\  X  =/= 
U )  ->  E. a  e.  P  E. b  e.  P  ( Y  e.  ( X I a )  /\  Z  e.  ( X I b )  /\  v  e.  ( a I b ) ) )  <->  ( ( U  e.  ( X I V )  /\  U  e.  ( Y I Z )  /\  X  =/= 
U )  ->  E. a  e.  P  E. b  e.  P  ( Y  e.  ( X I a )  /\  Z  e.  ( X I b )  /\  V  e.  ( a I b ) ) ) ) )
5951, 58rspc2v 3197 . . . 4  |-  ( ( U  e.  P  /\  V  e.  P )  ->  ( A. u  e.  P  A. v  e.  P  ( ( u  e.  ( X I v )  /\  u  e.  ( Y I Z )  /\  X  =/=  u )  ->  E. a  e.  P  E. b  e.  P  ( Y  e.  ( X I a )  /\  Z  e.  ( X I b )  /\  v  e.  ( a I b ) ) )  -> 
( ( U  e.  ( X I V )  /\  U  e.  ( Y I Z )  /\  X  =/= 
U )  ->  E. a  e.  P  E. b  e.  P  ( Y  e.  ( X I a )  /\  Z  e.  ( X I b )  /\  V  e.  ( a I b ) ) ) ) )
6045, 46, 59syl2anc 665 . . 3  |-  ( ph  ->  ( A. u  e.  P  A. v  e.  P  ( ( u  e.  ( X I v )  /\  u  e.  ( Y I Z )  /\  X  =/=  u )  ->  E. a  e.  P  E. b  e.  P  ( Y  e.  ( X I a )  /\  Z  e.  ( X I b )  /\  v  e.  ( a I b ) ) )  -> 
( ( U  e.  ( X I V )  /\  U  e.  ( Y I Z )  /\  X  =/= 
U )  ->  E. a  e.  P  E. b  e.  P  ( Y  e.  ( X I a )  /\  Z  e.  ( X I b )  /\  V  e.  ( a I b ) ) ) ) )
6144, 60mpd 15 . 2  |-  ( ph  ->  ( ( U  e.  ( X I V )  /\  U  e.  ( Y I Z )  /\  X  =/= 
U )  ->  E. a  e.  P  E. b  e.  P  ( Y  e.  ( X I a )  /\  Z  e.  ( X I b )  /\  V  e.  ( a I b ) ) ) )
621, 2, 3, 61mp3and 1363 1  |-  ( ph  ->  E. a  e.  P  E. b  e.  P  ( Y  e.  ( X I a )  /\  Z  e.  ( X I b )  /\  V  e.  ( a I b ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1870    =/= wne 2625   A.wral 2782   E.wrex 2783   _Vcvv 3087   ` cfv 5601  (class class class)co 6305   Basecbs 15084   distcds 15161  TarskiGEcstrkge 24346  Itvcitv 24347
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-trkge 24362
This theorem is referenced by:  f1otrge  24748
  Copyright terms: Public domain W3C validator