Description: Definition of projection operator in Hughes p. 47, except that we do not need linearity to be explicit by virtue of hmoplin . (Contributed by NM, 24-Apr-2006) (Revised by Mario Carneiro, 19-May-2014) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | dfpjop | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pjmfn | |
|
2 | fvelrnb | |
|
3 | 1 2 | ax-mp | |
4 | pjhmop | |
|
5 | pjidmco | |
|
6 | 4 5 | jca | |
7 | eleq1 | |
|
8 | id | |
|
9 | 8 8 | coeq12d | |
10 | 9 8 | eqeq12d | |
11 | 7 10 | anbi12d | |
12 | 6 11 | syl5ibcom | |
13 | 12 | rexlimiv | |
14 | 3 13 | sylbi | |
15 | hmopidmpj | |
|
16 | hmopidmch | |
|
17 | fnfvelrn | |
|
18 | 1 16 17 | sylancr | |
19 | 15 18 | eqeltrd | |
20 | 14 19 | impbii | |