Metamath Proof Explorer

Theorem metnrm

Description: A metric space is normal. (Contributed by Jeff Hankins, 31-Aug-2013) (Revised by Mario Carneiro, 5-Sep-2015) (Proof shortened by AV, 30-Sep-2020)

		Ref	Expression
	Hypothesis	metnrm.j	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
	Assertion	metnrm	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Nrm )

Proof

Step	Hyp	Ref	Expression
1		metnrm.j	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2	1	mopntop	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Top )
3		eqid	⊢ ( 𝑢 ∈ 𝑋 ↦ inf ( ran ( 𝑣 ∈ 𝑥 ↦ ( 𝑢 𝐷 𝑣 ) ) , ℝ^* , < ) ) = ( 𝑢 ∈ 𝑋 ↦ inf ( ran ( 𝑣 ∈ 𝑥 ↦ ( 𝑢 𝐷 𝑣 ) ) , ℝ^* , < ) )
4		simp1	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑦 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
5		simp2l	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑦 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → 𝑥 ∈ ( Clsd ‘ 𝐽 ) )
6		simp2r	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑦 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → 𝑦 ∈ ( Clsd ‘ 𝐽 ) )
7		simp3	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑦 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ( 𝑥 ∩ 𝑦 ) = ∅ )
8		eqid	⊢ ∪ 𝑠 ∈ 𝑦 ( 𝑠 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( ( 𝑢 ∈ 𝑋 ↦ inf ( ran ( 𝑣 ∈ 𝑥 ↦ ( 𝑢 𝐷 𝑣 ) ) , ℝ^* , < ) ) ‘ 𝑠 ) , 1 , ( ( 𝑢 ∈ 𝑋 ↦ inf ( ran ( 𝑣 ∈ 𝑥 ↦ ( 𝑢 𝐷 𝑣 ) ) , ℝ^* , < ) ) ‘ 𝑠 ) ) / 2 ) ) = ∪ 𝑠 ∈ 𝑦 ( 𝑠 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( ( 𝑢 ∈ 𝑋 ↦ inf ( ran ( 𝑣 ∈ 𝑥 ↦ ( 𝑢 𝐷 𝑣 ) ) , ℝ^* , < ) ) ‘ 𝑠 ) , 1 , ( ( 𝑢 ∈ 𝑋 ↦ inf ( ran ( 𝑣 ∈ 𝑥 ↦ ( 𝑢 𝐷 𝑣 ) ) , ℝ^* , < ) ) ‘ 𝑠 ) ) / 2 ) )
9		eqid	⊢ ( 𝑢 ∈ 𝑋 ↦ inf ( ran ( 𝑣 ∈ 𝑦 ↦ ( 𝑢 𝐷 𝑣 ) ) , ℝ^* , < ) ) = ( 𝑢 ∈ 𝑋 ↦ inf ( ran ( 𝑣 ∈ 𝑦 ↦ ( 𝑢 𝐷 𝑣 ) ) , ℝ^* , < ) )
10		eqid	⊢ ∪ 𝑡 ∈ 𝑥 ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( ( 𝑢 ∈ 𝑋 ↦ inf ( ran ( 𝑣 ∈ 𝑦 ↦ ( 𝑢 𝐷 𝑣 ) ) , ℝ^* , < ) ) ‘ 𝑡 ) , 1 , ( ( 𝑢 ∈ 𝑋 ↦ inf ( ran ( 𝑣 ∈ 𝑦 ↦ ( 𝑢 𝐷 𝑣 ) ) , ℝ^* , < ) ) ‘ 𝑡 ) ) / 2 ) ) = ∪ 𝑡 ∈ 𝑥 ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( ( 𝑢 ∈ 𝑋 ↦ inf ( ran ( 𝑣 ∈ 𝑦 ↦ ( 𝑢 𝐷 𝑣 ) ) , ℝ^* , < ) ) ‘ 𝑡 ) , 1 , ( ( 𝑢 ∈ 𝑋 ↦ inf ( ran ( 𝑣 ∈ 𝑦 ↦ ( 𝑢 𝐷 𝑣 ) ) , ℝ^* , < ) ) ‘ 𝑡 ) ) / 2 ) )
11	3 1 4 5 6 7 8 9 10	metnrmlem3	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑦 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ∃ 𝑧 ∈ 𝐽 ∃ 𝑤 ∈ 𝐽 ( 𝑥 ⊆ 𝑧 ∧ 𝑦 ⊆ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) )
12	11	3expia	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑦 ∈ ( Clsd ‘ 𝐽 ) ) ) → ( ( 𝑥 ∩ 𝑦 ) = ∅ → ∃ 𝑧 ∈ 𝐽 ∃ 𝑤 ∈ 𝐽 ( 𝑥 ⊆ 𝑧 ∧ 𝑦 ⊆ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) ) )
13	12	ralrimivva	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ∀ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑦 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑥 ∩ 𝑦 ) = ∅ → ∃ 𝑧 ∈ 𝐽 ∃ 𝑤 ∈ 𝐽 ( 𝑥 ⊆ 𝑧 ∧ 𝑦 ⊆ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) ) )
14		isnrm3	⊢ ( 𝐽 ∈ Nrm ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑦 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑥 ∩ 𝑦 ) = ∅ → ∃ 𝑧 ∈ 𝐽 ∃ 𝑤 ∈ 𝐽 ( 𝑥 ⊆ 𝑧 ∧ 𝑦 ⊆ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) ) ) )
15	2 13 14	sylanbrc	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Nrm )