Metamath Proof Explorer

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 ⊢ Y = R ↑ 𝑠 I
Assertion pwsms ⊢ R ∈ MetSp ∧ I ∈ Fin → Y ∈ MetSp

Proof

Step Hyp Ref Expression
1 pwsms.y ⊢ Y = R ↑ 𝑠 I
2 eqid ⊢ Scalar ⁡ R = Scalar ⁡ R
3 1 2 pwsval ⊢ R ∈ MetSp ∧ I ∈ Fin → Y = Scalar ⁡ R ⨉ 𝑠 I × R
4 fvexd ⊢ R ∈ MetSp ∧ I ∈ Fin → Scalar ⁡ R ∈ V
5 simpr ⊢ R ∈ MetSp ∧ I ∈ Fin → I ∈ Fin
6 fconst6g ⊢ R ∈ MetSp → I × R : I ⟶ MetSp
7 6 adantr ⊢ R ∈ MetSp ∧ I ∈ Fin → I × R : I ⟶ MetSp
8 eqid ⊢ Scalar ⁡ R ⨉ 𝑠 I × R = Scalar ⁡ R ⨉ 𝑠 I × R
9 8 prdsms ⊢ Scalar ⁡ R ∈ V ∧ I ∈ Fin ∧ I × R : I ⟶ MetSp → Scalar ⁡ R ⨉ 𝑠 I × R ∈ MetSp
10 4 5 7 9 syl3anc ⊢ R ∈ MetSp ∧ I ∈ Fin → Scalar ⁡ R ⨉ 𝑠 I × R ∈ MetSp
11 3 10 eqeltrd ⊢ R ∈ MetSp ∧ I ∈ Fin → Y ∈ MetSp