Theorem pjnormssi

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

	Ref	Expression
Hypotheses	pjco.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
	pjco.2	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	pjnormssi	$$⊢G\subseteq H\leftrightarrow \forall x\in \mathscr{H}{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		pjco.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjco.2	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
3	2 1	pjssmi	$$⊢x\in \mathscr{H}\to \left(G\subseteq H\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)={\mathrm{proj}}_{ℎ}\left(H\cap \perp \left(G\right)\right)\left(x\right)\right)$$
4	2 1	pjssge0i	$$⊢x\in \mathscr{H}\to \left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)={\mathrm{proj}}_{ℎ}\left(H\cap \perp \left(G\right)\right)\left(x\right)\to 0\le \left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right){\cdot }_{\mathrm{ih}}x\right)$$
5	3 4	syld	$$⊢x\in \mathscr{H}\to \left(G\subseteq H\to 0\le \left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right){\cdot }_{\mathrm{ih}}x\right)$$
6	2 1	pjdifnormi	$$⊢x\in \mathscr{H}\to \left(0\le \left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right){\cdot }_{\mathrm{ih}}x\leftrightarrow {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)\right)$$
7	5 6	sylibd	$$⊢x\in \mathscr{H}\to \left(G\subseteq H\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)\right)$$
8	7	com12	$$⊢G\subseteq H\to \left(x\in \mathscr{H}\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)\right)$$
9	8	ralrimiv	$$⊢G\subseteq H\to \forall x\in \mathscr{H}{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)$$
10	2	choccli	$$⊢\perp \left(H\right)\in {\mathbf{C}}_{\mathscr{H}}$$
11	10	cheli	$$⊢x\in \perp \left(H\right)\to x\in \mathscr{H}$$
12		breq2	$$⊢{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)=0\to \left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)\leftrightarrow {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\le 0\right)$$
13	12	biimpac	$$⊢\left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)\wedge {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)=0\right)\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\le 0$$
14	1	pjhcli	$$⊢x\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\in \mathscr{H}$$
15		normge0	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\in \mathscr{H}\to 0\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)$$
16	14 15	syl	$$⊢x\in \mathscr{H}\to 0\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)$$
17		normcl	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\in \mathscr{H}\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\in ℝ$$
18	14 17	syl	$$⊢x\in \mathscr{H}\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\in ℝ$$
19		0re	$$⊢0\in ℝ$$
20		letri3	$$⊢\left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\in ℝ\wedge 0\in ℝ\right)\to \left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)=0\leftrightarrow \left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\le 0\wedge 0\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\right)\right)$$
21	20	biimprd	$$⊢\left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\in ℝ\wedge 0\in ℝ\right)\to \left(\left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\le 0\wedge 0\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\right)\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)=0\right)$$
22	18 19 21	sylancl	$$⊢x\in \mathscr{H}\to \left(\left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\le 0\wedge 0\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\right)\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)=0\right)$$
23	16 22	sylan2i	$$⊢x\in \mathscr{H}\to \left(\left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\le 0\wedge x\in \mathscr{H}\right)\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)=0\right)$$
24	23	anabsi6	$$⊢\left(x\in \mathscr{H}\wedge {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\le 0\right)\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)=0$$
25	13 24	sylan2	$$⊢\left(x\in \mathscr{H}\wedge \left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)\wedge {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)=0\right)\right)\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)=0$$
26	25	expr	$$⊢\left(x\in \mathscr{H}\wedge {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)\right)\to \left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)=0\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)=0\right)$$
27	2	pjhcli	$$⊢x\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\in \mathscr{H}$$
28		norm-i	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\in \mathscr{H}\to \left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)=0\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)=0_{ℎ}\right)$$
29	27 28	syl	$$⊢x\in \mathscr{H}\to \left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)=0\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)=0_{ℎ}\right)$$
30		pjoc2	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in \mathscr{H}\right)\to \left(x\in \perp \left(H\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)=0_{ℎ}\right)$$
31	2 30	mpan	$$⊢x\in \mathscr{H}\to \left(x\in \perp \left(H\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)=0_{ℎ}\right)$$
32	29 31	bitr4d	$$⊢x\in \mathscr{H}\to \left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)=0\leftrightarrow x\in \perp \left(H\right)\right)$$
33	32	adantr	$$⊢\left(x\in \mathscr{H}\wedge {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)\right)\to \left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)=0\leftrightarrow x\in \perp \left(H\right)\right)$$
34		norm-i	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\in \mathscr{H}\to \left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)=0\leftrightarrow {\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)=0_{ℎ}\right)$$
35	14 34	syl	$$⊢x\in \mathscr{H}\to \left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)=0\leftrightarrow {\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)=0_{ℎ}\right)$$
36		pjoc2	$$⊢\left(G\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in \mathscr{H}\right)\to \left(x\in \perp \left(G\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)=0_{ℎ}\right)$$
37	1 36	mpan	$$⊢x\in \mathscr{H}\to \left(x\in \perp \left(G\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)=0_{ℎ}\right)$$
38	35 37	bitr4d	$$⊢x\in \mathscr{H}\to \left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)=0\leftrightarrow x\in \perp \left(G\right)\right)$$
39	38	adantr	$$⊢\left(x\in \mathscr{H}\wedge {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)\right)\to \left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)=0\leftrightarrow x\in \perp \left(G\right)\right)$$
40	26 33 39	3imtr3d	$$⊢\left(x\in \mathscr{H}\wedge {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)\right)\to \left(x\in \perp \left(H\right)\to x\in \perp \left(G\right)\right)$$
41	40	ex	$$⊢x\in \mathscr{H}\to \left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)\to \left(x\in \perp \left(H\right)\to x\in \perp \left(G\right)\right)\right)$$
42	41	a2i	$$⊢\left(x\in \mathscr{H}\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)\right)\to \left(x\in \mathscr{H}\to \left(x\in \perp \left(H\right)\to x\in \perp \left(G\right)\right)\right)$$
43	11 42	syl5	$$⊢\left(x\in \mathscr{H}\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)\right)\to \left(x\in \perp \left(H\right)\to \left(x\in \perp \left(H\right)\to x\in \perp \left(G\right)\right)\right)$$
44	43	pm2.43d	$$⊢\left(x\in \mathscr{H}\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)\right)\to \left(x\in \perp \left(H\right)\to x\in \perp \left(G\right)\right)$$
45	44	alimi	$$⊢\forall x\left(x\in \mathscr{H}\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)\right)\to \forall x\left(x\in \perp \left(H\right)\to x\in \perp \left(G\right)\right)$$
46		df-ral	$$⊢\forall x\in \mathscr{H}{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)\leftrightarrow \forall x\left(x\in \mathscr{H}\to {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)\right)$$
47		df-ss	$$⊢\perp \left(H\right)\subseteq \perp \left(G\right)\leftrightarrow \forall x\left(x\in \perp \left(H\right)\to x\in \perp \left(G\right)\right)$$
48	45 46 47	3imtr4i	$$⊢\forall x\in \mathscr{H}{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)\to \perp \left(H\right)\subseteq \perp \left(G\right)$$
49	1 2	chsscon3i	$$⊢G\subseteq H\leftrightarrow \perp \left(H\right)\subseteq \perp \left(G\right)$$
50	48 49	sylibr	$$⊢\forall x\in \mathscr{H}{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)\to G\subseteq H$$
51	9 50	impbii	$$⊢G\subseteq H\leftrightarrow \forall x\in \mathscr{H}{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right)\right)$$