Theorem pjorthi

Description: Projection components on orthocomplemented subspaces are orthogonal. (Contributed by NM, 26-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjorth.1	⊢ 𝐴 ∈ ℋ
	pjorth.2	⊢ 𝐵 ∈ ℋ
Assertion	pjorthi	⊢ ( 𝐻 ∈ Cℋ → ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ·ih ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐵 ) ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		pjorth.1	⊢ 𝐴 ∈ ℋ
2		pjorth.2	⊢ 𝐵 ∈ ℋ
3		chsh	⊢ ( 𝐻 ∈ Cℋ → 𝐻 ∈ Sℋ )
4		axpjcl	⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ 𝐻 )
5	1 4	mpan2	⊢ ( 𝐻 ∈ Cℋ → ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ 𝐻 )
6		choccl	⊢ ( 𝐻 ∈ Cℋ → ( ⊥ ‘ 𝐻 ) ∈ Cℋ )
7		axpjcl	⊢ ( ( ( ⊥ ‘ 𝐻 ) ∈ Cℋ ∧ 𝐵 ∈ ℋ ) → ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐵 ) ∈ ( ⊥ ‘ 𝐻 ) )
8	6 2 7	sylancl	⊢ ( 𝐻 ∈ Cℋ → ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐵 ) ∈ ( ⊥ ‘ 𝐻 ) )
9	5 8	jca	⊢ ( 𝐻 ∈ Cℋ → ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ 𝐻 ∧ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐵 ) ∈ ( ⊥ ‘ 𝐻 ) ) )
10		shocorth	⊢ ( 𝐻 ∈ Sℋ → ( ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ 𝐻 ∧ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐵 ) ∈ ( ⊥ ‘ 𝐻 ) ) → ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ·ih ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐵 ) ) = 0 ) )
11	3 9 10	sylc	⊢ ( 𝐻 ∈ Cℋ → ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ·ih ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐵 ) ) = 0 )