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𝐻 ) ‘ 𝐴 ) = 𝐴 )