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 4 eqcomd 
 |-  ( ( p = P /\ i = I ) -> P = p )
6 5 adantr 
 |-  ( ( ( p = P /\ i = I ) /\ x e. P ) -> P = p )
7 6 adantr 
 |-  ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) -> P = p )
8 7 adantr 
 |-  ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) -> P = p )
9 8 adantr 
 |-  ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) -> P = p )
10 simp-6r 
 |-  ( ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ v e. P ) -> i = I )
11 10 eqcomd 
 |-  ( ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ v e. P ) -> I = i )
12 11 oveqd 
 |-  ( ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ v e. P ) -> ( x I v ) = ( x i v ) )
13 12 eleq2d 
 |-  ( ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ v e. P ) -> ( u e. ( x I v ) <-> u e. ( x i v ) ) )
14 11 oveqd 
 |-  ( ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ v e. P ) -> ( y I z ) = ( y i z ) )
15 14 eleq2d 
 |-  ( ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ v e. P ) -> ( u e. ( y I z ) <-> u e. ( y i z ) ) )
16 13 15 3anbi12d 
 |-  ( ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ v e. P ) -> ( ( u e. ( x I v ) /\ u e. ( y I z ) /\ x =/= u ) <-> ( u e. ( x i v ) /\ u e. ( y i z ) /\ x =/= u ) ) )
17 9 adantr 
 |-  ( ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ v e. P ) -> P = p )
18 17 adantr 
 |-  ( ( ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ v e. P ) /\ a e. P ) -> P = p )
19 10 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ v e. P ) /\ a e. P ) /\ b e. P ) -> i = I )
20 19 eqcomd 
 |-  ( ( ( ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ v e. P ) /\ a e. P ) /\ b e. P ) -> I = i )
21 20 oveqd 
 |-  ( ( ( ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ v e. P ) /\ a e. P ) /\ b e. P ) -> ( x I a ) = ( x i a ) )
22 21 eleq2d 
 |-  ( ( ( ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ v e. P ) /\ a e. P ) /\ b e. P ) -> ( y e. ( x I a ) <-> y e. ( x i a ) ) )
23 20 oveqd 
 |-  ( ( ( ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ v e. P ) /\ a e. P ) /\ b e. P ) -> ( x I b ) = ( x i b ) )
24 23 eleq2d 
 |-  ( ( ( ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ v e. P ) /\ a e. P ) /\ b e. P ) -> ( z e. ( x I b ) <-> z e. ( x i b ) ) )
25 20 oveqd 
 |-  ( ( ( ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ v e. P ) /\ a e. P ) /\ b e. P ) -> ( a I b ) = ( a i b ) )
26 25 eleq2d 
 |-  ( ( ( ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ v e. P ) /\ a e. P ) /\ b e. P ) -> ( v e. ( a I b ) <-> v e. ( a i b ) ) )
27 22 24 26 3anbi123d 
 |-  ( ( ( ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ v e. P ) /\ a e. P ) /\ b e. P ) -> ( ( 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 ) ) ) )
28 18 27 rexeqbidva 
 |-  ( ( ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ v e. P ) /\ a e. P ) -> ( 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 ) ) ) )
29 17 28 rexeqbidva 
 |-  ( ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ v e. P ) -> ( 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 ) ) ) )
30 16 29 imbi12d 
 |-  ( ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ 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 ) ) ) ) )
31 9 30 raleqbidva 
 |-  ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ 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. 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 ) ) ) ) )
32 8 31 raleqbidva 
 |-  ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ 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 ) ) ) ) )
33 7 32 raleqbidva 
 |-  ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ 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. 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 ) ) ) ) )
34 6 33 raleqbidva 
 |-  ( ( ( p = P /\ i = I ) /\ 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. 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 ) ) ) ) )
35 5 34 raleqbidva 
 |-  ( ( 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 ) ) ) ) )
36 1 3 35 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 ) ) ) ) )
37 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 ) ) ) }
38 36 37 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 ) ) ) ) )