Theorem lejdii

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	lejdii	$$⊢A{\vee }_{\mathscr{H}}\left(B\cap C\right)\subseteq \left(A{\vee }_{\mathscr{H}}B\right)\cap \left(A{\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	1 2	chub1i	$$⊢A\subseteq A{\vee }_{\mathscr{H}}B$$
5	1 3	chub1i	$$⊢A\subseteq A{\vee }_{\mathscr{H}}C$$
6	4 5	ssini	$$⊢A\subseteq \left(A{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}C\right)$$
7		inss1	$$⊢B\cap C\subseteq B$$
8	2 1	chub2i	$$⊢B\subseteq A{\vee }_{\mathscr{H}}B$$
9	7 8	sstri	$$⊢B\cap C\subseteq A{\vee }_{\mathscr{H}}B$$
10		inss2	$$⊢B\cap C\subseteq C$$
11	3 1	chub2i	$$⊢C\subseteq A{\vee }_{\mathscr{H}}C$$
12	10 11	sstri	$$⊢B\cap C\subseteq A{\vee }_{\mathscr{H}}C$$
13	9 12	ssini	$$⊢B\cap C\subseteq \left(A{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}C\right)$$
14	2 3	chincli	$$⊢B\cap C\in {\mathbf{C}}_{\mathscr{H}}$$
15	1 2	chjcli	$$⊢A{\vee }_{\mathscr{H}}B\in {\mathbf{C}}_{\mathscr{H}}$$
16	1 3	chjcli	$$⊢A{\vee }_{\mathscr{H}}C\in {\mathbf{C}}_{\mathscr{H}}$$
17	15 16	chincli	$$⊢\left(A{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}C\right)\in {\mathbf{C}}_{\mathscr{H}}$$
18	1 14 17	chlubi	$$⊢\left(A\subseteq \left(A{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}C\right)\wedge B\cap C\subseteq \left(A{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}C\right)\right)\leftrightarrow A{\vee }_{\mathscr{H}}\left(B\cap C\right)\subseteq \left(A{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}C\right)$$
19	18	bicomi	$$⊢A{\vee }_{\mathscr{H}}\left(B\cap C\right)\subseteq \left(A{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}C\right)\leftrightarrow \left(A\subseteq \left(A{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}C\right)\wedge B\cap C\subseteq \left(A{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}C\right)\right)$$
20	6 13 19	mpbir2an	$$⊢A{\vee }_{\mathscr{H}}\left(B\cap C\right)\subseteq \left(A{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}C\right)$$