Metamath Proof Explorer


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 C
pjnorm.2 A
Assertion pjneli ¬ A H norm proj H A < norm A

Proof

Step Hyp Ref Expression
1 pjnorm.1 H C
2 pjnorm.2 A
3 1 2 pjnormi norm proj H A norm A
4 3 biantrur norm A norm proj H A norm proj H A norm A norm A norm proj H A
5 1 2 pjoc1i A H proj H A = 0
6 1 2 pjpythi norm A 2 = norm proj H A 2 + norm proj H A 2
7 sq0 0 2 = 0
8 7 oveq2i norm proj H A 2 + 0 2 = norm proj H A 2 + 0
9 1 2 pjhclii proj H A
10 9 normcli norm proj H A
11 10 resqcli norm proj H A 2
12 11 recni norm proj H A 2
13 12 addid1i norm proj H A 2 + 0 = norm proj H A 2
14 8 13 eqtr2i norm proj H A 2 = norm proj H A 2 + 0 2
15 6 14 eqeq12i norm A 2 = norm proj H A 2 norm proj H A 2 + norm proj H A 2 = norm proj H A 2 + 0 2
16 1 choccli H C
17 16 2 pjhclii proj H A
18 17 normcli norm proj H A
19 18 resqcli norm proj H A 2
20 19 recni norm proj H A 2
21 0cn 0
22 21 sqcli 0 2
23 12 20 22 addcani norm proj H A 2 + norm proj H A 2 = norm proj H A 2 + 0 2 norm proj H A 2 = 0 2
24 normge0 proj H A 0 norm proj H A
25 17 24 ax-mp 0 norm proj H A
26 0le0 0 0
27 0re 0
28 18 27 sq11i 0 norm proj H A 0 0 norm proj H A 2 = 0 2 norm proj H A = 0
29 25 26 28 mp2an norm proj H A 2 = 0 2 norm proj H A = 0
30 17 norm-i-i norm proj H A = 0 proj H A = 0
31 23 29 30 3bitri norm proj H A 2 + norm proj H A 2 = norm proj H A 2 + 0 2 proj H A = 0
32 15 31 bitr2i proj H A = 0 norm A 2 = norm proj H A 2
33 normge0 A 0 norm A
34 2 33 ax-mp 0 norm A
35 normge0 proj H A 0 norm proj H A
36 9 35 ax-mp 0 norm proj H A
37 2 normcli norm A
38 37 10 sq11i 0 norm A 0 norm proj H A norm A 2 = norm proj H A 2 norm A = norm proj H A
39 34 36 38 mp2an norm A 2 = norm proj H A 2 norm A = norm proj H A
40 5 32 39 3bitri A H norm A = norm proj H A
41 40 necon3bbii ¬ A H norm A norm proj H A
42 10 37 ltleni norm proj H A < norm A norm proj H A norm A norm A norm proj H A
43 4 41 42 3bitr4i ¬ A H norm proj H A < norm A