Theorem chj0i

Description: Join with lattice zero in CH . (Contributed by NM, 15-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypothesis	ch0le.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	chj0i	$$⊢A{\vee }_{\mathscr{H}}{0}_{\mathscr{H}}=A$$

Proof

Step	Hyp	Ref	Expression
1		ch0le.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		h0elch	$$⊢0_{\mathscr{H}}\in {\mathbf{C}}_{\mathscr{H}}$$
3	1 2	chjvali	$$⊢A{\vee }_{\mathscr{H}}{0}_{\mathscr{H}}=\perp \left(\perp \left(A\cup 0_{\mathscr{H}}\right)\right)$$
4	1	ch0lei	$$⊢0_{\mathscr{H}}\subseteq A$$
5		ssequn2	$$⊢0_{\mathscr{H}}\subseteq A\leftrightarrow A\cup 0_{\mathscr{H}}=A$$
6	4 5	mpbi	$$⊢A\cup 0_{\mathscr{H}}=A$$
7	6	fveq2i	$$⊢\perp \left(A\cup 0_{\mathscr{H}}\right)=\perp \left(A\right)$$
8	7	fveq2i	$$⊢\perp \left(\perp \left(A\cup 0_{\mathscr{H}}\right)\right)=\perp \left(\perp \left(A\right)\right)$$
9	1	pjococi	$$⊢\perp \left(\perp \left(A\right)\right)=A$$
10	3 8 9	3eqtri	$$⊢A{\vee }_{\mathscr{H}}{0}_{\mathscr{H}}=A$$