Step | Hyp | Ref
| Expression |
1 | | readdcl 11141 |
. . . 4
β’ ((π₯ β β β§ π¦ β β) β (π₯ + π¦) β β) |
2 | 1 | adantl 483 |
. . 3
β’ ((π β§ (π₯ β β β§ π¦ β β)) β (π₯ + π¦) β β) |
3 | | mbfadd.3 |
. . 3
β’ (π β πΉ:π΄βΆβ) |
4 | | mbfadd.4 |
. . 3
β’ (π β πΊ:π΄βΆβ) |
5 | 3 | fdmd 6684 |
. . . 4
β’ (π β dom πΉ = π΄) |
6 | | mbfadd.1 |
. . . . 5
β’ (π β πΉ β MblFn) |
7 | | mbfdm 25006 |
. . . . 5
β’ (πΉ β MblFn β dom πΉ β dom
vol) |
8 | 6, 7 | syl 17 |
. . . 4
β’ (π β dom πΉ β dom vol) |
9 | 5, 8 | eqeltrrd 2839 |
. . 3
β’ (π β π΄ β dom vol) |
10 | | inidm 4183 |
. . 3
β’ (π΄ β© π΄) = π΄ |
11 | 2, 3, 4, 9, 9, 10 | off 7640 |
. 2
β’ (π β (πΉ βf + πΊ):π΄βΆβ) |
12 | | eliun 4963 |
. . . . 5
β’ (π₯ β βͺ π β β ((β‘πΉ β (π(,)+β)) β© (β‘πΊ β ((π¦ β π)(,)+β))) β βπ β β π₯ β ((β‘πΉ β (π(,)+β)) β© (β‘πΊ β ((π¦ β π)(,)+β)))) |
13 | | r19.42v 3188 |
. . . . . . 7
β’
(βπ β
β (π₯ β π΄ β§ ((πΉβπ₯) β (π(,)+β) β§ (πΊβπ₯) β ((π¦ β π)(,)+β))) β (π₯ β π΄ β§ βπ β β ((πΉβπ₯) β (π(,)+β) β§ (πΊβπ₯) β ((π¦ β π)(,)+β)))) |
14 | | simplr 768 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β π¦ β β) |
15 | 4 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β β) β πΊ:π΄βΆβ) |
16 | 15 | ffvelcdmda 7040 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β (πΊβπ₯) β β) |
17 | 3 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β β) β πΉ:π΄βΆβ) |
18 | 17 | ffvelcdmda 7040 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β (πΉβπ₯) β β) |
19 | 14, 16, 18 | ltsubaddd 11758 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β ((π¦ β (πΊβπ₯)) < (πΉβπ₯) β π¦ < ((πΉβπ₯) + (πΊβπ₯)))) |
20 | 14 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π¦ β β) β§ π₯ β π΄) β§ π β β) β π¦ β β) |
21 | | qre 12885 |
. . . . . . . . . . . . . . 15
β’ (π β β β π β
β) |
22 | 21 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π¦ β β) β§ π₯ β π΄) β§ π β β) β π β β) |
23 | 16 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π¦ β β) β§ π₯ β π΄) β§ π β β) β (πΊβπ₯) β β) |
24 | | ltsub23 11642 |
. . . . . . . . . . . . . 14
β’ ((π¦ β β β§ π β β β§ (πΊβπ₯) β β) β ((π¦ β π) < (πΊβπ₯) β (π¦ β (πΊβπ₯)) < π)) |
25 | 20, 22, 23, 24 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((((π β§ π¦ β β) β§ π₯ β π΄) β§ π β β) β ((π¦ β π) < (πΊβπ₯) β (π¦ β (πΊβπ₯)) < π)) |
26 | 25 | anbi1cd 635 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β β) β§ π₯ β π΄) β§ π β β) β ((π < (πΉβπ₯) β§ (π¦ β π) < (πΊβπ₯)) β ((π¦ β (πΊβπ₯)) < π β§ π < (πΉβπ₯)))) |
27 | 26 | rexbidva 3174 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β (βπ β β (π < (πΉβπ₯) β§ (π¦ β π) < (πΊβπ₯)) β βπ β β ((π¦ β (πΊβπ₯)) < π β§ π < (πΉβπ₯)))) |
28 | 14, 16 | resubcld 11590 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β (π¦ β (πΊβπ₯)) β β) |
29 | 28 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π¦ β β) β§ π₯ β π΄) β§ π β β) β (π¦ β (πΊβπ₯)) β β) |
30 | 18 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π¦ β β) β§ π₯ β π΄) β§ π β β) β (πΉβπ₯) β β) |
31 | | lttr 11238 |
. . . . . . . . . . . . . 14
β’ (((π¦ β (πΊβπ₯)) β β β§ π β β β§ (πΉβπ₯) β β) β (((π¦ β (πΊβπ₯)) < π β§ π < (πΉβπ₯)) β (π¦ β (πΊβπ₯)) < (πΉβπ₯))) |
32 | 29, 22, 30, 31 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((((π β§ π¦ β β) β§ π₯ β π΄) β§ π β β) β (((π¦ β (πΊβπ₯)) < π β§ π < (πΉβπ₯)) β (π¦ β (πΊβπ₯)) < (πΉβπ₯))) |
33 | 32 | rexlimdva 3153 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β (βπ β β ((π¦ β (πΊβπ₯)) < π β§ π < (πΉβπ₯)) β (π¦ β (πΊβπ₯)) < (πΉβπ₯))) |
34 | | qbtwnre 13125 |
. . . . . . . . . . . . . 14
β’ (((π¦ β (πΊβπ₯)) β β β§ (πΉβπ₯) β β β§ (π¦ β (πΊβπ₯)) < (πΉβπ₯)) β βπ β β ((π¦ β (πΊβπ₯)) < π β§ π < (πΉβπ₯))) |
35 | 34 | 3expia 1122 |
. . . . . . . . . . . . 13
β’ (((π¦ β (πΊβπ₯)) β β β§ (πΉβπ₯) β β) β ((π¦ β (πΊβπ₯)) < (πΉβπ₯) β βπ β β ((π¦ β (πΊβπ₯)) < π β§ π < (πΉβπ₯)))) |
36 | 28, 18, 35 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β ((π¦ β (πΊβπ₯)) < (πΉβπ₯) β βπ β β ((π¦ β (πΊβπ₯)) < π β§ π < (πΉβπ₯)))) |
37 | 33, 36 | impbid 211 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β (βπ β β ((π¦ β (πΊβπ₯)) < π β§ π < (πΉβπ₯)) β (π¦ β (πΊβπ₯)) < (πΉβπ₯))) |
38 | 27, 37 | bitrd 279 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β (βπ β β (π < (πΉβπ₯) β§ (π¦ β π) < (πΊβπ₯)) β (π¦ β (πΊβπ₯)) < (πΉβπ₯))) |
39 | 3 | ffnd 6674 |
. . . . . . . . . . . . 13
β’ (π β πΉ Fn π΄) |
40 | 39 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β β) β πΉ Fn π΄) |
41 | 4 | ffnd 6674 |
. . . . . . . . . . . . 13
β’ (π β πΊ Fn π΄) |
42 | 41 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β β) β πΊ Fn π΄) |
43 | 9 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β β) β π΄ β dom vol) |
44 | | eqidd 2738 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β (πΉβπ₯) = (πΉβπ₯)) |
45 | | eqidd 2738 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β (πΊβπ₯) = (πΊβπ₯)) |
46 | 40, 42, 43, 43, 10, 44, 45 | ofval 7633 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β ((πΉ βf + πΊ)βπ₯) = ((πΉβπ₯) + (πΊβπ₯))) |
47 | 46 | breq2d 5122 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β (π¦ < ((πΉ βf + πΊ)βπ₯) β π¦ < ((πΉβπ₯) + (πΊβπ₯)))) |
48 | 19, 38, 47 | 3bitr4d 311 |
. . . . . . . . 9
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β (βπ β β (π < (πΉβπ₯) β§ (π¦ β π) < (πΊβπ₯)) β π¦ < ((πΉ βf + πΊ)βπ₯))) |
49 | 22 | rexrd 11212 |
. . . . . . . . . . . . 13
β’ ((((π β§ π¦ β β) β§ π₯ β π΄) β§ π β β) β π β β*) |
50 | | elioopnf 13367 |
. . . . . . . . . . . . 13
β’ (π β β*
β ((πΉβπ₯) β (π(,)+β) β ((πΉβπ₯) β β β§ π < (πΉβπ₯)))) |
51 | 49, 50 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β β) β§ π₯ β π΄) β§ π β β) β ((πΉβπ₯) β (π(,)+β) β ((πΉβπ₯) β β β§ π < (πΉβπ₯)))) |
52 | 30, 51 | mpbirand 706 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β β) β§ π₯ β π΄) β§ π β β) β ((πΉβπ₯) β (π(,)+β) β π < (πΉβπ₯))) |
53 | 20, 22 | resubcld 11590 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π¦ β β) β§ π₯ β π΄) β§ π β β) β (π¦ β π) β β) |
54 | 53 | rexrd 11212 |
. . . . . . . . . . . . 13
β’ ((((π β§ π¦ β β) β§ π₯ β π΄) β§ π β β) β (π¦ β π) β
β*) |
55 | | elioopnf 13367 |
. . . . . . . . . . . . 13
β’ ((π¦ β π) β β* β ((πΊβπ₯) β ((π¦ β π)(,)+β) β ((πΊβπ₯) β β β§ (π¦ β π) < (πΊβπ₯)))) |
56 | 54, 55 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β β) β§ π₯ β π΄) β§ π β β) β ((πΊβπ₯) β ((π¦ β π)(,)+β) β ((πΊβπ₯) β β β§ (π¦ β π) < (πΊβπ₯)))) |
57 | 23, 56 | mpbirand 706 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β β) β§ π₯ β π΄) β§ π β β) β ((πΊβπ₯) β ((π¦ β π)(,)+β) β (π¦ β π) < (πΊβπ₯))) |
58 | 52, 57 | anbi12d 632 |
. . . . . . . . . 10
β’ ((((π β§ π¦ β β) β§ π₯ β π΄) β§ π β β) β (((πΉβπ₯) β (π(,)+β) β§ (πΊβπ₯) β ((π¦ β π)(,)+β)) β (π < (πΉβπ₯) β§ (π¦ β π) < (πΊβπ₯)))) |
59 | 58 | rexbidva 3174 |
. . . . . . . . 9
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β (βπ β β ((πΉβπ₯) β (π(,)+β) β§ (πΊβπ₯) β ((π¦ β π)(,)+β)) β βπ β β (π < (πΉβπ₯) β§ (π¦ β π) < (πΊβπ₯)))) |
60 | 11 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β β) β (πΉ βf + πΊ):π΄βΆβ) |
61 | 60 | ffvelcdmda 7040 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β ((πΉ βf + πΊ)βπ₯) β β) |
62 | 14 | rexrd 11212 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β π¦ β β*) |
63 | | elioopnf 13367 |
. . . . . . . . . . 11
β’ (π¦ β β*
β (((πΉ
βf + πΊ)βπ₯) β (π¦(,)+β) β (((πΉ βf + πΊ)βπ₯) β β β§ π¦ < ((πΉ βf + πΊ)βπ₯)))) |
64 | 62, 63 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β (((πΉ βf + πΊ)βπ₯) β (π¦(,)+β) β (((πΉ βf + πΊ)βπ₯) β β β§ π¦ < ((πΉ βf + πΊ)βπ₯)))) |
65 | 61, 64 | mpbirand 706 |
. . . . . . . . 9
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β (((πΉ βf + πΊ)βπ₯) β (π¦(,)+β) β π¦ < ((πΉ βf + πΊ)βπ₯))) |
66 | 48, 59, 65 | 3bitr4d 311 |
. . . . . . . 8
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β (βπ β β ((πΉβπ₯) β (π(,)+β) β§ (πΊβπ₯) β ((π¦ β π)(,)+β)) β ((πΉ βf + πΊ)βπ₯) β (π¦(,)+β))) |
67 | 66 | pm5.32da 580 |
. . . . . . 7
β’ ((π β§ π¦ β β) β ((π₯ β π΄ β§ βπ β β ((πΉβπ₯) β (π(,)+β) β§ (πΊβπ₯) β ((π¦ β π)(,)+β))) β (π₯ β π΄ β§ ((πΉ βf + πΊ)βπ₯) β (π¦(,)+β)))) |
68 | 13, 67 | bitrid 283 |
. . . . . 6
β’ ((π β§ π¦ β β) β (βπ β β (π₯ β π΄ β§ ((πΉβπ₯) β (π(,)+β) β§ (πΊβπ₯) β ((π¦ β π)(,)+β))) β (π₯ β π΄ β§ ((πΉ βf + πΊ)βπ₯) β (π¦(,)+β)))) |
69 | | elpreima 7013 |
. . . . . . . . . 10
β’ (πΉ Fn π΄ β (π₯ β (β‘πΉ β (π(,)+β)) β (π₯ β π΄ β§ (πΉβπ₯) β (π(,)+β)))) |
70 | 40, 69 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π¦ β β) β (π₯ β (β‘πΉ β (π(,)+β)) β (π₯ β π΄ β§ (πΉβπ₯) β (π(,)+β)))) |
71 | | elpreima 7013 |
. . . . . . . . . 10
β’ (πΊ Fn π΄ β (π₯ β (β‘πΊ β ((π¦ β π)(,)+β)) β (π₯ β π΄ β§ (πΊβπ₯) β ((π¦ β π)(,)+β)))) |
72 | 42, 71 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π¦ β β) β (π₯ β (β‘πΊ β ((π¦ β π)(,)+β)) β (π₯ β π΄ β§ (πΊβπ₯) β ((π¦ β π)(,)+β)))) |
73 | 70, 72 | anbi12d 632 |
. . . . . . . 8
β’ ((π β§ π¦ β β) β ((π₯ β (β‘πΉ β (π(,)+β)) β§ π₯ β (β‘πΊ β ((π¦ β π)(,)+β))) β ((π₯ β π΄ β§ (πΉβπ₯) β (π(,)+β)) β§ (π₯ β π΄ β§ (πΊβπ₯) β ((π¦ β π)(,)+β))))) |
74 | | elin 3931 |
. . . . . . . 8
β’ (π₯ β ((β‘πΉ β (π(,)+β)) β© (β‘πΊ β ((π¦ β π)(,)+β))) β (π₯ β (β‘πΉ β (π(,)+β)) β§ π₯ β (β‘πΊ β ((π¦ β π)(,)+β)))) |
75 | | anandi 675 |
. . . . . . . 8
β’ ((π₯ β π΄ β§ ((πΉβπ₯) β (π(,)+β) β§ (πΊβπ₯) β ((π¦ β π)(,)+β))) β ((π₯ β π΄ β§ (πΉβπ₯) β (π(,)+β)) β§ (π₯ β π΄ β§ (πΊβπ₯) β ((π¦ β π)(,)+β)))) |
76 | 73, 74, 75 | 3bitr4g 314 |
. . . . . . 7
β’ ((π β§ π¦ β β) β (π₯ β ((β‘πΉ β (π(,)+β)) β© (β‘πΊ β ((π¦ β π)(,)+β))) β (π₯ β π΄ β§ ((πΉβπ₯) β (π(,)+β) β§ (πΊβπ₯) β ((π¦ β π)(,)+β))))) |
77 | 76 | rexbidv 3176 |
. . . . . 6
β’ ((π β§ π¦ β β) β (βπ β β π₯ β ((β‘πΉ β (π(,)+β)) β© (β‘πΊ β ((π¦ β π)(,)+β))) β βπ β β (π₯ β π΄ β§ ((πΉβπ₯) β (π(,)+β) β§ (πΊβπ₯) β ((π¦ β π)(,)+β))))) |
78 | 11 | ffnd 6674 |
. . . . . . . 8
β’ (π β (πΉ βf + πΊ) Fn π΄) |
79 | 78 | adantr 482 |
. . . . . . 7
β’ ((π β§ π¦ β β) β (πΉ βf + πΊ) Fn π΄) |
80 | | elpreima 7013 |
. . . . . . 7
β’ ((πΉ βf + πΊ) Fn π΄ β (π₯ β (β‘(πΉ βf + πΊ) β (π¦(,)+β)) β (π₯ β π΄ β§ ((πΉ βf + πΊ)βπ₯) β (π¦(,)+β)))) |
81 | 79, 80 | syl 17 |
. . . . . 6
β’ ((π β§ π¦ β β) β (π₯ β (β‘(πΉ βf + πΊ) β (π¦(,)+β)) β (π₯ β π΄ β§ ((πΉ βf + πΊ)βπ₯) β (π¦(,)+β)))) |
82 | 68, 77, 81 | 3bitr4d 311 |
. . . . 5
β’ ((π β§ π¦ β β) β (βπ β β π₯ β ((β‘πΉ β (π(,)+β)) β© (β‘πΊ β ((π¦ β π)(,)+β))) β π₯ β (β‘(πΉ βf + πΊ) β (π¦(,)+β)))) |
83 | 12, 82 | bitrid 283 |
. . . 4
β’ ((π β§ π¦ β β) β (π₯ β βͺ
π β β ((β‘πΉ β (π(,)+β)) β© (β‘πΊ β ((π¦ β π)(,)+β))) β π₯ β (β‘(πΉ βf + πΊ) β (π¦(,)+β)))) |
84 | 83 | eqrdv 2735 |
. . 3
β’ ((π β§ π¦ β β) β βͺ π β β ((β‘πΉ β (π(,)+β)) β© (β‘πΊ β ((π¦ β π)(,)+β))) = (β‘(πΉ βf + πΊ) β (π¦(,)+β))) |
85 | | qnnen 16102 |
. . . . 5
β’ β
β β |
86 | | endom 8926 |
. . . . 5
β’ (β
β β β β βΌ β) |
87 | 85, 86 | ax-mp 5 |
. . . 4
β’ β
βΌ β |
88 | | mbfima 25010 |
. . . . . . . 8
β’ ((πΉ β MblFn β§ πΉ:π΄βΆβ) β (β‘πΉ β (π(,)+β)) β dom
vol) |
89 | 6, 3, 88 | syl2anc 585 |
. . . . . . 7
β’ (π β (β‘πΉ β (π(,)+β)) β dom
vol) |
90 | | mbfadd.2 |
. . . . . . . 8
β’ (π β πΊ β MblFn) |
91 | | mbfima 25010 |
. . . . . . . 8
β’ ((πΊ β MblFn β§ πΊ:π΄βΆβ) β (β‘πΊ β ((π¦ β π)(,)+β)) β dom
vol) |
92 | 90, 4, 91 | syl2anc 585 |
. . . . . . 7
β’ (π β (β‘πΊ β ((π¦ β π)(,)+β)) β dom
vol) |
93 | | inmbl 24922 |
. . . . . . 7
β’ (((β‘πΉ β (π(,)+β)) β dom vol β§ (β‘πΊ β ((π¦ β π)(,)+β)) β dom vol) β ((β‘πΉ β (π(,)+β)) β© (β‘πΊ β ((π¦ β π)(,)+β))) β dom
vol) |
94 | 89, 92, 93 | syl2anc 585 |
. . . . . 6
β’ (π β ((β‘πΉ β (π(,)+β)) β© (β‘πΊ β ((π¦ β π)(,)+β))) β dom
vol) |
95 | 94 | ad2antrr 725 |
. . . . 5
β’ (((π β§ π¦ β β) β§ π β β) β ((β‘πΉ β (π(,)+β)) β© (β‘πΊ β ((π¦ β π)(,)+β))) β dom
vol) |
96 | 95 | ralrimiva 3144 |
. . . 4
β’ ((π β§ π¦ β β) β βπ β β ((β‘πΉ β (π(,)+β)) β© (β‘πΊ β ((π¦ β π)(,)+β))) β dom
vol) |
97 | | iunmbl2 24937 |
. . . 4
β’ ((β
βΌ β β§ βπ β β ((β‘πΉ β (π(,)+β)) β© (β‘πΊ β ((π¦ β π)(,)+β))) β dom vol) β
βͺ π β β ((β‘πΉ β (π(,)+β)) β© (β‘πΊ β ((π¦ β π)(,)+β))) β dom
vol) |
98 | 87, 96, 97 | sylancr 588 |
. . 3
β’ ((π β§ π¦ β β) β βͺ π β β ((β‘πΉ β (π(,)+β)) β© (β‘πΊ β ((π¦ β π)(,)+β))) β dom
vol) |
99 | 84, 98 | eqeltrrd 2839 |
. 2
β’ ((π β§ π¦ β β) β (β‘(πΉ βf + πΊ) β (π¦(,)+β)) β dom
vol) |
100 | 11, 99 | ismbf3d 25034 |
1
β’ (π β (πΉ βf + πΊ) β MblFn) |