# 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 ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\wedge {C}\in ℋ\right)\to \left(\left({A}\subset {B}\wedge {B}\subseteq {A}{\vee }_{ℋ}\mathrm{span}\left(\left\{{C}\right\}\right)\right)\to {B}={A}{\vee }_{ℋ}\mathrm{span}\left(\left\{{C}\right\}\right)\right)$

### Proof

Step Hyp Ref Expression
1 psseq1 ${⊢}{A}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\to \left({A}\subset {B}↔if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\subset {B}\right)$
2 oveq1 ${⊢}{A}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\to {A}{\vee }_{ℋ}\mathrm{span}\left(\left\{{C}\right\}\right)=if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right){\vee }_{ℋ}\mathrm{span}\left(\left\{{C}\right\}\right)$
3 2 sseq2d ${⊢}{A}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\to \left({B}\subseteq {A}{\vee }_{ℋ}\mathrm{span}\left(\left\{{C}\right\}\right)↔{B}\subseteq if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right){\vee }_{ℋ}\mathrm{span}\left(\left\{{C}\right\}\right)\right)$
4 1 3 anbi12d ${⊢}{A}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\to \left(\left({A}\subset {B}\wedge {B}\subseteq {A}{\vee }_{ℋ}\mathrm{span}\left(\left\{{C}\right\}\right)\right)↔\left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\subset {B}\wedge {B}\subseteq if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right){\vee }_{ℋ}\mathrm{span}\left(\left\{{C}\right\}\right)\right)\right)$
5 2 eqeq2d ${⊢}{A}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\to \left({B}={A}{\vee }_{ℋ}\mathrm{span}\left(\left\{{C}\right\}\right)↔{B}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right){\vee }_{ℋ}\mathrm{span}\left(\left\{{C}\right\}\right)\right)$
6 4 5 imbi12d ${⊢}{A}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\to \left(\left(\left({A}\subset {B}\wedge {B}\subseteq {A}{\vee }_{ℋ}\mathrm{span}\left(\left\{{C}\right\}\right)\right)\to {B}={A}{\vee }_{ℋ}\mathrm{span}\left(\left\{{C}\right\}\right)\right)↔\left(\left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\subset {B}\wedge {B}\subseteq if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right){\vee }_{ℋ}\mathrm{span}\left(\left\{{C}\right\}\right)\right)\to {B}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right){\vee }_{ℋ}\mathrm{span}\left(\left\{{C}\right\}\right)\right)\right)$
7 psseq2 ${⊢}{B}=if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\to \left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\subset {B}↔if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\subset if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\right)$
8 sseq1 ${⊢}{B}=if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\to \left({B}\subseteq if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right){\vee }_{ℋ}\mathrm{span}\left(\left\{{C}\right\}\right)↔if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\subseteq if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right){\vee }_{ℋ}\mathrm{span}\left(\left\{{C}\right\}\right)\right)$
9 7 8 anbi12d ${⊢}{B}=if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\to \left(\left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\subset {B}\wedge {B}\subseteq if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right){\vee }_{ℋ}\mathrm{span}\left(\left\{{C}\right\}\right)\right)↔\left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\subset if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\wedge if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\subseteq if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right){\vee }_{ℋ}\mathrm{span}\left(\left\{{C}\right\}\right)\right)\right)$
10 eqeq1 ${⊢}{B}=if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\to \left({B}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right){\vee }_{ℋ}\mathrm{span}\left(\left\{{C}\right\}\right)↔if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)=if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right){\vee }_{ℋ}\mathrm{span}\left(\left\{{C}\right\}\right)\right)$
11 9 10 imbi12d ${⊢}{B}=if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\to \left(\left(\left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\subset {B}\wedge {B}\subseteq if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right){\vee }_{ℋ}\mathrm{span}\left(\left\{{C}\right\}\right)\right)\to {B}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right){\vee }_{ℋ}\mathrm{span}\left(\left\{{C}\right\}\right)\right)↔\left(\left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\subset if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\wedge if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\subseteq if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right){\vee }_{ℋ}\mathrm{span}\left(\left\{{C}\right\}\right)\right)\to if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)=if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right){\vee }_{ℋ}\mathrm{span}\left(\left\{{C}\right\}\right)\right)\right)$
12 sneq ${⊢}{C}=if\left({C}\in ℋ,{C},{0}_{ℎ}\right)\to \left\{{C}\right\}=\left\{if\left({C}\in ℋ,{C},{0}_{ℎ}\right)\right\}$
13 12 fveq2d ${⊢}{C}=if\left({C}\in ℋ,{C},{0}_{ℎ}\right)\to \mathrm{span}\left(\left\{{C}\right\}\right)=\mathrm{span}\left(\left\{if\left({C}\in ℋ,{C},{0}_{ℎ}\right)\right\}\right)$
14 13 oveq2d ${⊢}{C}=if\left({C}\in ℋ,{C},{0}_{ℎ}\right)\to if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right){\vee }_{ℋ}\mathrm{span}\left(\left\{{C}\right\}\right)=if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right){\vee }_{ℋ}\mathrm{span}\left(\left\{if\left({C}\in ℋ,{C},{0}_{ℎ}\right)\right\}\right)$
15 14 sseq2d ${⊢}{C}=if\left({C}\in ℋ,{C},{0}_{ℎ}\right)\to \left(if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\subseteq if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right){\vee }_{ℋ}\mathrm{span}\left(\left\{{C}\right\}\right)↔if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\subseteq if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right){\vee }_{ℋ}\mathrm{span}\left(\left\{if\left({C}\in ℋ,{C},{0}_{ℎ}\right)\right\}\right)\right)$
16 15 anbi2d ${⊢}{C}=if\left({C}\in ℋ,{C},{0}_{ℎ}\right)\to \left(\left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\subset if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\wedge if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\subseteq if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right){\vee }_{ℋ}\mathrm{span}\left(\left\{{C}\right\}\right)\right)↔\left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\subset if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\wedge if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\subseteq if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right){\vee }_{ℋ}\mathrm{span}\left(\left\{if\left({C}\in ℋ,{C},{0}_{ℎ}\right)\right\}\right)\right)\right)$
17 14 eqeq2d ${⊢}{C}=if\left({C}\in ℋ,{C},{0}_{ℎ}\right)\to \left(if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)=if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right){\vee }_{ℋ}\mathrm{span}\left(\left\{{C}\right\}\right)↔if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)=if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right){\vee }_{ℋ}\mathrm{span}\left(\left\{if\left({C}\in ℋ,{C},{0}_{ℎ}\right)\right\}\right)\right)$
18 16 17 imbi12d ${⊢}{C}=if\left({C}\in ℋ,{C},{0}_{ℎ}\right)\to \left(\left(\left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\subset if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\wedge if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\subseteq if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right){\vee }_{ℋ}\mathrm{span}\left(\left\{{C}\right\}\right)\right)\to if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)=if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right){\vee }_{ℋ}\mathrm{span}\left(\left\{{C}\right\}\right)\right)↔\left(\left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\subset if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\wedge if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\subseteq if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right){\vee }_{ℋ}\mathrm{span}\left(\left\{if\left({C}\in ℋ,{C},{0}_{ℎ}\right)\right\}\right)\right)\to if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)=if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right){\vee }_{ℋ}\mathrm{span}\left(\left\{if\left({C}\in ℋ,{C},{0}_{ℎ}\right)\right\}\right)\right)\right)$
19 ifchhv ${⊢}if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\in {\mathbf{C}}_{ℋ}$
20 ifchhv ${⊢}if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\in {\mathbf{C}}_{ℋ}$
21 ifhvhv0 ${⊢}if\left({C}\in ℋ,{C},{0}_{ℎ}\right)\in ℋ$
22 19 20 21 spansncvi ${⊢}\left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\subset if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\wedge if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\subseteq if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right){\vee }_{ℋ}\mathrm{span}\left(\left\{if\left({C}\in ℋ,{C},{0}_{ℎ}\right)\right\}\right)\right)\to if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)=if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right){\vee }_{ℋ}\mathrm{span}\left(\left\{if\left({C}\in ℋ,{C},{0}_{ℎ}\right)\right\}\right)$
23 6 11 18 22 dedth3h ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\wedge {C}\in ℋ\right)\to \left(\left({A}\subset {B}\wedge {B}\subseteq {A}{\vee }_{ℋ}\mathrm{span}\left(\left\{{C}\right\}\right)\right)\to {B}={A}{\vee }_{ℋ}\mathrm{span}\left(\left\{{C}\right\}\right)\right)$