Step | Hyp | Ref
| Expression |
1 | | caragenuncllem.o |
. . . . . 6
β’ (π β π β OutMeas) |
2 | | caragenuncllem.s |
. . . . . 6
β’ π = (CaraGenβπ) |
3 | | caragenuncllem.x |
. . . . . 6
β’ π = βͺ
dom π |
4 | | caragenuncllem.e |
. . . . . 6
β’ (π β πΈ β π) |
5 | | caragenuncllem.a |
. . . . . . 7
β’ (π β π΄ β π) |
6 | 5 | ssinss1d 43330 |
. . . . . 6
β’ (π β (π΄ β© (πΈ βͺ πΉ)) β π) |
7 | 1, 2, 3, 4, 6 | caragensplit 44815 |
. . . . 5
β’ (π β ((πβ((π΄ β© (πΈ βͺ πΉ)) β© πΈ)) +π (πβ((π΄ β© (πΈ βͺ πΉ)) β πΈ))) = (πβ(π΄ β© (πΈ βͺ πΉ)))) |
8 | 7 | eqcomd 2743 |
. . . 4
β’ (π β (πβ(π΄ β© (πΈ βͺ πΉ))) = ((πβ((π΄ β© (πΈ βͺ πΉ)) β© πΈ)) +π (πβ((π΄ β© (πΈ βͺ πΉ)) β πΈ)))) |
9 | | inass 4184 |
. . . . . . . 8
β’ ((π΄ β© (πΈ βͺ πΉ)) β© πΈ) = (π΄ β© ((πΈ βͺ πΉ) β© πΈ)) |
10 | | incom 4166 |
. . . . . . . . . 10
β’ ((πΈ βͺ πΉ) β© πΈ) = (πΈ β© (πΈ βͺ πΉ)) |
11 | | inabs 4220 |
. . . . . . . . . 10
β’ (πΈ β© (πΈ βͺ πΉ)) = πΈ |
12 | 10, 11 | eqtri 2765 |
. . . . . . . . 9
β’ ((πΈ βͺ πΉ) β© πΈ) = πΈ |
13 | 12 | ineq2i 4174 |
. . . . . . . 8
β’ (π΄ β© ((πΈ βͺ πΉ) β© πΈ)) = (π΄ β© πΈ) |
14 | 9, 13 | eqtri 2765 |
. . . . . . 7
β’ ((π΄ β© (πΈ βͺ πΉ)) β© πΈ) = (π΄ β© πΈ) |
15 | 14 | fveq2i 6850 |
. . . . . 6
β’ (πβ((π΄ β© (πΈ βͺ πΉ)) β© πΈ)) = (πβ(π΄ β© πΈ)) |
16 | | incom 4166 |
. . . . . . . . . 10
β’ ((π΄ β πΈ) β© πΉ) = (πΉ β© (π΄ β πΈ)) |
17 | | indifcom 4237 |
. . . . . . . . . 10
β’ (πΉ β© (π΄ β πΈ)) = (π΄ β© (πΉ β πΈ)) |
18 | 16, 17 | eqtr2i 2766 |
. . . . . . . . 9
β’ (π΄ β© (πΉ β πΈ)) = ((π΄ β πΈ) β© πΉ) |
19 | 18 | eqcomi 2746 |
. . . . . . . 8
β’ ((π΄ β πΈ) β© πΉ) = (π΄ β© (πΉ β πΈ)) |
20 | | difundir 4245 |
. . . . . . . . . 10
β’ ((πΈ βͺ πΉ) β πΈ) = ((πΈ β πΈ) βͺ (πΉ β πΈ)) |
21 | | difid 4335 |
. . . . . . . . . . 11
β’ (πΈ β πΈ) = β
|
22 | 21 | uneq1i 4124 |
. . . . . . . . . 10
β’ ((πΈ β πΈ) βͺ (πΉ β πΈ)) = (β
βͺ (πΉ β πΈ)) |
23 | | 0un 4357 |
. . . . . . . . . 10
β’ (β
βͺ (πΉ β πΈ)) = (πΉ β πΈ) |
24 | 20, 22, 23 | 3eqtrri 2770 |
. . . . . . . . 9
β’ (πΉ β πΈ) = ((πΈ βͺ πΉ) β πΈ) |
25 | 24 | ineq2i 4174 |
. . . . . . . 8
β’ (π΄ β© (πΉ β πΈ)) = (π΄ β© ((πΈ βͺ πΉ) β πΈ)) |
26 | | indif2 4235 |
. . . . . . . 8
β’ (π΄ β© ((πΈ βͺ πΉ) β πΈ)) = ((π΄ β© (πΈ βͺ πΉ)) β πΈ) |
27 | 19, 25, 26 | 3eqtrri 2770 |
. . . . . . 7
β’ ((π΄ β© (πΈ βͺ πΉ)) β πΈ) = ((π΄ β πΈ) β© πΉ) |
28 | 27 | fveq2i 6850 |
. . . . . 6
β’ (πβ((π΄ β© (πΈ βͺ πΉ)) β πΈ)) = (πβ((π΄ β πΈ) β© πΉ)) |
29 | 15, 28 | oveq12i 7374 |
. . . . 5
β’ ((πβ((π΄ β© (πΈ βͺ πΉ)) β© πΈ)) +π (πβ((π΄ β© (πΈ βͺ πΉ)) β πΈ))) = ((πβ(π΄ β© πΈ)) +π (πβ((π΄ β πΈ) β© πΉ))) |
30 | 29 | a1i 11 |
. . . 4
β’ (π β ((πβ((π΄ β© (πΈ βͺ πΉ)) β© πΈ)) +π (πβ((π΄ β© (πΈ βͺ πΉ)) β πΈ))) = ((πβ(π΄ β© πΈ)) +π (πβ((π΄ β πΈ) β© πΉ)))) |
31 | | eqidd 2738 |
. . . 4
β’ (π β ((πβ(π΄ β© πΈ)) +π (πβ((π΄ β πΈ) β© πΉ))) = ((πβ(π΄ β© πΈ)) +π (πβ((π΄ β πΈ) β© πΉ)))) |
32 | 8, 30, 31 | 3eqtrd 2781 |
. . 3
β’ (π β (πβ(π΄ β© (πΈ βͺ πΉ))) = ((πβ(π΄ β© πΈ)) +π (πβ((π΄ β πΈ) β© πΉ)))) |
33 | | difun1 4254 |
. . . . 5
β’ (π΄ β (πΈ βͺ πΉ)) = ((π΄ β πΈ) β πΉ) |
34 | 33 | fveq2i 6850 |
. . . 4
β’ (πβ(π΄ β (πΈ βͺ πΉ))) = (πβ((π΄ β πΈ) β πΉ)) |
35 | 34 | a1i 11 |
. . 3
β’ (π β (πβ(π΄ β (πΈ βͺ πΉ))) = (πβ((π΄ β πΈ) β πΉ))) |
36 | 32, 35 | oveq12d 7380 |
. 2
β’ (π β ((πβ(π΄ β© (πΈ βͺ πΉ))) +π (πβ(π΄ β (πΈ βͺ πΉ)))) = (((πβ(π΄ β© πΈ)) +π (πβ((π΄ β πΈ) β© πΉ))) +π (πβ((π΄ β πΈ) β πΉ)))) |
37 | 5 | ssinss1d 43330 |
. . . . 5
β’ (π β (π΄ β© πΈ) β π) |
38 | 1, 3, 37 | omexrcl 44822 |
. . . 4
β’ (π β (πβ(π΄ β© πΈ)) β
β*) |
39 | 1, 3, 37 | omecl 44818 |
. . . . 5
β’ (π β (πβ(π΄ β© πΈ)) β (0[,]+β)) |
40 | 39 | xrge0nemnfd 43640 |
. . . 4
β’ (π β (πβ(π΄ β© πΈ)) β -β) |
41 | 38, 40 | jca 513 |
. . 3
β’ (π β ((πβ(π΄ β© πΈ)) β β* β§ (πβ(π΄ β© πΈ)) β -β)) |
42 | | caragenuncllem.f |
. . . . . . 7
β’ (π β πΉ β π) |
43 | 1, 2, 42, 3 | caragenelss 44816 |
. . . . . 6
β’ (π β πΉ β π) |
44 | 43 | ssinss2d 43342 |
. . . . 5
β’ (π β ((π΄ β πΈ) β© πΉ) β π) |
45 | 1, 3, 44 | omexrcl 44822 |
. . . 4
β’ (π β (πβ((π΄ β πΈ) β© πΉ)) β
β*) |
46 | 1, 3, 44 | omecl 44818 |
. . . . 5
β’ (π β (πβ((π΄ β πΈ) β© πΉ)) β (0[,]+β)) |
47 | 46 | xrge0nemnfd 43640 |
. . . 4
β’ (π β (πβ((π΄ β πΈ) β© πΉ)) β -β) |
48 | 45, 47 | jca 513 |
. . 3
β’ (π β ((πβ((π΄ β πΈ) β© πΉ)) β β* β§ (πβ((π΄ β πΈ) β© πΉ)) β -β)) |
49 | 5 | ssdifssd 4107 |
. . . . . 6
β’ (π β (π΄ β πΈ) β π) |
50 | 49 | ssdifssd 4107 |
. . . . 5
β’ (π β ((π΄ β πΈ) β πΉ) β π) |
51 | 1, 3, 50 | omexrcl 44822 |
. . . 4
β’ (π β (πβ((π΄ β πΈ) β πΉ)) β
β*) |
52 | 1, 3, 50 | omecl 44818 |
. . . . 5
β’ (π β (πβ((π΄ β πΈ) β πΉ)) β (0[,]+β)) |
53 | 52 | xrge0nemnfd 43640 |
. . . 4
β’ (π β (πβ((π΄ β πΈ) β πΉ)) β -β) |
54 | 51, 53 | jca 513 |
. . 3
β’ (π β ((πβ((π΄ β πΈ) β πΉ)) β β* β§ (πβ((π΄ β πΈ) β πΉ)) β -β)) |
55 | | xaddass 13175 |
. . 3
β’ ((((πβ(π΄ β© πΈ)) β β* β§ (πβ(π΄ β© πΈ)) β -β) β§ ((πβ((π΄ β πΈ) β© πΉ)) β β* β§ (πβ((π΄ β πΈ) β© πΉ)) β -β) β§ ((πβ((π΄ β πΈ) β πΉ)) β β* β§ (πβ((π΄ β πΈ) β πΉ)) β -β)) β (((πβ(π΄ β© πΈ)) +π (πβ((π΄ β πΈ) β© πΉ))) +π (πβ((π΄ β πΈ) β πΉ))) = ((πβ(π΄ β© πΈ)) +π ((πβ((π΄ β πΈ) β© πΉ)) +π (πβ((π΄ β πΈ) β πΉ))))) |
56 | 41, 48, 54, 55 | syl3anc 1372 |
. 2
β’ (π β (((πβ(π΄ β© πΈ)) +π (πβ((π΄ β πΈ) β© πΉ))) +π (πβ((π΄ β πΈ) β πΉ))) = ((πβ(π΄ β© πΈ)) +π ((πβ((π΄ β πΈ) β© πΉ)) +π (πβ((π΄ β πΈ) β πΉ))))) |
57 | 1, 2, 3, 42, 49 | caragensplit 44815 |
. . . 4
β’ (π β ((πβ((π΄ β πΈ) β© πΉ)) +π (πβ((π΄ β πΈ) β πΉ))) = (πβ(π΄ β πΈ))) |
58 | 57 | oveq2d 7378 |
. . 3
β’ (π β ((πβ(π΄ β© πΈ)) +π ((πβ((π΄ β πΈ) β© πΉ)) +π (πβ((π΄ β πΈ) β πΉ)))) = ((πβ(π΄ β© πΈ)) +π (πβ(π΄ β πΈ)))) |
59 | 1, 2, 3, 4, 5 | caragensplit 44815 |
. . 3
β’ (π β ((πβ(π΄ β© πΈ)) +π (πβ(π΄ β πΈ))) = (πβπ΄)) |
60 | 58, 59 | eqtrd 2777 |
. 2
β’ (π β ((πβ(π΄ β© πΈ)) +π ((πβ((π΄ β πΈ) β© πΉ)) +π (πβ((π΄ β πΈ) β πΉ)))) = (πβπ΄)) |
61 | 36, 56, 60 | 3eqtrd 2781 |
1
β’ (π β ((πβ(π΄ β© (πΈ βͺ πΉ))) +π (πβ(π΄ β (πΈ βͺ πΉ)))) = (πβπ΄)) |