# Metamath Proof Explorer

## Theorem pjdifnormi

Description: Theorem 4.5(v)<->(vi) of Beran p. 112. (Contributed by NM, 26-Sep-2001) (New usage is discouraged.)

Ref Expression
Hypotheses pjco.1 ${⊢}{G}\in {\mathbf{C}}_{ℋ}$
pjco.2 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
Assertion pjdifnormi ${⊢}{A}\in ℋ\to \left(0\le \left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right){\cdot }_{\mathrm{ih}}{A}↔{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 pjco.1 ${⊢}{G}\in {\mathbf{C}}_{ℋ}$
2 pjco.2 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
3 fveq2 ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)$
4 fveq2 ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)$
5 3 4 oveq12d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)$
6 id ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)$
7 5 6 oveq12d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to \left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right){\cdot }_{\mathrm{ih}}{A}=\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)\right){\cdot }_{\mathrm{ih}}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)$
8 7 breq2d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to \left(0\le \left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right){\cdot }_{\mathrm{ih}}{A}↔0\le \left({\mathrm{proj}}_{ℎ}\left({G}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)\right){\cdot }_{\mathrm{ih}}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)$
9 2fveq3 ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)\right)$
10 2fveq3 ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right)\right)={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)\right)$
11 9 10 breq12d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to \left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right)\right)↔{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)\right)\right)$
12 8 11 bibi12d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to \left(\left(0\le \left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right){\cdot }_{\mathrm{ih}}{A}↔{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right)\right)\right)↔\left(0\le \left({\mathrm{proj}}_{ℎ}\left({G}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)\right){\cdot }_{\mathrm{ih}}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)↔{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)\right)\right)\right)$
13 ifhvhv0 ${⊢}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\in ℋ$
14 2 13 1 pjdifnormii ${⊢}0\le \left({\mathrm{proj}}_{ℎ}\left({G}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)\right){\cdot }_{\mathrm{ih}}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)↔{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)\right)$
15 12 14 dedth ${⊢}{A}\in ℋ\to \left(0\le \left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right){\cdot }_{\mathrm{ih}}{A}↔{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right)\right)\right)$