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