Theorem pjssge0ii

Description: Theorem 4.5(iv)->(v) 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	pjssge0ii	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(G\cap \perp \left(H\right)\right)\left(A\right)\to 0\le \left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right){\cdot }_{\mathrm{ih}}A$$

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	1	choccli	$$⊢\perp \left(H\right)\in {\mathbf{C}}_{\mathscr{H}}$$
5	3 4	chincli	$$⊢G\cap \perp \left(H\right)\in {\mathbf{C}}_{\mathscr{H}}$$
6	5 2	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(G\cap \perp \left(H\right)\right)\left(A\right)\in \mathscr{H}$$
7	6	normcli	$$⊢{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\cap \perp \left(H\right)\right)\left(A\right)\right)\in ℝ$$
8	7	sqge0i	$$⊢0\le {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\cap \perp \left(H\right)\right)\left(A\right)\right)}^2$$
9		oveq1	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(G\cap \perp \left(H\right)\right)\left(A\right)\to \left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right){\cdot }_{\mathrm{ih}}A={\mathrm{proj}}_{ℎ}\left(G\cap \perp \left(H\right)\right)\left(A\right){\cdot }_{\mathrm{ih}}A$$
10	5 2	pjinormii	$$⊢{\mathrm{proj}}_{ℎ}\left(G\cap \perp \left(H\right)\right)\left(A\right){\cdot }_{\mathrm{ih}}A={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\cap \perp \left(H\right)\right)\left(A\right)\right)}^2$$
11	9 10	eqtrdi	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(G\cap \perp \left(H\right)\right)\left(A\right)\to \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\cap \perp \left(H\right)\right)\left(A\right)\right)}^2$$
12	8 11	breqtrrid	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(G\cap \perp \left(H\right)\right)\left(A\right)\to 0\le \left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right){\cdot }_{\mathrm{ih}}A$$