Theorem ledii

Description: An ortholattice is distributive in one ordering direction. (Contributed by NM, 6-Aug-2004) (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	ledii	$$⊢\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		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		inss1	$$⊢A\cap B\subseteq A$$
5		inss1	$$⊢A\cap C\subseteq A$$
6	1 2	chincli	$$⊢A\cap B\in {\mathbf{C}}_{\mathscr{H}}$$
7	1 3	chincli	$$⊢A\cap C\in {\mathbf{C}}_{\mathscr{H}}$$
8	6 7 1	chlubii	$$⊢\left(A\cap B\subseteq A\wedge A\cap C\subseteq A\right)\to \left(A\cap B\right){\vee }_{\mathscr{H}}\left(A\cap C\right)\subseteq A$$
9	4 5 8	mp2an	$$⊢\left(A\cap B\right){\vee }_{\mathscr{H}}\left(A\cap C\right)\subseteq A$$
10		inss2	$$⊢A\cap B\subseteq B$$
11		inss2	$$⊢A\cap C\subseteq C$$
12	6 2 7 3	chlej12i	$$⊢\left(A\cap B\subseteq B\wedge A\cap C\subseteq C\right)\to \left(A\cap B\right){\vee }_{\mathscr{H}}\left(A\cap C\right)\subseteq B{\vee }_{\mathscr{H}}C$$
13	10 11 12	mp2an	$$⊢\left(A\cap B\right){\vee }_{\mathscr{H}}\left(A\cap C\right)\subseteq B{\vee }_{\mathscr{H}}C$$
14	9 13	ssini	$$⊢\left(A\cap B\right){\vee }_{\mathscr{H}}\left(A\cap C\right)\subseteq A\cap \left(B{\vee }_{\mathscr{H}}C\right)$$