Metamath Proof Explorer


Theorem strlem3a

Description: Lemma for strong state theorem: the function S , that maps a closed subspace to the square of the norm of its projection onto a unit vector, is a state. (Contributed by NM, 28-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypothesis strlem3a.1 S = x C norm proj x u 2
Assertion strlem3a u norm u = 1 S States

Proof

Step Hyp Ref Expression
1 strlem3a.1 S = x C norm proj x u 2
2 id x C x C
3 simpl u norm u = 1 u
4 pjhcl x C u proj x u
5 2 3 4 syl2anr u norm u = 1 x C proj x u
6 normcl proj x u norm proj x u
7 5 6 syl u norm u = 1 x C norm proj x u
8 7 resqcld u norm u = 1 x C norm proj x u 2
9 7 sqge0d u norm u = 1 x C 0 norm proj x u 2
10 normge0 proj x u 0 norm proj x u
11 5 10 syl u norm u = 1 x C 0 norm proj x u
12 pjnorm x C u norm proj x u norm u
13 2 3 12 syl2anr u norm u = 1 x C norm proj x u norm u
14 simplr u norm u = 1 x C norm u = 1
15 13 14 breqtrd u norm u = 1 x C norm proj x u 1
16 2nn0 2 0
17 exple1 norm proj x u 0 norm proj x u norm proj x u 1 2 0 norm proj x u 2 1
18 16 17 mpan2 norm proj x u 0 norm proj x u norm proj x u 1 norm proj x u 2 1
19 7 11 15 18 syl3anc u norm u = 1 x C norm proj x u 2 1
20 elicc01 norm proj x u 2 0 1 norm proj x u 2 0 norm proj x u 2 norm proj x u 2 1
21 8 9 19 20 syl3anbrc u norm u = 1 x C norm proj x u 2 0 1
22 21 1 fmptd u norm u = 1 S : C 0 1
23 helch C
24 1 strlem2 C S = norm proj u 2
25 23 24 ax-mp S = norm proj u 2
26 pjch1 u proj u = u
27 26 fveq2d u norm proj u = norm u
28 27 oveq1d u norm proj u 2 = norm u 2
29 oveq1 norm u = 1 norm u 2 = 1 2
30 sq1 1 2 = 1
31 29 30 eqtrdi norm u = 1 norm u 2 = 1
32 28 31 sylan9eq u norm u = 1 norm proj u 2 = 1
33 25 32 syl5eq u norm u = 1 S = 1
34 pjcjt2 z C w C u z w proj z w u = proj z u + proj w u
35 34 imp z C w C u z w proj z w u = proj z u + proj w u
36 35 fveq2d z C w C u z w norm proj z w u = norm proj z u + proj w u
37 36 oveq1d z C w C u z w norm proj z w u 2 = norm proj z u + proj w u 2
38 pjopyth z C w C u z w norm proj z u + proj w u 2 = norm proj z u 2 + norm proj w u 2
39 38 imp z C w C u z w norm proj z u + proj w u 2 = norm proj z u 2 + norm proj w u 2
40 37 39 eqtrd z C w C u z w norm proj z w u 2 = norm proj z u 2 + norm proj w u 2
41 chjcl z C w C z w C
42 41 3adant3 z C w C u z w C
43 42 adantr z C w C u z w z w C
44 1 strlem2 z w C S z w = norm proj z w u 2
45 43 44 syl z C w C u z w S z w = norm proj z w u 2
46 3simpa z C w C u z C w C
47 46 adantr z C w C u z w z C w C
48 1 strlem2 z C S z = norm proj z u 2
49 1 strlem2 w C S w = norm proj w u 2
50 48 49 oveqan12d z C w C S z + S w = norm proj z u 2 + norm proj w u 2
51 47 50 syl z C w C u z w S z + S w = norm proj z u 2 + norm proj w u 2
52 40 45 51 3eqtr4d z C w C u z w S z w = S z + S w
53 52 3exp1 z C w C u z w S z w = S z + S w
54 53 com3r u z C w C z w S z w = S z + S w
55 54 adantr u norm u = 1 z C w C z w S z w = S z + S w
56 55 ralrimdv u norm u = 1 z C w C z w S z w = S z + S w
57 56 ralrimiv u norm u = 1 z C w C z w S z w = S z + S w
58 isst S States S : C 0 1 S = 1 z C w C z w S z w = S z + S w
59 22 33 57 58 syl3anbrc u norm u = 1 S States