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 ⊢ 𝐻 ∈ Cℋ
pjop.2 ⊢ 𝐴 ∈ ℋ
Assertion pjchi ( 𝐴 ∈ 𝐻 ↔ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) = 𝐴 )

Proof

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