Step | Hyp | Ref
| Expression |
1 | | remulcl 11143 |
. . . 4
β’ ((π₯ β β β§ π¦ β β) β (π₯ Β· π¦) β β) |
2 | 1 | adantl 483 |
. . 3
β’ ((π β§ (π₯ β β β§ π¦ β β)) β (π₯ Β· π¦) β β) |
3 | | i1fadd.1 |
. . . 4
β’ (π β πΉ β dom
β«1) |
4 | | i1ff 25056 |
. . . 4
β’ (πΉ β dom β«1
β πΉ:ββΆβ) |
5 | 3, 4 | syl 17 |
. . 3
β’ (π β πΉ:ββΆβ) |
6 | | i1fadd.2 |
. . . 4
β’ (π β πΊ β dom
β«1) |
7 | | i1ff 25056 |
. . . 4
β’ (πΊ β dom β«1
β πΊ:ββΆβ) |
8 | 6, 7 | syl 17 |
. . 3
β’ (π β πΊ:ββΆβ) |
9 | | reex 11149 |
. . . 4
β’ β
β V |
10 | 9 | a1i 11 |
. . 3
β’ (π β β β
V) |
11 | | inidm 4183 |
. . 3
β’ (β
β© β) = β |
12 | 2, 5, 8, 10, 10, 11 | off 7640 |
. 2
β’ (π β (πΉ βf Β· πΊ):ββΆβ) |
13 | | i1frn 25057 |
. . . . . 6
β’ (πΉ β dom β«1
β ran πΉ β
Fin) |
14 | 3, 13 | syl 17 |
. . . . 5
β’ (π β ran πΉ β Fin) |
15 | | i1frn 25057 |
. . . . . 6
β’ (πΊ β dom β«1
β ran πΊ β
Fin) |
16 | 6, 15 | syl 17 |
. . . . 5
β’ (π β ran πΊ β Fin) |
17 | | xpfi 9268 |
. . . . 5
β’ ((ran
πΉ β Fin β§ ran
πΊ β Fin) β (ran
πΉ Γ ran πΊ) β Fin) |
18 | 14, 16, 17 | syl2anc 585 |
. . . 4
β’ (π β (ran πΉ Γ ran πΊ) β Fin) |
19 | | eqid 2737 |
. . . . . 6
β’ (π’ β ran πΉ, π£ β ran πΊ β¦ (π’ Β· π£)) = (π’ β ran πΉ, π£ β ran πΊ β¦ (π’ Β· π£)) |
20 | | ovex 7395 |
. . . . . 6
β’ (π’ Β· π£) β V |
21 | 19, 20 | fnmpoi 8007 |
. . . . 5
β’ (π’ β ran πΉ, π£ β ran πΊ β¦ (π’ Β· π£)) Fn (ran πΉ Γ ran πΊ) |
22 | | dffn4 6767 |
. . . . 5
β’ ((π’ β ran πΉ, π£ β ran πΊ β¦ (π’ Β· π£)) Fn (ran πΉ Γ ran πΊ) β (π’ β ran πΉ, π£ β ran πΊ β¦ (π’ Β· π£)):(ran πΉ Γ ran πΊ)βontoβran (π’ β ran πΉ, π£ β ran πΊ β¦ (π’ Β· π£))) |
23 | 21, 22 | mpbi 229 |
. . . 4
β’ (π’ β ran πΉ, π£ β ran πΊ β¦ (π’ Β· π£)):(ran πΉ Γ ran πΊ)βontoβran (π’ β ran πΉ, π£ β ran πΊ β¦ (π’ Β· π£)) |
24 | | fofi 9289 |
. . . 4
β’ (((ran
πΉ Γ ran πΊ) β Fin β§ (π’ β ran πΉ, π£ β ran πΊ β¦ (π’ Β· π£)):(ran πΉ Γ ran πΊ)βontoβran (π’ β ran πΉ, π£ β ran πΊ β¦ (π’ Β· π£))) β ran (π’ β ran πΉ, π£ β ran πΊ β¦ (π’ Β· π£)) β Fin) |
25 | 18, 23, 24 | sylancl 587 |
. . 3
β’ (π β ran (π’ β ran πΉ, π£ β ran πΊ β¦ (π’ Β· π£)) β Fin) |
26 | | eqid 2737 |
. . . . . . . . 9
β’ (π₯ Β· π¦) = (π₯ Β· π¦) |
27 | | rspceov 7409 |
. . . . . . . . 9
β’ ((π₯ β ran πΉ β§ π¦ β ran πΊ β§ (π₯ Β· π¦) = (π₯ Β· π¦)) β βπ’ β ran πΉβπ£ β ran πΊ(π₯ Β· π¦) = (π’ Β· π£)) |
28 | 26, 27 | mp3an3 1451 |
. . . . . . . 8
β’ ((π₯ β ran πΉ β§ π¦ β ran πΊ) β βπ’ β ran πΉβπ£ β ran πΊ(π₯ Β· π¦) = (π’ Β· π£)) |
29 | | ovex 7395 |
. . . . . . . . 9
β’ (π₯ Β· π¦) β V |
30 | | eqeq1 2741 |
. . . . . . . . . 10
β’ (π€ = (π₯ Β· π¦) β (π€ = (π’ Β· π£) β (π₯ Β· π¦) = (π’ Β· π£))) |
31 | 30 | 2rexbidv 3214 |
. . . . . . . . 9
β’ (π€ = (π₯ Β· π¦) β (βπ’ β ran πΉβπ£ β ran πΊ π€ = (π’ Β· π£) β βπ’ β ran πΉβπ£ β ran πΊ(π₯ Β· π¦) = (π’ Β· π£))) |
32 | 29, 31 | elab 3635 |
. . . . . . . 8
β’ ((π₯ Β· π¦) β {π€ β£ βπ’ β ran πΉβπ£ β ran πΊ π€ = (π’ Β· π£)} β βπ’ β ran πΉβπ£ β ran πΊ(π₯ Β· π¦) = (π’ Β· π£)) |
33 | 28, 32 | sylibr 233 |
. . . . . . 7
β’ ((π₯ β ran πΉ β§ π¦ β ran πΊ) β (π₯ Β· π¦) β {π€ β£ βπ’ β ran πΉβπ£ β ran πΊ π€ = (π’ Β· π£)}) |
34 | 33 | adantl 483 |
. . . . . 6
β’ ((π β§ (π₯ β ran πΉ β§ π¦ β ran πΊ)) β (π₯ Β· π¦) β {π€ β£ βπ’ β ran πΉβπ£ β ran πΊ π€ = (π’ Β· π£)}) |
35 | 5 | ffnd 6674 |
. . . . . . 7
β’ (π β πΉ Fn β) |
36 | | dffn3 6686 |
. . . . . . 7
β’ (πΉ Fn β β πΉ:ββΆran πΉ) |
37 | 35, 36 | sylib 217 |
. . . . . 6
β’ (π β πΉ:ββΆran πΉ) |
38 | 8 | ffnd 6674 |
. . . . . . 7
β’ (π β πΊ Fn β) |
39 | | dffn3 6686 |
. . . . . . 7
β’ (πΊ Fn β β πΊ:ββΆran πΊ) |
40 | 38, 39 | sylib 217 |
. . . . . 6
β’ (π β πΊ:ββΆran πΊ) |
41 | 34, 37, 40, 10, 10, 11 | off 7640 |
. . . . 5
β’ (π β (πΉ βf Β· πΊ):ββΆ{π€ β£ βπ’ β ran πΉβπ£ β ran πΊ π€ = (π’ Β· π£)}) |
42 | 41 | frnd 6681 |
. . . 4
β’ (π β ran (πΉ βf Β· πΊ) β {π€ β£ βπ’ β ran πΉβπ£ β ran πΊ π€ = (π’ Β· π£)}) |
43 | 19 | rnmpo 7494 |
. . . 4
β’ ran
(π’ β ran πΉ, π£ β ran πΊ β¦ (π’ Β· π£)) = {π€ β£ βπ’ β ran πΉβπ£ β ran πΊ π€ = (π’ Β· π£)} |
44 | 42, 43 | sseqtrrdi 4000 |
. . 3
β’ (π β ran (πΉ βf Β· πΊ) β ran (π’ β ran πΉ, π£ β ran πΊ β¦ (π’ Β· π£))) |
45 | 25, 44 | ssfid 9218 |
. 2
β’ (π β ran (πΉ βf Β· πΊ) β Fin) |
46 | 12 | frnd 6681 |
. . . . . . 7
β’ (π β ran (πΉ βf Β· πΊ) β
β) |
47 | | ax-resscn 11115 |
. . . . . . 7
β’ β
β β |
48 | 46, 47 | sstrdi 3961 |
. . . . . 6
β’ (π β ran (πΉ βf Β· πΊ) β
β) |
49 | 48 | ssdifd 4105 |
. . . . 5
β’ (π β (ran (πΉ βf Β· πΊ) β {0}) β (β
β {0})) |
50 | 49 | sselda 3949 |
. . . 4
β’ ((π β§ π¦ β (ran (πΉ βf Β· πΊ) β {0})) β π¦ β (β β
{0})) |
51 | 3, 6 | i1fmullem 25074 |
. . . 4
β’ ((π β§ π¦ β (β β {0})) β (β‘(πΉ βf Β· πΊ) β {π¦}) = βͺ
π§ β (ran πΊ β {0})((β‘πΉ β {(π¦ / π§)}) β© (β‘πΊ β {π§}))) |
52 | 50, 51 | syldan 592 |
. . 3
β’ ((π β§ π¦ β (ran (πΉ βf Β· πΊ) β {0})) β (β‘(πΉ βf Β· πΊ) β {π¦}) = βͺ
π§ β (ran πΊ β {0})((β‘πΉ β {(π¦ / π§)}) β© (β‘πΊ β {π§}))) |
53 | | difss 4096 |
. . . . . 6
β’ (ran
πΊ β {0}) β ran
πΊ |
54 | | ssfi 9124 |
. . . . . 6
β’ ((ran
πΊ β Fin β§ (ran
πΊ β {0}) β ran
πΊ) β (ran πΊ β {0}) β
Fin) |
55 | 16, 53, 54 | sylancl 587 |
. . . . 5
β’ (π β (ran πΊ β {0}) β Fin) |
56 | | i1fima 25058 |
. . . . . . . 8
β’ (πΉ β dom β«1
β (β‘πΉ β {(π¦ / π§)}) β dom vol) |
57 | 3, 56 | syl 17 |
. . . . . . 7
β’ (π β (β‘πΉ β {(π¦ / π§)}) β dom vol) |
58 | | i1fima 25058 |
. . . . . . . 8
β’ (πΊ β dom β«1
β (β‘πΊ β {π§}) β dom vol) |
59 | 6, 58 | syl 17 |
. . . . . . 7
β’ (π β (β‘πΊ β {π§}) β dom vol) |
60 | | inmbl 24922 |
. . . . . . 7
β’ (((β‘πΉ β {(π¦ / π§)}) β dom vol β§ (β‘πΊ β {π§}) β dom vol) β ((β‘πΉ β {(π¦ / π§)}) β© (β‘πΊ β {π§})) β dom vol) |
61 | 57, 59, 60 | syl2anc 585 |
. . . . . 6
β’ (π β ((β‘πΉ β {(π¦ / π§)}) β© (β‘πΊ β {π§})) β dom vol) |
62 | 61 | ralrimivw 3148 |
. . . . 5
β’ (π β βπ§ β (ran πΊ β {0})((β‘πΉ β {(π¦ / π§)}) β© (β‘πΊ β {π§})) β dom vol) |
63 | | finiunmbl 24924 |
. . . . 5
β’ (((ran
πΊ β {0}) β Fin
β§ βπ§ β (ran
πΊ β {0})((β‘πΉ β {(π¦ / π§)}) β© (β‘πΊ β {π§})) β dom vol) β βͺ π§ β (ran πΊ β {0})((β‘πΉ β {(π¦ / π§)}) β© (β‘πΊ β {π§})) β dom vol) |
64 | 55, 62, 63 | syl2anc 585 |
. . . 4
β’ (π β βͺ π§ β (ran πΊ β {0})((β‘πΉ β {(π¦ / π§)}) β© (β‘πΊ β {π§})) β dom vol) |
65 | 64 | adantr 482 |
. . 3
β’ ((π β§ π¦ β (ran (πΉ βf Β· πΊ) β {0})) β βͺ π§ β (ran πΊ β {0})((β‘πΉ β {(π¦ / π§)}) β© (β‘πΊ β {π§})) β dom vol) |
66 | 52, 65 | eqeltrd 2838 |
. 2
β’ ((π β§ π¦ β (ran (πΉ βf Β· πΊ) β {0})) β (β‘(πΉ βf Β· πΊ) β {π¦}) β dom vol) |
67 | | mblvol 24910 |
. . . 4
β’ ((β‘(πΉ βf Β· πΊ) β {π¦}) β dom vol β (volβ(β‘(πΉ βf Β· πΊ) β {π¦})) = (vol*β(β‘(πΉ βf Β· πΊ) β {π¦}))) |
68 | 66, 67 | syl 17 |
. . 3
β’ ((π β§ π¦ β (ran (πΉ βf Β· πΊ) β {0})) β
(volβ(β‘(πΉ βf Β· πΊ) β {π¦})) = (vol*β(β‘(πΉ βf Β· πΊ) β {π¦}))) |
69 | | mblss 24911 |
. . . . 5
β’ ((β‘(πΉ βf Β· πΊ) β {π¦}) β dom vol β (β‘(πΉ βf Β· πΊ) β {π¦}) β β) |
70 | 66, 69 | syl 17 |
. . . 4
β’ ((π β§ π¦ β (ran (πΉ βf Β· πΊ) β {0})) β (β‘(πΉ βf Β· πΊ) β {π¦}) β β) |
71 | 55 | adantr 482 |
. . . . 5
β’ ((π β§ π¦ β (ran (πΉ βf Β· πΊ) β {0})) β (ran
πΊ β {0}) β
Fin) |
72 | | inss2 4194 |
. . . . . . 7
β’ ((β‘πΉ β {(π¦ / π§)}) β© (β‘πΊ β {π§})) β (β‘πΊ β {π§}) |
73 | 72 | a1i 11 |
. . . . . 6
β’ (((π β§ π¦ β (ran (πΉ βf Β· πΊ) β {0})) β§ π§ β (ran πΊ β {0})) β ((β‘πΉ β {(π¦ / π§)}) β© (β‘πΊ β {π§})) β (β‘πΊ β {π§})) |
74 | 59 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π¦ β (ran (πΉ βf Β· πΊ) β {0})) β§ π§ β (ran πΊ β {0})) β (β‘πΊ β {π§}) β dom vol) |
75 | | mblss 24911 |
. . . . . . 7
β’ ((β‘πΊ β {π§}) β dom vol β (β‘πΊ β {π§}) β β) |
76 | 74, 75 | syl 17 |
. . . . . 6
β’ (((π β§ π¦ β (ran (πΉ βf Β· πΊ) β {0})) β§ π§ β (ran πΊ β {0})) β (β‘πΊ β {π§}) β β) |
77 | | mblvol 24910 |
. . . . . . . 8
β’ ((β‘πΊ β {π§}) β dom vol β (volβ(β‘πΊ β {π§})) = (vol*β(β‘πΊ β {π§}))) |
78 | 74, 77 | syl 17 |
. . . . . . 7
β’ (((π β§ π¦ β (ran (πΉ βf Β· πΊ) β {0})) β§ π§ β (ran πΊ β {0})) β (volβ(β‘πΊ β {π§})) = (vol*β(β‘πΊ β {π§}))) |
79 | 6 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π¦ β (ran (πΉ βf Β· πΊ) β {0})) β πΊ β dom
β«1) |
80 | | i1fima2sn 25060 |
. . . . . . . 8
β’ ((πΊ β dom β«1
β§ π§ β (ran πΊ β {0})) β
(volβ(β‘πΊ β {π§})) β β) |
81 | 79, 80 | sylan 581 |
. . . . . . 7
β’ (((π β§ π¦ β (ran (πΉ βf Β· πΊ) β {0})) β§ π§ β (ran πΊ β {0})) β (volβ(β‘πΊ β {π§})) β β) |
82 | 78, 81 | eqeltrrd 2839 |
. . . . . 6
β’ (((π β§ π¦ β (ran (πΉ βf Β· πΊ) β {0})) β§ π§ β (ran πΊ β {0})) β (vol*β(β‘πΊ β {π§})) β β) |
83 | | ovolsscl 24866 |
. . . . . 6
β’ ((((β‘πΉ β {(π¦ / π§)}) β© (β‘πΊ β {π§})) β (β‘πΊ β {π§}) β§ (β‘πΊ β {π§}) β β β§ (vol*β(β‘πΊ β {π§})) β β) β
(vol*β((β‘πΉ β {(π¦ / π§)}) β© (β‘πΊ β {π§}))) β β) |
84 | 73, 76, 82, 83 | syl3anc 1372 |
. . . . 5
β’ (((π β§ π¦ β (ran (πΉ βf Β· πΊ) β {0})) β§ π§ β (ran πΊ β {0})) β (vol*β((β‘πΉ β {(π¦ / π§)}) β© (β‘πΊ β {π§}))) β β) |
85 | 71, 84 | fsumrecl 15626 |
. . . 4
β’ ((π β§ π¦ β (ran (πΉ βf Β· πΊ) β {0})) β
Ξ£π§ β (ran πΊ β {0})(vol*β((β‘πΉ β {(π¦ / π§)}) β© (β‘πΊ β {π§}))) β β) |
86 | 52 | fveq2d 6851 |
. . . . 5
β’ ((π β§ π¦ β (ran (πΉ βf Β· πΊ) β {0})) β
(vol*β(β‘(πΉ βf Β· πΊ) β {π¦})) = (vol*ββͺ π§ β (ran πΊ β {0})((β‘πΉ β {(π¦ / π§)}) β© (β‘πΊ β {π§})))) |
87 | | mblss 24911 |
. . . . . . . . . 10
β’ (((β‘πΉ β {(π¦ / π§)}) β© (β‘πΊ β {π§})) β dom vol β ((β‘πΉ β {(π¦ / π§)}) β© (β‘πΊ β {π§})) β β) |
88 | 61, 87 | syl 17 |
. . . . . . . . 9
β’ (π β ((β‘πΉ β {(π¦ / π§)}) β© (β‘πΊ β {π§})) β β) |
89 | 88 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π¦ β (ran (πΉ βf Β· πΊ) β {0})) β§ π§ β (ran πΊ β {0})) β ((β‘πΉ β {(π¦ / π§)}) β© (β‘πΊ β {π§})) β β) |
90 | 89, 84 | jca 513 |
. . . . . . 7
β’ (((π β§ π¦ β (ran (πΉ βf Β· πΊ) β {0})) β§ π§ β (ran πΊ β {0})) β (((β‘πΉ β {(π¦ / π§)}) β© (β‘πΊ β {π§})) β β β§ (vol*β((β‘πΉ β {(π¦ / π§)}) β© (β‘πΊ β {π§}))) β β)) |
91 | 90 | ralrimiva 3144 |
. . . . . 6
β’ ((π β§ π¦ β (ran (πΉ βf Β· πΊ) β {0})) β
βπ§ β (ran πΊ β {0})(((β‘πΉ β {(π¦ / π§)}) β© (β‘πΊ β {π§})) β β β§ (vol*β((β‘πΉ β {(π¦ / π§)}) β© (β‘πΊ β {π§}))) β β)) |
92 | | ovolfiniun 24881 |
. . . . . 6
β’ (((ran
πΊ β {0}) β Fin
β§ βπ§ β (ran
πΊ β {0})(((β‘πΉ β {(π¦ / π§)}) β© (β‘πΊ β {π§})) β β β§ (vol*β((β‘πΉ β {(π¦ / π§)}) β© (β‘πΊ β {π§}))) β β)) β
(vol*ββͺ π§ β (ran πΊ β {0})((β‘πΉ β {(π¦ / π§)}) β© (β‘πΊ β {π§}))) β€ Ξ£π§ β (ran πΊ β {0})(vol*β((β‘πΉ β {(π¦ / π§)}) β© (β‘πΊ β {π§})))) |
93 | 71, 91, 92 | syl2anc 585 |
. . . . 5
β’ ((π β§ π¦ β (ran (πΉ βf Β· πΊ) β {0})) β
(vol*ββͺ π§ β (ran πΊ β {0})((β‘πΉ β {(π¦ / π§)}) β© (β‘πΊ β {π§}))) β€ Ξ£π§ β (ran πΊ β {0})(vol*β((β‘πΉ β {(π¦ / π§)}) β© (β‘πΊ β {π§})))) |
94 | 86, 93 | eqbrtrd 5132 |
. . . 4
β’ ((π β§ π¦ β (ran (πΉ βf Β· πΊ) β {0})) β
(vol*β(β‘(πΉ βf Β· πΊ) β {π¦})) β€ Ξ£π§ β (ran πΊ β {0})(vol*β((β‘πΉ β {(π¦ / π§)}) β© (β‘πΊ β {π§})))) |
95 | | ovollecl 24863 |
. . . 4
β’ (((β‘(πΉ βf Β· πΊ) β {π¦}) β β β§ Ξ£π§ β (ran πΊ β {0})(vol*β((β‘πΉ β {(π¦ / π§)}) β© (β‘πΊ β {π§}))) β β β§ (vol*β(β‘(πΉ βf Β· πΊ) β {π¦})) β€ Ξ£π§ β (ran πΊ β {0})(vol*β((β‘πΉ β {(π¦ / π§)}) β© (β‘πΊ β {π§})))) β (vol*β(β‘(πΉ βf Β· πΊ) β {π¦})) β β) |
96 | 70, 85, 94, 95 | syl3anc 1372 |
. . 3
β’ ((π β§ π¦ β (ran (πΉ βf Β· πΊ) β {0})) β
(vol*β(β‘(πΉ βf Β· πΊ) β {π¦})) β β) |
97 | 68, 96 | eqeltrd 2838 |
. 2
β’ ((π β§ π¦ β (ran (πΉ βf Β· πΊ) β {0})) β
(volβ(β‘(πΉ βf Β· πΊ) β {π¦})) β β) |
98 | 12, 45, 66, 97 | i1fd 25061 |
1
β’ (π β (πΉ βf Β· πΊ) β dom
β«1) |