Theorem pjoci

Description: Projection of orthocomplement. First part of Theorem 27.3 of Halmos p. 45. (Contributed by NM, 26-Nov-2000) (New usage is discouraged.)

	Ref	Expression
Hypothesis	pjidmco.1	⊢ 𝐻 ∈ Cℋ
Assertion	pjoci	⊢ ( ( projℎ ‘ ℋ ) −op ( projℎ ‘ 𝐻 ) ) = ( projℎ ‘ ( ⊥ ‘ 𝐻 ) )

Proof

Step	Hyp	Ref	Expression
1		pjidmco.1	⊢ 𝐻 ∈ Cℋ
2	1	pjtoi	⊢ ( ( projℎ ‘ 𝐻 ) +op ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ) = ( projℎ ‘ ℋ )
3		helch	⊢ ℋ ∈ Cℋ
4	3	pjfi	⊢ ( projℎ ‘ ℋ ) : ℋ ⟶ ℋ
5	1	pjfi	⊢ ( projℎ ‘ 𝐻 ) : ℋ ⟶ ℋ
6	1	choccli	⊢ ( ⊥ ‘ 𝐻 ) ∈ Cℋ
7	6	pjfi	⊢ ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) : ℋ ⟶ ℋ
8	4 5 7	hodsi	⊢ ( ( ( projℎ ‘ ℋ ) −op ( projℎ ‘ 𝐻 ) ) = ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ↔ ( ( projℎ ‘ 𝐻 ) +op ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ) = ( projℎ ‘ ℋ ) )
9	2 8	mpbir	⊢ ( ( projℎ ‘ ℋ ) −op ( projℎ ‘ 𝐻 ) ) = ( projℎ ‘ ( ⊥ ‘ 𝐻 ) )