Theorem lejdiri

Description: An ortholattice is distributive in one ordering direction (join version). (Contributed by NM, 27-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ledi.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
	ledi.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
	ledi.3	$$⊢C\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	lejdiri	$$⊢\left(A\cap B\right){\vee }_{\mathscr{H}}C\subseteq \left(A{\vee }_{\mathscr{H}}C\right)\cap \left(B{\vee }_{\mathscr{H}}C\right)$$

Proof

Step	Hyp	Ref	Expression
1		ledi.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		ledi.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
3		ledi.3	$$⊢C\in {\mathbf{C}}_{\mathscr{H}}$$
4	3 1 2	lejdii	$$⊢C{\vee }_{\mathscr{H}}\left(A\cap B\right)\subseteq \left(C{\vee }_{\mathscr{H}}A\right)\cap \left(C{\vee }_{\mathscr{H}}B\right)$$
5	1 2	chincli	$$⊢A\cap B\in {\mathbf{C}}_{\mathscr{H}}$$
6	5 3	chjcomi	$$⊢\left(A\cap B\right){\vee }_{\mathscr{H}}C=C{\vee }_{\mathscr{H}}\left(A\cap B\right)$$
7	1 3	chjcomi	$$⊢A{\vee }_{\mathscr{H}}C=C{\vee }_{\mathscr{H}}A$$
8	2 3	chjcomi	$$⊢B{\vee }_{\mathscr{H}}C=C{\vee }_{\mathscr{H}}B$$
9	7 8	ineq12i	$$⊢\left(A{\vee }_{\mathscr{H}}C\right)\cap \left(B{\vee }_{\mathscr{H}}C\right)=\left(C{\vee }_{\mathscr{H}}A\right)\cap \left(C{\vee }_{\mathscr{H}}B\right)$$
10	4 6 9	3sstr4i	$$⊢\left(A\cap B\right){\vee }_{\mathscr{H}}C\subseteq \left(A{\vee }_{\mathscr{H}}C\right)\cap \left(B{\vee }_{\mathscr{H}}C\right)$$