Theorem ledi

Description: An ortholattice is distributive in one ordering direction. (Contributed by NM, 14-Jun-2006) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		ineq1	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\to A\cap B=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap B$$
2		ineq1	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\to A\cap C=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap C$$
3	1 2	oveq12d	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\to \left(A\cap B\right){\vee }_{\mathscr{H}}\left(A\cap C\right)=\left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap B\right){\vee }_{\mathscr{H}}\left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap C\right)$$
4		ineq1	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\to A\cap \left(B{\vee }_{\mathscr{H}}C\right)=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap \left(B{\vee }_{\mathscr{H}}C\right)$$
5	3 4	sseq12d	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\to \left(\left(A\cap B\right){\vee }_{\mathscr{H}}\left(A\cap C\right)\subseteq A\cap \left(B{\vee }_{\mathscr{H}}C\right)\leftrightarrow \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap B\right){\vee }_{\mathscr{H}}\left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap C\right)\subseteq if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap \left(B{\vee }_{\mathscr{H}}C\right)\right)$$
6		ineq2	$$⊢B=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,0_{\mathscr{H}}\right)\to if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap B=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,0_{\mathscr{H}}\right)$$
7	6	oveq1d	$$⊢B=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,0_{\mathscr{H}}\right)\to \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap B\right){\vee }_{\mathscr{H}}\left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap C\right)=\left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,0_{\mathscr{H}}\right)\right){\vee }_{\mathscr{H}}\left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap C\right)$$
8		oveq1	$$⊢B=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,0_{\mathscr{H}}\right)\to B{\vee }_{\mathscr{H}}C=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}C$$
9	8	ineq2d	$$⊢B=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,0_{\mathscr{H}}\right)\to if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap \left(B{\vee }_{\mathscr{H}}C\right)=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap \left(if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}C\right)$$
10	7 9	sseq12d	$$⊢B=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,0_{\mathscr{H}}\right)\to \left(\left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap B\right){\vee }_{\mathscr{H}}\left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap C\right)\subseteq if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap \left(B{\vee }_{\mathscr{H}}C\right)\leftrightarrow \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,0_{\mathscr{H}}\right)\right){\vee }_{\mathscr{H}}\left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap C\right)\subseteq if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap \left(if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}C\right)\right)$$
11		ineq2	$$⊢C=if\left(C\in {\mathbf{C}}_{\mathscr{H}},C,0_{\mathscr{H}}\right)\to if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap C=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap if\left(C\in {\mathbf{C}}_{\mathscr{H}},C,0_{\mathscr{H}}\right)$$
12	11	oveq2d	$$⊢C=if\left(C\in {\mathbf{C}}_{\mathscr{H}},C,0_{\mathscr{H}}\right)\to \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,0_{\mathscr{H}}\right)\right){\vee }_{\mathscr{H}}\left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap C\right)=\left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,0_{\mathscr{H}}\right)\right){\vee }_{\mathscr{H}}\left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap if\left(C\in {\mathbf{C}}_{\mathscr{H}},C,0_{\mathscr{H}}\right)\right)$$
13		oveq2	$$⊢C=if\left(C\in {\mathbf{C}}_{\mathscr{H}},C,0_{\mathscr{H}}\right)\to if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}C=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}if\left(C\in {\mathbf{C}}_{\mathscr{H}},C,0_{\mathscr{H}}\right)$$
14	13	ineq2d	$$⊢C=if\left(C\in {\mathbf{C}}_{\mathscr{H}},C,0_{\mathscr{H}}\right)\to if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap \left(if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}C\right)=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap \left(if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}if\left(C\in {\mathbf{C}}_{\mathscr{H}},C,0_{\mathscr{H}}\right)\right)$$
15	12 14	sseq12d	$$⊢C=if\left(C\in {\mathbf{C}}_{\mathscr{H}},C,0_{\mathscr{H}}\right)\to \left(\left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,0_{\mathscr{H}}\right)\right){\vee }_{\mathscr{H}}\left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap C\right)\subseteq if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap \left(if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}C\right)\leftrightarrow \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,0_{\mathscr{H}}\right)\right){\vee }_{\mathscr{H}}\left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap if\left(C\in {\mathbf{C}}_{\mathscr{H}},C,0_{\mathscr{H}}\right)\right)\subseteq if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap \left(if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}if\left(C\in {\mathbf{C}}_{\mathscr{H}},C,0_{\mathscr{H}}\right)\right)\right)$$
16		h0elch	$$⊢0_{\mathscr{H}}\in {\mathbf{C}}_{\mathscr{H}}$$
17	16	elimel	$$⊢if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
18	16	elimel	$$⊢if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,0_{\mathscr{H}}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
19	16	elimel	$$⊢if\left(C\in {\mathbf{C}}_{\mathscr{H}},C,0_{\mathscr{H}}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
20	17 18 19	ledii	$$⊢\left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,0_{\mathscr{H}}\right)\right){\vee }_{\mathscr{H}}\left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap if\left(C\in {\mathbf{C}}_{\mathscr{H}},C,0_{\mathscr{H}}\right)\right)\subseteq if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap \left(if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}if\left(C\in {\mathbf{C}}_{\mathscr{H}},C,0_{\mathscr{H}}\right)\right)$$
21	5 10 15 20	dedth3h	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A\cap B\right){\vee }_{\mathscr{H}}\left(A\cap C\right)\subseteq A\cap \left(B{\vee }_{\mathscr{H}}C\right)$$