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	⊢ 𝑃 = ( Base ‘ 𝐺 )
	hlcgreq.i	⊢ − = ( dist ‘ 𝐺 )
	hlcgreq.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
	hlcgreq.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	hlcgreq.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	hlcgreq.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
	hlcgreq.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	hlcgreq.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
	hlcgreq.1	⊢ ( 𝜑 → 𝐷 ≠ 𝐴 )
	hlcgreq.2	⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
	hlcgreq.3	⊢ ( 𝜑 → 𝑋 ( 𝐾 ‘ 𝐴 ) 𝐷 )
	hlcgreq.4	⊢ ( 𝜑 → 𝑌 ( 𝐾 ‘ 𝐴 ) 𝐷 )
	hlcgreq.5	⊢ ( 𝜑 → ( 𝐴 − 𝑋 ) = ( 𝐵 − 𝐶 ) )
	hlcgreq.6	⊢ ( 𝜑 → ( 𝐴 − 𝑌 ) = ( 𝐵 − 𝐶 ) )
Assertion	hlcgreq	⊢ ( 𝜑 → 𝑋 = 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		hlcgreq.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		hlcgreq.i	⊢ − = ( dist ‘ 𝐺 )
3		hlcgreq.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
4		hlcgreq.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
5		hlcgreq.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
6		hlcgreq.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
7		hlcgreq.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
8		hlcgreq.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
9		hlcgreq.1	⊢ ( 𝜑 → 𝐷 ≠ 𝐴 )
10		hlcgreq.2	⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
11		hlcgreq.3	⊢ ( 𝜑 → 𝑋 ( 𝐾 ‘ 𝐴 ) 𝐷 )
12		hlcgreq.4	⊢ ( 𝜑 → 𝑌 ( 𝐾 ‘ 𝐴 ) 𝐷 )
13		hlcgreq.5	⊢ ( 𝜑 → ( 𝐴 − 𝑋 ) = ( 𝐵 − 𝐶 ) )
14		hlcgreq.6	⊢ ( 𝜑 → ( 𝐴 − 𝑌 ) = ( 𝐵 − 𝐶 ) )
15		eqid	⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
16	1 15 3 7 4 11	hlgrcl1	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
17	1 15 3 7 4 12	hlgrcl1	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
18	1 15 3 4 5 6 7 8 2 9 10 16 17 11 12 13 14	hlcgreulem	⊢ ( 𝜑 → 𝑋 = 𝑌 )