Description: Lemma for strong set of CH states 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, 30-Jun-2006) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | hstrlem3.1 | |- S = ( x e. CH |-> ( ( projh ` x ) ` u ) ) |
|
| hstrlem3.2 | |- ( ph <-> ( u e. ( A \ B ) /\ ( normh ` u ) = 1 ) ) |
||
| hstrlem3.3 | |- A e. CH |
||
| hstrlem3.4 | |- B e. CH |
||
| Assertion | hstrlem3 | |- ( ph -> S e. CHStates ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hstrlem3.1 | |- S = ( x e. CH |-> ( ( projh ` x ) ` u ) ) |
|
| 2 | hstrlem3.2 | |- ( ph <-> ( u e. ( A \ B ) /\ ( normh ` u ) = 1 ) ) |
|
| 3 | hstrlem3.3 | |- A e. CH |
|
| 4 | hstrlem3.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 | hstrlem3a | |- ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> S e. CHStates ) |
| 9 | 7 8 | sylan | |- ( ( u e. ( A \ B ) /\ ( normh ` u ) = 1 ) -> S e. CHStates ) |
| 10 | 2 9 | sylbi | |- ( ph -> S e. CHStates ) |