Metamath Proof Explorer


Theorem pmeasmono

Description: This theorem's hypotheses define a pre-measure. A pre-measure is monotone. (Contributed by Thierry Arnoux, 19-Jul-2020)

Ref Expression
Hypotheses caraext.1 φP:R0+∞
caraext.2 φP=0
caraext.3 φxωxRDisjyxyPx=*yxPy
pmeasmono.1 φAR
pmeasmono.2 φBR
pmeasmono.3 φBAR
pmeasmono.4 φAB
Assertion pmeasmono φPAPB

Proof

Step Hyp Ref Expression
1 caraext.1 φP:R0+∞
2 caraext.2 φP=0
3 caraext.3 φxωxRDisjyxyPx=*yxPy
4 pmeasmono.1 φAR
5 pmeasmono.2 φBR
6 pmeasmono.3 φBAR
7 pmeasmono.4 φAB
8 eqimss A=BAABA
9 ssdifeq0 ABAA=
10 8 9 sylib A=BAA=
11 10 fveq2d A=BAPA=P
12 11 adantl φA=BAPA=P
13 2 adantr φA=BAP=0
14 12 13 eqtrd φA=BAPA=0
15 1 5 ffvelrnd φPB0+∞
16 elxrge0 PB0+∞PB*0PB
17 16 simprbi PB0+∞0PB
18 15 17 syl φ0PB
19 18 adantr φA=BA0PB
20 14 19 eqbrtrd φA=BAPAPB
21 iccssxr 0+∞*
22 1 adantr φABAP:R0+∞
23 4 adantr φABAAR
24 22 23 ffvelrnd φABAPA0+∞
25 21 24 sselid φABAPA*
26 6 adantr φABABAR
27 22 26 ffvelrnd φABAPBA0+∞
28 xrge0addge PA*PBA0+∞PAPA+𝑒PBA
29 25 27 28 syl2anc φABAPAPA+𝑒PBA
30 prct ARBARABAω
31 4 6 30 syl2anc φABAω
32 31 adantr φABAABAω
33 prssi ARBARABAR
34 4 6 33 syl2anc φABAR
35 34 adantr φABAABAR
36 disjdif ABA=
37 simpr φABAABA
38 id y=Ay=A
39 id y=BAy=BA
40 38 39 disjprg ARBARABADisjyABAyABA=
41 23 26 37 40 syl3anc φABADisjyABAyABA=
42 36 41 mpbiri φABADisjyABAy
43 32 35 42 3jca φABAABAωABARDisjyABAy
44 prex ABAV
45 biidd x=ABAφφ
46 breq1 x=ABAxωABAω
47 sseq1 x=ABAxRABAR
48 disjeq1 x=ABADisjyxyDisjyABAy
49 46 47 48 3anbi123d x=ABAxωxRDisjyxyABAωABARDisjyABAy
50 45 49 anbi12d x=ABAφxωxRDisjyxyφABAωABARDisjyABAy
51 unieq x=ABAx=ABA
52 51 fveq2d x=ABAPx=PABA
53 esumeq1 x=ABA*yxPy=*yABAPy
54 52 53 eqeq12d x=ABAPx=*yxPyPABA=*yABAPy
55 50 54 imbi12d x=ABAφxωxRDisjyxyPx=*yxPyφABAωABARDisjyABAyPABA=*yABAPy
56 55 3 vtoclg ABAVφABAωABARDisjyABAyPABA=*yABAPy
57 44 56 ax-mp φABAωABARDisjyABAyPABA=*yABAPy
58 57 adantlr φABAABAωABARDisjyABAyPABA=*yABAPy
59 43 58 mpdan φABAPABA=*yABAPy
60 uniprg ARBARABA=ABA
61 4 6 60 syl2anc φABA=ABA
62 undif ABABA=B
63 7 62 sylib φABA=B
64 61 63 eqtrd φABA=B
65 64 adantr φABAABA=B
66 65 fveq2d φABAPABA=PB
67 simpr φABAy=Ay=A
68 67 fveq2d φABAy=APy=PA
69 simpr φABAy=BAy=BA
70 69 fveq2d φABAy=BAPy=PBA
71 68 70 23 26 24 27 37 esumpr φABA*yABAPy=PA+𝑒PBA
72 59 66 71 3eqtr3d φABAPB=PA+𝑒PBA
73 29 72 breqtrrd φABAPAPB
74 20 73 pm2.61dane φPAPB