Theorem pwsms

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

	Ref	Expression
Hypothesis	pwsms.y	⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
Assertion	pwsms	⊢ ( ( 𝑅 ∈ MetSp ∧ 𝐼 ∈ Fin ) → 𝑌 ∈ MetSp )

Proof

Step	Hyp	Ref	Expression
1		pwsms.y	⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
2		eqid	⊢ ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑅 )
3	1 2	pwsval	⊢ ( ( 𝑅 ∈ MetSp ∧ 𝐼 ∈ Fin ) → 𝑌 = ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) )
4		fvexd	⊢ ( ( 𝑅 ∈ MetSp ∧ 𝐼 ∈ Fin ) → ( Scalar ‘ 𝑅 ) ∈ V )
5		simpr	⊢ ( ( 𝑅 ∈ MetSp ∧ 𝐼 ∈ Fin ) → 𝐼 ∈ Fin )
6		fconst6g	⊢ ( 𝑅 ∈ MetSp → ( 𝐼 × { 𝑅 } ) : 𝐼 ⟶ MetSp )
7	6	adantr	⊢ ( ( 𝑅 ∈ MetSp ∧ 𝐼 ∈ Fin ) → ( 𝐼 × { 𝑅 } ) : 𝐼 ⟶ MetSp )
8		eqid	⊢ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) = ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) )
9	8	prdsms	⊢ ( ( ( Scalar ‘ 𝑅 ) ∈ V ∧ 𝐼 ∈ Fin ∧ ( 𝐼 × { 𝑅 } ) : 𝐼 ⟶ MetSp ) → ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ∈ MetSp )
10	4 5 7 9	syl3anc	⊢ ( ( 𝑅 ∈ MetSp ∧ 𝐼 ∈ Fin ) → ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ∈ MetSp )
11	3 10	eqeltrd	⊢ ( ( 𝑅 ∈ MetSp ∧ 𝐼 ∈ Fin ) → 𝑌 ∈ MetSp )