Theorem stcltrthi

Description: Theorem for classically strong set of states. If there exists a "classically strong set of states" on lattice CH (or actually any ortholattice, which would have an identical proof), then any two elements of the lattice commute, i.e., the lattice is distributive. (Proof due to Mladen Pavicic.) Theorem 3.3 of MegPav2000 p. 2344. (Contributed by NM, 24-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	stcltrth.1	⊢ 𝐴 ∈ Cℋ
	stcltrth.2	⊢ 𝐵 ∈ Cℋ
	stcltrth.3	⊢ ∃ 𝑠 ∈ States ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( ( ( 𝑠 ‘ 𝑥 ) = 1 → ( 𝑠 ‘ 𝑦 ) = 1 ) → 𝑥 ⊆ 𝑦 )
Assertion	stcltrthi	⊢ 𝐵 ⊆ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		stcltrth.1	⊢ 𝐴 ∈ Cℋ
2		stcltrth.2	⊢ 𝐵 ∈ Cℋ
3		stcltrth.3	⊢ ∃ 𝑠 ∈ States ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( ( ( 𝑠 ‘ 𝑥 ) = 1 → ( 𝑠 ‘ 𝑦 ) = 1 ) → 𝑥 ⊆ 𝑦 )
4		biid	⊢ ( ( 𝑠 ∈ States ∧ ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( ( ( 𝑠 ‘ 𝑥 ) = 1 → ( 𝑠 ‘ 𝑦 ) = 1 ) → 𝑥 ⊆ 𝑦 ) ) ↔ ( 𝑠 ∈ States ∧ ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( ( ( 𝑠 ‘ 𝑥 ) = 1 → ( 𝑠 ‘ 𝑦 ) = 1 ) → 𝑥 ⊆ 𝑦 ) ) )
5	4 1 2	stcltrlem2	⊢ ( ( 𝑠 ∈ States ∧ ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( ( ( 𝑠 ‘ 𝑥 ) = 1 → ( 𝑠 ‘ 𝑦 ) = 1 ) → 𝑥 ⊆ 𝑦 ) ) → 𝐵 ⊆ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) )
6	5	rexlimiva	⊢ ( ∃ 𝑠 ∈ States ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( ( ( 𝑠 ‘ 𝑥 ) = 1 → ( 𝑠 ‘ 𝑦 ) = 1 ) → 𝑥 ⊆ 𝑦 ) → 𝐵 ⊆ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) )
7	3 6	ax-mp	⊢ 𝐵 ⊆ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) )