Metamath Proof Explorer

Theorem pjhcl

Description: Closure of a projection in Hilbert space. (Contributed by NM, 30-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion pjhcl 
|- ( ( H e. CH /\ A e. ~H ) -> ( ( projh ` H ) ` A ) e. ~H )

Proof

Step Hyp Ref Expression
1 chss 
 |-  ( H e. CH -> H C_ ~H )
2 1 adantr 
 |-  ( ( H e. CH /\ A e. ~H ) -> H C_ ~H )
3 axpjcl 
 |-  ( ( H e. CH /\ A e. ~H ) -> ( ( projh ` H ) ` A ) e. H )
4 2 3 sseldd 
 |-  ( ( H e. CH /\ A e. ~H ) -> ( ( projh ` H ) ` A ) e. ~H )