Step |
Hyp |
Ref |
Expression |
1 |
|
hoimbllem.x |
|- ( ph -> X e. Fin ) |
2 |
|
hoimbllem.n |
|- ( ph -> X =/= (/) ) |
3 |
|
hoimbllem.s |
|- S = dom ( voln ` X ) |
4 |
|
hoimbllem.a |
|- ( ph -> A : X --> RR ) |
5 |
|
hoimbllem.b |
|- ( ph -> B : X --> RR ) |
6 |
|
hoimbllem.h |
|- H = ( x e. Fin |-> ( l e. x , y e. RR |-> X_ i e. x if ( i = l , ( -oo (,) y ) , RR ) ) ) |
7 |
1 2 4 5 6
|
hspdifhsp |
|- ( ph -> X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) = |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) ) |
8 |
1
|
vonmea |
|- ( ph -> ( voln ` X ) e. Meas ) |
9 |
8 3
|
dmmeasal |
|- ( ph -> S e. SAlg ) |
10 |
|
fict |
|- ( X e. Fin -> X ~<_ _om ) |
11 |
1 10
|
syl |
|- ( ph -> X ~<_ _om ) |
12 |
9
|
adantr |
|- ( ( ph /\ i e. X ) -> S e. SAlg ) |
13 |
1
|
adantr |
|- ( ( ph /\ i e. X ) -> X e. Fin ) |
14 |
|
simpr |
|- ( ( ph /\ i e. X ) -> i e. X ) |
15 |
5
|
adantr |
|- ( ( ph /\ i e. X ) -> B : X --> RR ) |
16 |
15 14
|
ffvelrnd |
|- ( ( ph /\ i e. X ) -> ( B ` i ) e. RR ) |
17 |
6 13 14 16
|
hspmbl |
|- ( ( ph /\ i e. X ) -> ( i ( H ` X ) ( B ` i ) ) e. dom ( voln ` X ) ) |
18 |
3
|
eqcomi |
|- dom ( voln ` X ) = S |
19 |
18
|
a1i |
|- ( ( ph /\ i e. X ) -> dom ( voln ` X ) = S ) |
20 |
17 19
|
eleqtrd |
|- ( ( ph /\ i e. X ) -> ( i ( H ` X ) ( B ` i ) ) e. S ) |
21 |
4
|
ffvelrnda |
|- ( ( ph /\ i e. X ) -> ( A ` i ) e. RR ) |
22 |
6 13 14 21
|
hspmbl |
|- ( ( ph /\ i e. X ) -> ( i ( H ` X ) ( A ` i ) ) e. dom ( voln ` X ) ) |
23 |
22 19
|
eleqtrd |
|- ( ( ph /\ i e. X ) -> ( i ( H ` X ) ( A ` i ) ) e. S ) |
24 |
|
saldifcl2 |
|- ( ( S e. SAlg /\ ( i ( H ` X ) ( B ` i ) ) e. S /\ ( i ( H ` X ) ( A ` i ) ) e. S ) -> ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) e. S ) |
25 |
12 20 23 24
|
syl3anc |
|- ( ( ph /\ i e. X ) -> ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) e. S ) |
26 |
9 11 2 25
|
saliincl |
|- ( ph -> |^|_ i e. X ( ( i ( H ` X ) ( B ` i ) ) \ ( i ( H ` X ) ( A ` i ) ) ) e. S ) |
27 |
7 26
|
eqeltrd |
|- ( ph -> X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) e. S ) |