Metamath Proof Explorer


Theorem pjhfo

Description: A projection maps onto its subspace. (Contributed by NM, 24-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion pjhfo H C proj H : onto H

Proof

Step Hyp Ref Expression
1 fveq2 H = if H C H 0 proj H = proj if H C H 0
2 foeq1 proj H = proj if H C H 0 proj H : onto H proj if H C H 0 : onto H
3 1 2 syl H = if H C H 0 proj H : onto H proj if H C H 0 : onto H
4 foeq3 H = if H C H 0 proj if H C H 0 : onto H proj if H C H 0 : onto if H C H 0
5 h0elch 0 C
6 5 elimel if H C H 0 C
7 6 pjfoi proj if H C H 0 : onto if H C H 0
8 3 4 7 dedth2v H C proj H : onto H