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

Metamath Proof Explorer

Theorem prdsdsval2

Description: Value of the metric in a structure product. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Hypotheses prdsbasmpt2.y ⊢ 𝑌 = ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) )
prdsbasmpt2.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
prdsbasmpt2.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
prdsbasmpt2.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
prdsbasmpt2.r ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 𝑅 ∈ 𝑋 )
prdsdsval2.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
prdsdsval2.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
prdsdsval2.e ⊢ 𝐸 = ( dist ‘ 𝑅 )
prdsdsval2.d ⊢ 𝐷 = ( dist ‘ 𝑌 )
Assertion prdsdsval2 ( 𝜑 → ( 𝐹 𝐷 𝐺 ) = sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐺 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 prdsbasmpt2.y ⊢ 𝑌 = ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) )
2 prdsbasmpt2.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
3 prdsbasmpt2.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
4 prdsbasmpt2.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
5 prdsbasmpt2.r ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 𝑅 ∈ 𝑋 )
6 prdsdsval2.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
7 prdsdsval2.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
8 prdsdsval2.e ⊢ 𝐸 = ( dist ‘ 𝑅 )
9 prdsdsval2.d ⊢ 𝐷 = ( dist ‘ 𝑌 )
10 eqid ⊢ ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) = ( 𝑥 ∈ 𝐼 ↦ 𝑅 )
11 10 fnmpt ⊢ ( ∀ 𝑥 ∈ 𝐼 𝑅 ∈ 𝑋 → ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) Fn 𝐼 )
12 5 11 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) Fn 𝐼 )
13 1 2 3 4 12 6 7 9 prdsdsval ⊢ ( 𝜑 → ( 𝐹 𝐷 𝐺 ) = sup ( ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑦 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) ( 𝐺 ‘ 𝑦 ) ) ) ∪ { 0 } ) , ℝ* , < ) )
14 nfcv ⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑦 )
15 nfcv ⊢ Ⅎ 𝑥 dist
16 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 )
17 15 16 nffv ⊢ Ⅎ 𝑥 ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) )
18 nfcv ⊢ Ⅎ 𝑥 ( 𝐺 ‘ 𝑦 )
19 14 17 18 nfov ⊢ Ⅎ 𝑥 ( ( 𝐹 ‘ 𝑦 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) ( 𝐺 ‘ 𝑦 ) )
20 nfcv ⊢ Ⅎ 𝑦 ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) )
21 2fveq3 ⊢ ( 𝑦 = 𝑥 → ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) = ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑥 ) ) )
22 fveq2 ⊢ ( 𝑦 = 𝑥 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) )
23 fveq2 ⊢ ( 𝑦 = 𝑥 → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑥 ) )
24 21 22 23 oveq123d ⊢ ( 𝑦 = 𝑥 → ( ( 𝐹 ‘ 𝑦 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) ( 𝐺 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) )
25 19 20 24 cbvmpt ⊢ ( 𝑦 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑦 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) ( 𝐺 ‘ 𝑦 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) )
26 eqidd ⊢ ( 𝜑 → 𝐼 = 𝐼 )
27 10 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐼 ∧ 𝑅 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑥 ) = 𝑅 )
28 27 fveq2d ⊢ ( ( 𝑥 ∈ 𝐼 ∧ 𝑅 ∈ 𝑋 ) → ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑥 ) ) = ( dist ‘ 𝑅 ) )
29 28 8 eqtr4di ⊢ ( ( 𝑥 ∈ 𝐼 ∧ 𝑅 ∈ 𝑋 ) → ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑥 ) ) = 𝐸 )
30 29 oveqd ⊢ ( ( 𝑥 ∈ 𝐼 ∧ 𝑅 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐺 ‘ 𝑥 ) ) )
31 30 ralimiaa ⊢ ( ∀ 𝑥 ∈ 𝐼 𝑅 ∈ 𝑋 → ∀ 𝑥 ∈ 𝐼 ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐺 ‘ 𝑥 ) ) )
32 5 31 syl ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐺 ‘ 𝑥 ) ) )
33 mpteq12 ⊢ ( ( 𝐼 = 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐺 ‘ 𝑥 ) ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐺 ‘ 𝑥 ) ) ) )
34 26 32 33 syl2anc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐺 ‘ 𝑥 ) ) ) )
35 25 34 eqtrid ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑦 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) ( 𝐺 ‘ 𝑦 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐺 ‘ 𝑥 ) ) ) )
36 35 rneqd ⊢ ( 𝜑 → ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑦 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) ( 𝐺 ‘ 𝑦 ) ) ) = ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐺 ‘ 𝑥 ) ) ) )
37 36 uneq1d ⊢ ( 𝜑 → ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑦 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) ( 𝐺 ‘ 𝑦 ) ) ) ∪ { 0 } ) = ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐺 ‘ 𝑥 ) ) ) ∪ { 0 } ) )
38 37 supeq1d ⊢ ( 𝜑 → sup ( ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑦 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) ( 𝐺 ‘ 𝑦 ) ) ) ∪ { 0 } ) , ℝ* , < ) = sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐺 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) )
39 13 38 eqtrd ⊢ ( 𝜑 → ( 𝐹 𝐷 𝐺 ) = sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐺 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) )