Metamath Proof Explorer

Theorem hoimbllem

Description: Any n-dimensional half-open interval is Lebesgue measurable. This is a substep of Proposition 115G (a) of Fremlin1 p. 32. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses hoimbllem.x 
|- ( ph -> X e. Fin )
hoimbllem.n 
|- ( ph -> X =/= (/) )
hoimbllem.s 
|- S = dom ( voln ` X )
hoimbllem.a 
|- ( ph -> A : X --> RR )
hoimbllem.b 
|- ( ph -> B : X --> RR )
hoimbllem.h 
|- H = ( x e. Fin |-> ( l e. x , y e. RR |-> X_ i e. x if ( i = l , ( -oo (,) y ) , RR ) ) )
Assertion hoimbllem 
|- ( ph -> X_ i e. X ( ( A ` i ) [,) ( B ` i ) ) e. S )

Proof

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 ffvelcdmd 
 |-  ( ( 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 ffvelcdmda 
 |-  ( ( 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 )