Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  prdsxmetlem Structured version   Visualization version   Unicode version

Theorem prdsxmetlem 21395
 Description: The product metric is an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.)
Hypotheses
Ref Expression
prdsdsf.y s
prdsdsf.b
prdsdsf.v
prdsdsf.e
prdsdsf.d
prdsdsf.s
prdsdsf.i
prdsdsf.r
prdsdsf.m
Assertion
Ref Expression
prdsxmetlem
Distinct variable groups:   ,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()   ()   ()   ()   ()   ()

Proof of Theorem prdsxmetlem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prdsdsf.b . . . 4
2 fvex 5880 . . . 4
31, 2eqeltri 2527 . . 3
43a1i 11 . 2
5 prdsdsf.y . . . 4 s
6 prdsdsf.v . . . 4
7 prdsdsf.e . . . 4
8 prdsdsf.d . . . 4
9 prdsdsf.s . . . 4
10 prdsdsf.i . . . 4
11 prdsdsf.r . . . 4
12 prdsdsf.m . . . 4
135, 1, 6, 7, 8, 9, 10, 11, 12prdsdsf 21394 . . 3
14 iccssxr 11724 . . 3
15 fss 5742 . . 3
1613, 14, 15sylancl 669 . 2
1713fovrnda 6445 . . 3
18 elxrge0 11748 . . . 4
1918simprbi 466 . . 3
2017, 19syl 17 . 2
219adantr 467 . . . . 5
2210adantr 467 . . . . 5
2311ralrimiva 2804 . . . . . 6
2423adantr 467 . . . . 5
25 simprl 765 . . . . 5
26 simprr 767 . . . . 5
275, 1, 21, 22, 24, 25, 26, 6, 7, 8prdsdsval3 15395 . . . 4
2827breq1d 4415 . . 3
2912adantlr 722 . . . . . . . 8
305, 1, 21, 22, 24, 6, 25prdsbascl 15393 . . . . . . . . 9
3130r19.21bi 2759 . . . . . . . 8
325, 1, 21, 22, 24, 6, 26prdsbascl 15393 . . . . . . . . 9
3332r19.21bi 2759 . . . . . . . 8
34 xmetcl 21358 . . . . . . . 8
3529, 31, 33, 34syl3anc 1269 . . . . . . 7
36 eqid 2453 . . . . . . 7
3735, 36fmptd 6051 . . . . . 6
38 frn 5740 . . . . . 6
3937, 38syl 17 . . . . 5
40 0xr 9692 . . . . . . 7
4140a1i 11 . . . . . 6
4241snssd 4120 . . . . 5
4339, 42unssd 3612 . . . 4
44 supxrleub 11619 . . . 4
4543, 40, 44sylancl 669 . . 3
46 0le0 10706 . . . . . . 7
47 c0ex 9642 . . . . . . . 8
48 breq1 4408 . . . . . . . 8
4947, 48ralsn 4012 . . . . . . 7
5046, 49mpbir 213 . . . . . 6
51 ralunb 3617 . . . . . 6
5250, 51mpbiran2 931 . . . . 5
53 ovex 6323 . . . . . . 7
5453rgenw 2751 . . . . . 6
55 breq1 4408 . . . . . . 7
5636, 55ralrnmpt 6036 . . . . . 6
5754, 56ax-mp 5 . . . . 5
5852, 57bitri 253 . . . 4
59 xmetge0 21371 . . . . . . . . 9
6029, 31, 33, 59syl3anc 1269 . . . . . . . 8
6160biantrud 510 . . . . . . 7
62 xrletri3 11458 . . . . . . . 8
6335, 40, 62sylancl 669 . . . . . . 7
64 xmeteq0 21365 . . . . . . . 8
6529, 31, 33, 64syl3anc 1269 . . . . . . 7
6661, 63, 653bitr2d 285 . . . . . 6
6766ralbidva 2826 . . . . 5
68 eqid 2453 . . . . . . . . . 10
6968fnmpt 5709 . . . . . . . . 9
7023, 69syl 17 . . . . . . . 8
7170adantr 467 . . . . . . 7
725, 1, 21, 22, 71, 25prdsbasfn 15381 . . . . . 6
735, 1, 21, 22, 71, 26prdsbasfn 15381 . . . . . 6
74 eqfnfv 5981 . . . . . 6
7572, 73, 74syl2anc 667 . . . . 5
7667, 75bitr4d 260 . . . 4
7758, 76syl5bb 261 . . 3
7828, 45, 773bitrd 283 . 2
79273adantr3 1170 . . . 4
81123ad2antl1 1171 . . . . . . . . . 10
82303adantr3 1170 . . . . . . . . . . . 12
83823adant3 1029 . . . . . . . . . . 11
8483r19.21bi 2759 . . . . . . . . . 10
85323adantr3 1170 . . . . . . . . . . . 12
86853adant3 1029 . . . . . . . . . . 11
8786r19.21bi 2759 . . . . . . . . . 10
8881, 84, 87, 34syl3anc 1269 . . . . . . . . 9
8993ad2ant1 1030 . . . . . . . . . . . . . 14
90103ad2ant1 1030 . . . . . . . . . . . . . 14
91233ad2ant1 1030 . . . . . . . . . . . . . 14
92 simp23 1044 . . . . . . . . . . . . . 14
935, 1, 89, 90, 91, 6, 92prdsbascl 15393 . . . . . . . . . . . . 13
9493r19.21bi 2759 . . . . . . . . . . . 12
95 xmetcl 21358 . . . . . . . . . . . 12
9681, 94, 84, 95syl3anc 1269 . . . . . . . . . . 11
97 simp3l 1037 . . . . . . . . . . . 12
9897adantr 467 . . . . . . . . . . 11
99 xmetge0 21371 . . . . . . . . . . . 12
10081, 94, 84, 99syl3anc 1269 . . . . . . . . . . 11
101 eqid 2453 . . . . . . . . . . . . . . . . 17
10296, 101fmptd 6051 . . . . . . . . . . . . . . . 16
103 frn 5740 . . . . . . . . . . . . . . . 16
104102, 103syl 17 . . . . . . . . . . . . . . 15
10540a1i 11 . . . . . . . . . . . . . . . 16
106105snssd 4120 . . . . . . . . . . . . . . 15
107104, 106unssd 3612 . . . . . . . . . . . . . 14
108107adantr 467 . . . . . . . . . . . . 13
109 ssun1 3599 . . . . . . . . . . . . . 14
110 ovex 6323 . . . . . . . . . . . . . . . . 17
111110elabrex 6153 . . . . . . . . . . . . . . . 16
112111adantl 468 . . . . . . . . . . . . . . 15
113101rnmpt 5083 . . . . . . . . . . . . . . 15
114112, 113syl6eleqr 2542 . . . . . . . . . . . . . 14
115109, 114sseldi 3432 . . . . . . . . . . . . 13
116 supxrub 11617 . . . . . . . . . . . . 13
117108, 115, 116syl2anc 667 . . . . . . . . . . . 12
118 simp21 1042 . . . . . . . . . . . . . 14
1195, 1, 89, 90, 91, 92, 118, 6, 7, 8prdsdsval3 15395 . . . . . . . . . . . . 13
120119adantr 467 . . . . . . . . . . . 12
121117, 120breqtrrd 4432 . . . . . . . . . . 11
122 xrrege0 11476 . . . . . . . . . . 11
12396, 98, 100, 121, 122syl22anc 1270 . . . . . . . . . 10
124 xmetcl 21358 . . . . . . . . . . . 12
12581, 94, 87, 124syl3anc 1269 . . . . . . . . . . 11
126 simp3r 1038 . . . . . . . . . . . 12
127126adantr 467 . . . . . . . . . . 11
128 xmetge0 21371 . . . . . . . . . . . 12
12981, 94, 87, 128syl3anc 1269 . . . . . . . . . . 11
130 eqid 2453 . . . . . . . . . . . . . . . . 17
131125, 130fmptd 6051 . . . . . . . . . . . . . . . 16
132 frn 5740 . . . . . . . . . . . . . . . 16
133131, 132syl 17 . . . . . . . . . . . . . . 15
134133, 106unssd 3612 . . . . . . . . . . . . . 14
135134adantr 467 . . . . . . . . . . . . 13
136 ssun1 3599 . . . . . . . . . . . . . 14
137 ovex 6323 . . . . . . . . . . . . . . . . 17
138137elabrex 6153 . . . . . . . . . . . . . . . 16
139138adantl 468 . . . . . . . . . . . . . . 15
140130rnmpt 5083 . . . . . . . . . . . . . . 15
141139, 140syl6eleqr 2542 . . . . . . . . . . . . . 14
142136, 141sseldi 3432 . . . . . . . . . . . . 13
143 supxrub 11617 . . . . . . . . . . . . 13
144135, 142, 143syl2anc 667 . . . . . . . . . . . 12
145 simp22 1043 . . . . . . . . . . . . . 14
1465, 1, 89, 90, 91, 92, 145, 6, 7, 8prdsdsval3 15395 . . . . . . . . . . . . 13
147146adantr 467 . . . . . . . . . . . 12
148144, 147breqtrrd 4432 . . . . . . . . . . 11
149 xrrege0 11476 . . . . . . . . . . 11
150125, 127, 129, 148, 149syl22anc 1270 . . . . . . . . . 10
151123, 150readdcld 9675 . . . . . . . . 9
15281, 84, 87, 59syl3anc 1269 . . . . . . . . 9
153 xmettri2 21367 . . . . . . . . . . 11
15481, 94, 84, 87, 153syl13anc 1271 . . . . . . . . . 10
155 rexadd 11532 . . . . . . . . . . 11
156123, 150, 155syl2anc 667 . . . . . . . . . 10
157154, 156breqtrd 4430 . . . . . . . . 9
158 xrrege0 11476 . . . . . . . . 9
15988, 151, 152, 157, 158syl22anc 1270 . . . . . . . 8
160 readdcl 9627 . . . . . . . . . 10
1611603ad2ant3 1032 . . . . . . . . 9
162161adantr 467 . . . . . . . 8
163123, 150, 98, 127, 121, 148le2addd 10239 . . . . . . . 8
164159, 151, 162, 157, 163letrd 9797 . . . . . . 7
165164ralrimiva 2804 . . . . . 6
16688ralrimiva 2804 . . . . . . 7
167 breq1 4408 . . . . . . . 8
16836, 167ralrnmpt 6036 . . . . . . 7
169166, 168syl 17 . . . . . 6
170165, 169mpbird 236 . . . . 5
171133ad2ant1 1030 . . . . . . . . 9
172171, 92, 118fovrnd 6446 . . . . . . . 8
173 elxrge0 11748 . . . . . . . . 9
174173simprbi 466 . . . . . . . 8
175172, 174syl 17 . . . . . . 7
176171, 92, 145fovrnd 6446 . . . . . . . 8
177 elxrge0 11748 . . . . . . . . 9
178177simprbi 466 . . . . . . . 8
179176, 178syl 17 . . . . . . 7
18097, 126, 175, 179addge0d 10196 . . . . . 6
181 breq1 4408 . . . . . . 7
18247, 181ralsn 4012 . . . . . 6
183180, 182sylibr 216 . . . . 5
184 ralunb 3617 . . . . 5
185170, 183, 184sylanbrc 671 . . . 4
186433adantr3 1170 . . . . . 6
1871863adant3 1029 . . . . 5
188161rexrd 9695 . . . . 5
189 supxrleub 11619 . . . . 5
190187, 188, 189syl2anc 667 . . . 4
191185, 190mpbird 236 . . 3
19280, 191eqbrtrd 4426 . 2
1934, 16, 20, 78, 192isxmet2d 21354 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188   wa 371   w3a 986   wceq 1446   wcel 1889  cab 2439  wral 2739  wrex 2740  cvv 3047   cun 3404   wss 3406  csn 3970   class class class wbr 4405   cmpt 4464   cxp 4835   crn 4838   cres 4839   wfn 5580  wf 5581  cfv 5585  (class class class)co 6295  csup 7959  cr 9543  cc0 9544   caddc 9547   cpnf 9677  cxr 9679   clt 9680   cle 9681  cxad 11414  cicc 11645  cbs 15133  cds 15211  scprds 15356  cxmt 18967 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-rep 4518  ax-sep 4528  ax-nul 4537  ax-pow 4584  ax-pr 4642  ax-un 6588  ax-cnex 9600  ax-resscn 9601  ax-1cn 9602  ax-icn 9603  ax-addcl 9604  ax-addrcl 9605  ax-mulcl 9606  ax-mulrcl 9607  ax-mulcom 9608  ax-addass 9609  ax-mulass 9610  ax-distr 9611  ax-i2m1 9612  ax-1ne0 9613  ax-1rid 9614  ax-rnegex 9615  ax-rrecex 9616  ax-cnre 9617  ax-pre-lttri 9618  ax-pre-lttrn 9619  ax-pre-ltadd 9620  ax-pre-mulgt0 9621  ax-pre-sup 9622 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 987  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-nel 2627  df-ral 2744  df-rex 2745  df-reu 2746  df-rmo 2747  df-rab 2748  df-v 3049  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-pss 3422  df-nul 3734  df-if 3884  df-pw 3955  df-sn 3971  df-pr 3973  df-tp 3975  df-op 3977  df-uni 4202  df-int 4238  df-iun 4283  df-br 4406  df-opab 4465  df-mpt 4466  df-tr 4501  df-eprel 4748  df-id 4752  df-po 4758  df-so 4759  df-fr 4796  df-we 4798  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-pred 5383  df-ord 5429  df-on 5430  df-lim 5431  df-suc 5432  df-iota 5549  df-fun 5587  df-fn 5588  df-f 5589  df-f1 5590  df-fo 5591  df-f1o 5592  df-fv 5593  df-riota 6257  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-om 6698  df-1st 6798  df-2nd 6799  df-wrecs 7033  df-recs 7095  df-rdg 7133  df-1o 7187  df-oadd 7191  df-er 7368  df-map 7479  df-ixp 7528  df-en 7575  df-dom 7576  df-sdom 7577  df-fin 7578  df-sup 7961  df-pnf 9682  df-mnf 9683  df-xr 9684  df-ltxr 9685  df-le 9686  df-sub 9867  df-neg 9868  df-div 10277  df-nn 10617  df-2 10675  df-3 10676  df-4 10677  df-5 10678  df-6 10679  df-7 10680  df-8 10681  df-9 10682  df-10 10683  df-n0 10877  df-z 10945  df-dec 11059  df-uz 11167  df-rp 11310  df-xneg 11416  df-xadd 11417  df-xmul 11418  df-icc 11649  df-fz 11792  df-struct 15135  df-ndx 15136  df-slot 15137  df-base 15138  df-plusg 15215  df-mulr 15216  df-sca 15218  df-vsca 15219  df-ip 15220  df-tset 15221  df-ple 15222  df-ds 15224  df-hom 15226  df-cco 15227  df-prds 15358  df-xmet 18975 This theorem is referenced by:  prdsxmet  21396
 Copyright terms: Public domain W3C validator