Step | Hyp | Ref
| Expression |
1 | | mbfposadd.2 |
. . . . 5
β’ ((π β§ π₯ β π΄) β π΅ β β) |
2 | | 0re 11164 |
. . . . 5
β’ 0 β
β |
3 | | ifcl 4536 |
. . . . 5
β’ ((π΅ β β β§ 0 β
β) β if(0 β€ π΅, π΅, 0) β β) |
4 | 1, 2, 3 | sylancl 587 |
. . . 4
β’ ((π β§ π₯ β π΄) β if(0 β€ π΅, π΅, 0) β β) |
5 | | mbfposadd.4 |
. . . . 5
β’ ((π β§ π₯ β π΄) β πΆ β β) |
6 | | ifcl 4536 |
. . . . 5
β’ ((πΆ β β β§ 0 β
β) β if(0 β€ πΆ, πΆ, 0) β β) |
7 | 5, 2, 6 | sylancl 587 |
. . . 4
β’ ((π β§ π₯ β π΄) β if(0 β€ πΆ, πΆ, 0) β β) |
8 | 4, 7 | readdcld 11191 |
. . 3
β’ ((π β§ π₯ β π΄) β (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0)) β β) |
9 | 8 | fmpttd 7068 |
. 2
β’ (π β (π₯ β π΄ β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))):π΄βΆβ) |
10 | | ssrab2 4042 |
. . . 4
β’ {π₯ β π΄ β£ 0 β€ πΆ} β π΄ |
11 | | fssres 6713 |
. . . 4
β’ (((π₯ β π΄ β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))):π΄βΆβ β§ {π₯ β π΄ β£ 0 β€ πΆ} β π΄) β ((π₯ β π΄ β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) βΎ {π₯ β π΄ β£ 0 β€ πΆ}):{π₯ β π΄ β£ 0 β€ πΆ}βΆβ) |
12 | 9, 10, 11 | sylancl 587 |
. . 3
β’ (π β ((π₯ β π΄ β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) βΎ {π₯ β π΄ β£ 0 β€ πΆ}):{π₯ β π΄ β£ 0 β€ πΆ}βΆβ) |
13 | | inss2 4194 |
. . . . . 6
β’ ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β {π₯ β π΄ β£ 0 β€ πΆ} |
14 | | resabs1 5972 |
. . . . . 6
β’ (({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β {π₯ β π΄ β£ 0 β€ πΆ} β (((π₯ β π΄ β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) βΎ {π₯ β π΄ β£ 0 β€ πΆ}) βΎ ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) = ((π₯ β π΄ β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) βΎ ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}))) |
15 | 13, 14 | ax-mp 5 |
. . . . 5
β’ (((π₯ β π΄ β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) βΎ {π₯ β π΄ β£ 0 β€ πΆ}) βΎ ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) = ((π₯ β π΄ β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) βΎ ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) |
16 | | elin 3931 |
. . . . . . . . 9
β’ (π₯ β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β (π₯ β {π₯ β π΄ β£ 0 β€ π΅} β§ π₯ β {π₯ β π΄ β£ 0 β€ πΆ})) |
17 | | rabid 3430 |
. . . . . . . . . 10
β’ (π₯ β {π₯ β π΄ β£ 0 β€ π΅} β (π₯ β π΄ β§ 0 β€ π΅)) |
18 | | rabid 3430 |
. . . . . . . . . 10
β’ (π₯ β {π₯ β π΄ β£ 0 β€ πΆ} β (π₯ β π΄ β§ 0 β€ πΆ)) |
19 | 17, 18 | anbi12i 628 |
. . . . . . . . 9
β’ ((π₯ β {π₯ β π΄ β£ 0 β€ π΅} β§ π₯ β {π₯ β π΄ β£ 0 β€ πΆ}) β ((π₯ β π΄ β§ 0 β€ π΅) β§ (π₯ β π΄ β§ 0 β€ πΆ))) |
20 | 16, 19 | bitri 275 |
. . . . . . . 8
β’ (π₯ β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β ((π₯ β π΄ β§ 0 β€ π΅) β§ (π₯ β π΄ β§ 0 β€ πΆ))) |
21 | | iftrue 4497 |
. . . . . . . . . 10
β’ (0 β€
π΅ β if(0 β€ π΅, π΅, 0) = π΅) |
22 | | iftrue 4497 |
. . . . . . . . . 10
β’ (0 β€
πΆ β if(0 β€ πΆ, πΆ, 0) = πΆ) |
23 | 21, 22 | oveqan12d 7381 |
. . . . . . . . 9
β’ ((0 β€
π΅ β§ 0 β€ πΆ) β (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0)) = (π΅ + πΆ)) |
24 | 23 | ad2ant2l 745 |
. . . . . . . 8
β’ (((π₯ β π΄ β§ 0 β€ π΅) β§ (π₯ β π΄ β§ 0 β€ πΆ)) β (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0)) = (π΅ + πΆ)) |
25 | 20, 24 | sylbi 216 |
. . . . . . 7
β’ (π₯ β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0)) = (π΅ + πΆ)) |
26 | 25 | mpteq2ia 5213 |
. . . . . 6
β’ (π₯ β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) = (π₯ β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β¦ (π΅ + πΆ)) |
27 | | inss1 4193 |
. . . . . . . 8
β’ ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β {π₯ β π΄ β£ 0 β€ π΅} |
28 | | ssrab2 4042 |
. . . . . . . 8
β’ {π₯ β π΄ β£ 0 β€ π΅} β π΄ |
29 | 27, 28 | sstri 3958 |
. . . . . . 7
β’ ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β π΄ |
30 | | resmpt 5996 |
. . . . . . . 8
β’ (({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β π΄ β ((π¦ β π΄ β¦ β¦π¦ / π₯β¦(if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) βΎ ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) = (π¦ β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β¦ β¦π¦ / π₯β¦(if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0)))) |
31 | | nfcv 2908 |
. . . . . . . . . 10
β’
β²π¦(if(0
β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0)) |
32 | | nfcsb1v 3885 |
. . . . . . . . . 10
β’
β²π₯β¦π¦ / π₯β¦(if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0)) |
33 | | csbeq1a 3874 |
. . . . . . . . . 10
β’ (π₯ = π¦ β (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0)) = β¦π¦ / π₯β¦(if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) |
34 | 31, 32, 33 | cbvmpt 5221 |
. . . . . . . . 9
β’ (π₯ β π΄ β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) = (π¦ β π΄ β¦ β¦π¦ / π₯β¦(if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) |
35 | 34 | reseq1i 5938 |
. . . . . . . 8
β’ ((π₯ β π΄ β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) βΎ ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) = ((π¦ β π΄ β¦ β¦π¦ / π₯β¦(if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) βΎ ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) |
36 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π¦(π₯ β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β§ π§ = (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) |
37 | | nfrab1 3429 |
. . . . . . . . . . . . 13
β’
β²π₯{π₯ β π΄ β£ 0 β€ π΅} |
38 | | nfrab1 3429 |
. . . . . . . . . . . . 13
β’
β²π₯{π₯ β π΄ β£ 0 β€ πΆ} |
39 | 37, 38 | nfin 4181 |
. . . . . . . . . . . 12
β’
β²π₯({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) |
40 | 39 | nfcri 2895 |
. . . . . . . . . . 11
β’
β²π₯ π¦ β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) |
41 | 32 | nfeq2 2925 |
. . . . . . . . . . 11
β’
β²π₯ π§ = β¦π¦ / π₯β¦(if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0)) |
42 | 40, 41 | nfan 1903 |
. . . . . . . . . 10
β’
β²π₯(π¦ β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β§ π§ = β¦π¦ / π₯β¦(if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) |
43 | | eleq1w 2821 |
. . . . . . . . . . 11
β’ (π₯ = π¦ β (π₯ β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β π¦ β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}))) |
44 | 33 | eqeq2d 2748 |
. . . . . . . . . . 11
β’ (π₯ = π¦ β (π§ = (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0)) β π§ = β¦π¦ / π₯β¦(if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0)))) |
45 | 43, 44 | anbi12d 632 |
. . . . . . . . . 10
β’ (π₯ = π¦ β ((π₯ β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β§ π§ = (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) β (π¦ β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β§ π§ = β¦π¦ / π₯β¦(if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))))) |
46 | 36, 42, 45 | cbvopab1 5185 |
. . . . . . . . 9
β’
{β¨π₯, π§β© β£ (π₯ β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β§ π§ = (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0)))} = {β¨π¦, π§β© β£ (π¦ β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β§ π§ = β¦π¦ / π₯β¦(if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0)))} |
47 | | df-mpt 5194 |
. . . . . . . . 9
β’ (π₯ β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) = {β¨π₯, π§β© β£ (π₯ β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β§ π§ = (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0)))} |
48 | | df-mpt 5194 |
. . . . . . . . 9
β’ (π¦ β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β¦ β¦π¦ / π₯β¦(if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) = {β¨π¦, π§β© β£ (π¦ β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β§ π§ = β¦π¦ / π₯β¦(if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0)))} |
49 | 46, 47, 48 | 3eqtr4i 2775 |
. . . . . . . 8
β’ (π₯ β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) = (π¦ β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β¦ β¦π¦ / π₯β¦(if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) |
50 | 30, 35, 49 | 3eqtr4g 2802 |
. . . . . . 7
β’ (({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β π΄ β ((π₯ β π΄ β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) βΎ ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) = (π₯ β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0)))) |
51 | 29, 50 | ax-mp 5 |
. . . . . 6
β’ ((π₯ β π΄ β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) βΎ ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) = (π₯ β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) |
52 | | resmpt 5996 |
. . . . . . . 8
β’ (({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β π΄ β ((π¦ β π΄ β¦ β¦π¦ / π₯β¦(π΅ + πΆ)) βΎ ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) = (π¦ β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β¦ β¦π¦ / π₯β¦(π΅ + πΆ))) |
53 | | nfcv 2908 |
. . . . . . . . . 10
β’
β²π¦(π΅ + πΆ) |
54 | | nfcsb1v 3885 |
. . . . . . . . . 10
β’
β²π₯β¦π¦ / π₯β¦(π΅ + πΆ) |
55 | | csbeq1a 3874 |
. . . . . . . . . 10
β’ (π₯ = π¦ β (π΅ + πΆ) = β¦π¦ / π₯β¦(π΅ + πΆ)) |
56 | 53, 54, 55 | cbvmpt 5221 |
. . . . . . . . 9
β’ (π₯ β π΄ β¦ (π΅ + πΆ)) = (π¦ β π΄ β¦ β¦π¦ / π₯β¦(π΅ + πΆ)) |
57 | 56 | reseq1i 5938 |
. . . . . . . 8
β’ ((π₯ β π΄ β¦ (π΅ + πΆ)) βΎ ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) = ((π¦ β π΄ β¦ β¦π¦ / π₯β¦(π΅ + πΆ)) βΎ ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) |
58 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π¦(π₯ β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β§ π§ = (π΅ + πΆ)) |
59 | 54 | nfeq2 2925 |
. . . . . . . . . . 11
β’
β²π₯ π§ = β¦π¦ / π₯β¦(π΅ + πΆ) |
60 | 40, 59 | nfan 1903 |
. . . . . . . . . 10
β’
β²π₯(π¦ β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β§ π§ = β¦π¦ / π₯β¦(π΅ + πΆ)) |
61 | 55 | eqeq2d 2748 |
. . . . . . . . . . 11
β’ (π₯ = π¦ β (π§ = (π΅ + πΆ) β π§ = β¦π¦ / π₯β¦(π΅ + πΆ))) |
62 | 43, 61 | anbi12d 632 |
. . . . . . . . . 10
β’ (π₯ = π¦ β ((π₯ β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β§ π§ = (π΅ + πΆ)) β (π¦ β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β§ π§ = β¦π¦ / π₯β¦(π΅ + πΆ)))) |
63 | 58, 60, 62 | cbvopab1 5185 |
. . . . . . . . 9
β’
{β¨π₯, π§β© β£ (π₯ β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β§ π§ = (π΅ + πΆ))} = {β¨π¦, π§β© β£ (π¦ β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β§ π§ = β¦π¦ / π₯β¦(π΅ + πΆ))} |
64 | | df-mpt 5194 |
. . . . . . . . 9
β’ (π₯ β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β¦ (π΅ + πΆ)) = {β¨π₯, π§β© β£ (π₯ β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β§ π§ = (π΅ + πΆ))} |
65 | | df-mpt 5194 |
. . . . . . . . 9
β’ (π¦ β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β¦ β¦π¦ / π₯β¦(π΅ + πΆ)) = {β¨π¦, π§β© β£ (π¦ β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β§ π§ = β¦π¦ / π₯β¦(π΅ + πΆ))} |
66 | 63, 64, 65 | 3eqtr4i 2775 |
. . . . . . . 8
β’ (π₯ β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β¦ (π΅ + πΆ)) = (π¦ β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β¦ β¦π¦ / π₯β¦(π΅ + πΆ)) |
67 | 52, 57, 66 | 3eqtr4g 2802 |
. . . . . . 7
β’ (({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β π΄ β ((π₯ β π΄ β¦ (π΅ + πΆ)) βΎ ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) = (π₯ β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β¦ (π΅ + πΆ))) |
68 | 29, 67 | ax-mp 5 |
. . . . . 6
β’ ((π₯ β π΄ β¦ (π΅ + πΆ)) βΎ ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) = (π₯ β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β¦ (π΅ + πΆ)) |
69 | 26, 51, 68 | 3eqtr4i 2775 |
. . . . 5
β’ ((π₯ β π΄ β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) βΎ ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) = ((π₯ β π΄ β¦ (π΅ + πΆ)) βΎ ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) |
70 | 15, 69 | eqtri 2765 |
. . . 4
β’ (((π₯ β π΄ β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) βΎ {π₯ β π΄ β£ 0 β€ πΆ}) βΎ ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) = ((π₯ β π΄ β¦ (π΅ + πΆ)) βΎ ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) |
71 | | mbfposadd.5 |
. . . . 5
β’ (π β (π₯ β π΄ β¦ (π΅ + πΆ)) β MblFn) |
72 | 1 | biantrurd 534 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β (0 β€ π΅ β (π΅ β β β§ 0 β€ π΅))) |
73 | | elrege0 13378 |
. . . . . . . . . 10
β’ (π΅ β (0[,)+β) β
(π΅ β β β§ 0
β€ π΅)) |
74 | 72, 73 | bitr4di 289 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β (0 β€ π΅ β π΅ β (0[,)+β))) |
75 | 74 | rabbidva 3417 |
. . . . . . . 8
β’ (π β {π₯ β π΄ β£ 0 β€ π΅} = {π₯ β π΄ β£ π΅ β (0[,)+β)}) |
76 | | 0xr 11209 |
. . . . . . . . . . 11
β’ 0 β
β* |
77 | | pnfxr 11216 |
. . . . . . . . . . 11
β’ +β
β β* |
78 | | 0ltpnf 13050 |
. . . . . . . . . . 11
β’ 0 <
+β |
79 | | snunioo 13402 |
. . . . . . . . . . 11
β’ ((0
β β* β§ +β β β* β§ 0
< +β) β ({0} βͺ (0(,)+β)) =
(0[,)+β)) |
80 | 76, 77, 78, 79 | mp3an 1462 |
. . . . . . . . . 10
β’ ({0}
βͺ (0(,)+β)) = (0[,)+β) |
81 | 80 | imaeq2i 6016 |
. . . . . . . . 9
β’ (β‘(π₯ β π΄ β¦ π΅) β ({0} βͺ (0(,)+β))) =
(β‘(π₯ β π΄ β¦ π΅) β (0[,)+β)) |
82 | | imaundi 6107 |
. . . . . . . . 9
β’ (β‘(π₯ β π΄ β¦ π΅) β ({0} βͺ (0(,)+β))) =
((β‘(π₯ β π΄ β¦ π΅) β {0}) βͺ (β‘(π₯ β π΄ β¦ π΅) β (0(,)+β))) |
83 | | eqid 2737 |
. . . . . . . . . 10
β’ (π₯ β π΄ β¦ π΅) = (π₯ β π΄ β¦ π΅) |
84 | 83 | mptpreima 6195 |
. . . . . . . . 9
β’ (β‘(π₯ β π΄ β¦ π΅) β (0[,)+β)) = {π₯ β π΄ β£ π΅ β (0[,)+β)} |
85 | 81, 82, 84 | 3eqtr3ri 2774 |
. . . . . . . 8
β’ {π₯ β π΄ β£ π΅ β (0[,)+β)} = ((β‘(π₯ β π΄ β¦ π΅) β {0}) βͺ (β‘(π₯ β π΄ β¦ π΅) β (0(,)+β))) |
86 | 75, 85 | eqtrdi 2793 |
. . . . . . 7
β’ (π β {π₯ β π΄ β£ 0 β€ π΅} = ((β‘(π₯ β π΄ β¦ π΅) β {0}) βͺ (β‘(π₯ β π΄ β¦ π΅) β (0(,)+β)))) |
87 | | mbfposadd.1 |
. . . . . . . 8
β’ (π β (π₯ β π΄ β¦ π΅) β MblFn) |
88 | 1 | fmpttd 7068 |
. . . . . . . 8
β’ (π β (π₯ β π΄ β¦ π΅):π΄βΆβ) |
89 | | mbfimasn 25012 |
. . . . . . . . . 10
β’ (((π₯ β π΄ β¦ π΅) β MblFn β§ (π₯ β π΄ β¦ π΅):π΄βΆβ β§ 0 β β)
β (β‘(π₯ β π΄ β¦ π΅) β {0}) β dom
vol) |
90 | 2, 89 | mp3an3 1451 |
. . . . . . . . 9
β’ (((π₯ β π΄ β¦ π΅) β MblFn β§ (π₯ β π΄ β¦ π΅):π΄βΆβ) β (β‘(π₯ β π΄ β¦ π΅) β {0}) β dom
vol) |
91 | | mbfima 25010 |
. . . . . . . . 9
β’ (((π₯ β π΄ β¦ π΅) β MblFn β§ (π₯ β π΄ β¦ π΅):π΄βΆβ) β (β‘(π₯ β π΄ β¦ π΅) β (0(,)+β)) β dom
vol) |
92 | | unmbl 24917 |
. . . . . . . . 9
β’ (((β‘(π₯ β π΄ β¦ π΅) β {0}) β dom vol β§ (β‘(π₯ β π΄ β¦ π΅) β (0(,)+β)) β dom vol)
β ((β‘(π₯ β π΄ β¦ π΅) β {0}) βͺ (β‘(π₯ β π΄ β¦ π΅) β (0(,)+β))) β dom
vol) |
93 | 90, 91, 92 | syl2anc 585 |
. . . . . . . 8
β’ (((π₯ β π΄ β¦ π΅) β MblFn β§ (π₯ β π΄ β¦ π΅):π΄βΆβ) β ((β‘(π₯ β π΄ β¦ π΅) β {0}) βͺ (β‘(π₯ β π΄ β¦ π΅) β (0(,)+β))) β dom
vol) |
94 | 87, 88, 93 | syl2anc 585 |
. . . . . . 7
β’ (π β ((β‘(π₯ β π΄ β¦ π΅) β {0}) βͺ (β‘(π₯ β π΄ β¦ π΅) β (0(,)+β))) β dom
vol) |
95 | 86, 94 | eqeltrd 2838 |
. . . . . 6
β’ (π β {π₯ β π΄ β£ 0 β€ π΅} β dom vol) |
96 | 5 | biantrurd 534 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β (0 β€ πΆ β (πΆ β β β§ 0 β€ πΆ))) |
97 | | elrege0 13378 |
. . . . . . . . . 10
β’ (πΆ β (0[,)+β) β
(πΆ β β β§ 0
β€ πΆ)) |
98 | 96, 97 | bitr4di 289 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β (0 β€ πΆ β πΆ β (0[,)+β))) |
99 | 98 | rabbidva 3417 |
. . . . . . . 8
β’ (π β {π₯ β π΄ β£ 0 β€ πΆ} = {π₯ β π΄ β£ πΆ β (0[,)+β)}) |
100 | 80 | imaeq2i 6016 |
. . . . . . . . 9
β’ (β‘(π₯ β π΄ β¦ πΆ) β ({0} βͺ (0(,)+β))) =
(β‘(π₯ β π΄ β¦ πΆ) β (0[,)+β)) |
101 | | imaundi 6107 |
. . . . . . . . 9
β’ (β‘(π₯ β π΄ β¦ πΆ) β ({0} βͺ (0(,)+β))) =
((β‘(π₯ β π΄ β¦ πΆ) β {0}) βͺ (β‘(π₯ β π΄ β¦ πΆ) β (0(,)+β))) |
102 | | eqid 2737 |
. . . . . . . . . 10
β’ (π₯ β π΄ β¦ πΆ) = (π₯ β π΄ β¦ πΆ) |
103 | 102 | mptpreima 6195 |
. . . . . . . . 9
β’ (β‘(π₯ β π΄ β¦ πΆ) β (0[,)+β)) = {π₯ β π΄ β£ πΆ β (0[,)+β)} |
104 | 100, 101,
103 | 3eqtr3ri 2774 |
. . . . . . . 8
β’ {π₯ β π΄ β£ πΆ β (0[,)+β)} = ((β‘(π₯ β π΄ β¦ πΆ) β {0}) βͺ (β‘(π₯ β π΄ β¦ πΆ) β (0(,)+β))) |
105 | 99, 104 | eqtrdi 2793 |
. . . . . . 7
β’ (π β {π₯ β π΄ β£ 0 β€ πΆ} = ((β‘(π₯ β π΄ β¦ πΆ) β {0}) βͺ (β‘(π₯ β π΄ β¦ πΆ) β (0(,)+β)))) |
106 | | mbfposadd.3 |
. . . . . . . 8
β’ (π β (π₯ β π΄ β¦ πΆ) β MblFn) |
107 | 5 | fmpttd 7068 |
. . . . . . . 8
β’ (π β (π₯ β π΄ β¦ πΆ):π΄βΆβ) |
108 | | mbfimasn 25012 |
. . . . . . . . . 10
β’ (((π₯ β π΄ β¦ πΆ) β MblFn β§ (π₯ β π΄ β¦ πΆ):π΄βΆβ β§ 0 β β)
β (β‘(π₯ β π΄ β¦ πΆ) β {0}) β dom
vol) |
109 | 2, 108 | mp3an3 1451 |
. . . . . . . . 9
β’ (((π₯ β π΄ β¦ πΆ) β MblFn β§ (π₯ β π΄ β¦ πΆ):π΄βΆβ) β (β‘(π₯ β π΄ β¦ πΆ) β {0}) β dom
vol) |
110 | | mbfima 25010 |
. . . . . . . . 9
β’ (((π₯ β π΄ β¦ πΆ) β MblFn β§ (π₯ β π΄ β¦ πΆ):π΄βΆβ) β (β‘(π₯ β π΄ β¦ πΆ) β (0(,)+β)) β dom
vol) |
111 | | unmbl 24917 |
. . . . . . . . 9
β’ (((β‘(π₯ β π΄ β¦ πΆ) β {0}) β dom vol β§ (β‘(π₯ β π΄ β¦ πΆ) β (0(,)+β)) β dom vol)
β ((β‘(π₯ β π΄ β¦ πΆ) β {0}) βͺ (β‘(π₯ β π΄ β¦ πΆ) β (0(,)+β))) β dom
vol) |
112 | 109, 110,
111 | syl2anc 585 |
. . . . . . . 8
β’ (((π₯ β π΄ β¦ πΆ) β MblFn β§ (π₯ β π΄ β¦ πΆ):π΄βΆβ) β ((β‘(π₯ β π΄ β¦ πΆ) β {0}) βͺ (β‘(π₯ β π΄ β¦ πΆ) β (0(,)+β))) β dom
vol) |
113 | 106, 107,
112 | syl2anc 585 |
. . . . . . 7
β’ (π β ((β‘(π₯ β π΄ β¦ πΆ) β {0}) βͺ (β‘(π₯ β π΄ β¦ πΆ) β (0(,)+β))) β dom
vol) |
114 | 105, 113 | eqeltrd 2838 |
. . . . . 6
β’ (π β {π₯ β π΄ β£ 0 β€ πΆ} β dom vol) |
115 | | inmbl 24922 |
. . . . . 6
β’ (({π₯ β π΄ β£ 0 β€ π΅} β dom vol β§ {π₯ β π΄ β£ 0 β€ πΆ} β dom vol) β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β dom vol) |
116 | 95, 114, 115 | syl2anc 585 |
. . . . 5
β’ (π β ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β dom vol) |
117 | | mbfres 25024 |
. . . . 5
β’ (((π₯ β π΄ β¦ (π΅ + πΆ)) β MblFn β§ ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β dom vol) β ((π₯ β π΄ β¦ (π΅ + πΆ)) βΎ ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) β MblFn) |
118 | 71, 116, 117 | syl2anc 585 |
. . . 4
β’ (π β ((π₯ β π΄ β¦ (π΅ + πΆ)) βΎ ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) β MblFn) |
119 | 70, 118 | eqeltrid 2842 |
. . 3
β’ (π β (((π₯ β π΄ β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) βΎ {π₯ β π΄ β£ 0 β€ πΆ}) βΎ ({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) β MblFn) |
120 | | inss2 4194 |
. . . . . 6
β’ ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β {π₯ β π΄ β£ 0 β€ πΆ} |
121 | | resabs1 5972 |
. . . . . 6
β’ (({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β {π₯ β π΄ β£ 0 β€ πΆ} β (((π₯ β π΄ β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) βΎ {π₯ β π΄ β£ 0 β€ πΆ}) βΎ ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) = ((π₯ β π΄ β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) βΎ ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}))) |
122 | 120, 121 | ax-mp 5 |
. . . . 5
β’ (((π₯ β π΄ β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) βΎ {π₯ β π΄ β£ 0 β€ πΆ}) βΎ ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) = ((π₯ β π΄ β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) βΎ ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) |
123 | | rabid 3430 |
. . . . . . . . . 10
β’ (π₯ β {π₯ β π΄ β£ Β¬ 0 β€ π΅} β (π₯ β π΄ β§ Β¬ 0 β€ π΅)) |
124 | 123, 18 | anbi12i 628 |
. . . . . . . . 9
β’ ((π₯ β {π₯ β π΄ β£ Β¬ 0 β€ π΅} β§ π₯ β {π₯ β π΄ β£ 0 β€ πΆ}) β ((π₯ β π΄ β§ Β¬ 0 β€ π΅) β§ (π₯ β π΄ β§ 0 β€ πΆ))) |
125 | | elin 3931 |
. . . . . . . . 9
β’ (π₯ β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β (π₯ β {π₯ β π΄ β£ Β¬ 0 β€ π΅} β§ π₯ β {π₯ β π΄ β£ 0 β€ πΆ})) |
126 | | anandi 675 |
. . . . . . . . 9
β’ ((π₯ β π΄ β§ (Β¬ 0 β€ π΅ β§ 0 β€ πΆ)) β ((π₯ β π΄ β§ Β¬ 0 β€ π΅) β§ (π₯ β π΄ β§ 0 β€ πΆ))) |
127 | 124, 125,
126 | 3bitr4i 303 |
. . . . . . . 8
β’ (π₯ β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β (π₯ β π΄ β§ (Β¬ 0 β€ π΅ β§ 0 β€ πΆ))) |
128 | | iffalse 4500 |
. . . . . . . . . . 11
β’ (Β¬ 0
β€ π΅ β if(0 β€
π΅, π΅, 0) = 0) |
129 | 128, 22 | oveqan12d 7381 |
. . . . . . . . . 10
β’ ((Β¬ 0
β€ π΅ β§ 0 β€ πΆ) β (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0)) = (0 + πΆ)) |
130 | 129 | ad2antll 728 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π΄ β§ (Β¬ 0 β€ π΅ β§ 0 β€ πΆ))) β (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0)) = (0 + πΆ)) |
131 | 5 | recnd 11190 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β πΆ β β) |
132 | 131 | addid2d 11363 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β (0 + πΆ) = πΆ) |
133 | 132 | adantrr 716 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π΄ β§ (Β¬ 0 β€ π΅ β§ 0 β€ πΆ))) β (0 + πΆ) = πΆ) |
134 | 130, 133 | eqtrd 2777 |
. . . . . . . 8
β’ ((π β§ (π₯ β π΄ β§ (Β¬ 0 β€ π΅ β§ 0 β€ πΆ))) β (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0)) = πΆ) |
135 | 127, 134 | sylan2b 595 |
. . . . . . 7
β’ ((π β§ π₯ β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) β (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0)) = πΆ) |
136 | 135 | mpteq2dva 5210 |
. . . . . 6
β’ (π β (π₯ β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) = (π₯ β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β¦ πΆ)) |
137 | | inss1 4193 |
. . . . . . . 8
β’ ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β {π₯ β π΄ β£ Β¬ 0 β€ π΅} |
138 | | ssrab2 4042 |
. . . . . . . 8
β’ {π₯ β π΄ β£ Β¬ 0 β€ π΅} β π΄ |
139 | 137, 138 | sstri 3958 |
. . . . . . 7
β’ ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β π΄ |
140 | | resmpt 5996 |
. . . . . . . 8
β’ (({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β π΄ β ((π¦ β π΄ β¦ β¦π¦ / π₯β¦(if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) βΎ ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) = (π¦ β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β¦ β¦π¦ / π₯β¦(if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0)))) |
141 | 34 | reseq1i 5938 |
. . . . . . . 8
β’ ((π₯ β π΄ β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) βΎ ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) = ((π¦ β π΄ β¦ β¦π¦ / π₯β¦(if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) βΎ ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) |
142 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π¦(π₯ β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β§ π§ = (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) |
143 | | nfrab1 3429 |
. . . . . . . . . . . . 13
β’
β²π₯{π₯ β π΄ β£ Β¬ 0 β€ π΅} |
144 | 143, 38 | nfin 4181 |
. . . . . . . . . . . 12
β’
β²π₯({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) |
145 | 144 | nfcri 2895 |
. . . . . . . . . . 11
β’
β²π₯ π¦ β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) |
146 | 145, 41 | nfan 1903 |
. . . . . . . . . 10
β’
β²π₯(π¦ β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β§ π§ = β¦π¦ / π₯β¦(if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) |
147 | | eleq1w 2821 |
. . . . . . . . . . 11
β’ (π₯ = π¦ β (π₯ β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β π¦ β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}))) |
148 | 147, 44 | anbi12d 632 |
. . . . . . . . . 10
β’ (π₯ = π¦ β ((π₯ β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β§ π§ = (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) β (π¦ β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β§ π§ = β¦π¦ / π₯β¦(if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))))) |
149 | 142, 146,
148 | cbvopab1 5185 |
. . . . . . . . 9
β’
{β¨π₯, π§β© β£ (π₯ β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β§ π§ = (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0)))} = {β¨π¦, π§β© β£ (π¦ β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β§ π§ = β¦π¦ / π₯β¦(if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0)))} |
150 | | df-mpt 5194 |
. . . . . . . . 9
β’ (π₯ β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) = {β¨π₯, π§β© β£ (π₯ β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β§ π§ = (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0)))} |
151 | | df-mpt 5194 |
. . . . . . . . 9
β’ (π¦ β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β¦ β¦π¦ / π₯β¦(if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) = {β¨π¦, π§β© β£ (π¦ β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β§ π§ = β¦π¦ / π₯β¦(if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0)))} |
152 | 149, 150,
151 | 3eqtr4i 2775 |
. . . . . . . 8
β’ (π₯ β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) = (π¦ β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β¦ β¦π¦ / π₯β¦(if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) |
153 | 140, 141,
152 | 3eqtr4g 2802 |
. . . . . . 7
β’ (({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β π΄ β ((π₯ β π΄ β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) βΎ ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) = (π₯ β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0)))) |
154 | 139, 153 | ax-mp 5 |
. . . . . 6
β’ ((π₯ β π΄ β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) βΎ ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) = (π₯ β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) |
155 | | resmpt 5996 |
. . . . . . . 8
β’ (({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β π΄ β ((π¦ β π΄ β¦ β¦π¦ / π₯β¦πΆ) βΎ ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) = (π¦ β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β¦ β¦π¦ / π₯β¦πΆ)) |
156 | | nfcv 2908 |
. . . . . . . . . 10
β’
β²π¦πΆ |
157 | | nfcsb1v 3885 |
. . . . . . . . . 10
β’
β²π₯β¦π¦ / π₯β¦πΆ |
158 | | csbeq1a 3874 |
. . . . . . . . . 10
β’ (π₯ = π¦ β πΆ = β¦π¦ / π₯β¦πΆ) |
159 | 156, 157,
158 | cbvmpt 5221 |
. . . . . . . . 9
β’ (π₯ β π΄ β¦ πΆ) = (π¦ β π΄ β¦ β¦π¦ / π₯β¦πΆ) |
160 | 159 | reseq1i 5938 |
. . . . . . . 8
β’ ((π₯ β π΄ β¦ πΆ) βΎ ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) = ((π¦ β π΄ β¦ β¦π¦ / π₯β¦πΆ) βΎ ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) |
161 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π¦(π₯ β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β§ π§ = πΆ) |
162 | 157 | nfeq2 2925 |
. . . . . . . . . . 11
β’
β²π₯ π§ = β¦π¦ / π₯β¦πΆ |
163 | 145, 162 | nfan 1903 |
. . . . . . . . . 10
β’
β²π₯(π¦ β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β§ π§ = β¦π¦ / π₯β¦πΆ) |
164 | 158 | eqeq2d 2748 |
. . . . . . . . . . 11
β’ (π₯ = π¦ β (π§ = πΆ β π§ = β¦π¦ / π₯β¦πΆ)) |
165 | 147, 164 | anbi12d 632 |
. . . . . . . . . 10
β’ (π₯ = π¦ β ((π₯ β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β§ π§ = πΆ) β (π¦ β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β§ π§ = β¦π¦ / π₯β¦πΆ))) |
166 | 161, 163,
165 | cbvopab1 5185 |
. . . . . . . . 9
β’
{β¨π₯, π§β© β£ (π₯ β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β§ π§ = πΆ)} = {β¨π¦, π§β© β£ (π¦ β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β§ π§ = β¦π¦ / π₯β¦πΆ)} |
167 | | df-mpt 5194 |
. . . . . . . . 9
β’ (π₯ β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β¦ πΆ) = {β¨π₯, π§β© β£ (π₯ β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β§ π§ = πΆ)} |
168 | | df-mpt 5194 |
. . . . . . . . 9
β’ (π¦ β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β¦ β¦π¦ / π₯β¦πΆ) = {β¨π¦, π§β© β£ (π¦ β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β§ π§ = β¦π¦ / π₯β¦πΆ)} |
169 | 166, 167,
168 | 3eqtr4i 2775 |
. . . . . . . 8
β’ (π₯ β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β¦ πΆ) = (π¦ β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β¦ β¦π¦ / π₯β¦πΆ) |
170 | 155, 160,
169 | 3eqtr4g 2802 |
. . . . . . 7
β’ (({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β π΄ β ((π₯ β π΄ β¦ πΆ) βΎ ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) = (π₯ β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β¦ πΆ)) |
171 | 139, 170 | ax-mp 5 |
. . . . . 6
β’ ((π₯ β π΄ β¦ πΆ) βΎ ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) = (π₯ β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β¦ πΆ) |
172 | 136, 154,
171 | 3eqtr4g 2802 |
. . . . 5
β’ (π β ((π₯ β π΄ β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) βΎ ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) = ((π₯ β π΄ β¦ πΆ) βΎ ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}))) |
173 | 122, 172 | eqtrid 2789 |
. . . 4
β’ (π β (((π₯ β π΄ β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) βΎ {π₯ β π΄ β£ 0 β€ πΆ}) βΎ ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) = ((π₯ β π΄ β¦ πΆ) βΎ ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}))) |
174 | 83 | mptpreima 6195 |
. . . . . . . 8
β’ (β‘(π₯ β π΄ β¦ π΅) β (-β(,)0)) = {π₯ β π΄ β£ π΅ β (-β(,)0)} |
175 | | elioomnf 13368 |
. . . . . . . . . . 11
β’ (0 β
β* β (π΅ β (-β(,)0) β (π΅ β β β§ π΅ < 0))) |
176 | 76, 175 | ax-mp 5 |
. . . . . . . . . 10
β’ (π΅ β (-β(,)0) β
(π΅ β β β§
π΅ < 0)) |
177 | 1 | biantrurd 534 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β (π΅ < 0 β (π΅ β β β§ π΅ < 0))) |
178 | | ltnle 11241 |
. . . . . . . . . . . 12
β’ ((π΅ β β β§ 0 β
β) β (π΅ < 0
β Β¬ 0 β€ π΅)) |
179 | 1, 2, 178 | sylancl 587 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β (π΅ < 0 β Β¬ 0 β€ π΅)) |
180 | 177, 179 | bitr3d 281 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β ((π΅ β β β§ π΅ < 0) β Β¬ 0 β€ π΅)) |
181 | 176, 180 | bitrid 283 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β (π΅ β (-β(,)0) β Β¬ 0 β€
π΅)) |
182 | 181 | rabbidva 3417 |
. . . . . . . 8
β’ (π β {π₯ β π΄ β£ π΅ β (-β(,)0)} = {π₯ β π΄ β£ Β¬ 0 β€ π΅}) |
183 | 174, 182 | eqtrid 2789 |
. . . . . . 7
β’ (π β (β‘(π₯ β π΄ β¦ π΅) β (-β(,)0)) = {π₯ β π΄ β£ Β¬ 0 β€ π΅}) |
184 | | mbfima 25010 |
. . . . . . . 8
β’ (((π₯ β π΄ β¦ π΅) β MblFn β§ (π₯ β π΄ β¦ π΅):π΄βΆβ) β (β‘(π₯ β π΄ β¦ π΅) β (-β(,)0)) β dom
vol) |
185 | 87, 88, 184 | syl2anc 585 |
. . . . . . 7
β’ (π β (β‘(π₯ β π΄ β¦ π΅) β (-β(,)0)) β dom
vol) |
186 | 183, 185 | eqeltrrd 2839 |
. . . . . 6
β’ (π β {π₯ β π΄ β£ Β¬ 0 β€ π΅} β dom vol) |
187 | | inmbl 24922 |
. . . . . 6
β’ (({π₯ β π΄ β£ Β¬ 0 β€ π΅} β dom vol β§ {π₯ β π΄ β£ 0 β€ πΆ} β dom vol) β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β dom vol) |
188 | 186, 114,
187 | syl2anc 585 |
. . . . 5
β’ (π β ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β dom vol) |
189 | | mbfres 25024 |
. . . . 5
β’ (((π₯ β π΄ β¦ πΆ) β MblFn β§ ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) β dom vol) β ((π₯ β π΄ β¦ πΆ) βΎ ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) β MblFn) |
190 | 106, 188,
189 | syl2anc 585 |
. . . 4
β’ (π β ((π₯ β π΄ β¦ πΆ) βΎ ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) β MblFn) |
191 | 173, 190 | eqeltrd 2838 |
. . 3
β’ (π β (((π₯ β π΄ β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) βΎ {π₯ β π΄ β£ 0 β€ πΆ}) βΎ ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) β MblFn) |
192 | | ssid 3971 |
. . . . . 6
β’ π΄ β π΄ |
193 | | dfrab3ss 4277 |
. . . . . 6
β’ (π΄ β π΄ β {π₯ β π΄ β£ 0 β€ πΆ} = (π΄ β© {π₯ β π΄ β£ 0 β€ πΆ})) |
194 | 192, 193 | ax-mp 5 |
. . . . 5
β’ {π₯ β π΄ β£ 0 β€ πΆ} = (π΄ β© {π₯ β π΄ β£ 0 β€ πΆ}) |
195 | | rabxm 4351 |
. . . . . 6
β’ π΄ = ({π₯ β π΄ β£ 0 β€ π΅} βͺ {π₯ β π΄ β£ Β¬ 0 β€ π΅}) |
196 | 195 | ineq1i 4173 |
. . . . 5
β’ (π΄ β© {π₯ β π΄ β£ 0 β€ πΆ}) = (({π₯ β π΄ β£ 0 β€ π΅} βͺ {π₯ β π΄ β£ Β¬ 0 β€ π΅}) β© {π₯ β π΄ β£ 0 β€ πΆ}) |
197 | | indir 4240 |
. . . . 5
β’ (({π₯ β π΄ β£ 0 β€ π΅} βͺ {π₯ β π΄ β£ Β¬ 0 β€ π΅}) β© {π₯ β π΄ β£ 0 β€ πΆ}) = (({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) βͺ ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) |
198 | 194, 196,
197 | 3eqtrri 2770 |
. . . 4
β’ (({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) βͺ ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) = {π₯ β π΄ β£ 0 β€ πΆ} |
199 | 198 | a1i 11 |
. . 3
β’ (π β (({π₯ β π΄ β£ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ}) βͺ ({π₯ β π΄ β£ Β¬ 0 β€ π΅} β© {π₯ β π΄ β£ 0 β€ πΆ})) = {π₯ β π΄ β£ 0 β€ πΆ}) |
200 | 12, 119, 191, 199 | mbfres2 25025 |
. 2
β’ (π β ((π₯ β π΄ β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) βΎ {π₯ β π΄ β£ 0 β€ πΆ}) β MblFn) |
201 | | rabid 3430 |
. . . . . 6
β’ (π₯ β {π₯ β π΄ β£ Β¬ 0 β€ πΆ} β (π₯ β π΄ β§ Β¬ 0 β€ πΆ)) |
202 | | iffalse 4500 |
. . . . . . . . 9
β’ (Β¬ 0
β€ πΆ β if(0 β€
πΆ, πΆ, 0) = 0) |
203 | 202 | oveq2d 7378 |
. . . . . . . 8
β’ (Β¬ 0
β€ πΆ β (if(0 β€
π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0)) = (if(0 β€ π΅, π΅, 0) + 0)) |
204 | 4 | recnd 11190 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β if(0 β€ π΅, π΅, 0) β β) |
205 | 204 | addid1d 11362 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄) β (if(0 β€ π΅, π΅, 0) + 0) = if(0 β€ π΅, π΅, 0)) |
206 | 203, 205 | sylan9eqr 2799 |
. . . . . . 7
β’ (((π β§ π₯ β π΄) β§ Β¬ 0 β€ πΆ) β (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0)) = if(0 β€ π΅, π΅, 0)) |
207 | 206 | anasss 468 |
. . . . . 6
β’ ((π β§ (π₯ β π΄ β§ Β¬ 0 β€ πΆ)) β (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0)) = if(0 β€ π΅, π΅, 0)) |
208 | 201, 207 | sylan2b 595 |
. . . . 5
β’ ((π β§ π₯ β {π₯ β π΄ β£ Β¬ 0 β€ πΆ}) β (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0)) = if(0 β€ π΅, π΅, 0)) |
209 | 208 | mpteq2dva 5210 |
. . . 4
β’ (π β (π₯ β {π₯ β π΄ β£ Β¬ 0 β€ πΆ} β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) = (π₯ β {π₯ β π΄ β£ Β¬ 0 β€ πΆ} β¦ if(0 β€ π΅, π΅, 0))) |
210 | | ssrab2 4042 |
. . . . 5
β’ {π₯ β π΄ β£ Β¬ 0 β€ πΆ} β π΄ |
211 | | resmpt 5996 |
. . . . . 6
β’ ({π₯ β π΄ β£ Β¬ 0 β€ πΆ} β π΄ β ((π¦ β π΄ β¦ β¦π¦ / π₯β¦(if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) βΎ {π₯ β π΄ β£ Β¬ 0 β€ πΆ}) = (π¦ β {π₯ β π΄ β£ Β¬ 0 β€ πΆ} β¦ β¦π¦ / π₯β¦(if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0)))) |
212 | 34 | reseq1i 5938 |
. . . . . 6
β’ ((π₯ β π΄ β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) βΎ {π₯ β π΄ β£ Β¬ 0 β€ πΆ}) = ((π¦ β π΄ β¦ β¦π¦ / π₯β¦(if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) βΎ {π₯ β π΄ β£ Β¬ 0 β€ πΆ}) |
213 | | nfv 1918 |
. . . . . . . 8
β’
β²π¦(π₯ β {π₯ β π΄ β£ Β¬ 0 β€ πΆ} β§ π§ = (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) |
214 | | nfrab1 3429 |
. . . . . . . . . 10
β’
β²π₯{π₯ β π΄ β£ Β¬ 0 β€ πΆ} |
215 | 214 | nfcri 2895 |
. . . . . . . . 9
β’
β²π₯ π¦ β {π₯ β π΄ β£ Β¬ 0 β€ πΆ} |
216 | 215, 41 | nfan 1903 |
. . . . . . . 8
β’
β²π₯(π¦ β {π₯ β π΄ β£ Β¬ 0 β€ πΆ} β§ π§ = β¦π¦ / π₯β¦(if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) |
217 | | eleq1w 2821 |
. . . . . . . . 9
β’ (π₯ = π¦ β (π₯ β {π₯ β π΄ β£ Β¬ 0 β€ πΆ} β π¦ β {π₯ β π΄ β£ Β¬ 0 β€ πΆ})) |
218 | 217, 44 | anbi12d 632 |
. . . . . . . 8
β’ (π₯ = π¦ β ((π₯ β {π₯ β π΄ β£ Β¬ 0 β€ πΆ} β§ π§ = (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) β (π¦ β {π₯ β π΄ β£ Β¬ 0 β€ πΆ} β§ π§ = β¦π¦ / π₯β¦(if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))))) |
219 | 213, 216,
218 | cbvopab1 5185 |
. . . . . . 7
β’
{β¨π₯, π§β© β£ (π₯ β {π₯ β π΄ β£ Β¬ 0 β€ πΆ} β§ π§ = (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0)))} = {β¨π¦, π§β© β£ (π¦ β {π₯ β π΄ β£ Β¬ 0 β€ πΆ} β§ π§ = β¦π¦ / π₯β¦(if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0)))} |
220 | | df-mpt 5194 |
. . . . . . 7
β’ (π₯ β {π₯ β π΄ β£ Β¬ 0 β€ πΆ} β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) = {β¨π₯, π§β© β£ (π₯ β {π₯ β π΄ β£ Β¬ 0 β€ πΆ} β§ π§ = (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0)))} |
221 | | df-mpt 5194 |
. . . . . . 7
β’ (π¦ β {π₯ β π΄ β£ Β¬ 0 β€ πΆ} β¦ β¦π¦ / π₯β¦(if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) = {β¨π¦, π§β© β£ (π¦ β {π₯ β π΄ β£ Β¬ 0 β€ πΆ} β§ π§ = β¦π¦ / π₯β¦(if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0)))} |
222 | 219, 220,
221 | 3eqtr4i 2775 |
. . . . . 6
β’ (π₯ β {π₯ β π΄ β£ Β¬ 0 β€ πΆ} β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) = (π¦ β {π₯ β π΄ β£ Β¬ 0 β€ πΆ} β¦ β¦π¦ / π₯β¦(if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) |
223 | 211, 212,
222 | 3eqtr4g 2802 |
. . . . 5
β’ ({π₯ β π΄ β£ Β¬ 0 β€ πΆ} β π΄ β ((π₯ β π΄ β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) βΎ {π₯ β π΄ β£ Β¬ 0 β€ πΆ}) = (π₯ β {π₯ β π΄ β£ Β¬ 0 β€ πΆ} β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0)))) |
224 | 210, 223 | ax-mp 5 |
. . . 4
β’ ((π₯ β π΄ β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) βΎ {π₯ β π΄ β£ Β¬ 0 β€ πΆ}) = (π₯ β {π₯ β π΄ β£ Β¬ 0 β€ πΆ} β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) |
225 | | resmpt 5996 |
. . . . . 6
β’ ({π₯ β π΄ β£ Β¬ 0 β€ πΆ} β π΄ β ((π¦ β π΄ β¦ β¦π¦ / π₯β¦if(0 β€ π΅, π΅, 0)) βΎ {π₯ β π΄ β£ Β¬ 0 β€ πΆ}) = (π¦ β {π₯ β π΄ β£ Β¬ 0 β€ πΆ} β¦ β¦π¦ / π₯β¦if(0 β€ π΅, π΅, 0))) |
226 | | nfcv 2908 |
. . . . . . . 8
β’
β²π¦if(0
β€ π΅, π΅, 0) |
227 | | nfcsb1v 3885 |
. . . . . . . 8
β’
β²π₯β¦π¦ / π₯β¦if(0 β€ π΅, π΅, 0) |
228 | | csbeq1a 3874 |
. . . . . . . 8
β’ (π₯ = π¦ β if(0 β€ π΅, π΅, 0) = β¦π¦ / π₯β¦if(0 β€ π΅, π΅, 0)) |
229 | 226, 227,
228 | cbvmpt 5221 |
. . . . . . 7
β’ (π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) = (π¦ β π΄ β¦ β¦π¦ / π₯β¦if(0 β€ π΅, π΅, 0)) |
230 | 229 | reseq1i 5938 |
. . . . . 6
β’ ((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) βΎ {π₯ β π΄ β£ Β¬ 0 β€ πΆ}) = ((π¦ β π΄ β¦ β¦π¦ / π₯β¦if(0 β€ π΅, π΅, 0)) βΎ {π₯ β π΄ β£ Β¬ 0 β€ πΆ}) |
231 | | nfv 1918 |
. . . . . . . 8
β’
β²π¦(π₯ β {π₯ β π΄ β£ Β¬ 0 β€ πΆ} β§ π§ = if(0 β€ π΅, π΅, 0)) |
232 | 227 | nfeq2 2925 |
. . . . . . . . 9
β’
β²π₯ π§ = β¦π¦ / π₯β¦if(0 β€ π΅, π΅, 0) |
233 | 215, 232 | nfan 1903 |
. . . . . . . 8
β’
β²π₯(π¦ β {π₯ β π΄ β£ Β¬ 0 β€ πΆ} β§ π§ = β¦π¦ / π₯β¦if(0 β€ π΅, π΅, 0)) |
234 | 228 | eqeq2d 2748 |
. . . . . . . . 9
β’ (π₯ = π¦ β (π§ = if(0 β€ π΅, π΅, 0) β π§ = β¦π¦ / π₯β¦if(0 β€ π΅, π΅, 0))) |
235 | 217, 234 | anbi12d 632 |
. . . . . . . 8
β’ (π₯ = π¦ β ((π₯ β {π₯ β π΄ β£ Β¬ 0 β€ πΆ} β§ π§ = if(0 β€ π΅, π΅, 0)) β (π¦ β {π₯ β π΄ β£ Β¬ 0 β€ πΆ} β§ π§ = β¦π¦ / π₯β¦if(0 β€ π΅, π΅, 0)))) |
236 | 231, 233,
235 | cbvopab1 5185 |
. . . . . . 7
β’
{β¨π₯, π§β© β£ (π₯ β {π₯ β π΄ β£ Β¬ 0 β€ πΆ} β§ π§ = if(0 β€ π΅, π΅, 0))} = {β¨π¦, π§β© β£ (π¦ β {π₯ β π΄ β£ Β¬ 0 β€ πΆ} β§ π§ = β¦π¦ / π₯β¦if(0 β€ π΅, π΅, 0))} |
237 | | df-mpt 5194 |
. . . . . . 7
β’ (π₯ β {π₯ β π΄ β£ Β¬ 0 β€ πΆ} β¦ if(0 β€ π΅, π΅, 0)) = {β¨π₯, π§β© β£ (π₯ β {π₯ β π΄ β£ Β¬ 0 β€ πΆ} β§ π§ = if(0 β€ π΅, π΅, 0))} |
238 | | df-mpt 5194 |
. . . . . . 7
β’ (π¦ β {π₯ β π΄ β£ Β¬ 0 β€ πΆ} β¦ β¦π¦ / π₯β¦if(0 β€ π΅, π΅, 0)) = {β¨π¦, π§β© β£ (π¦ β {π₯ β π΄ β£ Β¬ 0 β€ πΆ} β§ π§ = β¦π¦ / π₯β¦if(0 β€ π΅, π΅, 0))} |
239 | 236, 237,
238 | 3eqtr4i 2775 |
. . . . . 6
β’ (π₯ β {π₯ β π΄ β£ Β¬ 0 β€ πΆ} β¦ if(0 β€ π΅, π΅, 0)) = (π¦ β {π₯ β π΄ β£ Β¬ 0 β€ πΆ} β¦ β¦π¦ / π₯β¦if(0 β€ π΅, π΅, 0)) |
240 | 225, 230,
239 | 3eqtr4g 2802 |
. . . . 5
β’ ({π₯ β π΄ β£ Β¬ 0 β€ πΆ} β π΄ β ((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) βΎ {π₯ β π΄ β£ Β¬ 0 β€ πΆ}) = (π₯ β {π₯ β π΄ β£ Β¬ 0 β€ πΆ} β¦ if(0 β€ π΅, π΅, 0))) |
241 | 210, 240 | ax-mp 5 |
. . . 4
β’ ((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) βΎ {π₯ β π΄ β£ Β¬ 0 β€ πΆ}) = (π₯ β {π₯ β π΄ β£ Β¬ 0 β€ πΆ} β¦ if(0 β€ π΅, π΅, 0)) |
242 | 209, 224,
241 | 3eqtr4g 2802 |
. . 3
β’ (π β ((π₯ β π΄ β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) βΎ {π₯ β π΄ β£ Β¬ 0 β€ πΆ}) = ((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) βΎ {π₯ β π΄ β£ Β¬ 0 β€ πΆ})) |
243 | 1, 87 | mbfpos 25031 |
. . . 4
β’ (π β (π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β MblFn) |
244 | 102 | mptpreima 6195 |
. . . . . 6
β’ (β‘(π₯ β π΄ β¦ πΆ) β (-β(,)0)) = {π₯ β π΄ β£ πΆ β (-β(,)0)} |
245 | | elioomnf 13368 |
. . . . . . . . 9
β’ (0 β
β* β (πΆ β (-β(,)0) β (πΆ β β β§ πΆ < 0))) |
246 | 76, 245 | ax-mp 5 |
. . . . . . . 8
β’ (πΆ β (-β(,)0) β
(πΆ β β β§
πΆ < 0)) |
247 | 5 | biantrurd 534 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β (πΆ < 0 β (πΆ β β β§ πΆ < 0))) |
248 | | ltnle 11241 |
. . . . . . . . . 10
β’ ((πΆ β β β§ 0 β
β) β (πΆ < 0
β Β¬ 0 β€ πΆ)) |
249 | 5, 2, 248 | sylancl 587 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β (πΆ < 0 β Β¬ 0 β€ πΆ)) |
250 | 247, 249 | bitr3d 281 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄) β ((πΆ β β β§ πΆ < 0) β Β¬ 0 β€ πΆ)) |
251 | 246, 250 | bitrid 283 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β (πΆ β (-β(,)0) β Β¬ 0 β€
πΆ)) |
252 | 251 | rabbidva 3417 |
. . . . . 6
β’ (π β {π₯ β π΄ β£ πΆ β (-β(,)0)} = {π₯ β π΄ β£ Β¬ 0 β€ πΆ}) |
253 | 244, 252 | eqtrid 2789 |
. . . . 5
β’ (π β (β‘(π₯ β π΄ β¦ πΆ) β (-β(,)0)) = {π₯ β π΄ β£ Β¬ 0 β€ πΆ}) |
254 | | mbfima 25010 |
. . . . . 6
β’ (((π₯ β π΄ β¦ πΆ) β MblFn β§ (π₯ β π΄ β¦ πΆ):π΄βΆβ) β (β‘(π₯ β π΄ β¦ πΆ) β (-β(,)0)) β dom
vol) |
255 | 106, 107,
254 | syl2anc 585 |
. . . . 5
β’ (π β (β‘(π₯ β π΄ β¦ πΆ) β (-β(,)0)) β dom
vol) |
256 | 253, 255 | eqeltrrd 2839 |
. . . 4
β’ (π β {π₯ β π΄ β£ Β¬ 0 β€ πΆ} β dom vol) |
257 | | mbfres 25024 |
. . . 4
β’ (((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β MblFn β§ {π₯ β π΄ β£ Β¬ 0 β€ πΆ} β dom vol) β ((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) βΎ {π₯ β π΄ β£ Β¬ 0 β€ πΆ}) β MblFn) |
258 | 243, 256,
257 | syl2anc 585 |
. . 3
β’ (π β ((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) βΎ {π₯ β π΄ β£ Β¬ 0 β€ πΆ}) β MblFn) |
259 | 242, 258 | eqeltrd 2838 |
. 2
β’ (π β ((π₯ β π΄ β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) βΎ {π₯ β π΄ β£ Β¬ 0 β€ πΆ}) β MblFn) |
260 | | rabxm 4351 |
. . . 4
β’ π΄ = ({π₯ β π΄ β£ 0 β€ πΆ} βͺ {π₯ β π΄ β£ Β¬ 0 β€ πΆ}) |
261 | 260 | eqcomi 2746 |
. . 3
β’ ({π₯ β π΄ β£ 0 β€ πΆ} βͺ {π₯ β π΄ β£ Β¬ 0 β€ πΆ}) = π΄ |
262 | 261 | a1i 11 |
. 2
β’ (π β ({π₯ β π΄ β£ 0 β€ πΆ} βͺ {π₯ β π΄ β£ Β¬ 0 β€ πΆ}) = π΄) |
263 | 9, 200, 259, 262 | mbfres2 25025 |
1
β’ (π β (π₯ β π΄ β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) β MblFn) |