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 )