Metamath Proof Explorer

Theorem pjs14i

Description: Theorem S-14 of Watanabe, p. 486. (Contributed by NM, 26-Sep-2001) (New usage is discouraged.)

Ref Expression
Hypotheses pjs14.1 ${⊢}{G}\in {\mathbf{C}}_{ℋ}$
pjs14.2 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
Assertion pjs14i ${⊢}{A}\in ℋ\to {norm}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right)\left({A}\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right)\right)$

Proof

Step Hyp Ref Expression
1 pjs14.1 ${⊢}{G}\in {\mathbf{C}}_{ℋ}$
2 pjs14.2 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
3 2 1 pjcoi ${⊢}{A}\in ℋ\to \left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right)\left({A}\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right)\right)$
4 3 fveq2d ${⊢}{A}\in ℋ\to {norm}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right)\left({A}\right)\right)={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right)\right)\right)$
5 1 pjhcli ${⊢}{A}\in ℋ\to {\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right)\in ℋ$
6 pjnorm ${⊢}\left({H}\in {\mathbf{C}}_{ℋ}\wedge {\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right)\in ℋ\right)\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right)\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right)\right)$
7 2 5 6 sylancr ${⊢}{A}\in ℋ\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right)\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right)\right)$
8 4 7 eqbrtrd ${⊢}{A}\in ℋ\to {norm}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right)\left({A}\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({A}\right)\right)$