Metamath Proof Explorer

Theorem axtgeucl

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)

Ref Expression
Hypotheses 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 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 ) ) )

Proof

Step Hyp Ref Expression
1 axtrkge.p 
 |-  P = ( Base ` G )
2 axtrkge.d 
 |-  .- = ( dist ` G )
3 axtrkge.i 
 |-  I = ( Itv ` G )
4 axtgeucl.g 
 |-  ( ph -> G e. TarskiGE )
5 axtgeucl.1 
 |-  ( ph -> X e. P )
6 axtgeucl.2 
 |-  ( ph -> Y e. P )
7 axtgeucl.3 
 |-  ( ph -> Z e. P )
8 axtgeucl.4 
 |-  ( ph -> U e. P )
9 axtgeucl.5 
 |-  ( ph -> V e. P )
10 axtgeucl.6 
 |-  ( ph -> U e. ( X I V ) )
11 axtgeucl.7 
 |-  ( ph -> U e. ( Y I Z ) )
12 axtgeucl.8 
 |-  ( ph -> X =/= U )
13 1 2 3 istrkge 
 |-  ( 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 ) ) ) ) )
14 4 13 sylib 
 |-  ( 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 ) ) ) ) )
15 14 simprd 
 |-  ( 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 ) ) ) )
16 oveq1 
 |-  ( x = X -> ( x I v ) = ( X I v ) )
17 16 eleq2d 
 |-  ( x = X -> ( u e. ( x I v ) <-> u e. ( X I v ) ) )
18 neeq1 
 |-  ( x = X -> ( x =/= u <-> X =/= u ) )
19 17 18 3anbi13d 
 |-  ( 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 ) ) )
20 oveq1 
 |-  ( x = X -> ( x I a ) = ( X I a ) )
21 20 eleq2d 
 |-  ( x = X -> ( y e. ( x I a ) <-> y e. ( X I a ) ) )
22 oveq1 
 |-  ( x = X -> ( x I b ) = ( X I b ) )
23 22 eleq2d 
 |-  ( x = X -> ( z e. ( x I b ) <-> z e. ( X I b ) ) )
24 21 23 3anbi12d 
 |-  ( 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 ) ) ) )
25 24 2rexbidv 
 |-  ( 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 ) ) ) )
26 19 25 imbi12d 
 |-  ( 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 ) ) ) ) )
27 26 2ralbidv 
 |-  ( 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 ) ) ) ) )
28 oveq1 
 |-  ( y = Y -> ( y I z ) = ( Y I z ) )
29 28 eleq2d 
 |-  ( y = Y -> ( u e. ( y I z ) <-> u e. ( Y I z ) ) )
30 29 3anbi2d 
 |-  ( 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 ) ) )
31 eleq1 
 |-  ( y = Y -> ( y e. ( X I a ) <-> Y e. ( X I a ) ) )
32 31 3anbi1d 
 |-  ( 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 ) ) ) )
33 32 2rexbidv 
 |-  ( 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 ) ) ) )
34 30 33 imbi12d 
 |-  ( 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 ) ) ) ) )
35 34 2ralbidv 
 |-  ( 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 ) ) ) ) )
36 oveq2 
 |-  ( z = Z -> ( Y I z ) = ( Y I Z ) )
37 36 eleq2d 
 |-  ( z = Z -> ( u e. ( Y I z ) <-> u e. ( Y I Z ) ) )
38 37 3anbi2d 
 |-  ( 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 ) ) )
39 eleq1 
 |-  ( z = Z -> ( z e. ( X I b ) <-> Z e. ( X I b ) ) )
40 39 3anbi2d 
 |-  ( 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 ) ) ) )
41 40 2rexbidv 
 |-  ( 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 ) ) ) )
42 38 41 imbi12d 
 |-  ( 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 ) ) ) ) )
43 42 2ralbidv 
 |-  ( 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 ) ) ) ) )
44 27 35 43 rspc3v 
 |-  ( ( 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 ) ) ) ) )
45 5 6 7 44 syl3anc 
 |-  ( 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 ) ) ) ) )
46 15 45 mpd 
 |-  ( 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 ) ) ) )
47 eleq1 
 |-  ( u = U -> ( u e. ( X I v ) <-> U e. ( X I v ) ) )
48 eleq1 
 |-  ( u = U -> ( u e. ( Y I Z ) <-> U e. ( Y I Z ) ) )
49 neeq2 
 |-  ( u = U -> ( X =/= u <-> X =/= U ) )
50 47 48 49 3anbi123d 
 |-  ( 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 ) ) )
51 50 imbi1d 
 |-  ( 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 
 |-  ( v = V -> ( X I v ) = ( X I V ) )
53 52 eleq2d 
 |-  ( v = V -> ( U e. ( X I v ) <-> U e. ( X I V ) ) )
54 53 3anbi1d 
 |-  ( 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 
 |-  ( v = V -> ( v e. ( a I b ) <-> V e. ( a I b ) ) )
56 55 3anbi3d 
 |-  ( 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 ) ) ) )
57 56 2rexbidv 
 |-  ( 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 ) ) ) )
58 54 57 imbi12d 
 |-  ( 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 ) ) ) ) )
59 51 58 rspc2v 
 |-  ( ( 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 ) ) ) ) )
60 8 9 59 syl2anc 
 |-  ( 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 ) ) ) ) )
61 46 60 mpd 
 |-  ( 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 ) ) ) )
62 10 11 12 61 mp3and 
 |-  ( ph -> E. a e. P E. b e. P ( Y e. ( X I a ) /\ Z e. ( X I b ) /\ V e. ( a I b ) ) )