Step |
Hyp |
Ref |
Expression |
1 |
|
difssd |
|- ( A e. dom vol -> ( RR \ A ) C_ RR ) |
2 |
|
elpwi |
|- ( x e. ~P RR -> x C_ RR ) |
3 |
|
inss1 |
|- ( x i^i A ) C_ x |
4 |
|
ovolsscl |
|- ( ( ( x i^i A ) C_ x /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i A ) ) e. RR ) |
5 |
3 4
|
mp3an1 |
|- ( ( x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i A ) ) e. RR ) |
6 |
5
|
3adant1 |
|- ( ( A e. dom vol /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i A ) ) e. RR ) |
7 |
6
|
recnd |
|- ( ( A e. dom vol /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i A ) ) e. CC ) |
8 |
|
difss |
|- ( x \ A ) C_ x |
9 |
|
ovolsscl |
|- ( ( ( x \ A ) C_ x /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x \ A ) ) e. RR ) |
10 |
8 9
|
mp3an1 |
|- ( ( x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x \ A ) ) e. RR ) |
11 |
10
|
3adant1 |
|- ( ( A e. dom vol /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x \ A ) ) e. RR ) |
12 |
11
|
recnd |
|- ( ( A e. dom vol /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x \ A ) ) e. CC ) |
13 |
7 12
|
addcomd |
|- ( ( A e. dom vol /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) = ( ( vol* ` ( x \ A ) ) + ( vol* ` ( x i^i A ) ) ) ) |
14 |
|
mblsplit |
|- ( ( A e. dom vol /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) ) |
15 |
|
indifcom |
|- ( RR i^i ( x \ A ) ) = ( x i^i ( RR \ A ) ) |
16 |
|
simp2 |
|- ( ( A e. dom vol /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> x C_ RR ) |
17 |
16
|
ssdifssd |
|- ( ( A e. dom vol /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( x \ A ) C_ RR ) |
18 |
|
sseqin2 |
|- ( ( x \ A ) C_ RR <-> ( RR i^i ( x \ A ) ) = ( x \ A ) ) |
19 |
17 18
|
sylib |
|- ( ( A e. dom vol /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( RR i^i ( x \ A ) ) = ( x \ A ) ) |
20 |
15 19
|
eqtr3id |
|- ( ( A e. dom vol /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( x i^i ( RR \ A ) ) = ( x \ A ) ) |
21 |
20
|
fveq2d |
|- ( ( A e. dom vol /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i ( RR \ A ) ) ) = ( vol* ` ( x \ A ) ) ) |
22 |
|
difin |
|- ( x \ ( x i^i ( RR \ A ) ) ) = ( x \ ( RR \ A ) ) |
23 |
20
|
difeq2d |
|- ( ( A e. dom vol /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( x \ ( x i^i ( RR \ A ) ) ) = ( x \ ( x \ A ) ) ) |
24 |
22 23
|
eqtr3id |
|- ( ( A e. dom vol /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( x \ ( RR \ A ) ) = ( x \ ( x \ A ) ) ) |
25 |
|
dfin4 |
|- ( x i^i A ) = ( x \ ( x \ A ) ) |
26 |
24 25
|
eqtr4di |
|- ( ( A e. dom vol /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( x \ ( RR \ A ) ) = ( x i^i A ) ) |
27 |
26
|
fveq2d |
|- ( ( A e. dom vol /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x \ ( RR \ A ) ) ) = ( vol* ` ( x i^i A ) ) ) |
28 |
21 27
|
oveq12d |
|- ( ( A e. dom vol /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( ( vol* ` ( x i^i ( RR \ A ) ) ) + ( vol* ` ( x \ ( RR \ A ) ) ) ) = ( ( vol* ` ( x \ A ) ) + ( vol* ` ( x i^i A ) ) ) ) |
29 |
13 14 28
|
3eqtr4d |
|- ( ( A e. dom vol /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` x ) = ( ( vol* ` ( x i^i ( RR \ A ) ) ) + ( vol* ` ( x \ ( RR \ A ) ) ) ) ) |
30 |
29
|
3expia |
|- ( ( A e. dom vol /\ x C_ RR ) -> ( ( vol* ` x ) e. RR -> ( vol* ` x ) = ( ( vol* ` ( x i^i ( RR \ A ) ) ) + ( vol* ` ( x \ ( RR \ A ) ) ) ) ) ) |
31 |
2 30
|
sylan2 |
|- ( ( A e. dom vol /\ x e. ~P RR ) -> ( ( vol* ` x ) e. RR -> ( vol* ` x ) = ( ( vol* ` ( x i^i ( RR \ A ) ) ) + ( vol* ` ( x \ ( RR \ A ) ) ) ) ) ) |
32 |
31
|
ralrimiva |
|- ( A e. dom vol -> A. x e. ~P RR ( ( vol* ` x ) e. RR -> ( vol* ` x ) = ( ( vol* ` ( x i^i ( RR \ A ) ) ) + ( vol* ` ( x \ ( RR \ A ) ) ) ) ) ) |
33 |
|
ismbl |
|- ( ( RR \ A ) e. dom vol <-> ( ( RR \ A ) C_ RR /\ A. x e. ~P RR ( ( vol* ` x ) e. RR -> ( vol* ` x ) = ( ( vol* ` ( x i^i ( RR \ A ) ) ) + ( vol* ` ( x \ ( RR \ A ) ) ) ) ) ) ) |
34 |
1 32 33
|
sylanbrc |
|- ( A e. dom vol -> ( RR \ A ) e. dom vol ) |