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=BaseG
ishlg.i I=ItvG
ishlg.k K=hl𝒢G
ishlg.a φAP
ishlg.b φBP
ishlg.c φCP
hlln.1 φG𝒢Tarski
hltr.d φDP
hlcgrex.m -˙=distG
hlcgrex.1 φDA
hlcgrex.2 φBC
Assertion hlcgrex φxPxKADA-˙x=B-˙C

Proof

Step Hyp Ref Expression
1 ishlg.p P=BaseG
2 ishlg.i I=ItvG
3 ishlg.k K=hl𝒢G
4 ishlg.a φAP
5 ishlg.b φBP
6 ishlg.c φCP
7 hlln.1 φG𝒢Tarski
8 hltr.d φDP
9 hlcgrex.m -˙=distG
10 hlcgrex.1 φDA
11 hlcgrex.2 φBC
12 7 ad2antrr φyPADIyAyG𝒢Tarski
13 simplr φyPADIyAyyP
14 4 ad2antrr φyPADIyAyAP
15 5 ad2antrr φyPADIyAyBP
16 6 ad2antrr φyPADIyAyCP
17 1 9 2 12 13 14 15 16 axtgsegcon φyPADIyAyxPAyIxA-˙x=B-˙C
18 12 ad2antrr φyPADIyAyxPAyIxA-˙x=B-˙CG𝒢Tarski
19 15 ad2antrr φyPADIyAyxPAyIxA-˙x=B-˙CBP
20 16 ad2antrr φyPADIyAyxPAyIxA-˙x=B-˙CCP
21 simplr φyPADIyAyxPAyIxA-˙x=B-˙CxP
22 14 ad2antrr φyPADIyAyxPAyIxA-˙x=B-˙CAP
23 simprr φyPADIyAyxPAyIxA-˙x=B-˙CA-˙x=B-˙C
24 1 9 2 18 22 21 19 20 23 tgcgrcoml φyPADIyAyxPAyIxA-˙x=B-˙Cx-˙A=B-˙C
25 24 eqcomd φyPADIyAyxPAyIxA-˙x=B-˙CB-˙C=x-˙A
26 11 ad4antr φyPADIyAyxPAyIxA-˙x=B-˙CBC
27 1 9 2 18 19 20 21 22 25 26 tgcgrneq φyPADIyAyxPAyIxA-˙x=B-˙CxA
28 10 ad4antr φyPADIyAyxPAyIxA-˙x=B-˙CDA
29 13 ad2antrr φyPADIyAyxPAyIxA-˙x=B-˙CyP
30 8 ad4antr φyPADIyAyxPAyIxA-˙x=B-˙CDP
31 simpllr φyPADIyAyxPAyIxA-˙x=B-˙CADIyAy
32 31 simprd φyPADIyAyxPAyIxA-˙x=B-˙CAy
33 32 necomd φyPADIyAyxPAyIxA-˙x=B-˙CyA
34 simprl φyPADIyAyxPAyIxA-˙x=B-˙CAyIx
35 31 simpld φyPADIyAyxPAyIxA-˙x=B-˙CADIy
36 1 9 2 18 30 22 29 35 tgbtwncom φyPADIyAyxPAyIxA-˙x=B-˙CAyID
37 1 2 18 29 22 21 30 33 34 36 tgbtwnconn2 φyPADIyAyxPAyIxA-˙x=B-˙CxAIDDAIx
38 1 2 3 21 30 22 18 ishlg φyPADIyAyxPAyIxA-˙x=B-˙CxKADxADAxAIDDAIx
39 27 28 37 38 mpbir3and φyPADIyAyxPAyIxA-˙x=B-˙CxKAD
40 39 23 jca φyPADIyAyxPAyIxA-˙x=B-˙CxKADA-˙x=B-˙C
41 40 ex φyPADIyAyxPAyIxA-˙x=B-˙CxKADA-˙x=B-˙C
42 41 reximdva φyPADIyAyxPAyIxA-˙x=B-˙CxPxKADA-˙x=B-˙C
43 17 42 mpd φyPADIyAyxPxKADA-˙x=B-˙C
44 1 fvexi PV
45 44 a1i φPV
46 45 5 6 11 nehash2 φ2P
47 1 9 2 7 8 4 46 tgbtwndiff φyPADIyAy
48 43 47 r19.29a φxPxKADA-˙x=B-˙C