Step | Hyp | Ref
| Expression |
1 | | itg10 25068 |
. . 3
β’
(β«1β(β Γ {0})) = 0 |
2 | | reex 11149 |
. . . . . 6
β’ β
β V |
3 | 2 | a1i 11 |
. . . . 5
β’ ((π β§ π΄ = 0) β β β
V) |
4 | | i1fmulc.2 |
. . . . . . 7
β’ (π β πΉ β dom
β«1) |
5 | | i1ff 25056 |
. . . . . . 7
β’ (πΉ β dom β«1
β πΉ:ββΆβ) |
6 | 4, 5 | syl 17 |
. . . . . 6
β’ (π β πΉ:ββΆβ) |
7 | 6 | adantr 482 |
. . . . 5
β’ ((π β§ π΄ = 0) β πΉ:ββΆβ) |
8 | | i1fmulc.3 |
. . . . . 6
β’ (π β π΄ β β) |
9 | 8 | adantr 482 |
. . . . 5
β’ ((π β§ π΄ = 0) β π΄ β β) |
10 | | 0red 11165 |
. . . . 5
β’ ((π β§ π΄ = 0) β 0 β
β) |
11 | | simplr 768 |
. . . . . . 7
β’ (((π β§ π΄ = 0) β§ π₯ β β) β π΄ = 0) |
12 | 11 | oveq1d 7377 |
. . . . . 6
β’ (((π β§ π΄ = 0) β§ π₯ β β) β (π΄ Β· π₯) = (0 Β· π₯)) |
13 | | mul02lem2 11339 |
. . . . . . 7
β’ (π₯ β β β (0
Β· π₯) =
0) |
14 | 13 | adantl 483 |
. . . . . 6
β’ (((π β§ π΄ = 0) β§ π₯ β β) β (0 Β· π₯) = 0) |
15 | 12, 14 | eqtrd 2777 |
. . . . 5
β’ (((π β§ π΄ = 0) β§ π₯ β β) β (π΄ Β· π₯) = 0) |
16 | 3, 7, 9, 10, 15 | caofid2 7656 |
. . . 4
β’ ((π β§ π΄ = 0) β ((β Γ {π΄}) βf Β·
πΉ) = (β Γ
{0})) |
17 | 16 | fveq2d 6851 |
. . 3
β’ ((π β§ π΄ = 0) β
(β«1β((β Γ {π΄}) βf Β· πΉ)) =
(β«1β(β Γ {0}))) |
18 | | simpr 486 |
. . . . 5
β’ ((π β§ π΄ = 0) β π΄ = 0) |
19 | 18 | oveq1d 7377 |
. . . 4
β’ ((π β§ π΄ = 0) β (π΄ Β· (β«1βπΉ)) = (0 Β·
(β«1βπΉ))) |
20 | | itg1cl 25065 |
. . . . . . . 8
β’ (πΉ β dom β«1
β (β«1βπΉ) β β) |
21 | 4, 20 | syl 17 |
. . . . . . 7
β’ (π β
(β«1βπΉ)
β β) |
22 | 21 | recnd 11190 |
. . . . . 6
β’ (π β
(β«1βπΉ)
β β) |
23 | 22 | mul02d 11360 |
. . . . 5
β’ (π β (0 Β·
(β«1βπΉ)) = 0) |
24 | 23 | adantr 482 |
. . . 4
β’ ((π β§ π΄ = 0) β (0 Β·
(β«1βπΉ)) = 0) |
25 | 19, 24 | eqtrd 2777 |
. . 3
β’ ((π β§ π΄ = 0) β (π΄ Β· (β«1βπΉ)) = 0) |
26 | 1, 17, 25 | 3eqtr4a 2803 |
. 2
β’ ((π β§ π΄ = 0) β
(β«1β((β Γ {π΄}) βf Β· πΉ)) = (π΄ Β· (β«1βπΉ))) |
27 | 4, 8 | i1fmulc 25084 |
. . . . . . . . . . . . . 14
β’ (π β ((β Γ {π΄}) βf Β·
πΉ) β dom
β«1) |
28 | 27 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π΄ β 0) β ((β Γ {π΄}) βf Β·
πΉ) β dom
β«1) |
29 | | i1ff 25056 |
. . . . . . . . . . . . 13
β’
(((β Γ {π΄}) βf Β· πΉ) β dom β«1
β ((β Γ {π΄}) βf Β· πΉ):ββΆβ) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π΄ β 0) β ((β Γ {π΄}) βf Β·
πΉ):ββΆβ) |
31 | 30 | frnd 6681 |
. . . . . . . . . . 11
β’ ((π β§ π΄ β 0) β ran ((β Γ {π΄}) βf Β·
πΉ) β
β) |
32 | 31 | ssdifssd 4107 |
. . . . . . . . . 10
β’ ((π β§ π΄ β 0) β (ran ((β Γ
{π΄}) βf
Β· πΉ) β {0})
β β) |
33 | 32 | sselda 3949 |
. . . . . . . . 9
β’ (((π β§ π΄ β 0) β§ π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
π β
β) |
34 | 33 | recnd 11190 |
. . . . . . . 8
β’ (((π β§ π΄ β 0) β§ π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
π β
β) |
35 | 8 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π΄ β 0) β π΄ β β) |
36 | 35 | recnd 11190 |
. . . . . . . . 9
β’ ((π β§ π΄ β 0) β π΄ β β) |
37 | 36 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π΄ β 0) β§ π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
π΄ β
β) |
38 | | simplr 768 |
. . . . . . . 8
β’ (((π β§ π΄ β 0) β§ π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
π΄ β 0) |
39 | 34, 37, 38 | divcan2d 11940 |
. . . . . . 7
β’ (((π β§ π΄ β 0) β§ π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
(π΄ Β· (π / π΄)) = π) |
40 | 4, 8 | i1fmulclem 25083 |
. . . . . . . . . 10
β’ (((π β§ π΄ β 0) β§ π β β) β (β‘((β Γ {π΄}) βf Β· πΉ) β {π}) = (β‘πΉ β {(π / π΄)})) |
41 | 33, 40 | syldan 592 |
. . . . . . . . 9
β’ (((π β§ π΄ β 0) β§ π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
(β‘((β Γ {π΄}) βf Β· πΉ) β {π}) = (β‘πΉ β {(π / π΄)})) |
42 | 41 | fveq2d 6851 |
. . . . . . . 8
β’ (((π β§ π΄ β 0) β§ π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
(volβ(β‘((β Γ {π΄}) βf Β·
πΉ) β {π})) = (volβ(β‘πΉ β {(π / π΄)}))) |
43 | 42 | eqcomd 2743 |
. . . . . . 7
β’ (((π β§ π΄ β 0) β§ π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
(volβ(β‘πΉ β {(π / π΄)})) = (volβ(β‘((β Γ {π΄}) βf Β· πΉ) β {π}))) |
44 | 39, 43 | oveq12d 7380 |
. . . . . 6
β’ (((π β§ π΄ β 0) β§ π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
((π΄ Β· (π / π΄)) Β· (volβ(β‘πΉ β {(π / π΄)}))) = (π Β· (volβ(β‘((β Γ {π΄}) βf Β· πΉ) β {π})))) |
45 | 8 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π΄ β 0) β§ π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
π΄ β
β) |
46 | 33, 45, 38 | redivcld 11990 |
. . . . . . . 8
β’ (((π β§ π΄ β 0) β§ π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
(π / π΄) β β) |
47 | 46 | recnd 11190 |
. . . . . . 7
β’ (((π β§ π΄ β 0) β§ π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
(π / π΄) β β) |
48 | 4 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π΄ β 0) β§ π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
πΉ β dom
β«1) |
49 | 45 | recnd 11190 |
. . . . . . . . . . 11
β’ (((π β§ π΄ β 0) β§ π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
π΄ β
β) |
50 | | eldifsni 4755 |
. . . . . . . . . . . 12
β’ (π β (ran ((β Γ
{π΄}) βf
Β· πΉ) β {0})
β π β
0) |
51 | 50 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β§ π΄ β 0) β§ π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
π β 0) |
52 | 34, 49, 51, 38 | divne0d 11954 |
. . . . . . . . . 10
β’ (((π β§ π΄ β 0) β§ π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
(π / π΄) β 0) |
53 | | eldifsn 4752 |
. . . . . . . . . 10
β’ ((π / π΄) β (β β {0}) β
((π / π΄) β β β§ (π / π΄) β 0)) |
54 | 46, 52, 53 | sylanbrc 584 |
. . . . . . . . 9
β’ (((π β§ π΄ β 0) β§ π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
(π / π΄) β (β β
{0})) |
55 | | i1fima2sn 25060 |
. . . . . . . . 9
β’ ((πΉ β dom β«1
β§ (π / π΄) β (β β {0}))
β (volβ(β‘πΉ β {(π / π΄)})) β β) |
56 | 48, 54, 55 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ π΄ β 0) β§ π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
(volβ(β‘πΉ β {(π / π΄)})) β β) |
57 | 56 | recnd 11190 |
. . . . . . 7
β’ (((π β§ π΄ β 0) β§ π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
(volβ(β‘πΉ β {(π / π΄)})) β β) |
58 | 37, 47, 57 | mulassd 11185 |
. . . . . 6
β’ (((π β§ π΄ β 0) β§ π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
((π΄ Β· (π / π΄)) Β· (volβ(β‘πΉ β {(π / π΄)}))) = (π΄ Β· ((π / π΄) Β· (volβ(β‘πΉ β {(π / π΄)}))))) |
59 | 44, 58 | eqtr3d 2779 |
. . . . 5
β’ (((π β§ π΄ β 0) β§ π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
(π Β·
(volβ(β‘((β Γ {π΄}) βf Β·
πΉ) β {π}))) = (π΄ Β· ((π / π΄) Β· (volβ(β‘πΉ β {(π / π΄)}))))) |
60 | 59 | sumeq2dv 15595 |
. . . 4
β’ ((π β§ π΄ β 0) β Ξ£π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})(π Β· (volβ(β‘((β Γ {π΄}) βf Β· πΉ) β {π}))) = Ξ£π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})(π΄ Β· ((π / π΄) Β· (volβ(β‘πΉ β {(π / π΄)}))))) |
61 | | i1frn 25057 |
. . . . . . 7
β’
(((β Γ {π΄}) βf Β· πΉ) β dom β«1
β ran ((β Γ {π΄}) βf Β· πΉ) β Fin) |
62 | 28, 61 | syl 17 |
. . . . . 6
β’ ((π β§ π΄ β 0) β ran ((β Γ {π΄}) βf Β·
πΉ) β
Fin) |
63 | | difss 4096 |
. . . . . 6
β’ (ran
((β Γ {π΄})
βf Β· πΉ) β {0}) β ran ((β Γ
{π΄}) βf
Β· πΉ) |
64 | | ssfi 9124 |
. . . . . 6
β’ ((ran
((β Γ {π΄})
βf Β· πΉ) β Fin β§ (ran ((β Γ
{π΄}) βf
Β· πΉ) β {0})
β ran ((β Γ {π΄}) βf Β· πΉ)) β (ran ((β Γ
{π΄}) βf
Β· πΉ) β {0})
β Fin) |
65 | 62, 63, 64 | sylancl 587 |
. . . . 5
β’ ((π β§ π΄ β 0) β (ran ((β Γ
{π΄}) βf
Β· πΉ) β {0})
β Fin) |
66 | 47, 57 | mulcld 11182 |
. . . . 5
β’ (((π β§ π΄ β 0) β§ π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
((π / π΄) Β· (volβ(β‘πΉ β {(π / π΄)}))) β β) |
67 | 65, 36, 66 | fsummulc2 15676 |
. . . 4
β’ ((π β§ π΄ β 0) β (π΄ Β· Ξ£π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})((π / π΄) Β· (volβ(β‘πΉ β {(π / π΄)})))) = Ξ£π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})(π΄ Β· ((π / π΄) Β· (volβ(β‘πΉ β {(π / π΄)}))))) |
68 | 60, 67 | eqtr4d 2780 |
. . 3
β’ ((π β§ π΄ β 0) β Ξ£π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})(π Β· (volβ(β‘((β Γ {π΄}) βf Β· πΉ) β {π}))) = (π΄ Β· Ξ£π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})((π / π΄) Β· (volβ(β‘πΉ β {(π / π΄)}))))) |
69 | | itg1val 25063 |
. . . 4
β’
(((β Γ {π΄}) βf Β· πΉ) β dom β«1
β (β«1β((β Γ {π΄}) βf Β· πΉ)) = Ξ£π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})(π Β· (volβ(β‘((β Γ {π΄}) βf Β· πΉ) β {π})))) |
70 | 28, 69 | syl 17 |
. . 3
β’ ((π β§ π΄ β 0) β
(β«1β((β Γ {π΄}) βf Β· πΉ)) = Ξ£π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})(π Β· (volβ(β‘((β Γ {π΄}) βf Β· πΉ) β {π})))) |
71 | 4 | adantr 482 |
. . . . . 6
β’ ((π β§ π΄ β 0) β πΉ β dom
β«1) |
72 | | itg1val 25063 |
. . . . . 6
β’ (πΉ β dom β«1
β (β«1βπΉ) = Ξ£π β (ran πΉ β {0})(π Β· (volβ(β‘πΉ β {π})))) |
73 | 71, 72 | syl 17 |
. . . . 5
β’ ((π β§ π΄ β 0) β
(β«1βπΉ)
= Ξ£π β (ran
πΉ β {0})(π Β· (volβ(β‘πΉ β {π})))) |
74 | | id 22 |
. . . . . . 7
β’ (π = (π / π΄) β π = (π / π΄)) |
75 | | sneq 4601 |
. . . . . . . . 9
β’ (π = (π / π΄) β {π} = {(π / π΄)}) |
76 | 75 | imaeq2d 6018 |
. . . . . . . 8
β’ (π = (π / π΄) β (β‘πΉ β {π}) = (β‘πΉ β {(π / π΄)})) |
77 | 76 | fveq2d 6851 |
. . . . . . 7
β’ (π = (π / π΄) β (volβ(β‘πΉ β {π})) = (volβ(β‘πΉ β {(π / π΄)}))) |
78 | 74, 77 | oveq12d 7380 |
. . . . . 6
β’ (π = (π / π΄) β (π Β· (volβ(β‘πΉ β {π}))) = ((π / π΄) Β· (volβ(β‘πΉ β {(π / π΄)})))) |
79 | | eqid 2737 |
. . . . . . 7
β’ (π β (ran ((β Γ
{π΄}) βf
Β· πΉ) β {0})
β¦ (π / π΄)) = (π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0}) β¦
(π / π΄)) |
80 | | eldifi 4091 |
. . . . . . . . 9
β’ (π β (ran ((β Γ
{π΄}) βf
Β· πΉ) β {0})
β π β ran
((β Γ {π΄})
βf Β· πΉ)) |
81 | 2 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β
V) |
82 | 6 | ffnd 6674 |
. . . . . . . . . . . . . . . . 17
β’ (π β πΉ Fn β) |
83 | | eqidd 2738 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π¦ β β) β (πΉβπ¦) = (πΉβπ¦)) |
84 | 81, 8, 82, 83 | ofc1 7648 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β β) β (((β Γ
{π΄}) βf
Β· πΉ)βπ¦) = (π΄ Β· (πΉβπ¦))) |
85 | 84 | adantlr 714 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π΄ β 0) β§ π¦ β β) β (((β Γ
{π΄}) βf
Β· πΉ)βπ¦) = (π΄ Β· (πΉβπ¦))) |
86 | 85 | oveq1d 7377 |
. . . . . . . . . . . . . 14
β’ (((π β§ π΄ β 0) β§ π¦ β β) β ((((β Γ
{π΄}) βf
Β· πΉ)βπ¦) / π΄) = ((π΄ Β· (πΉβπ¦)) / π΄)) |
87 | 6 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π΄ β 0) β πΉ:ββΆβ) |
88 | 87 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π΄ β 0) β§ π¦ β β) β (πΉβπ¦) β β) |
89 | 88 | recnd 11190 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π΄ β 0) β§ π¦ β β) β (πΉβπ¦) β β) |
90 | 36 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π΄ β 0) β§ π¦ β β) β π΄ β β) |
91 | | simplr 768 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π΄ β 0) β§ π¦ β β) β π΄ β 0) |
92 | 89, 90, 91 | divcan3d 11943 |
. . . . . . . . . . . . . 14
β’ (((π β§ π΄ β 0) β§ π¦ β β) β ((π΄ Β· (πΉβπ¦)) / π΄) = (πΉβπ¦)) |
93 | 86, 92 | eqtrd 2777 |
. . . . . . . . . . . . 13
β’ (((π β§ π΄ β 0) β§ π¦ β β) β ((((β Γ
{π΄}) βf
Β· πΉ)βπ¦) / π΄) = (πΉβπ¦)) |
94 | 87 | ffnd 6674 |
. . . . . . . . . . . . . 14
β’ ((π β§ π΄ β 0) β πΉ Fn β) |
95 | | fnfvelrn 7036 |
. . . . . . . . . . . . . 14
β’ ((πΉ Fn β β§ π¦ β β) β (πΉβπ¦) β ran πΉ) |
96 | 94, 95 | sylan 581 |
. . . . . . . . . . . . 13
β’ (((π β§ π΄ β 0) β§ π¦ β β) β (πΉβπ¦) β ran πΉ) |
97 | 93, 96 | eqeltrd 2838 |
. . . . . . . . . . . 12
β’ (((π β§ π΄ β 0) β§ π¦ β β) β ((((β Γ
{π΄}) βf
Β· πΉ)βπ¦) / π΄) β ran πΉ) |
98 | 97 | ralrimiva 3144 |
. . . . . . . . . . 11
β’ ((π β§ π΄ β 0) β βπ¦ β β ((((β Γ {π΄}) βf Β·
πΉ)βπ¦) / π΄) β ran πΉ) |
99 | 30 | ffnd 6674 |
. . . . . . . . . . . 12
β’ ((π β§ π΄ β 0) β ((β Γ {π΄}) βf Β·
πΉ) Fn
β) |
100 | | oveq1 7369 |
. . . . . . . . . . . . . 14
β’ (π = (((β Γ {π΄}) βf Β·
πΉ)βπ¦) β (π / π΄) = ((((β Γ {π΄}) βf Β· πΉ)βπ¦) / π΄)) |
101 | 100 | eleq1d 2823 |
. . . . . . . . . . . . 13
β’ (π = (((β Γ {π΄}) βf Β·
πΉ)βπ¦) β ((π / π΄) β ran πΉ β ((((β Γ {π΄}) βf Β·
πΉ)βπ¦) / π΄) β ran πΉ)) |
102 | 101 | ralrn 7043 |
. . . . . . . . . . . 12
β’
(((β Γ {π΄}) βf Β· πΉ) Fn β β
(βπ β ran
((β Γ {π΄})
βf Β· πΉ)(π / π΄) β ran πΉ β βπ¦ β β ((((β Γ {π΄}) βf Β·
πΉ)βπ¦) / π΄) β ran πΉ)) |
103 | 99, 102 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π΄ β 0) β (βπ β ran ((β Γ {π΄}) βf Β·
πΉ)(π / π΄) β ran πΉ β βπ¦ β β ((((β Γ {π΄}) βf Β·
πΉ)βπ¦) / π΄) β ran πΉ)) |
104 | 98, 103 | mpbird 257 |
. . . . . . . . . 10
β’ ((π β§ π΄ β 0) β βπ β ran ((β Γ {π΄}) βf Β·
πΉ)(π / π΄) β ran πΉ) |
105 | 104 | r19.21bi 3237 |
. . . . . . . . 9
β’ (((π β§ π΄ β 0) β§ π β ran ((β Γ {π΄}) βf Β·
πΉ)) β (π / π΄) β ran πΉ) |
106 | 80, 105 | sylan2 594 |
. . . . . . . 8
β’ (((π β§ π΄ β 0) β§ π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
(π / π΄) β ran πΉ) |
107 | 32 | sselda 3949 |
. . . . . . . . . 10
β’ (((π β§ π΄ β 0) β§ π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
π β
β) |
108 | 107 | recnd 11190 |
. . . . . . . . 9
β’ (((π β§ π΄ β 0) β§ π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
π β
β) |
109 | 36 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π΄ β 0) β§ π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
π΄ β
β) |
110 | | eldifsni 4755 |
. . . . . . . . . 10
β’ (π β (ran ((β Γ
{π΄}) βf
Β· πΉ) β {0})
β π β
0) |
111 | 110 | adantl 483 |
. . . . . . . . 9
β’ (((π β§ π΄ β 0) β§ π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
π β 0) |
112 | | simplr 768 |
. . . . . . . . 9
β’ (((π β§ π΄ β 0) β§ π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
π΄ β 0) |
113 | 108, 109,
111, 112 | divne0d 11954 |
. . . . . . . 8
β’ (((π β§ π΄ β 0) β§ π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
(π / π΄) β 0) |
114 | | eldifsn 4752 |
. . . . . . . 8
β’ ((π / π΄) β (ran πΉ β {0}) β ((π / π΄) β ran πΉ β§ (π / π΄) β 0)) |
115 | 106, 113,
114 | sylanbrc 584 |
. . . . . . 7
β’ (((π β§ π΄ β 0) β§ π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
(π / π΄) β (ran πΉ β {0})) |
116 | | eldifi 4091 |
. . . . . . . . 9
β’ (π β (ran πΉ β {0}) β π β ran πΉ) |
117 | | fnfvelrn 7036 |
. . . . . . . . . . . . . 14
β’
((((β Γ {π΄}) βf Β· πΉ) Fn β β§ π¦ β β) β
(((β Γ {π΄})
βf Β· πΉ)βπ¦) β ran ((β Γ {π΄}) βf Β·
πΉ)) |
118 | 99, 117 | sylan 581 |
. . . . . . . . . . . . 13
β’ (((π β§ π΄ β 0) β§ π¦ β β) β (((β Γ
{π΄}) βf
Β· πΉ)βπ¦) β ran ((β Γ
{π΄}) βf
Β· πΉ)) |
119 | 85, 118 | eqeltrrd 2839 |
. . . . . . . . . . . 12
β’ (((π β§ π΄ β 0) β§ π¦ β β) β (π΄ Β· (πΉβπ¦)) β ran ((β Γ {π΄}) βf Β·
πΉ)) |
120 | 119 | ralrimiva 3144 |
. . . . . . . . . . 11
β’ ((π β§ π΄ β 0) β βπ¦ β β (π΄ Β· (πΉβπ¦)) β ran ((β Γ {π΄}) βf Β·
πΉ)) |
121 | | oveq2 7370 |
. . . . . . . . . . . . . 14
β’ (π = (πΉβπ¦) β (π΄ Β· π) = (π΄ Β· (πΉβπ¦))) |
122 | 121 | eleq1d 2823 |
. . . . . . . . . . . . 13
β’ (π = (πΉβπ¦) β ((π΄ Β· π) β ran ((β Γ {π΄}) βf Β·
πΉ) β (π΄ Β· (πΉβπ¦)) β ran ((β Γ {π΄}) βf Β·
πΉ))) |
123 | 122 | ralrn 7043 |
. . . . . . . . . . . 12
β’ (πΉ Fn β β
(βπ β ran πΉ(π΄ Β· π) β ran ((β Γ {π΄}) βf Β·
πΉ) β βπ¦ β β (π΄ Β· (πΉβπ¦)) β ran ((β Γ {π΄}) βf Β·
πΉ))) |
124 | 94, 123 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π΄ β 0) β (βπ β ran πΉ(π΄ Β· π) β ran ((β Γ {π΄}) βf Β·
πΉ) β βπ¦ β β (π΄ Β· (πΉβπ¦)) β ran ((β Γ {π΄}) βf Β·
πΉ))) |
125 | 120, 124 | mpbird 257 |
. . . . . . . . . 10
β’ ((π β§ π΄ β 0) β βπ β ran πΉ(π΄ Β· π) β ran ((β Γ {π΄}) βf Β·
πΉ)) |
126 | 125 | r19.21bi 3237 |
. . . . . . . . 9
β’ (((π β§ π΄ β 0) β§ π β ran πΉ) β (π΄ Β· π) β ran ((β Γ {π΄}) βf Β·
πΉ)) |
127 | 116, 126 | sylan2 594 |
. . . . . . . 8
β’ (((π β§ π΄ β 0) β§ π β (ran πΉ β {0})) β (π΄ Β· π) β ran ((β Γ {π΄}) βf Β·
πΉ)) |
128 | 36 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π΄ β 0) β§ π β (ran πΉ β {0})) β π΄ β β) |
129 | 87 | frnd 6681 |
. . . . . . . . . . . 12
β’ ((π β§ π΄ β 0) β ran πΉ β β) |
130 | 129 | ssdifssd 4107 |
. . . . . . . . . . 11
β’ ((π β§ π΄ β 0) β (ran πΉ β {0}) β
β) |
131 | 130 | sselda 3949 |
. . . . . . . . . 10
β’ (((π β§ π΄ β 0) β§ π β (ran πΉ β {0})) β π β β) |
132 | 131 | recnd 11190 |
. . . . . . . . 9
β’ (((π β§ π΄ β 0) β§ π β (ran πΉ β {0})) β π β β) |
133 | | simplr 768 |
. . . . . . . . 9
β’ (((π β§ π΄ β 0) β§ π β (ran πΉ β {0})) β π΄ β 0) |
134 | | eldifsni 4755 |
. . . . . . . . . 10
β’ (π β (ran πΉ β {0}) β π β 0) |
135 | 134 | adantl 483 |
. . . . . . . . 9
β’ (((π β§ π΄ β 0) β§ π β (ran πΉ β {0})) β π β 0) |
136 | 128, 132,
133, 135 | mulne0d 11814 |
. . . . . . . 8
β’ (((π β§ π΄ β 0) β§ π β (ran πΉ β {0})) β (π΄ Β· π) β 0) |
137 | | eldifsn 4752 |
. . . . . . . 8
β’ ((π΄ Β· π) β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0}) β
((π΄ Β· π) β ran ((β Γ
{π΄}) βf
Β· πΉ) β§ (π΄ Β· π) β 0)) |
138 | 127, 136,
137 | sylanbrc 584 |
. . . . . . 7
β’ (((π β§ π΄ β 0) β§ π β (ran πΉ β {0})) β (π΄ Β· π) β (ran ((β Γ {π΄}) βf Β·
πΉ) β
{0})) |
139 | | simpl 484 |
. . . . . . . . . . . 12
β’ ((π β (ran ((β Γ
{π΄}) βf
Β· πΉ) β {0})
β§ π β (ran πΉ β {0})) β π β (ran ((β Γ
{π΄}) βf
Β· πΉ) β
{0})) |
140 | | ssel2 3944 |
. . . . . . . . . . . 12
β’ (((ran
((β Γ {π΄})
βf Β· πΉ) β {0}) β β β§ π β (ran ((β Γ
{π΄}) βf
Β· πΉ) β {0}))
β π β
β) |
141 | 32, 139, 140 | syl2an 597 |
. . . . . . . . . . 11
β’ (((π β§ π΄ β 0) β§ (π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0}) β§ π β (ran πΉ β {0}))) β π β β) |
142 | 141 | recnd 11190 |
. . . . . . . . . 10
β’ (((π β§ π΄ β 0) β§ (π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0}) β§ π β (ran πΉ β {0}))) β π β β) |
143 | 8 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π΄ β 0) β§ (π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0}) β§ π β (ran πΉ β {0}))) β π΄ β β) |
144 | 143 | recnd 11190 |
. . . . . . . . . 10
β’ (((π β§ π΄ β 0) β§ (π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0}) β§ π β (ran πΉ β {0}))) β π΄ β β) |
145 | 131 | adantrl 715 |
. . . . . . . . . . 11
β’ (((π β§ π΄ β 0) β§ (π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0}) β§ π β (ran πΉ β {0}))) β π β β) |
146 | 145 | recnd 11190 |
. . . . . . . . . 10
β’ (((π β§ π΄ β 0) β§ (π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0}) β§ π β (ran πΉ β {0}))) β π β β) |
147 | | simplr 768 |
. . . . . . . . . 10
β’ (((π β§ π΄ β 0) β§ (π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0}) β§ π β (ran πΉ β {0}))) β π΄ β 0) |
148 | 142, 144,
146, 147 | divmuld 11960 |
. . . . . . . . 9
β’ (((π β§ π΄ β 0) β§ (π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0}) β§ π β (ran πΉ β {0}))) β ((π / π΄) = π β (π΄ Β· π) = π)) |
149 | 148 | bicomd 222 |
. . . . . . . 8
β’ (((π β§ π΄ β 0) β§ (π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0}) β§ π β (ran πΉ β {0}))) β ((π΄ Β· π) = π β (π / π΄) = π)) |
150 | | eqcom 2744 |
. . . . . . . 8
β’ (π = (π΄ Β· π) β (π΄ Β· π) = π) |
151 | | eqcom 2744 |
. . . . . . . 8
β’ (π = (π / π΄) β (π / π΄) = π) |
152 | 149, 150,
151 | 3bitr4g 314 |
. . . . . . 7
β’ (((π β§ π΄ β 0) β§ (π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0}) β§ π β (ran πΉ β {0}))) β (π = (π΄ Β· π) β π = (π / π΄))) |
153 | 79, 115, 138, 152 | f1o2d 7612 |
. . . . . 6
β’ ((π β§ π΄ β 0) β (π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0}) β¦
(π / π΄)):(ran ((β Γ {π΄}) βf Β· πΉ) β {0})β1-1-ontoβ(ran πΉ β {0})) |
154 | | oveq1 7369 |
. . . . . . . 8
β’ (π = π β (π / π΄) = (π / π΄)) |
155 | | ovex 7395 |
. . . . . . . 8
β’ (π / π΄) β V |
156 | 154, 79, 155 | fvmpt 6953 |
. . . . . . 7
β’ (π β (ran ((β Γ
{π΄}) βf
Β· πΉ) β {0})
β ((π β (ran
((β Γ {π΄})
βf Β· πΉ) β {0}) β¦ (π / π΄))βπ) = (π / π΄)) |
157 | 156 | adantl 483 |
. . . . . 6
β’ (((π β§ π΄ β 0) β§ π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
((π β (ran ((β
Γ {π΄})
βf Β· πΉ) β {0}) β¦ (π / π΄))βπ) = (π / π΄)) |
158 | | i1fima2sn 25060 |
. . . . . . . . 9
β’ ((πΉ β dom β«1
β§ π β (ran πΉ β {0})) β
(volβ(β‘πΉ β {π})) β β) |
159 | 71, 158 | sylan 581 |
. . . . . . . 8
β’ (((π β§ π΄ β 0) β§ π β (ran πΉ β {0})) β (volβ(β‘πΉ β {π})) β β) |
160 | 131, 159 | remulcld 11192 |
. . . . . . 7
β’ (((π β§ π΄ β 0) β§ π β (ran πΉ β {0})) β (π Β· (volβ(β‘πΉ β {π}))) β β) |
161 | 160 | recnd 11190 |
. . . . . 6
β’ (((π β§ π΄ β 0) β§ π β (ran πΉ β {0})) β (π Β· (volβ(β‘πΉ β {π}))) β β) |
162 | 78, 65, 153, 157, 161 | fsumf1o 15615 |
. . . . 5
β’ ((π β§ π΄ β 0) β Ξ£π β (ran πΉ β {0})(π Β· (volβ(β‘πΉ β {π}))) = Ξ£π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})((π / π΄) Β· (volβ(β‘πΉ β {(π / π΄)})))) |
163 | 73, 162 | eqtrd 2777 |
. . . 4
β’ ((π β§ π΄ β 0) β
(β«1βπΉ)
= Ξ£π β (ran
((β Γ {π΄})
βf Β· πΉ) β {0})((π / π΄) Β· (volβ(β‘πΉ β {(π / π΄)})))) |
164 | 163 | oveq2d 7378 |
. . 3
β’ ((π β§ π΄ β 0) β (π΄ Β· (β«1βπΉ)) = (π΄ Β· Ξ£π β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})((π / π΄) Β· (volβ(β‘πΉ β {(π / π΄)}))))) |
165 | 68, 70, 164 | 3eqtr4d 2787 |
. 2
β’ ((π β§ π΄ β 0) β
(β«1β((β Γ {π΄}) βf Β· πΉ)) = (π΄ Β· (β«1βπΉ))) |
166 | 26, 165 | pm2.61dane 3033 |
1
β’ (π β
(β«1β((β Γ {π΄}) βf Β· πΉ)) = (π΄ Β· (β«1βπΉ))) |