Metamath Proof Explorer

Theorem 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 ∈ ∞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 prdsxms ⊢ 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