Metamath Proof Explorer

Theorem largei

Description: A Hilbert lattice admits a largei set of states. Remark in Mayet p. 370. (Contributed by NM, 7-Apr-2001) (New usage is discouraged.)

Ref Expression
Hypothesis large.1 
|- A e. CH
Assertion largei 
|- ( -. A = 0H <-> E. f e. States ( f ` A ) = 1 )

Proof

Step Hyp Ref Expression
1 large.1 
 |-  A e. CH
2 ralnex 
 |-  ( A. f e. States -. ( f ` A ) = 1 <-> -. E. f e. States ( f ` A ) = 1 )
3 ax-1ne0 
 |-  1 =/= 0
4 3 neii 
 |-  -. 1 = 0
5 st0 
 |-  ( f e. States -> ( f ` 0H ) = 0 )
6 5 eqeq1d 
 |-  ( f e. States -> ( ( f ` 0H ) = 1 <-> 0 = 1 ) )
7 eqcom 
 |-  ( 0 = 1 <-> 1 = 0 )
8 6 7 bitrdi 
 |-  ( f e. States -> ( ( f ` 0H ) = 1 <-> 1 = 0 ) )
9 4 8 mtbiri 
 |-  ( f e. States -> -. ( f ` 0H ) = 1 )
10 mtt 
 |-  ( -. ( f ` 0H ) = 1 -> ( -. ( f ` A ) = 1 <-> ( ( f ` A ) = 1 -> ( f ` 0H ) = 1 ) ) )
11 9 10 syl 
 |-  ( f e. States -> ( -. ( f ` A ) = 1 <-> ( ( f ` A ) = 1 -> ( f ` 0H ) = 1 ) ) )
12 11 ralbiia 
 |-  ( A. f e. States -. ( f ` A ) = 1 <-> A. f e. States ( ( f ` A ) = 1 -> ( f ` 0H ) = 1 ) )
13 h0elch 
 |-  0H e. CH
14 1 13 strb 
 |-  ( A. f e. States ( ( f ` A ) = 1 -> ( f ` 0H ) = 1 ) <-> A C_ 0H )
15 1 chle0i 
 |-  ( A C_ 0H <-> A = 0H )
16 12 14 15 3bitri 
 |-  ( A. f e. States -. ( f ` A ) = 1 <-> A = 0H )
17 2 16 bitr3i 
 |-  ( -. E. f e. States ( f ` A ) = 1 <-> A = 0H )
18 17 con1bii 
 |-  ( -. A = 0H <-> E. f e. States ( f ` A ) = 1 )