fh1

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, 14-Jun-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	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)$

Proof

Step	Hyp	Ref	Expression
1		chincl	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to A \cap B \in C_{ℋ}$
2		chincl	$⊢ (A \in C_{ℋ} \land C \in C_{ℋ}) \to A \cap C \in C_{ℋ}$
3		chjcl	$⊢ (A \cap B \in C_{ℋ} \land A \cap C \in C_{ℋ}) \to (A \cap B) \lor_{ℋ} (A \cap C) \in C_{ℋ}$
4	1 2 3	syl2an	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land (A \in C_{ℋ} \land C \in C_{ℋ})) \to (A \cap B) \lor_{ℋ} (A \cap C) \in C_{ℋ}$
5	4	anandis	$⊢ (A \in C_{ℋ} \land (B \in C_{ℋ} \land C \in C_{ℋ})) \to (A \cap B) \lor_{ℋ} (A \cap C) \in C_{ℋ}$
6		chjcl	$⊢ (B \in C_{ℋ} \land C \in C_{ℋ}) \to B \lor_{ℋ} C \in C_{ℋ}$
7		chincl	$⊢ (A \in C_{ℋ} \land B \lor_{ℋ} C \in C_{ℋ}) \to A \cap (B \lor_{ℋ} C) \in C_{ℋ}$
8	6 7	sylan2	$⊢ (A \in C_{ℋ} \land (B \in C_{ℋ} \land C \in C_{ℋ})) \to A \cap (B \lor_{ℋ} C) \in C_{ℋ}$
9		chsh	$⊢ A \cap (B \lor_{ℋ} C) \in C_{ℋ} \to A \cap (B \lor_{ℋ} C) \in S_{ℋ}$
10	8 9	syl	$⊢ (A \in C_{ℋ} \land (B \in C_{ℋ} \land C \in C_{ℋ})) \to A \cap (B \lor_{ℋ} C) \in S_{ℋ}$
11	5 10	jca	$⊢ (A \in C_{ℋ} \land (B \in C_{ℋ} \land C \in C_{ℋ})) \to ((A \cap B) \lor_{ℋ} (A \cap C) \in C_{ℋ} \land A \cap (B \lor_{ℋ} C) \in S_{ℋ})$
12	11	3impb	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \to ((A \cap B) \lor_{ℋ} (A \cap C) \in C_{ℋ} \land A \cap (B \lor_{ℋ} C) \in S_{ℋ})$
13	12	adantr	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land (A 𝐶_{ℋ} B \land A 𝐶_{ℋ} C)) \to ((A \cap B) \lor_{ℋ} (A \cap C) \in C_{ℋ} \land A \cap (B \lor_{ℋ} C) \in S_{ℋ})$
14		ledi	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \to (A \cap B) \lor_{ℋ} (A \cap C) \subseteq A \cap (B \lor_{ℋ} C)$
15	14	adantr	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land (A 𝐶_{ℋ} B \land A 𝐶_{ℋ} C)) \to (A \cap B) \lor_{ℋ} (A \cap C) \subseteq A \cap (B \lor_{ℋ} C)$
16		incom	$⊢ A \cap (B \lor_{ℋ} C) = (B \lor_{ℋ} C) \cap A$
17	16	a1i	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land (A \in C_{ℋ} \land C \in C_{ℋ})) \to A \cap (B \lor_{ℋ} C) = (B \lor_{ℋ} C) \cap A$
18		chdmj1	$⊢ (A \cap B \in C_{ℋ} \land A \cap C \in C_{ℋ}) \to ⊥ ((A \cap B) \lor_{ℋ} (A \cap C)) = ⊥ (A \cap B) \cap ⊥ (A \cap C)$
19	1 2 18	syl2an	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land (A \in C_{ℋ} \land C \in C_{ℋ})) \to ⊥ ((A \cap B) \lor_{ℋ} (A \cap C)) = ⊥ (A \cap B) \cap ⊥ (A \cap C)$
20		chdmm1	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to ⊥ (A \cap B) = ⊥ (A) \lor_{ℋ} ⊥ (B)$
21		chdmm1	$⊢ (A \in C_{ℋ} \land C \in C_{ℋ}) \to ⊥ (A \cap C) = ⊥ (A) \lor_{ℋ} ⊥ (C)$
22	20 21	ineqan12d	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land (A \in C_{ℋ} \land C \in C_{ℋ})) \to ⊥ (A \cap B) \cap ⊥ (A \cap C) = (⊥ (A) \lor_{ℋ} ⊥ (B)) \cap (⊥ (A) \lor_{ℋ} ⊥ (C))$
23	19 22	eqtrd	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land (A \in C_{ℋ} \land C \in C_{ℋ})) \to ⊥ ((A \cap B) \lor_{ℋ} (A \cap C)) = (⊥ (A) \lor_{ℋ} ⊥ (B)) \cap (⊥ (A) \lor_{ℋ} ⊥ (C))$
24	17 23	ineq12d	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land (A \in C_{ℋ} \land C \in C_{ℋ})) \to (A \cap (B \lor_{ℋ} C)) \cap ⊥ ((A \cap B) \lor_{ℋ} (A \cap C)) = ((B \lor_{ℋ} C) \cap A) \cap ((⊥ (A) \lor_{ℋ} ⊥ (B)) \cap (⊥ (A) \lor_{ℋ} ⊥ (C)))$
25	24	3impdi	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \to (A \cap (B \lor_{ℋ} C)) \cap ⊥ ((A \cap B) \lor_{ℋ} (A \cap C)) = ((B \lor_{ℋ} C) \cap A) \cap ((⊥ (A) \lor_{ℋ} ⊥ (B)) \cap (⊥ (A) \lor_{ℋ} ⊥ (C)))$
26	25	adantr	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land (A 𝐶_{ℋ} B \land A 𝐶_{ℋ} C)) \to (A \cap (B \lor_{ℋ} C)) \cap ⊥ ((A \cap B) \lor_{ℋ} (A \cap C)) = ((B \lor_{ℋ} C) \cap A) \cap ((⊥ (A) \lor_{ℋ} ⊥ (B)) \cap (⊥ (A) \lor_{ℋ} ⊥ (C)))$
27		inass	$⊢ ((B \lor_{ℋ} C) \cap A) \cap ((⊥ (A) \lor_{ℋ} ⊥ (B)) \cap (⊥ (A) \lor_{ℋ} ⊥ (C))) = (B \lor_{ℋ} C) \cap (A \cap ((⊥ (A) \lor_{ℋ} ⊥ (B)) \cap (⊥ (A) \lor_{ℋ} ⊥ (C))))$
28		cmcm2	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A 𝐶_{ℋ} B \leftrightarrow A 𝐶_{ℋ} ⊥ (B))$
29		choccl	$⊢ B \in C_{ℋ} \to ⊥ (B) \in C_{ℋ}$
30		cmbr3	$⊢ (A \in C_{ℋ} \land ⊥ (B) \in C_{ℋ}) \to (A 𝐶_{ℋ} ⊥ (B) \leftrightarrow A \cap (⊥ (A) \lor_{ℋ} ⊥ (B)) = A \cap ⊥ (B))$
31	29 30	sylan2	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A 𝐶_{ℋ} ⊥ (B) \leftrightarrow A \cap (⊥ (A) \lor_{ℋ} ⊥ (B)) = A \cap ⊥ (B))$
32	28 31	bitrd	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A 𝐶_{ℋ} B \leftrightarrow A \cap (⊥ (A) \lor_{ℋ} ⊥ (B)) = A \cap ⊥ (B))$
33	32	biimpa	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land A 𝐶_{ℋ} B) \to A \cap (⊥ (A) \lor_{ℋ} ⊥ (B)) = A \cap ⊥ (B)$
34	33	3adantl3	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land A 𝐶_{ℋ} B) \to A \cap (⊥ (A) \lor_{ℋ} ⊥ (B)) = A \cap ⊥ (B)$
35	34	adantrr	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land (A 𝐶_{ℋ} B \land A 𝐶_{ℋ} C)) \to A \cap (⊥ (A) \lor_{ℋ} ⊥ (B)) = A \cap ⊥ (B)$
36		cmcm2	$⊢ (A \in C_{ℋ} \land C \in C_{ℋ}) \to (A 𝐶_{ℋ} C \leftrightarrow A 𝐶_{ℋ} ⊥ (C))$
37		choccl	$⊢ C \in C_{ℋ} \to ⊥ (C) \in C_{ℋ}$
38		cmbr3	$⊢ (A \in C_{ℋ} \land ⊥ (C) \in C_{ℋ}) \to (A 𝐶_{ℋ} ⊥ (C) \leftrightarrow A \cap (⊥ (A) \lor_{ℋ} ⊥ (C)) = A \cap ⊥ (C))$
39	37 38	sylan2	$⊢ (A \in C_{ℋ} \land C \in C_{ℋ}) \to (A 𝐶_{ℋ} ⊥ (C) \leftrightarrow A \cap (⊥ (A) \lor_{ℋ} ⊥ (C)) = A \cap ⊥ (C))$
40	36 39	bitrd	$⊢ (A \in C_{ℋ} \land C \in C_{ℋ}) \to (A 𝐶_{ℋ} C \leftrightarrow A \cap (⊥ (A) \lor_{ℋ} ⊥ (C)) = A \cap ⊥ (C))$
41	40	biimpa	$⊢ ((A \in C_{ℋ} \land C \in C_{ℋ}) \land A 𝐶_{ℋ} C) \to A \cap (⊥ (A) \lor_{ℋ} ⊥ (C)) = A \cap ⊥ (C)$
42	41	3adantl2	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land A 𝐶_{ℋ} C) \to A \cap (⊥ (A) \lor_{ℋ} ⊥ (C)) = A \cap ⊥ (C)$
43	42	adantrl	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land (A 𝐶_{ℋ} B \land A 𝐶_{ℋ} C)) \to A \cap (⊥ (A) \lor_{ℋ} ⊥ (C)) = A \cap ⊥ (C)$
44	35 43	ineq12d	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land (A 𝐶_{ℋ} B \land A 𝐶_{ℋ} C)) \to (A \cap (⊥ (A) \lor_{ℋ} ⊥ (B))) \cap (A \cap (⊥ (A) \lor_{ℋ} ⊥ (C))) = (A \cap ⊥ (B)) \cap (A \cap ⊥ (C))$
45		inindi	$⊢ A \cap ((⊥ (A) \lor_{ℋ} ⊥ (B)) \cap (⊥ (A) \lor_{ℋ} ⊥ (C))) = (A \cap (⊥ (A) \lor_{ℋ} ⊥ (B))) \cap (A \cap (⊥ (A) \lor_{ℋ} ⊥ (C)))$
46		inindi	$⊢ A \cap (⊥ (B) \cap ⊥ (C)) = (A \cap ⊥ (B)) \cap (A \cap ⊥ (C))$
47	44 45 46	3eqtr4g	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land (A 𝐶_{ℋ} B \land A 𝐶_{ℋ} C)) \to A \cap ((⊥ (A) \lor_{ℋ} ⊥ (B)) \cap (⊥ (A) \lor_{ℋ} ⊥ (C))) = A \cap (⊥ (B) \cap ⊥ (C))$
48	47	ineq2d	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land (A 𝐶_{ℋ} B \land A 𝐶_{ℋ} C)) \to (B \lor_{ℋ} C) \cap (A \cap ((⊥ (A) \lor_{ℋ} ⊥ (B)) \cap (⊥ (A) \lor_{ℋ} ⊥ (C)))) = (B \lor_{ℋ} C) \cap (A \cap (⊥ (B) \cap ⊥ (C)))$
49	27 48	syl5eq	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land (A 𝐶_{ℋ} B \land A 𝐶_{ℋ} C)) \to ((B \lor_{ℋ} C) \cap A) \cap ((⊥ (A) \lor_{ℋ} ⊥ (B)) \cap (⊥ (A) \lor_{ℋ} ⊥ (C))) = (B \lor_{ℋ} C) \cap (A \cap (⊥ (B) \cap ⊥ (C)))$
50		in12	$⊢ (B \lor_{ℋ} C) \cap (A \cap (⊥ (B) \cap ⊥ (C))) = A \cap ((B \lor_{ℋ} C) \cap (⊥ (B) \cap ⊥ (C)))$
51	49 50	eqtrdi	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land (A 𝐶_{ℋ} B \land A 𝐶_{ℋ} C)) \to ((B \lor_{ℋ} C) \cap A) \cap ((⊥ (A) \lor_{ℋ} ⊥ (B)) \cap (⊥ (A) \lor_{ℋ} ⊥ (C))) = A \cap ((B \lor_{ℋ} C) \cap (⊥ (B) \cap ⊥ (C)))$
52		chdmj1	$⊢ (B \in C_{ℋ} \land C \in C_{ℋ}) \to ⊥ (B \lor_{ℋ} C) = ⊥ (B) \cap ⊥ (C)$
53	52	ineq2d	$⊢ (B \in C_{ℋ} \land C \in C_{ℋ}) \to (B \lor_{ℋ} C) \cap ⊥ (B \lor_{ℋ} C) = (B \lor_{ℋ} C) \cap (⊥ (B) \cap ⊥ (C))$
54		chocin	$⊢ B \lor_{ℋ} C \in C_{ℋ} \to (B \lor_{ℋ} C) \cap ⊥ (B \lor_{ℋ} C) = 0_{ℋ}$
55	6 54	syl	$⊢ (B \in C_{ℋ} \land C \in C_{ℋ}) \to (B \lor_{ℋ} C) \cap ⊥ (B \lor_{ℋ} C) = 0_{ℋ}$
56	53 55	eqtr3d	$⊢ (B \in C_{ℋ} \land C \in C_{ℋ}) \to (B \lor_{ℋ} C) \cap (⊥ (B) \cap ⊥ (C)) = 0_{ℋ}$
57	56	ineq2d	$⊢ (B \in C_{ℋ} \land C \in C_{ℋ}) \to A \cap ((B \lor_{ℋ} C) \cap (⊥ (B) \cap ⊥ (C))) = A \cap 0_{ℋ}$
58		chm0	$⊢ A \in C_{ℋ} \to A \cap 0_{ℋ} = 0_{ℋ}$
59	57 58	sylan9eqr	$⊢ (A \in C_{ℋ} \land (B \in C_{ℋ} \land C \in C_{ℋ})) \to A \cap ((B \lor_{ℋ} C) \cap (⊥ (B) \cap ⊥ (C))) = 0_{ℋ}$
60	59	3impb	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \to A \cap ((B \lor_{ℋ} C) \cap (⊥ (B) \cap ⊥ (C))) = 0_{ℋ}$
61	60	adantr	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land (A 𝐶_{ℋ} B \land A 𝐶_{ℋ} C)) \to A \cap ((B \lor_{ℋ} C) \cap (⊥ (B) \cap ⊥ (C))) = 0_{ℋ}$
62	51 61	eqtrd	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land (A 𝐶_{ℋ} B \land A 𝐶_{ℋ} C)) \to ((B \lor_{ℋ} C) \cap A) \cap ((⊥ (A) \lor_{ℋ} ⊥ (B)) \cap (⊥ (A) \lor_{ℋ} ⊥ (C))) = 0_{ℋ}$
63	26 62	eqtrd	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land (A 𝐶_{ℋ} B \land A 𝐶_{ℋ} C)) \to (A \cap (B \lor_{ℋ} C)) \cap ⊥ ((A \cap B) \lor_{ℋ} (A \cap C)) = 0_{ℋ}$
64		pjoml	$⊢ (((A \cap B) \lor_{ℋ} (A \cap C) \in C_{ℋ} \land A \cap (B \lor_{ℋ} C) \in S_{ℋ}) \land ((A \cap B) \lor_{ℋ} (A \cap C) \subseteq A \cap (B \lor_{ℋ} C) \land (A \cap (B \lor_{ℋ} C)) \cap ⊥ ((A \cap B) \lor_{ℋ} (A \cap C)) = 0_{ℋ})) \to (A \cap B) \lor_{ℋ} (A \cap C) = A \cap (B \lor_{ℋ} C)$
65	13 15 63 64	syl12anc	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land (A 𝐶_{ℋ} B \land A 𝐶_{ℋ} C)) \to (A \cap B) \lor_{ℋ} (A \cap C) = A \cap (B \lor_{ℋ} C)$
66	65	eqcomd	$⊢ ((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)$

Metamath Proof Explorer

Theorem fh1

Proof