Metamath Proof Explorer

Theorem vonhoire

Description: The Lebesgue measure of a n-dimensional half-open interval is a real number. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses vonhoire.n 
|- F/ k ph
vonhoire.x 
|- ( ph -> X e. Fin )
vonhoire.a 
|- ( ( ph /\ k e. X ) -> A e. RR )
vonhoire.b 
|- ( ( ph /\ k e. X ) -> B e. RR )
Assertion vonhoire 
|- ( ph -> ( ( voln ` X ) ` X_ k e. X ( A [,) B ) ) e. RR )

Proof

Step Hyp Ref Expression
1 vonhoire.n 
 |-  F/ k ph
2 vonhoire.x 
 |-  ( ph -> X e. Fin )
3 vonhoire.a 
 |-  ( ( ph /\ k e. X ) -> A e. RR )
4 vonhoire.b 
 |-  ( ( ph /\ k e. X ) -> B e. RR )
5 fveq2 
 |-  ( X = (/) -> ( voln ` X ) = ( voln ` (/) ) )
6 5 fveq1d 
 |-  ( X = (/) -> ( ( voln ` X ) ` X_ k e. X ( A [,) B ) ) = ( ( voln ` (/) ) ` X_ k e. X ( A [,) B ) ) )
7 6 adantl 
 |-  ( ( ph /\ X = (/) ) -> ( ( voln ` X ) ` X_ k e. X ( A [,) B ) ) = ( ( voln ` (/) ) ` X_ k e. X ( A [,) B ) ) )
8 ixpeq1 
 |-  ( X = (/) -> X_ k e. X ( A [,) B ) = X_ k e. (/) ( A [,) B ) )
9 8 adantl 
 |-  ( ( ph /\ X = (/) ) -> X_ k e. X ( A [,) B ) = X_ k e. (/) ( A [,) B ) )
10 0fin 
 |-  (/) e. Fin
11 10 a1i 
 |-  ( ph -> (/) e. Fin )
12 eqid 
 |-  dom ( voln ` (/) ) = dom ( voln ` (/) )
13 noel 
 |-  -. k e. (/)
14 13 pm2.21i 
 |-  ( k e. (/) -> A e. RR )
15 14 adantl 
 |-  ( ( ph /\ k e. (/) ) -> A e. RR )
16 13 pm2.21i 
 |-  ( k e. (/) -> B e. RR )
17 16 adantl 
 |-  ( ( ph /\ k e. (/) ) -> B e. RR )
18 1 11 12 15 17 hoimbl2 
 |-  ( ph -> X_ k e. (/) ( A [,) B ) e. dom ( voln ` (/) ) )
19 18 adantr 
 |-  ( ( ph /\ X = (/) ) -> X_ k e. (/) ( A [,) B ) e. dom ( voln ` (/) ) )
20 9 19 eqeltrd 
 |-  ( ( ph /\ X = (/) ) -> X_ k e. X ( A [,) B ) e. dom ( voln ` (/) ) )
21 20 von0val 
 |-  ( ( ph /\ X = (/) ) -> ( ( voln ` (/) ) ` X_ k e. X ( A [,) B ) ) = 0 )
22 7 21 eqtrd 
 |-  ( ( ph /\ X = (/) ) -> ( ( voln ` X ) ` X_ k e. X ( A [,) B ) ) = 0 )
23 0red 
 |-  ( ( ph /\ X = (/) ) -> 0 e. RR )
24 22 23 eqeltrd 
 |-  ( ( ph /\ X = (/) ) -> ( ( voln ` X ) ` X_ k e. X ( A [,) B ) ) e. RR )
25 neqne 
 |-  ( -. X = (/) -> X =/= (/) )
26 25 adantl 
 |-  ( ( ph /\ -. X = (/) ) -> X =/= (/) )
27 simpr 
 |-  ( ( ph /\ j e. X ) -> j e. X )
28 nfv 
 |-  F/ k j e. X
29 1 28 nfan 
 |-  F/ k ( ph /\ j e. X )
30 nfcv 
 |-  F/_ k j
31 30 nfcsb1 
 |-  F/_ k [_ j / k ]_ A
32 31 nfel1 
 |-  F/ k [_ j / k ]_ A e. RR
33 29 32 nfim 
 |-  F/ k ( ( ph /\ j e. X ) -> [_ j / k ]_ A e. RR )
34 eleq1w 
 |-  ( k = j -> ( k e. X <-> j e. X ) )
35 34 anbi2d 
 |-  ( k = j -> ( ( ph /\ k e. X ) <-> ( ph /\ j e. X ) ) )
36 csbeq1a 
 |-  ( k = j -> A = [_ j / k ]_ A )
37 36 eleq1d 
 |-  ( k = j -> ( A e. RR <-> [_ j / k ]_ A e. RR ) )
38 35 37 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ k e. X ) -> A e. RR ) <-> ( ( ph /\ j e. X ) -> [_ j / k ]_ A e. RR ) ) )
39 33 38 3 chvarfv 
 |-  ( ( ph /\ j e. X ) -> [_ j / k ]_ A e. RR )
40 eqid 
 |-  ( k e. X |-> A ) = ( k e. X |-> A )
41 30 31 36 40 fvmptf 
 |-  ( ( j e. X /\ [_ j / k ]_ A e. RR ) -> ( ( k e. X |-> A ) ` j ) = [_ j / k ]_ A )
42 27 39 41 syl2anc 
 |-  ( ( ph /\ j e. X ) -> ( ( k e. X |-> A ) ` j ) = [_ j / k ]_ A )
43 30 nfcsb1 
 |-  F/_ k [_ j / k ]_ B
44 nfcv 
 |-  F/_ k RR
45 43 44 nfel 
 |-  F/ k [_ j / k ]_ B e. RR
46 29 45 nfim 
 |-  F/ k ( ( ph /\ j e. X ) -> [_ j / k ]_ B e. RR )
47 csbeq1a 
 |-  ( k = j -> B = [_ j / k ]_ B )
48 47 eleq1d 
 |-  ( k = j -> ( B e. RR <-> [_ j / k ]_ B e. RR ) )
49 35 48 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ k e. X ) -> B e. RR ) <-> ( ( ph /\ j e. X ) -> [_ j / k ]_ B e. RR ) ) )
50 46 49 4 chvarfv 
 |-  ( ( ph /\ j e. X ) -> [_ j / k ]_ B e. RR )
51 eqid 
 |-  ( k e. X |-> B ) = ( k e. X |-> B )
52 30 43 47 51 fvmptf 
 |-  ( ( j e. X /\ [_ j / k ]_ B e. RR ) -> ( ( k e. X |-> B ) ` j ) = [_ j / k ]_ B )
53 27 50 52 syl2anc 
 |-  ( ( ph /\ j e. X ) -> ( ( k e. X |-> B ) ` j ) = [_ j / k ]_ B )
54 42 53 oveq12d 
 |-  ( ( ph /\ j e. X ) -> ( ( ( k e. X |-> A ) ` j ) [,) ( ( k e. X |-> B ) ` j ) ) = ( [_ j / k ]_ A [,) [_ j / k ]_ B ) )
55 54 ixpeq2dva 
 |-  ( ph -> X_ j e. X ( ( ( k e. X |-> A ) ` j ) [,) ( ( k e. X |-> B ) ` j ) ) = X_ j e. X ( [_ j / k ]_ A [,) [_ j / k ]_ B ) )
56 nfcv 
 |-  F/_ j ( A [,) B )
57 nfcv 
 |-  F/_ k [,)
58 31 57 43 nfov 
 |-  F/_ k ( [_ j / k ]_ A [,) [_ j / k ]_ B )
59 36 47 oveq12d 
 |-  ( k = j -> ( A [,) B ) = ( [_ j / k ]_ A [,) [_ j / k ]_ B ) )
60 56 58 59 cbvixp 
 |-  X_ k e. X ( A [,) B ) = X_ j e. X ( [_ j / k ]_ A [,) [_ j / k ]_ B )
61 60 eqcomi 
 |-  X_ j e. X ( [_ j / k ]_ A [,) [_ j / k ]_ B ) = X_ k e. X ( A [,) B )
62 61 a1i 
 |-  ( ph -> X_ j e. X ( [_ j / k ]_ A [,) [_ j / k ]_ B ) = X_ k e. X ( A [,) B ) )
63 55 62 eqtr2d 
 |-  ( ph -> X_ k e. X ( A [,) B ) = X_ j e. X ( ( ( k e. X |-> A ) ` j ) [,) ( ( k e. X |-> B ) ` j ) ) )
64 63 fveq2d 
 |-  ( ph -> ( ( voln ` X ) ` X_ k e. X ( A [,) B ) ) = ( ( voln ` X ) ` X_ j e. X ( ( ( k e. X |-> A ) ` j ) [,) ( ( k e. X |-> B ) ` j ) ) ) )
65 64 adantr 
 |-  ( ( ph /\ X =/= (/) ) -> ( ( voln ` X ) ` X_ k e. X ( A [,) B ) ) = ( ( voln ` X ) ` X_ j e. X ( ( ( k e. X |-> A ) ` j ) [,) ( ( k e. X |-> B ) ` j ) ) ) )
66 2 adantr 
 |-  ( ( ph /\ X =/= (/) ) -> X e. Fin )
67 simpr 
 |-  ( ( ph /\ X =/= (/) ) -> X =/= (/) )
68 1 3 40 fmptdf 
 |-  ( ph -> ( k e. X |-> A ) : X --> RR )
69 68 adantr 
 |-  ( ( ph /\ X =/= (/) ) -> ( k e. X |-> A ) : X --> RR )
70 1 4 51 fmptdf 
 |-  ( ph -> ( k e. X |-> B ) : X --> RR )
71 70 adantr 
 |-  ( ( ph /\ X =/= (/) ) -> ( k e. X |-> B ) : X --> RR )
72 eqid 
 |-  X_ j e. X ( ( ( k e. X |-> A ) ` j ) [,) ( ( k e. X |-> B ) ` j ) ) = X_ j e. X ( ( ( k e. X |-> A ) ` j ) [,) ( ( k e. X |-> B ) ` j ) )
73 66 67 69 71 72 vonn0hoi 
 |-  ( ( ph /\ X =/= (/) ) -> ( ( voln ` X ) ` X_ j e. X ( ( ( k e. X |-> A ) ` j ) [,) ( ( k e. X |-> B ) ` j ) ) ) = prod_ j e. X ( vol ` ( ( ( k e. X |-> A ) ` j ) [,) ( ( k e. X |-> B ) ` j ) ) ) )
74 65 73 eqtrd 
 |-  ( ( ph /\ X =/= (/) ) -> ( ( voln ` X ) ` X_ k e. X ( A [,) B ) ) = prod_ j e. X ( vol ` ( ( ( k e. X |-> A ) ` j ) [,) ( ( k e. X |-> B ) ` j ) ) ) )
75 42 39 eqeltrd 
 |-  ( ( ph /\ j e. X ) -> ( ( k e. X |-> A ) ` j ) e. RR )
76 53 50 eqeltrd 
 |-  ( ( ph /\ j e. X ) -> ( ( k e. X |-> B ) ` j ) e. RR )
77 volicore 
 |-  ( ( ( ( k e. X |-> A ) ` j ) e. RR /\ ( ( k e. X |-> B ) ` j ) e. RR ) -> ( vol ` ( ( ( k e. X |-> A ) ` j ) [,) ( ( k e. X |-> B ) ` j ) ) ) e. RR )
78 75 76 77 syl2anc 
 |-  ( ( ph /\ j e. X ) -> ( vol ` ( ( ( k e. X |-> A ) ` j ) [,) ( ( k e. X |-> B ) ` j ) ) ) e. RR )
79 2 78 fprodrecl 
 |-  ( ph -> prod_ j e. X ( vol ` ( ( ( k e. X |-> A ) ` j ) [,) ( ( k e. X |-> B ) ` j ) ) ) e. RR )
80 79 adantr 
 |-  ( ( ph /\ X =/= (/) ) -> prod_ j e. X ( vol ` ( ( ( k e. X |-> A ) ` j ) [,) ( ( k e. X |-> B ) ` j ) ) ) e. RR )
81 74 80 eqeltrd 
 |-  ( ( ph /\ X =/= (/) ) -> ( ( voln ` X ) ` X_ k e. X ( A [,) B ) ) e. RR )
82 26 81 syldan 
 |-  ( ( ph /\ -. X = (/) ) -> ( ( voln ` X ) ` X_ k e. X ( A [,) B ) ) e. RR )
83 24 82 pm2.61dan 
 |-  ( ph -> ( ( voln ` X ) ` X_ k e. X ( A [,) B ) ) e. RR )