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

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ℎ ‘ 𝐻 ) ‘ 𝐴 ) )