Theorem chdmm1

Description: De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	chdmm1	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \perp \left(A\cap B\right)=\perp \left(A\right){\vee }_{\mathscr{H}}\perp \left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		ineq1	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to A\cap B=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\cap B$$
2	1	fveq2d	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to \perp \left(A\cap B\right)=\perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\cap B\right)$$
3		fveq2	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to \perp \left(A\right)=\perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\right)$$
4	3	oveq1d	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to \perp \left(A\right){\vee }_{\mathscr{H}}\perp \left(B\right)=\perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\right){\vee }_{\mathscr{H}}\perp \left(B\right)$$
5	2 4	eqeq12d	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to \left(\perp \left(A\cap B\right)=\perp \left(A\right){\vee }_{\mathscr{H}}\perp \left(B\right)\leftrightarrow \perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\cap B\right)=\perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\right){\vee }_{\mathscr{H}}\perp \left(B\right)\right)$$
6		ineq2	$$⊢B=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\to if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\cap B=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\cap if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)$$
7	6	fveq2d	$$⊢B=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\to \perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\cap B\right)=\perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\cap if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\right)$$
8		fveq2	$$⊢B=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\to \perp \left(B\right)=\perp \left(if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\right)$$
9	8	oveq2d	$$⊢B=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\to \perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\right){\vee }_{\mathscr{H}}\perp \left(B\right)=\perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\right){\vee }_{\mathscr{H}}\perp \left(if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\right)$$
10	7 9	eqeq12d	$$⊢B=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\to \left(\perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\cap B\right)=\perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\right){\vee }_{\mathscr{H}}\perp \left(B\right)\leftrightarrow \perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\cap if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\right)=\perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\right){\vee }_{\mathscr{H}}\perp \left(if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\right)\right)$$
11		ifchhv	$$⊢if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
12		ifchhv	$$⊢if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
13	11 12	chdmm1i	$$⊢\perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\cap if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\right)=\perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\right){\vee }_{\mathscr{H}}\perp \left(if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\right)$$
14	5 10 13	dedth2h	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \perp \left(A\cap B\right)=\perp \left(A\right){\vee }_{\mathscr{H}}\perp \left(B\right)$$