Theorem hlcgreq

Description: A constructed point on a half-line, at a given distance of its origin, (see hlcgrex ) is unique. Theorem 6.11 of Schwabhauser p. 44. (Contributed by Thierry Arnoux, 9-Aug-2020)

	Ref	Expression
Hypotheses	hlcgreq.p	|- P = ( Base ` G )
	hlcgreq.i	|- .- = ( dist ` G )
	hlcgreq.k	|- K = ( hlG ` G )
	hlcgreq.a	|- ( ph -> A e. P )
	hlcgreq.b	|- ( ph -> B e. P )
	hlcgreq.c	|- ( ph -> C e. P )
	hlcgreq.g	|- ( ph -> G e. TarskiG )
	hlcgreq.d	|- ( ph -> D e. P )
	hlcgreq.1	|- ( ph -> D =/= A )
	hlcgreq.2	|- ( ph -> B =/= C )
	hlcgreq.3	|- ( ph -> X ( K ` A ) D )
	hlcgreq.4	|- ( ph -> Y ( K ` A ) D )
	hlcgreq.5	|- ( ph -> ( A .- X ) = ( B .- C ) )
	hlcgreq.6	|- ( ph -> ( A .- Y ) = ( B .- C ) )
Assertion	hlcgreq	|- ( ph -> X = Y )

Proof

Step	Hyp	Ref	Expression
1		hlcgreq.p	|- P = ( Base ` G )
2		hlcgreq.i	|- .- = ( dist ` G )
3		hlcgreq.k	|- K = ( hlG ` G )
4		hlcgreq.a	|- ( ph -> A e. P )
5		hlcgreq.b	|- ( ph -> B e. P )
6		hlcgreq.c	|- ( ph -> C e. P )
7		hlcgreq.g	|- ( ph -> G e. TarskiG )
8		hlcgreq.d	|- ( ph -> D e. P )
9		hlcgreq.1	|- ( ph -> D =/= A )
10		hlcgreq.2	|- ( ph -> B =/= C )
11		hlcgreq.3	|- ( ph -> X ( K ` A ) D )
12		hlcgreq.4	|- ( ph -> Y ( K ` A ) D )
13		hlcgreq.5	|- ( ph -> ( A .- X ) = ( B .- C ) )
14		hlcgreq.6	|- ( ph -> ( A .- Y ) = ( B .- C ) )
15		eqid	|- ( Itv ` G ) = ( Itv ` G )
16	1 15 3 7 4 11	hlgrcl1	|- ( ph -> X e. P )
17	1 15 3 7 4 12	hlgrcl1	|- ( ph -> Y e. P )
18	1 15 3 4 5 6 7 8 2 9 10 16 17 11 12 13 14	hlcgreulem	|- ( ph -> X = Y )