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

Metamath Proof Explorer

Theorem prdsdsfn

Description: Structure product distance function. (Contributed by Mario Carneiro, 15-Sep-2015)

Ref Expression
Hypotheses prdsbas.p ⊢ 𝑃 = ( 𝑆 Xs 𝑅 )
prdsbas.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
prdsbas.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
prdsbas.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
prdsbas.i ⊢ ( 𝜑 → dom 𝑅 = 𝐼 )
prdsds.l ⊢ 𝐷 = ( dist ‘ 𝑃 )
Assertion prdsdsfn ( 𝜑 → 𝐷 Fn ( 𝐵 × 𝐵 ) )

Proof

Step Hyp Ref Expression
1 prdsbas.p ⊢ 𝑃 = ( 𝑆 Xs 𝑅 )
2 prdsbas.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
3 prdsbas.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
4 prdsbas.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
5 prdsbas.i ⊢ ( 𝜑 → dom 𝑅 = 𝐼 )
6 prdsds.l ⊢ 𝐷 = ( dist ‘ 𝑃 )
7 eqid ⊢ ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) )
8 xrltso ⊢ < Or ℝ*
9 8 supex ⊢ sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ∈ V
10 7 9 fnmpoi ⊢ ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) Fn ( 𝐵 × 𝐵 )
11 1 2 3 4 5 6 prdsds ⊢ ( 𝜑 → 𝐷 = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) )
12 11 fneq1d ⊢ ( 𝜑 → ( 𝐷 Fn ( 𝐵 × 𝐵 ) ↔ ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) Fn ( 𝐵 × 𝐵 ) ) )
13 10 12 mpbiri ⊢ ( 𝜑 → 𝐷 Fn ( 𝐵 × 𝐵 ) )