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

Metamath Proof Explorer

Theorem chcv1

Description: The Hilbert lattice has the covering property. Proposition 1(ii) of Kalmbach p. 140 (and its converse). (Contributed by NM, 11-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion chcv1 
|- ( ( A e. CH /\ B e. HAtoms ) -> ( -. B C_ A <-> A

Proof

Step Hyp Ref Expression
1 atom1d 
 |-  ( B e. HAtoms <-> E. x e. ~H ( x =/= 0h /\ B = ( span ` { x } ) ) )
2 spansncv2 
 |-  ( ( A e. CH /\ x e. ~H ) -> ( -. ( span ` { x } ) C_ A -> A
3 sseq1 
 |-  ( B = ( span ` { x } ) -> ( B C_ A <-> ( span ` { x } ) C_ A ) )
4 3 notbid 
 |-  ( B = ( span ` { x } ) -> ( -. B C_ A <-> -. ( span ` { x } ) C_ A ) )
5 oveq2 
 |-  ( B = ( span ` { x } ) -> ( A vH B ) = ( A vH ( span ` { x } ) ) )
6 5 breq2d 
 |-  ( B = ( span ` { x } ) -> ( A  A
7 4 6 imbi12d 
 |-  ( B = ( span ` { x } ) -> ( ( -. B C_ A -> A  ( -. ( span ` { x } ) C_ A -> A
8 2 7 syl5ibrcom 
 |-  ( ( A e. CH /\ x e. ~H ) -> ( B = ( span ` { x } ) -> ( -. B C_ A -> A
9 8 adantld 
 |-  ( ( A e. CH /\ x e. ~H ) -> ( ( x =/= 0h /\ B = ( span ` { x } ) ) -> ( -. B C_ A -> A
10 9 rexlimdva 
 |-  ( A e. CH -> ( E. x e. ~H ( x =/= 0h /\ B = ( span ` { x } ) ) -> ( -. B C_ A -> A
11 10 imp 
 |-  ( ( A e. CH /\ E. x e. ~H ( x =/= 0h /\ B = ( span ` { x } ) ) ) -> ( -. B C_ A -> A
12 1 11 sylan2b 
 |-  ( ( A e. CH /\ B e. HAtoms ) -> ( -. B C_ A -> A
13 atelch 
 |-  ( B e. HAtoms -> B e. CH )
14 chjcl 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A vH B ) e. CH )
15 cvpss 
 |-  ( ( A e. CH /\ ( A vH B ) e. CH ) -> ( A  A C. ( A vH B ) ) )
16 14 15 syldan 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A  A C. ( A vH B ) ) )
17 chnle 
 |-  ( ( A e. CH /\ B e. CH ) -> ( -. B C_ A <-> A C. ( A vH B ) ) )
18 16 17 sylibrd 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A  -. B C_ A ) )
19 13 18 sylan2 
 |-  ( ( A e. CH /\ B e. HAtoms ) -> ( A  -. B C_ A ) )
20 12 19 impbid 
 |-  ( ( A e. CH /\ B e. HAtoms ) -> ( -. B C_ A <-> A