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}}_{\mathscr{H}}$$
	pjs14.2	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	pjs14i	$$⊢A\in \mathscr{H}\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}}_{\mathscr{H}}$$
2		pjs14.2	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
3	2 1	pjcoi	$$⊢A\in \mathscr{H}\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 \mathscr{H}\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 \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\in \mathscr{H}$$
6		pjnorm	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge {\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\in \mathscr{H}\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 \mathscr{H}\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 \mathscr{H}\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)$$