This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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