Metamath Proof Explorer

Theorem stri

Description: Strong state theorem. The states on a Hilbert lattice define an ordering. Remark in Mayet p. 370. (Contributed by NM, 2-Nov-1999) (New usage is discouraged.)

Ref Expression
Hypotheses str.1 
|- A e. CH
str.2 
|- B e. CH
Assertion stri 
|- ( A. f e. States ( ( f ` A ) = 1 -> ( f ` B ) = 1 ) -> A C_ B )

Proof

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