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

Proof

Step	Hyp	Ref	Expression
1		ledi.1	$⊢ A \in C_{ℋ}$
2		ledi.2	$⊢ B \in C_{ℋ}$
3		ledi.3	$⊢ C \in C_{ℋ}$
4	1 2	chub1i	$⊢ A \subseteq A \lor_{ℋ} B$
5	1 3	chub1i	$⊢ A \subseteq A \lor_{ℋ} C$
6	4 5	ssini	$⊢ A \subseteq (A \lor_{ℋ} B) \cap (A \lor_{ℋ} C)$
7		inss1	$⊢ B \cap C \subseteq B$
8	2 1	chub2i	$⊢ B \subseteq A \lor_{ℋ} B$
9	7 8	sstri	$⊢ B \cap C \subseteq A \lor_{ℋ} B$
10		inss2	$⊢ B \cap C \subseteq C$
11	3 1	chub2i	$⊢ C \subseteq A \lor_{ℋ} C$
12	10 11	sstri	$⊢ B \cap C \subseteq A \lor_{ℋ} C$
13	9 12	ssini	$⊢ B \cap C \subseteq (A \lor_{ℋ} B) \cap (A \lor_{ℋ} C)$
14	2 3	chincli	$⊢ B \cap C \in C_{ℋ}$
15	1 2	chjcli	$⊢ A \lor_{ℋ} B \in C_{ℋ}$
16	1 3	chjcli	$⊢ A \lor_{ℋ} C \in C_{ℋ}$
17	15 16	chincli	$⊢ (A \lor_{ℋ} B) \cap (A \lor_{ℋ} C) \in C_{ℋ}$
18	1 14 17	chlubi	$⊢ (A \subseteq (A \lor_{ℋ} B) \cap (A \lor_{ℋ} C) \land B \cap C \subseteq (A \lor_{ℋ} B) \cap (A \lor_{ℋ} C)) \leftrightarrow A \lor_{ℋ} (B \cap C) \subseteq (A \lor_{ℋ} B) \cap (A \lor_{ℋ} C)$
19	18	bicomi	$⊢ A \lor_{ℋ} (B \cap C) \subseteq (A \lor_{ℋ} B) \cap (A \lor_{ℋ} C) \leftrightarrow (A \subseteq (A \lor_{ℋ} B) \cap (A \lor_{ℋ} C) \land B \cap C \subseteq (A \lor_{ℋ} B) \cap (A \lor_{ℋ} C))$
20	6 13 19	mpbir2an	$⊢ A \lor_{ℋ} (B \cap C) \subseteq (A \lor_{ℋ} B) \cap (A \lor_{ℋ} C)$

Metamath Proof Explorer

Theorem lejdii

Proof