Metamath Proof Explorer


Theorem hlcgrex

Description: Construct a point on a half-line, at a given distance of its origin. (Contributed by Thierry Arnoux, 1-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 hlcgrex ( 𝜑 → ∃ 𝑥𝑃 ( 𝑥 ( 𝐾𝐴 ) 𝐷 ∧ ( 𝐴 𝑥 ) = ( 𝐵 𝐶 ) ) )

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 7 ad2antrr ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) → 𝐺 ∈ TarskiG )
13 simplr ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) → 𝑦𝑃 )
14 4 ad2antrr ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) → 𝐴𝑃 )
15 5 ad2antrr ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) → 𝐵𝑃 )
16 6 ad2antrr ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) → 𝐶𝑃 )
17 1 9 2 12 13 14 15 16 axtgsegcon ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) → ∃ 𝑥𝑃 ( 𝐴 ∈ ( 𝑦 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐵 𝐶 ) ) )
18 12 ad2antrr ( ( ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) ∧ 𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝑦 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐵 𝐶 ) ) ) → 𝐺 ∈ TarskiG )
19 15 ad2antrr ( ( ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) ∧ 𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝑦 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐵 𝐶 ) ) ) → 𝐵𝑃 )
20 16 ad2antrr ( ( ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) ∧ 𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝑦 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐵 𝐶 ) ) ) → 𝐶𝑃 )
21 simplr ( ( ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) ∧ 𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝑦 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐵 𝐶 ) ) ) → 𝑥𝑃 )
22 14 ad2antrr ( ( ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) ∧ 𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝑦 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐵 𝐶 ) ) ) → 𝐴𝑃 )
23 simprr ( ( ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) ∧ 𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝑦 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐵 𝐶 ) ) ) → ( 𝐴 𝑥 ) = ( 𝐵 𝐶 ) )
24 1 9 2 18 22 21 19 20 23 tgcgrcoml ( ( ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) ∧ 𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝑦 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐵 𝐶 ) ) ) → ( 𝑥 𝐴 ) = ( 𝐵 𝐶 ) )
25 24 eqcomd ( ( ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) ∧ 𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝑦 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐵 𝐶 ) ) ) → ( 𝐵 𝐶 ) = ( 𝑥 𝐴 ) )
26 11 ad4antr ( ( ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) ∧ 𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝑦 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐵 𝐶 ) ) ) → 𝐵𝐶 )
27 1 9 2 18 19 20 21 22 25 26 tgcgrneq ( ( ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) ∧ 𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝑦 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐵 𝐶 ) ) ) → 𝑥𝐴 )
28 10 ad4antr ( ( ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) ∧ 𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝑦 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐵 𝐶 ) ) ) → 𝐷𝐴 )
29 13 ad2antrr ( ( ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) ∧ 𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝑦 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐵 𝐶 ) ) ) → 𝑦𝑃 )
30 8 ad4antr ( ( ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) ∧ 𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝑦 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐵 𝐶 ) ) ) → 𝐷𝑃 )
31 simpllr ( ( ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) ∧ 𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝑦 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐵 𝐶 ) ) ) → ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) )
32 31 simprd ( ( ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) ∧ 𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝑦 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐵 𝐶 ) ) ) → 𝐴𝑦 )
33 32 necomd ( ( ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) ∧ 𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝑦 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐵 𝐶 ) ) ) → 𝑦𝐴 )
34 simprl ( ( ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) ∧ 𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝑦 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐵 𝐶 ) ) ) → 𝐴 ∈ ( 𝑦 𝐼 𝑥 ) )
35 31 simpld ( ( ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) ∧ 𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝑦 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐵 𝐶 ) ) ) → 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) )
36 1 9 2 18 30 22 29 35 tgbtwncom ( ( ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) ∧ 𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝑦 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐵 𝐶 ) ) ) → 𝐴 ∈ ( 𝑦 𝐼 𝐷 ) )
37 1 2 18 29 22 21 30 33 34 36 tgbtwnconn2 ( ( ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) ∧ 𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝑦 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐵 𝐶 ) ) ) → ( 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) ∨ 𝐷 ∈ ( 𝐴 𝐼 𝑥 ) ) )
38 1 2 3 21 30 22 18 ishlg ( ( ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) ∧ 𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝑦 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐵 𝐶 ) ) ) → ( 𝑥 ( 𝐾𝐴 ) 𝐷 ↔ ( 𝑥𝐴𝐷𝐴 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) ∨ 𝐷 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ) )
39 27 28 37 38 mpbir3and ( ( ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) ∧ 𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝑦 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐵 𝐶 ) ) ) → 𝑥 ( 𝐾𝐴 ) 𝐷 )
40 39 23 jca ( ( ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) ∧ 𝑥𝑃 ) ∧ ( 𝐴 ∈ ( 𝑦 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐵 𝐶 ) ) ) → ( 𝑥 ( 𝐾𝐴 ) 𝐷 ∧ ( 𝐴 𝑥 ) = ( 𝐵 𝐶 ) ) )
41 40 ex ( ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) ∧ 𝑥𝑃 ) → ( ( 𝐴 ∈ ( 𝑦 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐵 𝐶 ) ) → ( 𝑥 ( 𝐾𝐴 ) 𝐷 ∧ ( 𝐴 𝑥 ) = ( 𝐵 𝐶 ) ) ) )
42 41 reximdva ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) → ( ∃ 𝑥𝑃 ( 𝐴 ∈ ( 𝑦 𝐼 𝑥 ) ∧ ( 𝐴 𝑥 ) = ( 𝐵 𝐶 ) ) → ∃ 𝑥𝑃 ( 𝑥 ( 𝐾𝐴 ) 𝐷 ∧ ( 𝐴 𝑥 ) = ( 𝐵 𝐶 ) ) ) )
43 17 42 mpd ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) → ∃ 𝑥𝑃 ( 𝑥 ( 𝐾𝐴 ) 𝐷 ∧ ( 𝐴 𝑥 ) = ( 𝐵 𝐶 ) ) )
44 1 fvexi 𝑃 ∈ V
45 44 a1i ( 𝜑𝑃 ∈ V )
46 45 5 6 11 nehash2 ( 𝜑 → 2 ≤ ( ♯ ‘ 𝑃 ) )
47 1 9 2 7 8 4 46 tgbtwndiff ( 𝜑 → ∃ 𝑦𝑃 ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) )
48 43 47 r19.29a ( 𝜑 → ∃ 𝑥𝑃 ( 𝑥 ( 𝐾𝐴 ) 𝐷 ∧ ( 𝐴 𝑥 ) = ( 𝐵 𝐶 ) ) )