Metamath Proof Explorer

Theorem prdsdsf

Description: The product metric is a function into the nonnegative extended reals. In general this means that it is not a metric but rather an *extended* metric (even when all the factors are metrics), but it will be a metric when restricted to regions where it does not take infinite values. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Hypotheses prdsdsf.y ⊒ π‘Œ = ( 𝑆 Xs ( π‘₯ ∈ 𝐼 ↦ 𝑅 ) )
prdsdsf.b ⊒ 𝐡 = ( Base β€˜ π‘Œ )
prdsdsf.v ⊒ 𝑉 = ( Base β€˜ 𝑅 )
prdsdsf.e ⊒ 𝐸 = ( ( dist β€˜ 𝑅 ) β†Ύ ( 𝑉 Γ— 𝑉 ) )
prdsdsf.d ⊒ 𝐷 = ( dist β€˜ π‘Œ )
prdsdsf.s ⊒ ( πœ‘ β†’ 𝑆 ∈ π‘Š )
prdsdsf.i ⊒ ( πœ‘ β†’ 𝐼 ∈ 𝑋 )
prdsdsf.r ⊒ ( ( πœ‘ ∧ π‘₯ ∈ 𝐼 ) β†’ 𝑅 ∈ 𝑍 )
prdsdsf.m ⊒ ( ( πœ‘ ∧ π‘₯ ∈ 𝐼 ) β†’ 𝐸 ∈ ( ∞Met β€˜ 𝑉 ) )
Assertion prdsdsf ( πœ‘ β†’ 𝐷 : ( 𝐡 Γ— 𝐡 ) ⟢ ( 0 [,] +∞ ) )

Proof

Step Hyp Ref Expression
1 prdsdsf.y ⊒ π‘Œ = ( 𝑆 Xs ( π‘₯ ∈ 𝐼 ↦ 𝑅 ) )
2 prdsdsf.b ⊒ 𝐡 = ( Base β€˜ π‘Œ )
3 prdsdsf.v ⊒ 𝑉 = ( Base β€˜ 𝑅 )
4 prdsdsf.e ⊒ 𝐸 = ( ( dist β€˜ 𝑅 ) β†Ύ ( 𝑉 Γ— 𝑉 ) )
5 prdsdsf.d ⊒ 𝐷 = ( dist β€˜ π‘Œ )
6 prdsdsf.s ⊒ ( πœ‘ β†’ 𝑆 ∈ π‘Š )
7 prdsdsf.i ⊒ ( πœ‘ β†’ 𝐼 ∈ 𝑋 )
8 prdsdsf.r ⊒ ( ( πœ‘ ∧ π‘₯ ∈ 𝐼 ) β†’ 𝑅 ∈ 𝑍 )
9 prdsdsf.m ⊒ ( ( πœ‘ ∧ π‘₯ ∈ 𝐼 ) β†’ 𝐸 ∈ ( ∞Met β€˜ 𝑉 ) )
10 simpr ⊒ ( ( ( πœ‘ ∧ ( 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡 ) ) ∧ 𝑦 ∈ 𝐼 ) β†’ 𝑦 ∈ 𝐼 )
11 8 elexd ⊒ ( ( πœ‘ ∧ π‘₯ ∈ 𝐼 ) β†’ 𝑅 ∈ V )
12 11 ralrimiva ⊒ ( πœ‘ β†’ βˆ€ π‘₯ ∈ 𝐼 𝑅 ∈ V )
13 12 adantr ⊒ ( ( πœ‘ ∧ ( 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡 ) ) β†’ βˆ€ π‘₯ ∈ 𝐼 𝑅 ∈ V )
14 nfcsb1v ⊒ β„² π‘₯ ⦋ 𝑦 / π‘₯ ⦌ 𝑅
15 14 nfel1 ⊒ β„² π‘₯ ⦋ 𝑦 / π‘₯ ⦌ 𝑅 ∈ V
16 csbeq1a ⊒ ( π‘₯ = 𝑦 β†’ 𝑅 = ⦋ 𝑦 / π‘₯ ⦌ 𝑅 )
17 16 eleq1d ⊒ ( π‘₯ = 𝑦 β†’ ( 𝑅 ∈ V ↔ ⦋ 𝑦 / π‘₯ ⦌ 𝑅 ∈ V ) )
18 15 17 rspc ⊒ ( 𝑦 ∈ 𝐼 β†’ ( βˆ€ π‘₯ ∈ 𝐼 𝑅 ∈ V β†’ ⦋ 𝑦 / π‘₯ ⦌ 𝑅 ∈ V ) )
19 13 18 mpan9 ⊒ ( ( ( πœ‘ ∧ ( 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡 ) ) ∧ 𝑦 ∈ 𝐼 ) β†’ ⦋ 𝑦 / π‘₯ ⦌ 𝑅 ∈ V )
20 eqid ⊒ ( π‘₯ ∈ 𝐼 ↦ 𝑅 ) = ( π‘₯ ∈ 𝐼 ↦ 𝑅 )
21 20 fvmpts ⊒ ( ( 𝑦 ∈ 𝐼 ∧ ⦋ 𝑦 / π‘₯ ⦌ 𝑅 ∈ V ) β†’ ( ( π‘₯ ∈ 𝐼 ↦ 𝑅 ) β€˜ 𝑦 ) = ⦋ 𝑦 / π‘₯ ⦌ 𝑅 )
22 10 19 21 syl2anc ⊒ ( ( ( πœ‘ ∧ ( 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡 ) ) ∧ 𝑦 ∈ 𝐼 ) β†’ ( ( π‘₯ ∈ 𝐼 ↦ 𝑅 ) β€˜ 𝑦 ) = ⦋ 𝑦 / π‘₯ ⦌ 𝑅 )
23 22 fveq2d ⊒ ( ( ( πœ‘ ∧ ( 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡 ) ) ∧ 𝑦 ∈ 𝐼 ) β†’ ( dist β€˜ ( ( π‘₯ ∈ 𝐼 ↦ 𝑅 ) β€˜ 𝑦 ) ) = ( dist β€˜ ⦋ 𝑦 / π‘₯ ⦌ 𝑅 ) )
24 23 oveqd ⊒ ( ( ( πœ‘ ∧ ( 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡 ) ) ∧ 𝑦 ∈ 𝐼 ) β†’ ( ( 𝑓 β€˜ 𝑦 ) ( dist β€˜ ( ( π‘₯ ∈ 𝐼 ↦ 𝑅 ) β€˜ 𝑦 ) ) ( 𝑔 β€˜ 𝑦 ) ) = ( ( 𝑓 β€˜ 𝑦 ) ( dist β€˜ ⦋ 𝑦 / π‘₯ ⦌ 𝑅 ) ( 𝑔 β€˜ 𝑦 ) ) )
25 6 adantr ⊒ ( ( πœ‘ ∧ ( 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡 ) ) β†’ 𝑆 ∈ π‘Š )
26 7 adantr ⊒ ( ( πœ‘ ∧ ( 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡 ) ) β†’ 𝐼 ∈ 𝑋 )
27 simprl ⊒ ( ( πœ‘ ∧ ( 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡 ) ) β†’ 𝑓 ∈ 𝐡 )
28 1 2 25 26 13 3 27 prdsbascl ⊒ ( ( πœ‘ ∧ ( 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡 ) ) β†’ βˆ€ π‘₯ ∈ 𝐼 ( 𝑓 β€˜ π‘₯ ) ∈ 𝑉 )
29 nfcsb1v ⊒ β„² π‘₯ ⦋ 𝑦 / π‘₯ ⦌ 𝑉
30 29 nfel2 ⊒ β„² π‘₯ ( 𝑓 β€˜ 𝑦 ) ∈ ⦋ 𝑦 / π‘₯ ⦌ 𝑉
31 fveq2 ⊒ ( π‘₯ = 𝑦 β†’ ( 𝑓 β€˜ π‘₯ ) = ( 𝑓 β€˜ 𝑦 ) )
32 csbeq1a ⊒ ( π‘₯ = 𝑦 β†’ 𝑉 = ⦋ 𝑦 / π‘₯ ⦌ 𝑉 )
33 31 32 eleq12d ⊒ ( π‘₯ = 𝑦 β†’ ( ( 𝑓 β€˜ π‘₯ ) ∈ 𝑉 ↔ ( 𝑓 β€˜ 𝑦 ) ∈ ⦋ 𝑦 / π‘₯ ⦌ 𝑉 ) )
34 30 33 rspc ⊒ ( 𝑦 ∈ 𝐼 β†’ ( βˆ€ π‘₯ ∈ 𝐼 ( 𝑓 β€˜ π‘₯ ) ∈ 𝑉 β†’ ( 𝑓 β€˜ 𝑦 ) ∈ ⦋ 𝑦 / π‘₯ ⦌ 𝑉 ) )
35 28 34 mpan9 ⊒ ( ( ( πœ‘ ∧ ( 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡 ) ) ∧ 𝑦 ∈ 𝐼 ) β†’ ( 𝑓 β€˜ 𝑦 ) ∈ ⦋ 𝑦 / π‘₯ ⦌ 𝑉 )
36 simprr ⊒ ( ( πœ‘ ∧ ( 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡 ) ) β†’ 𝑔 ∈ 𝐡 )
37 1 2 25 26 13 3 36 prdsbascl ⊒ ( ( πœ‘ ∧ ( 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡 ) ) β†’ βˆ€ π‘₯ ∈ 𝐼 ( 𝑔 β€˜ π‘₯ ) ∈ 𝑉 )
38 29 nfel2 ⊒ β„² π‘₯ ( 𝑔 β€˜ 𝑦 ) ∈ ⦋ 𝑦 / π‘₯ ⦌ 𝑉
39 fveq2 ⊒ ( π‘₯ = 𝑦 β†’ ( 𝑔 β€˜ π‘₯ ) = ( 𝑔 β€˜ 𝑦 ) )
40 39 32 eleq12d ⊒ ( π‘₯ = 𝑦 β†’ ( ( 𝑔 β€˜ π‘₯ ) ∈ 𝑉 ↔ ( 𝑔 β€˜ 𝑦 ) ∈ ⦋ 𝑦 / π‘₯ ⦌ 𝑉 ) )
41 38 40 rspc ⊒ ( 𝑦 ∈ 𝐼 β†’ ( βˆ€ π‘₯ ∈ 𝐼 ( 𝑔 β€˜ π‘₯ ) ∈ 𝑉 β†’ ( 𝑔 β€˜ 𝑦 ) ∈ ⦋ 𝑦 / π‘₯ ⦌ 𝑉 ) )
42 37 41 mpan9 ⊒ ( ( ( πœ‘ ∧ ( 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡 ) ) ∧ 𝑦 ∈ 𝐼 ) β†’ ( 𝑔 β€˜ 𝑦 ) ∈ ⦋ 𝑦 / π‘₯ ⦌ 𝑉 )
43 35 42 ovresd ⊒ ( ( ( πœ‘ ∧ ( 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡 ) ) ∧ 𝑦 ∈ 𝐼 ) β†’ ( ( 𝑓 β€˜ 𝑦 ) ( ( dist β€˜ ⦋ 𝑦 / π‘₯ ⦌ 𝑅 ) β†Ύ ( ⦋ 𝑦 / π‘₯ ⦌ 𝑉 Γ— ⦋ 𝑦 / π‘₯ ⦌ 𝑉 ) ) ( 𝑔 β€˜ 𝑦 ) ) = ( ( 𝑓 β€˜ 𝑦 ) ( dist β€˜ ⦋ 𝑦 / π‘₯ ⦌ 𝑅 ) ( 𝑔 β€˜ 𝑦 ) ) )
44 24 43 eqtr4d ⊒ ( ( ( πœ‘ ∧ ( 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡 ) ) ∧ 𝑦 ∈ 𝐼 ) β†’ ( ( 𝑓 β€˜ 𝑦 ) ( dist β€˜ ( ( π‘₯ ∈ 𝐼 ↦ 𝑅 ) β€˜ 𝑦 ) ) ( 𝑔 β€˜ 𝑦 ) ) = ( ( 𝑓 β€˜ 𝑦 ) ( ( dist β€˜ ⦋ 𝑦 / π‘₯ ⦌ 𝑅 ) β†Ύ ( ⦋ 𝑦 / π‘₯ ⦌ 𝑉 Γ— ⦋ 𝑦 / π‘₯ ⦌ 𝑉 ) ) ( 𝑔 β€˜ 𝑦 ) ) )
45 9 ralrimiva ⊒ ( πœ‘ β†’ βˆ€ π‘₯ ∈ 𝐼 𝐸 ∈ ( ∞Met β€˜ 𝑉 ) )
46 45 adantr ⊒ ( ( πœ‘ ∧ ( 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡 ) ) β†’ βˆ€ π‘₯ ∈ 𝐼 𝐸 ∈ ( ∞Met β€˜ 𝑉 ) )
47 nfcv ⊒ β„² π‘₯ dist
48 47 14 nffv ⊒ β„² π‘₯ ( dist β€˜ ⦋ 𝑦 / π‘₯ ⦌ 𝑅 )
49 29 29 nfxp ⊒ β„² π‘₯ ( ⦋ 𝑦 / π‘₯ ⦌ 𝑉 Γ— ⦋ 𝑦 / π‘₯ ⦌ 𝑉 )
50 48 49 nfres ⊒ β„² π‘₯ ( ( dist β€˜ ⦋ 𝑦 / π‘₯ ⦌ 𝑅 ) β†Ύ ( ⦋ 𝑦 / π‘₯ ⦌ 𝑉 Γ— ⦋ 𝑦 / π‘₯ ⦌ 𝑉 ) )
51 nfcv ⊒ β„² π‘₯ ∞Met
52 51 29 nffv ⊒ β„² π‘₯ ( ∞Met β€˜ ⦋ 𝑦 / π‘₯ ⦌ 𝑉 )
53 50 52 nfel ⊒ β„² π‘₯ ( ( dist β€˜ ⦋ 𝑦 / π‘₯ ⦌ 𝑅 ) β†Ύ ( ⦋ 𝑦 / π‘₯ ⦌ 𝑉 Γ— ⦋ 𝑦 / π‘₯ ⦌ 𝑉 ) ) ∈ ( ∞Met β€˜ ⦋ 𝑦 / π‘₯ ⦌ 𝑉 )
54 16 fveq2d ⊒ ( π‘₯ = 𝑦 β†’ ( dist β€˜ 𝑅 ) = ( dist β€˜ ⦋ 𝑦 / π‘₯ ⦌ 𝑅 ) )
55 32 sqxpeqd ⊒ ( π‘₯ = 𝑦 β†’ ( 𝑉 Γ— 𝑉 ) = ( ⦋ 𝑦 / π‘₯ ⦌ 𝑉 Γ— ⦋ 𝑦 / π‘₯ ⦌ 𝑉 ) )
56 54 55 reseq12d ⊒ ( π‘₯ = 𝑦 β†’ ( ( dist β€˜ 𝑅 ) β†Ύ ( 𝑉 Γ— 𝑉 ) ) = ( ( dist β€˜ ⦋ 𝑦 / π‘₯ ⦌ 𝑅 ) β†Ύ ( ⦋ 𝑦 / π‘₯ ⦌ 𝑉 Γ— ⦋ 𝑦 / π‘₯ ⦌ 𝑉 ) ) )
57 4 56 eqtrid ⊒ ( π‘₯ = 𝑦 β†’ 𝐸 = ( ( dist β€˜ ⦋ 𝑦 / π‘₯ ⦌ 𝑅 ) β†Ύ ( ⦋ 𝑦 / π‘₯ ⦌ 𝑉 Γ— ⦋ 𝑦 / π‘₯ ⦌ 𝑉 ) ) )
58 32 fveq2d ⊒ ( π‘₯ = 𝑦 β†’ ( ∞Met β€˜ 𝑉 ) = ( ∞Met β€˜ ⦋ 𝑦 / π‘₯ ⦌ 𝑉 ) )
59 57 58 eleq12d ⊒ ( π‘₯ = 𝑦 β†’ ( 𝐸 ∈ ( ∞Met β€˜ 𝑉 ) ↔ ( ( dist β€˜ ⦋ 𝑦 / π‘₯ ⦌ 𝑅 ) β†Ύ ( ⦋ 𝑦 / π‘₯ ⦌ 𝑉 Γ— ⦋ 𝑦 / π‘₯ ⦌ 𝑉 ) ) ∈ ( ∞Met β€˜ ⦋ 𝑦 / π‘₯ ⦌ 𝑉 ) ) )
60 53 59 rspc ⊒ ( 𝑦 ∈ 𝐼 β†’ ( βˆ€ π‘₯ ∈ 𝐼 𝐸 ∈ ( ∞Met β€˜ 𝑉 ) β†’ ( ( dist β€˜ ⦋ 𝑦 / π‘₯ ⦌ 𝑅 ) β†Ύ ( ⦋ 𝑦 / π‘₯ ⦌ 𝑉 Γ— ⦋ 𝑦 / π‘₯ ⦌ 𝑉 ) ) ∈ ( ∞Met β€˜ ⦋ 𝑦 / π‘₯ ⦌ 𝑉 ) ) )
61 46 60 mpan9 ⊒ ( ( ( πœ‘ ∧ ( 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡 ) ) ∧ 𝑦 ∈ 𝐼 ) β†’ ( ( dist β€˜ ⦋ 𝑦 / π‘₯ ⦌ 𝑅 ) β†Ύ ( ⦋ 𝑦 / π‘₯ ⦌ 𝑉 Γ— ⦋ 𝑦 / π‘₯ ⦌ 𝑉 ) ) ∈ ( ∞Met β€˜ ⦋ 𝑦 / π‘₯ ⦌ 𝑉 ) )
62 xmetcl ⊒ ( ( ( ( dist β€˜ ⦋ 𝑦 / π‘₯ ⦌ 𝑅 ) β†Ύ ( ⦋ 𝑦 / π‘₯ ⦌ 𝑉 Γ— ⦋ 𝑦 / π‘₯ ⦌ 𝑉 ) ) ∈ ( ∞Met β€˜ ⦋ 𝑦 / π‘₯ ⦌ 𝑉 ) ∧ ( 𝑓 β€˜ 𝑦 ) ∈ ⦋ 𝑦 / π‘₯ ⦌ 𝑉 ∧ ( 𝑔 β€˜ 𝑦 ) ∈ ⦋ 𝑦 / π‘₯ ⦌ 𝑉 ) β†’ ( ( 𝑓 β€˜ 𝑦 ) ( ( dist β€˜ ⦋ 𝑦 / π‘₯ ⦌ 𝑅 ) β†Ύ ( ⦋ 𝑦 / π‘₯ ⦌ 𝑉 Γ— ⦋ 𝑦 / π‘₯ ⦌ 𝑉 ) ) ( 𝑔 β€˜ 𝑦 ) ) ∈ ℝ* )
63 61 35 42 62 syl3anc ⊒ ( ( ( πœ‘ ∧ ( 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡 ) ) ∧ 𝑦 ∈ 𝐼 ) β†’ ( ( 𝑓 β€˜ 𝑦 ) ( ( dist β€˜ ⦋ 𝑦 / π‘₯ ⦌ 𝑅 ) β†Ύ ( ⦋ 𝑦 / π‘₯ ⦌ 𝑉 Γ— ⦋ 𝑦 / π‘₯ ⦌ 𝑉 ) ) ( 𝑔 β€˜ 𝑦 ) ) ∈ ℝ* )
64 44 63 eqeltrd ⊒ ( ( ( πœ‘ ∧ ( 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡 ) ) ∧ 𝑦 ∈ 𝐼 ) β†’ ( ( 𝑓 β€˜ 𝑦 ) ( dist β€˜ ( ( π‘₯ ∈ 𝐼 ↦ 𝑅 ) β€˜ 𝑦 ) ) ( 𝑔 β€˜ 𝑦 ) ) ∈ ℝ* )
65 64 fmpttd ⊒ ( ( πœ‘ ∧ ( 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡 ) ) β†’ ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 β€˜ 𝑦 ) ( dist β€˜ ( ( π‘₯ ∈ 𝐼 ↦ 𝑅 ) β€˜ 𝑦 ) ) ( 𝑔 β€˜ 𝑦 ) ) ) : 𝐼 ⟢ ℝ* )
66 65 frnd ⊒ ( ( πœ‘ ∧ ( 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡 ) ) β†’ ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 β€˜ 𝑦 ) ( dist β€˜ ( ( π‘₯ ∈ 𝐼 ↦ 𝑅 ) β€˜ 𝑦 ) ) ( 𝑔 β€˜ 𝑦 ) ) ) βŠ† ℝ* )
67 0xr ⊒ 0 ∈ ℝ*
68 67 a1i ⊒ ( ( πœ‘ ∧ ( 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡 ) ) β†’ 0 ∈ ℝ* )
69 68 snssd ⊒ ( ( πœ‘ ∧ ( 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡 ) ) β†’ { 0 } βŠ† ℝ* )
70 66 69 unssd ⊒ ( ( πœ‘ ∧ ( 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡 ) ) β†’ ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 β€˜ 𝑦 ) ( dist β€˜ ( ( π‘₯ ∈ 𝐼 ↦ 𝑅 ) β€˜ 𝑦 ) ) ( 𝑔 β€˜ 𝑦 ) ) ) βˆͺ { 0 } ) βŠ† ℝ* )
71 supxrcl ⊒ ( ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 β€˜ 𝑦 ) ( dist β€˜ ( ( π‘₯ ∈ 𝐼 ↦ 𝑅 ) β€˜ 𝑦 ) ) ( 𝑔 β€˜ 𝑦 ) ) ) βˆͺ { 0 } ) βŠ† ℝ* β†’ sup ( ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 β€˜ 𝑦 ) ( dist β€˜ ( ( π‘₯ ∈ 𝐼 ↦ 𝑅 ) β€˜ 𝑦 ) ) ( 𝑔 β€˜ 𝑦 ) ) ) βˆͺ { 0 } ) , ℝ* , < ) ∈ ℝ* )
72 70 71 syl ⊒ ( ( πœ‘ ∧ ( 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡 ) ) β†’ sup ( ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 β€˜ 𝑦 ) ( dist β€˜ ( ( π‘₯ ∈ 𝐼 ↦ 𝑅 ) β€˜ 𝑦 ) ) ( 𝑔 β€˜ 𝑦 ) ) ) βˆͺ { 0 } ) , ℝ* , < ) ∈ ℝ* )
73 ssun2 ⊒ { 0 } βŠ† ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 β€˜ 𝑦 ) ( dist β€˜ ( ( π‘₯ ∈ 𝐼 ↦ 𝑅 ) β€˜ 𝑦 ) ) ( 𝑔 β€˜ 𝑦 ) ) ) βˆͺ { 0 } )
74 c0ex ⊒ 0 ∈ V
75 74 snss ⊒ ( 0 ∈ ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 β€˜ 𝑦 ) ( dist β€˜ ( ( π‘₯ ∈ 𝐼 ↦ 𝑅 ) β€˜ 𝑦 ) ) ( 𝑔 β€˜ 𝑦 ) ) ) βˆͺ { 0 } ) ↔ { 0 } βŠ† ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 β€˜ 𝑦 ) ( dist β€˜ ( ( π‘₯ ∈ 𝐼 ↦ 𝑅 ) β€˜ 𝑦 ) ) ( 𝑔 β€˜ 𝑦 ) ) ) βˆͺ { 0 } ) )
76 73 75 mpbir ⊒ 0 ∈ ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 β€˜ 𝑦 ) ( dist β€˜ ( ( π‘₯ ∈ 𝐼 ↦ 𝑅 ) β€˜ 𝑦 ) ) ( 𝑔 β€˜ 𝑦 ) ) ) βˆͺ { 0 } )
77 supxrub ⊒ ( ( ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 β€˜ 𝑦 ) ( dist β€˜ ( ( π‘₯ ∈ 𝐼 ↦ 𝑅 ) β€˜ 𝑦 ) ) ( 𝑔 β€˜ 𝑦 ) ) ) βˆͺ { 0 } ) βŠ† ℝ* ∧ 0 ∈ ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 β€˜ 𝑦 ) ( dist β€˜ ( ( π‘₯ ∈ 𝐼 ↦ 𝑅 ) β€˜ 𝑦 ) ) ( 𝑔 β€˜ 𝑦 ) ) ) βˆͺ { 0 } ) ) β†’ 0 ≀ sup ( ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 β€˜ 𝑦 ) ( dist β€˜ ( ( π‘₯ ∈ 𝐼 ↦ 𝑅 ) β€˜ 𝑦 ) ) ( 𝑔 β€˜ 𝑦 ) ) ) βˆͺ { 0 } ) , ℝ* , < ) )
78 70 76 77 sylancl ⊒ ( ( πœ‘ ∧ ( 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡 ) ) β†’ 0 ≀ sup ( ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 β€˜ 𝑦 ) ( dist β€˜ ( ( π‘₯ ∈ 𝐼 ↦ 𝑅 ) β€˜ 𝑦 ) ) ( 𝑔 β€˜ 𝑦 ) ) ) βˆͺ { 0 } ) , ℝ* , < ) )
79 elxrge0 ⊒ ( sup ( ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 β€˜ 𝑦 ) ( dist β€˜ ( ( π‘₯ ∈ 𝐼 ↦ 𝑅 ) β€˜ 𝑦 ) ) ( 𝑔 β€˜ 𝑦 ) ) ) βˆͺ { 0 } ) , ℝ* , < ) ∈ ( 0 [,] +∞ ) ↔ ( sup ( ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 β€˜ 𝑦 ) ( dist β€˜ ( ( π‘₯ ∈ 𝐼 ↦ 𝑅 ) β€˜ 𝑦 ) ) ( 𝑔 β€˜ 𝑦 ) ) ) βˆͺ { 0 } ) , ℝ* , < ) ∈ ℝ* ∧ 0 ≀ sup ( ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 β€˜ 𝑦 ) ( dist β€˜ ( ( π‘₯ ∈ 𝐼 ↦ 𝑅 ) β€˜ 𝑦 ) ) ( 𝑔 β€˜ 𝑦 ) ) ) βˆͺ { 0 } ) , ℝ* , < ) ) )
80 72 78 79 sylanbrc ⊒ ( ( πœ‘ ∧ ( 𝑓 ∈ 𝐡 ∧ 𝑔 ∈ 𝐡 ) ) β†’ sup ( ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 β€˜ 𝑦 ) ( dist β€˜ ( ( π‘₯ ∈ 𝐼 ↦ 𝑅 ) β€˜ 𝑦 ) ) ( 𝑔 β€˜ 𝑦 ) ) ) βˆͺ { 0 } ) , ℝ* , < ) ∈ ( 0 [,] +∞ ) )
81 80 ralrimivva ⊒ ( πœ‘ β†’ βˆ€ 𝑓 ∈ 𝐡 βˆ€ 𝑔 ∈ 𝐡 sup ( ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 β€˜ 𝑦 ) ( dist β€˜ ( ( π‘₯ ∈ 𝐼 ↦ 𝑅 ) β€˜ 𝑦 ) ) ( 𝑔 β€˜ 𝑦 ) ) ) βˆͺ { 0 } ) , ℝ* , < ) ∈ ( 0 [,] +∞ ) )
82 eqid ⊒ ( 𝑓 ∈ 𝐡 , 𝑔 ∈ 𝐡 ↦ sup ( ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 β€˜ 𝑦 ) ( dist β€˜ ( ( π‘₯ ∈ 𝐼 ↦ 𝑅 ) β€˜ 𝑦 ) ) ( 𝑔 β€˜ 𝑦 ) ) ) βˆͺ { 0 } ) , ℝ* , < ) ) = ( 𝑓 ∈ 𝐡 , 𝑔 ∈ 𝐡 ↦ sup ( ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 β€˜ 𝑦 ) ( dist β€˜ ( ( π‘₯ ∈ 𝐼 ↦ 𝑅 ) β€˜ 𝑦 ) ) ( 𝑔 β€˜ 𝑦 ) ) ) βˆͺ { 0 } ) , ℝ* , < ) )
83 82 fmpo ⊒ ( βˆ€ 𝑓 ∈ 𝐡 βˆ€ 𝑔 ∈ 𝐡 sup ( ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 β€˜ 𝑦 ) ( dist β€˜ ( ( π‘₯ ∈ 𝐼 ↦ 𝑅 ) β€˜ 𝑦 ) ) ( 𝑔 β€˜ 𝑦 ) ) ) βˆͺ { 0 } ) , ℝ* , < ) ∈ ( 0 [,] +∞ ) ↔ ( 𝑓 ∈ 𝐡 , 𝑔 ∈ 𝐡 ↦ sup ( ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 β€˜ 𝑦 ) ( dist β€˜ ( ( π‘₯ ∈ 𝐼 ↦ 𝑅 ) β€˜ 𝑦 ) ) ( 𝑔 β€˜ 𝑦 ) ) ) βˆͺ { 0 } ) , ℝ* , < ) ) : ( 𝐡 Γ— 𝐡 ) ⟢ ( 0 [,] +∞ ) )
84 81 83 sylib ⊒ ( πœ‘ β†’ ( 𝑓 ∈ 𝐡 , 𝑔 ∈ 𝐡 ↦ sup ( ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 β€˜ 𝑦 ) ( dist β€˜ ( ( π‘₯ ∈ 𝐼 ↦ 𝑅 ) β€˜ 𝑦 ) ) ( 𝑔 β€˜ 𝑦 ) ) ) βˆͺ { 0 } ) , ℝ* , < ) ) : ( 𝐡 Γ— 𝐡 ) ⟢ ( 0 [,] +∞ ) )
85 7 mptexd ⊒ ( πœ‘ β†’ ( π‘₯ ∈ 𝐼 ↦ 𝑅 ) ∈ V )
86 8 ralrimiva ⊒ ( πœ‘ β†’ βˆ€ π‘₯ ∈ 𝐼 𝑅 ∈ 𝑍 )
87 dmmptg ⊒ ( βˆ€ π‘₯ ∈ 𝐼 𝑅 ∈ 𝑍 β†’ dom ( π‘₯ ∈ 𝐼 ↦ 𝑅 ) = 𝐼 )
88 86 87 syl ⊒ ( πœ‘ β†’ dom ( π‘₯ ∈ 𝐼 ↦ 𝑅 ) = 𝐼 )
89 1 6 85 2 88 5 prdsds ⊒ ( πœ‘ β†’ 𝐷 = ( 𝑓 ∈ 𝐡 , 𝑔 ∈ 𝐡 ↦ sup ( ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 β€˜ 𝑦 ) ( dist β€˜ ( ( π‘₯ ∈ 𝐼 ↦ 𝑅 ) β€˜ 𝑦 ) ) ( 𝑔 β€˜ 𝑦 ) ) ) βˆͺ { 0 } ) , ℝ* , < ) ) )
90 89 feq1d ⊒ ( πœ‘ β†’ ( 𝐷 : ( 𝐡 Γ— 𝐡 ) ⟢ ( 0 [,] +∞ ) ↔ ( 𝑓 ∈ 𝐡 , 𝑔 ∈ 𝐡 ↦ sup ( ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 β€˜ 𝑦 ) ( dist β€˜ ( ( π‘₯ ∈ 𝐼 ↦ 𝑅 ) β€˜ 𝑦 ) ) ( 𝑔 β€˜ 𝑦 ) ) ) βˆͺ { 0 } ) , ℝ* , < ) ) : ( 𝐡 Γ— 𝐡 ) ⟢ ( 0 [,] +∞ ) ) )
91 84 90 mpbird ⊒ ( πœ‘ β†’ 𝐷 : ( 𝐡 Γ— 𝐡 ) ⟢ ( 0 [,] +∞ ) )