Metamath Proof Explorer

Theorem atcveq0

Description: A Hilbert lattice element covered by an atom must be the zero subspace. (Contributed by NM, 11-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion atcveq0 ⊢ A ∈ C ℋ ∧ B ∈ HAtoms → A ⋖ ℋ B ↔ A = 0 ℋ

Proof

Step Hyp Ref Expression
1 atelch ⊢ B ∈ HAtoms → B ∈ C ℋ
2 cvpss ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A ⋖ ℋ B → A ⊂ B
3 1 2 sylan2 ⊢ A ∈ C ℋ ∧ B ∈ HAtoms → A ⋖ ℋ B → A ⊂ B
4 ch0le ⊢ A ∈ C ℋ → 0 ℋ ⊆ A
5 4 adantr ⊢ A ∈ C ℋ ∧ B ∈ HAtoms → 0 ℋ ⊆ A
6 3 5 jctild ⊢ A ∈ C ℋ ∧ B ∈ HAtoms → A ⋖ ℋ B → 0 ℋ ⊆ A ∧ A ⊂ B
7 atcv0 ⊢ B ∈ HAtoms → 0 ℋ ⋖ ℋ B
8 7 adantr ⊢ B ∈ HAtoms ∧ A ∈ C ℋ → 0 ℋ ⋖ ℋ B
9 h0elch ⊢ 0 ℋ ∈ C ℋ
10 cvnbtwn3 ⊢ 0 ℋ ∈ C ℋ ∧ B ∈ C ℋ ∧ A ∈ C ℋ → 0 ℋ ⋖ ℋ B → 0 ℋ ⊆ A ∧ A ⊂ B → A = 0 ℋ
11 9 10 mp3an1 ⊢ B ∈ C ℋ ∧ A ∈ C ℋ → 0 ℋ ⋖ ℋ B → 0 ℋ ⊆ A ∧ A ⊂ B → A = 0 ℋ
12 1 11 sylan ⊢ B ∈ HAtoms ∧ A ∈ C ℋ → 0 ℋ ⋖ ℋ B → 0 ℋ ⊆ A ∧ A ⊂ B → A = 0 ℋ
13 8 12 mpd ⊢ B ∈ HAtoms ∧ A ∈ C ℋ → 0 ℋ ⊆ A ∧ A ⊂ B → A = 0 ℋ
14 13 ancoms ⊢ A ∈ C ℋ ∧ B ∈ HAtoms → 0 ℋ ⊆ A ∧ A ⊂ B → A = 0 ℋ
15 6 14 syld ⊢ A ∈ C ℋ ∧ B ∈ HAtoms → A ⋖ ℋ B → A = 0 ℋ
16 breq1 ⊢ A = 0 ℋ → A ⋖ ℋ B ↔ 0 ℋ ⋖ ℋ B
17 7 16 syl5ibrcom ⊢ B ∈ HAtoms → A = 0 ℋ → A ⋖ ℋ B
18 17 adantl ⊢ A ∈ C ℋ ∧ B ∈ HAtoms → A = 0 ℋ → A ⋖ ℋ B
19 15 18 impbid ⊢ A ∈ C ℋ ∧ B ∈ HAtoms → A ⋖ ℋ B ↔ A = 0 ℋ