blpnfctr

Description: The infinity ball in an extended metric acts like an ultrametric ball in that every point in the ball is also its center. (Contributed by Mario Carneiro, 21-Aug-2015)

		Ref	Expression
	Assertion	blpnfctr	$⊢ (D \in ∞Met (X) \land P \in X \land A \in (P ball (D) +∞)) \to P ball (D) +∞ = A ball (D) +∞$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ D^{-1} [ℝ] = D^{-1} [ℝ]$
2	1	xmeter	$⊢ D \in ∞Met (X) \to D^{-1} [ℝ] Er X$
3	2	3ad2ant1	$⊢ (D \in ∞Met (X) \land P \in X \land A \in (P ball (D) +∞)) \to D^{-1} [ℝ] Er X$
4		simp3	$⊢ (D \in ∞Met (X) \land P \in X \land A \in (P ball (D) +∞)) \to A \in (P ball (D) +∞)$
5	1	xmetec	$⊢ (D \in ∞Met (X) \land P \in X) \to [P] D^{-1} [ℝ] = P ball (D) +∞$
6	5	3adant3	$⊢ (D \in ∞Met (X) \land P \in X \land A \in (P ball (D) +∞)) \to [P] D^{-1} [ℝ] = P ball (D) +∞$
7	4 6	eleqtrrd	$⊢ (D \in ∞Met (X) \land P \in X \land A \in (P ball (D) +∞)) \to A \in [P] D^{-1} [ℝ]$
8		elecg	$⊢ (A \in (P ball (D) +∞) \land P \in X) \to (A \in [P] D^{-1} [ℝ] \leftrightarrow P D^{-1} [ℝ] A)$
9	8	ancoms	$⊢ (P \in X \land A \in (P ball (D) +∞)) \to (A \in [P] D^{-1} [ℝ] \leftrightarrow P D^{-1} [ℝ] A)$
10	9	3adant1	$⊢ (D \in ∞Met (X) \land P \in X \land A \in (P ball (D) +∞)) \to (A \in [P] D^{-1} [ℝ] \leftrightarrow P D^{-1} [ℝ] A)$
11	7 10	mpbid	$⊢ (D \in ∞Met (X) \land P \in X \land A \in (P ball (D) +∞)) \to P D^{-1} [ℝ] A$
12	3 11	erthi	$⊢ (D \in ∞Met (X) \land P \in X \land A \in (P ball (D) +∞)) \to [P] D^{-1} [ℝ] = [A] D^{-1} [ℝ]$
13		pnfxr	$⊢ +∞ \in ℝ^{*}$
14		blssm	$⊢ (D \in ∞Met (X) \land P \in X \land +∞ \in ℝ^{*}) \to P ball (D) +∞ \subseteq X$
15	13 14	mp3an3	$⊢ (D \in ∞Met (X) \land P \in X) \to P ball (D) +∞ \subseteq X$
16	15	sselda	$⊢ ((D \in ∞Met (X) \land P \in X) \land A \in (P ball (D) +∞)) \to A \in X$
17	1	xmetec	$⊢ (D \in ∞Met (X) \land A \in X) \to [A] D^{-1} [ℝ] = A ball (D) +∞$
18	17	adantlr	$⊢ ((D \in ∞Met (X) \land P \in X) \land A \in X) \to [A] D^{-1} [ℝ] = A ball (D) +∞$
19	16 18	syldan	$⊢ ((D \in ∞Met (X) \land P \in X) \land A \in (P ball (D) +∞)) \to [A] D^{-1} [ℝ] = A ball (D) +∞$
20	19	3impa	$⊢ (D \in ∞Met (X) \land P \in X \land A \in (P ball (D) +∞)) \to [A] D^{-1} [ℝ] = A ball (D) +∞$
21	12 6 20	3eqtr3d	$⊢ (D \in ∞Met (X) \land P \in X \land A \in (P ball (D) +∞)) \to P ball (D) +∞ = A ball (D) +∞$

Metamath Proof Explorer

Theorem blpnfctr

Proof