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 ACBCCABBAspanCB=AspanC

Proof

Step Hyp Ref Expression
1 psseq1 A=ifACAABifACAB
2 oveq1 A=ifACAAspanC=ifACAspanC
3 2 sseq2d A=ifACABAspanCBifACAspanC
4 1 3 anbi12d A=ifACAABBAspanCifACABBifACAspanC
5 2 eqeq2d A=ifACAB=AspanCB=ifACAspanC
6 4 5 imbi12d A=ifACAABBAspanCB=AspanCifACABBifACAspanCB=ifACAspanC
7 psseq2 B=ifBCBifACABifACAifBCB
8 sseq1 B=ifBCBBifACAspanCifBCBifACAspanC
9 7 8 anbi12d B=ifBCBifACABBifACAspanCifACAifBCBifBCBifACAspanC
10 eqeq1 B=ifBCBB=ifACAspanCifBCB=ifACAspanC
11 9 10 imbi12d B=ifBCBifACABBifACAspanCB=ifACAspanCifACAifBCBifBCBifACAspanCifBCB=ifACAspanC
12 sneq C=ifCC0C=ifCC0
13 12 fveq2d C=ifCC0spanC=spanifCC0
14 13 oveq2d C=ifCC0ifACAspanC=ifACAspanifCC0
15 14 sseq2d C=ifCC0ifBCBifACAspanCifBCBifACAspanifCC0
16 15 anbi2d C=ifCC0ifACAifBCBifBCBifACAspanCifACAifBCBifBCBifACAspanifCC0
17 14 eqeq2d C=ifCC0ifBCB=ifACAspanCifBCB=ifACAspanifCC0
18 16 17 imbi12d C=ifCC0ifACAifBCBifBCBifACAspanCifBCB=ifACAspanCifACAifBCBifBCBifACAspanifCC0ifBCB=ifACAspanifCC0
19 ifchhv ifACAC
20 ifchhv ifBCBC
21 ifhvhv0 ifCC0
22 19 20 21 spansncvi ifACAifBCBifBCBifACAspanifCC0ifBCB=ifACAspanifCC0
23 6 11 18 22 dedth3h ACBCCABBAspanCB=AspanC