Step | Hyp | Ref
| Expression |
1 | | caragenel.s |
. . . 4
β’ π = (CaraGenβπ) |
2 | | caragenel.o |
. . . . 5
β’ (π β π β OutMeas) |
3 | | caragenval 44808 |
. . . . 5
β’ (π β OutMeas β
(CaraGenβπ) = {π β π« βͺ dom π β£ βπ β π« βͺ dom π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ)}) |
4 | 2, 3 | syl 17 |
. . . 4
β’ (π β (CaraGenβπ) = {π β π« βͺ dom π β£ βπ β π« βͺ dom π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ)}) |
5 | 1, 4 | eqtrid 2789 |
. . 3
β’ (π β π = {π β π« βͺ dom π β£ βπ β π« βͺ dom π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ)}) |
6 | 5 | eleq2d 2824 |
. 2
β’ (π β (πΈ β π β πΈ β {π β π« βͺ dom π β£ βπ β π« βͺ dom π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ)})) |
7 | | ineq2 4171 |
. . . . . . . 8
β’ (π = πΈ β (π β© π) = (π β© πΈ)) |
8 | 7 | fveq2d 6851 |
. . . . . . 7
β’ (π = πΈ β (πβ(π β© π)) = (πβ(π β© πΈ))) |
9 | | difeq2 4081 |
. . . . . . . 8
β’ (π = πΈ β (π β π) = (π β πΈ)) |
10 | 9 | fveq2d 6851 |
. . . . . . 7
β’ (π = πΈ β (πβ(π β π)) = (πβ(π β πΈ))) |
11 | 8, 10 | oveq12d 7380 |
. . . . . 6
β’ (π = πΈ β ((πβ(π β© π)) +π (πβ(π β π))) = ((πβ(π β© πΈ)) +π (πβ(π β πΈ)))) |
12 | 11 | eqeq1d 2739 |
. . . . 5
β’ (π = πΈ β (((πβ(π β© π)) +π (πβ(π β π))) = (πβπ) β ((πβ(π β© πΈ)) +π (πβ(π β πΈ))) = (πβπ))) |
13 | 12 | ralbidv 3175 |
. . . 4
β’ (π = πΈ β (βπ β π« βͺ dom π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ) β βπ β π« βͺ dom π((πβ(π β© πΈ)) +π (πβ(π β πΈ))) = (πβπ))) |
14 | 13 | elrab 3650 |
. . 3
β’ (πΈ β {π β π« βͺ dom π β£ βπ β π« βͺ dom π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ)} β (πΈ β π« βͺ dom π β§ βπ β π« βͺ dom π((πβ(π β© πΈ)) +π (πβ(π β πΈ))) = (πβπ))) |
15 | 14 | a1i 11 |
. 2
β’ (π β (πΈ β {π β π« βͺ dom π β£ βπ β π« βͺ dom π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ)} β (πΈ β π« βͺ dom π β§ βπ β π« βͺ dom π((πβ(π β© πΈ)) +π (πβ(π β πΈ))) = (πβπ)))) |
16 | 6, 15 | bitrd 279 |
1
β’ (π β (πΈ β π β (πΈ β π« βͺ dom π β§ βπ β π« βͺ dom π((πβ(π β© πΈ)) +π (πβ(π β πΈ))) = (πβπ)))) |