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