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	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to \left(A\in H\leftrightarrow {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)={norm}_{ℎ}\left(A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		pjhcl	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathscr{H}$$
2		normcl	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathscr{H}\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)\in ℝ$$
3	1 2	syl	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)\in ℝ$$
4		normcl	$$⊢A\in \mathscr{H}\to {norm}_{ℎ}\left(A\right)\in ℝ$$
5	4	adantl	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to {norm}_{ℎ}\left(A\right)\in ℝ$$
6	3 5	eqleltd	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to \left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)={norm}_{ℎ}\left(A\right)\leftrightarrow \left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)\le {norm}_{ℎ}\left(A\right)\wedge \neg {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)<{norm}_{ℎ}\left(A\right)\right)\right)$$
7		pjnorm	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)\le {norm}_{ℎ}\left(A\right)$$
8	7	biantrurd	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to \left(\neg {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)<{norm}_{ℎ}\left(A\right)\leftrightarrow \left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)\le {norm}_{ℎ}\left(A\right)\wedge \neg {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)<{norm}_{ℎ}\left(A\right)\right)\right)$$
9		pjnel	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to \left(\neg A\in H\leftrightarrow {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)<{norm}_{ℎ}\left(A\right)\right)$$
10	9	con1bid	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to \left(\neg {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)<{norm}_{ℎ}\left(A\right)\leftrightarrow A\in H\right)$$
11	6 8 10	3bitr2rd	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to \left(A\in H\leftrightarrow {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)={norm}_{ℎ}\left(A\right)\right)$$