Theorem pjneli

Description: If a vector does not belong to subspace, the norm of its projection is less than its norm. (Contributed by NM, 27-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjnorm.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
	pjnorm.2	$$⊢A\in \mathscr{H}$$
Assertion	pjneli	$$⊢\neg A\in H\leftrightarrow {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)<{norm}_{ℎ}\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		pjnorm.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjnorm.2	$$⊢A\in \mathscr{H}$$
3	1 2	pjnormi	$$⊢{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)\le {norm}_{ℎ}\left(A\right)$$
4	3	biantrur	$$⊢{norm}_{ℎ}\left(A\right)\ne {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)\leftrightarrow \left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)\le {norm}_{ℎ}\left(A\right)\wedge {norm}_{ℎ}\left(A\right)\ne {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)\right)$$
5	1 2	pjoc1i	$$⊢A\in H\leftrightarrow {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)=0_{ℎ}$$
6	1 2	pjpythi	$$⊢{{norm}_{ℎ}\left(A\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2+{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right)}^2$$
7		sq0	$$⊢0^2=0$$
8	7	oveq2i	$$⊢{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2+0^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2+0$$
9	1 2	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathscr{H}$$
10	9	normcli	$$⊢{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)\in ℝ$$
11	10	resqcli	$$⊢{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2\in ℝ$$
12	11	recni	$$⊢{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2\in ℂ$$
13	12	addridi	$$⊢{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2+0={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2$$
14	8 13	eqtr2i	$$⊢{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2+0^2$$
15	6 14	eqeq12i	$$⊢{{norm}_{ℎ}\left(A\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+{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2+0^2$$
16	1	choccli	$$⊢\perp \left(H\right)\in {\mathbf{C}}_{\mathscr{H}}$$
17	16 2	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\in \mathscr{H}$$
18	17	normcli	$$⊢{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right)\in ℝ$$
19	18	resqcli	$$⊢{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right)}^2\in ℝ$$
20	19	recni	$$⊢{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right)}^2\in ℂ$$
21		0cn	$$⊢0\in ℂ$$
22	21	sqcli	$$⊢0^2\in ℂ$$
23	12 20 22	addcani	$$⊢{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2+{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2+0^2\leftrightarrow {{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right)}^2=0^2$$
24		normge0	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\in \mathscr{H}\to 0\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right)$$
25	17 24	ax-mp	$$⊢0\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right)$$
26		0le0	$$⊢0\le 0$$
27		0re	$$⊢0\in ℝ$$
28	18 27	sq11i	$$⊢\left(0\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right)\wedge 0\le 0\right)\to \left({{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right)}^2=0^2\leftrightarrow {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right)=0\right)$$
29	25 26 28	mp2an	$$⊢{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right)}^2=0^2\leftrightarrow {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right)=0$$
30	17	norm-i-i	$$⊢{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right)=0\leftrightarrow {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)=0_{ℎ}$$
31	23 29 30	3bitri	$$⊢{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2+{{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2+0^2\leftrightarrow {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)=0_{ℎ}$$
32	15 31	bitr2i	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)=0_{ℎ}\leftrightarrow {{norm}_{ℎ}\left(A\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2$$
33		normge0	$$⊢A\in \mathscr{H}\to 0\le {norm}_{ℎ}\left(A\right)$$
34	2 33	ax-mp	$$⊢0\le {norm}_{ℎ}\left(A\right)$$
35		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)$$
36	9 35	ax-mp	$$⊢0\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)$$
37	2	normcli	$$⊢{norm}_{ℎ}\left(A\right)\in ℝ$$
38	37 10	sq11i	$$⊢\left(0\le {norm}_{ℎ}\left(A\right)\wedge 0\le {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)\right)\to \left({{norm}_{ℎ}\left(A\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2\leftrightarrow {norm}_{ℎ}\left(A\right)={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)\right)$$
39	34 36 38	mp2an	$$⊢{{norm}_{ℎ}\left(A\right)}^2={{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)}^2\leftrightarrow {norm}_{ℎ}\left(A\right)={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)$$
40	5 32 39	3bitri	$$⊢A\in H\leftrightarrow {norm}_{ℎ}\left(A\right)={norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)$$
41	40	necon3bbii	$$⊢\neg A\in H\leftrightarrow {norm}_{ℎ}\left(A\right)\ne {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)$$
42	10 37	ltleni	$$⊢{norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)<{norm}_{ℎ}\left(A\right)\leftrightarrow \left({norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)\le {norm}_{ℎ}\left(A\right)\wedge {norm}_{ℎ}\left(A\right)\ne {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)\right)$$
43	4 41 42	3bitr4i	$$⊢\neg A\in H\leftrightarrow {norm}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)<{norm}_{ℎ}\left(A\right)$$