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

Metamath Proof Explorer

Theorem pjid

Description: The projection of a vector in the projection subspace is itself. (Contributed by NM, 9-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion pjid ⊢ H ∈ C ℋ ∧ A ∈ H → proj ℎ ⁡ H ⁡ A = A

Proof

Step Hyp Ref Expression
1 simpl ⊢ H ∈ C ℋ ∧ A ∈ H → H ∈ C ℋ
2 chel ⊢ H ∈ C ℋ ∧ A ∈ H → A ∈ ℋ
3 1 2 jca ⊢ H ∈ C ℋ ∧ A ∈ H → H ∈ C ℋ ∧ A ∈ ℋ
4 pjch ⊢ H ∈ C ℋ ∧ A ∈ ℋ → A ∈ H ↔ proj ℎ ⁡ H ⁡ A = A
5 4 biimpa ⊢ H ∈ C ℋ ∧ A ∈ ℋ ∧ A ∈ H → proj ℎ ⁡ H ⁡ A = A
6 3 5 sylancom ⊢ H ∈ C ℋ ∧ A ∈ H → proj ℎ ⁡ H ⁡ A = A