This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. CH /\ B e. ~H ) -> ( -. ( span ` { B } ) C_ A -> A

Proof

Step Hyp Ref Expression
1 spansncv 
 |-  ( ( A e. CH /\ x e. CH /\ B e. ~H ) -> ( ( A C. x /\ x C_ ( A vH ( span ` { B } ) ) ) -> x = ( A vH ( span ` { B } ) ) ) )
2 1 3exp 
 |-  ( A e. CH -> ( x e. CH -> ( B e. ~H -> ( ( A C. x /\ x C_ ( A vH ( span ` { B } ) ) ) -> x = ( A vH ( span ` { B } ) ) ) ) ) )
3 2 com23 
 |-  ( A e. CH -> ( B e. ~H -> ( x e. CH -> ( ( A C. x /\ x C_ ( A vH ( span ` { B } ) ) ) -> x = ( A vH ( span ` { B } ) ) ) ) ) )
4 3 imp 
 |-  ( ( A e. CH /\ B e. ~H ) -> ( x e. CH -> ( ( A C. x /\ x C_ ( A vH ( span ` { B } ) ) ) -> x = ( A vH ( span ` { B } ) ) ) ) )
5 4 ralrimiv 
 |-  ( ( A e. CH /\ B e. ~H ) -> A. x e. CH ( ( A C. x /\ x C_ ( A vH ( span ` { B } ) ) ) -> x = ( A vH ( span ` { B } ) ) ) )
6 5 anim2i 
 |-  ( ( A C. ( A vH ( span ` { B } ) ) /\ ( A e. CH /\ B e. ~H ) ) -> ( A C. ( A vH ( span ` { B } ) ) /\ A. x e. CH ( ( A C. x /\ x C_ ( A vH ( span ` { B } ) ) ) -> x = ( A vH ( span ` { B } ) ) ) ) )
7 6 expcom 
 |-  ( ( A e. CH /\ B e. ~H ) -> ( A C. ( A vH ( span ` { B } ) ) -> ( A C. ( A vH ( span ` { B } ) ) /\ A. x e. CH ( ( A C. x /\ x C_ ( A vH ( span ` { B } ) ) ) -> x = ( A vH ( span ` { B } ) ) ) ) ) )
8 spansnch 
 |-  ( B e. ~H -> ( span ` { B } ) e. CH )
9 chnle 
 |-  ( ( A e. CH /\ ( span ` { B } ) e. CH ) -> ( -. ( span ` { B } ) C_ A <-> A C. ( A vH ( span ` { B } ) ) ) )
10 8 9 sylan2 
 |-  ( ( A e. CH /\ B e. ~H ) -> ( -. ( span ` { B } ) C_ A <-> A C. ( A vH ( span ` { B } ) ) ) )
11 chjcl 
 |-  ( ( A e. CH /\ ( span ` { B } ) e. CH ) -> ( A vH ( span ` { B } ) ) e. CH )
12 8 11 sylan2 
 |-  ( ( A e. CH /\ B e. ~H ) -> ( A vH ( span ` { B } ) ) e. CH )
13 cvbr2 
 |-  ( ( A e. CH /\ ( A vH ( span ` { B } ) ) e. CH ) -> ( A  ( A C. ( A vH ( span ` { B } ) ) /\ A. x e. CH ( ( A C. x /\ x C_ ( A vH ( span ` { B } ) ) ) -> x = ( A vH ( span ` { B } ) ) ) ) ) )
14 12 13 syldan 
 |-  ( ( A e. CH /\ B e. ~H ) -> ( A  ( A C. ( A vH ( span ` { B } ) ) /\ A. x e. CH ( ( A C. x /\ x C_ ( A vH ( span ` { B } ) ) ) -> x = ( A vH ( span ` { B } ) ) ) ) ) )
15 7 10 14 3imtr4d 
 |-  ( ( A e. CH /\ B e. ~H ) -> ( -. ( span ` { B } ) C_ A -> A