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 C_{ℋ}$
	ledi.2	$⊢ B \in C_{ℋ}$
	ledi.3	$⊢ C \in C_{ℋ}$
Assertion	ledii	$⊢ (A \cap B) \lor_{ℋ} (A \cap C) \subseteq A \cap (B \lor_{ℋ} C)$

Step	Hyp	Ref	Expression
1		ledi.1	$⊢ A \in C_{ℋ}$
2		ledi.2	$⊢ B \in C_{ℋ}$
3		ledi.3	$⊢ C \in C_{ℋ}$
4		inss1	$⊢ A \cap B \subseteq A$
5		inss1	$⊢ A \cap C \subseteq A$
6	1 2	chincli	$⊢ A \cap B \in C_{ℋ}$
7	1 3	chincli	$⊢ A \cap C \in C_{ℋ}$
8	6 7 1	chlubii	$⊢ (A \cap B \subseteq A \land A \cap C \subseteq A) \to (A \cap B) \lor_{ℋ} (A \cap C) \subseteq A$
9	4 5 8	mp2an	$⊢ (A \cap B) \lor_{ℋ} (A \cap C) \subseteq A$
10		inss2	$⊢ A \cap B \subseteq B$
11		inss2	$⊢ A \cap C \subseteq C$
12	6 2 7 3	chlej12i	$⊢ (A \cap B \subseteq B \land A \cap C \subseteq C) \to (A \cap B) \lor_{ℋ} (A \cap C) \subseteq B \lor_{ℋ} C$
13	10 11 12	mp2an	$⊢ (A \cap B) \lor_{ℋ} (A \cap C) \subseteq B \lor_{ℋ} C$
14	9 13	ssini	$⊢ (A \cap B) \lor_{ℋ} (A \cap C) \subseteq A \cap (B \lor_{ℋ} C)$

Metamath Proof Explorer