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 ACB¬spanBAAAspanB

Proof

Step Hyp Ref Expression
1 spansncv ACxCBAxxAspanBx=AspanB
2 1 3exp ACxCBAxxAspanBx=AspanB
3 2 com23 ACBxCAxxAspanBx=AspanB
4 3 imp ACBxCAxxAspanBx=AspanB
5 4 ralrimiv ACBxCAxxAspanBx=AspanB
6 5 anim2i AAspanBACBAAspanBxCAxxAspanBx=AspanB
7 6 expcom ACBAAspanBAAspanBxCAxxAspanBx=AspanB
8 spansnch BspanBC
9 chnle ACspanBC¬spanBAAAspanB
10 8 9 sylan2 ACB¬spanBAAAspanB
11 chjcl ACspanBCAspanBC
12 8 11 sylan2 ACBAspanBC
13 cvbr2 ACAspanBCAAspanBAAspanBxCAxxAspanBx=AspanB
14 12 13 syldan ACBAAspanBAAspanBxCAxxAspanBx=AspanB
15 7 10 14 3imtr4d ACB¬spanBAAAspanB