Step | Hyp | Ref
| Expression |
1 | | itgulm2.z |
. . 3
⊢ 𝑍 =
(ℤ≥‘𝑀) |
2 | | itgulm2.m |
. . 3
⊢ (𝜑 → 𝑀 ∈ ℤ) |
3 | | itgulm2.l |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑥 ∈ 𝑆 ↦ 𝐴) ∈
𝐿1) |
4 | | eqid 2610 |
. . . 4
⊢ (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴)) |
5 | 3, 4 | fmptd 6292 |
. . 3
⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴)):𝑍⟶𝐿1) |
6 | | itgulm2.u |
. . 3
⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))(⇝𝑢‘𝑆)(𝑥 ∈ 𝑆 ↦ 𝐵)) |
7 | | itgulm2.s |
. . 3
⊢ (𝜑 → (vol‘𝑆) ∈
ℝ) |
8 | 1, 2, 5, 6, 7 | iblulm 23965 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐵) ∈
𝐿1) |
9 | 1, 2, 5, 6, 7 | itgulm 23966 |
. . 3
⊢ (𝜑 → (𝑛 ∈ 𝑍 ↦ ∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑧) d𝑧) ⇝ ∫𝑆((𝑥 ∈ 𝑆 ↦ 𝐵)‘𝑧) d𝑧) |
10 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑘𝑆 |
11 | | nffvmpt1 6111 |
. . . . . . 7
⊢
Ⅎ𝑘((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛) |
12 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑘𝑧 |
13 | 11, 12 | nffv 6110 |
. . . . . 6
⊢
Ⅎ𝑘(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑧) |
14 | 10, 13 | nfitg 23347 |
. . . . 5
⊢
Ⅎ𝑘∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑧) d𝑧 |
15 | | nfcv 2751 |
. . . . 5
⊢
Ⅎ𝑛∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑘)‘𝑥) d𝑥 |
16 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑧 = 𝑥 → (((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑧) = (((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑥)) |
17 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝑍 |
18 | | nfmpt1 4675 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑥 ∈ 𝑆 ↦ 𝐴) |
19 | 17, 18 | nfmpt 4674 |
. . . . . . . . 9
⊢
Ⅎ𝑥(𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴)) |
20 | | nfcv 2751 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝑛 |
21 | 19, 20 | nffv 6110 |
. . . . . . . 8
⊢
Ⅎ𝑥((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛) |
22 | | nfcv 2751 |
. . . . . . . 8
⊢
Ⅎ𝑥𝑧 |
23 | 21, 22 | nffv 6110 |
. . . . . . 7
⊢
Ⅎ𝑥(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑧) |
24 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑧(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑥) |
25 | 16, 23, 24 | cbvitg 23348 |
. . . . . 6
⊢
∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑧) d𝑧 = ∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑥) d𝑥 |
26 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → ((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛) = ((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑘)) |
27 | 26 | fveq1d 6105 |
. . . . . . . 8
⊢ (𝑛 = 𝑘 → (((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑥) = (((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑘)‘𝑥)) |
28 | 27 | adantr 480 |
. . . . . . 7
⊢ ((𝑛 = 𝑘 ∧ 𝑥 ∈ 𝑆) → (((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑥) = (((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑘)‘𝑥)) |
29 | 28 | itgeq2dv 23354 |
. . . . . 6
⊢ (𝑛 = 𝑘 → ∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑥) d𝑥 = ∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑘)‘𝑥) d𝑥) |
30 | 25, 29 | syl5eq 2656 |
. . . . 5
⊢ (𝑛 = 𝑘 → ∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑧) d𝑧 = ∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑘)‘𝑥) d𝑥) |
31 | 14, 15, 30 | cbvmpt 4677 |
. . . 4
⊢ (𝑛 ∈ 𝑍 ↦ ∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑧) d𝑧) = (𝑘 ∈ 𝑍 ↦ ∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑘)‘𝑥) d𝑥) |
32 | | simplr 788 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑥 ∈ 𝑆) → 𝑘 ∈ 𝑍) |
33 | | ulmscl 23937 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))(⇝𝑢‘𝑆)(𝑥 ∈ 𝑆 ↦ 𝐵) → 𝑆 ∈ V) |
34 | | mptexg 6389 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ V → (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ V) |
35 | 6, 33, 34 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ V) |
36 | 35 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑥 ∈ 𝑆) → (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ V) |
37 | 4 | fvmpt2 6200 |
. . . . . . . . 9
⊢ ((𝑘 ∈ 𝑍 ∧ (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ V) → ((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑘) = (𝑥 ∈ 𝑆 ↦ 𝐴)) |
38 | 32, 36, 37 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑥 ∈ 𝑆) → ((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑘) = (𝑥 ∈ 𝑆 ↦ 𝐴)) |
39 | 38 | fveq1d 6105 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑥 ∈ 𝑆) → (((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑘)‘𝑥) = ((𝑥 ∈ 𝑆 ↦ 𝐴)‘𝑥)) |
40 | | simpr 476 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆) |
41 | 35 | ralrimivw 2950 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑘 ∈ 𝑍 (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ V) |
42 | 4 | fnmpt 5933 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑘 ∈
𝑍 (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ V → (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴)) Fn 𝑍) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴)) Fn 𝑍) |
44 | | ulmf2 23942 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴)) Fn 𝑍 ∧ (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))(⇝𝑢‘𝑆)(𝑥 ∈ 𝑆 ↦ 𝐵)) → (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴)):𝑍⟶(ℂ ↑𝑚
𝑆)) |
45 | 43, 6, 44 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴)):𝑍⟶(ℂ ↑𝑚
𝑆)) |
46 | 4 | fmpt 6289 |
. . . . . . . . . . . . 13
⊢
(∀𝑘 ∈
𝑍 (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ (ℂ ↑𝑚
𝑆) ↔ (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴)):𝑍⟶(ℂ ↑𝑚
𝑆)) |
47 | 45, 46 | sylibr 223 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑘 ∈ 𝑍 (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ (ℂ ↑𝑚
𝑆)) |
48 | 47 | r19.21bi 2916 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ (ℂ ↑𝑚
𝑆)) |
49 | | elmapi 7765 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑆 ↦ 𝐴) ∈ (ℂ ↑𝑚
𝑆) → (𝑥 ∈ 𝑆 ↦ 𝐴):𝑆⟶ℂ) |
50 | 48, 49 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑥 ∈ 𝑆 ↦ 𝐴):𝑆⟶ℂ) |
51 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝑆 ↦ 𝐴) = (𝑥 ∈ 𝑆 ↦ 𝐴) |
52 | 51 | fmpt 6289 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝑆 𝐴 ∈ ℂ ↔ (𝑥 ∈ 𝑆 ↦ 𝐴):𝑆⟶ℂ) |
53 | 50, 52 | sylibr 223 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ∀𝑥 ∈ 𝑆 𝐴 ∈ ℂ) |
54 | 53 | r19.21bi 2916 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℂ) |
55 | 51 | fvmpt2 6200 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑆 ∧ 𝐴 ∈ ℂ) → ((𝑥 ∈ 𝑆 ↦ 𝐴)‘𝑥) = 𝐴) |
56 | 40, 54, 55 | syl2anc 691 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑥 ∈ 𝑆) → ((𝑥 ∈ 𝑆 ↦ 𝐴)‘𝑥) = 𝐴) |
57 | 39, 56 | eqtrd 2644 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑥 ∈ 𝑆) → (((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑘)‘𝑥) = 𝐴) |
58 | 57 | itgeq2dv 23354 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑘)‘𝑥) d𝑥 = ∫𝑆𝐴 d𝑥) |
59 | 58 | mpteq2dva 4672 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ ∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑘)‘𝑥) d𝑥) = (𝑘 ∈ 𝑍 ↦ ∫𝑆𝐴 d𝑥)) |
60 | 31, 59 | syl5eq 2656 |
. . 3
⊢ (𝜑 → (𝑛 ∈ 𝑍 ↦ ∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑧) d𝑧) = (𝑘 ∈ 𝑍 ↦ ∫𝑆𝐴 d𝑥)) |
61 | | fveq2 6103 |
. . . . 5
⊢ (𝑧 = 𝑥 → ((𝑥 ∈ 𝑆 ↦ 𝐵)‘𝑧) = ((𝑥 ∈ 𝑆 ↦ 𝐵)‘𝑥)) |
62 | | nffvmpt1 6111 |
. . . . 5
⊢
Ⅎ𝑥((𝑥 ∈ 𝑆 ↦ 𝐵)‘𝑧) |
63 | | nfcv 2751 |
. . . . 5
⊢
Ⅎ𝑧((𝑥 ∈ 𝑆 ↦ 𝐵)‘𝑥) |
64 | 61, 62, 63 | cbvitg 23348 |
. . . 4
⊢
∫𝑆((𝑥 ∈ 𝑆 ↦ 𝐵)‘𝑧) d𝑧 = ∫𝑆((𝑥 ∈ 𝑆 ↦ 𝐵)‘𝑥) d𝑥 |
65 | | simpr 476 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆) |
66 | | ulmcl 23939 |
. . . . . . . . 9
⊢ ((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))(⇝𝑢‘𝑆)(𝑥 ∈ 𝑆 ↦ 𝐵) → (𝑥 ∈ 𝑆 ↦ 𝐵):𝑆⟶ℂ) |
67 | 6, 66 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐵):𝑆⟶ℂ) |
68 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑆 ↦ 𝐵) = (𝑥 ∈ 𝑆 ↦ 𝐵) |
69 | 68 | fmpt 6289 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝑆 𝐵 ∈ ℂ ↔ (𝑥 ∈ 𝑆 ↦ 𝐵):𝑆⟶ℂ) |
70 | 67, 69 | sylibr 223 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 𝐵 ∈ ℂ) |
71 | 70 | r19.21bi 2916 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ ℂ) |
72 | 68 | fvmpt2 6200 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑆 ∧ 𝐵 ∈ ℂ) → ((𝑥 ∈ 𝑆 ↦ 𝐵)‘𝑥) = 𝐵) |
73 | 65, 71, 72 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((𝑥 ∈ 𝑆 ↦ 𝐵)‘𝑥) = 𝐵) |
74 | 73 | itgeq2dv 23354 |
. . . 4
⊢ (𝜑 → ∫𝑆((𝑥 ∈ 𝑆 ↦ 𝐵)‘𝑥) d𝑥 = ∫𝑆𝐵 d𝑥) |
75 | 64, 74 | syl5eq 2656 |
. . 3
⊢ (𝜑 → ∫𝑆((𝑥 ∈ 𝑆 ↦ 𝐵)‘𝑧) d𝑧 = ∫𝑆𝐵 d𝑥) |
76 | 9, 60, 75 | 3brtr3d 4614 |
. 2
⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ ∫𝑆𝐴 d𝑥) ⇝ ∫𝑆𝐵 d𝑥) |
77 | 8, 76 | jca 553 |
1
⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ 𝐵) ∈ 𝐿1 ∧ (𝑘 ∈ 𝑍 ↦ ∫𝑆𝐴 d𝑥) ⇝ ∫𝑆𝐵 d𝑥)) |