Description: A projection maps onto its subspace. (Contributed by NM, 24-Apr-2006) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypothesis | pjfn.1 | |- H e. CH |
|
Assertion | pjfoi | |- ( projh ` H ) : ~H -onto-> H |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pjfn.1 | |- H e. CH |
|
2 | 1 | pjfni | |- ( projh ` H ) Fn ~H |
3 | 1 | pjrni | |- ran ( projh ` H ) = H |
4 | df-fo | |- ( ( projh ` H ) : ~H -onto-> H <-> ( ( projh ` H ) Fn ~H /\ ran ( projh ` H ) = H ) ) |
|
5 | 2 3 4 | mpbir2an | |- ( projh ` H ) : ~H -onto-> H |