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