fh1i

Description: Foulis-Holland Theorem. If any 2 pairs in a triple of orthomodular lattice elements commute, the triple is distributive. First of two parts. Theorem 5 of Kalmbach p. 25. (Contributed by NM, 7-Aug-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	fh1.1	$⊢ A \in C_{ℋ}$
	fh1.2	$⊢ B \in C_{ℋ}$
	fh1.3	$⊢ C \in C_{ℋ}$
	fh1.4	$⊢ A 𝐶_{ℋ} B$
	fh1.5	$⊢ A 𝐶_{ℋ} C$
Assertion	fh1i	$⊢ A \cap (B \lor_{ℋ} C) = (A \cap B) \lor_{ℋ} (A \cap C)$

Proof

Step	Hyp	Ref	Expression
1		fh1.1	$⊢ A \in C_{ℋ}$
2		fh1.2	$⊢ B \in C_{ℋ}$
3		fh1.3	$⊢ C \in C_{ℋ}$
4		fh1.4	$⊢ A 𝐶_{ℋ} B$
5		fh1.5	$⊢ A 𝐶_{ℋ} C$
6	1 2 3	3pm3.2i	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ})$
7	4 5	pm3.2i	$⊢ (A 𝐶_{ℋ} B \land A 𝐶_{ℋ} C)$
8		fh1	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land (A 𝐶_{ℋ} B \land A 𝐶_{ℋ} C)) \to A \cap (B \lor_{ℋ} C) = (A \cap B) \lor_{ℋ} (A \cap C)$
9	6 7 8	mp2an	$⊢ A \cap (B \lor_{ℋ} C) = (A \cap B) \lor_{ℋ} (A \cap C)$

Metamath Proof Explorer

Theorem fh1i

Proof