Metamath Proof Explorer


Theorem strlem3

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. This lemma restates the hypotheses in a more convenient form to work with. (Contributed by NM, 28-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses strlem3.1 𝑆 = ( 𝑥C ↦ ( ( norm ‘ ( ( proj𝑥 ) ‘ 𝑢 ) ) ↑ 2 ) )
strlem3.2 ( 𝜑 ↔ ( 𝑢 ∈ ( 𝐴𝐵 ) ∧ ( norm𝑢 ) = 1 ) )
strlem3.3 𝐴C
strlem3.4 𝐵C
Assertion strlem3 ( 𝜑𝑆 ∈ States )

Proof

Step Hyp Ref Expression
1 strlem3.1 𝑆 = ( 𝑥C ↦ ( ( norm ‘ ( ( proj𝑥 ) ‘ 𝑢 ) ) ↑ 2 ) )
2 strlem3.2 ( 𝜑 ↔ ( 𝑢 ∈ ( 𝐴𝐵 ) ∧ ( norm𝑢 ) = 1 ) )
3 strlem3.3 𝐴C
4 strlem3.4 𝐵C
5 eldifi ( 𝑢 ∈ ( 𝐴𝐵 ) → 𝑢𝐴 )
6 3 cheli ( 𝑢𝐴𝑢 ∈ ℋ )
7 5 6 syl ( 𝑢 ∈ ( 𝐴𝐵 ) → 𝑢 ∈ ℋ )
8 1 strlem3a ( ( 𝑢 ∈ ℋ ∧ ( norm𝑢 ) = 1 ) → 𝑆 ∈ States )
9 7 8 sylan ( ( 𝑢 ∈ ( 𝐴𝐵 ) ∧ ( norm𝑢 ) = 1 ) → 𝑆 ∈ States )
10 2 9 sylbi ( 𝜑𝑆 ∈ States )