fh2

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

		Ref	Expression
	Assertion	fh2	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land (B 𝐶_{ℋ} A \land B 𝐶_{ℋ} 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 (B 𝐶_{ℋ} A \land B 𝐶_{ℋ} 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 (B 𝐶_{ℋ} A \land B 𝐶_{ℋ} C)) \to (A \cap B) \lor_{ℋ} (A \cap C) \subseteq A \cap (B \lor_{ℋ} C)$
16		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)$
17	1 2 16	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)$
18		chdmm1	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to ⊥ (A \cap B) = ⊥ (A) \lor_{ℋ} ⊥ (B)$
19	18	adantr	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land (A \in C_{ℋ} \land C \in C_{ℋ})) \to ⊥ (A \cap B) = ⊥ (A) \lor_{ℋ} ⊥ (B)$
20	19	ineq1d	$⊢ ((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 \cap C)$
21	17 20	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 \cap C)$
22	21	3impdi	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \to ⊥ ((A \cap B) \lor_{ℋ} (A \cap C)) = (⊥ (A) \lor_{ℋ} ⊥ (B)) \cap ⊥ (A \cap C)$
23	22	ineq2d	$⊢ (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)) = (A \cap (B \lor_{ℋ} C)) \cap ((⊥ (A) \lor_{ℋ} ⊥ (B)) \cap ⊥ (A \cap C))$
24	23	adantr	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land (B 𝐶_{ℋ} A \land B 𝐶_{ℋ} C)) \to (A \cap (B \lor_{ℋ} C)) \cap ⊥ ((A \cap B) \lor_{ℋ} (A \cap C)) = (A \cap (B \lor_{ℋ} C)) \cap ((⊥ (A) \lor_{ℋ} ⊥ (B)) \cap ⊥ (A \cap C))$
25		in4	$⊢ (A \cap (B \lor_{ℋ} C)) \cap ((⊥ (A) \lor_{ℋ} ⊥ (B)) \cap ⊥ (A \cap C)) = (A \cap (⊥ (A) \lor_{ℋ} ⊥ (B))) \cap ((B \lor_{ℋ} C) \cap ⊥ (A \cap C))$
26		cmcm2	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A 𝐶_{ℋ} B \leftrightarrow A 𝐶_{ℋ} ⊥ (B))$
27		cmcm	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A 𝐶_{ℋ} B \leftrightarrow B 𝐶_{ℋ} A)$
28		choccl	$⊢ B \in C_{ℋ} \to ⊥ (B) \in C_{ℋ}$
29		cmbr3	$⊢ (A \in C_{ℋ} \land ⊥ (B) \in C_{ℋ}) \to (A 𝐶_{ℋ} ⊥ (B) \leftrightarrow A \cap (⊥ (A) \lor_{ℋ} ⊥ (B)) = A \cap ⊥ (B))$
30	28 29	sylan2	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A 𝐶_{ℋ} ⊥ (B) \leftrightarrow A \cap (⊥ (A) \lor_{ℋ} ⊥ (B)) = A \cap ⊥ (B))$
31	26 27 30	3bitr3d	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (B 𝐶_{ℋ} A \leftrightarrow A \cap (⊥ (A) \lor_{ℋ} ⊥ (B)) = A \cap ⊥ (B))$
32	31	biimpa	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land B 𝐶_{ℋ} A) \to A \cap (⊥ (A) \lor_{ℋ} ⊥ (B)) = A \cap ⊥ (B)$
33		incom	$⊢ A \cap ⊥ (B) = ⊥ (B) \cap A$
34	32 33	eqtrdi	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land B 𝐶_{ℋ} A) \to A \cap (⊥ (A) \lor_{ℋ} ⊥ (B)) = ⊥ (B) \cap A$
35	34	3adantl3	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land B 𝐶_{ℋ} A) \to A \cap (⊥ (A) \lor_{ℋ} ⊥ (B)) = ⊥ (B) \cap A$
36	35	adantrr	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land (B 𝐶_{ℋ} A \land B 𝐶_{ℋ} C)) \to A \cap (⊥ (A) \lor_{ℋ} ⊥ (B)) = ⊥ (B) \cap A$
37	36	ineq1d	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land (B 𝐶_{ℋ} A \land B 𝐶_{ℋ} C)) \to (A \cap (⊥ (A) \lor_{ℋ} ⊥ (B))) \cap ((B \lor_{ℋ} C) \cap ⊥ (A \cap C)) = (⊥ (B) \cap A) \cap ((B \lor_{ℋ} C) \cap ⊥ (A \cap C))$
38	25 37	syl5eq	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land (B 𝐶_{ℋ} A \land B 𝐶_{ℋ} C)) \to (A \cap (B \lor_{ℋ} C)) \cap ((⊥ (A) \lor_{ℋ} ⊥ (B)) \cap ⊥ (A \cap C)) = (⊥ (B) \cap A) \cap ((B \lor_{ℋ} C) \cap ⊥ (A \cap C))$
39	24 38	eqtrd	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land (B 𝐶_{ℋ} A \land B 𝐶_{ℋ} C)) \to (A \cap (B \lor_{ℋ} C)) \cap ⊥ ((A \cap B) \lor_{ℋ} (A \cap C)) = (⊥ (B) \cap A) \cap ((B \lor_{ℋ} C) \cap ⊥ (A \cap C))$
40		in4	$⊢ (⊥ (B) \cap A) \cap ((B \lor_{ℋ} C) \cap ⊥ (A \cap C)) = (⊥ (B) \cap (B \lor_{ℋ} C)) \cap (A \cap ⊥ (A \cap C))$
41	39 40	eqtrdi	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land (B 𝐶_{ℋ} A \land B 𝐶_{ℋ} C)) \to (A \cap (B \lor_{ℋ} C)) \cap ⊥ ((A \cap B) \lor_{ℋ} (A \cap C)) = (⊥ (B) \cap (B \lor_{ℋ} C)) \cap (A \cap ⊥ (A \cap C))$
42		ococ	$⊢ B \in C_{ℋ} \to ⊥ (⊥ (B)) = B$
43	42	oveq1d	$⊢ B \in C_{ℋ} \to ⊥ (⊥ (B)) \lor_{ℋ} C = B \lor_{ℋ} C$
44	43	ineq2d	$⊢ B \in C_{ℋ} \to ⊥ (B) \cap (⊥ (⊥ (B)) \lor_{ℋ} C) = ⊥ (B) \cap (B \lor_{ℋ} C)$
45	44	3ad2ant2	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \to ⊥ (B) \cap (⊥ (⊥ (B)) \lor_{ℋ} C) = ⊥ (B) \cap (B \lor_{ℋ} C)$
46	45	adantr	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land (B 𝐶_{ℋ} A \land B 𝐶_{ℋ} C)) \to ⊥ (B) \cap (⊥ (⊥ (B)) \lor_{ℋ} C) = ⊥ (B) \cap (B \lor_{ℋ} C)$
47		cmcm3	$⊢ (B \in C_{ℋ} \land C \in C_{ℋ}) \to (B 𝐶_{ℋ} C \leftrightarrow ⊥ (B) 𝐶_{ℋ} C)$
48		cmbr3	$⊢ (⊥ (B) \in C_{ℋ} \land C \in C_{ℋ}) \to (⊥ (B) 𝐶_{ℋ} C \leftrightarrow ⊥ (B) \cap (⊥ (⊥ (B)) \lor_{ℋ} C) = ⊥ (B) \cap C)$
49	28 48	sylan	$⊢ (B \in C_{ℋ} \land C \in C_{ℋ}) \to (⊥ (B) 𝐶_{ℋ} C \leftrightarrow ⊥ (B) \cap (⊥ (⊥ (B)) \lor_{ℋ} C) = ⊥ (B) \cap C)$
50	47 49	bitrd	$⊢ (B \in C_{ℋ} \land C \in C_{ℋ}) \to (B 𝐶_{ℋ} C \leftrightarrow ⊥ (B) \cap (⊥ (⊥ (B)) \lor_{ℋ} C) = ⊥ (B) \cap C)$
51	50	biimpa	$⊢ ((B \in C_{ℋ} \land C \in C_{ℋ}) \land B 𝐶_{ℋ} C) \to ⊥ (B) \cap (⊥ (⊥ (B)) \lor_{ℋ} C) = ⊥ (B) \cap C$
52	51	3adantl1	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land B 𝐶_{ℋ} C) \to ⊥ (B) \cap (⊥ (⊥ (B)) \lor_{ℋ} C) = ⊥ (B) \cap C$
53	52	adantrl	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land (B 𝐶_{ℋ} A \land B 𝐶_{ℋ} C)) \to ⊥ (B) \cap (⊥ (⊥ (B)) \lor_{ℋ} C) = ⊥ (B) \cap C$
54	46 53	eqtr3d	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land (B 𝐶_{ℋ} A \land B 𝐶_{ℋ} C)) \to ⊥ (B) \cap (B \lor_{ℋ} C) = ⊥ (B) \cap C$
55	54	ineq1d	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land (B 𝐶_{ℋ} A \land B 𝐶_{ℋ} C)) \to (⊥ (B) \cap (B \lor_{ℋ} C)) \cap (A \cap ⊥ (A \cap C)) = (⊥ (B) \cap C) \cap (A \cap ⊥ (A \cap C))$
56		inass	$⊢ (⊥ (B) \cap C) \cap (A \cap ⊥ (A \cap C)) = ⊥ (B) \cap (C \cap (A \cap ⊥ (A \cap C)))$
57		in12	$⊢ C \cap (A \cap ⊥ (A \cap C)) = A \cap (C \cap ⊥ (A \cap C))$
58		inass	$⊢ (A \cap C) \cap ⊥ (A \cap C) = A \cap (C \cap ⊥ (A \cap C))$
59	57 58	eqtr4i	$⊢ C \cap (A \cap ⊥ (A \cap C)) = (A \cap C) \cap ⊥ (A \cap C)$
60		chocin	$⊢ A \cap C \in C_{ℋ} \to (A \cap C) \cap ⊥ (A \cap C) = 0_{ℋ}$
61	2 60	syl	$⊢ (A \in C_{ℋ} \land C \in C_{ℋ}) \to (A \cap C) \cap ⊥ (A \cap C) = 0_{ℋ}$
62	59 61	syl5eq	$⊢ (A \in C_{ℋ} \land C \in C_{ℋ}) \to C \cap (A \cap ⊥ (A \cap C)) = 0_{ℋ}$
63	62	ineq2d	$⊢ (A \in C_{ℋ} \land C \in C_{ℋ}) \to ⊥ (B) \cap (C \cap (A \cap ⊥ (A \cap C))) = ⊥ (B) \cap 0_{ℋ}$
64	56 63	syl5eq	$⊢ (A \in C_{ℋ} \land C \in C_{ℋ}) \to (⊥ (B) \cap C) \cap (A \cap ⊥ (A \cap C)) = ⊥ (B) \cap 0_{ℋ}$
65	64	3adant2	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \to (⊥ (B) \cap C) \cap (A \cap ⊥ (A \cap C)) = ⊥ (B) \cap 0_{ℋ}$
66		chm0	$⊢ ⊥ (B) \in C_{ℋ} \to ⊥ (B) \cap 0_{ℋ} = 0_{ℋ}$
67	28 66	syl	$⊢ B \in C_{ℋ} \to ⊥ (B) \cap 0_{ℋ} = 0_{ℋ}$
68	67	3ad2ant2	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \to ⊥ (B) \cap 0_{ℋ} = 0_{ℋ}$
69	65 68	eqtrd	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \to (⊥ (B) \cap C) \cap (A \cap ⊥ (A \cap C)) = 0_{ℋ}$
70	69	adantr	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land (B 𝐶_{ℋ} A \land B 𝐶_{ℋ} C)) \to (⊥ (B) \cap C) \cap (A \cap ⊥ (A \cap C)) = 0_{ℋ}$
71	55 70	eqtrd	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land (B 𝐶_{ℋ} A \land B 𝐶_{ℋ} C)) \to (⊥ (B) \cap (B \lor_{ℋ} C)) \cap (A \cap ⊥ (A \cap C)) = 0_{ℋ}$
72	41 71	eqtrd	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land (B 𝐶_{ℋ} A \land B 𝐶_{ℋ} C)) \to (A \cap (B \lor_{ℋ} C)) \cap ⊥ ((A \cap B) \lor_{ℋ} (A \cap C)) = 0_{ℋ}$
73		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)$
74	13 15 72 73	syl12anc	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land (B 𝐶_{ℋ} A \land B 𝐶_{ℋ} C)) \to (A \cap B) \lor_{ℋ} (A \cap C) = A \cap (B \lor_{ℋ} C)$
75	74	eqcomd	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \land (B 𝐶_{ℋ} A \land B 𝐶_{ℋ} C)) \to A \cap (B \lor_{ℋ} C) = (A \cap B) \lor_{ℋ} (A \cap C)$

Metamath Proof Explorer

Theorem fh2

Proof