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 ( 𝜑 → ∃! 𝑥𝑃 ( 𝑥 ( 𝐾𝐴 ) 𝐷 ∧ ( 𝐴 𝑥 ) = ( 𝐵 𝐶 ) ) )