Theorem chj0

Description: Join with Hilbert lattice zero. (Contributed by NM, 22-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	chj0	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to A{\vee }_{\mathscr{H}}{0}_{\mathscr{H}}=A$$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\to A{\vee }_{\mathscr{H}}{0}_{\mathscr{H}}=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}{0}_{\mathscr{H}}$$
2		id	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\to A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)$$
3	1 2	eqeq12d	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\to \left(A{\vee }_{\mathscr{H}}{0}_{\mathscr{H}}=A\leftrightarrow if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}{0}_{\mathscr{H}}=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\right)$$
4		h0elch	$$⊢0_{\mathscr{H}}\in {\mathbf{C}}_{\mathscr{H}}$$
5	4	elimel	$$⊢if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
6	5	chj0i	$$⊢if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}{0}_{\mathscr{H}}=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)$$
7	3 6	dedth	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to A{\vee }_{\mathscr{H}}{0}_{\mathscr{H}}=A$$