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

Metamath Proof Explorer

Theorem pjoc2i

Description: Projection of a vector in the orthocomplement of the projection subspace. Lemma 4.4(iii) of Beran p. 111. (Contributed by NM, 27-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses pjoc2.1 ⊢ H ∈ C ℋ
pjoc2.2 ⊢ A ∈ ℋ
Assertion pjoc2i ⊢ A ∈ ⊥ ⁡ H ↔ proj ℎ ⁡ H ⁡ A = 0 ℎ

Proof

Step Hyp Ref Expression
1 pjoc2.1 ⊢ H ∈ C ℋ
2 pjoc2.2 ⊢ A ∈ ℋ
3 1 choccli ⊢ ⊥ ⁡ H ∈ C ℋ
4 3 2 pjoc1i ⊢ A ∈ ⊥ ⁡ H ↔ proj ℎ ⁡ ⊥ ⁡ ⊥ ⁡ H ⁡ A = 0 ℎ
5 1 pjococi ⊢ ⊥ ⁡ ⊥ ⁡ H = H
6 5 fveq2i ⊢ proj ℎ ⁡ ⊥ ⁡ ⊥ ⁡ H = proj ℎ ⁡ H
7 6 fveq1i ⊢ proj ℎ ⁡ ⊥ ⁡ ⊥ ⁡ H ⁡ A = proj ℎ ⁡ H ⁡ A
8 7 eqeq1i ⊢ proj ℎ ⁡ ⊥ ⁡ ⊥ ⁡ H ⁡ A = 0 ℎ ↔ proj ℎ ⁡ H ⁡ A = 0 ℎ
9 4 8 bitri ⊢ A ∈ ⊥ ⁡ H ↔ proj ℎ ⁡ H ⁡ A = 0 ℎ