Metamath Proof Explorer

Theorem istrkge

Description: Property of fulfilling Euclid's axiom. (Contributed by Thierry Arnoux, 14-Mar-2019)

Ref Expression
Hypotheses istrkg.p 
|- P = ( Base ` G )
istrkg.d 
|- .- = ( dist ` G )
istrkg.i 
|- I = ( Itv ` G )
Assertion 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 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 istrkg.p 
 |-  P = ( Base ` G )
2 istrkg.d 
 |-  .- = ( dist ` G )
3 istrkg.i 
 |-  I = ( Itv ` G )
4 simpl 
 |-  ( ( p = P /\ i = I ) -> p = P )
5 simpr 
 |-  ( ( p = P /\ i = I ) -> i = I )
6 5 oveqd 
 |-  ( ( p = P /\ i = I ) -> ( x i v ) = ( x I v ) )
7 6 eleq2d 
 |-  ( ( p = P /\ i = I ) -> ( u e. ( x i v ) <-> u e. ( x I v ) ) )
8 5 oveqd 
 |-  ( ( p = P /\ i = I ) -> ( y i z ) = ( y I z ) )
9 8 eleq2d 
 |-  ( ( p = P /\ i = I ) -> ( u e. ( y i z ) <-> u e. ( y I z ) ) )
10 7 9 3anbi12d 
 |-  ( ( p = P /\ i = I ) -> ( ( u e. ( x i v ) /\ u e. ( y i z ) /\ x =/= u ) <-> ( u e. ( x I v ) /\ u e. ( y I z ) /\ x =/= u ) ) )
11 5 oveqd 
 |-  ( ( p = P /\ i = I ) -> ( x i a ) = ( x I a ) )
12 11 eleq2d 
 |-  ( ( p = P /\ i = I ) -> ( y e. ( x i a ) <-> y e. ( x I a ) ) )
13 5 oveqd 
 |-  ( ( p = P /\ i = I ) -> ( x i b ) = ( x I b ) )
14 13 eleq2d 
 |-  ( ( p = P /\ i = I ) -> ( z e. ( x i b ) <-> z e. ( x I b ) ) )
15 5 oveqd 
 |-  ( ( p = P /\ i = I ) -> ( a i b ) = ( a I b ) )
16 15 eleq2d 
 |-  ( ( p = P /\ i = I ) -> ( v e. ( a i b ) <-> v e. ( a I b ) ) )
17 12 14 16 3anbi123d 
 |-  ( ( p = P /\ i = I ) -> ( ( 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 ) ) ) )
18 4 17 rexeqbidv 
 |-  ( ( p = P /\ i = I ) -> ( E. b e. p ( y e. ( x i a ) /\ z e. ( x i b ) /\ v e. ( a i b ) ) <-> E. b e. P ( y e. ( x I a ) /\ z e. ( x I b ) /\ v e. ( a I b ) ) ) )
19 4 18 rexeqbidv 
 |-  ( ( p = P /\ i = I ) -> ( 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 ) ) ) )
20 10 19 imbi12d 
 |-  ( ( p = P /\ i = I ) -> ( ( ( 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 ) ) ) ) )
21 4 20 raleqbidv 
 |-  ( ( p = P /\ i = I ) -> ( 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. 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 ) ) ) ) )
22 4 21 raleqbidv 
 |-  ( ( p = P /\ i = I ) -> ( 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 ) ) ) ) )
23 4 22 raleqbidv 
 |-  ( ( p = P /\ i = I ) -> ( 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. 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 ) ) ) ) )
24 4 23 raleqbidv 
 |-  ( ( p = P /\ i = I ) -> ( 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. 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 ) ) ) ) )
25 4 24 raleqbidv 
 |-  ( ( p = P /\ i = I ) -> ( 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. 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 ) ) ) ) )
26 1 3 25 sbcie2s 
 |-  ( f = G -> ( [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. 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. 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 ) ) ) ) )
27 df-trkge 
 |-  TarskiGE = { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. 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 ) ) ) }
28 26 27 elab4g 
 |-  ( 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 ) ) ) ) )