Step | Hyp | Ref
| Expression |
1 | | itgulm2.z |
. . 3
⊢ 𝑍 =
(ℤ≥‘𝑀) |
2 | | itgulm2.m |
. . 3
⊢ (𝜑 → 𝑀 ∈ ℤ) |
3 | | itgulm2.l |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑥 ∈ 𝑆 ↦ 𝐴) ∈
𝐿1) |
4 | 3 | fmpttd 6953 |
. . 3
⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴)):𝑍⟶𝐿1) |
5 | | itgulm2.u |
. . 3
⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))(⇝𝑢‘𝑆)(𝑥 ∈ 𝑆 ↦ 𝐵)) |
6 | | itgulm2.s |
. . 3
⊢ (𝜑 → (vol‘𝑆) ∈
ℝ) |
7 | 1, 2, 4, 5, 6 | iblulm 25328 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐵) ∈
𝐿1) |
8 | 1, 2, 4, 5, 6 | itgulm 25329 |
. . 3
⊢ (𝜑 → (𝑛 ∈ 𝑍 ↦ ∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑧) d𝑧) ⇝ ∫𝑆((𝑥 ∈ 𝑆 ↦ 𝐵)‘𝑧) d𝑧) |
9 | | nfcv 2906 |
. . . . . 6
⊢
Ⅎ𝑘𝑆 |
10 | | nffvmpt1 6749 |
. . . . . . 7
⊢
Ⅎ𝑘((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛) |
11 | | nfcv 2906 |
. . . . . . 7
⊢
Ⅎ𝑘𝑧 |
12 | 10, 11 | nffv 6748 |
. . . . . 6
⊢
Ⅎ𝑘(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑧) |
13 | 9, 12 | nfitg 24701 |
. . . . 5
⊢
Ⅎ𝑘∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑧) d𝑧 |
14 | | nfcv 2906 |
. . . . 5
⊢
Ⅎ𝑛∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑘)‘𝑥) d𝑥 |
15 | | fveq2 6738 |
. . . . . . 7
⊢ (𝑧 = 𝑥 → (((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑧) = (((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑥)) |
16 | | nfcv 2906 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝑍 |
17 | | nfmpt1 5169 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑥 ∈ 𝑆 ↦ 𝐴) |
18 | 16, 17 | nfmpt 5168 |
. . . . . . . . 9
⊢
Ⅎ𝑥(𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴)) |
19 | | nfcv 2906 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝑛 |
20 | 18, 19 | nffv 6748 |
. . . . . . . 8
⊢
Ⅎ𝑥((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛) |
21 | | nfcv 2906 |
. . . . . . . 8
⊢
Ⅎ𝑥𝑧 |
22 | 20, 21 | nffv 6748 |
. . . . . . 7
⊢
Ⅎ𝑥(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑧) |
23 | | nfcv 2906 |
. . . . . . 7
⊢
Ⅎ𝑧(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑥) |
24 | 15, 22, 23 | cbvitg 24702 |
. . . . . 6
⊢
∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑧) d𝑧 = ∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑥) d𝑥 |
25 | | fveq2 6738 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → ((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛) = ((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑘)) |
26 | 25 | fveq1d 6740 |
. . . . . . . 8
⊢ (𝑛 = 𝑘 → (((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑥) = (((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑘)‘𝑥)) |
27 | 26 | adantr 484 |
. . . . . . 7
⊢ ((𝑛 = 𝑘 ∧ 𝑥 ∈ 𝑆) → (((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑥) = (((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑘)‘𝑥)) |
28 | 27 | itgeq2dv 24708 |
. . . . . 6
⊢ (𝑛 = 𝑘 → ∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑥) d𝑥 = ∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑘)‘𝑥) d𝑥) |
29 | 24, 28 | syl5eq 2792 |
. . . . 5
⊢ (𝑛 = 𝑘 → ∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑧) d𝑧 = ∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑘)‘𝑥) d𝑥) |
30 | 13, 14, 29 | cbvmpt 5172 |
. . . 4
⊢ (𝑛 ∈ 𝑍 ↦ ∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑧) d𝑧) = (𝑘 ∈ 𝑍 ↦ ∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑘)‘𝑥) d𝑥) |
31 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑥 ∈ 𝑆) → 𝑘 ∈ 𝑍) |
32 | | ulmscl 25300 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))(⇝𝑢‘𝑆)(𝑥 ∈ 𝑆 ↦ 𝐵) → 𝑆 ∈ V) |
33 | | mptexg 7058 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ V → (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ V) |
34 | 5, 32, 33 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ V) |
35 | 34 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑥 ∈ 𝑆) → (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ V) |
36 | | eqid 2739 |
. . . . . . . . . 10
⊢ (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴)) |
37 | 36 | fvmpt2 6850 |
. . . . . . . . 9
⊢ ((𝑘 ∈ 𝑍 ∧ (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ V) → ((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑘) = (𝑥 ∈ 𝑆 ↦ 𝐴)) |
38 | 31, 35, 37 | syl2anc 587 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑥 ∈ 𝑆) → ((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑘) = (𝑥 ∈ 𝑆 ↦ 𝐴)) |
39 | 38 | fveq1d 6740 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑥 ∈ 𝑆) → (((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑘)‘𝑥) = ((𝑥 ∈ 𝑆 ↦ 𝐴)‘𝑥)) |
40 | | simpr 488 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆) |
41 | 34 | ralrimivw 3108 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑘 ∈ 𝑍 (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ V) |
42 | 36 | fnmpt 6539 |
. . . . . . . . . . . . 13
⊢
(∀𝑘 ∈
𝑍 (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ V → (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴)) Fn 𝑍) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴)) Fn 𝑍) |
44 | | ulmf2 25305 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴)) Fn 𝑍 ∧ (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))(⇝𝑢‘𝑆)(𝑥 ∈ 𝑆 ↦ 𝐵)) → (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴)):𝑍⟶(ℂ ↑m 𝑆)) |
45 | 43, 5, 44 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴)):𝑍⟶(ℂ ↑m 𝑆)) |
46 | 45 | fvmptelrn 6951 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ (ℂ ↑m 𝑆)) |
47 | | elmapi 8553 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝑆 ↦ 𝐴) ∈ (ℂ ↑m 𝑆) → (𝑥 ∈ 𝑆 ↦ 𝐴):𝑆⟶ℂ) |
48 | 46, 47 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑥 ∈ 𝑆 ↦ 𝐴):𝑆⟶ℂ) |
49 | 48 | fvmptelrn 6951 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℂ) |
50 | | eqid 2739 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑆 ↦ 𝐴) = (𝑥 ∈ 𝑆 ↦ 𝐴) |
51 | 50 | fvmpt2 6850 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑆 ∧ 𝐴 ∈ ℂ) → ((𝑥 ∈ 𝑆 ↦ 𝐴)‘𝑥) = 𝐴) |
52 | 40, 49, 51 | syl2anc 587 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑥 ∈ 𝑆) → ((𝑥 ∈ 𝑆 ↦ 𝐴)‘𝑥) = 𝐴) |
53 | 39, 52 | eqtrd 2779 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑥 ∈ 𝑆) → (((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑘)‘𝑥) = 𝐴) |
54 | 53 | itgeq2dv 24708 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑘)‘𝑥) d𝑥 = ∫𝑆𝐴 d𝑥) |
55 | 54 | mpteq2dva 5166 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ ∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑘)‘𝑥) d𝑥) = (𝑘 ∈ 𝑍 ↦ ∫𝑆𝐴 d𝑥)) |
56 | 30, 55 | syl5eq 2792 |
. . 3
⊢ (𝜑 → (𝑛 ∈ 𝑍 ↦ ∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑧) d𝑧) = (𝑘 ∈ 𝑍 ↦ ∫𝑆𝐴 d𝑥)) |
57 | | fveq2 6738 |
. . . . 5
⊢ (𝑧 = 𝑥 → ((𝑥 ∈ 𝑆 ↦ 𝐵)‘𝑧) = ((𝑥 ∈ 𝑆 ↦ 𝐵)‘𝑥)) |
58 | | nffvmpt1 6749 |
. . . . 5
⊢
Ⅎ𝑥((𝑥 ∈ 𝑆 ↦ 𝐵)‘𝑧) |
59 | | nfcv 2906 |
. . . . 5
⊢
Ⅎ𝑧((𝑥 ∈ 𝑆 ↦ 𝐵)‘𝑥) |
60 | 57, 58, 59 | cbvitg 24702 |
. . . 4
⊢
∫𝑆((𝑥 ∈ 𝑆 ↦ 𝐵)‘𝑧) d𝑧 = ∫𝑆((𝑥 ∈ 𝑆 ↦ 𝐵)‘𝑥) d𝑥 |
61 | | simpr 488 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆) |
62 | | ulmcl 25302 |
. . . . . . . 8
⊢ ((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))(⇝𝑢‘𝑆)(𝑥 ∈ 𝑆 ↦ 𝐵) → (𝑥 ∈ 𝑆 ↦ 𝐵):𝑆⟶ℂ) |
63 | 5, 62 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐵):𝑆⟶ℂ) |
64 | 63 | fvmptelrn 6951 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ ℂ) |
65 | | eqid 2739 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑆 ↦ 𝐵) = (𝑥 ∈ 𝑆 ↦ 𝐵) |
66 | 65 | fvmpt2 6850 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑆 ∧ 𝐵 ∈ ℂ) → ((𝑥 ∈ 𝑆 ↦ 𝐵)‘𝑥) = 𝐵) |
67 | 61, 64, 66 | syl2anc 587 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((𝑥 ∈ 𝑆 ↦ 𝐵)‘𝑥) = 𝐵) |
68 | 67 | itgeq2dv 24708 |
. . . 4
⊢ (𝜑 → ∫𝑆((𝑥 ∈ 𝑆 ↦ 𝐵)‘𝑥) d𝑥 = ∫𝑆𝐵 d𝑥) |
69 | 60, 68 | syl5eq 2792 |
. . 3
⊢ (𝜑 → ∫𝑆((𝑥 ∈ 𝑆 ↦ 𝐵)‘𝑧) d𝑧 = ∫𝑆𝐵 d𝑥) |
70 | 8, 56, 69 | 3brtr3d 5100 |
. 2
⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ ∫𝑆𝐴 d𝑥) ⇝ ∫𝑆𝐵 d𝑥) |
71 | 7, 70 | jca 515 |
1
⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ 𝐵) ∈ 𝐿1 ∧ (𝑘 ∈ 𝑍 ↦ ∫𝑆𝐴 d𝑥) ⇝ ∫𝑆𝐵 d𝑥)) |