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 | |- S = ( x e. CH |-> ( ( normh ` ( ( projh ` x ) ` u ) ) ^ 2 ) ) |
|
| strlem3.2 | |- ( ph <-> ( u e. ( A \ B ) /\ ( normh ` u ) = 1 ) ) |
||
| strlem3.3 | |- A e. CH |
||
| strlem3.4 | |- B e. CH |
||
| Assertion | strlem3 | |- ( ph -> S e. States ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | strlem3.1 | |- S = ( x e. CH |-> ( ( normh ` ( ( projh ` x ) ` u ) ) ^ 2 ) ) |
|
| 2 | strlem3.2 | |- ( ph <-> ( u e. ( A \ B ) /\ ( normh ` u ) = 1 ) ) |
|
| 3 | strlem3.3 | |- A e. CH |
|
| 4 | strlem3.4 | |- B e. CH |
|
| 5 | eldifi | |- ( u e. ( A \ B ) -> u e. A ) |
|
| 6 | 3 | cheli | |- ( u e. A -> u e. ~H ) |
| 7 | 5 6 | syl | |- ( u e. ( A \ B ) -> u e. ~H ) |
| 8 | 1 | strlem3a | |- ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> S e. States ) |
| 9 | 7 8 | sylan | |- ( ( u e. ( A \ B ) /\ ( normh ` u ) = 1 ) -> S e. States ) |
| 10 | 2 9 | sylbi | |- ( ph -> S e. States ) |