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 ⊢ 𝑆 = ( 𝑥 ∈ Cℋ ↦ ( ( normℎ ‘ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ↑ 2 ) )
Assertion strlem3a ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) → 𝑆 ∈ States )

Proof

Step Hyp Ref Expression
1 strlem3a.1 ⊢ 𝑆 = ( 𝑥 ∈ Cℋ ↦ ( ( normℎ ‘ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ↑ 2 ) )
2 id ⊢ ( 𝑥 ∈ Cℋ → 𝑥 ∈ Cℋ )
3 simpl ⊢ ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) → 𝑢 ∈ ℋ )
4 pjhcl ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝑢 ∈ ℋ ) → ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ∈ ℋ )
5 2 3 4 syl2anr ⊢ ( ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) ∧ 𝑥 ∈ Cℋ ) → ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ∈ ℋ )
6 normcl ⊢ ( ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ∈ ℋ → ( normℎ ‘ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ∈ ℝ )
7 5 6 syl ⊢ ( ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) ∧ 𝑥 ∈ Cℋ ) → ( normℎ ‘ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ∈ ℝ )
8 7 resqcld ⊢ ( ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) ∧ 𝑥 ∈ Cℋ ) → ( ( normℎ ‘ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ↑ 2 ) ∈ ℝ )
9 7 sqge0d ⊢ ( ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) ∧ 𝑥 ∈ Cℋ ) → 0 ≤ ( ( normℎ ‘ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ↑ 2 ) )
10 normge0 ⊢ ( ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ∈ ℋ → 0 ≤ ( normℎ ‘ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) )
11 5 10 syl ⊢ ( ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) ∧ 𝑥 ∈ Cℋ ) → 0 ≤ ( normℎ ‘ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) )
12 pjnorm ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝑢 ∈ ℋ ) → ( normℎ ‘ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ≤ ( normℎ ‘ 𝑢 ) )
13 2 3 12 syl2anr ⊢ ( ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) ∧ 𝑥 ∈ Cℋ ) → ( normℎ ‘ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ≤ ( normℎ ‘ 𝑢 ) )
14 simplr ⊢ ( ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) ∧ 𝑥 ∈ Cℋ ) → ( normℎ ‘ 𝑢 ) = 1 )
15 13 14 breqtrd ⊢ ( ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) ∧ 𝑥 ∈ Cℋ ) → ( normℎ ‘ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ≤ 1 )
16 2nn0 ⊢ 2 ∈ ℕ0
17 exple1 ⊢ ( ( ( ( normℎ ‘ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ∈ ℝ ∧ 0 ≤ ( normℎ ‘ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ∧ ( normℎ ‘ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ≤ 1 ) ∧ 2 ∈ ℕ0 ) → ( ( normℎ ‘ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ↑ 2 ) ≤ 1 )
18 16 17 mpan2 ⊢ ( ( ( normℎ ‘ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ∈ ℝ ∧ 0 ≤ ( normℎ ‘ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ∧ ( normℎ ‘ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ≤ 1 ) → ( ( normℎ ‘ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ↑ 2 ) ≤ 1 )
19 7 11 15 18 syl3anc ⊢ ( ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) ∧ 𝑥 ∈ Cℋ ) → ( ( normℎ ‘ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ↑ 2 ) ≤ 1 )
20 elicc01 ⊢ ( ( ( normℎ ‘ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ↑ 2 ) ∈ ( 0 [,] 1 ) ↔ ( ( ( normℎ ‘ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( ( normℎ ‘ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ↑ 2 ) ∧ ( ( normℎ ‘ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ↑ 2 ) ≤ 1 ) )
21 8 9 19 20 syl3anbrc ⊢ ( ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) ∧ 𝑥 ∈ Cℋ ) → ( ( normℎ ‘ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ↑ 2 ) ∈ ( 0 [,] 1 ) )
22 21 1 fmptd ⊢ ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) → 𝑆 : Cℋ ⟶ ( 0 [,] 1 ) )
23 helch ⊢ ℋ ∈ Cℋ
24 1 strlem2 ⊢ ( ℋ ∈ Cℋ → ( 𝑆 ‘ ℋ ) = ( ( normℎ ‘ ( ( projℎ ‘ ℋ ) ‘ 𝑢 ) ) ↑ 2 ) )
25 23 24 ax-mp ⊢ ( 𝑆 ‘ ℋ ) = ( ( normℎ ‘ ( ( projℎ ‘ ℋ ) ‘ 𝑢 ) ) ↑ 2 )
26 pjch1 ⊢ ( 𝑢 ∈ ℋ → ( ( projℎ ‘ ℋ ) ‘ 𝑢 ) = 𝑢 )
27 26 fveq2d ⊢ ( 𝑢 ∈ ℋ → ( normℎ ‘ ( ( projℎ ‘ ℋ ) ‘ 𝑢 ) ) = ( normℎ ‘ 𝑢 ) )
28 27 oveq1d ⊢ ( 𝑢 ∈ ℋ → ( ( normℎ ‘ ( ( projℎ ‘ ℋ ) ‘ 𝑢 ) ) ↑ 2 ) = ( ( normℎ ‘ 𝑢 ) ↑ 2 ) )
29 oveq1 ⊢ ( ( normℎ ‘ 𝑢 ) = 1 → ( ( normℎ ‘ 𝑢 ) ↑ 2 ) = ( 1 ↑ 2 ) )
30 sq1 ⊢ ( 1 ↑ 2 ) = 1
31 29 30 eqtrdi ⊢ ( ( normℎ ‘ 𝑢 ) = 1 → ( ( normℎ ‘ 𝑢 ) ↑ 2 ) = 1 )
32 28 31 sylan9eq ⊢ ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) → ( ( normℎ ‘ ( ( projℎ ‘ ℋ ) ‘ 𝑢 ) ) ↑ 2 ) = 1 )
33 25 32 syl5eq ⊢ ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) → ( 𝑆 ‘ ℋ ) = 1 )
34 pjcjt2 ⊢ ( ( 𝑧 ∈ Cℋ ∧ 𝑤 ∈ Cℋ ∧ 𝑢 ∈ ℋ ) → ( 𝑧 ⊆ ( ⊥ ‘ 𝑤 ) → ( ( projℎ ‘ ( 𝑧 ∨ℋ 𝑤 ) ) ‘ 𝑢 ) = ( ( ( projℎ ‘ 𝑧 ) ‘ 𝑢 ) +ℎ ( ( projℎ ‘ 𝑤 ) ‘ 𝑢 ) ) ) )
35 34 imp ⊢ ( ( ( 𝑧 ∈ Cℋ ∧ 𝑤 ∈ Cℋ ∧ 𝑢 ∈ ℋ ) ∧ 𝑧 ⊆ ( ⊥ ‘ 𝑤 ) ) → ( ( projℎ ‘ ( 𝑧 ∨ℋ 𝑤 ) ) ‘ 𝑢 ) = ( ( ( projℎ ‘ 𝑧 ) ‘ 𝑢 ) +ℎ ( ( projℎ ‘ 𝑤 ) ‘ 𝑢 ) ) )
36 35 fveq2d ⊢ ( ( ( 𝑧 ∈ Cℋ ∧ 𝑤 ∈ Cℋ ∧ 𝑢 ∈ ℋ ) ∧ 𝑧 ⊆ ( ⊥ ‘ 𝑤 ) ) → ( normℎ ‘ ( ( projℎ ‘ ( 𝑧 ∨ℋ 𝑤 ) ) ‘ 𝑢 ) ) = ( normℎ ‘ ( ( ( projℎ ‘ 𝑧 ) ‘ 𝑢 ) +ℎ ( ( projℎ ‘ 𝑤 ) ‘ 𝑢 ) ) ) )
37 36 oveq1d ⊢ ( ( ( 𝑧 ∈ Cℋ ∧ 𝑤 ∈ Cℋ ∧ 𝑢 ∈ ℋ ) ∧ 𝑧 ⊆ ( ⊥ ‘ 𝑤 ) ) → ( ( normℎ ‘ ( ( projℎ ‘ ( 𝑧 ∨ℋ 𝑤 ) ) ‘ 𝑢 ) ) ↑ 2 ) = ( ( normℎ ‘ ( ( ( projℎ ‘ 𝑧 ) ‘ 𝑢 ) +ℎ ( ( projℎ ‘ 𝑤 ) ‘ 𝑢 ) ) ) ↑ 2 ) )
38 pjopyth ⊢ ( ( 𝑧 ∈ Cℋ ∧ 𝑤 ∈ Cℋ ∧ 𝑢 ∈ ℋ ) → ( 𝑧 ⊆ ( ⊥ ‘ 𝑤 ) → ( ( normℎ ‘ ( ( ( projℎ ‘ 𝑧 ) ‘ 𝑢 ) +ℎ ( ( projℎ ‘ 𝑤 ) ‘ 𝑢 ) ) ) ↑ 2 ) = ( ( ( normℎ ‘ ( ( projℎ ‘ 𝑧 ) ‘ 𝑢 ) ) ↑ 2 ) + ( ( normℎ ‘ ( ( projℎ ‘ 𝑤 ) ‘ 𝑢 ) ) ↑ 2 ) ) ) )
39 38 imp ⊢ ( ( ( 𝑧 ∈ Cℋ ∧ 𝑤 ∈ Cℋ ∧ 𝑢 ∈ ℋ ) ∧ 𝑧 ⊆ ( ⊥ ‘ 𝑤 ) ) → ( ( normℎ ‘ ( ( ( projℎ ‘ 𝑧 ) ‘ 𝑢 ) +ℎ ( ( projℎ ‘ 𝑤 ) ‘ 𝑢 ) ) ) ↑ 2 ) = ( ( ( normℎ ‘ ( ( projℎ ‘ 𝑧 ) ‘ 𝑢 ) ) ↑ 2 ) + ( ( normℎ ‘ ( ( projℎ ‘ 𝑤 ) ‘ 𝑢 ) ) ↑ 2 ) ) )
40 37 39 eqtrd ⊢ ( ( ( 𝑧 ∈ Cℋ ∧ 𝑤 ∈ Cℋ ∧ 𝑢 ∈ ℋ ) ∧ 𝑧 ⊆ ( ⊥ ‘ 𝑤 ) ) → ( ( normℎ ‘ ( ( projℎ ‘ ( 𝑧 ∨ℋ 𝑤 ) ) ‘ 𝑢 ) ) ↑ 2 ) = ( ( ( normℎ ‘ ( ( projℎ ‘ 𝑧 ) ‘ 𝑢 ) ) ↑ 2 ) + ( ( normℎ ‘ ( ( projℎ ‘ 𝑤 ) ‘ 𝑢 ) ) ↑ 2 ) ) )
41 chjcl ⊢ ( ( 𝑧 ∈ Cℋ ∧ 𝑤 ∈ Cℋ ) → ( 𝑧 ∨ℋ 𝑤 ) ∈ Cℋ )
42 41 3adant3 ⊢ ( ( 𝑧 ∈ Cℋ ∧ 𝑤 ∈ Cℋ ∧ 𝑢 ∈ ℋ ) → ( 𝑧 ∨ℋ 𝑤 ) ∈ Cℋ )
43 42 adantr ⊢ ( ( ( 𝑧 ∈ Cℋ ∧ 𝑤 ∈ Cℋ ∧ 𝑢 ∈ ℋ ) ∧ 𝑧 ⊆ ( ⊥ ‘ 𝑤 ) ) → ( 𝑧 ∨ℋ 𝑤 ) ∈ Cℋ )
44 1 strlem2 ⊢ ( ( 𝑧 ∨ℋ 𝑤 ) ∈ Cℋ → ( 𝑆 ‘ ( 𝑧 ∨ℋ 𝑤 ) ) = ( ( normℎ ‘ ( ( projℎ ‘ ( 𝑧 ∨ℋ 𝑤 ) ) ‘ 𝑢 ) ) ↑ 2 ) )
45 43 44 syl ⊢ ( ( ( 𝑧 ∈ Cℋ ∧ 𝑤 ∈ Cℋ ∧ 𝑢 ∈ ℋ ) ∧ 𝑧 ⊆ ( ⊥ ‘ 𝑤 ) ) → ( 𝑆 ‘ ( 𝑧 ∨ℋ 𝑤 ) ) = ( ( normℎ ‘ ( ( projℎ ‘ ( 𝑧 ∨ℋ 𝑤 ) ) ‘ 𝑢 ) ) ↑ 2 ) )
46 3simpa ⊢ ( ( 𝑧 ∈ Cℋ ∧ 𝑤 ∈ Cℋ ∧ 𝑢 ∈ ℋ ) → ( 𝑧 ∈ Cℋ ∧ 𝑤 ∈ Cℋ ) )
47 46 adantr ⊢ ( ( ( 𝑧 ∈ Cℋ ∧ 𝑤 ∈ Cℋ ∧ 𝑢 ∈ ℋ ) ∧ 𝑧 ⊆ ( ⊥ ‘ 𝑤 ) ) → ( 𝑧 ∈ Cℋ ∧ 𝑤 ∈ Cℋ ) )
48 1 strlem2 ⊢ ( 𝑧 ∈ Cℋ → ( 𝑆 ‘ 𝑧 ) = ( ( normℎ ‘ ( ( projℎ ‘ 𝑧 ) ‘ 𝑢 ) ) ↑ 2 ) )
49 1 strlem2 ⊢ ( 𝑤 ∈ Cℋ → ( 𝑆 ‘ 𝑤 ) = ( ( normℎ ‘ ( ( projℎ ‘ 𝑤 ) ‘ 𝑢 ) ) ↑ 2 ) )
50 48 49 oveqan12d ⊢ ( ( 𝑧 ∈ Cℋ ∧ 𝑤 ∈ Cℋ ) → ( ( 𝑆 ‘ 𝑧 ) + ( 𝑆 ‘ 𝑤 ) ) = ( ( ( normℎ ‘ ( ( projℎ ‘ 𝑧 ) ‘ 𝑢 ) ) ↑ 2 ) + ( ( normℎ ‘ ( ( projℎ ‘ 𝑤 ) ‘ 𝑢 ) ) ↑ 2 ) ) )
51 47 50 syl ⊢ ( ( ( 𝑧 ∈ Cℋ ∧ 𝑤 ∈ Cℋ ∧ 𝑢 ∈ ℋ ) ∧ 𝑧 ⊆ ( ⊥ ‘ 𝑤 ) ) → ( ( 𝑆 ‘ 𝑧 ) + ( 𝑆 ‘ 𝑤 ) ) = ( ( ( normℎ ‘ ( ( projℎ ‘ 𝑧 ) ‘ 𝑢 ) ) ↑ 2 ) + ( ( normℎ ‘ ( ( projℎ ‘ 𝑤 ) ‘ 𝑢 ) ) ↑ 2 ) ) )
52 40 45 51 3eqtr4d ⊢ ( ( ( 𝑧 ∈ Cℋ ∧ 𝑤 ∈ Cℋ ∧ 𝑢 ∈ ℋ ) ∧ 𝑧 ⊆ ( ⊥ ‘ 𝑤 ) ) → ( 𝑆 ‘ ( 𝑧 ∨ℋ 𝑤 ) ) = ( ( 𝑆 ‘ 𝑧 ) + ( 𝑆 ‘ 𝑤 ) ) )
53 52 3exp1 ⊢ ( 𝑧 ∈ Cℋ → ( 𝑤 ∈ Cℋ → ( 𝑢 ∈ ℋ → ( 𝑧 ⊆ ( ⊥ ‘ 𝑤 ) → ( 𝑆 ‘ ( 𝑧 ∨ℋ 𝑤 ) ) = ( ( 𝑆 ‘ 𝑧 ) + ( 𝑆 ‘ 𝑤 ) ) ) ) ) )
54 53 com3r ⊢ ( 𝑢 ∈ ℋ → ( 𝑧 ∈ Cℋ → ( 𝑤 ∈ Cℋ → ( 𝑧 ⊆ ( ⊥ ‘ 𝑤 ) → ( 𝑆 ‘ ( 𝑧 ∨ℋ 𝑤 ) ) = ( ( 𝑆 ‘ 𝑧 ) + ( 𝑆 ‘ 𝑤 ) ) ) ) ) )
55 54 adantr ⊢ ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) → ( 𝑧 ∈ Cℋ → ( 𝑤 ∈ Cℋ → ( 𝑧 ⊆ ( ⊥ ‘ 𝑤 ) → ( 𝑆 ‘ ( 𝑧 ∨ℋ 𝑤 ) ) = ( ( 𝑆 ‘ 𝑧 ) + ( 𝑆 ‘ 𝑤 ) ) ) ) ) )
56 55 ralrimdv ⊢ ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) → ( 𝑧 ∈ Cℋ → ∀ 𝑤 ∈ Cℋ ( 𝑧 ⊆ ( ⊥ ‘ 𝑤 ) → ( 𝑆 ‘ ( 𝑧 ∨ℋ 𝑤 ) ) = ( ( 𝑆 ‘ 𝑧 ) + ( 𝑆 ‘ 𝑤 ) ) ) ) )
57 56 ralrimiv ⊢ ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) → ∀ 𝑧 ∈ Cℋ ∀ 𝑤 ∈ Cℋ ( 𝑧 ⊆ ( ⊥ ‘ 𝑤 ) → ( 𝑆 ‘ ( 𝑧 ∨ℋ 𝑤 ) ) = ( ( 𝑆 ‘ 𝑧 ) + ( 𝑆 ‘ 𝑤 ) ) ) )
58 isst ⊢ ( 𝑆 ∈ States ↔ ( 𝑆 : Cℋ ⟶ ( 0 [,] 1 ) ∧ ( 𝑆 ‘ ℋ ) = 1 ∧ ∀ 𝑧 ∈ Cℋ ∀ 𝑤 ∈ Cℋ ( 𝑧 ⊆ ( ⊥ ‘ 𝑤 ) → ( 𝑆 ‘ ( 𝑧 ∨ℋ 𝑤 ) ) = ( ( 𝑆 ‘ 𝑧 ) + ( 𝑆 ‘ 𝑤 ) ) ) ) )
59 22 33 57 58 syl3anbrc ⊢ ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) → 𝑆 ∈ States )