Metamath Proof Explorer

Theorem vonn0ioo2

Description: The n-dimensional Lebesgue measure of an open interval when the dimension of the space is nonzero. This is the first statement in Proposition 115G (d) of Fremlin1 p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses vonn0ioo2.k 
|- F/ k ph
vonn0ioo2.x 
|- ( ph -> X e. Fin )
vonn0ioo2.n 
|- ( ph -> X =/= (/) )
vonn0ioo2.a 
|- ( ( ph /\ k e. X ) -> A e. RR )
vonn0ioo2.b 
|- ( ( ph /\ k e. X ) -> B e. RR )
vonn0ioo2.i 
|- I = X_ k e. X ( A (,) B )
Assertion vonn0ioo2 
|- ( ph -> ( ( voln ` X ) ` I ) = prod_ k e. X ( vol ` ( A (,) B ) ) )

Proof

Step Hyp Ref Expression
1 vonn0ioo2.k 
 |-  F/ k ph
2 vonn0ioo2.x 
 |-  ( ph -> X e. Fin )
3 vonn0ioo2.n 
 |-  ( ph -> X =/= (/) )
4 vonn0ioo2.a 
 |-  ( ( ph /\ k e. X ) -> A e. RR )
5 vonn0ioo2.b 
 |-  ( ( ph /\ k e. X ) -> B e. RR )
6 vonn0ioo2.i 
 |-  I = X_ k e. X ( A (,) B )
7 6 a1i 
 |-  ( ph -> I = X_ k e. X ( A (,) B ) )
8 simpr 
 |-  ( ( ph /\ j e. X ) -> j e. X )
9 nfv 
 |-  F/ k j e. X
10 1 9 nfan 
 |-  F/ k ( ph /\ j e. X )
11 nfcsb1v 
 |-  F/_ k [_ j / k ]_ A
12 nfcv 
 |-  F/_ k RR
13 11 12 nfel 
 |-  F/ k [_ j / k ]_ A e. RR
14 10 13 nfim 
 |-  F/ k ( ( ph /\ j e. X ) -> [_ j / k ]_ A e. RR )
15 eleq1w 
 |-  ( k = j -> ( k e. X <-> j e. X ) )
16 15 anbi2d 
 |-  ( k = j -> ( ( ph /\ k e. X ) <-> ( ph /\ j e. X ) ) )
17 csbeq1a 
 |-  ( k = j -> A = [_ j / k ]_ A )
18 17 eleq1d 
 |-  ( k = j -> ( A e. RR <-> [_ j / k ]_ A e. RR ) )
19 16 18 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ k e. X ) -> A e. RR ) <-> ( ( ph /\ j e. X ) -> [_ j / k ]_ A e. RR ) ) )
20 14 19 4 chvarfv 
 |-  ( ( ph /\ j e. X ) -> [_ j / k ]_ A e. RR )
21 eqid 
 |-  ( k e. X |-> A ) = ( k e. X |-> A )
22 21 fvmpts 
 |-  ( ( j e. X /\ [_ j / k ]_ A e. RR ) -> ( ( k e. X |-> A ) ` j ) = [_ j / k ]_ A )
23 8 20 22 syl2anc 
 |-  ( ( ph /\ j e. X ) -> ( ( k e. X |-> A ) ` j ) = [_ j / k ]_ A )
24 nfcsb1v 
 |-  F/_ k [_ j / k ]_ B
25 24 12 nfel 
 |-  F/ k [_ j / k ]_ B e. RR
26 10 25 nfim 
 |-  F/ k ( ( ph /\ j e. X ) -> [_ j / k ]_ B e. RR )
27 csbeq1a 
 |-  ( k = j -> B = [_ j / k ]_ B )
28 27 eleq1d 
 |-  ( k = j -> ( B e. RR <-> [_ j / k ]_ B e. RR ) )
29 16 28 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ k e. X ) -> B e. RR ) <-> ( ( ph /\ j e. X ) -> [_ j / k ]_ B e. RR ) ) )
30 26 29 5 chvarfv 
 |-  ( ( ph /\ j e. X ) -> [_ j / k ]_ B e. RR )
31 eqid 
 |-  ( k e. X |-> B ) = ( k e. X |-> B )
32 31 fvmpts 
 |-  ( ( j e. X /\ [_ j / k ]_ B e. RR ) -> ( ( k e. X |-> B ) ` j ) = [_ j / k ]_ B )
33 8 30 32 syl2anc 
 |-  ( ( ph /\ j e. X ) -> ( ( k e. X |-> B ) ` j ) = [_ j / k ]_ B )
34 23 33 oveq12d 
 |-  ( ( ph /\ j e. X ) -> ( ( ( k e. X |-> A ) ` j ) (,) ( ( k e. X |-> B ) ` j ) ) = ( [_ j / k ]_ A (,) [_ j / k ]_ B ) )
35 34 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 ) )
36 nfcv 
 |-  F/_ k (,)
37 11 36 24 nfov 
 |-  F/_ k ( [_ j / k ]_ A (,) [_ j / k ]_ B )
38 nfcv 
 |-  F/_ j ( A (,) B )
39 17 equcoms 
 |-  ( j = k -> A = [_ j / k ]_ A )
40 39 eqcomd 
 |-  ( j = k -> [_ j / k ]_ A = A )
41 eqidd 
 |-  ( j = k -> A = A )
42 40 41 eqtrd 
 |-  ( j = k -> [_ j / k ]_ A = A )
43 27 equcoms 
 |-  ( j = k -> B = [_ j / k ]_ B )
44 43 eqcomd 
 |-  ( j = k -> [_ j / k ]_ B = B )
45 42 44 oveq12d 
 |-  ( j = k -> ( [_ j / k ]_ A (,) [_ j / k ]_ B ) = ( A (,) B ) )
46 37 38 45 cbvixp 
 |-  X_ j e. X ( [_ j / k ]_ A (,) [_ j / k ]_ B ) = X_ k e. X ( A (,) B )
47 46 a1i 
 |-  ( ph -> X_ j e. X ( [_ j / k ]_ A (,) [_ j / k ]_ B ) = X_ k e. X ( A (,) B ) )
48 35 47 eqtrd 
 |-  ( ph -> X_ j e. X ( ( ( k e. X |-> A ) ` j ) (,) ( ( k e. X |-> B ) ` j ) ) = X_ k e. X ( A (,) B ) )
49 7 48 eqtr4d 
 |-  ( ph -> I = X_ j e. X ( ( ( k e. X |-> A ) ` j ) (,) ( ( k e. X |-> B ) ` j ) ) )
50 49 fveq2d 
 |-  ( ph -> ( ( voln ` X ) ` I ) = ( ( voln ` X ) ` X_ j e. X ( ( ( k e. X |-> A ) ` j ) (,) ( ( k e. X |-> B ) ` j ) ) ) )
51 1 4 21 fmptdf 
 |-  ( ph -> ( k e. X |-> A ) : X --> RR )
52 1 5 31 fmptdf 
 |-  ( ph -> ( k e. X |-> B ) : X --> RR )
53 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 ) )
54 2 3 51 52 53 vonn0ioo 
 |-  ( ph -> ( ( 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 ) ) ) )
55 23 33 oveq12d 
 |-  ( ( ph /\ j e. X ) -> ( ( ( k e. X |-> A ) ` j ) [,) ( ( k e. X |-> B ) ` j ) ) = ( [_ j / k ]_ A [,) [_ j / k ]_ B ) )
56 55 fveq2d 
 |-  ( ( ph /\ j e. X ) -> ( vol ` ( ( ( k e. X |-> A ) ` j ) [,) ( ( k e. X |-> B ) ` j ) ) ) = ( vol ` ( [_ j / k ]_ A [,) [_ j / k ]_ B ) ) )
57 20 30 voliooico 
 |-  ( ( ph /\ j e. X ) -> ( vol ` ( [_ j / k ]_ A (,) [_ j / k ]_ B ) ) = ( vol ` ( [_ j / k ]_ A [,) [_ j / k ]_ B ) ) )
58 57 eqcomd 
 |-  ( ( ph /\ j e. X ) -> ( vol ` ( [_ j / k ]_ A [,) [_ j / k ]_ B ) ) = ( vol ` ( [_ j / k ]_ A (,) [_ j / k ]_ B ) ) )
59 56 58 eqtrd 
 |-  ( ( ph /\ j e. X ) -> ( vol ` ( ( ( k e. X |-> A ) ` j ) [,) ( ( k e. X |-> B ) ` j ) ) ) = ( vol ` ( [_ j / k ]_ A (,) [_ j / k ]_ B ) ) )
60 59 prodeq2dv 
 |-  ( ph -> prod_ j e. X ( vol ` ( ( ( k e. X |-> A ) ` j ) [,) ( ( k e. X |-> B ) ` j ) ) ) = prod_ j e. X ( vol ` ( [_ j / k ]_ A (,) [_ j / k ]_ B ) ) )
61 45 fveq2d 
 |-  ( j = k -> ( vol ` ( [_ j / k ]_ A (,) [_ j / k ]_ B ) ) = ( vol ` ( A (,) B ) ) )
62 nfcv 
 |-  F/_ k X
63 nfcv 
 |-  F/_ j X
64 nfcv 
 |-  F/_ k vol
65 64 37 nffv 
 |-  F/_ k ( vol ` ( [_ j / k ]_ A (,) [_ j / k ]_ B ) )
66 nfcv 
 |-  F/_ j ( vol ` ( A (,) B ) )
67 61 62 63 65 66 cbvprod 
 |-  prod_ j e. X ( vol ` ( [_ j / k ]_ A (,) [_ j / k ]_ B ) ) = prod_ k e. X ( vol ` ( A (,) B ) )
68 67 a1i 
 |-  ( ph -> prod_ j e. X ( vol ` ( [_ j / k ]_ A (,) [_ j / k ]_ B ) ) = prod_ k e. X ( vol ` ( A (,) B ) ) )
69 60 68 eqtrd 
 |-  ( ph -> prod_ j e. X ( vol ` ( ( ( k e. X |-> A ) ` j ) [,) ( ( k e. X |-> B ) ` j ) ) ) = prod_ k e. X ( vol ` ( A (,) B ) ) )
70 50 54 69 3eqtrd 
 |-  ( ph -> ( ( voln ` X ) ` I ) = prod_ k e. X ( vol ` ( A (,) B ) ) )