Metamath Proof Explorer


Theorem prdsxms

Description: The indexed product structure is an extended metric space when the index set is finite. (Although the extended metric is still valid when the index set is infinite, it no longer agrees with the product topology, which is not metrizable in any case.) (Contributed by Mario Carneiro, 28-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 prdsxms.y 𝑌 = ( 𝑆 Xs 𝑅 )
2 simp1 ( ( 𝑆𝑊𝐼 ∈ Fin ∧ 𝑅 : 𝐼 ⟶ ∞MetSp ) → 𝑆𝑊 )
3 simp2 ( ( 𝑆𝑊𝐼 ∈ Fin ∧ 𝑅 : 𝐼 ⟶ ∞MetSp ) → 𝐼 ∈ Fin )
4 eqid ( dist ‘ 𝑌 ) = ( dist ‘ 𝑌 )
5 eqid ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
6 simp3 ( ( 𝑆𝑊𝐼 ∈ Fin ∧ 𝑅 : 𝐼 ⟶ ∞MetSp ) → 𝑅 : 𝐼 ⟶ ∞MetSp )
7 1 2 3 4 5 6 prdsxmslem1 ( ( 𝑆𝑊𝐼 ∈ Fin ∧ 𝑅 : 𝐼 ⟶ ∞MetSp ) → ( dist ‘ 𝑌 ) ∈ ( ∞Met ‘ ( Base ‘ 𝑌 ) ) )
8 ssid ( Base ‘ 𝑌 ) ⊆ ( Base ‘ 𝑌 )
9 xmetres2 ( ( ( dist ‘ 𝑌 ) ∈ ( ∞Met ‘ ( Base ‘ 𝑌 ) ) ∧ ( Base ‘ 𝑌 ) ⊆ ( Base ‘ 𝑌 ) ) → ( ( dist ‘ 𝑌 ) ↾ ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝑌 ) ) )
10 7 8 9 sylancl ( ( 𝑆𝑊𝐼 ∈ Fin ∧ 𝑅 : 𝐼 ⟶ ∞MetSp ) → ( ( dist ‘ 𝑌 ) ↾ ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝑌 ) ) )
11 eqid ( TopOpen ‘ 𝑌 ) = ( TopOpen ‘ 𝑌 )
12 eqid ( Base ‘ ( 𝑅𝑘 ) ) = ( Base ‘ ( 𝑅𝑘 ) )
13 eqid ( ( dist ‘ ( 𝑅𝑘 ) ) ↾ ( ( Base ‘ ( 𝑅𝑘 ) ) × ( Base ‘ ( 𝑅𝑘 ) ) ) ) = ( ( dist ‘ ( 𝑅𝑘 ) ) ↾ ( ( Base ‘ ( 𝑅𝑘 ) ) × ( Base ‘ ( 𝑅𝑘 ) ) ) )
14 eqid ( TopOpen ‘ ( 𝑅𝑘 ) ) = ( TopOpen ‘ ( 𝑅𝑘 ) )
15 eqid { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘𝐼 ( 𝑔𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼𝑧 ) ( 𝑔𝑘 ) = ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ 𝑥 = X 𝑘𝐼 ( 𝑔𝑘 ) ) } = { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘𝐼 ( 𝑔𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼𝑧 ) ( 𝑔𝑘 ) = ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ 𝑥 = X 𝑘𝐼 ( 𝑔𝑘 ) ) }
16 1 2 3 4 5 6 11 12 13 14 15 prdsxmslem2 ( ( 𝑆𝑊𝐼 ∈ Fin ∧ 𝑅 : 𝐼 ⟶ ∞MetSp ) → ( TopOpen ‘ 𝑌 ) = ( MetOpen ‘ ( dist ‘ 𝑌 ) ) )
17 xmetf ( ( dist ‘ 𝑌 ) ∈ ( ∞Met ‘ ( Base ‘ 𝑌 ) ) → ( dist ‘ 𝑌 ) : ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) ⟶ ℝ* )
18 ffn ( ( dist ‘ 𝑌 ) : ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) ⟶ ℝ* → ( dist ‘ 𝑌 ) Fn ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) )
19 fnresdm ( ( dist ‘ 𝑌 ) Fn ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) → ( ( dist ‘ 𝑌 ) ↾ ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) ) = ( dist ‘ 𝑌 ) )
20 7 17 18 19 4syl ( ( 𝑆𝑊𝐼 ∈ Fin ∧ 𝑅 : 𝐼 ⟶ ∞MetSp ) → ( ( dist ‘ 𝑌 ) ↾ ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) ) = ( dist ‘ 𝑌 ) )
21 20 fveq2d ( ( 𝑆𝑊𝐼 ∈ Fin ∧ 𝑅 : 𝐼 ⟶ ∞MetSp ) → ( MetOpen ‘ ( ( dist ‘ 𝑌 ) ↾ ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) ) ) = ( MetOpen ‘ ( dist ‘ 𝑌 ) ) )
22 16 21 eqtr4d ( ( 𝑆𝑊𝐼 ∈ Fin ∧ 𝑅 : 𝐼 ⟶ ∞MetSp ) → ( TopOpen ‘ 𝑌 ) = ( MetOpen ‘ ( ( dist ‘ 𝑌 ) ↾ ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) ) ) )
23 eqid ( ( dist ‘ 𝑌 ) ↾ ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) ) = ( ( dist ‘ 𝑌 ) ↾ ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) )
24 11 5 23 isxms2 ( 𝑌 ∈ ∞MetSp ↔ ( ( ( dist ‘ 𝑌 ) ↾ ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝑌 ) ) ∧ ( TopOpen ‘ 𝑌 ) = ( MetOpen ‘ ( ( dist ‘ 𝑌 ) ↾ ( ( Base ‘ 𝑌 ) × ( Base ‘ 𝑌 ) ) ) ) ) )
25 10 22 24 sylanbrc ( ( 𝑆𝑊𝐼 ∈ Fin ∧ 𝑅 : 𝐼 ⟶ ∞MetSp ) → 𝑌 ∈ ∞MetSp )