Metamath Proof Explorer

Theorem prdsms

Description: The indexed product structure is a metric space when the index set is finite. (Contributed by Mario Carneiro, 28-Aug-2015)

Ref Expression
Hypothesis prdsxms.y ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
Assertion prdsms ( ( 𝑆 ∈ 𝑊 ∧ 𝐼 ∈ Fin ∧ 𝑅 : 𝐼 ⟶ MetSp ) → 𝑌 ∈ MetSp )

Proof

Step Hyp Ref Expression
1 prdsxms.y ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
2 msxms ⊢ ( 𝑥 ∈ MetSp → 𝑥 ∈ ∞MetSp )
3 2 ssriv ⊢ MetSp ⊆ ∞MetSp
4 fss ⊢ ( ( 𝑅 : 𝐼 ⟶ MetSp ∧ MetSp ⊆ ∞MetSp ) → 𝑅 : 𝐼 ⟶ ∞MetSp )
5 3 4 mpan2 ⊢ ( 𝑅 : 𝐼 ⟶ MetSp → 𝑅 : 𝐼 ⟶ ∞MetSp )
6 1 prdsxms ⊢ ( ( 𝑆 ∈ 𝑊 ∧ 𝐼 ∈ Fin ∧ 𝑅 : 𝐼 ⟶ ∞MetSp ) → 𝑌 ∈ ∞MetSp )
7 5 6 syl3an3 ⊢ ( ( 𝑆 ∈ 𝑊 ∧ 𝐼 ∈ Fin ∧ 𝑅 : 𝐼 ⟶ MetSp ) → 𝑌 ∈ ∞MetSp )
8 simp1 ⊢ ( ( 𝑆 ∈ 𝑊 ∧ 𝐼 ∈ Fin ∧ 𝑅 : 𝐼 ⟶ MetSp ) → 𝑆 ∈ 𝑊 )
9 simp2 ⊢ ( ( 𝑆 ∈ 𝑊 ∧ 𝐼 ∈ Fin ∧ 𝑅 : 𝐼 ⟶ MetSp ) → 𝐼 ∈ Fin )
10 eqid ⊢ ( dist ‘ 𝑌 ) = ( dist ‘ 𝑌 )
11 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
12 simp3 ⊢ ( ( 𝑆 ∈ 𝑊 ∧ 𝐼 ∈ Fin ∧ 𝑅 : 𝐼 ⟶ MetSp ) → 𝑅 : 𝐼 ⟶ MetSp )
13 1 8 9 10 11 12 prdsmslem1 ⊢ ( ( 𝑆 ∈ 𝑊 ∧ 𝐼 ∈ Fin ∧ 𝑅 : 𝐼 ⟶ MetSp ) → ( dist ‘ 𝑌 ) ∈ ( Met ‘ ( Base ‘ 𝑌 ) ) )
14 ssid ⊢ ( Base ‘ 𝑌 ) ⊆ ( Base ‘ 𝑌 )
15 metres2 ⊢ ( ( ( dist ‘ 𝑌 ) ∈ ( Met ‘ ( Base ‘ 𝑌 ) ) ∧ ( Base ‘ 𝑌 ) ⊆ ( Base ‘ 𝑌 ) ) → ( ( dist ‘ 𝑌 ) ↾ ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) ) ∈ ( Met ‘ ( Base ‘ 𝑌 ) ) )
16 13 14 15 sylancl ⊢ ( ( 𝑆 ∈ 𝑊 ∧ 𝐼 ∈ Fin ∧ 𝑅 : 𝐼 ⟶ MetSp ) → ( ( dist ‘ 𝑌 ) ↾ ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) ) ∈ ( Met ‘ ( Base ‘ 𝑌 ) ) )
17 eqid ⊢ ( TopOpen ‘ 𝑌 ) = ( TopOpen ‘ 𝑌 )
18 eqid ⊢ ( ( dist ‘ 𝑌 ) ↾ ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) ) = ( ( dist ‘ 𝑌 ) ↾ ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) )
19 17 11 18 isms ⊢ ( 𝑌 ∈ MetSp ↔ ( 𝑌 ∈ ∞MetSp ∧ ( ( dist ‘ 𝑌 ) ↾ ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) ) ∈ ( Met ‘ ( Base ‘ 𝑌 ) ) ) )
20 7 16 19 sylanbrc ⊢ ( ( 𝑆 ∈ 𝑊 ∧ 𝐼 ∈ Fin ∧ 𝑅 : 𝐼 ⟶ MetSp ) → 𝑌 ∈ MetSp )