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	⊢ 𝐴 ∈ Cℋ
Assertion	largei	⊢ ( ¬ 𝐴 = 0ℋ ↔ ∃ 𝑓 ∈ States ( 𝑓 ‘ 𝐴 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		large.1	⊢ 𝐴 ∈ Cℋ
2		ralnex	⊢ ( ∀ 𝑓 ∈ States ¬ ( 𝑓 ‘ 𝐴 ) = 1 ↔ ¬ ∃ 𝑓 ∈ States ( 𝑓 ‘ 𝐴 ) = 1 )
3		ax-1ne0	⊢ 1 ≠ 0
4	3	neii	⊢ ¬ 1 = 0
5		st0	⊢ ( 𝑓 ∈ States → ( 𝑓 ‘ 0ℋ ) = 0 )
6	5	eqeq1d	⊢ ( 𝑓 ∈ States → ( ( 𝑓 ‘ 0ℋ ) = 1 ↔ 0 = 1 ) )
7		eqcom	⊢ ( 0 = 1 ↔ 1 = 0 )
8	6 7	bitrdi	⊢ ( 𝑓 ∈ States → ( ( 𝑓 ‘ 0ℋ ) = 1 ↔ 1 = 0 ) )
9	4 8	mtbiri	⊢ ( 𝑓 ∈ States → ¬ ( 𝑓 ‘ 0ℋ ) = 1 )
10		mtt	⊢ ( ¬ ( 𝑓 ‘ 0ℋ ) = 1 → ( ¬ ( 𝑓 ‘ 𝐴 ) = 1 ↔ ( ( 𝑓 ‘ 𝐴 ) = 1 → ( 𝑓 ‘ 0ℋ ) = 1 ) ) )
11	9 10	syl	⊢ ( 𝑓 ∈ States → ( ¬ ( 𝑓 ‘ 𝐴 ) = 1 ↔ ( ( 𝑓 ‘ 𝐴 ) = 1 → ( 𝑓 ‘ 0ℋ ) = 1 ) ) )
12	11	ralbiia	⊢ ( ∀ 𝑓 ∈ States ¬ ( 𝑓 ‘ 𝐴 ) = 1 ↔ ∀ 𝑓 ∈ States ( ( 𝑓 ‘ 𝐴 ) = 1 → ( 𝑓 ‘ 0ℋ ) = 1 ) )
13		h0elch	⊢ 0ℋ ∈ Cℋ
14	1 13	strb	⊢ ( ∀ 𝑓 ∈ States ( ( 𝑓 ‘ 𝐴 ) = 1 → ( 𝑓 ‘ 0ℋ ) = 1 ) ↔ 𝐴 ⊆ 0ℋ )
15	1	chle0i	⊢ ( 𝐴 ⊆ 0ℋ ↔ 𝐴 = 0ℋ )
16	12 14 15	3bitri	⊢ ( ∀ 𝑓 ∈ States ¬ ( 𝑓 ‘ 𝐴 ) = 1 ↔ 𝐴 = 0ℋ )
17	2 16	bitr3i	⊢ ( ¬ ∃ 𝑓 ∈ States ( 𝑓 ‘ 𝐴 ) = 1 ↔ 𝐴 = 0ℋ )
18	17	con1bii	⊢ ( ¬ 𝐴 = 0ℋ ↔ ∃ 𝑓 ∈ States ( 𝑓 ‘ 𝐴 ) = 1 )