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 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 )