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 e. CH
pjop.2 
|- A e. ~H
Assertion pjchi 
|- ( A e. H <-> ( ( projh ` H ) ` A ) = A )

Proof

Step Hyp Ref Expression
1 pjop.1 
 |-  H e. CH
2 pjop.2 
 |-  A e. ~H
3 1 2 pjhclii 
 |-  ( ( projh ` H ) ` A ) e. ~H
4 ax-hvaddid 
 |-  ( ( ( projh ` H ) ` A ) e. ~H -> ( ( ( projh ` H ) ` A ) +h 0h ) = ( ( projh ` H ) ` A ) )
5 3 4 ax-mp 
 |-  ( ( ( projh ` H ) ` A ) +h 0h ) = ( ( projh ` H ) ` A )
6 1 2 pjpji 
 |-  A = ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) )
7 1 2 pjoc1i 
 |-  ( A e. H <-> ( ( projh ` ( _|_ ` H ) ) ` A ) = 0h )
8 7 biimpi 
 |-  ( A e. H -> ( ( projh ` ( _|_ ` H ) ) ` A ) = 0h )
9 8 oveq2d 
 |-  ( A e. H -> ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) = ( ( ( projh ` H ) ` A ) +h 0h ) )
10 6 9 eqtr2id 
 |-  ( A e. H -> ( ( ( projh ` H ) ` A ) +h 0h ) = A )
11 5 10 eqtr3id 
 |-  ( A e. H -> ( ( projh ` H ) ` A ) = A )
12 1 2 pjclii 
 |-  ( ( projh ` H ) ` A ) e. H
13 eleq1 
 |-  ( ( ( projh ` H ) ` A ) = A -> ( ( ( projh ` H ) ` A ) e. H <-> A e. H ) )
14 12 13 mpbii 
 |-  ( ( ( projh ` H ) ` A ) = A -> A e. H )
15 11 14 impbii 
 |-  ( A e. H <-> ( ( projh ` H ) ` A ) = A )