Metamath Proof Explorer


Theorem pjoccl

Description: The part of a vector that belongs to the orthocomplemented space. (Contributed by NM, 11-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion pjoccl ( ( 𝐻C𝐴 ∈ ℋ ) → ( 𝐴 ( ( proj𝐻 ) ‘ 𝐴 ) ) ∈ ( ⊥ ‘ 𝐻 ) )

Proof

Step Hyp Ref Expression
1 pjop ( ( 𝐻C𝐴 ∈ ℋ ) → ( ( proj ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) = ( 𝐴 ( ( proj𝐻 ) ‘ 𝐴 ) ) )
2 choccl ( 𝐻C → ( ⊥ ‘ 𝐻 ) ∈ C )
3 axpjcl ( ( ( ⊥ ‘ 𝐻 ) ∈ C𝐴 ∈ ℋ ) → ( ( proj ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐻 ) )
4 2 3 sylan ( ( 𝐻C𝐴 ∈ ℋ ) → ( ( proj ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐻 ) )
5 1 4 eqeltrrd ( ( 𝐻C𝐴 ∈ ℋ ) → ( 𝐴 ( ( proj𝐻 ) ‘ 𝐴 ) ) ∈ ( ⊥ ‘ 𝐻 ) )