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

Metamath Proof Explorer

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 )