Theorem pjnormi

Description: The norm of the projection is less than or equal to the norm. (Contributed by NM, 27-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjnorm.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
	pjnorm.2	$$⊢A\in \mathscr{H}$$
Assertion	pjnormi	$$⊢{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)\le {norm}_{ℎ}\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		pjnorm.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjnorm.2	$$⊢A\in \mathscr{H}$$
3	1 2	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathscr{H}$$
4	1	choccli	$$⊢\perp \left(H\right)\in {\mathbf{C}}_{\mathscr{H}}$$
5	4 2	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\in \mathscr{H}$$
6	3 5	pm3.2i	$$⊢\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathscr{H}\wedge {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\in \mathscr{H}\right)$$
7	2 2	pjorthi	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)=0$$
8	1 7	ax-mp	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)=0$$
9		normpyc	$$⊢\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathscr{H}\wedge {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\in \mathscr{H}\right)\to \left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)=0\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right)\right)$$
10	6 8 9	mp2	$$⊢{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right)$$
11	1 2	pjpji	$$⊢A={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)$$
12	11	fveq2i	$$⊢{norm}_{ℎ}\left(A\right)={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right)$$
13	10 12	breqtrri	$$⊢{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)\le {norm}_{ℎ}\left(A\right)$$