Metamath Proof Explorer


Theorem ismbl2

Description: From ovolun , it suffices to show that the measure of x is at least the sum of the measures of x i^i A and x \ A . (Contributed by Mario Carneiro, 15-Jun-2014)

Ref Expression
Assertion ismbl2 AdomvolAx𝒫vol*xvol*xA+vol*xAvol*x

Proof

Step Hyp Ref Expression
1 ismbl AdomvolAx𝒫vol*xvol*x=vol*xA+vol*xA
2 elpwi x𝒫x
3 inundif xAxA=x
4 3 fveq2i vol*xAxA=vol*x
5 inss1 xAx
6 simprl Axvol*xx
7 5 6 sstrid Axvol*xxA
8 ovolsscl xAxxvol*xvol*xA
9 5 8 mp3an1 xvol*xvol*xA
10 9 adantl Axvol*xvol*xA
11 difss xAx
12 11 6 sstrid Axvol*xxA
13 ovolsscl xAxxvol*xvol*xA
14 11 13 mp3an1 xvol*xvol*xA
15 14 adantl Axvol*xvol*xA
16 ovolun xAvol*xAxAvol*xAvol*xAxAvol*xA+vol*xA
17 7 10 12 15 16 syl22anc Axvol*xvol*xAxAvol*xA+vol*xA
18 4 17 eqbrtrrid Axvol*xvol*xvol*xA+vol*xA
19 simprr Axvol*xvol*x
20 10 15 readdcld Axvol*xvol*xA+vol*xA
21 19 20 letri3d Axvol*xvol*x=vol*xA+vol*xAvol*xvol*xA+vol*xAvol*xA+vol*xAvol*x
22 18 21 mpbirand Axvol*xvol*x=vol*xA+vol*xAvol*xA+vol*xAvol*x
23 22 expr Axvol*xvol*x=vol*xA+vol*xAvol*xA+vol*xAvol*x
24 23 pm5.74d Axvol*xvol*x=vol*xA+vol*xAvol*xvol*xA+vol*xAvol*x
25 2 24 sylan2 Ax𝒫vol*xvol*x=vol*xA+vol*xAvol*xvol*xA+vol*xAvol*x
26 25 ralbidva Ax𝒫vol*xvol*x=vol*xA+vol*xAx𝒫vol*xvol*xA+vol*xAvol*x
27 26 pm5.32i Ax𝒫vol*xvol*x=vol*xA+vol*xAAx𝒫vol*xvol*xA+vol*xAvol*x
28 1 27 bitri AdomvolAx𝒫vol*xvol*xA+vol*xAvol*x