Metamath Proof Explorer

Theorem repwsmet

Description: The supremum metric on RR ^ I is a metric. (Contributed by Jeff Madsen, 15-Sep-2015)

Ref Expression
Hypotheses rrnequiv.y ⊢ 𝑌 = ( ( ℂfld ↾s ℝ ) ↑s 𝐼 )
rrnequiv.d ⊢ 𝐷 = ( dist ‘ 𝑌 )
rrnequiv.1 ⊢ 𝑋 = ( ℝ ↑m 𝐼 )
Assertion repwsmet ( 𝐼 ∈ Fin → 𝐷 ∈ ( Met ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 rrnequiv.y ⊢ 𝑌 = ( ( ℂfld ↾s ℝ ) ↑s 𝐼 )
2 rrnequiv.d ⊢ 𝐷 = ( dist ‘ 𝑌 )
3 rrnequiv.1 ⊢ 𝑋 = ( ℝ ↑m 𝐼 )
4 fconstmpt ⊢ ( 𝐼 × { ( ℂfld ↾s ℝ ) } ) = ( 𝑘 ∈ 𝐼 ↦ ( ℂfld ↾s ℝ ) )
5 4 oveq2i ⊢ ( ( Scalar ‘ ℂfld ) Xs ( 𝐼 × { ( ℂfld ↾s ℝ ) } ) ) = ( ( Scalar ‘ ℂfld ) Xs ( 𝑘 ∈ 𝐼 ↦ ( ℂfld ↾s ℝ ) ) )
6 eqid ⊢ ( Base ‘ ( ( Scalar ‘ ℂfld ) Xs ( 𝐼 × { ( ℂfld ↾s ℝ ) } ) ) ) = ( Base ‘ ( ( Scalar ‘ ℂfld ) Xs ( 𝐼 × { ( ℂfld ↾s ℝ ) } ) ) )
7 ax-resscn ⊢ ℝ ⊆ ℂ
8 eqid ⊢ ( ℂfld ↾s ℝ ) = ( ℂfld ↾s ℝ )
9 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
10 8 9 ressbas2 ⊢ ( ℝ ⊆ ℂ → ℝ = ( Base ‘ ( ℂfld ↾s ℝ ) ) )
11 7 10 ax-mp ⊢ ℝ = ( Base ‘ ( ℂfld ↾s ℝ ) )
12 reex ⊢ ℝ ∈ V
13 cnfldds ⊢ ( abs ∘ − ) = ( dist ‘ ℂfld )
14 8 13 ressds ⊢ ( ℝ ∈ V → ( abs ∘ − ) = ( dist ‘ ( ℂfld ↾s ℝ ) ) )
15 12 14 ax-mp ⊢ ( abs ∘ − ) = ( dist ‘ ( ℂfld ↾s ℝ ) )
16 15 reseq1i ⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) = ( ( dist ‘ ( ℂfld ↾s ℝ ) ) ↾ ( ℝ × ℝ ) )
17 eqid ⊢ ( dist ‘ ( ( Scalar ‘ ℂfld ) Xs ( 𝐼 × { ( ℂfld ↾s ℝ ) } ) ) ) = ( dist ‘ ( ( Scalar ‘ ℂfld ) Xs ( 𝐼 × { ( ℂfld ↾s ℝ ) } ) ) )
18 fvexd ⊢ ( 𝐼 ∈ Fin → ( Scalar ‘ ℂfld ) ∈ V )
19 id ⊢ ( 𝐼 ∈ Fin → 𝐼 ∈ Fin )
20 ovex ⊢ ( ℂfld ↾s ℝ ) ∈ V
21 20 a1i ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑘 ∈ 𝐼 ) → ( ℂfld ↾s ℝ ) ∈ V )
22 eqid ⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
23 22 remet ⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( Met ‘ ℝ )
24 23 a1i ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑘 ∈ 𝐼 ) → ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( Met ‘ ℝ ) )
25 5 6 11 16 17 18 19 21 24 prdsmet ⊢ ( 𝐼 ∈ Fin → ( dist ‘ ( ( Scalar ‘ ℂfld ) Xs ( 𝐼 × { ( ℂfld ↾s ℝ ) } ) ) ) ∈ ( Met ‘ ( Base ‘ ( ( Scalar ‘ ℂfld ) Xs ( 𝐼 × { ( ℂfld ↾s ℝ ) } ) ) ) ) )
26 eqid ⊢ ( Scalar ‘ ℂfld ) = ( Scalar ‘ ℂfld )
27 8 26 resssca ⊢ ( ℝ ∈ V → ( Scalar ‘ ℂfld ) = ( Scalar ‘ ( ℂfld ↾s ℝ ) ) )
28 12 27 ax-mp ⊢ ( Scalar ‘ ℂfld ) = ( Scalar ‘ ( ℂfld ↾s ℝ ) )
29 1 28 pwsval ⊢ ( ( ( ℂfld ↾s ℝ ) ∈ V ∧ 𝐼 ∈ Fin ) → 𝑌 = ( ( Scalar ‘ ℂfld ) Xs ( 𝐼 × { ( ℂfld ↾s ℝ ) } ) ) )
30 20 29 mpan ⊢ ( 𝐼 ∈ Fin → 𝑌 = ( ( Scalar ‘ ℂfld ) Xs ( 𝐼 × { ( ℂfld ↾s ℝ ) } ) ) )
31 30 fveq2d ⊢ ( 𝐼 ∈ Fin → ( dist ‘ 𝑌 ) = ( dist ‘ ( ( Scalar ‘ ℂfld ) Xs ( 𝐼 × { ( ℂfld ↾s ℝ ) } ) ) ) )
32 2 31 syl5eq ⊢ ( 𝐼 ∈ Fin → 𝐷 = ( dist ‘ ( ( Scalar ‘ ℂfld ) Xs ( 𝐼 × { ( ℂfld ↾s ℝ ) } ) ) ) )
33 1 11 pwsbas ⊢ ( ( ( ℂfld ↾s ℝ ) ∈ V ∧ 𝐼 ∈ Fin ) → ( ℝ ↑m 𝐼 ) = ( Base ‘ 𝑌 ) )
34 20 33 mpan ⊢ ( 𝐼 ∈ Fin → ( ℝ ↑m 𝐼 ) = ( Base ‘ 𝑌 ) )
35 30 fveq2d ⊢ ( 𝐼 ∈ Fin → ( Base ‘ 𝑌 ) = ( Base ‘ ( ( Scalar ‘ ℂfld ) Xs ( 𝐼 × { ( ℂfld ↾s ℝ ) } ) ) ) )
36 34 35 eqtrd ⊢ ( 𝐼 ∈ Fin → ( ℝ ↑m 𝐼 ) = ( Base ‘ ( ( Scalar ‘ ℂfld ) Xs ( 𝐼 × { ( ℂfld ↾s ℝ ) } ) ) ) )
37 3 36 syl5eq ⊢ ( 𝐼 ∈ Fin → 𝑋 = ( Base ‘ ( ( Scalar ‘ ℂfld ) Xs ( 𝐼 × { ( ℂfld ↾s ℝ ) } ) ) ) )
38 37 fveq2d ⊢ ( 𝐼 ∈ Fin → ( Met ‘ 𝑋 ) = ( Met ‘ ( Base ‘ ( ( Scalar ‘ ℂfld ) Xs ( 𝐼 × { ( ℂfld ↾s ℝ ) } ) ) ) ) )
39 25 32 38 3eltr4d ⊢ ( 𝐼 ∈ Fin → 𝐷 ∈ ( Met ‘ 𝑋 ) )