Step | Hyp | Ref
| Expression |
1 | | itgulm2.z |
. . 3
β’ π =
(β€β₯βπ) |
2 | | itgulm2.m |
. . 3
β’ (π β π β β€) |
3 | | itgulm2.l |
. . . 4
β’ ((π β§ π β π) β (π₯ β π β¦ π΄) β
πΏ1) |
4 | 3 | fmpttd 7068 |
. . 3
β’ (π β (π β π β¦ (π₯ β π β¦ π΄)):πβΆπΏ1) |
5 | | itgulm2.u |
. . 3
β’ (π β (π β π β¦ (π₯ β π β¦ π΄))(βπ’βπ)(π₯ β π β¦ π΅)) |
6 | | itgulm2.s |
. . 3
β’ (π β (volβπ) β
β) |
7 | 1, 2, 4, 5, 6 | iblulm 25782 |
. 2
β’ (π β (π₯ β π β¦ π΅) β
πΏ1) |
8 | 1, 2, 4, 5, 6 | itgulm 25783 |
. . 3
β’ (π β (π β π β¦ β«π(((π β π β¦ (π₯ β π β¦ π΄))βπ)βπ§) dπ§) β β«π((π₯ β π β¦ π΅)βπ§) dπ§) |
9 | | nfcv 2908 |
. . . . . 6
β’
β²ππ |
10 | | nffvmpt1 6858 |
. . . . . . 7
β’
β²π((π β π β¦ (π₯ β π β¦ π΄))βπ) |
11 | | nfcv 2908 |
. . . . . . 7
β’
β²ππ§ |
12 | 10, 11 | nffv 6857 |
. . . . . 6
β’
β²π(((π β π β¦ (π₯ β π β¦ π΄))βπ)βπ§) |
13 | 9, 12 | nfitg 25155 |
. . . . 5
β’
β²πβ«π(((π β π β¦ (π₯ β π β¦ π΄))βπ)βπ§) dπ§ |
14 | | nfcv 2908 |
. . . . 5
β’
β²πβ«π(((π β π β¦ (π₯ β π β¦ π΄))βπ)βπ₯) dπ₯ |
15 | | fveq2 6847 |
. . . . . . 7
β’ (π§ = π₯ β (((π β π β¦ (π₯ β π β¦ π΄))βπ)βπ§) = (((π β π β¦ (π₯ β π β¦ π΄))βπ)βπ₯)) |
16 | | nfcv 2908 |
. . . . . . . . . 10
β’
β²π₯π |
17 | | nfmpt1 5218 |
. . . . . . . . . 10
β’
β²π₯(π₯ β π β¦ π΄) |
18 | 16, 17 | nfmpt 5217 |
. . . . . . . . 9
β’
β²π₯(π β π β¦ (π₯ β π β¦ π΄)) |
19 | | nfcv 2908 |
. . . . . . . . 9
β’
β²π₯π |
20 | 18, 19 | nffv 6857 |
. . . . . . . 8
β’
β²π₯((π β π β¦ (π₯ β π β¦ π΄))βπ) |
21 | | nfcv 2908 |
. . . . . . . 8
β’
β²π₯π§ |
22 | 20, 21 | nffv 6857 |
. . . . . . 7
β’
β²π₯(((π β π β¦ (π₯ β π β¦ π΄))βπ)βπ§) |
23 | | nfcv 2908 |
. . . . . . 7
β’
β²π§(((π β π β¦ (π₯ β π β¦ π΄))βπ)βπ₯) |
24 | 15, 22, 23 | cbvitg 25156 |
. . . . . 6
β’
β«π(((π β π β¦ (π₯ β π β¦ π΄))βπ)βπ§) dπ§ = β«π(((π β π β¦ (π₯ β π β¦ π΄))βπ)βπ₯) dπ₯ |
25 | | fveq2 6847 |
. . . . . . . . 9
β’ (π = π β ((π β π β¦ (π₯ β π β¦ π΄))βπ) = ((π β π β¦ (π₯ β π β¦ π΄))βπ)) |
26 | 25 | fveq1d 6849 |
. . . . . . . 8
β’ (π = π β (((π β π β¦ (π₯ β π β¦ π΄))βπ)βπ₯) = (((π β π β¦ (π₯ β π β¦ π΄))βπ)βπ₯)) |
27 | 26 | adantr 482 |
. . . . . . 7
β’ ((π = π β§ π₯ β π) β (((π β π β¦ (π₯ β π β¦ π΄))βπ)βπ₯) = (((π β π β¦ (π₯ β π β¦ π΄))βπ)βπ₯)) |
28 | 27 | itgeq2dv 25162 |
. . . . . 6
β’ (π = π β β«π(((π β π β¦ (π₯ β π β¦ π΄))βπ)βπ₯) dπ₯ = β«π(((π β π β¦ (π₯ β π β¦ π΄))βπ)βπ₯) dπ₯) |
29 | 24, 28 | eqtrid 2789 |
. . . . 5
β’ (π = π β β«π(((π β π β¦ (π₯ β π β¦ π΄))βπ)βπ§) dπ§ = β«π(((π β π β¦ (π₯ β π β¦ π΄))βπ)βπ₯) dπ₯) |
30 | 13, 14, 29 | cbvmpt 5221 |
. . . 4
β’ (π β π β¦ β«π(((π β π β¦ (π₯ β π β¦ π΄))βπ)βπ§) dπ§) = (π β π β¦ β«π(((π β π β¦ (π₯ β π β¦ π΄))βπ)βπ₯) dπ₯) |
31 | | simplr 768 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π₯ β π) β π β π) |
32 | | ulmscl 25754 |
. . . . . . . . . . 11
β’ ((π β π β¦ (π₯ β π β¦ π΄))(βπ’βπ)(π₯ β π β¦ π΅) β π β V) |
33 | | mptexg 7176 |
. . . . . . . . . . 11
β’ (π β V β (π₯ β π β¦ π΄) β V) |
34 | 5, 32, 33 | 3syl 18 |
. . . . . . . . . 10
β’ (π β (π₯ β π β¦ π΄) β V) |
35 | 34 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π₯ β π) β (π₯ β π β¦ π΄) β V) |
36 | | eqid 2737 |
. . . . . . . . . 10
β’ (π β π β¦ (π₯ β π β¦ π΄)) = (π β π β¦ (π₯ β π β¦ π΄)) |
37 | 36 | fvmpt2 6964 |
. . . . . . . . 9
β’ ((π β π β§ (π₯ β π β¦ π΄) β V) β ((π β π β¦ (π₯ β π β¦ π΄))βπ) = (π₯ β π β¦ π΄)) |
38 | 31, 35, 37 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ π β π) β§ π₯ β π) β ((π β π β¦ (π₯ β π β¦ π΄))βπ) = (π₯ β π β¦ π΄)) |
39 | 38 | fveq1d 6849 |
. . . . . . 7
β’ (((π β§ π β π) β§ π₯ β π) β (((π β π β¦ (π₯ β π β¦ π΄))βπ)βπ₯) = ((π₯ β π β¦ π΄)βπ₯)) |
40 | | simpr 486 |
. . . . . . . 8
β’ (((π β§ π β π) β§ π₯ β π) β π₯ β π) |
41 | 34 | ralrimivw 3148 |
. . . . . . . . . . . . 13
β’ (π β βπ β π (π₯ β π β¦ π΄) β V) |
42 | 36 | fnmpt 6646 |
. . . . . . . . . . . . 13
β’
(βπ β
π (π₯ β π β¦ π΄) β V β (π β π β¦ (π₯ β π β¦ π΄)) Fn π) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (π β π β¦ (π₯ β π β¦ π΄)) Fn π) |
44 | | ulmf2 25759 |
. . . . . . . . . . . 12
β’ (((π β π β¦ (π₯ β π β¦ π΄)) Fn π β§ (π β π β¦ (π₯ β π β¦ π΄))(βπ’βπ)(π₯ β π β¦ π΅)) β (π β π β¦ (π₯ β π β¦ π΄)):πβΆ(β βm π)) |
45 | 43, 5, 44 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β (π β π β¦ (π₯ β π β¦ π΄)):πβΆ(β βm π)) |
46 | 45 | fvmptelcdm 7066 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (π₯ β π β¦ π΄) β (β βm π)) |
47 | | elmapi 8794 |
. . . . . . . . . 10
β’ ((π₯ β π β¦ π΄) β (β βm π) β (π₯ β π β¦ π΄):πβΆβ) |
48 | 46, 47 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π β π) β (π₯ β π β¦ π΄):πβΆβ) |
49 | 48 | fvmptelcdm 7066 |
. . . . . . . 8
β’ (((π β§ π β π) β§ π₯ β π) β π΄ β β) |
50 | | eqid 2737 |
. . . . . . . . 9
β’ (π₯ β π β¦ π΄) = (π₯ β π β¦ π΄) |
51 | 50 | fvmpt2 6964 |
. . . . . . . 8
β’ ((π₯ β π β§ π΄ β β) β ((π₯ β π β¦ π΄)βπ₯) = π΄) |
52 | 40, 49, 51 | syl2anc 585 |
. . . . . . 7
β’ (((π β§ π β π) β§ π₯ β π) β ((π₯ β π β¦ π΄)βπ₯) = π΄) |
53 | 39, 52 | eqtrd 2777 |
. . . . . 6
β’ (((π β§ π β π) β§ π₯ β π) β (((π β π β¦ (π₯ β π β¦ π΄))βπ)βπ₯) = π΄) |
54 | 53 | itgeq2dv 25162 |
. . . . 5
β’ ((π β§ π β π) β β«π(((π β π β¦ (π₯ β π β¦ π΄))βπ)βπ₯) dπ₯ = β«ππ΄ dπ₯) |
55 | 54 | mpteq2dva 5210 |
. . . 4
β’ (π β (π β π β¦ β«π(((π β π β¦ (π₯ β π β¦ π΄))βπ)βπ₯) dπ₯) = (π β π β¦ β«ππ΄ dπ₯)) |
56 | 30, 55 | eqtrid 2789 |
. . 3
β’ (π β (π β π β¦ β«π(((π β π β¦ (π₯ β π β¦ π΄))βπ)βπ§) dπ§) = (π β π β¦ β«ππ΄ dπ₯)) |
57 | | fveq2 6847 |
. . . . 5
β’ (π§ = π₯ β ((π₯ β π β¦ π΅)βπ§) = ((π₯ β π β¦ π΅)βπ₯)) |
58 | | nffvmpt1 6858 |
. . . . 5
β’
β²π₯((π₯ β π β¦ π΅)βπ§) |
59 | | nfcv 2908 |
. . . . 5
β’
β²π§((π₯ β π β¦ π΅)βπ₯) |
60 | 57, 58, 59 | cbvitg 25156 |
. . . 4
β’
β«π((π₯ β π β¦ π΅)βπ§) dπ§ = β«π((π₯ β π β¦ π΅)βπ₯) dπ₯ |
61 | | simpr 486 |
. . . . . 6
β’ ((π β§ π₯ β π) β π₯ β π) |
62 | | ulmcl 25756 |
. . . . . . . 8
β’ ((π β π β¦ (π₯ β π β¦ π΄))(βπ’βπ)(π₯ β π β¦ π΅) β (π₯ β π β¦ π΅):πβΆβ) |
63 | 5, 62 | syl 17 |
. . . . . . 7
β’ (π β (π₯ β π β¦ π΅):πβΆβ) |
64 | 63 | fvmptelcdm 7066 |
. . . . . 6
β’ ((π β§ π₯ β π) β π΅ β β) |
65 | | eqid 2737 |
. . . . . . 7
β’ (π₯ β π β¦ π΅) = (π₯ β π β¦ π΅) |
66 | 65 | fvmpt2 6964 |
. . . . . 6
β’ ((π₯ β π β§ π΅ β β) β ((π₯ β π β¦ π΅)βπ₯) = π΅) |
67 | 61, 64, 66 | syl2anc 585 |
. . . . 5
β’ ((π β§ π₯ β π) β ((π₯ β π β¦ π΅)βπ₯) = π΅) |
68 | 67 | itgeq2dv 25162 |
. . . 4
β’ (π β β«π((π₯ β π β¦ π΅)βπ₯) dπ₯ = β«ππ΅ dπ₯) |
69 | 60, 68 | eqtrid 2789 |
. . 3
β’ (π β β«π((π₯ β π β¦ π΅)βπ§) dπ§ = β«ππ΅ dπ₯) |
70 | 8, 56, 69 | 3brtr3d 5141 |
. 2
β’ (π β (π β π β¦ β«ππ΄ dπ₯) β β«ππ΅ dπ₯) |
71 | 7, 70 | jca 513 |
1
β’ (π β ((π₯ β π β¦ π΅) β πΏ1 β§ (π β π β¦ β«ππ΄ dπ₯) β β«ππ΅ dπ₯)) |