Metamath Proof Explorer

Theorem imasf1oxmet

Description: The image of an extended metric is an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Hypotheses imasf1oxmet.u ⊢φ→U=F“𝑠R
imasf1oxmet.v ⊢φ→V=BaseR
imasf1oxmet.f ⊢φ→F:V⟶1-1 ontoB
imasf1oxmet.r ⊢φ→R∈Z
imasf1oxmet.e ⊢E=dist⁡R↾V×V
imasf1oxmet.d ⊢D=dist⁡U
imasf1oxmet.m ⊢φ→E∈∞Met⁡V
Assertion imasf1oxmet ⊢φ→D∈∞Met⁡B

Proof

Step Hyp Ref Expression
1 imasf1oxmet.u ⊢φ→U=F“𝑠R
2 imasf1oxmet.v ⊢φ→V=BaseR
3 imasf1oxmet.f ⊢φ→F:V⟶1-1 ontoB
4 imasf1oxmet.r ⊢φ→R∈Z
5 imasf1oxmet.e ⊢E=dist⁡R↾V×V
6 imasf1oxmet.d ⊢D=dist⁡U
7 imasf1oxmet.m ⊢φ→E∈∞Met⁡V
8 f1ofo ⊢F:V⟶1-1 ontoB→F:V⟶ontoB
9 3 8 syl ⊢φ→F:V⟶ontoB
10 eqid ⊢dist⁡R=dist⁡R
11 1 2 9 4 10 6 imasdsfn ⊢φ→DFnB×B
12 1 adantr ⊢φ∧a∈V∧b∈V→U=F“𝑠R
13 2 adantr ⊢φ∧a∈V∧b∈V→V=BaseR
14 3 adantr ⊢φ∧a∈V∧b∈V→F:V⟶1-1 ontoB
15 4 adantr ⊢φ∧a∈V∧b∈V→R∈Z
16 7 adantr ⊢φ∧a∈V∧b∈V→E∈∞Met⁡V
17 simprl ⊢φ∧a∈V∧b∈V→a∈V
18 simprr ⊢φ∧a∈V∧b∈V→b∈V
19 12 13 14 15 5 6 16 17 18 imasdsf1o ⊢φ∧a∈V∧b∈V→F⁡aDF⁡b=aEb
20 xmetcl ⊢E∈∞Met⁡V∧a∈V∧b∈V→aEb∈ℝ*
21 20 3expb ⊢E∈∞Met⁡V∧a∈V∧b∈V→aEb∈ℝ*
22 7 21 sylan ⊢φ∧a∈V∧b∈V→aEb∈ℝ*
23 19 22 eqeltrd ⊢φ∧a∈V∧b∈V→F⁡aDF⁡b∈ℝ*
24 23 ralrimivva ⊢φ→∀a∈V∀b∈VF⁡aDF⁡b∈ℝ*
25 f1ofn ⊢F:V⟶1-1 ontoB→FFnV
26 3 25 syl ⊢φ→FFnV
27 oveq2 ⊢y=F⁡b→F⁡aDy=F⁡aDF⁡b
28 27 eleq1d ⊢y=F⁡b→F⁡aDy∈ℝ*↔F⁡aDF⁡b∈ℝ*
29 28 ralrn ⊢FFnV→∀y∈ran⁡FF⁡aDy∈ℝ*↔∀b∈VF⁡aDF⁡b∈ℝ*
30 26 29 syl ⊢φ→∀y∈ran⁡FF⁡aDy∈ℝ*↔∀b∈VF⁡aDF⁡b∈ℝ*
31 forn ⊢F:V⟶ontoB→ran⁡F=B
32 9 31 syl ⊢φ→ran⁡F=B
33 32 raleqdv ⊢φ→∀y∈ran⁡FF⁡aDy∈ℝ*↔∀y∈BF⁡aDy∈ℝ*
34 30 33 bitr3d ⊢φ→∀b∈VF⁡aDF⁡b∈ℝ*↔∀y∈BF⁡aDy∈ℝ*
35 34 ralbidv ⊢φ→∀a∈V∀b∈VF⁡aDF⁡b∈ℝ*↔∀a∈V∀y∈BF⁡aDy∈ℝ*
36 24 35 mpbid ⊢φ→∀a∈V∀y∈BF⁡aDy∈ℝ*
37 oveq1 ⊢x=F⁡a→xDy=F⁡aDy
38 37 eleq1d ⊢x=F⁡a→xDy∈ℝ*↔F⁡aDy∈ℝ*
39 38 ralbidv ⊢x=F⁡a→∀y∈BxDy∈ℝ*↔∀y∈BF⁡aDy∈ℝ*
40 39 ralrn ⊢FFnV→∀x∈ran⁡F∀y∈BxDy∈ℝ*↔∀a∈V∀y∈BF⁡aDy∈ℝ*
41 26 40 syl ⊢φ→∀x∈ran⁡F∀y∈BxDy∈ℝ*↔∀a∈V∀y∈BF⁡aDy∈ℝ*
42 32 raleqdv ⊢φ→∀x∈ran⁡F∀y∈BxDy∈ℝ*↔∀x∈B∀y∈BxDy∈ℝ*
43 41 42 bitr3d ⊢φ→∀a∈V∀y∈BF⁡aDy∈ℝ*↔∀x∈B∀y∈BxDy∈ℝ*
44 36 43 mpbid ⊢φ→∀x∈B∀y∈BxDy∈ℝ*
45 ffnov ⊢D:B×B⟶ℝ*↔DFnB×B∧∀x∈B∀y∈BxDy∈ℝ*
46 11 44 45 sylanbrc ⊢φ→D:B×B⟶ℝ*
47 xmeteq0 ⊢E∈∞Met⁡V∧a∈V∧b∈V→aEb=0↔a=b
48 16 17 18 47 syl3anc ⊢φ∧a∈V∧b∈V→aEb=0↔a=b
49 19 eqeq1d ⊢φ∧a∈V∧b∈V→F⁡aDF⁡b=0↔aEb=0
50 f1of1 ⊢F:V⟶1-1 ontoB→F:V⟶1-1B
51 3 50 syl ⊢φ→F:V⟶1-1B
52 f1fveq ⊢F:V⟶1-1B∧a∈V∧b∈V→F⁡a=F⁡b↔a=b
53 51 52 sylan ⊢φ∧a∈V∧b∈V→F⁡a=F⁡b↔a=b
54 48 49 53 3bitr4d ⊢φ∧a∈V∧b∈V→F⁡aDF⁡b=0↔F⁡a=F⁡b
55 16 adantr ⊢φ∧a∈V∧b∈V∧c∈V→E∈∞Met⁡V
56 simpr ⊢φ∧a∈V∧b∈V∧c∈V→c∈V
57 17 adantr ⊢φ∧a∈V∧b∈V∧c∈V→a∈V
58 18 adantr ⊢φ∧a∈V∧b∈V∧c∈V→b∈V
59 xmettri2 ⊢E∈∞Met⁡V∧c∈V∧a∈V∧b∈V→aEb≤cEa+𝑒cEb
60 55 56 57 58 59 syl13anc ⊢φ∧a∈V∧b∈V∧c∈V→aEb≤cEa+𝑒cEb
61 19 adantr ⊢φ∧a∈V∧b∈V∧c∈V→F⁡aDF⁡b=aEb
62 12 adantr ⊢φ∧a∈V∧b∈V∧c∈V→U=F“𝑠R
63 13 adantr ⊢φ∧a∈V∧b∈V∧c∈V→V=BaseR
64 14 adantr ⊢φ∧a∈V∧b∈V∧c∈V→F:V⟶1-1 ontoB
65 15 adantr ⊢φ∧a∈V∧b∈V∧c∈V→R∈Z
66 62 63 64 65 5 6 55 56 57 imasdsf1o ⊢φ∧a∈V∧b∈V∧c∈V→F⁡cDF⁡a=cEa
67 62 63 64 65 5 6 55 56 58 imasdsf1o ⊢φ∧a∈V∧b∈V∧c∈V→F⁡cDF⁡b=cEb
68 66 67 oveq12d ⊢φ∧a∈V∧b∈V∧c∈V→F⁡cDF⁡a+𝑒F⁡cDF⁡b=cEa+𝑒cEb
69 60 61 68 3brtr4d ⊢φ∧a∈V∧b∈V∧c∈V→F⁡aDF⁡b≤F⁡cDF⁡a+𝑒F⁡cDF⁡b
70 69 ralrimiva ⊢φ∧a∈V∧b∈V→∀c∈VF⁡aDF⁡b≤F⁡cDF⁡a+𝑒F⁡cDF⁡b
71 oveq1 ⊢z=F⁡c→zDF⁡a=F⁡cDF⁡a
72 oveq1 ⊢z=F⁡c→zDF⁡b=F⁡cDF⁡b
73 71 72 oveq12d ⊢z=F⁡c→zDF⁡a+𝑒zDF⁡b=F⁡cDF⁡a+𝑒F⁡cDF⁡b
74 73 breq2d ⊢z=F⁡c→F⁡aDF⁡b≤zDF⁡a+𝑒zDF⁡b↔F⁡aDF⁡b≤F⁡cDF⁡a+𝑒F⁡cDF⁡b
75 74 ralrn ⊢FFnV→∀z∈ran⁡FF⁡aDF⁡b≤zDF⁡a+𝑒zDF⁡b↔∀c∈VF⁡aDF⁡b≤F⁡cDF⁡a+𝑒F⁡cDF⁡b
76 26 75 syl ⊢φ→∀z∈ran⁡FF⁡aDF⁡b≤zDF⁡a+𝑒zDF⁡b↔∀c∈VF⁡aDF⁡b≤F⁡cDF⁡a+𝑒F⁡cDF⁡b
77 32 raleqdv ⊢φ→∀z∈ran⁡FF⁡aDF⁡b≤zDF⁡a+𝑒zDF⁡b↔∀z∈BF⁡aDF⁡b≤zDF⁡a+𝑒zDF⁡b
78 76 77 bitr3d ⊢φ→∀c∈VF⁡aDF⁡b≤F⁡cDF⁡a+𝑒F⁡cDF⁡b↔∀z∈BF⁡aDF⁡b≤zDF⁡a+𝑒zDF⁡b
79 78 adantr ⊢φ∧a∈V∧b∈V→∀c∈VF⁡aDF⁡b≤F⁡cDF⁡a+𝑒F⁡cDF⁡b↔∀z∈BF⁡aDF⁡b≤zDF⁡a+𝑒zDF⁡b
80 70 79 mpbid ⊢φ∧a∈V∧b∈V→∀z∈BF⁡aDF⁡b≤zDF⁡a+𝑒zDF⁡b
81 54 80 jca ⊢φ∧a∈V∧b∈V→F⁡aDF⁡b=0↔F⁡a=F⁡b∧∀z∈BF⁡aDF⁡b≤zDF⁡a+𝑒zDF⁡b
82 81 ralrimivva ⊢φ→∀a∈V∀b∈VF⁡aDF⁡b=0↔F⁡a=F⁡b∧∀z∈BF⁡aDF⁡b≤zDF⁡a+𝑒zDF⁡b
83 27 eqeq1d ⊢y=F⁡b→F⁡aDy=0↔F⁡aDF⁡b=0
84 eqeq2 ⊢y=F⁡b→F⁡a=y↔F⁡a=F⁡b
85 83 84 bibi12d ⊢y=F⁡b→F⁡aDy=0↔F⁡a=y↔F⁡aDF⁡b=0↔F⁡a=F⁡b
86 oveq2 ⊢y=F⁡b→zDy=zDF⁡b
87 86 oveq2d ⊢y=F⁡b→zDF⁡a+𝑒zDy=zDF⁡a+𝑒zDF⁡b
88 27 87 breq12d ⊢y=F⁡b→F⁡aDy≤zDF⁡a+𝑒zDy↔F⁡aDF⁡b≤zDF⁡a+𝑒zDF⁡b
89 88 ralbidv ⊢y=F⁡b→∀z∈BF⁡aDy≤zDF⁡a+𝑒zDy↔∀z∈BF⁡aDF⁡b≤zDF⁡a+𝑒zDF⁡b
90 85 89 anbi12d ⊢y=F⁡b→F⁡aDy=0↔F⁡a=y∧∀z∈BF⁡aDy≤zDF⁡a+𝑒zDy↔F⁡aDF⁡b=0↔F⁡a=F⁡b∧∀z∈BF⁡aDF⁡b≤zDF⁡a+𝑒zDF⁡b
91 90 ralrn ⊢FFnV→∀y∈ran⁡FF⁡aDy=0↔F⁡a=y∧∀z∈BF⁡aDy≤zDF⁡a+𝑒zDy↔∀b∈VF⁡aDF⁡b=0↔F⁡a=F⁡b∧∀z∈BF⁡aDF⁡b≤zDF⁡a+𝑒zDF⁡b
92 26 91 syl ⊢φ→∀y∈ran⁡FF⁡aDy=0↔F⁡a=y∧∀z∈BF⁡aDy≤zDF⁡a+𝑒zDy↔∀b∈VF⁡aDF⁡b=0↔F⁡a=F⁡b∧∀z∈BF⁡aDF⁡b≤zDF⁡a+𝑒zDF⁡b
93 32 raleqdv ⊢φ→∀y∈ran⁡FF⁡aDy=0↔F⁡a=y∧∀z∈BF⁡aDy≤zDF⁡a+𝑒zDy↔∀y∈BF⁡aDy=0↔F⁡a=y∧∀z∈BF⁡aDy≤zDF⁡a+𝑒zDy
94 92 93 bitr3d ⊢φ→∀b∈VF⁡aDF⁡b=0↔F⁡a=F⁡b∧∀z∈BF⁡aDF⁡b≤zDF⁡a+𝑒zDF⁡b↔∀y∈BF⁡aDy=0↔F⁡a=y∧∀z∈BF⁡aDy≤zDF⁡a+𝑒zDy
95 94 ralbidv ⊢φ→∀a∈V∀b∈VF⁡aDF⁡b=0↔F⁡a=F⁡b∧∀z∈BF⁡aDF⁡b≤zDF⁡a+𝑒zDF⁡b↔∀a∈V∀y∈BF⁡aDy=0↔F⁡a=y∧∀z∈BF⁡aDy≤zDF⁡a+𝑒zDy
96 82 95 mpbid ⊢φ→∀a∈V∀y∈BF⁡aDy=0↔F⁡a=y∧∀z∈BF⁡aDy≤zDF⁡a+𝑒zDy
97 37 eqeq1d ⊢x=F⁡a→xDy=0↔F⁡aDy=0
98 eqeq1 ⊢x=F⁡a→x=y↔F⁡a=y
99 97 98 bibi12d ⊢x=F⁡a→xDy=0↔x=y↔F⁡aDy=0↔F⁡a=y
100 oveq2 ⊢x=F⁡a→zDx=zDF⁡a
101 100 oveq1d ⊢x=F⁡a→zDx+𝑒zDy=zDF⁡a+𝑒zDy
102 37 101 breq12d ⊢x=F⁡a→xDy≤zDx+𝑒zDy↔F⁡aDy≤zDF⁡a+𝑒zDy
103 102 ralbidv ⊢x=F⁡a→∀z∈BxDy≤zDx+𝑒zDy↔∀z∈BF⁡aDy≤zDF⁡a+𝑒zDy
104 99 103 anbi12d ⊢x=F⁡a→xDy=0↔x=y∧∀z∈BxDy≤zDx+𝑒zDy↔F⁡aDy=0↔F⁡a=y∧∀z∈BF⁡aDy≤zDF⁡a+𝑒zDy
105 104 ralbidv ⊢x=F⁡a→∀y∈BxDy=0↔x=y∧∀z∈BxDy≤zDx+𝑒zDy↔∀y∈BF⁡aDy=0↔F⁡a=y∧∀z∈BF⁡aDy≤zDF⁡a+𝑒zDy
106 105 ralrn ⊢FFnV→∀x∈ran⁡F∀y∈BxDy=0↔x=y∧∀z∈BxDy≤zDx+𝑒zDy↔∀a∈V∀y∈BF⁡aDy=0↔F⁡a=y∧∀z∈BF⁡aDy≤zDF⁡a+𝑒zDy
107 26 106 syl ⊢φ→∀x∈ran⁡F∀y∈BxDy=0↔x=y∧∀z∈BxDy≤zDx+𝑒zDy↔∀a∈V∀y∈BF⁡aDy=0↔F⁡a=y∧∀z∈BF⁡aDy≤zDF⁡a+𝑒zDy
108 32 raleqdv ⊢φ→∀x∈ran⁡F∀y∈BxDy=0↔x=y∧∀z∈BxDy≤zDx+𝑒zDy↔∀x∈B∀y∈BxDy=0↔x=y∧∀z∈BxDy≤zDx+𝑒zDy
109 107 108 bitr3d ⊢φ→∀a∈V∀y∈BF⁡aDy=0↔F⁡a=y∧∀z∈BF⁡aDy≤zDF⁡a+𝑒zDy↔∀x∈B∀y∈BxDy=0↔x=y∧∀z∈BxDy≤zDx+𝑒zDy
110 96 109 mpbid ⊢φ→∀x∈B∀y∈BxDy=0↔x=y∧∀z∈BxDy≤zDx+𝑒zDy
111 7 elfvexd ⊢φ→V∈V
112 focdmex ⊢V∈V→F:V⟶ontoB→B∈V
113 111 9 112 sylc ⊢φ→B∈V
114 isxmet ⊢B∈V→D∈∞Met⁡B↔D:B×B⟶ℝ*∧∀x∈B∀y∈BxDy=0↔x=y∧∀z∈BxDy≤zDx+𝑒zDy
115 113 114 syl ⊢φ→D∈∞Met⁡B↔D:B×B⟶ℝ*∧∀x∈B∀y∈BxDy=0↔x=y∧∀z∈BxDy≤zDx+𝑒zDy
116 46 110 115 mpbir2and ⊢φ→D∈∞Met⁡B