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	⊢ 𝐴 ∈ Cℋ
	chjcl.2	⊢ 𝐵 ∈ Cℋ
Assertion	chj00i	⊢ ( ( 𝐴 = 0ℋ ∧ 𝐵 = 0ℋ ) ↔ ( 𝐴 ∨ℋ 𝐵 ) = 0ℋ )

Proof

Step	Hyp	Ref	Expression
1		ch0le.1	⊢ 𝐴 ∈ Cℋ
2		chjcl.2	⊢ 𝐵 ∈ Cℋ
3		oveq12	⊢ ( ( 𝐴 = 0ℋ ∧ 𝐵 = 0ℋ ) → ( 𝐴 ∨ℋ 𝐵 ) = ( 0ℋ ∨ℋ 0ℋ ) )
4		h0elch	⊢ 0ℋ ∈ Cℋ
5	4	chj0i	⊢ ( 0ℋ ∨ℋ 0ℋ ) = 0ℋ
6	3 5	eqtrdi	⊢ ( ( 𝐴 = 0ℋ ∧ 𝐵 = 0ℋ ) → ( 𝐴 ∨ℋ 𝐵 ) = 0ℋ )
7	1 2	chub1i	⊢ 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐵 )
8		sseq2	⊢ ( ( 𝐴 ∨ℋ 𝐵 ) = 0ℋ → ( 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ↔ 𝐴 ⊆ 0ℋ ) )
9	7 8	mpbii	⊢ ( ( 𝐴 ∨ℋ 𝐵 ) = 0ℋ → 𝐴 ⊆ 0ℋ )
10	1	chle0i	⊢ ( 𝐴 ⊆ 0ℋ ↔ 𝐴 = 0ℋ )
11	9 10	sylib	⊢ ( ( 𝐴 ∨ℋ 𝐵 ) = 0ℋ → 𝐴 = 0ℋ )
12	2 1	chub2i	⊢ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐵 )
13		sseq2	⊢ ( ( 𝐴 ∨ℋ 𝐵 ) = 0ℋ → ( 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ↔ 𝐵 ⊆ 0ℋ ) )
14	12 13	mpbii	⊢ ( ( 𝐴 ∨ℋ 𝐵 ) = 0ℋ → 𝐵 ⊆ 0ℋ )
15	2	chle0i	⊢ ( 𝐵 ⊆ 0ℋ ↔ 𝐵 = 0ℋ )
16	14 15	sylib	⊢ ( ( 𝐴 ∨ℋ 𝐵 ) = 0ℋ → 𝐵 = 0ℋ )
17	11 16	jca	⊢ ( ( 𝐴 ∨ℋ 𝐵 ) = 0ℋ → ( 𝐴 = 0ℋ ∧ 𝐵 = 0ℋ ) )
18	6 17	impbii	⊢ ( ( 𝐴 = 0ℋ ∧ 𝐵 = 0ℋ ) ↔ ( 𝐴 ∨ℋ 𝐵 ) = 0ℋ )