hlcgreulem

	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$
	hlcgreulem.x	$⊢ φ \to X \in P$
	hlcgreulem.y	$⊢ φ \to Y \in P$
	hlcgreulem.1	$⊢ φ \to X K (A) D$
	hlcgreulem.2	$⊢ φ \to Y K (A) D$
	hlcgreulem.3	$⊢ φ \to A \underset{˙}{-} X = B \underset{˙}{-} C$
	hlcgreulem.4	$⊢ φ \to A \underset{˙}{-} Y = B \underset{˙}{-} C$
Assertion	hlcgreulem	$⊢ φ \to X = Y$

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		hlcgreulem.x	$⊢ φ \to X \in P$
13		hlcgreulem.y	$⊢ φ \to Y \in P$
14		hlcgreulem.1	$⊢ φ \to X K (A) D$
15		hlcgreulem.2	$⊢ φ \to Y K (A) D$
16		hlcgreulem.3	$⊢ φ \to A \underset{˙}{-} X = B \underset{˙}{-} C$
17		hlcgreulem.4	$⊢ φ \to A \underset{˙}{-} Y = B \underset{˙}{-} C$
18	7	ad2antrr	$⊢ ((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \to G \in 𝒢_{Tarski}$
19	4	ad2antrr	$⊢ ((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \to A \in P$
20	5	ad2antrr	$⊢ ((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \to B \in P$
21	6	ad2antrr	$⊢ ((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \to C \in P$
22		simplr	$⊢ ((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \to y \in P$
23	12	ad2antrr	$⊢ ((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \to X \in P$
24	13	ad2antrr	$⊢ ((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \to Y \in P$
25		simprr	$⊢ ((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \to A \neq y$
26	25	necomd	$⊢ ((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \to y \neq A$
27	8	ad2antrr	$⊢ ((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \to D \in P$
28	1 2 3 12 8 4 7 14	hlcomd	$⊢ φ \to D K (A) X$
29	28	ad2antrr	$⊢ ((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \to D K (A) X$
30		simprl	$⊢ ((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \to A \in (D I y)$
31	1 2 3 27 23 22 18 19 29 30	btwnhl	$⊢ ((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \to A \in (X I y)$
32	1 9 2 18 23 19 22 31	tgbtwncom	$⊢ ((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \to A \in (y I X)$
33	1 2 3 13 8 4 7 15	hlcomd	$⊢ φ \to D K (A) Y$
34	33	ad2antrr	$⊢ ((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \to D K (A) Y$
35	1 2 3 27 24 22 18 19 34 30	btwnhl	$⊢ ((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \to A \in (Y I y)$
36	1 9 2 18 24 19 22 35	tgbtwncom	$⊢ ((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \to A \in (y I Y)$
37	16	ad2antrr	$⊢ ((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \to A \underset{˙}{-} X = B \underset{˙}{-} C$
38	17	ad2antrr	$⊢ ((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \to A \underset{˙}{-} Y = B \underset{˙}{-} C$
39	1 9 2 18 19 20 21 22 23 24 26 32 36 37 38	tgsegconeq	$⊢ ((φ \land y \in P) \land (A \in (D I y) \land A \neq y)) \to X = Y$
40	1	fvexi	$⊢ P \in V$
41	40	a1i	$⊢ φ \to P \in V$
42	41 5 6 11	nehash2	$⊢ φ \to 2 \leq \|P\|$
43	1 9 2 7 8 4 42	tgbtwndiff	$⊢ φ \to \exists y \in P (A \in (D I y) \land A \neq y)$
44	39 43	r19.29a	$⊢ φ \to X = Y$

Metamath Proof Explorer

Theorem hlcgreulem

Proof