Step | Hyp | Ref
| Expression |
1 | | readdcl 11135 |
. . . 4
β’ ((π₯ β β β§ π¦ β β) β (π₯ + π¦) β β) |
2 | 1 | adantl 483 |
. . 3
β’ ((π β§ (π₯ β β β§ π¦ β β)) β (π₯ + π¦) β β) |
3 | | i1fadd.1 |
. . . 4
β’ (π β πΉ β dom
β«1) |
4 | | i1ff 25043 |
. . . 4
β’ (πΉ β dom β«1
β πΉ:ββΆβ) |
5 | 3, 4 | syl 17 |
. . 3
β’ (π β πΉ:ββΆβ) |
6 | | i1fadd.2 |
. . . 4
β’ (π β πΊ β dom
β«1) |
7 | | i1ff 25043 |
. . . 4
β’ (πΊ β dom β«1
β πΊ:ββΆβ) |
8 | 6, 7 | syl 17 |
. . 3
β’ (π β πΊ:ββΆβ) |
9 | | reex 11143 |
. . . 4
β’ β
β V |
10 | 9 | a1i 11 |
. . 3
β’ (π β β β
V) |
11 | | inidm 4179 |
. . 3
β’ (β
β© β) = β |
12 | 2, 5, 8, 10, 10, 11 | off 7636 |
. 2
β’ (π β (πΉ βf + πΊ):ββΆβ) |
13 | | i1frn 25044 |
. . . . . 6
β’ (πΉ β dom β«1
β ran πΉ β
Fin) |
14 | 3, 13 | syl 17 |
. . . . 5
β’ (π β ran πΉ β Fin) |
15 | | i1frn 25044 |
. . . . . 6
β’ (πΊ β dom β«1
β ran πΊ β
Fin) |
16 | 6, 15 | syl 17 |
. . . . 5
β’ (π β ran πΊ β Fin) |
17 | | xpfi 9262 |
. . . . 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 7391 |
. . . . . 6
β’ (π’ + π£) β V |
21 | 19, 20 | fnmpoi 8003 |
. . . . 5
β’ (π’ β ran πΉ, π£ β ran πΊ β¦ (π’ + π£)) Fn (ran πΉ Γ ran πΊ) |
22 | | dffn4 6763 |
. . . . 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 9283 |
. . . 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 7405 |
. . . . . . . . 9
β’ ((π₯ β ran πΉ β§ π¦ β ran πΊ β§ (π₯ + π¦) = (π₯ + π¦)) β βπ’ β ran πΉβπ£ β ran πΊ(π₯ + π¦) = (π’ + π£)) |
28 | 26, 27 | mp3an3 1451 |
. . . . . . . 8
β’ ((π₯ β ran πΉ β§ π¦ β ran πΊ) β βπ’ β ran πΉβπ£ β ran πΊ(π₯ + π¦) = (π’ + π£)) |
29 | | ovex 7391 |
. . . . . . . . 9
β’ (π₯ + π¦) β V |
30 | | eqeq1 2741 |
. . . . . . . . . 10
β’ (π€ = (π₯ + π¦) β (π€ = (π’ + π£) β (π₯ + π¦) = (π’ + π£))) |
31 | 30 | 2rexbidv 3214 |
. . . . . . . . 9
β’ (π€ = (π₯ + π¦) β (βπ’ β ran πΉβπ£ β ran πΊ π€ = (π’ + π£) β βπ’ β ran πΉβπ£ β ran πΊ(π₯ + π¦) = (π’ + π£))) |
32 | 29, 31 | elab 3631 |
. . . . . . . 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 6670 |
. . . . . . 7
β’ (π β πΉ Fn β) |
36 | | dffn3 6682 |
. . . . . . 7
β’ (πΉ Fn β β πΉ:ββΆran πΉ) |
37 | 35, 36 | sylib 217 |
. . . . . 6
β’ (π β πΉ:ββΆran πΉ) |
38 | 8 | ffnd 6670 |
. . . . . . 7
β’ (π β πΊ Fn β) |
39 | | dffn3 6682 |
. . . . . . 7
β’ (πΊ Fn β β πΊ:ββΆran πΊ) |
40 | 38, 39 | sylib 217 |
. . . . . 6
β’ (π β πΊ:ββΆran πΊ) |
41 | 34, 37, 40, 10, 10, 11 | off 7636 |
. . . . 5
β’ (π β (πΉ βf + πΊ):ββΆ{π€ β£ βπ’ β ran πΉβπ£ β ran πΊ π€ = (π’ + π£)}) |
42 | 41 | frnd 6677 |
. . . 4
β’ (π β ran (πΉ βf + πΊ) β {π€ β£ βπ’ β ran πΉβπ£ β ran πΊ π€ = (π’ + π£)}) |
43 | 19 | rnmpo 7490 |
. . . 4
β’ ran
(π’ β ran πΉ, π£ β ran πΊ β¦ (π’ + π£)) = {π€ β£ βπ’ β ran πΉβπ£ β ran πΊ π€ = (π’ + π£)} |
44 | 42, 43 | sseqtrrdi 3996 |
. . 3
β’ (π β ran (πΉ βf + πΊ) β ran (π’ β ran πΉ, π£ β ran πΊ β¦ (π’ + π£))) |
45 | 25, 44 | ssfid 9212 |
. 2
β’ (π β ran (πΉ βf + πΊ) β Fin) |
46 | 12 | frnd 6677 |
. . . . . . 7
β’ (π β ran (πΉ βf + πΊ) β β) |
47 | 46 | ssdifssd 4103 |
. . . . . 6
β’ (π β (ran (πΉ βf + πΊ) β {0}) β
β) |
48 | 47 | sselda 3945 |
. . . . 5
β’ ((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β π¦ β β) |
49 | 48 | recnd 11184 |
. . . 4
β’ ((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β π¦ β β) |
50 | 3, 6 | i1faddlem 25060 |
. . . 4
β’ ((π β§ π¦ β β) β (β‘(πΉ βf + πΊ) β {π¦}) = βͺ
π§ β ran πΊ((β‘πΉ β {(π¦ β π§)}) β© (β‘πΊ β {π§}))) |
51 | 49, 50 | syldan 592 |
. . 3
β’ ((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β (β‘(πΉ βf + πΊ) β {π¦}) = βͺ
π§ β ran πΊ((β‘πΉ β {(π¦ β π§)}) β© (β‘πΊ β {π§}))) |
52 | 16 | adantr 482 |
. . . 4
β’ ((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β ran πΊ β Fin) |
53 | 3 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ π§ β ran πΊ) β πΉ β dom
β«1) |
54 | | i1fmbf 25042 |
. . . . . . . 8
β’ (πΉ β dom β«1
β πΉ β
MblFn) |
55 | 53, 54 | syl 17 |
. . . . . . 7
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ π§ β ran πΊ) β πΉ β MblFn) |
56 | 5 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ π§ β ran πΊ) β πΉ:ββΆβ) |
57 | 12 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ π§ β ran πΊ) β (πΉ βf + πΊ):ββΆβ) |
58 | 57 | frnd 6677 |
. . . . . . . . 9
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ π§ β ran πΊ) β ran (πΉ βf + πΊ) β β) |
59 | | eldifi 4087 |
. . . . . . . . . 10
β’ (π¦ β (ran (πΉ βf + πΊ) β {0}) β π¦ β ran (πΉ βf + πΊ)) |
60 | 59 | ad2antlr 726 |
. . . . . . . . 9
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ π§ β ran πΊ) β π¦ β ran (πΉ βf + πΊ)) |
61 | 58, 60 | sseldd 3946 |
. . . . . . . 8
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ π§ β ran πΊ) β π¦ β β) |
62 | 8 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β πΊ:ββΆβ) |
63 | 62 | frnd 6677 |
. . . . . . . . 9
β’ ((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β ran πΊ β β) |
64 | 63 | sselda 3945 |
. . . . . . . 8
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ π§ β ran πΊ) β π§ β β) |
65 | 61, 64 | resubcld 11584 |
. . . . . . 7
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ π§ β ran πΊ) β (π¦ β π§) β β) |
66 | | mbfimasn 24999 |
. . . . . . 7
β’ ((πΉ β MblFn β§ πΉ:ββΆβ β§
(π¦ β π§) β β) β (β‘πΉ β {(π¦ β π§)}) β dom vol) |
67 | 55, 56, 65, 66 | syl3anc 1372 |
. . . . . 6
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ π§ β ran πΊ) β (β‘πΉ β {(π¦ β π§)}) β dom vol) |
68 | 6 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ π§ β ran πΊ) β πΊ β dom
β«1) |
69 | | i1fmbf 25042 |
. . . . . . . 8
β’ (πΊ β dom β«1
β πΊ β
MblFn) |
70 | 68, 69 | syl 17 |
. . . . . . 7
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ π§ β ran πΊ) β πΊ β MblFn) |
71 | 8 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ π§ β ran πΊ) β πΊ:ββΆβ) |
72 | | mbfimasn 24999 |
. . . . . . 7
β’ ((πΊ β MblFn β§ πΊ:ββΆβ β§
π§ β β) β
(β‘πΊ β {π§}) β dom vol) |
73 | 70, 71, 64, 72 | syl3anc 1372 |
. . . . . 6
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ π§ β ran πΊ) β (β‘πΊ β {π§}) β dom vol) |
74 | | inmbl 24909 |
. . . . . 6
β’ (((β‘πΉ β {(π¦ β π§)}) β dom vol β§ (β‘πΊ β {π§}) β dom vol) β ((β‘πΉ β {(π¦ β π§)}) β© (β‘πΊ β {π§})) β dom vol) |
75 | 67, 73, 74 | syl2anc 585 |
. . . . 5
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ π§ β ran πΊ) β ((β‘πΉ β {(π¦ β π§)}) β© (β‘πΊ β {π§})) β dom vol) |
76 | 75 | ralrimiva 3144 |
. . . 4
β’ ((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β βπ§ β ran πΊ((β‘πΉ β {(π¦ β π§)}) β© (β‘πΊ β {π§})) β dom vol) |
77 | | finiunmbl 24911 |
. . . 4
β’ ((ran
πΊ β Fin β§
βπ§ β ran πΊ((β‘πΉ β {(π¦ β π§)}) β© (β‘πΊ β {π§})) β dom vol) β βͺ π§ β ran πΊ((β‘πΉ β {(π¦ β π§)}) β© (β‘πΊ β {π§})) β dom vol) |
78 | 52, 76, 77 | syl2anc 585 |
. . 3
β’ ((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β βͺ π§ β ran πΊ((β‘πΉ β {(π¦ β π§)}) β© (β‘πΊ β {π§})) β dom vol) |
79 | 51, 78 | eqeltrd 2838 |
. 2
β’ ((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β (β‘(πΉ βf + πΊ) β {π¦}) β dom vol) |
80 | | mblvol 24897 |
. . . 4
β’ ((β‘(πΉ βf + πΊ) β {π¦}) β dom vol β (volβ(β‘(πΉ βf + πΊ) β {π¦})) = (vol*β(β‘(πΉ βf + πΊ) β {π¦}))) |
81 | 79, 80 | syl 17 |
. . 3
β’ ((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β (volβ(β‘(πΉ βf + πΊ) β {π¦})) = (vol*β(β‘(πΉ βf + πΊ) β {π¦}))) |
82 | | mblss 24898 |
. . . . 5
β’ ((β‘(πΉ βf + πΊ) β {π¦}) β dom vol β (β‘(πΉ βf + πΊ) β {π¦}) β β) |
83 | 79, 82 | syl 17 |
. . . 4
β’ ((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β (β‘(πΉ βf + πΊ) β {π¦}) β β) |
84 | | inss1 4189 |
. . . . . . . 8
β’ ((β‘πΉ β {(π¦ β π§)}) β© (β‘πΊ β {π§})) β (β‘πΉ β {(π¦ β π§)}) |
85 | 67 | adantrr 716 |
. . . . . . . . 9
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ (π§ β ran πΊ β§ π§ = 0)) β (β‘πΉ β {(π¦ β π§)}) β dom vol) |
86 | | mblss 24898 |
. . . . . . . . 9
β’ ((β‘πΉ β {(π¦ β π§)}) β dom vol β (β‘πΉ β {(π¦ β π§)}) β β) |
87 | 85, 86 | syl 17 |
. . . . . . . 8
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ (π§ β ran πΊ β§ π§ = 0)) β (β‘πΉ β {(π¦ β π§)}) β β) |
88 | | mblvol 24897 |
. . . . . . . . . 10
β’ ((β‘πΉ β {(π¦ β π§)}) β dom vol β (volβ(β‘πΉ β {(π¦ β π§)})) = (vol*β(β‘πΉ β {(π¦ β π§)}))) |
89 | 85, 88 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ (π§ β ran πΊ β§ π§ = 0)) β (volβ(β‘πΉ β {(π¦ β π§)})) = (vol*β(β‘πΉ β {(π¦ β π§)}))) |
90 | | simprr 772 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ (π§ β ran πΊ β§ π§ = 0)) β π§ = 0) |
91 | 90 | oveq2d 7374 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ (π§ β ran πΊ β§ π§ = 0)) β (π¦ β π§) = (π¦ β 0)) |
92 | 49 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ (π§ β ran πΊ β§ π§ = 0)) β π¦ β β) |
93 | 92 | subid1d 11502 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ (π§ β ran πΊ β§ π§ = 0)) β (π¦ β 0) = π¦) |
94 | 91, 93 | eqtrd 2777 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ (π§ β ran πΊ β§ π§ = 0)) β (π¦ β π§) = π¦) |
95 | 94 | sneqd 4599 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ (π§ β ran πΊ β§ π§ = 0)) β {(π¦ β π§)} = {π¦}) |
96 | 95 | imaeq2d 6014 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ (π§ β ran πΊ β§ π§ = 0)) β (β‘πΉ β {(π¦ β π§)}) = (β‘πΉ β {π¦})) |
97 | 96 | fveq2d 6847 |
. . . . . . . . . 10
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ (π§ β ran πΊ β§ π§ = 0)) β (volβ(β‘πΉ β {(π¦ β π§)})) = (volβ(β‘πΉ β {π¦}))) |
98 | | i1fima2sn 25047 |
. . . . . . . . . . . 12
β’ ((πΉ β dom β«1
β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β
(volβ(β‘πΉ β {π¦})) β β) |
99 | 3, 98 | sylan 581 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β (volβ(β‘πΉ β {π¦})) β β) |
100 | 99 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ (π§ β ran πΊ β§ π§ = 0)) β (volβ(β‘πΉ β {π¦})) β β) |
101 | 97, 100 | eqeltrd 2838 |
. . . . . . . . 9
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ (π§ β ran πΊ β§ π§ = 0)) β (volβ(β‘πΉ β {(π¦ β π§)})) β β) |
102 | 89, 101 | eqeltrrd 2839 |
. . . . . . . 8
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ (π§ β ran πΊ β§ π§ = 0)) β (vol*β(β‘πΉ β {(π¦ β π§)})) β β) |
103 | | ovolsscl 24853 |
. . . . . . . 8
β’ ((((β‘πΉ β {(π¦ β π§)}) β© (β‘πΊ β {π§})) β (β‘πΉ β {(π¦ β π§)}) β§ (β‘πΉ β {(π¦ β π§)}) β β β§ (vol*β(β‘πΉ β {(π¦ β π§)})) β β) β
(vol*β((β‘πΉ β {(π¦ β π§)}) β© (β‘πΊ β {π§}))) β β) |
104 | 84, 87, 102, 103 | mp3an2i 1467 |
. . . . . . 7
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ (π§ β ran πΊ β§ π§ = 0)) β (vol*β((β‘πΉ β {(π¦ β π§)}) β© (β‘πΊ β {π§}))) β β) |
105 | 104 | expr 458 |
. . . . . 6
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ π§ β ran πΊ) β (π§ = 0 β (vol*β((β‘πΉ β {(π¦ β π§)}) β© (β‘πΊ β {π§}))) β β)) |
106 | | eldifsn 4748 |
. . . . . . . 8
β’ (π§ β (ran πΊ β {0}) β (π§ β ran πΊ β§ π§ β 0)) |
107 | | inss2 4190 |
. . . . . . . . 9
β’ ((β‘πΉ β {(π¦ β π§)}) β© (β‘πΊ β {π§})) β (β‘πΊ β {π§}) |
108 | | eldifi 4087 |
. . . . . . . . . 10
β’ (π§ β (ran πΊ β {0}) β π§ β ran πΊ) |
109 | | mblss 24898 |
. . . . . . . . . . 11
β’ ((β‘πΊ β {π§}) β dom vol β (β‘πΊ β {π§}) β β) |
110 | 73, 109 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ π§ β ran πΊ) β (β‘πΊ β {π§}) β β) |
111 | 108, 110 | sylan2 594 |
. . . . . . . . 9
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ π§ β (ran πΊ β {0})) β (β‘πΊ β {π§}) β β) |
112 | | i1fima 25045 |
. . . . . . . . . . . . 13
β’ (πΊ β dom β«1
β (β‘πΊ β {π§}) β dom vol) |
113 | 6, 112 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (β‘πΊ β {π§}) β dom vol) |
114 | 113 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ π§ β (ran πΊ β {0})) β (β‘πΊ β {π§}) β dom vol) |
115 | | mblvol 24897 |
. . . . . . . . . . 11
β’ ((β‘πΊ β {π§}) β dom vol β (volβ(β‘πΊ β {π§})) = (vol*β(β‘πΊ β {π§}))) |
116 | 114, 115 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ π§ β (ran πΊ β {0})) β (volβ(β‘πΊ β {π§})) = (vol*β(β‘πΊ β {π§}))) |
117 | 6 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β πΊ β dom
β«1) |
118 | | i1fima2sn 25047 |
. . . . . . . . . . 11
β’ ((πΊ β dom β«1
β§ π§ β (ran πΊ β {0})) β
(volβ(β‘πΊ β {π§})) β β) |
119 | 117, 118 | sylan 581 |
. . . . . . . . . 10
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ π§ β (ran πΊ β {0})) β (volβ(β‘πΊ β {π§})) β β) |
120 | 116, 119 | eqeltrrd 2839 |
. . . . . . . . 9
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ π§ β (ran πΊ β {0})) β (vol*β(β‘πΊ β {π§})) β β) |
121 | | ovolsscl 24853 |
. . . . . . . . 9
β’ ((((β‘πΉ β {(π¦ β π§)}) β© (β‘πΊ β {π§})) β (β‘πΊ β {π§}) β§ (β‘πΊ β {π§}) β β β§ (vol*β(β‘πΊ β {π§})) β β) β
(vol*β((β‘πΉ β {(π¦ β π§)}) β© (β‘πΊ β {π§}))) β β) |
122 | 107, 111,
120, 121 | mp3an2i 1467 |
. . . . . . . 8
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ π§ β (ran πΊ β {0})) β (vol*β((β‘πΉ β {(π¦ β π§)}) β© (β‘πΊ β {π§}))) β β) |
123 | 106, 122 | sylan2br 596 |
. . . . . . 7
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ (π§ β ran πΊ β§ π§ β 0)) β (vol*β((β‘πΉ β {(π¦ β π§)}) β© (β‘πΊ β {π§}))) β β) |
124 | 123 | expr 458 |
. . . . . 6
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ π§ β ran πΊ) β (π§ β 0 β (vol*β((β‘πΉ β {(π¦ β π§)}) β© (β‘πΊ β {π§}))) β β)) |
125 | 105, 124 | pm2.61dne 3032 |
. . . . 5
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ π§ β ran πΊ) β (vol*β((β‘πΉ β {(π¦ β π§)}) β© (β‘πΊ β {π§}))) β β) |
126 | 52, 125 | fsumrecl 15620 |
. . . 4
β’ ((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β Ξ£π§ β ran πΊ(vol*β((β‘πΉ β {(π¦ β π§)}) β© (β‘πΊ β {π§}))) β β) |
127 | 51 | fveq2d 6847 |
. . . . 5
β’ ((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β (vol*β(β‘(πΉ βf + πΊ) β {π¦})) = (vol*ββͺ π§ β ran πΊ((β‘πΉ β {(π¦ β π§)}) β© (β‘πΊ β {π§})))) |
128 | 107, 110 | sstrid 3956 |
. . . . . . . 8
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ π§ β ran πΊ) β ((β‘πΉ β {(π¦ β π§)}) β© (β‘πΊ β {π§})) β β) |
129 | 128, 125 | jca 513 |
. . . . . . 7
β’ (((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β§ π§ β ran πΊ) β (((β‘πΉ β {(π¦ β π§)}) β© (β‘πΊ β {π§})) β β β§ (vol*β((β‘πΉ β {(π¦ β π§)}) β© (β‘πΊ β {π§}))) β β)) |
130 | 129 | ralrimiva 3144 |
. . . . . 6
β’ ((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β βπ§ β ran πΊ(((β‘πΉ β {(π¦ β π§)}) β© (β‘πΊ β {π§})) β β β§ (vol*β((β‘πΉ β {(π¦ β π§)}) β© (β‘πΊ β {π§}))) β β)) |
131 | | ovolfiniun 24868 |
. . . . . 6
β’ ((ran
πΊ β Fin β§
βπ§ β ran πΊ(((β‘πΉ β {(π¦ β π§)}) β© (β‘πΊ β {π§})) β β β§ (vol*β((β‘πΉ β {(π¦ β π§)}) β© (β‘πΊ β {π§}))) β β)) β
(vol*ββͺ π§ β ran πΊ((β‘πΉ β {(π¦ β π§)}) β© (β‘πΊ β {π§}))) β€ Ξ£π§ β ran πΊ(vol*β((β‘πΉ β {(π¦ β π§)}) β© (β‘πΊ β {π§})))) |
132 | 52, 130, 131 | syl2anc 585 |
. . . . 5
β’ ((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β (vol*ββͺ π§ β ran πΊ((β‘πΉ β {(π¦ β π§)}) β© (β‘πΊ β {π§}))) β€ Ξ£π§ β ran πΊ(vol*β((β‘πΉ β {(π¦ β π§)}) β© (β‘πΊ β {π§})))) |
133 | 127, 132 | eqbrtrd 5128 |
. . . 4
β’ ((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β (vol*β(β‘(πΉ βf + πΊ) β {π¦})) β€ Ξ£π§ β ran πΊ(vol*β((β‘πΉ β {(π¦ β π§)}) β© (β‘πΊ β {π§})))) |
134 | | ovollecl 24850 |
. . . 4
β’ (((β‘(πΉ βf + πΊ) β {π¦}) β β β§ Ξ£π§ β ran πΊ(vol*β((β‘πΉ β {(π¦ β π§)}) β© (β‘πΊ β {π§}))) β β β§ (vol*β(β‘(πΉ βf + πΊ) β {π¦})) β€ Ξ£π§ β ran πΊ(vol*β((β‘πΉ β {(π¦ β π§)}) β© (β‘πΊ β {π§})))) β (vol*β(β‘(πΉ βf + πΊ) β {π¦})) β β) |
135 | 83, 126, 133, 134 | syl3anc 1372 |
. . 3
β’ ((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β (vol*β(β‘(πΉ βf + πΊ) β {π¦})) β β) |
136 | 81, 135 | eqeltrd 2838 |
. 2
β’ ((π β§ π¦ β (ran (πΉ βf + πΊ) β {0})) β (volβ(β‘(πΉ βf + πΊ) β {π¦})) β β) |
137 | 12, 45, 79, 136 | i1fd 25048 |
1
β’ (π β (πΉ βf + πΊ) β dom
β«1) |