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	$⊢ P = {Base}_{G}$
	ishlg.i	$⊢ I = Itv (G)$
	ishlg.k	$⊢ K = {hl}_{𝒢} (G)$
	ishlg.a	$⊢ φ \to A \in P$
	ishlg.b	$⊢ φ \to B \in P$
	ishlg.c	$⊢ φ \to C \in P$
	hlln.1	$⊢ φ \to G \in 𝒢_{Tarski}$
	hltr.d	$⊢ φ \to D \in P$
	hlcgrex.m	$⊢ \underset{˙}{-} = dist (G)$
	hlcgrex.1	$⊢ φ \to D \neq A$
	hlcgrex.2	$⊢ φ \to B \neq C$
Assertion	hlcgrex	$⊢ φ \to \exists x \in P (x K (A) D \land A \underset{˙}{-} x = B \underset{˙}{-} C)$

Proof

Step	Hyp	Ref	Expression
1		ishlg.p	$⊢ P = {Base}_{G}$
2		ishlg.i	$⊢ I = Itv (G)$
3		ishlg.k	$⊢ K = {hl}_{𝒢} (G)$
4		ishlg.a	$⊢ φ \to A \in P$
5		ishlg.b	$⊢ φ \to B \in P$
6		ishlg.c	$⊢ φ \to C \in P$
7		hlln.1	$⊢ φ \to G \in 𝒢_{Tarski}$
8		hltr.d	$⊢ φ \to D \in P$
9		hlcgrex.m	$⊢ \underset{˙}{-} = dist (G)$
10		hlcgrex.1	$⊢ φ \to D \neq A$
11		hlcgrex.2	$⊢ φ \to B \neq C$
12	7	ad2antrr	$⊢ ((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \to G \in 𝒢_{Tarski}$
13		simplr	$⊢ ((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \to y \in P$
14	4	ad2antrr	$⊢ ((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \to A \in P$
15	5	ad2antrr	$⊢ ((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \to B \in P$
16	6	ad2antrr	$⊢ ((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \to C \in P$
17	1 9 2 12 13 14 15 16	axtgsegcon	$⊢ ((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \to \exists x \in P (A \in (y I x) \land A \underset{˙}{-} x = B \underset{˙}{-} C)$
18	12	ad2antrr	$⊢ ((((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \land x \in P) \land (A \in (y I x) \land A \underset{˙}{-} x = B \underset{˙}{-} C)) \to G \in 𝒢_{Tarski}$
19	15	ad2antrr	$⊢ ((((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \land x \in P) \land (A \in (y I x) \land A \underset{˙}{-} x = B \underset{˙}{-} C)) \to B \in P$
20	16	ad2antrr	$⊢ ((((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \land x \in P) \land (A \in (y I x) \land A \underset{˙}{-} x = B \underset{˙}{-} C)) \to C \in P$
21		simplr	$⊢ ((((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \land x \in P) \land (A \in (y I x) \land A \underset{˙}{-} x = B \underset{˙}{-} C)) \to x \in P$
22	14	ad2antrr	$⊢ ((((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \land x \in P) \land (A \in (y I x) \land A \underset{˙}{-} x = B \underset{˙}{-} C)) \to A \in P$
23		simprr	$⊢ ((((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \land x \in P) \land (A \in (y I x) \land A \underset{˙}{-} x = B \underset{˙}{-} C)) \to A \underset{˙}{-} x = B \underset{˙}{-} C$
24	1 9 2 18 22 21 19 20 23	tgcgrcoml	$⊢ ((((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \land x \in P) \land (A \in (y I x) \land A \underset{˙}{-} x = B \underset{˙}{-} C)) \to x \underset{˙}{-} A = B \underset{˙}{-} C$
25	24	eqcomd	$⊢ ((((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \land x \in P) \land (A \in (y I x) \land A \underset{˙}{-} x = B \underset{˙}{-} C)) \to B \underset{˙}{-} C = x \underset{˙}{-} A$
26	11	ad4antr	$⊢ ((((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \land x \in P) \land (A \in (y I x) \land A \underset{˙}{-} x = B \underset{˙}{-} C)) \to B \neq C$
27	1 9 2 18 19 20 21 22 25 26	tgcgrneq	$⊢ ((((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \land x \in P) \land (A \in (y I x) \land A \underset{˙}{-} x = B \underset{˙}{-} C)) \to x \neq A$
28	10	ad4antr	$⊢ ((((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \land x \in P) \land (A \in (y I x) \land A \underset{˙}{-} x = B \underset{˙}{-} C)) \to D \neq A$
29	13	ad2antrr	$⊢ ((((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \land x \in P) \land (A \in (y I x) \land A \underset{˙}{-} x = B \underset{˙}{-} C)) \to y \in P$
30	8	ad4antr	$⊢ ((((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \land x \in P) \land (A \in (y I x) \land A \underset{˙}{-} x = B \underset{˙}{-} C)) \to D \in P$
31		simpllr	$⊢ ((((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \land x \in P) \land (A \in (y I x) \land A \underset{˙}{-} x = B \underset{˙}{-} C)) \to (A \in (D I y) \land A \neq y)$
32	31	simprd	$⊢ ((((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \land x \in P) \land (A \in (y I x) \land A \underset{˙}{-} x = B \underset{˙}{-} C)) \to A \neq y$
33	32	necomd	$⊢ ((((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \land x \in P) \land (A \in (y I x) \land A \underset{˙}{-} x = B \underset{˙}{-} C)) \to y \neq A$
34		simprl	$⊢ ((((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \land x \in P) \land (A \in (y I x) \land A \underset{˙}{-} x = B \underset{˙}{-} C)) \to A \in (y I x)$
35	31	simpld	$⊢ ((((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \land x \in P) \land (A \in (y I x) \land A \underset{˙}{-} x = B \underset{˙}{-} C)) \to A \in (D I y)$
36	1 9 2 18 30 22 29 35	tgbtwncom	$⊢ ((((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \land x \in P) \land (A \in (y I x) \land A \underset{˙}{-} x = B \underset{˙}{-} C)) \to A \in (y I D)$
37	1 2 18 29 22 21 30 33 34 36	tgbtwnconn2	$⊢ ((((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \land x \in P) \land (A \in (y I x) \land A \underset{˙}{-} x = B \underset{˙}{-} C)) \to (x \in (A I D) \lor D \in (A I x))$
38	1 2 3 21 30 22 18	ishlg	$⊢ ((((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \land x \in P) \land (A \in (y I x) \land A \underset{˙}{-} x = B \underset{˙}{-} C)) \to (x K (A) D \leftrightarrow (x \neq A \land D \neq A \land (x \in (A I D) \lor D \in (A I x))))$
39	27 28 37 38	mpbir3and	$⊢ ((((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \land x \in P) \land (A \in (y I x) \land A \underset{˙}{-} x = B \underset{˙}{-} C)) \to x K (A) D$
40	39 23	jca	$⊢ ((((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \land x \in P) \land (A \in (y I x) \land A \underset{˙}{-} x = B \underset{˙}{-} C)) \to (x K (A) D \land A \underset{˙}{-} x = B \underset{˙}{-} C)$
41	40	ex	$⊢ (((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \land x \in P) \to ((A \in (y I x) \land A \underset{˙}{-} x = B \underset{˙}{-} C) \to (x K (A) D \land A \underset{˙}{-} x = B \underset{˙}{-} C))$
42	41	reximdva	$⊢ ((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \to (\exists x \in P (A \in (y I x) \land A \underset{˙}{-} x = B \underset{˙}{-} C) \to \exists x \in P (x K (A) D \land A \underset{˙}{-} x = B \underset{˙}{-} C))$
43	17 42	mpd	$⊢ ((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \to \exists x \in P (x K (A) D \land A \underset{˙}{-} x = B \underset{˙}{-} C)$
44	1	fvexi	$⊢ P \in V$
45	44	a1i	$⊢ φ \to P \in V$
46	45 5 6 11	nehash2	$⊢ φ \to 2 \leq \|P\|$
47	1 9 2 7 8 4 46	tgbtwndiff	$⊢ φ \to \exists y \in P (A \in (D I y) \land A \neq y)$
48	43 47	r19.29a	$⊢ φ \to \exists x \in P (x K (A) D \land A \underset{˙}{-} x = B \underset{˙}{-} C)$

Metamath Proof Explorer

Theorem hlcgrex

Proof