Step | Hyp | Ref
| Expression |
1 | | iffalse 4500 |
. . . . . . . 8
β’ (Β¬
(π = 0 β§ π = 0) β if((π = 0 β§ π = 0), 0, (volβ((β‘πΉ β {π}) β© (β‘πΊ β {π})))) = (volβ((β‘πΉ β {π}) β© (β‘πΊ β {π})))) |
2 | 1 | adantl 483 |
. . . . . . 7
β’ (((π β§ (π β β β§ π β β)) β§ Β¬ (π = 0 β§ π = 0)) β if((π = 0 β§ π = 0), 0, (volβ((β‘πΉ β {π}) β© (β‘πΊ β {π})))) = (volβ((β‘πΉ β {π}) β© (β‘πΊ β {π})))) |
3 | | i1fadd.1 |
. . . . . . . . . . 11
β’ (π β πΉ β dom
β«1) |
4 | | i1fima 25058 |
. . . . . . . . . . 11
β’ (πΉ β dom β«1
β (β‘πΉ β {π}) β dom vol) |
5 | 3, 4 | syl 17 |
. . . . . . . . . 10
β’ (π β (β‘πΉ β {π}) β dom vol) |
6 | | i1fadd.2 |
. . . . . . . . . . 11
β’ (π β πΊ β dom
β«1) |
7 | | i1fima 25058 |
. . . . . . . . . . 11
β’ (πΊ β dom β«1
β (β‘πΊ β {π}) β dom vol) |
8 | 6, 7 | syl 17 |
. . . . . . . . . 10
β’ (π β (β‘πΊ β {π}) β dom vol) |
9 | | inmbl 24922 |
. . . . . . . . . 10
β’ (((β‘πΉ β {π}) β dom vol β§ (β‘πΊ β {π}) β dom vol) β ((β‘πΉ β {π}) β© (β‘πΊ β {π})) β dom vol) |
10 | 5, 8, 9 | syl2anc 585 |
. . . . . . . . 9
β’ (π β ((β‘πΉ β {π}) β© (β‘πΊ β {π})) β dom vol) |
11 | 10 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ (π β β β§ π β β)) β§ Β¬ (π = 0 β§ π = 0)) β ((β‘πΉ β {π}) β© (β‘πΊ β {π})) β dom vol) |
12 | | mblvol 24910 |
. . . . . . . 8
β’ (((β‘πΉ β {π}) β© (β‘πΊ β {π})) β dom vol β (volβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))) = (vol*β((β‘πΉ β {π}) β© (β‘πΊ β {π})))) |
13 | 11, 12 | syl 17 |
. . . . . . 7
β’ (((π β§ (π β β β§ π β β)) β§ Β¬ (π = 0 β§ π = 0)) β (volβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))) = (vol*β((β‘πΉ β {π}) β© (β‘πΊ β {π})))) |
14 | 2, 13 | eqtrd 2777 |
. . . . . 6
β’ (((π β§ (π β β β§ π β β)) β§ Β¬ (π = 0 β§ π = 0)) β if((π = 0 β§ π = 0), 0, (volβ((β‘πΉ β {π}) β© (β‘πΊ β {π})))) = (vol*β((β‘πΉ β {π}) β© (β‘πΊ β {π})))) |
15 | | neorian 3040 |
. . . . . . 7
β’ ((π β 0 β¨ π β 0) β Β¬ (π = 0 β§ π = 0)) |
16 | | inss1 4193 |
. . . . . . . . 9
β’ ((β‘πΉ β {π}) β© (β‘πΊ β {π})) β (β‘πΉ β {π}) |
17 | 5 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ (π β β β§ π β β)) β§ π β 0) β (β‘πΉ β {π}) β dom vol) |
18 | | mblss 24911 |
. . . . . . . . . 10
β’ ((β‘πΉ β {π}) β dom vol β (β‘πΉ β {π}) β β) |
19 | 17, 18 | syl 17 |
. . . . . . . . 9
β’ (((π β§ (π β β β§ π β β)) β§ π β 0) β (β‘πΉ β {π}) β β) |
20 | | mblvol 24910 |
. . . . . . . . . . 11
β’ ((β‘πΉ β {π}) β dom vol β (volβ(β‘πΉ β {π})) = (vol*β(β‘πΉ β {π}))) |
21 | 17, 20 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ (π β β β§ π β β)) β§ π β 0) β (volβ(β‘πΉ β {π})) = (vol*β(β‘πΉ β {π}))) |
22 | 3 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (π β β β§ π β β)) β§ π β 0) β πΉ β dom
β«1) |
23 | | simplrl 776 |
. . . . . . . . . . . 12
β’ (((π β§ (π β β β§ π β β)) β§ π β 0) β π β β) |
24 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π β§ (π β β β§ π β β)) β§ π β 0) β π β 0) |
25 | | eldifsn 4752 |
. . . . . . . . . . . 12
β’ (π β (β β {0})
β (π β β
β§ π β
0)) |
26 | 23, 24, 25 | sylanbrc 584 |
. . . . . . . . . . 11
β’ (((π β§ (π β β β§ π β β)) β§ π β 0) β π β (β β
{0})) |
27 | | i1fima2sn 25060 |
. . . . . . . . . . 11
β’ ((πΉ β dom β«1
β§ π β (β
β {0})) β (volβ(β‘πΉ β {π})) β β) |
28 | 22, 26, 27 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ (π β β β§ π β β)) β§ π β 0) β (volβ(β‘πΉ β {π})) β β) |
29 | 21, 28 | eqeltrrd 2839 |
. . . . . . . . 9
β’ (((π β§ (π β β β§ π β β)) β§ π β 0) β (vol*β(β‘πΉ β {π})) β β) |
30 | | ovolsscl 24866 |
. . . . . . . . 9
β’ ((((β‘πΉ β {π}) β© (β‘πΊ β {π})) β (β‘πΉ β {π}) β§ (β‘πΉ β {π}) β β β§ (vol*β(β‘πΉ β {π})) β β) β
(vol*β((β‘πΉ β {π}) β© (β‘πΊ β {π}))) β β) |
31 | 16, 19, 29, 30 | mp3an2i 1467 |
. . . . . . . 8
β’ (((π β§ (π β β β§ π β β)) β§ π β 0) β (vol*β((β‘πΉ β {π}) β© (β‘πΊ β {π}))) β β) |
32 | | inss2 4194 |
. . . . . . . . 9
β’ ((β‘πΉ β {π}) β© (β‘πΊ β {π})) β (β‘πΊ β {π}) |
33 | 6 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β β§ π β β)) β πΊ β dom
β«1) |
34 | 33, 7 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ (π β β β§ π β β)) β (β‘πΊ β {π}) β dom vol) |
35 | 34 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ (π β β β§ π β β)) β§ π β 0) β (β‘πΊ β {π}) β dom vol) |
36 | | mblss 24911 |
. . . . . . . . . 10
β’ ((β‘πΊ β {π}) β dom vol β (β‘πΊ β {π}) β β) |
37 | 35, 36 | syl 17 |
. . . . . . . . 9
β’ (((π β§ (π β β β§ π β β)) β§ π β 0) β (β‘πΊ β {π}) β β) |
38 | | mblvol 24910 |
. . . . . . . . . . 11
β’ ((β‘πΊ β {π}) β dom vol β (volβ(β‘πΊ β {π})) = (vol*β(β‘πΊ β {π}))) |
39 | 35, 38 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ (π β β β§ π β β)) β§ π β 0) β (volβ(β‘πΊ β {π})) = (vol*β(β‘πΊ β {π}))) |
40 | 6 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (π β β β§ π β β)) β§ π β 0) β πΊ β dom
β«1) |
41 | | simplrr 777 |
. . . . . . . . . . . 12
β’ (((π β§ (π β β β§ π β β)) β§ π β 0) β π β β) |
42 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π β§ (π β β β§ π β β)) β§ π β 0) β π β 0) |
43 | | eldifsn 4752 |
. . . . . . . . . . . 12
β’ (π β (β β {0})
β (π β β
β§ π β
0)) |
44 | 41, 42, 43 | sylanbrc 584 |
. . . . . . . . . . 11
β’ (((π β§ (π β β β§ π β β)) β§ π β 0) β π β (β β
{0})) |
45 | | i1fima2sn 25060 |
. . . . . . . . . . 11
β’ ((πΊ β dom β«1
β§ π β (β
β {0})) β (volβ(β‘πΊ β {π})) β β) |
46 | 40, 44, 45 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ (π β β β§ π β β)) β§ π β 0) β (volβ(β‘πΊ β {π})) β β) |
47 | 39, 46 | eqeltrrd 2839 |
. . . . . . . . 9
β’ (((π β§ (π β β β§ π β β)) β§ π β 0) β (vol*β(β‘πΊ β {π})) β β) |
48 | | ovolsscl 24866 |
. . . . . . . . 9
β’ ((((β‘πΉ β {π}) β© (β‘πΊ β {π})) β (β‘πΊ β {π}) β§ (β‘πΊ β {π}) β β β§ (vol*β(β‘πΊ β {π})) β β) β
(vol*β((β‘πΉ β {π}) β© (β‘πΊ β {π}))) β β) |
49 | 32, 37, 47, 48 | mp3an2i 1467 |
. . . . . . . 8
β’ (((π β§ (π β β β§ π β β)) β§ π β 0) β (vol*β((β‘πΉ β {π}) β© (β‘πΊ β {π}))) β β) |
50 | 31, 49 | jaodan 957 |
. . . . . . 7
β’ (((π β§ (π β β β§ π β β)) β§ (π β 0 β¨ π β 0)) β (vol*β((β‘πΉ β {π}) β© (β‘πΊ β {π}))) β β) |
51 | 15, 50 | sylan2br 596 |
. . . . . 6
β’ (((π β§ (π β β β§ π β β)) β§ Β¬ (π = 0 β§ π = 0)) β (vol*β((β‘πΉ β {π}) β© (β‘πΊ β {π}))) β β) |
52 | 14, 51 | eqeltrd 2838 |
. . . . 5
β’ (((π β§ (π β β β§ π β β)) β§ Β¬ (π = 0 β§ π = 0)) β if((π = 0 β§ π = 0), 0, (volβ((β‘πΉ β {π}) β© (β‘πΊ β {π})))) β β) |
53 | 52 | ex 414 |
. . . 4
β’ ((π β§ (π β β β§ π β β)) β (Β¬ (π = 0 β§ π = 0) β if((π = 0 β§ π = 0), 0, (volβ((β‘πΉ β {π}) β© (β‘πΊ β {π})))) β β)) |
54 | | iftrue 4497 |
. . . . 5
β’ ((π = 0 β§ π = 0) β if((π = 0 β§ π = 0), 0, (volβ((β‘πΉ β {π}) β© (β‘πΊ β {π})))) = 0) |
55 | | 0re 11164 |
. . . . 5
β’ 0 β
β |
56 | 54, 55 | eqeltrdi 2846 |
. . . 4
β’ ((π = 0 β§ π = 0) β if((π = 0 β§ π = 0), 0, (volβ((β‘πΉ β {π}) β© (β‘πΊ β {π})))) β β) |
57 | 53, 56 | pm2.61d2 181 |
. . 3
β’ ((π β§ (π β β β§ π β β)) β if((π = 0 β§ π = 0), 0, (volβ((β‘πΉ β {π}) β© (β‘πΊ β {π})))) β β) |
58 | 57 | ralrimivva 3198 |
. 2
β’ (π β βπ β β βπ β β if((π = 0 β§ π = 0), 0, (volβ((β‘πΉ β {π}) β© (β‘πΊ β {π})))) β β) |
59 | | itg1add.3 |
. . 3
β’ πΌ = (π β β, π β β β¦ if((π = 0 β§ π = 0), 0, (volβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))))) |
60 | 59 | fmpo 8005 |
. 2
β’
(βπ β
β βπ β
β if((π = 0 β§
π = 0), 0,
(volβ((β‘πΉ β {π}) β© (β‘πΊ β {π})))) β β β πΌ:(β Γ
β)βΆβ) |
61 | 58, 60 | sylib 217 |
1
β’ (π β πΌ:(β Γ
β)βΆβ) |