Metamath Proof Explorer

Theorem hlcgrex

Description: Construct a point on a half-line, at a given distance of its origin. (Contributed by Thierry Arnoux, 1-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 hlcgrex 
|- ( 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 7 ad2antrr 
 |-  ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) -> G e. TarskiG )
13 simplr 
 |-  ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) -> y e. P )
14 4 ad2antrr 
 |-  ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) -> A e. P )
15 5 ad2antrr 
 |-  ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) -> B e. P )
16 6 ad2antrr 
 |-  ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) -> C e. P )
17 1 9 2 12 13 14 15 16 axtgsegcon 
 |-  ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) -> E. x e. P ( A e. ( y I x ) /\ ( A .- x ) = ( B .- C ) ) )
18 12 ad2antrr 
 |-  ( ( ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) /\ x e. P ) /\ ( A e. ( y I x ) /\ ( A .- x ) = ( B .- C ) ) ) -> G e. TarskiG )
19 15 ad2antrr 
 |-  ( ( ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) /\ x e. P ) /\ ( A e. ( y I x ) /\ ( A .- x ) = ( B .- C ) ) ) -> B e. P )
20 16 ad2antrr 
 |-  ( ( ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) /\ x e. P ) /\ ( A e. ( y I x ) /\ ( A .- x ) = ( B .- C ) ) ) -> C e. P )
21 simplr 
 |-  ( ( ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) /\ x e. P ) /\ ( A e. ( y I x ) /\ ( A .- x ) = ( B .- C ) ) ) -> x e. P )
22 14 ad2antrr 
 |-  ( ( ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) /\ x e. P ) /\ ( A e. ( y I x ) /\ ( A .- x ) = ( B .- C ) ) ) -> A e. P )
23 simprr 
 |-  ( ( ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) /\ x e. P ) /\ ( A e. ( y I x ) /\ ( A .- x ) = ( B .- C ) ) ) -> ( A .- x ) = ( B .- C ) )
24 1 9 2 18 22 21 19 20 23 tgcgrcoml 
 |-  ( ( ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) /\ x e. P ) /\ ( A e. ( y I x ) /\ ( A .- x ) = ( B .- C ) ) ) -> ( x .- A ) = ( B .- C ) )
25 24 eqcomd 
 |-  ( ( ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) /\ x e. P ) /\ ( A e. ( y I x ) /\ ( A .- x ) = ( B .- C ) ) ) -> ( B .- C ) = ( x .- A ) )
26 11 ad4antr 
 |-  ( ( ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) /\ x e. P ) /\ ( A e. ( y I x ) /\ ( A .- x ) = ( B .- C ) ) ) -> B =/= C )
27 1 9 2 18 19 20 21 22 25 26 tgcgrneq 
 |-  ( ( ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) /\ x e. P ) /\ ( A e. ( y I x ) /\ ( A .- x ) = ( B .- C ) ) ) -> x =/= A )
28 10 ad4antr 
 |-  ( ( ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) /\ x e. P ) /\ ( A e. ( y I x ) /\ ( A .- x ) = ( B .- C ) ) ) -> D =/= A )
29 13 ad2antrr 
 |-  ( ( ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) /\ x e. P ) /\ ( A e. ( y I x ) /\ ( A .- x ) = ( B .- C ) ) ) -> y e. P )
30 8 ad4antr 
 |-  ( ( ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) /\ x e. P ) /\ ( A e. ( y I x ) /\ ( A .- x ) = ( B .- C ) ) ) -> D e. P )
31 simpllr 
 |-  ( ( ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) /\ x e. P ) /\ ( A e. ( y I x ) /\ ( A .- x ) = ( B .- C ) ) ) -> ( A e. ( D I y ) /\ A =/= y ) )
32 31 simprd 
 |-  ( ( ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) /\ x e. P ) /\ ( A e. ( y I x ) /\ ( A .- x ) = ( B .- C ) ) ) -> A =/= y )
33 32 necomd 
 |-  ( ( ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) /\ x e. P ) /\ ( A e. ( y I x ) /\ ( A .- x ) = ( B .- C ) ) ) -> y =/= A )
34 simprl 
 |-  ( ( ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) /\ x e. P ) /\ ( A e. ( y I x ) /\ ( A .- x ) = ( B .- C ) ) ) -> A e. ( y I x ) )
35 31 simpld 
 |-  ( ( ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) /\ x e. P ) /\ ( A e. ( y I x ) /\ ( A .- x ) = ( B .- C ) ) ) -> A e. ( D I y ) )
36 1 9 2 18 30 22 29 35 tgbtwncom 
 |-  ( ( ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) /\ x e. P ) /\ ( A e. ( y I x ) /\ ( A .- x ) = ( B .- C ) ) ) -> A e. ( y I D ) )
37 1 2 18 29 22 21 30 33 34 36 tgbtwnconn2 
 |-  ( ( ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) /\ x e. P ) /\ ( A e. ( y I x ) /\ ( A .- x ) = ( B .- C ) ) ) -> ( x e. ( A I D ) \/ D e. ( A I x ) ) )
38 1 2 3 21 30 22 18 ishlg 
 |-  ( ( ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) /\ x e. P ) /\ ( A e. ( y I x ) /\ ( A .- x ) = ( B .- C ) ) ) -> ( x ( K ` A ) D <-> ( x =/= A /\ D =/= A /\ ( x e. ( A I D ) \/ D e. ( A I x ) ) ) ) )
39 27 28 37 38 mpbir3and 
 |-  ( ( ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) /\ x e. P ) /\ ( A e. ( y I x ) /\ ( A .- x ) = ( B .- C ) ) ) -> x ( K ` A ) D )
40 39 23 jca 
 |-  ( ( ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) /\ x e. P ) /\ ( A e. ( y I x ) /\ ( A .- x ) = ( B .- C ) ) ) -> ( x ( K ` A ) D /\ ( A .- x ) = ( B .- C ) ) )
41 40 ex 
 |-  ( ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) /\ x e. P ) -> ( ( A e. ( y I x ) /\ ( A .- x ) = ( B .- C ) ) -> ( x ( K ` A ) D /\ ( A .- x ) = ( B .- C ) ) ) )
42 41 reximdva 
 |-  ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) -> ( E. x e. P ( A e. ( y I x ) /\ ( A .- x ) = ( B .- C ) ) -> E. x e. P ( x ( K ` A ) D /\ ( A .- x ) = ( B .- C ) ) ) )
43 17 42 mpd 
 |-  ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) -> E. x e. P ( x ( K ` A ) D /\ ( A .- x ) = ( B .- C ) ) )
44 1 fvexi 
 |-  P e. _V
45 44 a1i 
 |-  ( ph -> P e. _V )
46 45 5 6 11 nehash2 
 |-  ( ph -> 2 <_ ( # ` P ) )
47 1 9 2 7 8 4 46 tgbtwndiff 
 |-  ( ph -> E. y e. P ( A e. ( D I y ) /\ A =/= y ) )
48 43 47 r19.29a 
 |-  ( ph -> E. x e. P ( x ( K ` A ) D /\ ( A .- x ) = ( B .- C ) ) )