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

Metamath Proof Explorer

Theorem pjchi

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

Ref Expression
Hypotheses pjop.1 ⊢ H ∈ C ℋ
pjop.2 ⊢ A ∈ ℋ
Assertion pjchi ⊢ A ∈ H ↔ proj ℎ ⁡ H ⁡ A = A

Proof

Step Hyp Ref Expression
1 pjop.1 ⊢ H ∈ C ℋ
2 pjop.2 ⊢ A ∈ ℋ
3 1 2 pjhclii ⊢ proj ℎ ⁡ H ⁡ A ∈ ℋ
4 ax-hvaddid ⊢ proj ℎ ⁡ H ⁡ A ∈ ℋ → proj ℎ ⁡ H ⁡ A + ℎ 0 ℎ = proj ℎ ⁡ H ⁡ A
5 3 4 ax-mp ⊢ proj ℎ ⁡ H ⁡ A + ℎ 0 ℎ = proj ℎ ⁡ H ⁡ A
6 1 2 pjpji ⊢ A = proj ℎ ⁡ H ⁡ A + ℎ proj ℎ ⁡ ⊥ ⁡ H ⁡ A
7 1 2 pjoc1i ⊢ A ∈ H ↔ proj ℎ ⁡ ⊥ ⁡ H ⁡ A = 0 ℎ
8 7 biimpi ⊢ A ∈ H → proj ℎ ⁡ ⊥ ⁡ H ⁡ A = 0 ℎ
9 8 oveq2d ⊢ A ∈ H → proj ℎ ⁡ H ⁡ A + ℎ proj ℎ ⁡ ⊥ ⁡ H ⁡ A = proj ℎ ⁡ H ⁡ A + ℎ 0 ℎ
10 6 9 eqtr2id ⊢ A ∈ H → proj ℎ ⁡ H ⁡ A + ℎ 0 ℎ = A
11 5 10 eqtr3id ⊢ A ∈ H → proj ℎ ⁡ H ⁡ A = A
12 1 2 pjclii ⊢ proj ℎ ⁡ H ⁡ A ∈ H
13 eleq1 ⊢ proj ℎ ⁡ H ⁡ A = A → proj ℎ ⁡ H ⁡ A ∈ H ↔ A ∈ H
14 12 13 mpbii ⊢ proj ℎ ⁡ H ⁡ A = A → A ∈ H
15 11 14 impbii ⊢ A ∈ H ↔ proj ℎ ⁡ H ⁡ A = A