Metamath Proof Explorer


Theorem vonn0icc2

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

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

Proof

Step Hyp Ref Expression
1 vonn0icc2.k
 |-  F/ k ph
2 vonn0icc2.x
 |-  ( ph -> X e. Fin )
3 vonn0icc2.n
 |-  ( ph -> X =/= (/) )
4 vonn0icc2.a
 |-  ( ( ph /\ k e. X ) -> A e. RR )
5 vonn0icc2.b
 |-  ( ( ph /\ k e. X ) -> B e. RR )
6 vonn0icc2.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 vonn0icc
 |-  ( 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 34 fveq2d
 |-  ( ( ph /\ j e. X ) -> ( vol ` ( ( ( k e. X |-> A ) ` j ) [,] ( ( k e. X |-> B ) ` j ) ) ) = ( vol ` ( [_ j / k ]_ A [,] [_ j / k ]_ B ) ) )
56 55 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 ) ) )
57 45 fveq2d
 |-  ( j = k -> ( vol ` ( [_ j / k ]_ A [,] [_ j / k ]_ B ) ) = ( vol ` ( A [,] B ) ) )
58 nfcv
 |-  F/_ k X
59 nfcv
 |-  F/_ j X
60 nfcv
 |-  F/_ k vol
61 60 37 nffv
 |-  F/_ k ( vol ` ( [_ j / k ]_ A [,] [_ j / k ]_ B ) )
62 nfcv
 |-  F/_ j ( vol ` ( A [,] B ) )
63 57 58 59 61 62 cbvprod
 |-  prod_ j e. X ( vol ` ( [_ j / k ]_ A [,] [_ j / k ]_ B ) ) = prod_ k e. X ( vol ` ( A [,] B ) )
64 63 a1i
 |-  ( ph -> prod_ j e. X ( vol ` ( [_ j / k ]_ A [,] [_ j / k ]_ B ) ) = prod_ k e. X ( vol ` ( A [,] B ) ) )
65 56 64 eqtrd
 |-  ( ph -> prod_ j e. X ( vol ` ( ( ( k e. X |-> A ) ` j ) [,] ( ( k e. X |-> B ) ` j ) ) ) = prod_ k e. X ( vol ` ( A [,] B ) ) )
66 50 54 65 3eqtrd
 |-  ( ph -> ( ( voln ` X ) ` I ) = prod_ k e. X ( vol ` ( A [,] B ) ) )