Step | Hyp | Ref
| Expression |
1 | | caragendifcl.o |
. 2
β’ (π β π β OutMeas) |
2 | | eqid 2737 |
. 2
β’ βͺ dom π = βͺ dom π |
3 | | caragendifcl.s |
. 2
β’ π = (CaraGenβπ) |
4 | 3 | caragenss 44819 |
. . . . . 6
β’ (π β OutMeas β π β dom π) |
5 | 1, 4 | syl 17 |
. . . . 5
β’ (π β π β dom π) |
6 | 5 | unissd 4880 |
. . . 4
β’ (π β βͺ π
β βͺ dom π) |
7 | 6 | ssdifssd 4107 |
. . 3
β’ (π β (βͺ π
β πΈ) β βͺ dom π) |
8 | 3 | fvexi 6861 |
. . . . . . 7
β’ π β V |
9 | 8 | uniex 7683 |
. . . . . 6
β’ βͺ π
β V |
10 | | difexg 5289 |
. . . . . 6
β’ (βͺ π
β V β (βͺ π β πΈ) β V) |
11 | 9, 10 | ax-mp 5 |
. . . . 5
β’ (βͺ π
β πΈ) β
V |
12 | 11 | a1i 11 |
. . . 4
β’ (π β (βͺ π
β πΈ) β
V) |
13 | | elpwg 4568 |
. . . 4
β’ ((βͺ π
β πΈ) β V β
((βͺ π β πΈ) β π« βͺ dom π β (βͺ π β πΈ) β βͺ dom
π)) |
14 | 12, 13 | syl 17 |
. . 3
β’ (π β ((βͺ π
β πΈ) β π«
βͺ dom π β (βͺ π β πΈ) β βͺ dom
π)) |
15 | 7, 14 | mpbird 257 |
. 2
β’ (π β (βͺ π
β πΈ) β π«
βͺ dom π) |
16 | | elpwi 4572 |
. . . . . . . . 9
β’ (π β π« βͺ dom π β π β βͺ dom
π) |
17 | 16 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β π« βͺ dom π) β π β βͺ dom
π) |
18 | 1, 3 | caragenuni 44826 |
. . . . . . . . . 10
β’ (π β βͺ π =
βͺ dom π) |
19 | 18 | eqcomd 2743 |
. . . . . . . . 9
β’ (π β βͺ dom π = βͺ π) |
20 | 19 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β π« βͺ dom π) β βͺ dom
π = βͺ π) |
21 | 17, 20 | sseqtrd 3989 |
. . . . . . 7
β’ ((π β§ π β π« βͺ dom π) β π β βͺ π) |
22 | | difin2 4256 |
. . . . . . 7
β’ (π β βͺ π
β (π β πΈ) = ((βͺ π
β πΈ) β© π)) |
23 | 21, 22 | syl 17 |
. . . . . 6
β’ ((π β§ π β π« βͺ dom π) β (π β πΈ) = ((βͺ π β πΈ) β© π)) |
24 | | incom 4166 |
. . . . . . 7
β’ ((βͺ π
β πΈ) β© π) = (π β© (βͺ π β πΈ)) |
25 | 24 | a1i 11 |
. . . . . 6
β’ ((π β§ π β π« βͺ dom π) β ((βͺ
π β πΈ) β© π) = (π β© (βͺ π β πΈ))) |
26 | 23, 25 | eqtr2d 2778 |
. . . . 5
β’ ((π β§ π β π« βͺ dom π) β (π β© (βͺ π β πΈ)) = (π β πΈ)) |
27 | 26 | fveq2d 6851 |
. . . 4
β’ ((π β§ π β π« βͺ dom π) β (πβ(π β© (βͺ π β πΈ))) = (πβ(π β πΈ))) |
28 | 21 | ssdifd 4105 |
. . . . . . . 8
β’ ((π β§ π β π« βͺ dom π) β (π β πΈ) β (βͺ
π β πΈ)) |
29 | | sscon 4103 |
. . . . . . . 8
β’ ((π β πΈ) β (βͺ
π β πΈ) β (π β (βͺ π β πΈ)) β (π β (π β πΈ))) |
30 | 28, 29 | syl 17 |
. . . . . . 7
β’ ((π β§ π β π« βͺ dom π) β (π β (βͺ π β πΈ)) β (π β (π β πΈ))) |
31 | | dfin4 4232 |
. . . . . . . . 9
β’ (π β© πΈ) = (π β (π β πΈ)) |
32 | 31 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π β π« βͺ dom π) β (π β© πΈ) = (π β (π β πΈ))) |
33 | | eqimss2 4006 |
. . . . . . . 8
β’ ((π β© πΈ) = (π β (π β πΈ)) β (π β (π β πΈ)) β (π β© πΈ)) |
34 | 32, 33 | syl 17 |
. . . . . . 7
β’ ((π β§ π β π« βͺ dom π) β (π β (π β πΈ)) β (π β© πΈ)) |
35 | 30, 34 | sstrd 3959 |
. . . . . 6
β’ ((π β§ π β π« βͺ dom π) β (π β (βͺ π β πΈ)) β (π β© πΈ)) |
36 | | elinel1 4160 |
. . . . . . . . 9
β’ (π₯ β (π β© πΈ) β π₯ β π) |
37 | | elinel2 4161 |
. . . . . . . . . 10
β’ (π₯ β (π β© πΈ) β π₯ β πΈ) |
38 | | elndif 4093 |
. . . . . . . . . 10
β’ (π₯ β πΈ β Β¬ π₯ β (βͺ π β πΈ)) |
39 | 37, 38 | syl 17 |
. . . . . . . . 9
β’ (π₯ β (π β© πΈ) β Β¬ π₯ β (βͺ π β πΈ)) |
40 | 36, 39 | eldifd 3926 |
. . . . . . . 8
β’ (π₯ β (π β© πΈ) β π₯ β (π β (βͺ π β πΈ))) |
41 | 40 | ssriv 3953 |
. . . . . . 7
β’ (π β© πΈ) β (π β (βͺ π β πΈ)) |
42 | 41 | a1i 11 |
. . . . . 6
β’ ((π β§ π β π« βͺ dom π) β (π β© πΈ) β (π β (βͺ π β πΈ))) |
43 | 35, 42 | eqssd 3966 |
. . . . 5
β’ ((π β§ π β π« βͺ dom π) β (π β (βͺ π β πΈ)) = (π β© πΈ)) |
44 | 43 | fveq2d 6851 |
. . . 4
β’ ((π β§ π β π« βͺ dom π) β (πβ(π β (βͺ π β πΈ))) = (πβ(π β© πΈ))) |
45 | 27, 44 | oveq12d 7380 |
. . 3
β’ ((π β§ π β π« βͺ dom π) β ((πβ(π β© (βͺ π β πΈ))) +π (πβ(π β (βͺ π β πΈ)))) = ((πβ(π β πΈ)) +π (πβ(π β© πΈ)))) |
46 | | iccssxr 13354 |
. . . . 5
β’
(0[,]+β) β β* |
47 | 1 | adantr 482 |
. . . . . 6
β’ ((π β§ π β π« βͺ dom π) β π β OutMeas) |
48 | 17 | ssdifssd 4107 |
. . . . . 6
β’ ((π β§ π β π« βͺ dom π) β (π β πΈ) β βͺ dom
π) |
49 | 47, 2, 48 | omecl 44818 |
. . . . 5
β’ ((π β§ π β π« βͺ dom π) β (πβ(π β πΈ)) β (0[,]+β)) |
50 | 46, 49 | sselid 3947 |
. . . 4
β’ ((π β§ π β π« βͺ dom π) β (πβ(π β πΈ)) β
β*) |
51 | | ssinss1 4202 |
. . . . . . . 8
β’ (π β βͺ dom π β (π β© πΈ) β βͺ dom
π) |
52 | 16, 51 | syl 17 |
. . . . . . 7
β’ (π β π« βͺ dom π β (π β© πΈ) β βͺ dom
π) |
53 | 52 | adantl 483 |
. . . . . 6
β’ ((π β§ π β π« βͺ dom π) β (π β© πΈ) β βͺ dom
π) |
54 | 47, 2, 53 | omecl 44818 |
. . . . 5
β’ ((π β§ π β π« βͺ dom π) β (πβ(π β© πΈ)) β (0[,]+β)) |
55 | 46, 54 | sselid 3947 |
. . . 4
β’ ((π β§ π β π« βͺ dom π) β (πβ(π β© πΈ)) β
β*) |
56 | 50, 55 | xaddcomd 43632 |
. . 3
β’ ((π β§ π β π« βͺ dom π) β ((πβ(π β πΈ)) +π (πβ(π β© πΈ))) = ((πβ(π β© πΈ)) +π (πβ(π β πΈ)))) |
57 | | caragendifcl.e |
. . . . . 6
β’ (π β πΈ β π) |
58 | 1, 3 | caragenel 44810 |
. . . . . 6
β’ (π β (πΈ β π β (πΈ β π« βͺ dom π β§ βπ β π« βͺ dom π((πβ(π β© πΈ)) +π (πβ(π β πΈ))) = (πβπ)))) |
59 | 57, 58 | mpbid 231 |
. . . . 5
β’ (π β (πΈ β π« βͺ dom π β§ βπ β π« βͺ dom π((πβ(π β© πΈ)) +π (πβ(π β πΈ))) = (πβπ))) |
60 | 59 | simprd 497 |
. . . 4
β’ (π β βπ β π« βͺ dom π((πβ(π β© πΈ)) +π (πβ(π β πΈ))) = (πβπ)) |
61 | 60 | r19.21bi 3237 |
. . 3
β’ ((π β§ π β π« βͺ dom π) β ((πβ(π β© πΈ)) +π (πβ(π β πΈ))) = (πβπ)) |
62 | 45, 56, 61 | 3eqtrd 2781 |
. 2
β’ ((π β§ π β π« βͺ dom π) β ((πβ(π β© (βͺ π β πΈ))) +π (πβ(π β (βͺ π β πΈ)))) = (πβπ)) |
63 | 1, 2, 3, 15, 62 | carageneld 44817 |
1
β’ (π β (βͺ π
β πΈ) β π) |