Metamath Proof Explorer

Theorem hlcgreu

Description: The point constructed in hlcgrex is unique. Theorem 6.11 of Schwabhauser p. 44. (Contributed by Thierry Arnoux, 9-Aug-2020)

Ref Expression
Hypotheses ishlg.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
ishlg.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
ishlg.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
ishlg.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
ishlg.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
ishlg.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
hlln.1 ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
hltr.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
hlcgrex.m ⊢ − = ( dist ‘ 𝐺 )
hlcgrex.1 ⊢ ( 𝜑 → 𝐷 ≠ 𝐴 )
hlcgrex.2 ⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
Assertion hlcgreu ( 𝜑 → ∃! 𝑥 ∈ 𝑃 ( 𝑥 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 ishlg.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 ishlg.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 ishlg.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
4 ishlg.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
5 ishlg.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
6 ishlg.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
7 hlln.1 ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
8 hltr.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
9 hlcgrex.m ⊢ − = ( dist ‘ 𝐺 )
10 hlcgrex.1 ⊢ ( 𝜑 → 𝐷 ≠ 𝐴 )
11 hlcgrex.2 ⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
12 1 2 3 4 5 6 7 8 9 10 11 hlcgrex ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) )
13 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝐴 ∈ 𝑃 )
14 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝐵 ∈ 𝑃 )
15 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝐶 ∈ 𝑃 )
16 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝐺 ∈ TarskiG )
17 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝐷 ∈ 𝑃 )
18 10 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝐷 ≠ 𝐴 )
19 11 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝐵 ≠ 𝐶 )
20 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝑥 ∈ 𝑃 )
21 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝑦 ∈ 𝑃 )
22 simprll ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝑥 ( 𝐾 ‘ 𝐴 ) 𝐷 )
23 simprrl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝑦 ( 𝐾 ‘ 𝐴 ) 𝐷 )
24 simprlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → ( 𝐴 − 𝑥 ) = ( 𝐵 − 𝐶 ) )
25 simprrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → ( 𝐴 − 𝑦 ) = ( 𝐵 − 𝐶 ) )
26 1 2 3 13 14 15 16 17 9 18 19 20 21 22 23 24 25 hlcgreulem ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝑥 = 𝑦 )
27 26 ex ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) → ( ( ( 𝑥 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) → 𝑥 = 𝑦 ) )
28 27 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → ∀ 𝑦 ∈ 𝑃 ( ( ( 𝑥 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) → 𝑥 = 𝑦 ) )
29 28 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( ( ( 𝑥 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) → 𝑥 = 𝑦 ) )
30 breq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ( 𝐾 ‘ 𝐴 ) 𝐷 ↔ 𝑦 ( 𝐾 ‘ 𝐴 ) 𝐷 ) )
31 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 − 𝑥 ) = ( 𝐴 − 𝑦 ) )
32 31 eqeq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 − 𝑥 ) = ( 𝐵 − 𝐶 ) ↔ ( 𝐴 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) )
33 30 32 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) ↔ ( 𝑦 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) )
34 33 reu4 ⊢ ( ∃! 𝑥 ∈ 𝑃 ( 𝑥 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) ↔ ( ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( ( ( 𝑥 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) → 𝑥 = 𝑦 ) ) )
35 12 29 34 sylanbrc ⊢ ( 𝜑 → ∃! 𝑥 ∈ 𝑃 ( 𝑥 ( 𝐾 ‘ 𝐴 ) 𝐷 ∧ ( 𝐴 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) )