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	syl5req	|- ( A e. H -> ( ( ( projh ` H ) ` A ) +h 0h ) = A )
11	5 10	syl5eqr	|- ( 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 )