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 ⊒Y=S⨉𝑠x∈I⟼R
prdsdsf.b ⊒B=BaseY
prdsdsf.v ⊒V=BaseR
prdsdsf.e ⊒E=dist⁑Rβ†ΎVΓ—V
prdsdsf.d ⊒D=dist⁑Y
prdsdsf.s βŠ’Ο†β†’S∈W
prdsdsf.i βŠ’Ο†β†’I∈X
prdsdsf.r βŠ’Ο†βˆ§x∈Iβ†’R∈Z
prdsdsf.m βŠ’Ο†βˆ§x∈Iβ†’E∈∞Met⁑V
Assertion prdsdsf βŠ’Ο†β†’D:BΓ—B⟢0+∞

Proof

Step Hyp Ref Expression
1 prdsdsf.y ⊒Y=S⨉𝑠x∈I⟼R
2 prdsdsf.b ⊒B=BaseY
3 prdsdsf.v ⊒V=BaseR
4 prdsdsf.e ⊒E=dist⁑Rβ†ΎVΓ—V
5 prdsdsf.d ⊒D=dist⁑Y
6 prdsdsf.s βŠ’Ο†β†’S∈W
7 prdsdsf.i βŠ’Ο†β†’I∈X
8 prdsdsf.r βŠ’Ο†βˆ§x∈Iβ†’R∈Z
9 prdsdsf.m βŠ’Ο†βˆ§x∈Iβ†’E∈∞Met⁑V
10 simpr βŠ’Ο†βˆ§f∈B∧g∈B∧y∈Iβ†’y∈I
11 8 elexd βŠ’Ο†βˆ§x∈Iβ†’R∈V
12 11 ralrimiva βŠ’Ο†β†’βˆ€x∈IR∈V
13 12 adantr βŠ’Ο†βˆ§f∈B∧g∈Bβ†’βˆ€x∈IR∈V
14 nfcsb1v βŠ’β„²_x⦋y/x⦌R
15 14 nfel1 βŠ’β„²x⦋y/x⦌R∈V
16 csbeq1a ⊒x=yβ†’R=⦋y/x⦌R
17 16 eleq1d ⊒x=yβ†’R∈V↔⦋y/x⦌R∈V
18 15 17 rspc ⊒y∈Iβ†’βˆ€x∈IR∈V→⦋y/x⦌R∈V
19 13 18 mpan9 βŠ’Ο†βˆ§f∈B∧g∈B∧y∈I→⦋y/x⦌R∈V
20 eqid ⊒x∈I⟼R=x∈I⟼R
21 20 fvmpts ⊒y∈Iβˆ§β¦‹y/x⦌R∈Vβ†’x∈I⟼R⁑y=⦋y/x⦌R
22 10 19 21 syl2anc βŠ’Ο†βˆ§f∈B∧g∈B∧y∈Iβ†’x∈I⟼R⁑y=⦋y/x⦌R
23 22 fveq2d βŠ’Ο†βˆ§f∈B∧g∈B∧y∈Iβ†’dist⁑x∈I⟼R⁑y=dist⁑⦋y/x⦌R
24 23 oveqd βŠ’Ο†βˆ§f∈B∧g∈B∧y∈Iβ†’f⁑ydist⁑x∈I⟼R⁑yg⁑y=f⁑ydist⁑⦋y/x⦌Rg⁑y
25 6 adantr βŠ’Ο†βˆ§f∈B∧g∈Bβ†’S∈W
26 7 adantr βŠ’Ο†βˆ§f∈B∧g∈Bβ†’I∈X
27 simprl βŠ’Ο†βˆ§f∈B∧g∈Bβ†’f∈B
28 1 2 25 26 13 3 27 prdsbascl βŠ’Ο†βˆ§f∈B∧g∈Bβ†’βˆ€x∈If⁑x∈V
29 nfcsb1v βŠ’β„²_x⦋y/x⦌V
30 29 nfel2 βŠ’β„²xf⁑yβˆˆβ¦‹y/x⦌V
31 fveq2 ⊒x=yβ†’f⁑x=f⁑y
32 csbeq1a ⊒x=yβ†’V=⦋y/x⦌V
33 31 32 eleq12d ⊒x=yβ†’f⁑x∈V↔f⁑yβˆˆβ¦‹y/x⦌V
34 30 33 rspc ⊒y∈Iβ†’βˆ€x∈If⁑x∈Vβ†’f⁑yβˆˆβ¦‹y/x⦌V
35 28 34 mpan9 βŠ’Ο†βˆ§f∈B∧g∈B∧y∈Iβ†’f⁑yβˆˆβ¦‹y/x⦌V
36 simprr βŠ’Ο†βˆ§f∈B∧g∈Bβ†’g∈B
37 1 2 25 26 13 3 36 prdsbascl βŠ’Ο†βˆ§f∈B∧g∈Bβ†’βˆ€x∈Ig⁑x∈V
38 29 nfel2 βŠ’β„²xg⁑yβˆˆβ¦‹y/x⦌V
39 fveq2 ⊒x=yβ†’g⁑x=g⁑y
40 39 32 eleq12d ⊒x=yβ†’g⁑x∈V↔g⁑yβˆˆβ¦‹y/x⦌V
41 38 40 rspc ⊒y∈Iβ†’βˆ€x∈Ig⁑x∈Vβ†’g⁑yβˆˆβ¦‹y/x⦌V
42 37 41 mpan9 βŠ’Ο†βˆ§f∈B∧g∈B∧y∈Iβ†’g⁑yβˆˆβ¦‹y/x⦌V
43 35 42 ovresd βŠ’Ο†βˆ§f∈B∧g∈B∧y∈Iβ†’f⁑ydist⁑⦋y/x⦌R↾⦋y/x⦌V×⦋y/x⦌Vg⁑y=f⁑ydist⁑⦋y/x⦌Rg⁑y
44 24 43 eqtr4d βŠ’Ο†βˆ§f∈B∧g∈B∧y∈Iβ†’f⁑ydist⁑x∈I⟼R⁑yg⁑y=f⁑ydist⁑⦋y/x⦌R↾⦋y/x⦌V×⦋y/x⦌Vg⁑y
45 9 ralrimiva βŠ’Ο†β†’βˆ€x∈IE∈∞Met⁑V
46 45 adantr βŠ’Ο†βˆ§f∈B∧g∈Bβ†’βˆ€x∈IE∈∞Met⁑V
47 nfcv βŠ’β„²_xdist
48 47 14 nffv βŠ’β„²_xdist⁑⦋y/x⦌R
49 29 29 nfxp βŠ’β„²_x⦋y/x⦌V×⦋y/x⦌V
50 48 49 nfres βŠ’β„²_xdist⁑⦋y/x⦌R↾⦋y/x⦌V×⦋y/x⦌V
51 nfcv βŠ’β„²_x∞Met
52 51 29 nffv βŠ’β„²_x∞Met⁑⦋y/x⦌V
53 50 52 nfel βŠ’β„²xdist⁑⦋y/x⦌R↾⦋y/x⦌V×⦋y/x⦌V∈∞Met⁑⦋y/x⦌V
54 16 fveq2d ⊒x=yβ†’dist⁑R=dist⁑⦋y/x⦌R
55 32 sqxpeqd ⊒x=yβ†’VΓ—V=⦋y/x⦌V×⦋y/x⦌V
56 54 55 reseq12d ⊒x=yβ†’dist⁑Rβ†ΎVΓ—V=dist⁑⦋y/x⦌R↾⦋y/x⦌V×⦋y/x⦌V
57 4 56 eqtrid ⊒x=yβ†’E=dist⁑⦋y/x⦌R↾⦋y/x⦌V×⦋y/x⦌V
58 32 fveq2d ⊒x=yβ†’βˆžMet⁑V=∞Met⁑⦋y/x⦌V
59 57 58 eleq12d ⊒x=yβ†’E∈∞Met⁑V↔dist⁑⦋y/x⦌R↾⦋y/x⦌V×⦋y/x⦌V∈∞Met⁑⦋y/x⦌V
60 53 59 rspc ⊒y∈Iβ†’βˆ€x∈IE∈∞Met⁑Vβ†’dist⁑⦋y/x⦌R↾⦋y/x⦌V×⦋y/x⦌V∈∞Met⁑⦋y/x⦌V
61 46 60 mpan9 βŠ’Ο†βˆ§f∈B∧g∈B∧y∈Iβ†’dist⁑⦋y/x⦌R↾⦋y/x⦌V×⦋y/x⦌V∈∞Met⁑⦋y/x⦌V
62 xmetcl ⊒dist⁑⦋y/x⦌R↾⦋y/x⦌V×⦋y/x⦌V∈∞Met⁑⦋y/x⦌V∧f⁑yβˆˆβ¦‹y/x⦌V∧g⁑yβˆˆβ¦‹y/x⦌Vβ†’f⁑ydist⁑⦋y/x⦌R↾⦋y/x⦌V×⦋y/x⦌Vg⁑yβˆˆβ„*
63 61 35 42 62 syl3anc βŠ’Ο†βˆ§f∈B∧g∈B∧y∈Iβ†’f⁑ydist⁑⦋y/x⦌R↾⦋y/x⦌V×⦋y/x⦌Vg⁑yβˆˆβ„*
64 44 63 eqeltrd βŠ’Ο†βˆ§f∈B∧g∈B∧y∈Iβ†’f⁑ydist⁑x∈I⟼R⁑yg⁑yβˆˆβ„*
65 64 fmpttd βŠ’Ο†βˆ§f∈B∧g∈Bβ†’y∈I⟼f⁑ydist⁑x∈I⟼R⁑yg⁑y:IβŸΆβ„*
66 65 frnd βŠ’Ο†βˆ§f∈B∧g∈Bβ†’ran⁑y∈I⟼f⁑ydist⁑x∈I⟼R⁑yg⁑yβŠ†β„*
67 0xr ⊒0βˆˆβ„*
68 67 a1i βŠ’Ο†βˆ§f∈B∧g∈Bβ†’0βˆˆβ„*
69 68 snssd βŠ’Ο†βˆ§f∈B∧g∈Bβ†’0βŠ†β„*
70 66 69 unssd βŠ’Ο†βˆ§f∈B∧g∈Bβ†’ran⁑y∈I⟼f⁑ydist⁑x∈I⟼R⁑yg⁑yβˆͺ0βŠ†β„*
71 supxrcl ⊒ran⁑y∈I⟼f⁑ydist⁑x∈I⟼R⁑yg⁑yβˆͺ0βŠ†β„*β†’supran⁑y∈I⟼f⁑ydist⁑x∈I⟼R⁑yg⁑yβˆͺ0ℝ*<βˆˆβ„*
72 70 71 syl βŠ’Ο†βˆ§f∈B∧g∈Bβ†’supran⁑y∈I⟼f⁑ydist⁑x∈I⟼R⁑yg⁑yβˆͺ0ℝ*<βˆˆβ„*
73 ssun2 ⊒0βŠ†ran⁑y∈I⟼f⁑ydist⁑x∈I⟼R⁑yg⁑yβˆͺ0
74 c0ex ⊒0∈V
75 74 snss ⊒0∈ran⁑y∈I⟼f⁑ydist⁑x∈I⟼R⁑yg⁑yβˆͺ0↔0βŠ†ran⁑y∈I⟼f⁑ydist⁑x∈I⟼R⁑yg⁑yβˆͺ0
76 73 75 mpbir ⊒0∈ran⁑y∈I⟼f⁑ydist⁑x∈I⟼R⁑yg⁑yβˆͺ0
77 supxrub ⊒ran⁑y∈I⟼f⁑ydist⁑x∈I⟼R⁑yg⁑yβˆͺ0βŠ†β„*∧0∈ran⁑y∈I⟼f⁑ydist⁑x∈I⟼R⁑yg⁑yβˆͺ0β†’0≀supran⁑y∈I⟼f⁑ydist⁑x∈I⟼R⁑yg⁑yβˆͺ0ℝ*<
78 70 76 77 sylancl βŠ’Ο†βˆ§f∈B∧g∈Bβ†’0≀supran⁑y∈I⟼f⁑ydist⁑x∈I⟼R⁑yg⁑yβˆͺ0ℝ*<
79 elxrge0 ⊒supran⁑y∈I⟼f⁑ydist⁑x∈I⟼R⁑yg⁑yβˆͺ0ℝ*<∈0+βˆžβ†”supran⁑y∈I⟼f⁑ydist⁑x∈I⟼R⁑yg⁑yβˆͺ0ℝ*<βˆˆβ„*∧0≀supran⁑y∈I⟼f⁑ydist⁑x∈I⟼R⁑yg⁑yβˆͺ0ℝ*<
80 72 78 79 sylanbrc βŠ’Ο†βˆ§f∈B∧g∈Bβ†’supran⁑y∈I⟼f⁑ydist⁑x∈I⟼R⁑yg⁑yβˆͺ0ℝ*<∈0+∞
81 80 ralrimivva βŠ’Ο†β†’βˆ€f∈Bβˆ€g∈Bsupran⁑y∈I⟼f⁑ydist⁑x∈I⟼R⁑yg⁑yβˆͺ0ℝ*<∈0+∞
82 eqid ⊒f∈B,g∈B⟼supran⁑y∈I⟼f⁑ydist⁑x∈I⟼R⁑yg⁑yβˆͺ0ℝ*<=f∈B,g∈B⟼supran⁑y∈I⟼f⁑ydist⁑x∈I⟼R⁑yg⁑yβˆͺ0ℝ*<
83 82 fmpo βŠ’βˆ€f∈Bβˆ€g∈Bsupran⁑y∈I⟼f⁑ydist⁑x∈I⟼R⁑yg⁑yβˆͺ0ℝ*<∈0+βˆžβ†”f∈B,g∈B⟼supran⁑y∈I⟼f⁑ydist⁑x∈I⟼R⁑yg⁑yβˆͺ0ℝ*<:BΓ—B⟢0+∞
84 81 83 sylib βŠ’Ο†β†’f∈B,g∈B⟼supran⁑y∈I⟼f⁑ydist⁑x∈I⟼R⁑yg⁑yβˆͺ0ℝ*<:BΓ—B⟢0+∞
85 7 mptexd βŠ’Ο†β†’x∈I⟼R∈V
86 8 ralrimiva βŠ’Ο†β†’βˆ€x∈IR∈Z
87 dmmptg βŠ’βˆ€x∈IR∈Zβ†’dom⁑x∈I⟼R=I
88 86 87 syl βŠ’Ο†β†’dom⁑x∈I⟼R=I
89 1 6 85 2 88 5 prdsds βŠ’Ο†β†’D=f∈B,g∈B⟼supran⁑y∈I⟼f⁑ydist⁑x∈I⟼R⁑yg⁑yβˆͺ0ℝ*<
90 89 feq1d βŠ’Ο†β†’D:BΓ—B⟢0+βˆžβ†”f∈B,g∈B⟼supran⁑y∈I⟼f⁑ydist⁑x∈I⟼R⁑yg⁑yβˆͺ0ℝ*<:BΓ—B⟢0+∞
91 84 90 mpbird βŠ’Ο†β†’D:BΓ—B⟢0+∞