pwsxms

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

		Ref	Expression
	Hypothesis	pwsms.y	$⊢ Y = R ↑_{𝑠} I$
	Assertion	pwsxms	$⊢ (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	prdsxms	$⊢ (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