Metamath Proof Explorer

Theorem prdsdsval3

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

Ref Expression
Hypotheses prdsbasmpt2.y ⊢ 𝑌 = ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) )
prdsbasmpt2.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
prdsbasmpt2.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
prdsbasmpt2.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
prdsbasmpt2.r ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 𝑅 ∈ 𝑋 )
prdsdsval2.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
prdsdsval2.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
prdsdsval3.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
prdsdsval3.e ⊢ 𝐸 = ( ( dist ‘ 𝑅 ) ↾ ( 𝐾 × 𝐾 ) )
prdsdsval3.d ⊢ 𝐷 = ( dist ‘ 𝑌 )
Assertion prdsdsval3 ( 𝜑 → ( 𝐹 𝐷 𝐺 ) = 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 prdsdsval3.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
9 prdsdsval3.e ⊢ 𝐸 = ( ( dist ‘ 𝑅 ) ↾ ( 𝐾 × 𝐾 ) )
10 prdsdsval3.d ⊢ 𝐷 = ( dist ‘ 𝑌 )
11 eqid ⊢ ( dist ‘ 𝑅 ) = ( dist ‘ 𝑅 )
12 1 2 3 4 5 6 7 11 10 prdsdsval2 ⊢ ( 𝜑 → ( 𝐹 𝐷 𝐺 ) = sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ 𝑅 ) ( 𝐺 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) )
13 eqidd ⊢ ( 𝜑 → 𝐼 = 𝐼 )
14 1 2 3 4 5 8 6 prdsbascl ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ 𝐾 )
15 1 2 3 4 5 8 7 prdsbascl ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 ( 𝐺 ‘ 𝑥 ) ∈ 𝐾 )
16 9 oveqi ⊢ ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( ( dist ‘ 𝑅 ) ↾ ( 𝐾 × 𝐾 ) ) ( 𝐺 ‘ 𝑥 ) )
17 ovres ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑥 ) ∈ 𝐾 ) → ( ( 𝐹 ‘ 𝑥 ) ( ( dist ‘ 𝑅 ) ↾ ( 𝐾 × 𝐾 ) ) ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ 𝑅 ) ( 𝐺 ‘ 𝑥 ) ) )
18 16 17 syl5eq ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑥 ) ∈ 𝐾 ) → ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ 𝑅 ) ( 𝐺 ‘ 𝑥 ) ) )
19 18 ex ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐾 → ( ( 𝐺 ‘ 𝑥 ) ∈ 𝐾 → ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ 𝑅 ) ( 𝐺 ‘ 𝑥 ) ) ) )
20 19 ral2imi ⊢ ( ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ 𝐾 → ( ∀ 𝑥 ∈ 𝐼 ( 𝐺 ‘ 𝑥 ) ∈ 𝐾 → ∀ 𝑥 ∈ 𝐼 ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ 𝑅 ) ( 𝐺 ‘ 𝑥 ) ) ) )
21 14 15 20 sylc ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ 𝑅 ) ( 𝐺 ‘ 𝑥 ) ) )
22 mpteq12 ⊢ ( ( 𝐼 = 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ 𝑅 ) ( 𝐺 ‘ 𝑥 ) ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐺 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ 𝑅 ) ( 𝐺 ‘ 𝑥 ) ) ) )
23 13 21 22 syl2anc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐺 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ 𝑅 ) ( 𝐺 ‘ 𝑥 ) ) ) )
24 23 rneqd ⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐺 ‘ 𝑥 ) ) ) = ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ 𝑅 ) ( 𝐺 ‘ 𝑥 ) ) ) )
25 24 uneq1d ⊢ ( 𝜑 → ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐺 ‘ 𝑥 ) ) ) ∪ { 0 } ) = ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ 𝑅 ) ( 𝐺 ‘ 𝑥 ) ) ) ∪ { 0 } ) )
26 25 supeq1d ⊢ ( 𝜑 → sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐺 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) = sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( dist ‘ 𝑅 ) ( 𝐺 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) )
27 12 26 eqtr4d ⊢ ( 𝜑 → ( 𝐹 𝐷 𝐺 ) = sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐺 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) )