Metamath Proof Explorer

Theorem mideu

Description: Existence and uniqueness of the midpoint, Theorem 8.22 of Schwabhauser p. 64. (Contributed by Thierry Arnoux, 25-Nov-2019)

Ref Expression
Hypotheses colperpex.p 
|- P = ( Base ` G )
colperpex.d 
|- .- = ( dist ` G )
colperpex.i 
|- I = ( Itv ` G )
colperpex.l 
|- L = ( LineG ` G )
colperpex.g 
|- ( ph -> G e. TarskiG )
mideu.s 
|- S = ( pInvG ` G )
mideu.1 
|- ( ph -> A e. P )
mideu.2 
|- ( ph -> B e. P )
mideu.3 
|- ( ph -> G TarskiGDim>= 2 )
Assertion mideu 
|- ( ph -> E! x e. P B = ( ( S ` x ) ` A ) )

Proof

Step Hyp Ref Expression
1 colperpex.p 
 |-  P = ( Base ` G )
2 colperpex.d 
 |-  .- = ( dist ` G )
3 colperpex.i 
 |-  I = ( Itv ` G )
4 colperpex.l 
 |-  L = ( LineG ` G )
5 colperpex.g 
 |-  ( ph -> G e. TarskiG )
6 mideu.s 
 |-  S = ( pInvG ` G )
7 mideu.1 
 |-  ( ph -> A e. P )
8 mideu.2 
 |-  ( ph -> B e. P )
9 mideu.3 
 |-  ( ph -> G TarskiGDim>= 2 )
10 1 2 3 4 5 6 7 8 9 midex 
 |-  ( ph -> E. x e. P B = ( ( S ` x ) ` A ) )
11 5 ad2antrr 
 |-  ( ( ( ph /\ ( x e. P /\ y e. P ) ) /\ ( B = ( ( S ` x ) ` A ) /\ B = ( ( S ` y ) ` A ) ) ) -> G e. TarskiG )
12 simplrl 
 |-  ( ( ( ph /\ ( x e. P /\ y e. P ) ) /\ ( B = ( ( S ` x ) ` A ) /\ B = ( ( S ` y ) ` A ) ) ) -> x e. P )
13 simplrr 
 |-  ( ( ( ph /\ ( x e. P /\ y e. P ) ) /\ ( B = ( ( S ` x ) ` A ) /\ B = ( ( S ` y ) ` A ) ) ) -> y e. P )
14 7 ad2antrr 
 |-  ( ( ( ph /\ ( x e. P /\ y e. P ) ) /\ ( B = ( ( S ` x ) ` A ) /\ B = ( ( S ` y ) ` A ) ) ) -> A e. P )
15 8 ad2antrr 
 |-  ( ( ( ph /\ ( x e. P /\ y e. P ) ) /\ ( B = ( ( S ` x ) ` A ) /\ B = ( ( S ` y ) ` A ) ) ) -> B e. P )
16 simprl 
 |-  ( ( ( ph /\ ( x e. P /\ y e. P ) ) /\ ( B = ( ( S ` x ) ` A ) /\ B = ( ( S ` y ) ` A ) ) ) -> B = ( ( S ` x ) ` A ) )
17 16 eqcomd 
 |-  ( ( ( ph /\ ( x e. P /\ y e. P ) ) /\ ( B = ( ( S ` x ) ` A ) /\ B = ( ( S ` y ) ` A ) ) ) -> ( ( S ` x ) ` A ) = B )
18 simprr 
 |-  ( ( ( ph /\ ( x e. P /\ y e. P ) ) /\ ( B = ( ( S ` x ) ` A ) /\ B = ( ( S ` y ) ` A ) ) ) -> B = ( ( S ` y ) ` A ) )
19 18 eqcomd 
 |-  ( ( ( ph /\ ( x e. P /\ y e. P ) ) /\ ( B = ( ( S ` x ) ` A ) /\ B = ( ( S ` y ) ` A ) ) ) -> ( ( S ` y ) ` A ) = B )
20 1 2 3 4 6 11 12 13 14 15 17 19 miduniq 
 |-  ( ( ( ph /\ ( x e. P /\ y e. P ) ) /\ ( B = ( ( S ` x ) ` A ) /\ B = ( ( S ` y ) ` A ) ) ) -> x = y )
21 20 ex 
 |-  ( ( ph /\ ( x e. P /\ y e. P ) ) -> ( ( B = ( ( S ` x ) ` A ) /\ B = ( ( S ` y ) ` A ) ) -> x = y ) )
22 21 ralrimivva 
 |-  ( ph -> A. x e. P A. y e. P ( ( B = ( ( S ` x ) ` A ) /\ B = ( ( S ` y ) ` A ) ) -> x = y ) )
23 fveq2 
 |-  ( x = y -> ( S ` x ) = ( S ` y ) )
24 23 fveq1d 
 |-  ( x = y -> ( ( S ` x ) ` A ) = ( ( S ` y ) ` A ) )
25 24 eqeq2d 
 |-  ( x = y -> ( B = ( ( S ` x ) ` A ) <-> B = ( ( S ` y ) ` A ) ) )
26 25 rmo4 
 |-  ( E* x e. P B = ( ( S ` x ) ` A ) <-> A. x e. P A. y e. P ( ( B = ( ( S ` x ) ` A ) /\ B = ( ( S ` y ) ` A ) ) -> x = y ) )
27 22 26 sylibr 
 |-  ( ph -> E* x e. P B = ( ( S ` x ) ` A ) )
28 reu5 
 |-  ( E! x e. P B = ( ( S ` x ) ` A ) <-> ( E. x e. P B = ( ( S ` x ) ` A ) /\ E* x e. P B = ( ( S ` x ) ` A ) ) )
29 10 27 28 sylanbrc 
 |-  ( ph -> E! x e. P B = ( ( S ` x ) ` A ) )