atordi

Description: An ordering law for a Hilbert lattice atom and a commuting subspace. (Contributed by NM, 12-Jun-2006) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	atoml.1	$⊢ A \in C_{ℋ}$
	Assertion	atordi	$⊢ (B \in HAtoms \land A 𝐶_{ℋ} B) \to (B \subseteq A \lor B \subseteq ⊥ (A))$

Proof

Step	Hyp	Ref	Expression
1		atoml.1	$⊢ A \in C_{ℋ}$
2		atelch	$⊢ B \in HAtoms \to B \in C_{ℋ}$
3	1	choccli	$⊢ ⊥ (A) \in C_{ℋ}$
4		chincl	$⊢ (⊥ (A) \in C_{ℋ} \land B \in C_{ℋ}) \to ⊥ (A) \cap B \in C_{ℋ}$
5	3 4	mpan	$⊢ B \in C_{ℋ} \to ⊥ (A) \cap B \in C_{ℋ}$
6		chj0	$⊢ ⊥ (A) \cap B \in C_{ℋ} \to (⊥ (A) \cap B) \lor_{ℋ} 0_{ℋ} = ⊥ (A) \cap B$
7	5 6	syl	$⊢ B \in C_{ℋ} \to (⊥ (A) \cap B) \lor_{ℋ} 0_{ℋ} = ⊥ (A) \cap B$
8		incom	$⊢ ⊥ (A) \cap B = B \cap ⊥ (A)$
9	7 8	syl6eq	$⊢ B \in C_{ℋ} \to (⊥ (A) \cap B) \lor_{ℋ} 0_{ℋ} = B \cap ⊥ (A)$
10		h0elch	$⊢ 0_{ℋ} \in C_{ℋ}$
11		chjcom	$⊢ (⊥ (A) \cap B \in C_{ℋ} \land 0_{ℋ} \in C_{ℋ}) \to (⊥ (A) \cap B) \lor_{ℋ} 0_{ℋ} = 0_{ℋ} \lor_{ℋ} (⊥ (A) \cap B)$
12	5 10 11	sylancl	$⊢ B \in C_{ℋ} \to (⊥ (A) \cap B) \lor_{ℋ} 0_{ℋ} = 0_{ℋ} \lor_{ℋ} (⊥ (A) \cap B)$
13	9 12	eqtr3d	$⊢ B \in C_{ℋ} \to B \cap ⊥ (A) = 0_{ℋ} \lor_{ℋ} (⊥ (A) \cap B)$
14		incom	$⊢ ⊥ (A) \cap A = A \cap ⊥ (A)$
15	1	chocini	$⊢ A \cap ⊥ (A) = 0_{ℋ}$
16	14 15	eqtri	$⊢ ⊥ (A) \cap A = 0_{ℋ}$
17	16	oveq1i	$⊢ (⊥ (A) \cap A) \lor_{ℋ} (⊥ (A) \cap B) = 0_{ℋ} \lor_{ℋ} (⊥ (A) \cap B)$
18	13 17	syl6eqr	$⊢ B \in C_{ℋ} \to B \cap ⊥ (A) = (⊥ (A) \cap A) \lor_{ℋ} (⊥ (A) \cap B)$
19	18	adantr	$⊢ (B \in C_{ℋ} \land A 𝐶_{ℋ} B) \to B \cap ⊥ (A) = (⊥ (A) \cap A) \lor_{ℋ} (⊥ (A) \cap B)$
20	1	cmidi	$⊢ A 𝐶_{ℋ} A$
21	1 1 20	cmcm2ii	$⊢ A 𝐶_{ℋ} ⊥ (A)$
22		fh2	$⊢ ((⊥ (A) \in C_{ℋ} \land A \in C_{ℋ} \land B \in C_{ℋ}) \land (A 𝐶_{ℋ} ⊥ (A) \land A 𝐶_{ℋ} B)) \to ⊥ (A) \cap (A \lor_{ℋ} B) = (⊥ (A) \cap A) \lor_{ℋ} (⊥ (A) \cap B)$
23	21 22	mpanr1	$⊢ ((⊥ (A) \in C_{ℋ} \land A \in C_{ℋ} \land B \in C_{ℋ}) \land A 𝐶_{ℋ} B) \to ⊥ (A) \cap (A \lor_{ℋ} B) = (⊥ (A) \cap A) \lor_{ℋ} (⊥ (A) \cap B)$
24	1 23	mp3anl2	$⊢ ((⊥ (A) \in C_{ℋ} \land B \in C_{ℋ}) \land A 𝐶_{ℋ} B) \to ⊥ (A) \cap (A \lor_{ℋ} B) = (⊥ (A) \cap A) \lor_{ℋ} (⊥ (A) \cap B)$
25	3 24	mpanl1	$⊢ (B \in C_{ℋ} \land A 𝐶_{ℋ} B) \to ⊥ (A) \cap (A \lor_{ℋ} B) = (⊥ (A) \cap A) \lor_{ℋ} (⊥ (A) \cap B)$
26	19 25	eqtr4d	$⊢ (B \in C_{ℋ} \land A 𝐶_{ℋ} B) \to B \cap ⊥ (A) = ⊥ (A) \cap (A \lor_{ℋ} B)$
27	2 26	sylan	$⊢ (B \in HAtoms \land A 𝐶_{ℋ} B) \to B \cap ⊥ (A) = ⊥ (A) \cap (A \lor_{ℋ} B)$
28		incom	$⊢ ⊥ (A) \cap (A \lor_{ℋ} B) = (A \lor_{ℋ} B) \cap ⊥ (A)$
29	27 28	syl6eq	$⊢ (B \in HAtoms \land A 𝐶_{ℋ} B) \to B \cap ⊥ (A) = (A \lor_{ℋ} B) \cap ⊥ (A)$
30	29	adantr	$⊢ ((B \in HAtoms \land A 𝐶_{ℋ} B) \land \neg B \subseteq A) \to B \cap ⊥ (A) = (A \lor_{ℋ} B) \cap ⊥ (A)$
31	1	atoml2i	$⊢ (B \in HAtoms \land \neg B \subseteq A) \to (A \lor_{ℋ} B) \cap ⊥ (A) \in HAtoms$
32	31	adantlr	$⊢ ((B \in HAtoms \land A 𝐶_{ℋ} B) \land \neg B \subseteq A) \to (A \lor_{ℋ} B) \cap ⊥ (A) \in HAtoms$
33	30 32	eqeltrd	$⊢ ((B \in HAtoms \land A 𝐶_{ℋ} B) \land \neg B \subseteq A) \to B \cap ⊥ (A) \in HAtoms$
34		atssma	$⊢ (B \in HAtoms \land ⊥ (A) \in C_{ℋ}) \to (B \subseteq ⊥ (A) \leftrightarrow B \cap ⊥ (A) \in HAtoms)$
35	3 34	mpan2	$⊢ B \in HAtoms \to (B \subseteq ⊥ (A) \leftrightarrow B \cap ⊥ (A) \in HAtoms)$
36	35	ad2antrr	$⊢ ((B \in HAtoms \land A 𝐶_{ℋ} B) \land \neg B \subseteq A) \to (B \subseteq ⊥ (A) \leftrightarrow B \cap ⊥ (A) \in HAtoms)$
37	33 36	mpbird	$⊢ ((B \in HAtoms \land A 𝐶_{ℋ} B) \land \neg B \subseteq A) \to B \subseteq ⊥ (A)$
38	37	ex	$⊢ (B \in HAtoms \land A 𝐶_{ℋ} B) \to (\neg B \subseteq A \to B \subseteq ⊥ (A))$
39	38	orrd	$⊢ (B \in HAtoms \land A 𝐶_{ℋ} B) \to (B \subseteq A \lor B \subseteq ⊥ (A))$

Metamath Proof Explorer

Theorem atordi

Proof