pwsms

Description: A power of a metric space is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015)

		Ref	Expression
	Hypothesis	pwsms.y	$⊢ Y = R ↑_{𝑠} I$
	Assertion	pwsms	$⊢ (R \in MetSp \land I \in Fin) \to Y \in MetSp$

Step	Hyp	Ref	Expression
1		pwsms.y	$⊢ Y = R ↑_{𝑠} I$
2		eqid	$⊢ Scalar (R) = Scalar (R)$
3	1 2	pwsval	$⊢ (R \in MetSp \land I \in Fin) \to Y = Scalar (R) ⨉_{𝑠} (I \times \{R\})$
4		fvexd	$⊢ (R \in MetSp \land I \in Fin) \to Scalar (R) \in V$
5		simpr	$⊢ (R \in MetSp \land I \in Fin) \to I \in Fin$
6		fconst6g	$⊢ R \in MetSp \to (I \times \{R\}) : I ⟶ MetSp$
7	6	adantr	$⊢ (R \in MetSp \land I \in Fin) \to (I \times \{R\}) : I ⟶ MetSp$
8		eqid	$⊢ Scalar (R) ⨉_{𝑠} (I \times \{R\}) = Scalar (R) ⨉_{𝑠} (I \times \{R\})$
9	8	prdsms	$⊢ (Scalar (R) \in V \land I \in Fin \land (I \times \{R\}) : I ⟶ MetSp) \to Scalar (R) ⨉_{𝑠} (I \times \{R\}) \in MetSp$
10	4 5 7 9	syl3anc	$⊢ (R \in MetSp \land I \in Fin) \to Scalar (R) ⨉_{𝑠} (I \times \{R\}) \in MetSp$
11	3 10	eqeltrd	$⊢ (R \in MetSp \land I \in Fin) \to Y \in MetSp$

Metamath Proof Explorer