Metamath Proof Explorer

Theorem hstri

Description: Hilbert space admits a strong set of Hilbert-space-valued states (CH-states). Theorem in Mayet3 p. 10. (Contributed by NM, 30-Jun-2006) (New usage is discouraged.)

Ref Expression
Hypotheses hstr.1 
|- A e. CH
hstr.2 
|- B e. CH
Assertion hstri 
|- ( A. f e. CHStates ( ( normh ` ( f ` A ) ) = 1 -> ( normh ` ( f ` B ) ) = 1 ) -> A C_ B )

Proof

Step Hyp Ref Expression
1 hstr.1 
 |-  A e. CH
2 hstr.2 
 |-  B e. CH
3 dfral2 
 |-  ( A. f e. CHStates ( ( normh ` ( f ` A ) ) = 1 -> ( normh ` ( f ` B ) ) = 1 ) <-> -. E. f e. CHStates -. ( ( normh ` ( f ` A ) ) = 1 -> ( normh ` ( f ` B ) ) = 1 ) )
4 1 2 strlem1 
 |-  ( -. A C_ B -> E. u e. ( A \ B ) ( normh ` u ) = 1 )
5 eqid 
 |-  ( x e. CH |-> ( ( projh ` x ) ` u ) ) = ( x e. CH |-> ( ( projh ` x ) ` u ) )
6 biid 
 |-  ( ( u e. ( A \ B ) /\ ( normh ` u ) = 1 ) <-> ( u e. ( A \ B ) /\ ( normh ` u ) = 1 ) )
7 5 6 1 2 hstrlem3 
 |-  ( ( u e. ( A \ B ) /\ ( normh ` u ) = 1 ) -> ( x e. CH |-> ( ( projh ` x ) ` u ) ) e. CHStates )
8 5 6 1 2 hstrlem6 
 |-  ( ( u e. ( A \ B ) /\ ( normh ` u ) = 1 ) -> -. ( ( normh ` ( ( x e. CH |-> ( ( projh ` x ) ` u ) ) ` A ) ) = 1 -> ( normh ` ( ( x e. CH |-> ( ( projh ` x ) ` u ) ) ` B ) ) = 1 ) )
9 fveq1 
 |-  ( f = ( x e. CH |-> ( ( projh ` x ) ` u ) ) -> ( f ` A ) = ( ( x e. CH |-> ( ( projh ` x ) ` u ) ) ` A ) )
10 9 fveqeq2d 
 |-  ( f = ( x e. CH |-> ( ( projh ` x ) ` u ) ) -> ( ( normh ` ( f ` A ) ) = 1 <-> ( normh ` ( ( x e. CH |-> ( ( projh ` x ) ` u ) ) ` A ) ) = 1 ) )
11 fveq1 
 |-  ( f = ( x e. CH |-> ( ( projh ` x ) ` u ) ) -> ( f ` B ) = ( ( x e. CH |-> ( ( projh ` x ) ` u ) ) ` B ) )
12 11 fveqeq2d 
 |-  ( f = ( x e. CH |-> ( ( projh ` x ) ` u ) ) -> ( ( normh ` ( f ` B ) ) = 1 <-> ( normh ` ( ( x e. CH |-> ( ( projh ` x ) ` u ) ) ` B ) ) = 1 ) )
13 10 12 imbi12d 
 |-  ( f = ( x e. CH |-> ( ( projh ` x ) ` u ) ) -> ( ( ( normh ` ( f ` A ) ) = 1 -> ( normh ` ( f ` B ) ) = 1 ) <-> ( ( normh ` ( ( x e. CH |-> ( ( projh ` x ) ` u ) ) ` A ) ) = 1 -> ( normh ` ( ( x e. CH |-> ( ( projh ` x ) ` u ) ) ` B ) ) = 1 ) ) )
14 13 notbid 
 |-  ( f = ( x e. CH |-> ( ( projh ` x ) ` u ) ) -> ( -. ( ( normh ` ( f ` A ) ) = 1 -> ( normh ` ( f ` B ) ) = 1 ) <-> -. ( ( normh ` ( ( x e. CH |-> ( ( projh ` x ) ` u ) ) ` A ) ) = 1 -> ( normh ` ( ( x e. CH |-> ( ( projh ` x ) ` u ) ) ` B ) ) = 1 ) ) )
15 14 rspcev 
 |-  ( ( ( x e. CH |-> ( ( projh ` x ) ` u ) ) e. CHStates /\ -. ( ( normh ` ( ( x e. CH |-> ( ( projh ` x ) ` u ) ) ` A ) ) = 1 -> ( normh ` ( ( x e. CH |-> ( ( projh ` x ) ` u ) ) ` B ) ) = 1 ) ) -> E. f e. CHStates -. ( ( normh ` ( f ` A ) ) = 1 -> ( normh ` ( f ` B ) ) = 1 ) )
16 7 8 15 syl2anc 
 |-  ( ( u e. ( A \ B ) /\ ( normh ` u ) = 1 ) -> E. f e. CHStates -. ( ( normh ` ( f ` A ) ) = 1 -> ( normh ` ( f ` B ) ) = 1 ) )
17 16 rexlimiva 
 |-  ( E. u e. ( A \ B ) ( normh ` u ) = 1 -> E. f e. CHStates -. ( ( normh ` ( f ` A ) ) = 1 -> ( normh ` ( f ` B ) ) = 1 ) )
18 4 17 syl 
 |-  ( -. A C_ B -> E. f e. CHStates -. ( ( normh ` ( f ` A ) ) = 1 -> ( normh ` ( f ` B ) ) = 1 ) )
19 18 con1i 
 |-  ( -. E. f e. CHStates -. ( ( normh ` ( f ` A ) ) = 1 -> ( normh ` ( f ` B ) ) = 1 ) -> A C_ B )
20 3 19 sylbi 
 |-  ( A. f e. CHStates ( ( normh ` ( f ` A ) ) = 1 -> ( normh ` ( f ` B ) ) = 1 ) -> A C_ B )