This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
Assertion pwsxms ( ( 𝑅 ∈ ∞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 prdsxms ⊢ ( ( ( 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 )