Step | Hyp | Ref
| Expression |
1 | | unieq 4877 |
. . . . 5
β’ (π = β
β βͺ π =
βͺ β
) |
2 | 1 | ineq2d 4173 |
. . . 4
β’ (π = β
β (πΈ β© βͺ π) =
(πΈ β© βͺ β
)) |
3 | 2 | fveq2d 6847 |
. . 3
β’ (π = β
β (πβ(πΈ β© βͺ π)) = (πβ(πΈ β© βͺ
β
))) |
4 | | esumeq1 32690 |
. . 3
β’ (π = β
β
Ξ£*π¦ β
π(πβ(πΈ β© π¦)) = Ξ£*π¦ β β
(πβ(πΈ β© π¦))) |
5 | 3, 4 | eqeq12d 2749 |
. 2
β’ (π = β
β ((πβ(πΈ β© βͺ π)) = Ξ£*π¦ β π(πβ(πΈ β© π¦)) β (πβ(πΈ β© βͺ
β
)) = Ξ£*π¦ β β
(πβ(πΈ β© π¦)))) |
6 | | unieq 4877 |
. . . . 5
β’ (π = π β βͺ π = βͺ
π) |
7 | 6 | ineq2d 4173 |
. . . 4
β’ (π = π β (πΈ β© βͺ π) = (πΈ β© βͺ π)) |
8 | 7 | fveq2d 6847 |
. . 3
β’ (π = π β (πβ(πΈ β© βͺ π)) = (πβ(πΈ β© βͺ π))) |
9 | | esumeq1 32690 |
. . 3
β’ (π = π β Ξ£*π¦ β π(πβ(πΈ β© π¦)) = Ξ£*π¦ β π(πβ(πΈ β© π¦))) |
10 | 8, 9 | eqeq12d 2749 |
. 2
β’ (π = π β ((πβ(πΈ β© βͺ π)) = Ξ£*π¦ β π(πβ(πΈ β© π¦)) β (πβ(πΈ β© βͺ π)) = Ξ£*π¦ β π(πβ(πΈ β© π¦)))) |
11 | | unieq 4877 |
. . . . 5
β’ (π = (π βͺ {π₯}) β βͺ π = βͺ
(π βͺ {π₯})) |
12 | 11 | ineq2d 4173 |
. . . 4
β’ (π = (π βͺ {π₯}) β (πΈ β© βͺ π) = (πΈ β© βͺ (π βͺ {π₯}))) |
13 | 12 | fveq2d 6847 |
. . 3
β’ (π = (π βͺ {π₯}) β (πβ(πΈ β© βͺ π)) = (πβ(πΈ β© βͺ (π βͺ {π₯})))) |
14 | | esumeq1 32690 |
. . 3
β’ (π = (π βͺ {π₯}) β Ξ£*π¦ β π(πβ(πΈ β© π¦)) = Ξ£*π¦ β (π βͺ {π₯})(πβ(πΈ β© π¦))) |
15 | 13, 14 | eqeq12d 2749 |
. 2
β’ (π = (π βͺ {π₯}) β ((πβ(πΈ β© βͺ π)) = Ξ£*π¦ β π(πβ(πΈ β© π¦)) β (πβ(πΈ β© βͺ (π βͺ {π₯}))) = Ξ£*π¦ β (π βͺ {π₯})(πβ(πΈ β© π¦)))) |
16 | | unieq 4877 |
. . . . 5
β’ (π = π΄ β βͺ π = βͺ
π΄) |
17 | 16 | ineq2d 4173 |
. . . 4
β’ (π = π΄ β (πΈ β© βͺ π) = (πΈ β© βͺ π΄)) |
18 | 17 | fveq2d 6847 |
. . 3
β’ (π = π΄ β (πβ(πΈ β© βͺ π)) = (πβ(πΈ β© βͺ π΄))) |
19 | | esumeq1 32690 |
. . 3
β’ (π = π΄ β Ξ£*π¦ β π(πβ(πΈ β© π¦)) = Ξ£*π¦ β π΄(πβ(πΈ β© π¦))) |
20 | 18, 19 | eqeq12d 2749 |
. 2
β’ (π = π΄ β ((πβ(πΈ β© βͺ π)) = Ξ£*π¦ β π(πβ(πΈ β© π¦)) β (πβ(πΈ β© βͺ π΄)) = Ξ£*π¦ β π΄(πβ(πΈ β© π¦)))) |
21 | | carsgsiga.1 |
. . 3
β’ (π β (πββ
) = 0) |
22 | | uni0 4897 |
. . . . . 6
β’ βͺ β
= β
|
23 | 22 | ineq2i 4170 |
. . . . 5
β’ (πΈ β© βͺ β
) = (πΈ β© β
) |
24 | | in0 4352 |
. . . . 5
β’ (πΈ β© β
) =
β
|
25 | 23, 24 | eqtri 2761 |
. . . 4
β’ (πΈ β© βͺ β
) = β
|
26 | 25 | fveq2i 6846 |
. . 3
β’ (πβ(πΈ β© βͺ
β
)) = (πββ
) |
27 | | esumnul 32704 |
. . 3
β’
Ξ£*π¦
β β
(πβ(πΈ β© π¦)) = 0 |
28 | 21, 26, 27 | 3eqtr4g 2798 |
. 2
β’ (π β (πβ(πΈ β© βͺ
β
)) = Ξ£*π¦ β β
(πβ(πΈ β© π¦))) |
29 | | simpr 486 |
. . . . . 6
β’ (((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β§ (πβ(πΈ β© βͺ π)) = Ξ£*π¦ β π(πβ(πΈ β© π¦))) β (πβ(πΈ β© βͺ π)) = Ξ£*π¦ β π(πβ(πΈ β© π¦))) |
30 | 29 | eqcomd 2739 |
. . . . 5
β’ (((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β§ (πβ(πΈ β© βͺ π)) = Ξ£*π¦ β π(πβ(πΈ β© π¦))) β Ξ£*π¦ β π(πβ(πΈ β© π¦)) = (πβ(πΈ β© βͺ π))) |
31 | | simpr 486 |
. . . . . . . . 9
β’ (((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β§ π¦ = π₯) β π¦ = π₯) |
32 | 31 | ineq2d 4173 |
. . . . . . . 8
β’ (((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β§ π¦ = π₯) β (πΈ β© π¦) = (πΈ β© π₯)) |
33 | 32 | fveq2d 6847 |
. . . . . . 7
β’ (((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β§ π¦ = π₯) β (πβ(πΈ β© π¦)) = (πβ(πΈ β© π₯))) |
34 | | simprr 772 |
. . . . . . 7
β’ ((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β π₯ β (π΄ β π)) |
35 | | carsgval.2 |
. . . . . . . . 9
β’ (π β π:π« πβΆ(0[,]+β)) |
36 | 35 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β π:π« πβΆ(0[,]+β)) |
37 | | carsgclctunlem1.2 |
. . . . . . . . . 10
β’ (π β πΈ β π« π) |
38 | 37 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β πΈ β π« π) |
39 | 38 | elpwincl1 31496 |
. . . . . . . 8
β’ ((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β (πΈ β© π₯) β π« π) |
40 | 36, 39 | ffvelcdmd 7037 |
. . . . . . 7
β’ ((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β (πβ(πΈ β© π₯)) β (0[,]+β)) |
41 | 33, 34, 40 | esumsn 32721 |
. . . . . 6
β’ ((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β Ξ£*π¦ β {π₯} (πβ(πΈ β© π¦)) = (πβ(πΈ β© π₯))) |
42 | 41 | adantr 482 |
. . . . 5
β’ (((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β§ (πβ(πΈ β© βͺ π)) = Ξ£*π¦ β π(πβ(πΈ β© π¦))) β Ξ£*π¦ β {π₯} (πβ(πΈ β© π¦)) = (πβ(πΈ β© π₯))) |
43 | 30, 42 | oveq12d 7376 |
. . . 4
β’ (((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β§ (πβ(πΈ β© βͺ π)) = Ξ£*π¦ β π(πβ(πΈ β© π¦))) β (Ξ£*π¦ β π(πβ(πΈ β© π¦)) +π
Ξ£*π¦ β
{π₯} (πβ(πΈ β© π¦))) = ((πβ(πΈ β© βͺ π)) +π (πβ(πΈ β© π₯)))) |
44 | | nfv 1918 |
. . . . . 6
β’
β²π¦(π β§ (π β π΄ β§ π₯ β (π΄ β π))) |
45 | | nfcv 2904 |
. . . . . 6
β’
β²π¦π |
46 | | nfcv 2904 |
. . . . . 6
β’
β²π¦{π₯} |
47 | | vex 3448 |
. . . . . . 7
β’ π β V |
48 | 47 | a1i 11 |
. . . . . 6
β’ ((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β π β V) |
49 | | vsnex 5387 |
. . . . . . 7
β’ {π₯} β V |
50 | 49 | a1i 11 |
. . . . . 6
β’ ((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β {π₯} β V) |
51 | 34 | eldifbd 3924 |
. . . . . . 7
β’ ((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β Β¬ π₯ β π) |
52 | | disjsn 4673 |
. . . . . . 7
β’ ((π β© {π₯}) = β
β Β¬ π₯ β π) |
53 | 51, 52 | sylibr 233 |
. . . . . 6
β’ ((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β (π β© {π₯}) = β
) |
54 | 35 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β§ π¦ β π) β π:π« πβΆ(0[,]+β)) |
55 | 37 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β§ π¦ β π) β πΈ β π« π) |
56 | 55 | elpwincl1 31496 |
. . . . . . 7
β’ (((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β§ π¦ β π) β (πΈ β© π¦) β π« π) |
57 | 54, 56 | ffvelcdmd 7037 |
. . . . . 6
β’ (((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β§ π¦ β π) β (πβ(πΈ β© π¦)) β (0[,]+β)) |
58 | 35 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β§ π¦ β {π₯}) β π:π« πβΆ(0[,]+β)) |
59 | 37 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β§ π¦ β {π₯}) β πΈ β π« π) |
60 | 59 | elpwincl1 31496 |
. . . . . . 7
β’ (((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β§ π¦ β {π₯}) β (πΈ β© π¦) β π« π) |
61 | 58, 60 | ffvelcdmd 7037 |
. . . . . 6
β’ (((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β§ π¦ β {π₯}) β (πβ(πΈ β© π¦)) β (0[,]+β)) |
62 | 44, 45, 46, 48, 50, 53, 57, 61 | esumsplit 32709 |
. . . . 5
β’ ((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β Ξ£*π¦ β (π βͺ {π₯})(πβ(πΈ β© π¦)) = (Ξ£*π¦ β π(πβ(πΈ β© π¦)) +π
Ξ£*π¦ β
{π₯} (πβ(πΈ β© π¦)))) |
63 | 62 | adantr 482 |
. . . 4
β’ (((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β§ (πβ(πΈ β© βͺ π)) = Ξ£*π¦ β π(πβ(πΈ β© π¦))) β Ξ£*π¦ β (π βͺ {π₯})(πβ(πΈ β© π¦)) = (Ξ£*π¦ β π(πβ(πΈ β© π¦)) +π
Ξ£*π¦ β
{π₯} (πβ(πΈ β© π¦)))) |
64 | | uniun 4892 |
. . . . . . . 8
β’ βͺ (π
βͺ {π₯}) = (βͺ π
βͺ βͺ {π₯}) |
65 | | unisnv 4889 |
. . . . . . . . 9
β’ βͺ {π₯}
= π₯ |
66 | 65 | uneq2i 4121 |
. . . . . . . 8
β’ (βͺ π
βͺ βͺ {π₯}) = (βͺ π βͺ π₯) |
67 | 64, 66 | eqtri 2761 |
. . . . . . 7
β’ βͺ (π
βͺ {π₯}) = (βͺ π
βͺ π₯) |
68 | 67 | ineq2i 4170 |
. . . . . 6
β’ (πΈ β© βͺ (π
βͺ {π₯})) = (πΈ β© (βͺ π
βͺ π₯)) |
69 | 68 | fveq2i 6846 |
. . . . 5
β’ (πβ(πΈ β© βͺ (π βͺ {π₯}))) = (πβ(πΈ β© (βͺ π βͺ π₯))) |
70 | | inass 4180 |
. . . . . . . . . 10
β’ ((πΈ β© (βͺ π
βͺ π₯)) β© βͺ π) =
(πΈ β© ((βͺ π
βͺ π₯) β© βͺ π)) |
71 | | indir 4236 |
. . . . . . . . . . . 12
β’ ((βͺ π
βͺ π₯) β© βͺ π) =
((βͺ π β© βͺ π) βͺ (π₯ β© βͺ π)) |
72 | | inidm 4179 |
. . . . . . . . . . . . . . 15
β’ (βͺ π
β© βͺ π) = βͺ π |
73 | 72 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β (βͺ
π β© βͺ π) =
βͺ π) |
74 | | incom 4162 |
. . . . . . . . . . . . . . 15
β’ (βͺ π
β© π₯) = (π₯ β© βͺ π) |
75 | | carsgclctunlem1.1 |
. . . . . . . . . . . . . . . . 17
β’ (π β Disj π¦ β π΄ π¦) |
76 | 75 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β Disj π¦ β π΄ π¦) |
77 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β π΄) β π β π΄) |
78 | 77 | adantrr 716 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β π β π΄) |
79 | 76, 78, 34 | disjuniel 31561 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β (βͺ
π β© π₯) = β
) |
80 | 74, 79 | eqtr3id 2787 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β (π₯ β© βͺ π) = β
) |
81 | 73, 80 | uneq12d 4125 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β ((βͺ
π β© βͺ π)
βͺ (π₯ β© βͺ π))
= (βͺ π βͺ β
)) |
82 | | un0 4351 |
. . . . . . . . . . . . 13
β’ (βͺ π
βͺ β
) = βͺ π |
83 | 81, 82 | eqtrdi 2789 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β ((βͺ
π β© βͺ π)
βͺ (π₯ β© βͺ π))
= βͺ π) |
84 | 71, 83 | eqtrid 2785 |
. . . . . . . . . . 11
β’ ((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β ((βͺ
π βͺ π₯) β© βͺ π) = βͺ
π) |
85 | 84 | ineq2d 4173 |
. . . . . . . . . 10
β’ ((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β (πΈ β© ((βͺ π βͺ π₯) β© βͺ π)) = (πΈ β© βͺ π)) |
86 | 70, 85 | eqtrid 2785 |
. . . . . . . . 9
β’ ((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β ((πΈ β© (βͺ π βͺ π₯)) β© βͺ π) = (πΈ β© βͺ π)) |
87 | 86 | fveq2d 6847 |
. . . . . . . 8
β’ ((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β (πβ((πΈ β© (βͺ π βͺ π₯)) β© βͺ π)) = (πβ(πΈ β© βͺ π))) |
88 | | indif2 4231 |
. . . . . . . . . 10
β’ (πΈ β© ((βͺ π
βͺ π₯) β βͺ π))
= ((πΈ β© (βͺ π
βͺ π₯)) β βͺ π) |
89 | | uncom 4114 |
. . . . . . . . . . . . . 14
β’ (βͺ π
βͺ π₯) = (π₯ βͺ βͺ π) |
90 | 89 | difeq1i 4079 |
. . . . . . . . . . . . 13
β’ ((βͺ π
βͺ π₯) β βͺ π) =
((π₯ βͺ βͺ π)
β βͺ π) |
91 | | difun2 4441 |
. . . . . . . . . . . . . 14
β’ ((π₯ βͺ βͺ π)
β βͺ π) = (π₯ β βͺ π) |
92 | | disj3 4414 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β© βͺ π) =
β
β π₯ = (π₯ β βͺ π)) |
93 | 92 | biimpi 215 |
. . . . . . . . . . . . . 14
β’ ((π₯ β© βͺ π) =
β
β π₯ = (π₯ β βͺ π)) |
94 | 91, 93 | eqtr4id 2792 |
. . . . . . . . . . . . 13
β’ ((π₯ β© βͺ π) =
β
β ((π₯ βͺ
βͺ π) β βͺ π) = π₯) |
95 | 90, 94 | eqtrid 2785 |
. . . . . . . . . . . 12
β’ ((π₯ β© βͺ π) =
β
β ((βͺ π βͺ π₯) β βͺ π) = π₯) |
96 | 80, 95 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β ((βͺ
π βͺ π₯) β βͺ π) = π₯) |
97 | 96 | ineq2d 4173 |
. . . . . . . . . 10
β’ ((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β (πΈ β© ((βͺ π βͺ π₯) β βͺ π)) = (πΈ β© π₯)) |
98 | 88, 97 | eqtr3id 2787 |
. . . . . . . . 9
β’ ((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β ((πΈ β© (βͺ π βͺ π₯)) β βͺ π) = (πΈ β© π₯)) |
99 | 98 | fveq2d 6847 |
. . . . . . . 8
β’ ((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β (πβ((πΈ β© (βͺ π βͺ π₯)) β βͺ π)) = (πβ(πΈ β© π₯))) |
100 | 87, 99 | oveq12d 7376 |
. . . . . . 7
β’ ((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β ((πβ((πΈ β© (βͺ π βͺ π₯)) β© βͺ π)) +π (πβ((πΈ β© (βͺ π βͺ π₯)) β βͺ π))) = ((πβ(πΈ β© βͺ π)) +π (πβ(πΈ β© π₯)))) |
101 | | carsgval.1 |
. . . . . . . . . . . . 13
β’ (π β π β π) |
102 | 101 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΄) β π β π) |
103 | 35 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΄) β π:π« πβΆ(0[,]+β)) |
104 | 21 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΄) β (πββ
) = 0) |
105 | | carsgsiga.2 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ βΌ Ο β§ π₯ β π« π) β (πββͺ π₯) β€ Ξ£*π¦ β π₯(πβπ¦)) |
106 | 105 | 3adant1r 1178 |
. . . . . . . . . . . 12
β’ (((π β§ π β π΄) β§ π₯ βΌ Ο β§ π₯ β π« π) β (πββͺ π₯) β€ Ξ£*π¦ β π₯(πβπ¦)) |
107 | | fiunelcarsg.1 |
. . . . . . . . . . . . 13
β’ (π β π΄ β Fin) |
108 | | ssfi 9120 |
. . . . . . . . . . . . 13
β’ ((π΄ β Fin β§ π β π΄) β π β Fin) |
109 | 107, 108 | sylan 581 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΄) β π β Fin) |
110 | | fiunelcarsg.2 |
. . . . . . . . . . . . . 14
β’ (π β π΄ β (toCaraSigaβπ)) |
111 | 110 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΄) β π΄ β (toCaraSigaβπ)) |
112 | 77, 111 | sstrd 3955 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΄) β π β (toCaraSigaβπ)) |
113 | 102, 103,
104, 106, 109, 112 | fiunelcarsg 32973 |
. . . . . . . . . . 11
β’ ((π β§ π β π΄) β βͺ π β (toCaraSigaβπ)) |
114 | 101, 35 | elcarsg 32962 |
. . . . . . . . . . . 12
β’ (π β (βͺ π
β (toCaraSigaβπ)
β (βͺ π β π β§ βπ β π« π((πβ(π β© βͺ π)) +π (πβ(π β βͺ π))) = (πβπ)))) |
115 | 114 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β π΄) β (βͺ π β (toCaraSigaβπ) β (βͺ π
β π β§
βπ β π«
π((πβ(π β© βͺ π)) +π (πβ(π β βͺ π))) = (πβπ)))) |
116 | 113, 115 | mpbid 231 |
. . . . . . . . . 10
β’ ((π β§ π β π΄) β (βͺ π β π β§ βπ β π« π((πβ(π β© βͺ π)) +π (πβ(π β βͺ π))) = (πβπ))) |
117 | 116 | simprd 497 |
. . . . . . . . 9
β’ ((π β§ π β π΄) β βπ β π« π((πβ(π β© βͺ π)) +π (πβ(π β βͺ π))) = (πβπ)) |
118 | 117 | adantrr 716 |
. . . . . . . 8
β’ ((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β βπ β π« π((πβ(π β© βͺ π)) +π (πβ(π β βͺ π))) = (πβπ)) |
119 | 38 | elpwincl1 31496 |
. . . . . . . . 9
β’ ((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β (πΈ β© (βͺ π βͺ π₯)) β π« π) |
120 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β§ π = (πΈ β© (βͺ π βͺ π₯))) β π = (πΈ β© (βͺ π βͺ π₯))) |
121 | 120 | ineq1d 4172 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β§ π = (πΈ β© (βͺ π βͺ π₯))) β (π β© βͺ π) = ((πΈ β© (βͺ π βͺ π₯)) β© βͺ π)) |
122 | 121 | fveq2d 6847 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β§ π = (πΈ β© (βͺ π βͺ π₯))) β (πβ(π β© βͺ π)) = (πβ((πΈ β© (βͺ π βͺ π₯)) β© βͺ π))) |
123 | 120 | difeq1d 4082 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β§ π = (πΈ β© (βͺ π βͺ π₯))) β (π β βͺ π) = ((πΈ β© (βͺ π βͺ π₯)) β βͺ π)) |
124 | 123 | fveq2d 6847 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β§ π = (πΈ β© (βͺ π βͺ π₯))) β (πβ(π β βͺ π)) = (πβ((πΈ β© (βͺ π βͺ π₯)) β βͺ π))) |
125 | 122, 124 | oveq12d 7376 |
. . . . . . . . . 10
β’ (((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β§ π = (πΈ β© (βͺ π βͺ π₯))) β ((πβ(π β© βͺ π)) +π (πβ(π β βͺ π))) = ((πβ((πΈ β© (βͺ π βͺ π₯)) β© βͺ π)) +π (πβ((πΈ β© (βͺ π βͺ π₯)) β βͺ π)))) |
126 | 120 | fveq2d 6847 |
. . . . . . . . . 10
β’ (((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β§ π = (πΈ β© (βͺ π βͺ π₯))) β (πβπ) = (πβ(πΈ β© (βͺ π βͺ π₯)))) |
127 | 125, 126 | eqeq12d 2749 |
. . . . . . . . 9
β’ (((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β§ π = (πΈ β© (βͺ π βͺ π₯))) β (((πβ(π β© βͺ π)) +π (πβ(π β βͺ π))) = (πβπ) β ((πβ((πΈ β© (βͺ π βͺ π₯)) β© βͺ π)) +π (πβ((πΈ β© (βͺ π βͺ π₯)) β βͺ π))) = (πβ(πΈ β© (βͺ π βͺ π₯))))) |
128 | 119, 127 | rspcdv 3572 |
. . . . . . . 8
β’ ((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β (βπ β π« π((πβ(π β© βͺ π)) +π (πβ(π β βͺ π))) = (πβπ) β ((πβ((πΈ β© (βͺ π βͺ π₯)) β© βͺ π)) +π (πβ((πΈ β© (βͺ π βͺ π₯)) β βͺ π))) = (πβ(πΈ β© (βͺ π βͺ π₯))))) |
129 | 118, 128 | mpd 15 |
. . . . . . 7
β’ ((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β ((πβ((πΈ β© (βͺ π βͺ π₯)) β© βͺ π)) +π (πβ((πΈ β© (βͺ π βͺ π₯)) β βͺ π))) = (πβ(πΈ β© (βͺ π βͺ π₯)))) |
130 | 100, 129 | eqtr3d 2775 |
. . . . . 6
β’ ((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β ((πβ(πΈ β© βͺ π)) +π (πβ(πΈ β© π₯))) = (πβ(πΈ β© (βͺ π βͺ π₯)))) |
131 | 130 | adantr 482 |
. . . . 5
β’ (((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β§ (πβ(πΈ β© βͺ π)) = Ξ£*π¦ β π(πβ(πΈ β© π¦))) β ((πβ(πΈ β© βͺ π)) +π (πβ(πΈ β© π₯))) = (πβ(πΈ β© (βͺ π βͺ π₯)))) |
132 | 69, 131 | eqtr4id 2792 |
. . . 4
β’ (((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β§ (πβ(πΈ β© βͺ π)) = Ξ£*π¦ β π(πβ(πΈ β© π¦))) β (πβ(πΈ β© βͺ (π βͺ {π₯}))) = ((πβ(πΈ β© βͺ π)) +π (πβ(πΈ β© π₯)))) |
133 | 43, 63, 132 | 3eqtr4rd 2784 |
. . 3
β’ (((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β§ (πβ(πΈ β© βͺ π)) = Ξ£*π¦ β π(πβ(πΈ β© π¦))) β (πβ(πΈ β© βͺ (π βͺ {π₯}))) = Ξ£*π¦ β (π βͺ {π₯})(πβ(πΈ β© π¦))) |
134 | 133 | ex 414 |
. 2
β’ ((π β§ (π β π΄ β§ π₯ β (π΄ β π))) β ((πβ(πΈ β© βͺ π)) = Ξ£*π¦ β π(πβ(πΈ β© π¦)) β (πβ(πΈ β© βͺ (π βͺ {π₯}))) = Ξ£*π¦ β (π βͺ {π₯})(πβ(πΈ β© π¦)))) |
135 | 5, 10, 15, 20, 28, 134, 107 | findcard2d 9113 |
1
β’ (π β (πβ(πΈ β© βͺ π΄)) = Ξ£*π¦ β π΄(πβ(πΈ β© π¦))) |