Theorem pjdifnormii

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

	Ref	Expression
Hypotheses	pjidm.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
	pjidm.2	$$⊢A\in \mathscr{H}$$
	pjsslem.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	pjdifnormii	$$⊢0\le \left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right){\cdot }_{\mathrm{ih}}A\leftrightarrow {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		pjidm.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjidm.2	$$⊢A\in \mathscr{H}$$
3		pjsslem.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
4	3 2	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\in \mathscr{H}$$
5	4	normcli	$$⊢{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)\in ℝ$$
6	5	resqcli	$$⊢{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)}^2\in ℝ$$
7	1 2	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathscr{H}$$
8	7	normcli	$$⊢{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)\in ℝ$$
9	8	resqcli	$$⊢{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2\in ℝ$$
10	6 9	subge0i	$$⊢0\le {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)}^2-{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2\leftrightarrow {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2\le {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)}^2$$
11		his2sub	$$⊢\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\in \mathscr{H}\wedge {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathscr{H}\wedge A\in \mathscr{H}\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(A\right){\cdot }_{\mathrm{ih}}A\right)-\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}A\right)$$
12	4 7 2 11	mp3an	$$⊢\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(A\right){\cdot }_{\mathrm{ih}}A\right)-\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}A\right)$$
13	3 2	pjinormii	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right){\cdot }_{\mathrm{ih}}A={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)}^2$$
14	1 2	pjinormii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}A={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2$$
15	13 14	oveq12i	$$⊢\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right){\cdot }_{\mathrm{ih}}A\right)-\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}A\right)={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)}^2-{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2$$
16	12 15	eqtri	$$⊢\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(G\right)\left(A\right)\right)}^2-{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2$$
17	16	breq2i	$$⊢0\le \left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right){\cdot }_{\mathrm{ih}}A\leftrightarrow 0\le {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)}^2-{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2$$
18		normge0	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathscr{H}\to 0\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)$$
19	7 18	ax-mp	$$⊢0\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)$$
20		normge0	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\in \mathscr{H}\to 0\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)$$
21	4 20	ax-mp	$$⊢0\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)$$
22	8 5	le2sqi	$$⊢\left(0\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)\wedge 0\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)\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)\leftrightarrow {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2\le {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)}^2\right)$$
23	19 21 22	mp2an	$$⊢{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)\leftrightarrow {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2\le {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)}^2$$
24	10 17 23	3bitr4i	$$⊢0\le \left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right){\cdot }_{\mathrm{ih}}A\leftrightarrow {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)$$