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

Step	Hyp	Ref	Expression
1		ledi.1	$⊢ A \in C_{ℋ}$
2		ledi.2	$⊢ B \in C_{ℋ}$
3		ledi.3	$⊢ C \in C_{ℋ}$
4	3 1 2	ledii	$⊢ (C \cap A) \lor_{ℋ} (C \cap B) \subseteq C \cap (A \lor_{ℋ} B)$
5		incom	$⊢ A \cap C = C \cap A$
6		incom	$⊢ B \cap C = C \cap B$
7	5 6	oveq12i	$⊢ (A \cap C) \lor_{ℋ} (B \cap C) = (C \cap A) \lor_{ℋ} (C \cap B)$
8		incom	$⊢ (A \lor_{ℋ} B) \cap C = C \cap (A \lor_{ℋ} B)$
9	4 7 8	3sstr4i	$⊢ (A \cap C) \lor_{ℋ} (B \cap C) \subseteq (A \lor_{ℋ} B) \cap C$

Metamath Proof Explorer