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