Metamath Proof Explorer

Theorem chcv1

Description: The Hilbert lattice has the covering property. Proposition 1(ii) of Kalmbach p. 140 (and its converse). (Contributed by NM, 11-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion chcv1 ⊢ A ∈ C ℋ ∧ B ∈ HAtoms → ¬ B ⊆ A ↔ A ⋖ ℋ A ∨ ℋ B

Proof

Step Hyp Ref Expression
1 atom1d ⊢ B ∈ HAtoms ↔ ∃ x ∈ ℋ x ≠ 0 ℎ ∧ B = span ⁡ x
2 spansncv2 ⊢ A ∈ C ℋ ∧ x ∈ ℋ → ¬ span ⁡ x ⊆ A → A ⋖ ℋ A ∨ ℋ span ⁡ x
3 sseq1 ⊢ B = span ⁡ x → B ⊆ A ↔ span ⁡ x ⊆ A
4 3 notbid ⊢ B = span ⁡ x → ¬ B ⊆ A ↔ ¬ span ⁡ x ⊆ A
5 oveq2 ⊢ B = span ⁡ x → A ∨ ℋ B = A ∨ ℋ span ⁡ x
6 5 breq2d ⊢ B = span ⁡ x → A ⋖ ℋ A ∨ ℋ B ↔ A ⋖ ℋ A ∨ ℋ span ⁡ x
7 4 6 imbi12d ⊢ B = span ⁡ x → ¬ B ⊆ A → A ⋖ ℋ A ∨ ℋ B ↔ ¬ span ⁡ x ⊆ A → A ⋖ ℋ A ∨ ℋ span ⁡ x
8 2 7 syl5ibrcom ⊢ A ∈ C ℋ ∧ x ∈ ℋ → B = span ⁡ x → ¬ B ⊆ A → A ⋖ ℋ A ∨ ℋ B
9 8 adantld ⊢ A ∈ C ℋ ∧ x ∈ ℋ → x ≠ 0 ℎ ∧ B = span ⁡ x → ¬ B ⊆ A → A ⋖ ℋ A ∨ ℋ B
10 9 rexlimdva ⊢ A ∈ C ℋ → ∃ x ∈ ℋ x ≠ 0 ℎ ∧ B = span ⁡ x → ¬ B ⊆ A → A ⋖ ℋ A ∨ ℋ B
11 10 imp ⊢ A ∈ C ℋ ∧ ∃ x ∈ ℋ x ≠ 0 ℎ ∧ B = span ⁡ x → ¬ B ⊆ A → A ⋖ ℋ A ∨ ℋ B
12 1 11 sylan2b ⊢ A ∈ C ℋ ∧ B ∈ HAtoms → ¬ B ⊆ A → A ⋖ ℋ A ∨ ℋ B
13 atelch ⊢ B ∈ HAtoms → B ∈ C ℋ
14 chjcl ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A ∨ ℋ B ∈ C ℋ
15 cvpss ⊢ A ∈ C ℋ ∧ A ∨ ℋ B ∈ C ℋ → A ⋖ ℋ A ∨ ℋ B → A ⊂ A ∨ ℋ B
16 14 15 syldan ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A ⋖ ℋ A ∨ ℋ B → A ⊂ A ∨ ℋ B
17 chnle ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → ¬ B ⊆ A ↔ A ⊂ A ∨ ℋ B
18 16 17 sylibrd ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A ⋖ ℋ A ∨ ℋ B → ¬ B ⊆ A
19 13 18 sylan2 ⊢ A ∈ C ℋ ∧ B ∈ HAtoms → A ⋖ ℋ A ∨ ℋ B → ¬ B ⊆ A
20 12 19 impbid ⊢ A ∈ C ℋ ∧ B ∈ HAtoms → ¬ B ⊆ A ↔ A ⋖ ℋ A ∨ ℋ B