Theorem lediri

Description: An ortholattice is distributive in one ordering direction. (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	lediri	$$⊢\left(A\cap C\right){\vee }_{\mathscr{H}}\left(B\cap C\right)\subseteq \left(A{\vee }_{\mathscr{H}}B\right)\cap C$$

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	ledii	$$⊢\left(C\cap A\right){\vee }_{\mathscr{H}}\left(C\cap B\right)\subseteq C\cap \left(A{\vee }_{\mathscr{H}}B\right)$$
5		incom	$$⊢A\cap C=C\cap A$$
6		incom	$$⊢B\cap C=C\cap B$$
7	5 6	oveq12i	$$⊢\left(A\cap C\right){\vee }_{\mathscr{H}}\left(B\cap C\right)=\left(C\cap A\right){\vee }_{\mathscr{H}}\left(C\cap B\right)$$
8		incom	$$⊢\left(A{\vee }_{\mathscr{H}}B\right)\cap C=C\cap \left(A{\vee }_{\mathscr{H}}B\right)$$
9	4 7 8	3sstr4i	$$⊢\left(A\cap C\right){\vee }_{\mathscr{H}}\left(B\cap C\right)\subseteq \left(A{\vee }_{\mathscr{H}}B\right)\cap C$$