Metamath Proof Explorer

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 ⊢H∈Cℋ∧A∈ℋ→A∈H↔normℎ⁡projℎ⁡H⁡A=normℎ⁡A

Proof

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