Theorem pjnorm

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

	Ref	Expression
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)$$
2	1	fveq1d	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right)$$
3	2	fveq2d	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right)\right)$$
4	3	breq1d	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\to \left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)\le {norm}_{ℎ}\left(A\right)\leftrightarrow {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right)\right)\le {norm}_{ℎ}\left(A\right)\right)$$
5		2fveq3	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right)\right)={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)\right)$$
6		fveq2	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to {norm}_{ℎ}\left(A\right)={norm}_{ℎ}\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)$$
7	5 6	breq12d	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to \left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right)\right)\le {norm}_{ℎ}\left(A\right)\leftrightarrow {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)\right)\le {norm}_{ℎ}\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)\right)$$
8		ifchhv	$$⊢if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
9		ifhvhv0	$$⊢if\left(A\in \mathscr{H},A,0_{ℎ}\right)\in \mathscr{H}$$
10	8 9	pjnormi	$$⊢{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)\right)\le {norm}_{ℎ}\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)$$
11	4 7 10	dedth2h	$$⊢\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)$$