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	$⊢ Y = S ⨉_{𝑠} R$
	Assertion	prdsms	$⊢ (S \in W \land I \in Fin \land R : I ⟶ MetSp) \to Y \in MetSp$

Proof

Step	Hyp	Ref	Expression
1		prdsxms.y	$⊢ Y = S ⨉_{𝑠} R$
2		msxms	$⊢ x \in MetSp \to x \in ∞MetSp$
3	2	ssriv	$⊢ MetSp \subseteq ∞MetSp$
4		fss	$⊢ (R : I ⟶ MetSp \land MetSp \subseteq ∞MetSp) \to R : I ⟶ ∞MetSp$
5	3 4	mpan2	$⊢ R : I ⟶ MetSp \to R : I ⟶ ∞MetSp$
6	1	prdsxms	$⊢ (S \in W \land I \in Fin \land R : I ⟶ ∞MetSp) \to Y \in ∞MetSp$
7	5 6	syl3an3	$⊢ (S \in W \land I \in Fin \land R : I ⟶ MetSp) \to Y \in ∞MetSp$
8		simp1	$⊢ (S \in W \land I \in Fin \land R : I ⟶ MetSp) \to S \in W$
9		simp2	$⊢ (S \in W \land I \in Fin \land R : I ⟶ MetSp) \to I \in Fin$
10		eqid	$⊢ dist (Y) = dist (Y)$
11		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
12		simp3	$⊢ (S \in W \land I \in Fin \land R : I ⟶ MetSp) \to R : I ⟶ MetSp$
13	1 8 9 10 11 12	prdsmslem1	$⊢ (S \in W \land I \in Fin \land R : I ⟶ MetSp) \to dist (Y) \in Met ({Base}_{Y})$
14		ssid	$⊢ {Base}_{Y} \subseteq {Base}_{Y}$
15		metres2	$⊢ (dist (Y) \in Met ({Base}_{Y}) \land {Base}_{Y} \subseteq {Base}_{Y}) \to {dist (Y) ↾}_{({Base}_{Y} \times {Base}_{Y})} \in Met ({Base}_{Y})$
16	13 14 15	sylancl	$⊢ (S \in W \land I \in Fin \land R : I ⟶ MetSp) \to {dist (Y) ↾}_{({Base}_{Y} \times {Base}_{Y})} \in Met ({Base}_{Y})$
17		eqid	$⊢ TopOpen (Y) = TopOpen (Y)$
18		eqid	$⊢ {dist (Y) ↾}_{({Base}_{Y} \times {Base}_{Y})} = {dist (Y) ↾}_{({Base}_{Y} \times {Base}_{Y})}$
19	17 11 18	isms	$⊢ Y \in MetSp \leftrightarrow (Y \in ∞MetSp \land {dist (Y) ↾}_{({Base}_{Y} \times {Base}_{Y})} \in Met ({Base}_{Y}))$
20	7 16 19	sylanbrc	$⊢ (S \in W \land I \in Fin \land R : I ⟶ MetSp) \to Y \in MetSp$

Metamath Proof Explorer

Theorem prdsms

Proof