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={\mathrm{Base}}_G$$
	hlcgreq.i	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	hlcgreq.k	$$⊢K={hl}_{𝒢}\left(G\right)$$
	hlcgreq.a	$$⊢\phi \to A\in P$$
	hlcgreq.b	$$⊢\phi \to B\in P$$
	hlcgreq.c	$$⊢\phi \to C\in P$$
	hlcgreq.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	hlcgreq.d	$$⊢\phi \to D\in P$$
	hlcgreq.1	$$⊢\phi \to D\ne A$$
	hlcgreq.2	$$⊢\phi \to B\ne C$$
	hlcgreq.3	$$⊢\phi \to XK\left(A\right)D$$
	hlcgreq.4	$$⊢\phi \to YK\left(A\right)D$$
	hlcgreq.5	$$⊢\phi \to A\underset{\dot{}}{-}X=B\underset{\dot{}}{-}C$$
	hlcgreq.6	$$⊢\phi \to A\underset{\dot{}}{-}Y=B\underset{\dot{}}{-}C$$
Assertion	hlcgreq	$$⊢\phi \to X=Y$$

Proof

Step	Hyp	Ref	Expression
1		hlcgreq.p	$$⊢P={\mathrm{Base}}_G$$
2		hlcgreq.i	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		hlcgreq.k	$$⊢K={hl}_{𝒢}\left(G\right)$$
4		hlcgreq.a	$$⊢\phi \to A\in P$$
5		hlcgreq.b	$$⊢\phi \to B\in P$$
6		hlcgreq.c	$$⊢\phi \to C\in P$$
7		hlcgreq.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
8		hlcgreq.d	$$⊢\phi \to D\in P$$
9		hlcgreq.1	$$⊢\phi \to D\ne A$$
10		hlcgreq.2	$$⊢\phi \to B\ne C$$
11		hlcgreq.3	$$⊢\phi \to XK\left(A\right)D$$
12		hlcgreq.4	$$⊢\phi \to YK\left(A\right)D$$
13		hlcgreq.5	$$⊢\phi \to A\underset{\dot{}}{-}X=B\underset{\dot{}}{-}C$$
14		hlcgreq.6	$$⊢\phi \to A\underset{\dot{}}{-}Y=B\underset{\dot{}}{-}C$$
15		eqid	$$⊢\mathrm{Itv}\left(G\right)=\mathrm{Itv}\left(G\right)$$
16	1 15 3 7 4 11	hlgrcl1	$$⊢\phi \to X\in P$$
17	1 15 3 7 4 12	hlgrcl1	$$⊢\phi \to Y\in P$$
18	1 15 3 4 5 6 7 8 2 9 10 16 17 11 12 13 14	hlcgreulem	$$⊢\phi \to X=Y$$