# Metamath Proof Explorer

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