Step |
Hyp |
Ref |
Expression |
1 |
|
itgulm2.z |
|- Z = ( ZZ>= ` M ) |
2 |
|
itgulm2.m |
|- ( ph -> M e. ZZ ) |
3 |
|
itgulm2.l |
|- ( ( ph /\ k e. Z ) -> ( x e. S |-> A ) e. L^1 ) |
4 |
|
itgulm2.u |
|- ( ph -> ( k e. Z |-> ( x e. S |-> A ) ) ( ~~>u ` S ) ( x e. S |-> B ) ) |
5 |
|
itgulm2.s |
|- ( ph -> ( vol ` S ) e. RR ) |
6 |
3
|
fmpttd |
|- ( ph -> ( k e. Z |-> ( x e. S |-> A ) ) : Z --> L^1 ) |
7 |
1 2 6 4 5
|
iblulm |
|- ( ph -> ( x e. S |-> B ) e. L^1 ) |
8 |
1 2 6 4 5
|
itgulm |
|- ( ph -> ( n e. Z |-> S. S ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` n ) ` z ) _d z ) ~~> S. S ( ( x e. S |-> B ) ` z ) _d z ) |
9 |
|
nfcv |
|- F/_ k S |
10 |
|
nffvmpt1 |
|- F/_ k ( ( k e. Z |-> ( x e. S |-> A ) ) ` n ) |
11 |
|
nfcv |
|- F/_ k z |
12 |
10 11
|
nffv |
|- F/_ k ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` n ) ` z ) |
13 |
9 12
|
nfitg |
|- F/_ k S. S ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` n ) ` z ) _d z |
14 |
|
nfcv |
|- F/_ n S. S ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` k ) ` x ) _d x |
15 |
|
fveq2 |
|- ( z = x -> ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` n ) ` z ) = ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` n ) ` x ) ) |
16 |
|
nfcv |
|- F/_ x Z |
17 |
|
nfmpt1 |
|- F/_ x ( x e. S |-> A ) |
18 |
16 17
|
nfmpt |
|- F/_ x ( k e. Z |-> ( x e. S |-> A ) ) |
19 |
|
nfcv |
|- F/_ x n |
20 |
18 19
|
nffv |
|- F/_ x ( ( k e. Z |-> ( x e. S |-> A ) ) ` n ) |
21 |
|
nfcv |
|- F/_ x z |
22 |
20 21
|
nffv |
|- F/_ x ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` n ) ` z ) |
23 |
|
nfcv |
|- F/_ z ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` n ) ` x ) |
24 |
15 22 23
|
cbvitg |
|- S. S ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` n ) ` z ) _d z = S. S ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` n ) ` x ) _d x |
25 |
|
fveq2 |
|- ( n = k -> ( ( k e. Z |-> ( x e. S |-> A ) ) ` n ) = ( ( k e. Z |-> ( x e. S |-> A ) ) ` k ) ) |
26 |
25
|
fveq1d |
|- ( n = k -> ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` n ) ` x ) = ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` k ) ` x ) ) |
27 |
26
|
adantr |
|- ( ( n = k /\ x e. S ) -> ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` n ) ` x ) = ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` k ) ` x ) ) |
28 |
27
|
itgeq2dv |
|- ( n = k -> S. S ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` n ) ` x ) _d x = S. S ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` k ) ` x ) _d x ) |
29 |
24 28
|
syl5eq |
|- ( n = k -> S. S ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` n ) ` z ) _d z = S. S ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` k ) ` x ) _d x ) |
30 |
13 14 29
|
cbvmpt |
|- ( n e. Z |-> S. S ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` n ) ` z ) _d z ) = ( k e. Z |-> S. S ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` k ) ` x ) _d x ) |
31 |
|
simplr |
|- ( ( ( ph /\ k e. Z ) /\ x e. S ) -> k e. Z ) |
32 |
|
ulmscl |
|- ( ( k e. Z |-> ( x e. S |-> A ) ) ( ~~>u ` S ) ( x e. S |-> B ) -> S e. _V ) |
33 |
|
mptexg |
|- ( S e. _V -> ( x e. S |-> A ) e. _V ) |
34 |
4 32 33
|
3syl |
|- ( ph -> ( x e. S |-> A ) e. _V ) |
35 |
34
|
ad2antrr |
|- ( ( ( ph /\ k e. Z ) /\ x e. S ) -> ( x e. S |-> A ) e. _V ) |
36 |
|
eqid |
|- ( k e. Z |-> ( x e. S |-> A ) ) = ( k e. Z |-> ( x e. S |-> A ) ) |
37 |
36
|
fvmpt2 |
|- ( ( k e. Z /\ ( x e. S |-> A ) e. _V ) -> ( ( k e. Z |-> ( x e. S |-> A ) ) ` k ) = ( x e. S |-> A ) ) |
38 |
31 35 37
|
syl2anc |
|- ( ( ( ph /\ k e. Z ) /\ x e. S ) -> ( ( k e. Z |-> ( x e. S |-> A ) ) ` k ) = ( x e. S |-> A ) ) |
39 |
38
|
fveq1d |
|- ( ( ( ph /\ k e. Z ) /\ x e. S ) -> ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` k ) ` x ) = ( ( x e. S |-> A ) ` x ) ) |
40 |
|
simpr |
|- ( ( ( ph /\ k e. Z ) /\ x e. S ) -> x e. S ) |
41 |
34
|
ralrimivw |
|- ( ph -> A. k e. Z ( x e. S |-> A ) e. _V ) |
42 |
36
|
fnmpt |
|- ( A. k e. Z ( x e. S |-> A ) e. _V -> ( k e. Z |-> ( x e. S |-> A ) ) Fn Z ) |
43 |
41 42
|
syl |
|- ( ph -> ( k e. Z |-> ( x e. S |-> A ) ) Fn Z ) |
44 |
|
ulmf2 |
|- ( ( ( k e. Z |-> ( x e. S |-> A ) ) Fn Z /\ ( k e. Z |-> ( x e. S |-> A ) ) ( ~~>u ` S ) ( x e. S |-> B ) ) -> ( k e. Z |-> ( x e. S |-> A ) ) : Z --> ( CC ^m S ) ) |
45 |
43 4 44
|
syl2anc |
|- ( ph -> ( k e. Z |-> ( x e. S |-> A ) ) : Z --> ( CC ^m S ) ) |
46 |
45
|
fvmptelrn |
|- ( ( ph /\ k e. Z ) -> ( x e. S |-> A ) e. ( CC ^m S ) ) |
47 |
|
elmapi |
|- ( ( x e. S |-> A ) e. ( CC ^m S ) -> ( x e. S |-> A ) : S --> CC ) |
48 |
46 47
|
syl |
|- ( ( ph /\ k e. Z ) -> ( x e. S |-> A ) : S --> CC ) |
49 |
48
|
fvmptelrn |
|- ( ( ( ph /\ k e. Z ) /\ x e. S ) -> A e. CC ) |
50 |
|
eqid |
|- ( x e. S |-> A ) = ( x e. S |-> A ) |
51 |
50
|
fvmpt2 |
|- ( ( x e. S /\ A e. CC ) -> ( ( x e. S |-> A ) ` x ) = A ) |
52 |
40 49 51
|
syl2anc |
|- ( ( ( ph /\ k e. Z ) /\ x e. S ) -> ( ( x e. S |-> A ) ` x ) = A ) |
53 |
39 52
|
eqtrd |
|- ( ( ( ph /\ k e. Z ) /\ x e. S ) -> ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` k ) ` x ) = A ) |
54 |
53
|
itgeq2dv |
|- ( ( ph /\ k e. Z ) -> S. S ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` k ) ` x ) _d x = S. S A _d x ) |
55 |
54
|
mpteq2dva |
|- ( ph -> ( k e. Z |-> S. S ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` k ) ` x ) _d x ) = ( k e. Z |-> S. S A _d x ) ) |
56 |
30 55
|
syl5eq |
|- ( ph -> ( n e. Z |-> S. S ( ( ( k e. Z |-> ( x e. S |-> A ) ) ` n ) ` z ) _d z ) = ( k e. Z |-> S. S A _d x ) ) |
57 |
|
fveq2 |
|- ( z = x -> ( ( x e. S |-> B ) ` z ) = ( ( x e. S |-> B ) ` x ) ) |
58 |
|
nffvmpt1 |
|- F/_ x ( ( x e. S |-> B ) ` z ) |
59 |
|
nfcv |
|- F/_ z ( ( x e. S |-> B ) ` x ) |
60 |
57 58 59
|
cbvitg |
|- S. S ( ( x e. S |-> B ) ` z ) _d z = S. S ( ( x e. S |-> B ) ` x ) _d x |
61 |
|
simpr |
|- ( ( ph /\ x e. S ) -> x e. S ) |
62 |
|
ulmcl |
|- ( ( k e. Z |-> ( x e. S |-> A ) ) ( ~~>u ` S ) ( x e. S |-> B ) -> ( x e. S |-> B ) : S --> CC ) |
63 |
4 62
|
syl |
|- ( ph -> ( x e. S |-> B ) : S --> CC ) |
64 |
63
|
fvmptelrn |
|- ( ( ph /\ x e. S ) -> B e. CC ) |
65 |
|
eqid |
|- ( x e. S |-> B ) = ( x e. S |-> B ) |
66 |
65
|
fvmpt2 |
|- ( ( x e. S /\ B e. CC ) -> ( ( x e. S |-> B ) ` x ) = B ) |
67 |
61 64 66
|
syl2anc |
|- ( ( ph /\ x e. S ) -> ( ( x e. S |-> B ) ` x ) = B ) |
68 |
67
|
itgeq2dv |
|- ( ph -> S. S ( ( x e. S |-> B ) ` x ) _d x = S. S B _d x ) |
69 |
60 68
|
syl5eq |
|- ( ph -> S. S ( ( x e. S |-> B ) ` z ) _d z = S. S B _d x ) |
70 |
8 56 69
|
3brtr3d |
|- ( ph -> ( k e. Z |-> S. S A _d x ) ~~> S. S B _d x ) |
71 |
7 70
|
jca |
|- ( ph -> ( ( x e. S |-> B ) e. L^1 /\ ( k e. Z |-> S. S A _d x ) ~~> S. S B _d x ) ) |