Theorem pjoc2i

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

	Ref	Expression
Hypotheses	pjoc2.1	⊢ 𝐻 ∈ Cℋ
	pjoc2.2	⊢ 𝐴 ∈ ℋ
Assertion	pjoc2i	⊢ ( 𝐴 ∈ ( ⊥ ‘ 𝐻 ) ↔ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) = 0ℎ )

Proof

Step	Hyp	Ref	Expression
1		pjoc2.1	⊢ 𝐻 ∈ Cℋ
2		pjoc2.2	⊢ 𝐴 ∈ ℋ
3	1	choccli	⊢ ( ⊥ ‘ 𝐻 ) ∈ Cℋ
4	3 2	pjoc1i	⊢ ( 𝐴 ∈ ( ⊥ ‘ 𝐻 ) ↔ ( ( projℎ ‘ ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) = 0ℎ )
5	1	pjococi	⊢ ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) = 𝐻
6	5	fveq2i	⊢ ( projℎ ‘ ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) ) = ( projℎ ‘ 𝐻 )
7	6	fveq1i	⊢ ( ( projℎ ‘ ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) = ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 )
8	7	eqeq1i	⊢ ( ( ( projℎ ‘ ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) ) ‘ 𝐴 ) = 0ℎ ↔ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) = 0ℎ )
9	4 8	bitri	⊢ ( 𝐴 ∈ ( ⊥ ‘ 𝐻 ) ↔ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) = 0ℎ )