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 )