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 } ) , ℝ* , < ) )