Metamath Proof Explorer


Theorem pjopi

Description: Orthocomplement projection in terms of projection. (Contributed by NM, 31-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses pjop.1 𝐻C
pjop.2 𝐴 ∈ ℋ
Assertion pjopi ( ( proj ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) = ( 𝐴 ( ( proj𝐻 ) ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 pjop.1 𝐻C
2 pjop.2 𝐴 ∈ ℋ
3 pjop ( ( 𝐻C𝐴 ∈ ℋ ) → ( ( proj ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) = ( 𝐴 ( ( proj𝐻 ) ‘ 𝐴 ) ) )
4 1 2 3 mp2an ( ( proj ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) = ( 𝐴 ( ( proj𝐻 ) ‘ 𝐴 ) )