Theorem chnlei

Description: Equivalent expressions for "not less than" in the Hilbert lattice. (Contributed by NM, 5-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ch0le.1	|- A e. CH
	chjcl.2	|- B e. CH
Assertion	chnlei	|- ( -. B C_ A <-> A C. ( A vH B ) )

Proof

Step	Hyp	Ref	Expression
1		ch0le.1	|- A e. CH
2		chjcl.2	|- B e. CH
3	1 2	chub1i	|- A C_ ( A vH B )
4	3	biantrur	|- ( -. A = ( A vH B ) <-> ( A C_ ( A vH B ) /\ -. A = ( A vH B ) ) )
5	2 1	chlejb1i	|- ( B C_ A <-> ( B vH A ) = A )
6		eqcom	|- ( ( B vH A ) = A <-> A = ( B vH A ) )
7	2 1	chjcomi	|- ( B vH A ) = ( A vH B )
8	7	eqeq2i	|- ( A = ( B vH A ) <-> A = ( A vH B ) )
9	5 6 8	3bitri	|- ( B C_ A <-> A = ( A vH B ) )
10	9	notbii	|- ( -. B C_ A <-> -. A = ( A vH B ) )
11		dfpss2	|- ( A C. ( A vH B ) <-> ( A C_ ( A vH B ) /\ -. A = ( A vH B ) ) )
12	4 10 11	3bitr4i	|- ( -. B C_ A <-> A C. ( A vH B ) )