| Step | Hyp | Ref
| Expression |
| 1 | | itgulm2.z |
. . 3
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 2 | | itgulm2.m |
. . 3
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 3 | | itgulm2.l |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑥 ∈ 𝑆 ↦ 𝐴) ∈
𝐿1) |
| 4 | 3 | fmpttd 7135 |
. . 3
⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴)):𝑍⟶𝐿1) |
| 5 | | itgulm2.u |
. . 3
⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))(⇝𝑢‘𝑆)(𝑥 ∈ 𝑆 ↦ 𝐵)) |
| 6 | | itgulm2.s |
. . 3
⊢ (𝜑 → (vol‘𝑆) ∈
ℝ) |
| 7 | 1, 2, 4, 5, 6 | iblulm 26450 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐵) ∈
𝐿1) |
| 8 | 1, 2, 4, 5, 6 | itgulm 26451 |
. . 3
⊢ (𝜑 → (𝑛 ∈ 𝑍 ↦ ∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑧) d𝑧) ⇝ ∫𝑆((𝑥 ∈ 𝑆 ↦ 𝐵)‘𝑧) d𝑧) |
| 9 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑘𝑆 |
| 10 | | nffvmpt1 6917 |
. . . . . . 7
⊢
Ⅎ𝑘((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛) |
| 11 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑘𝑧 |
| 12 | 10, 11 | nffv 6916 |
. . . . . 6
⊢
Ⅎ𝑘(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑧) |
| 13 | 9, 12 | nfitg 25810 |
. . . . 5
⊢
Ⅎ𝑘∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑧) d𝑧 |
| 14 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑛∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑘)‘𝑥) d𝑥 |
| 15 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑧 = 𝑥 → (((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑧) = (((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑥)) |
| 16 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝑍 |
| 17 | | nfmpt1 5250 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑥 ∈ 𝑆 ↦ 𝐴) |
| 18 | 16, 17 | nfmpt 5249 |
. . . . . . . . 9
⊢
Ⅎ𝑥(𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴)) |
| 19 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝑛 |
| 20 | 18, 19 | nffv 6916 |
. . . . . . . 8
⊢
Ⅎ𝑥((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛) |
| 21 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑥𝑧 |
| 22 | 20, 21 | nffv 6916 |
. . . . . . 7
⊢
Ⅎ𝑥(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑧) |
| 23 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑧(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑥) |
| 24 | 15, 22, 23 | cbvitg 25811 |
. . . . . 6
⊢
∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑧) d𝑧 = ∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑥) d𝑥 |
| 25 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → ((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛) = ((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑘)) |
| 26 | 25 | fveq1d 6908 |
. . . . . . . 8
⊢ (𝑛 = 𝑘 → (((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑥) = (((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑘)‘𝑥)) |
| 27 | 26 | adantr 480 |
. . . . . . 7
⊢ ((𝑛 = 𝑘 ∧ 𝑥 ∈ 𝑆) → (((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑥) = (((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑘)‘𝑥)) |
| 28 | 27 | itgeq2dv 25817 |
. . . . . 6
⊢ (𝑛 = 𝑘 → ∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑥) d𝑥 = ∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑘)‘𝑥) d𝑥) |
| 29 | 24, 28 | eqtrid 2789 |
. . . . 5
⊢ (𝑛 = 𝑘 → ∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑧) d𝑧 = ∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑘)‘𝑥) d𝑥) |
| 30 | 13, 14, 29 | cbvmpt 5253 |
. . . 4
⊢ (𝑛 ∈ 𝑍 ↦ ∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑧) d𝑧) = (𝑘 ∈ 𝑍 ↦ ∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑘)‘𝑥) d𝑥) |
| 31 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑥 ∈ 𝑆) → 𝑘 ∈ 𝑍) |
| 32 | | ulmscl 26422 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))(⇝𝑢‘𝑆)(𝑥 ∈ 𝑆 ↦ 𝐵) → 𝑆 ∈ V) |
| 33 | | mptexg 7241 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ V → (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ V) |
| 34 | 5, 32, 33 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ V) |
| 35 | 34 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑥 ∈ 𝑆) → (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ V) |
| 36 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴)) |
| 37 | 36 | fvmpt2 7027 |
. . . . . . . . 9
⊢ ((𝑘 ∈ 𝑍 ∧ (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ V) → ((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑘) = (𝑥 ∈ 𝑆 ↦ 𝐴)) |
| 38 | 31, 35, 37 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑥 ∈ 𝑆) → ((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑘) = (𝑥 ∈ 𝑆 ↦ 𝐴)) |
| 39 | 38 | fveq1d 6908 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑥 ∈ 𝑆) → (((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑘)‘𝑥) = ((𝑥 ∈ 𝑆 ↦ 𝐴)‘𝑥)) |
| 40 | | simpr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆) |
| 41 | 34 | ralrimivw 3150 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑘 ∈ 𝑍 (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ V) |
| 42 | 36 | fnmpt 6708 |
. . . . . . . . . . . . 13
⊢
(∀𝑘 ∈
𝑍 (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ V → (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴)) Fn 𝑍) |
| 43 | 41, 42 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴)) Fn 𝑍) |
| 44 | | ulmf2 26427 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴)) Fn 𝑍 ∧ (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))(⇝𝑢‘𝑆)(𝑥 ∈ 𝑆 ↦ 𝐵)) → (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴)):𝑍⟶(ℂ ↑m 𝑆)) |
| 45 | 43, 5, 44 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴)):𝑍⟶(ℂ ↑m 𝑆)) |
| 46 | 45 | fvmptelcdm 7133 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ (ℂ ↑m 𝑆)) |
| 47 | | elmapi 8889 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝑆 ↦ 𝐴) ∈ (ℂ ↑m 𝑆) → (𝑥 ∈ 𝑆 ↦ 𝐴):𝑆⟶ℂ) |
| 48 | 46, 47 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑥 ∈ 𝑆 ↦ 𝐴):𝑆⟶ℂ) |
| 49 | 48 | fvmptelcdm 7133 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℂ) |
| 50 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑆 ↦ 𝐴) = (𝑥 ∈ 𝑆 ↦ 𝐴) |
| 51 | 50 | fvmpt2 7027 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑆 ∧ 𝐴 ∈ ℂ) → ((𝑥 ∈ 𝑆 ↦ 𝐴)‘𝑥) = 𝐴) |
| 52 | 40, 49, 51 | syl2anc 584 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑥 ∈ 𝑆) → ((𝑥 ∈ 𝑆 ↦ 𝐴)‘𝑥) = 𝐴) |
| 53 | 39, 52 | eqtrd 2777 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑥 ∈ 𝑆) → (((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑘)‘𝑥) = 𝐴) |
| 54 | 53 | itgeq2dv 25817 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑘)‘𝑥) d𝑥 = ∫𝑆𝐴 d𝑥) |
| 55 | 54 | mpteq2dva 5242 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ ∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑘)‘𝑥) d𝑥) = (𝑘 ∈ 𝑍 ↦ ∫𝑆𝐴 d𝑥)) |
| 56 | 30, 55 | eqtrid 2789 |
. . 3
⊢ (𝜑 → (𝑛 ∈ 𝑍 ↦ ∫𝑆(((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))‘𝑛)‘𝑧) d𝑧) = (𝑘 ∈ 𝑍 ↦ ∫𝑆𝐴 d𝑥)) |
| 57 | | fveq2 6906 |
. . . . 5
⊢ (𝑧 = 𝑥 → ((𝑥 ∈ 𝑆 ↦ 𝐵)‘𝑧) = ((𝑥 ∈ 𝑆 ↦ 𝐵)‘𝑥)) |
| 58 | | nffvmpt1 6917 |
. . . . 5
⊢
Ⅎ𝑥((𝑥 ∈ 𝑆 ↦ 𝐵)‘𝑧) |
| 59 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑧((𝑥 ∈ 𝑆 ↦ 𝐵)‘𝑥) |
| 60 | 57, 58, 59 | cbvitg 25811 |
. . . 4
⊢
∫𝑆((𝑥 ∈ 𝑆 ↦ 𝐵)‘𝑧) d𝑧 = ∫𝑆((𝑥 ∈ 𝑆 ↦ 𝐵)‘𝑥) d𝑥 |
| 61 | | simpr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆) |
| 62 | | ulmcl 26424 |
. . . . . . . 8
⊢ ((𝑘 ∈ 𝑍 ↦ (𝑥 ∈ 𝑆 ↦ 𝐴))(⇝𝑢‘𝑆)(𝑥 ∈ 𝑆 ↦ 𝐵) → (𝑥 ∈ 𝑆 ↦ 𝐵):𝑆⟶ℂ) |
| 63 | 5, 62 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐵):𝑆⟶ℂ) |
| 64 | 63 | fvmptelcdm 7133 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ ℂ) |
| 65 | | eqid 2737 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑆 ↦ 𝐵) = (𝑥 ∈ 𝑆 ↦ 𝐵) |
| 66 | 65 | fvmpt2 7027 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑆 ∧ 𝐵 ∈ ℂ) → ((𝑥 ∈ 𝑆 ↦ 𝐵)‘𝑥) = 𝐵) |
| 67 | 61, 64, 66 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((𝑥 ∈ 𝑆 ↦ 𝐵)‘𝑥) = 𝐵) |
| 68 | 67 | itgeq2dv 25817 |
. . . 4
⊢ (𝜑 → ∫𝑆((𝑥 ∈ 𝑆 ↦ 𝐵)‘𝑥) d𝑥 = ∫𝑆𝐵 d𝑥) |
| 69 | 60, 68 | eqtrid 2789 |
. . 3
⊢ (𝜑 → ∫𝑆((𝑥 ∈ 𝑆 ↦ 𝐵)‘𝑧) d𝑧 = ∫𝑆𝐵 d𝑥) |
| 70 | 8, 56, 69 | 3brtr3d 5174 |
. 2
⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ ∫𝑆𝐴 d𝑥) ⇝ ∫𝑆𝐵 d𝑥) |
| 71 | 7, 70 | jca 511 |
1
⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ 𝐵) ∈ 𝐿1 ∧ (𝑘 ∈ 𝑍 ↦ ∫𝑆𝐴 d𝑥) ⇝ ∫𝑆𝐵 d𝑥)) |