atoml2i

Description: An assertion holding in atomic orthomodular lattices that is equivalent to the exchange axiom. Proposition P8(ii) of BeltramettiCassinelli1 p. 400. (Contributed by NM, 12-Jun-2006) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	atoml.1	$⊢ A \in C_{ℋ}$
	Assertion	atoml2i	$⊢ (B \in HAtoms \land \neg B \subseteq A) \to (A \lor_{ℋ} B) \cap ⊥ (A) \in HAtoms$

Proof

Step	Hyp	Ref	Expression
1		atoml.1	$⊢ A \in C_{ℋ}$
2		atelch	$⊢ B \in HAtoms \to B \in C_{ℋ}$
3		pjoml5	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to A \lor_{ℋ} (⊥ (A) \cap (A \lor_{ℋ} B)) = A \lor_{ℋ} B$
4	1 2 3	sylancr	$⊢ B \in HAtoms \to A \lor_{ℋ} (⊥ (A) \cap (A \lor_{ℋ} B)) = A \lor_{ℋ} B$
5		incom	$⊢ (A \lor_{ℋ} B) \cap ⊥ (A) = ⊥ (A) \cap (A \lor_{ℋ} B)$
6	5	eqeq1i	$⊢ (A \lor_{ℋ} B) \cap ⊥ (A) = 0_{ℋ} \leftrightarrow ⊥ (A) \cap (A \lor_{ℋ} B) = 0_{ℋ}$
7	6	biimpi	$⊢ (A \lor_{ℋ} B) \cap ⊥ (A) = 0_{ℋ} \to ⊥ (A) \cap (A \lor_{ℋ} B) = 0_{ℋ}$
8	7	oveq2d	$⊢ (A \lor_{ℋ} B) \cap ⊥ (A) = 0_{ℋ} \to A \lor_{ℋ} (⊥ (A) \cap (A \lor_{ℋ} B)) = A \lor_{ℋ} 0_{ℋ}$
9	1	chj0i	$⊢ A \lor_{ℋ} 0_{ℋ} = A$
10	8 9	syl6eq	$⊢ (A \lor_{ℋ} B) \cap ⊥ (A) = 0_{ℋ} \to A \lor_{ℋ} (⊥ (A) \cap (A \lor_{ℋ} B)) = A$
11	4 10	sylan9req	$⊢ (B \in HAtoms \land (A \lor_{ℋ} B) \cap ⊥ (A) = 0_{ℋ}) \to A \lor_{ℋ} B = A$
12	11	ex	$⊢ B \in HAtoms \to ((A \lor_{ℋ} B) \cap ⊥ (A) = 0_{ℋ} \to A \lor_{ℋ} B = A)$
13		chlejb2	$⊢ (B \in C_{ℋ} \land A \in C_{ℋ}) \to (B \subseteq A \leftrightarrow A \lor_{ℋ} B = A)$
14	2 1 13	sylancl	$⊢ B \in HAtoms \to (B \subseteq A \leftrightarrow A \lor_{ℋ} B = A)$
15	12 14	sylibrd	$⊢ B \in HAtoms \to ((A \lor_{ℋ} B) \cap ⊥ (A) = 0_{ℋ} \to B \subseteq A)$
16	15	con3d	$⊢ B \in HAtoms \to (\neg B \subseteq A \to \neg (A \lor_{ℋ} B) \cap ⊥ (A) = 0_{ℋ})$
17	1	atomli	$⊢ B \in HAtoms \to (A \lor_{ℋ} B) \cap ⊥ (A) \in (HAtoms \cup \{0_{ℋ}\})$
18		elun	$⊢ (A \lor_{ℋ} B) \cap ⊥ (A) \in (HAtoms \cup \{0_{ℋ}\}) \leftrightarrow ((A \lor_{ℋ} B) \cap ⊥ (A) \in HAtoms \lor (A \lor_{ℋ} B) \cap ⊥ (A) \in \{0_{ℋ}\})$
19		h0elch	$⊢ 0_{ℋ} \in C_{ℋ}$
20	19	elexi	$⊢ 0_{ℋ} \in V$
21	20	elsn2	$⊢ (A \lor_{ℋ} B) \cap ⊥ (A) \in \{0_{ℋ}\} \leftrightarrow (A \lor_{ℋ} B) \cap ⊥ (A) = 0_{ℋ}$
22	21	orbi2i	$⊢ ((A \lor_{ℋ} B) \cap ⊥ (A) \in HAtoms \lor (A \lor_{ℋ} B) \cap ⊥ (A) \in \{0_{ℋ}\}) \leftrightarrow ((A \lor_{ℋ} B) \cap ⊥ (A) \in HAtoms \lor (A \lor_{ℋ} B) \cap ⊥ (A) = 0_{ℋ})$
23		orcom	$⊢ ((A \lor_{ℋ} B) \cap ⊥ (A) \in HAtoms \lor (A \lor_{ℋ} B) \cap ⊥ (A) = 0_{ℋ}) \leftrightarrow ((A \lor_{ℋ} B) \cap ⊥ (A) = 0_{ℋ} \lor (A \lor_{ℋ} B) \cap ⊥ (A) \in HAtoms)$
24	18 22 23	3bitri	$⊢ (A \lor_{ℋ} B) \cap ⊥ (A) \in (HAtoms \cup \{0_{ℋ}\}) \leftrightarrow ((A \lor_{ℋ} B) \cap ⊥ (A) = 0_{ℋ} \lor (A \lor_{ℋ} B) \cap ⊥ (A) \in HAtoms)$
25	17 24	sylib	$⊢ B \in HAtoms \to ((A \lor_{ℋ} B) \cap ⊥ (A) = 0_{ℋ} \lor (A \lor_{ℋ} B) \cap ⊥ (A) \in HAtoms)$
26	25	ord	$⊢ B \in HAtoms \to (\neg (A \lor_{ℋ} B) \cap ⊥ (A) = 0_{ℋ} \to (A \lor_{ℋ} B) \cap ⊥ (A) \in HAtoms)$
27	16 26	syld	$⊢ B \in HAtoms \to (\neg B \subseteq A \to (A \lor_{ℋ} B) \cap ⊥ (A) \in HAtoms)$
28	27	imp	$⊢ (B \in HAtoms \land \neg B \subseteq A) \to (A \lor_{ℋ} B) \cap ⊥ (A) \in HAtoms$

Metamath Proof Explorer

Theorem atoml2i

Proof