Metamath Proof Explorer

Theorem spansncv

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

Ref Expression
Assertion spansncv ⊢ A ∈ C ℋ ∧ B ∈ C ℋ ∧ C ∈ ℋ → A ⊂ B ∧ B ⊆ A ∨ ℋ span ⁡ C → B = A ∨ ℋ span ⁡ C

Proof

Step Hyp Ref Expression
1 psseq1 ⊢ A = if A ∈ C ℋ A ℋ → A ⊂ B ↔ if A ∈ C ℋ A ℋ ⊂ B
2 oveq1 ⊢ A = if A ∈ C ℋ A ℋ → A ∨ ℋ span ⁡ C = if A ∈ C ℋ A ℋ ∨ ℋ span ⁡ C
3 2 sseq2d ⊢ A = if A ∈ C ℋ A ℋ → B ⊆ A ∨ ℋ span ⁡ C ↔ B ⊆ if A ∈ C ℋ A ℋ ∨ ℋ span ⁡ C
4 1 3 anbi12d ⊢ A = if A ∈ C ℋ A ℋ → A ⊂ B ∧ B ⊆ A ∨ ℋ span ⁡ C ↔ if A ∈ C ℋ A ℋ ⊂ B ∧ B ⊆ if A ∈ C ℋ A ℋ ∨ ℋ span ⁡ C
5 2 eqeq2d ⊢ A = if A ∈ C ℋ A ℋ → B = A ∨ ℋ span ⁡ C ↔ B = if A ∈ C ℋ A ℋ ∨ ℋ span ⁡ C
6 4 5 imbi12d ⊢ A = if A ∈ C ℋ A ℋ → A ⊂ B ∧ B ⊆ A ∨ ℋ span ⁡ C → B = A ∨ ℋ span ⁡ C ↔ if A ∈ C ℋ A ℋ ⊂ B ∧ B ⊆ if A ∈ C ℋ A ℋ ∨ ℋ span ⁡ C → B = if A ∈ C ℋ A ℋ ∨ ℋ span ⁡ C
7 psseq2 ⊢ B = if B ∈ C ℋ B ℋ → if A ∈ C ℋ A ℋ ⊂ B ↔ if A ∈ C ℋ A ℋ ⊂ if B ∈ C ℋ B ℋ
8 sseq1 ⊢ B = if B ∈ C ℋ B ℋ → B ⊆ if A ∈ C ℋ A ℋ ∨ ℋ span ⁡ C ↔ if B ∈ C ℋ B ℋ ⊆ if A ∈ C ℋ A ℋ ∨ ℋ span ⁡ C
9 7 8 anbi12d ⊢ B = if B ∈ C ℋ B ℋ → if A ∈ C ℋ A ℋ ⊂ B ∧ B ⊆ if A ∈ C ℋ A ℋ ∨ ℋ span ⁡ C ↔ if A ∈ C ℋ A ℋ ⊂ if B ∈ C ℋ B ℋ ∧ if B ∈ C ℋ B ℋ ⊆ if A ∈ C ℋ A ℋ ∨ ℋ span ⁡ C
10 eqeq1 ⊢ B = if B ∈ C ℋ B ℋ → B = if A ∈ C ℋ A ℋ ∨ ℋ span ⁡ C ↔ if B ∈ C ℋ B ℋ = if A ∈ C ℋ A ℋ ∨ ℋ span ⁡ C
11 9 10 imbi12d ⊢ B = if B ∈ C ℋ B ℋ → if A ∈ C ℋ A ℋ ⊂ B ∧ B ⊆ if A ∈ C ℋ A ℋ ∨ ℋ span ⁡ C → B = if A ∈ C ℋ A ℋ ∨ ℋ span ⁡ C ↔ if A ∈ C ℋ A ℋ ⊂ if B ∈ C ℋ B ℋ ∧ if B ∈ C ℋ B ℋ ⊆ if A ∈ C ℋ A ℋ ∨ ℋ span ⁡ C → if B ∈ C ℋ B ℋ = if A ∈ C ℋ A ℋ ∨ ℋ span ⁡ C
12 sneq ⊢ C = if C ∈ ℋ C 0 ℎ → C = if C ∈ ℋ C 0 ℎ
13 12 fveq2d ⊢ C = if C ∈ ℋ C 0 ℎ → span ⁡ C = span ⁡ if C ∈ ℋ C 0 ℎ
14 13 oveq2d ⊢ C = if C ∈ ℋ C 0 ℎ → if A ∈ C ℋ A ℋ ∨ ℋ span ⁡ C = if A ∈ C ℋ A ℋ ∨ ℋ span ⁡ if C ∈ ℋ C 0 ℎ
15 14 sseq2d ⊢ C = if C ∈ ℋ C 0 ℎ → if B ∈ C ℋ B ℋ ⊆ if A ∈ C ℋ A ℋ ∨ ℋ span ⁡ C ↔ if B ∈ C ℋ B ℋ ⊆ if A ∈ C ℋ A ℋ ∨ ℋ span ⁡ if C ∈ ℋ C 0 ℎ
16 15 anbi2d ⊢ C = if C ∈ ℋ C 0 ℎ → if A ∈ C ℋ A ℋ ⊂ if B ∈ C ℋ B ℋ ∧ if B ∈ C ℋ B ℋ ⊆ if A ∈ C ℋ A ℋ ∨ ℋ span ⁡ C ↔ if A ∈ C ℋ A ℋ ⊂ if B ∈ C ℋ B ℋ ∧ if B ∈ C ℋ B ℋ ⊆ if A ∈ C ℋ A ℋ ∨ ℋ span ⁡ if C ∈ ℋ C 0 ℎ
17 14 eqeq2d ⊢ C = if C ∈ ℋ C 0 ℎ → if B ∈ C ℋ B ℋ = if A ∈ C ℋ A ℋ ∨ ℋ span ⁡ C ↔ if B ∈ C ℋ B ℋ = if A ∈ C ℋ A ℋ ∨ ℋ span ⁡ if C ∈ ℋ C 0 ℎ
18 16 17 imbi12d ⊢ C = if C ∈ ℋ C 0 ℎ → if A ∈ C ℋ A ℋ ⊂ if B ∈ C ℋ B ℋ ∧ if B ∈ C ℋ B ℋ ⊆ if A ∈ C ℋ A ℋ ∨ ℋ span ⁡ C → if B ∈ C ℋ B ℋ = if A ∈ C ℋ A ℋ ∨ ℋ span ⁡ C ↔ if A ∈ C ℋ A ℋ ⊂ if B ∈ C ℋ B ℋ ∧ if B ∈ C ℋ B ℋ ⊆ if A ∈ C ℋ A ℋ ∨ ℋ span ⁡ if C ∈ ℋ C 0 ℎ → if B ∈ C ℋ B ℋ = if A ∈ C ℋ A ℋ ∨ ℋ span ⁡ if C ∈ ℋ C 0 ℎ
19 ifchhv ⊢ if A ∈ C ℋ A ℋ ∈ C ℋ
20 ifchhv ⊢ if B ∈ C ℋ B ℋ ∈ C ℋ
21 ifhvhv0 ⊢ if C ∈ ℋ C 0 ℎ ∈ ℋ
22 19 20 21 spansncvi ⊢ if A ∈ C ℋ A ℋ ⊂ if B ∈ C ℋ B ℋ ∧ if B ∈ C ℋ B ℋ ⊆ if A ∈ C ℋ A ℋ ∨ ℋ span ⁡ if C ∈ ℋ C 0 ℎ → if B ∈ C ℋ B ℋ = if A ∈ C ℋ A ℋ ∨ ℋ span ⁡ if C ∈ ℋ C 0 ℎ
23 6 11 18 22 dedth3h ⊢ A ∈ C ℋ ∧ B ∈ C ℋ ∧ C ∈ ℋ → A ⊂ B ∧ B ⊆ A ∨ ℋ span ⁡ C → B = A ∨ ℋ span ⁡ C