Metamath Proof Explorer

Theorem spansncv2

Description: Hilbert space has the covering property (using spans of singletons to represent atoms). Proposition 1(ii) of Kalmbach p. 153. (Contributed by NM, 9-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion spansncv2 ⊢ A ∈ C ℋ ∧ B ∈ ℋ → ¬ span ⁡ B ⊆ A → A ⋖ ℋ A ∨ ℋ span ⁡ B

Proof

Step Hyp Ref Expression
1 spansncv ⊢ A ∈ C ℋ ∧ x ∈ C ℋ ∧ B ∈ ℋ → A ⊂ x ∧ x ⊆ A ∨ ℋ span ⁡ B → x = A ∨ ℋ span ⁡ B
2 1 3exp ⊢ A ∈ C ℋ → x ∈ C ℋ → B ∈ ℋ → A ⊂ x ∧ x ⊆ A ∨ ℋ span ⁡ B → x = A ∨ ℋ span ⁡ B
3 2 com23 ⊢ A ∈ C ℋ → B ∈ ℋ → x ∈ C ℋ → A ⊂ x ∧ x ⊆ A ∨ ℋ span ⁡ B → x = A ∨ ℋ span ⁡ B
4 3 imp ⊢ A ∈ C ℋ ∧ B ∈ ℋ → x ∈ C ℋ → A ⊂ x ∧ x ⊆ A ∨ ℋ span ⁡ B → x = A ∨ ℋ span ⁡ B
5 4 ralrimiv ⊢ A ∈ C ℋ ∧ B ∈ ℋ → ∀ x ∈ C ℋ A ⊂ x ∧ x ⊆ A ∨ ℋ span ⁡ B → x = A ∨ ℋ span ⁡ B
6 5 anim2i ⊢ A ⊂ A ∨ ℋ span ⁡ B ∧ A ∈ C ℋ ∧ B ∈ ℋ → A ⊂ A ∨ ℋ span ⁡ B ∧ ∀ x ∈ C ℋ A ⊂ x ∧ x ⊆ A ∨ ℋ span ⁡ B → x = A ∨ ℋ span ⁡ B
7 6 expcom ⊢ A ∈ C ℋ ∧ B ∈ ℋ → A ⊂ A ∨ ℋ span ⁡ B → A ⊂ A ∨ ℋ span ⁡ B ∧ ∀ x ∈ C ℋ A ⊂ x ∧ x ⊆ A ∨ ℋ span ⁡ B → x = A ∨ ℋ span ⁡ B
8 spansnch ⊢ B ∈ ℋ → span ⁡ B ∈ C ℋ
9 chnle ⊢ A ∈ C ℋ ∧ span ⁡ B ∈ C ℋ → ¬ span ⁡ B ⊆ A ↔ A ⊂ A ∨ ℋ span ⁡ B
10 8 9 sylan2 ⊢ A ∈ C ℋ ∧ B ∈ ℋ → ¬ span ⁡ B ⊆ A ↔ A ⊂ A ∨ ℋ span ⁡ B
11 chjcl ⊢ A ∈ C ℋ ∧ span ⁡ B ∈ C ℋ → A ∨ ℋ span ⁡ B ∈ C ℋ
12 8 11 sylan2 ⊢ A ∈ C ℋ ∧ B ∈ ℋ → A ∨ ℋ span ⁡ B ∈ C ℋ
13 cvbr2 ⊢ A ∈ C ℋ ∧ A ∨ ℋ span ⁡ B ∈ C ℋ → A ⋖ ℋ A ∨ ℋ span ⁡ B ↔ A ⊂ A ∨ ℋ span ⁡ B ∧ ∀ x ∈ C ℋ A ⊂ x ∧ x ⊆ A ∨ ℋ span ⁡ B → x = A ∨ ℋ span ⁡ B
14 12 13 syldan ⊢ A ∈ C ℋ ∧ B ∈ ℋ → A ⋖ ℋ A ∨ ℋ span ⁡ B ↔ A ⊂ A ∨ ℋ span ⁡ B ∧ ∀ x ∈ C ℋ A ⊂ x ∧ x ⊆ A ∨ ℋ span ⁡ B → x = A ∨ ℋ span ⁡ B
15 7 10 14 3imtr4d ⊢ A ∈ C ℋ ∧ B ∈ ℋ → ¬ span ⁡ B ⊆ A → A ⋖ ℋ A ∨ ℋ span ⁡ B