Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  pstmxmet Structured version   Unicode version

Theorem pstmxmet 24294
 Description: The metric induced by a pseudometric is a full-fledged metric on the equivalence classes of the metric identification. (Contributed by Thierry Arnoux, 11-Feb-2018.)
Hypothesis
Ref Expression
pstmval.1 ~Met
Assertion
Ref Expression
pstmxmet PsMet pstoMet

Proof of Theorem pstmxmet
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 2961 . . . . . . . . 9
2 vex 2961 . . . . . . . . 9
31, 2ab2rexex 6228 . . . . . . . 8
43uniex 4707 . . . . . . 7
54rgen2w 2776 . . . . . 6
6 eqid 2438 . . . . . . 7
76fnmpt2 6421 . . . . . 6
85, 7ax-mp 8 . . . . 5
9 pstmval.1 . . . . . . 7 ~Met
109pstmval 24292 . . . . . 6 PsMet pstoMet
1110fneq1d 5538 . . . . 5 PsMet pstoMet
128, 11mpbiri 226 . . . 4 PsMet pstoMet
13 simpllr 737 . . . . . . . . . 10 PsMet
14 simpr 449 . . . . . . . . . 10 PsMet
1513, 14oveq12d 6101 . . . . . . . . 9 PsMet pstoMet pstoMet
16 simp-5l 746 . . . . . . . . . 10 PsMet PsMet
17 simp-4r 745 . . . . . . . . . 10 PsMet
18 simplr 733 . . . . . . . . . 10 PsMet
199pstmfval 24293 . . . . . . . . . 10 PsMet pstoMet
2016, 17, 18, 19syl3anc 1185 . . . . . . . . 9 PsMet pstoMet
2115, 20eqtrd 2470 . . . . . . . 8 PsMet pstoMet
22 psmetf 18339 . . . . . . . . . 10 PsMet
2316, 22syl 16 . . . . . . . . 9 PsMet
2423, 17, 18fovrnd 6220 . . . . . . . 8 PsMet
2521, 24eqeltrd 2512 . . . . . . 7 PsMet pstoMet
26 elqsi 6960 . . . . . . . . 9
2726ad2antll 711 . . . . . . . 8 PsMet
2827ad2antrr 708 . . . . . . 7 PsMet
2925, 28r19.29a 2852 . . . . . 6 PsMet pstoMet
30 elqsi 6960 . . . . . . 7
3130ad2antrl 710 . . . . . 6 PsMet
3229, 31r19.29a 2852 . . . . 5 PsMet pstoMet
3332ralrimivva 2800 . . . 4 PsMet pstoMet
34 ffnov 6176 . . . 4 pstoMet pstoMet pstoMet
3512, 33, 34sylanbrc 647 . . 3 PsMet pstoMet
36 simpll 732 . . . . . . . . . . . . . . 15 PsMet PsMet
37 simplr 733 . . . . . . . . . . . . . . 15 PsMet
38 simpr 449 . . . . . . . . . . . . . . 15 PsMet
3936, 37, 38, 19syl3anc 1185 . . . . . . . . . . . . . 14 PsMet pstoMet
4039eqeq1d 2446 . . . . . . . . . . . . 13 PsMet pstoMet
419breqi 4220 . . . . . . . . . . . . . 14 ~Met
42 metidv 24289 . . . . . . . . . . . . . . 15 PsMet ~Met
4342anassrs 631 . . . . . . . . . . . . . 14 PsMet ~Met
4441, 43syl5bb 250 . . . . . . . . . . . . 13 PsMet
4540, 44bitr4d 249 . . . . . . . . . . . 12 PsMet pstoMet
46 metider 24291 . . . . . . . . . . . . . . 15 PsMet ~Met
4736, 46syl 16 . . . . . . . . . . . . . 14 PsMet ~Met
48 ereq1 6914 . . . . . . . . . . . . . . 15 ~Met ~Met
499, 48ax-mp 8 . . . . . . . . . . . . . 14 ~Met
5047, 49sylibr 205 . . . . . . . . . . . . 13 PsMet
5150, 37erth 6951 . . . . . . . . . . . 12 PsMet
5245, 51bitrd 246 . . . . . . . . . . 11 PsMet pstoMet
5352adantllr 701 . . . . . . . . . 10 PsMet pstoMet
5453adantlr 697 . . . . . . . . 9 PsMet pstoMet
5554adantr 453 . . . . . . . 8 PsMet pstoMet
5615eqeq1d 2446 . . . . . . . 8 PsMet pstoMet pstoMet
5713, 14eqeq12d 2452 . . . . . . . 8 PsMet
5855, 56, 573bitr4d 278 . . . . . . 7 PsMet pstoMet
5958, 28r19.29a 2852 . . . . . 6 PsMet pstoMet
6059, 31r19.29a 2852 . . . . 5 PsMet pstoMet
61 simp-6l 748 . . . . . . . . . . . . . . 15 PsMet PsMet
62 simplr 733 . . . . . . . . . . . . . . 15 PsMet
63 simp-6r 749 . . . . . . . . . . . . . . 15 PsMet
64 simp-4r 745 . . . . . . . . . . . . . . 15 PsMet
65 psmettri2 18342 . . . . . . . . . . . . . . 15 PsMet
6661, 62, 63, 64, 65syl13anc 1187 . . . . . . . . . . . . . 14 PsMet
67 simp-5r 747 . . . . . . . . . . . . . . . . 17 PsMet
68 simpllr 737 . . . . . . . . . . . . . . . . 17 PsMet
6967, 68oveq12d 6101 . . . . . . . . . . . . . . . 16 PsMet pstoMet pstoMet
7061, 63, 64, 39syl21anc 1184 . . . . . . . . . . . . . . . 16 PsMet pstoMet
7169, 70eqtrd 2470 . . . . . . . . . . . . . . 15 PsMet pstoMet
72 simpr 449 . . . . . . . . . . . . . . . . . 18 PsMet
7372, 67oveq12d 6101 . . . . . . . . . . . . . . . . 17 PsMet pstoMet pstoMet
749pstmfval 24293 . . . . . . . . . . . . . . . . . 18 PsMet pstoMet
7561, 62, 63, 74syl3anc 1185 . . . . . . . . . . . . . . . . 17 PsMet pstoMet
7673, 75eqtrd 2470 . . . . . . . . . . . . . . . 16 PsMet pstoMet
7772, 68oveq12d 6101 . . . . . . . . . . . . . . . . 17 PsMet pstoMet pstoMet
789pstmfval 24293 . . . . . . . . . . . . . . . . . 18 PsMet pstoMet
7961, 62, 64, 78syl3anc 1185 . . . . . . . . . . . . . . . . 17 PsMet pstoMet
8077, 79eqtrd 2470 . . . . . . . . . . . . . . . 16 PsMet pstoMet
8176, 80oveq12d 6101 . . . . . . . . . . . . . . 15 PsMet pstoMetpstoMet
8271, 81breq12d 4227 . . . . . . . . . . . . . 14 PsMet pstoMet pstoMetpstoMet
8366, 82mpbird 225 . . . . . . . . . . . . 13 PsMet pstoMet pstoMetpstoMet
8483adantl6r 23961 . . . . . . . . . . . 12 PsMet pstoMet pstoMetpstoMet
85 elqsi 6960 . . . . . . . . . . . . 13
8685ad5antlr 717 . . . . . . . . . . . 12 PsMet
8784, 86r19.29a 2852 . . . . . . . . . . 11 PsMet pstoMet pstoMetpstoMet
8887adantl5r 23960 . . . . . . . . . 10 PsMet pstoMet pstoMetpstoMet
8926ad4antlr 715 . . . . . . . . . 10 PsMet
9088, 89r19.29a 2852 . . . . . . . . 9 PsMet pstoMet pstoMetpstoMet
9190adantl4r 23959 . . . . . . . 8 PsMet pstoMet pstoMetpstoMet
9230ad3antlr 713 . . . . . . . 8 PsMet
9391, 92r19.29a 2852 . . . . . . 7 PsMet pstoMet pstoMetpstoMet
9493ralrimiva 2791 . . . . . 6 PsMet pstoMet pstoMetpstoMet
9594anasss 630 . . . . 5 PsMet pstoMet pstoMetpstoMet
9660, 95jca 520 . . . 4 PsMet pstoMet pstoMet pstoMetpstoMet
9796ralrimivva 2800 . . 3 PsMet pstoMet pstoMet pstoMetpstoMet
9835, 97jca 520 . 2 PsMet pstoMet pstoMet pstoMet pstoMetpstoMet
99 elfvex 5760 . . 3 PsMet
100 qsexg 6964 . . 3
101 isxmet 18356 . . 3 pstoMet pstoMet pstoMet pstoMet pstoMetpstoMet
10299, 100, 1013syl 19 . 2 PsMet pstoMet pstoMet pstoMet pstoMet pstoMetpstoMet
10398, 102mpbird 225 1 PsMet pstoMet
 Colors of variables: wff set class Syntax hints:   wi 4   wb 178   wa 360   wceq 1653   wcel 1726  cab 2424  wral 2707  wrex 2708  cvv 2958  cuni 4017   class class class wbr 4214   cxp 4878   wfn 5451  wf 5452  cfv 5456  (class class class)co 6083   cmpt2 6085   wer 6904  cec 6905  cqs 6906  cc0 8992  cxr 9121   cle 9123  cxad 10710  PsMetcpsmet 16687  cxmt 16688  ~Metcmetid 24283  pstoMetcpstm 24284 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-rep 4322  ax-sep 4332  ax-nul 4340  ax-pow 4379  ax-pr 4405  ax-un 4703  ax-cnex 9048  ax-resscn 9049  ax-1cn 9050  ax-icn 9051  ax-addcl 9052  ax-addrcl 9053  ax-mulcl 9054  ax-mulrcl 9055  ax-mulcom 9056  ax-addass 9057  ax-mulass 9058  ax-distr 9059  ax-i2m1 9060  ax-1ne0 9061  ax-1rid 9062  ax-rnegex 9063  ax-rrecex 9064  ax-cnre 9065  ax-pre-lttri 9066  ax-pre-lttrn 9067  ax-pre-ltadd 9068  ax-pre-mulgt0 9069 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2712  df-rex 2713  df-reu 2714  df-rmo 2715  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-iun 4097  df-br 4215  df-opab 4269  df-mpt 4270  df-id 4500  df-po 4505  df-so 4506  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-iota 5420  df-fun 5458  df-fn 5459  df-f 5460  df-f1 5461  df-fo 5462  df-f1o 5463  df-fv 5464  df-ov 6086  df-oprab 6087  df-mpt2 6088  df-1st 6351  df-2nd 6352  df-riota 6551  df-er 6907  df-ec 6909  df-qs 6913  df-map 7022  df-en 7112  df-dom 7113  df-sdom 7114  df-pnf 9124  df-mnf 9125  df-xr 9126  df-ltxr 9127  df-le 9128  df-sub 9295  df-neg 9296  df-div 9680  df-2 10060  df-rp 10615  df-xneg 10712  df-xadd 10713  df-xmul 10714  df-psmet 16696  df-xmet 16697  df-metid 24285  df-pstm 24286
 Copyright terms: Public domain W3C validator