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	$⊢ 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	hlcgreu	$⊢ φ \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	1 2 3 4 5 6 7 8 9 10 11	hlcgrex	$⊢ φ \to \exists x \in P (x K (A) D \land A \underset{˙}{-} x = B \underset{˙}{-} C)$
13	4	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (A) D \land A \underset{˙}{-} x = B \underset{˙}{-} C) \land (y K (A) D \land A \underset{˙}{-} y = B \underset{˙}{-} C))) \to A \in P$
14	5	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (A) D \land A \underset{˙}{-} x = B \underset{˙}{-} C) \land (y K (A) D \land A \underset{˙}{-} y = B \underset{˙}{-} C))) \to B \in P$
15	6	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (A) D \land A \underset{˙}{-} x = B \underset{˙}{-} C) \land (y K (A) D \land A \underset{˙}{-} y = B \underset{˙}{-} C))) \to C \in P$
16	7	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (A) D \land A \underset{˙}{-} x = B \underset{˙}{-} C) \land (y K (A) D \land A \underset{˙}{-} y = B \underset{˙}{-} C))) \to G \in 𝒢_{Tarski}$
17	8	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (A) D \land A \underset{˙}{-} x = B \underset{˙}{-} C) \land (y K (A) D \land A \underset{˙}{-} y = B \underset{˙}{-} C))) \to D \in P$
18	10	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (A) D \land A \underset{˙}{-} x = B \underset{˙}{-} C) \land (y K (A) D \land A \underset{˙}{-} y = B \underset{˙}{-} C))) \to D \neq A$
19	11	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (A) D \land A \underset{˙}{-} x = B \underset{˙}{-} C) \land (y K (A) D \land A \underset{˙}{-} y = B \underset{˙}{-} C))) \to B \neq C$
20		simpllr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (A) D \land A \underset{˙}{-} x = B \underset{˙}{-} C) \land (y K (A) D \land A \underset{˙}{-} y = B \underset{˙}{-} C))) \to x \in P$
21		simplr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (A) D \land A \underset{˙}{-} x = B \underset{˙}{-} C) \land (y K (A) D \land A \underset{˙}{-} y = B \underset{˙}{-} C))) \to y \in P$
22		simprll	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (A) D \land A \underset{˙}{-} x = B \underset{˙}{-} C) \land (y K (A) D \land A \underset{˙}{-} y = B \underset{˙}{-} C))) \to x K (A) D$
23		simprrl	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (A) D \land A \underset{˙}{-} x = B \underset{˙}{-} C) \land (y K (A) D \land A \underset{˙}{-} y = B \underset{˙}{-} C))) \to y K (A) D$
24		simprlr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (A) D \land A \underset{˙}{-} x = B \underset{˙}{-} C) \land (y K (A) D \land A \underset{˙}{-} y = B \underset{˙}{-} C))) \to A \underset{˙}{-} x = B \underset{˙}{-} C$
25		simprrr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (A) D \land A \underset{˙}{-} x = B \underset{˙}{-} C) \land (y K (A) D \land A \underset{˙}{-} y = B \underset{˙}{-} C))) \to A \underset{˙}{-} y = B \underset{˙}{-} C$
26	1 2 3 13 14 15 16 17 9 18 19 20 21 22 23 24 25	hlcgreulem	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (A) D \land A \underset{˙}{-} x = B \underset{˙}{-} C) \land (y K (A) D \land A \underset{˙}{-} y = B \underset{˙}{-} C))) \to x = y$
27	26	ex	$⊢ ((φ \land x \in P) \land y \in P) \to (((x K (A) D \land A \underset{˙}{-} x = B \underset{˙}{-} C) \land (y K (A) D \land A \underset{˙}{-} y = B \underset{˙}{-} C)) \to x = y)$
28	27	ralrimiva	$⊢ (φ \land x \in P) \to \forall y \in P (((x K (A) D \land A \underset{˙}{-} x = B \underset{˙}{-} C) \land (y K (A) D \land A \underset{˙}{-} y = B \underset{˙}{-} C)) \to x = y)$
29	28	ralrimiva	$⊢ φ \to \forall x \in P \forall y \in P (((x K (A) D \land A \underset{˙}{-} x = B \underset{˙}{-} C) \land (y K (A) D \land A \underset{˙}{-} y = B \underset{˙}{-} C)) \to x = y)$
30		breq1	$⊢ x = y \to (x K (A) D \leftrightarrow y K (A) D)$
31		oveq2	$⊢ x = y \to A \underset{˙}{-} x = A \underset{˙}{-} y$
32	31	eqeq1d	$⊢ x = y \to (A \underset{˙}{-} x = B \underset{˙}{-} C \leftrightarrow A \underset{˙}{-} y = B \underset{˙}{-} C)$
33	30 32	anbi12d	$⊢ x = y \to ((x K (A) D \land A \underset{˙}{-} x = B \underset{˙}{-} C) \leftrightarrow (y K (A) D \land A \underset{˙}{-} y = B \underset{˙}{-} C))$
34	33	reu4	$⊢ \exists! x \in P (x K (A) D \land A \underset{˙}{-} x = B \underset{˙}{-} C) \leftrightarrow (\exists x \in P (x K (A) D \land A \underset{˙}{-} x = B \underset{˙}{-} C) \land \forall x \in P \forall y \in P (((x K (A) D \land A \underset{˙}{-} x = B \underset{˙}{-} C) \land (y K (A) D \land A \underset{˙}{-} y = B \underset{˙}{-} C)) \to x = y))$
35	12 29 34	sylanbrc	$⊢ φ \to \exists! x \in P (x K (A) D \land A \underset{˙}{-} x = B \underset{˙}{-} C)$

Metamath Proof Explorer

Theorem hlcgreu

Proof