Description: The value of a projection in terms of components. (Contributed by NM, 28-Nov-2000) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | pjfn.1 | |- H e. CH |
|
| Assertion | pjvi | |- ( ( A e. H /\ B e. ( _|_ ` H ) ) -> ( ( projh ` H ) ` ( A +h B ) ) = A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pjfn.1 | |- H e. CH |
|
| 2 | 1 | pjcompi | |- ( ( A e. H /\ B e. ( _|_ ` H ) ) -> ( ( projh ` H ) ` ( A +h B ) ) = A ) |