Metamath Proof Explorer


Theorem prdsdsval

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

Ref Expression
Hypotheses prdsbasmpt.y 𝑌 = ( 𝑆 Xs 𝑅 )
prdsbasmpt.b 𝐵 = ( Base ‘ 𝑌 )
prdsbasmpt.s ( 𝜑𝑆𝑉 )
prdsbasmpt.i ( 𝜑𝐼𝑊 )
prdsbasmpt.r ( 𝜑𝑅 Fn 𝐼 )
prdsplusgval.f ( 𝜑𝐹𝐵 )
prdsplusgval.g ( 𝜑𝐺𝐵 )
prdsdsval.d 𝐷 = ( dist ‘ 𝑌 )
Assertion prdsdsval ( 𝜑 → ( 𝐹 𝐷 𝐺 ) = sup ( ( ran ( 𝑥𝐼 ↦ ( ( 𝐹𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝐺𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 prdsbasmpt.y 𝑌 = ( 𝑆 Xs 𝑅 )
2 prdsbasmpt.b 𝐵 = ( Base ‘ 𝑌 )
3 prdsbasmpt.s ( 𝜑𝑆𝑉 )
4 prdsbasmpt.i ( 𝜑𝐼𝑊 )
5 prdsbasmpt.r ( 𝜑𝑅 Fn 𝐼 )
6 prdsplusgval.f ( 𝜑𝐹𝐵 )
7 prdsplusgval.g ( 𝜑𝐺𝐵 )
8 prdsdsval.d 𝐷 = ( dist ‘ 𝑌 )
9 fnex ( ( 𝑅 Fn 𝐼𝐼𝑊 ) → 𝑅 ∈ V )
10 5 4 9 syl2anc ( 𝜑𝑅 ∈ V )
11 fndm ( 𝑅 Fn 𝐼 → dom 𝑅 = 𝐼 )
12 5 11 syl ( 𝜑 → dom 𝑅 = 𝐼 )
13 1 3 10 2 12 8 prdsds ( 𝜑𝐷 = ( 𝑓𝐵 , 𝑔𝐵 ↦ sup ( ( ran ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) )
14 fveq1 ( 𝑓 = 𝐹 → ( 𝑓𝑥 ) = ( 𝐹𝑥 ) )
15 fveq1 ( 𝑔 = 𝐺 → ( 𝑔𝑥 ) = ( 𝐺𝑥 ) )
16 14 15 oveqan12d ( ( 𝑓 = 𝐹𝑔 = 𝐺 ) → ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) = ( ( 𝐹𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝐺𝑥 ) ) )
17 16 adantl ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) → ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) = ( ( 𝐹𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝐺𝑥 ) ) )
18 17 mpteq2dv ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) → ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) = ( 𝑥𝐼 ↦ ( ( 𝐹𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝐺𝑥 ) ) ) )
19 18 rneqd ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) → ran ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) = ran ( 𝑥𝐼 ↦ ( ( 𝐹𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝐺𝑥 ) ) ) )
20 19 uneq1d ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) → ( ran ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) = ( ran ( 𝑥𝐼 ↦ ( ( 𝐹𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝐺𝑥 ) ) ) ∪ { 0 } ) )
21 20 supeq1d ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑔 = 𝐺 ) ) → sup ( ( ran ( 𝑥𝐼 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) = sup ( ( ran ( 𝑥𝐼 ↦ ( ( 𝐹𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝐺𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) )
22 xrltso < Or ℝ*
23 22 supex sup ( ( ran ( 𝑥𝐼 ↦ ( ( 𝐹𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝐺𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ∈ V
24 23 a1i ( 𝜑 → sup ( ( ran ( 𝑥𝐼 ↦ ( ( 𝐹𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝐺𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ∈ V )
25 13 21 6 7 24 ovmpod ( 𝜑 → ( 𝐹 𝐷 𝐺 ) = sup ( ( ran ( 𝑥𝐼 ↦ ( ( 𝐹𝑥 ) ( dist ‘ ( 𝑅𝑥 ) ) ( 𝐺𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) )