Metamath Proof Explorer

Theorem iccvonmbllem

Description: Any n-dimensional closed interval is Lebesgue measurable. This is the second statement in Proposition 115G (c) of Fremlin1 p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses iccvonmbllem.x 
|- ( ph -> X e. Fin )
iccvonmbllem.s 
|- S = dom ( voln ` X )
iccvonmbllem.a 
|- ( ph -> A : X --> RR )
iccvonmbllem.b 
|- ( ph -> B : X --> RR )
iccvonmbllem.c 
|- C = ( n e. NN |-> ( i e. X |-> ( ( A ` i ) - ( 1 / n ) ) ) )
iccvonmbllem.d 
|- D = ( n e. NN |-> ( i e. X |-> ( ( B ` i ) + ( 1 / n ) ) ) )
Assertion iccvonmbllem 
|- ( ph -> X_ i e. X ( ( A ` i ) [,] ( B ` i ) ) e. S )

Proof

Step Hyp Ref Expression
1 iccvonmbllem.x 
 |-  ( ph -> X e. Fin )
2 iccvonmbllem.s 
 |-  S = dom ( voln ` X )
3 iccvonmbllem.a 
 |-  ( ph -> A : X --> RR )
4 iccvonmbllem.b 
 |-  ( ph -> B : X --> RR )
5 iccvonmbllem.c 
 |-  C = ( n e. NN |-> ( i e. X |-> ( ( A ` i ) - ( 1 / n ) ) ) )
6 iccvonmbllem.d 
 |-  D = ( n e. NN |-> ( i e. X |-> ( ( B ` i ) + ( 1 / n ) ) ) )
7 5 a1i 
 |-  ( ph -> C = ( n e. NN |-> ( i e. X |-> ( ( A ` i ) - ( 1 / n ) ) ) ) )
8 1 adantr 
 |-  ( ( ph /\ n e. NN ) -> X e. Fin )
9 8 mptexd 
 |-  ( ( ph /\ n e. NN ) -> ( i e. X |-> ( ( A ` i ) - ( 1 / n ) ) ) e. _V )
10 7 9 fvmpt2d 
 |-  ( ( ph /\ n e. NN ) -> ( C ` n ) = ( i e. X |-> ( ( A ` i ) - ( 1 / n ) ) ) )
11 3 ffvelrnda 
 |-  ( ( ph /\ i e. X ) -> ( A ` i ) e. RR )
12 11 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ i e. X ) -> ( A ` i ) e. RR )
13 nnrecre 
 |-  ( n e. NN -> ( 1 / n ) e. RR )
14 13 ad2antlr 
 |-  ( ( ( ph /\ n e. NN ) /\ i e. X ) -> ( 1 / n ) e. RR )
15 12 14 resubcld 
 |-  ( ( ( ph /\ n e. NN ) /\ i e. X ) -> ( ( A ` i ) - ( 1 / n ) ) e. RR )
16 10 15 fvmpt2d 
 |-  ( ( ( ph /\ n e. NN ) /\ i e. X ) -> ( ( C ` n ) ` i ) = ( ( A ` i ) - ( 1 / n ) ) )
17 16 an32s 
 |-  ( ( ( ph /\ i e. X ) /\ n e. NN ) -> ( ( C ` n ) ` i ) = ( ( A ` i ) - ( 1 / n ) ) )
18 6 a1i 
 |-  ( ph -> D = ( n e. NN |-> ( i e. X |-> ( ( B ` i ) + ( 1 / n ) ) ) ) )
19 8 mptexd 
 |-  ( ( ph /\ n e. NN ) -> ( i e. X |-> ( ( B ` i ) + ( 1 / n ) ) ) e. _V )
20 18 19 fvmpt2d 
 |-  ( ( ph /\ n e. NN ) -> ( D ` n ) = ( i e. X |-> ( ( B ` i ) + ( 1 / n ) ) ) )
21 4 ffvelrnda 
 |-  ( ( ph /\ i e. X ) -> ( B ` i ) e. RR )
22 21 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ i e. X ) -> ( B ` i ) e. RR )
23 22 14 readdcld 
 |-  ( ( ( ph /\ n e. NN ) /\ i e. X ) -> ( ( B ` i ) + ( 1 / n ) ) e. RR )
24 20 23 fvmpt2d 
 |-  ( ( ( ph /\ n e. NN ) /\ i e. X ) -> ( ( D ` n ) ` i ) = ( ( B ` i ) + ( 1 / n ) ) )
25 24 an32s 
 |-  ( ( ( ph /\ i e. X ) /\ n e. NN ) -> ( ( D ` n ) ` i ) = ( ( B ` i ) + ( 1 / n ) ) )
26 17 25 oveq12d 
 |-  ( ( ( ph /\ i e. X ) /\ n e. NN ) -> ( ( ( C ` n ) ` i ) (,) ( ( D ` n ) ` i ) ) = ( ( ( A ` i ) - ( 1 / n ) ) (,) ( ( B ` i ) + ( 1 / n ) ) ) )
27 26 iineq2dv 
 |-  ( ( ph /\ i e. X ) -> |^|_ n e. NN ( ( ( C ` n ) ` i ) (,) ( ( D ` n ) ` i ) ) = |^|_ n e. NN ( ( ( A ` i ) - ( 1 / n ) ) (,) ( ( B ` i ) + ( 1 / n ) ) ) )
28 11 21 iooiinicc 
 |-  ( ( ph /\ i e. X ) -> |^|_ n e. NN ( ( ( A ` i ) - ( 1 / n ) ) (,) ( ( B ` i ) + ( 1 / n ) ) ) = ( ( A ` i ) [,] ( B ` i ) ) )
29 27 28 eqtrd 
 |-  ( ( ph /\ i e. X ) -> |^|_ n e. NN ( ( ( C ` n ) ` i ) (,) ( ( D ` n ) ` i ) ) = ( ( A ` i ) [,] ( B ` i ) ) )
30 29 ixpeq2dva 
 |-  ( ph -> X_ i e. X |^|_ n e. NN ( ( ( C ` n ) ` i ) (,) ( ( D ` n ) ` i ) ) = X_ i e. X ( ( A ` i ) [,] ( B ` i ) ) )
31 30 eqcomd 
 |-  ( ph -> X_ i e. X ( ( A ` i ) [,] ( B ` i ) ) = X_ i e. X |^|_ n e. NN ( ( ( C ` n ) ` i ) (,) ( ( D ` n ) ` i ) ) )
32 eqidd 
 |-  ( ph -> X_ i e. X ( ( A ` i ) [,] ( B ` i ) ) = X_ i e. X ( ( A ` i ) [,] ( B ` i ) ) )
33 nnn0 
 |-  NN =/= (/)
34 33 a1i 
 |-  ( ph -> NN =/= (/) )
35 ixpiin 
 |-  ( NN =/= (/) -> X_ i e. X |^|_ n e. NN ( ( ( C ` n ) ` i ) (,) ( ( D ` n ) ` i ) ) = |^|_ n e. NN X_ i e. X ( ( ( C ` n ) ` i ) (,) ( ( D ` n ) ` i ) ) )
36 34 35 syl 
 |-  ( ph -> X_ i e. X |^|_ n e. NN ( ( ( C ` n ) ` i ) (,) ( ( D ` n ) ` i ) ) = |^|_ n e. NN X_ i e. X ( ( ( C ` n ) ` i ) (,) ( ( D ` n ) ` i ) ) )
37 31 32 36 3eqtr3d 
 |-  ( ph -> X_ i e. X ( ( A ` i ) [,] ( B ` i ) ) = |^|_ n e. NN X_ i e. X ( ( ( C ` n ) ` i ) (,) ( ( D ` n ) ` i ) ) )
38 1 2 dmovnsal 
 |-  ( ph -> S e. SAlg )
39 nnct 
 |-  NN ~<_ _om
40 39 a1i 
 |-  ( ph -> NN ~<_ _om )
41 15 fmpttd 
 |-  ( ( ph /\ n e. NN ) -> ( i e. X |-> ( ( A ` i ) - ( 1 / n ) ) ) : X --> RR )
42 ressxr 
 |-  RR C_ RR*
43 42 a1i 
 |-  ( ( ph /\ n e. NN ) -> RR C_ RR* )
44 41 43 fssd 
 |-  ( ( ph /\ n e. NN ) -> ( i e. X |-> ( ( A ` i ) - ( 1 / n ) ) ) : X --> RR* )
45 10 feq1d 
 |-  ( ( ph /\ n e. NN ) -> ( ( C ` n ) : X --> RR* <-> ( i e. X |-> ( ( A ` i ) - ( 1 / n ) ) ) : X --> RR* ) )
46 44 45 mpbird 
 |-  ( ( ph /\ n e. NN ) -> ( C ` n ) : X --> RR* )
47 23 fmpttd 
 |-  ( ( ph /\ n e. NN ) -> ( i e. X |-> ( ( B ` i ) + ( 1 / n ) ) ) : X --> RR )
48 47 43 fssd 
 |-  ( ( ph /\ n e. NN ) -> ( i e. X |-> ( ( B ` i ) + ( 1 / n ) ) ) : X --> RR* )
49 20 feq1d 
 |-  ( ( ph /\ n e. NN ) -> ( ( D ` n ) : X --> RR* <-> ( i e. X |-> ( ( B ` i ) + ( 1 / n ) ) ) : X --> RR* ) )
50 48 49 mpbird 
 |-  ( ( ph /\ n e. NN ) -> ( D ` n ) : X --> RR* )
51 8 2 46 50 ioovonmbl 
 |-  ( ( ph /\ n e. NN ) -> X_ i e. X ( ( ( C ` n ) ` i ) (,) ( ( D ` n ) ` i ) ) e. S )
52 38 40 34 51 saliincl 
 |-  ( ph -> |^|_ n e. NN X_ i e. X ( ( ( C ` n ) ` i ) (,) ( ( D ` n ) ` i ) ) e. S )
53 37 52 eqeltrd 
 |-  ( ph -> X_ i e. X ( ( A ` i ) [,] ( B ` i ) ) e. S )