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 eqtrid ( ( ( 𝐹𝑥 ) ∈ 𝐾 ∧ ( 𝐺𝑥 ) ∈ 𝐾 ) → ( ( 𝐹𝑥 ) 𝐸 ( 𝐺𝑥 ) ) = ( ( 𝐹𝑥 ) ( 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 } ) , ℝ* , < ) )