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	⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ 𝐻 ) → ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ 𝐻 ) → 𝐻 ∈ Cℋ )
2		chel	⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ 𝐻 ) → 𝐴 ∈ ℋ )
3	1 2	jca	⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ 𝐻 ) → ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) )
4		pjch	⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( 𝐴 ∈ 𝐻 ↔ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) = 𝐴 ) )
5	4	biimpa	⊢ ( ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) ∧ 𝐴 ∈ 𝐻 ) → ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) = 𝐴 )
6	3 5	sylancom	⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ 𝐻 ) → ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) = 𝐴 )