Theorem chj00i

Description: Two Hilbert lattice elements are zero iff their join is zero. (Contributed by NM, 7-Aug-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ch0le.1	|- A e. CH
	chjcl.2	|- B e. CH
Assertion	chj00i	|- ( ( A = 0H /\ B = 0H ) <-> ( A vH B ) = 0H )

Proof

Step	Hyp	Ref	Expression
1		ch0le.1	|- A e. CH
2		chjcl.2	|- B e. CH
3		oveq12	|- ( ( A = 0H /\ B = 0H ) -> ( A vH B ) = ( 0H vH 0H ) )
4		h0elch	|- 0H e. CH
5	4	chj0i	|- ( 0H vH 0H ) = 0H
6	3 5	eqtrdi	|- ( ( A = 0H /\ B = 0H ) -> ( A vH B ) = 0H )
7	1 2	chub1i	|- A C_ ( A vH B )
8		sseq2	|- ( ( A vH B ) = 0H -> ( A C_ ( A vH B ) <-> A C_ 0H ) )
9	7 8	mpbii	|- ( ( A vH B ) = 0H -> A C_ 0H )
10	1	chle0i	|- ( A C_ 0H <-> A = 0H )
11	9 10	sylib	|- ( ( A vH B ) = 0H -> A = 0H )
12	2 1	chub2i	|- B C_ ( A vH B )
13		sseq2	|- ( ( A vH B ) = 0H -> ( B C_ ( A vH B ) <-> B C_ 0H ) )
14	12 13	mpbii	|- ( ( A vH B ) = 0H -> B C_ 0H )
15	2	chle0i	|- ( B C_ 0H <-> B = 0H )
16	14 15	sylib	|- ( ( A vH B ) = 0H -> B = 0H )
17	11 16	jca	|- ( ( A vH B ) = 0H -> ( A = 0H /\ B = 0H ) )
18	6 17	impbii	|- ( ( A = 0H /\ B = 0H ) <-> ( A vH B ) = 0H )