Metamath Proof Explorer

Theorem hlcgreu

Description: The point constructed in hlcgrex is unique. Theorem 6.11 of Schwabhauser p. 44. (Contributed by Thierry Arnoux, 9-Aug-2020)

Ref Expression
Hypotheses ishlg.p 
|- P = ( Base ` G )
ishlg.i 
|- I = ( Itv ` G )
ishlg.k 
|- K = ( hlG ` G )
ishlg.a 
|- ( ph -> A e. P )
ishlg.b 
|- ( ph -> B e. P )
ishlg.c 
|- ( ph -> C e. P )
hlln.1 
|- ( ph -> G e. TarskiG )
hltr.d 
|- ( ph -> D e. P )
hlcgrex.m 
|- .- = ( dist ` G )
hlcgrex.1 
|- ( ph -> D =/= A )
hlcgrex.2 
|- ( ph -> B =/= C )
Assertion hlcgreu 
|- ( ph -> E! x e. P ( x ( K ` A ) D /\ ( A .- x ) = ( B .- C ) ) )

Proof

Step Hyp Ref Expression
1 ishlg.p 
 |-  P = ( Base ` G )
2 ishlg.i 
 |-  I = ( Itv ` G )
3 ishlg.k 
 |-  K = ( hlG ` G )
4 ishlg.a 
 |-  ( ph -> A e. P )
5 ishlg.b 
 |-  ( ph -> B e. P )
6 ishlg.c 
 |-  ( ph -> C e. P )
7 hlln.1 
 |-  ( ph -> G e. TarskiG )
8 hltr.d 
 |-  ( ph -> D e. P )
9 hlcgrex.m 
 |-  .- = ( dist ` G )
10 hlcgrex.1 
 |-  ( ph -> D =/= A )
11 hlcgrex.2 
 |-  ( ph -> B =/= C )
12 1 2 3 4 5 6 7 8 9 10 11 hlcgrex 
 |-  ( ph -> E. x e. P ( x ( K ` A ) D /\ ( A .- x ) = ( B .- C ) ) )
13 4 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` A ) D /\ ( A .- x ) = ( B .- C ) ) /\ ( y ( K ` A ) D /\ ( A .- y ) = ( B .- C ) ) ) ) -> A e. P )
14 5 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` A ) D /\ ( A .- x ) = ( B .- C ) ) /\ ( y ( K ` A ) D /\ ( A .- y ) = ( B .- C ) ) ) ) -> B e. P )
15 6 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` A ) D /\ ( A .- x ) = ( B .- C ) ) /\ ( y ( K ` A ) D /\ ( A .- y ) = ( B .- C ) ) ) ) -> C e. P )
16 7 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` A ) D /\ ( A .- x ) = ( B .- C ) ) /\ ( y ( K ` A ) D /\ ( A .- y ) = ( B .- C ) ) ) ) -> G e. TarskiG )
17 8 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` A ) D /\ ( A .- x ) = ( B .- C ) ) /\ ( y ( K ` A ) D /\ ( A .- y ) = ( B .- C ) ) ) ) -> D e. P )
18 10 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` A ) D /\ ( A .- x ) = ( B .- C ) ) /\ ( y ( K ` A ) D /\ ( A .- y ) = ( B .- C ) ) ) ) -> D =/= A )
19 11 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` A ) D /\ ( A .- x ) = ( B .- C ) ) /\ ( y ( K ` A ) D /\ ( A .- y ) = ( B .- C ) ) ) ) -> B =/= C )
20 simpllr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` A ) D /\ ( A .- x ) = ( B .- C ) ) /\ ( y ( K ` A ) D /\ ( A .- y ) = ( B .- C ) ) ) ) -> x e. P )
21 simplr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` A ) D /\ ( A .- x ) = ( B .- C ) ) /\ ( y ( K ` A ) D /\ ( A .- y ) = ( B .- C ) ) ) ) -> y e. P )
22 simprll 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` A ) D /\ ( A .- x ) = ( B .- C ) ) /\ ( y ( K ` A ) D /\ ( A .- y ) = ( B .- C ) ) ) ) -> x ( K ` A ) D )
23 simprrl 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` A ) D /\ ( A .- x ) = ( B .- C ) ) /\ ( y ( K ` A ) D /\ ( A .- y ) = ( B .- C ) ) ) ) -> y ( K ` A ) D )
24 simprlr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` A ) D /\ ( A .- x ) = ( B .- C ) ) /\ ( y ( K ` A ) D /\ ( A .- y ) = ( B .- C ) ) ) ) -> ( A .- x ) = ( B .- C ) )
25 simprrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` A ) D /\ ( A .- x ) = ( B .- C ) ) /\ ( y ( K ` A ) D /\ ( A .- y ) = ( B .- C ) ) ) ) -> ( A .- y ) = ( B .- C ) )
26 1 2 3 13 14 15 16 17 9 18 19 20 21 22 23 24 25 hlcgreulem 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` A ) D /\ ( A .- x ) = ( B .- C ) ) /\ ( y ( K ` A ) D /\ ( A .- y ) = ( B .- C ) ) ) ) -> x = y )
27 26 ex 
 |-  ( ( ( ph /\ x e. P ) /\ y e. P ) -> ( ( ( x ( K ` A ) D /\ ( A .- x ) = ( B .- C ) ) /\ ( y ( K ` A ) D /\ ( A .- y ) = ( B .- C ) ) ) -> x = y ) )
28 27 ralrimiva 
 |-  ( ( ph /\ x e. P ) -> A. y e. P ( ( ( x ( K ` A ) D /\ ( A .- x ) = ( B .- C ) ) /\ ( y ( K ` A ) D /\ ( A .- y ) = ( B .- C ) ) ) -> x = y ) )
29 28 ralrimiva 
 |-  ( ph -> A. x e. P A. y e. P ( ( ( x ( K ` A ) D /\ ( A .- x ) = ( B .- C ) ) /\ ( y ( K ` A ) D /\ ( A .- y ) = ( B .- C ) ) ) -> x = y ) )
30 breq1 
 |-  ( x = y -> ( x ( K ` A ) D <-> y ( K ` A ) D ) )
31 oveq2 
 |-  ( x = y -> ( A .- x ) = ( A .- y ) )
32 31 eqeq1d 
 |-  ( x = y -> ( ( A .- x ) = ( B .- C ) <-> ( A .- y ) = ( B .- C ) ) )
33 30 32 anbi12d 
 |-  ( x = y -> ( ( x ( K ` A ) D /\ ( A .- x ) = ( B .- C ) ) <-> ( y ( K ` A ) D /\ ( A .- y ) = ( B .- C ) ) ) )
34 33 reu4 
 |-  ( E! x e. P ( x ( K ` A ) D /\ ( A .- x ) = ( B .- C ) ) <-> ( E. x e. P ( x ( K ` A ) D /\ ( A .- x ) = ( B .- C ) ) /\ A. x e. P A. y e. P ( ( ( x ( K ` A ) D /\ ( A .- x ) = ( B .- C ) ) /\ ( y ( K ` A ) D /\ ( A .- y ) = ( B .- C ) ) ) -> x = y ) ) )
35 12 29 34 sylanbrc 
 |-  ( ph -> E! x e. P ( x ( K ` A ) D /\ ( A .- x ) = ( B .- C ) ) )