Theorem pjnorm2

Description: A vector belongs to the subspace of a projection iff the norm of its projection equals its norm. This and pjch yield Theorem 26.3 of Halmos p. 44. (Contributed by NM, 7-Apr-2001) (New usage is discouraged.)

	Ref	Expression
Assertion	pjnorm2	⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( 𝐴 ∈ 𝐻 ↔ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) = ( normℎ ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pjhcl	⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ ℋ )
2		normcl	⊢ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ ℋ → ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ∈ ℝ )
3	1 2	syl	⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ∈ ℝ )
4		normcl	⊢ ( 𝐴 ∈ ℋ → ( normℎ ‘ 𝐴 ) ∈ ℝ )
5	4	adantl	⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( normℎ ‘ 𝐴 ) ∈ ℝ )
6	3 5	eqleltd	⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) = ( normℎ ‘ 𝐴 ) ↔ ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ≤ ( normℎ ‘ 𝐴 ) ∧ ¬ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) < ( normℎ ‘ 𝐴 ) ) ) )
7		pjnorm	⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ≤ ( normℎ ‘ 𝐴 ) )
8	7	biantrurd	⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( ¬ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) < ( normℎ ‘ 𝐴 ) ↔ ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ≤ ( normℎ ‘ 𝐴 ) ∧ ¬ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) < ( normℎ ‘ 𝐴 ) ) ) )
9		pjnel	⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( ¬ 𝐴 ∈ 𝐻 ↔ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) < ( normℎ ‘ 𝐴 ) ) )
10	9	con1bid	⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( ¬ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) < ( normℎ ‘ 𝐴 ) ↔ 𝐴 ∈ 𝐻 ) )
11	6 8 10	3bitr2rd	⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( 𝐴 ∈ 𝐻 ↔ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) = ( normℎ ‘ 𝐴 ) ) )