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 \in C_{ℋ}$
	chjcl.2	$⊢ B \in C_{ℋ}$
Assertion	chj00i	$⊢ (A = 0_{ℋ} \land B = 0_{ℋ}) \leftrightarrow A \lor_{ℋ} B = 0_{ℋ}$

Step	Hyp	Ref	Expression
1		ch0le.1	$⊢ A \in C_{ℋ}$
2		chjcl.2	$⊢ B \in C_{ℋ}$
3		oveq12	$⊢ (A = 0_{ℋ} \land B = 0_{ℋ}) \to A \lor_{ℋ} B = 0_{ℋ} \lor_{ℋ} 0_{ℋ}$
4		h0elch	$⊢ 0_{ℋ} \in C_{ℋ}$
5	4	chj0i	$⊢ 0_{ℋ} \lor_{ℋ} 0_{ℋ} = 0_{ℋ}$
6	3 5	eqtrdi	$⊢ (A = 0_{ℋ} \land B = 0_{ℋ}) \to A \lor_{ℋ} B = 0_{ℋ}$
7	1 2	chub1i	$⊢ A \subseteq A \lor_{ℋ} B$
8		sseq2	$⊢ A \lor_{ℋ} B = 0_{ℋ} \to (A \subseteq A \lor_{ℋ} B \leftrightarrow A \subseteq 0_{ℋ})$
9	7 8	mpbii	$⊢ A \lor_{ℋ} B = 0_{ℋ} \to A \subseteq 0_{ℋ}$
10	1	chle0i	$⊢ A \subseteq 0_{ℋ} \leftrightarrow A = 0_{ℋ}$
11	9 10	sylib	$⊢ A \lor_{ℋ} B = 0_{ℋ} \to A = 0_{ℋ}$
12	2 1	chub2i	$⊢ B \subseteq A \lor_{ℋ} B$
13		sseq2	$⊢ A \lor_{ℋ} B = 0_{ℋ} \to (B \subseteq A \lor_{ℋ} B \leftrightarrow B \subseteq 0_{ℋ})$
14	12 13	mpbii	$⊢ A \lor_{ℋ} B = 0_{ℋ} \to B \subseteq 0_{ℋ}$
15	2	chle0i	$⊢ B \subseteq 0_{ℋ} \leftrightarrow B = 0_{ℋ}$
16	14 15	sylib	$⊢ A \lor_{ℋ} B = 0_{ℋ} \to B = 0_{ℋ}$
17	11 16	jca	$⊢ A \lor_{ℋ} B = 0_{ℋ} \to (A = 0_{ℋ} \land B = 0_{ℋ})$
18	6 17	impbii	$⊢ (A = 0_{ℋ} \land B = 0_{ℋ}) \leftrightarrow A \lor_{ℋ} B = 0_{ℋ}$

Metamath Proof Explorer