atomli

Description: An assertion holding in atomic orthomodular lattices that is equivalent to the exchange axiom. Proposition 3.2.17 of PtakPulmannova p. 66. (Contributed by NM, 24-Jun-2004) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	atoml.1	$⊢ A \in C_{ℋ}$
	Assertion	atomli	$⊢ B \in HAtoms \to (A \lor_{ℋ} B) \cap ⊥ (A) \in (HAtoms \cup \{0_{ℋ}\})$

Proof

Step	Hyp	Ref	Expression
1		atoml.1	$⊢ A \in C_{ℋ}$
2		atelch	$⊢ B \in HAtoms \to B \in C_{ℋ}$
3		chjcl	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to A \lor_{ℋ} B \in C_{ℋ}$
4	1 2 3	sylancr	$⊢ B \in HAtoms \to A \lor_{ℋ} B \in C_{ℋ}$
5	1	choccli	$⊢ ⊥ (A) \in C_{ℋ}$
6		chincl	$⊢ (A \lor_{ℋ} B \in C_{ℋ} \land ⊥ (A) \in C_{ℋ}) \to (A \lor_{ℋ} B) \cap ⊥ (A) \in C_{ℋ}$
7	4 5 6	sylancl	$⊢ B \in HAtoms \to (A \lor_{ℋ} B) \cap ⊥ (A) \in C_{ℋ}$
8		hatomic	$⊢ ((A \lor_{ℋ} B) \cap ⊥ (A) \in C_{ℋ} \land (A \lor_{ℋ} B) \cap ⊥ (A) \neq 0_{ℋ}) \to \exists x \in HAtoms x \subseteq (A \lor_{ℋ} B) \cap ⊥ (A)$
9	7 8	sylan	$⊢ (B \in HAtoms \land (A \lor_{ℋ} B) \cap ⊥ (A) \neq 0_{ℋ}) \to \exists x \in HAtoms x \subseteq (A \lor_{ℋ} B) \cap ⊥ (A)$
10		atelch	$⊢ x \in HAtoms \to x \in C_{ℋ}$
11		inss2	$⊢ (A \lor_{ℋ} B) \cap ⊥ (A) \subseteq ⊥ (A)$
12		sstr	$⊢ (x \subseteq (A \lor_{ℋ} B) \cap ⊥ (A) \land (A \lor_{ℋ} B) \cap ⊥ (A) \subseteq ⊥ (A)) \to x \subseteq ⊥ (A)$
13	11 12	mpan2	$⊢ x \subseteq (A \lor_{ℋ} B) \cap ⊥ (A) \to x \subseteq ⊥ (A)$
14	1	pjococi	$⊢ ⊥ (⊥ (A)) = A$
15	14	oveq1i	$⊢ ⊥ (⊥ (A)) \lor_{ℋ} x = A \lor_{ℋ} x$
16	15	ineq1i	$⊢ (⊥ (⊥ (A)) \lor_{ℋ} x) \cap ⊥ (A) = (A \lor_{ℋ} x) \cap ⊥ (A)$
17		incom	$⊢ (⊥ (⊥ (A)) \lor_{ℋ} x) \cap ⊥ (A) = ⊥ (A) \cap (⊥ (⊥ (A)) \lor_{ℋ} x)$
18	16 17	eqtr3i	$⊢ (A \lor_{ℋ} x) \cap ⊥ (A) = ⊥ (A) \cap (⊥ (⊥ (A)) \lor_{ℋ} x)$
19		pjoml3	$⊢ (⊥ (A) \in C_{ℋ} \land x \in C_{ℋ}) \to (x \subseteq ⊥ (A) \to ⊥ (A) \cap (⊥ (⊥ (A)) \lor_{ℋ} x) = x)$
20	5 19	mpan	$⊢ x \in C_{ℋ} \to (x \subseteq ⊥ (A) \to ⊥ (A) \cap (⊥ (⊥ (A)) \lor_{ℋ} x) = x)$
21	20	imp	$⊢ (x \in C_{ℋ} \land x \subseteq ⊥ (A)) \to ⊥ (A) \cap (⊥ (⊥ (A)) \lor_{ℋ} x) = x$
22	18 21	syl5eq	$⊢ (x \in C_{ℋ} \land x \subseteq ⊥ (A)) \to (A \lor_{ℋ} x) \cap ⊥ (A) = x$
23	10 13 22	syl2an	$⊢ (x \in HAtoms \land x \subseteq (A \lor_{ℋ} B) \cap ⊥ (A)) \to (A \lor_{ℋ} x) \cap ⊥ (A) = x$
24	23	ad2ant2lr	$⊢ ((B \in HAtoms \land x \in HAtoms) \land (x \subseteq (A \lor_{ℋ} B) \cap ⊥ (A) \land (A \lor_{ℋ} B) \cap ⊥ (A) \neq 0_{ℋ})) \to (A \lor_{ℋ} x) \cap ⊥ (A) = x$
25		inss1	$⊢ (A \lor_{ℋ} B) \cap ⊥ (A) \subseteq A \lor_{ℋ} B$
26		sstr	$⊢ (x \subseteq (A \lor_{ℋ} B) \cap ⊥ (A) \land (A \lor_{ℋ} B) \cap ⊥ (A) \subseteq A \lor_{ℋ} B) \to x \subseteq A \lor_{ℋ} B$
27	25 26	mpan2	$⊢ x \subseteq (A \lor_{ℋ} B) \cap ⊥ (A) \to x \subseteq A \lor_{ℋ} B$
28		chub1	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to A \subseteq A \lor_{ℋ} B$
29	1 28	mpan	$⊢ B \in C_{ℋ} \to A \subseteq A \lor_{ℋ} B$
30	29	adantr	$⊢ (B \in C_{ℋ} \land x \in C_{ℋ}) \to A \subseteq A \lor_{ℋ} B$
31	1 3	mpan	$⊢ B \in C_{ℋ} \to A \lor_{ℋ} B \in C_{ℋ}$
32		chlub	$⊢ (A \in C_{ℋ} \land x \in C_{ℋ} \land A \lor_{ℋ} B \in C_{ℋ}) \to ((A \subseteq A \lor_{ℋ} B \land x \subseteq A \lor_{ℋ} B) \leftrightarrow A \lor_{ℋ} x \subseteq A \lor_{ℋ} B)$
33	1 32	mp3an1	$⊢ (x \in C_{ℋ} \land A \lor_{ℋ} B \in C_{ℋ}) \to ((A \subseteq A \lor_{ℋ} B \land x \subseteq A \lor_{ℋ} B) \leftrightarrow A \lor_{ℋ} x \subseteq A \lor_{ℋ} B)$
34	31 33	sylan2	$⊢ (x \in C_{ℋ} \land B \in C_{ℋ}) \to ((A \subseteq A \lor_{ℋ} B \land x \subseteq A \lor_{ℋ} B) \leftrightarrow A \lor_{ℋ} x \subseteq A \lor_{ℋ} B)$
35	34	biimpd	$⊢ (x \in C_{ℋ} \land B \in C_{ℋ}) \to ((A \subseteq A \lor_{ℋ} B \land x \subseteq A \lor_{ℋ} B) \to A \lor_{ℋ} x \subseteq A \lor_{ℋ} B)$
36	35	ancoms	$⊢ (B \in C_{ℋ} \land x \in C_{ℋ}) \to ((A \subseteq A \lor_{ℋ} B \land x \subseteq A \lor_{ℋ} B) \to A \lor_{ℋ} x \subseteq A \lor_{ℋ} B)$
37	30 36	mpand	$⊢ (B \in C_{ℋ} \land x \in C_{ℋ}) \to (x \subseteq A \lor_{ℋ} B \to A \lor_{ℋ} x \subseteq A \lor_{ℋ} B)$
38	2 10 37	syl2an	$⊢ (B \in HAtoms \land x \in HAtoms) \to (x \subseteq A \lor_{ℋ} B \to A \lor_{ℋ} x \subseteq A \lor_{ℋ} B)$
39	38	imp	$⊢ ((B \in HAtoms \land x \in HAtoms) \land x \subseteq A \lor_{ℋ} B) \to A \lor_{ℋ} x \subseteq A \lor_{ℋ} B$
40	27 39	sylan2	$⊢ ((B \in HAtoms \land x \in HAtoms) \land x \subseteq (A \lor_{ℋ} B) \cap ⊥ (A)) \to A \lor_{ℋ} x \subseteq A \lor_{ℋ} B$
41	40	adantrr	$⊢ ((B \in HAtoms \land x \in HAtoms) \land (x \subseteq (A \lor_{ℋ} B) \cap ⊥ (A) \land (A \lor_{ℋ} B) \cap ⊥ (A) \neq 0_{ℋ})) \to A \lor_{ℋ} x \subseteq A \lor_{ℋ} B$
42		chjcl	$⊢ (A \in C_{ℋ} \land x \in C_{ℋ}) \to A \lor_{ℋ} x \in C_{ℋ}$
43	1 10 42	sylancr	$⊢ x \in HAtoms \to A \lor_{ℋ} x \in C_{ℋ}$
44	2 43	anim12i	$⊢ (B \in HAtoms \land x \in HAtoms) \to (B \in C_{ℋ} \land A \lor_{ℋ} x \in C_{ℋ})$
45	44	adantr	$⊢ ((B \in HAtoms \land x \in HAtoms) \land (x \subseteq (A \lor_{ℋ} B) \cap ⊥ (A) \land (A \lor_{ℋ} B) \cap ⊥ (A) \neq 0_{ℋ})) \to (B \in C_{ℋ} \land A \lor_{ℋ} x \in C_{ℋ})$
46		chub1	$⊢ (A \in C_{ℋ} \land x \in C_{ℋ}) \to A \subseteq A \lor_{ℋ} x$
47	1 10 46	sylancr	$⊢ x \in HAtoms \to A \subseteq A \lor_{ℋ} x$
48	47	ad2antlr	$⊢ ((B \in HAtoms \land x \in HAtoms) \land (x \subseteq (A \lor_{ℋ} B) \cap ⊥ (A) \land (A \lor_{ℋ} B) \cap ⊥ (A) \neq 0_{ℋ})) \to A \subseteq A \lor_{ℋ} x$
49		pm3.22	$⊢ (B \in HAtoms \land x \in HAtoms) \to (x \in HAtoms \land B \in HAtoms)$
50	49	adantr	$⊢ ((B \in HAtoms \land x \in HAtoms) \land (x \subseteq (A \lor_{ℋ} B) \cap ⊥ (A) \land (A \lor_{ℋ} B) \cap ⊥ (A) \neq 0_{ℋ})) \to (x \in HAtoms \land B \in HAtoms)$
51	27	adantl	$⊢ (x \in HAtoms \land x \subseteq (A \lor_{ℋ} B) \cap ⊥ (A)) \to x \subseteq A \lor_{ℋ} B$
52		incom	$⊢ A \cap x = x \cap A$
53		chsh	$⊢ x \in C_{ℋ} \to x \in S_{ℋ}$
54	1	chshii	$⊢ A \in S_{ℋ}$
55		orthin	$⊢ (x \in S_{ℋ} \land A \in S_{ℋ}) \to (x \subseteq ⊥ (A) \to x \cap A = 0_{ℋ})$
56	53 54 55	sylancl	$⊢ x \in C_{ℋ} \to (x \subseteq ⊥ (A) \to x \cap A = 0_{ℋ})$
57	56	imp	$⊢ (x \in C_{ℋ} \land x \subseteq ⊥ (A)) \to x \cap A = 0_{ℋ}$
58	52 57	syl5eq	$⊢ (x \in C_{ℋ} \land x \subseteq ⊥ (A)) \to A \cap x = 0_{ℋ}$
59	10 13 58	syl2an	$⊢ (x \in HAtoms \land x \subseteq (A \lor_{ℋ} B) \cap ⊥ (A)) \to A \cap x = 0_{ℋ}$
60	51 59	jca	$⊢ (x \in HAtoms \land x \subseteq (A \lor_{ℋ} B) \cap ⊥ (A)) \to (x \subseteq A \lor_{ℋ} B \land A \cap x = 0_{ℋ})$
61	60	ad2ant2lr	$⊢ ((B \in HAtoms \land x \in HAtoms) \land (x \subseteq (A \lor_{ℋ} B) \cap ⊥ (A) \land (A \lor_{ℋ} B) \cap ⊥ (A) \neq 0_{ℋ})) \to (x \subseteq A \lor_{ℋ} B \land A \cap x = 0_{ℋ})$
62		atexch	$⊢ (A \in C_{ℋ} \land x \in HAtoms \land B \in HAtoms) \to ((x \subseteq A \lor_{ℋ} B \land A \cap x = 0_{ℋ}) \to B \subseteq A \lor_{ℋ} x)$
63	1 62	mp3an1	$⊢ (x \in HAtoms \land B \in HAtoms) \to ((x \subseteq A \lor_{ℋ} B \land A \cap x = 0_{ℋ}) \to B \subseteq A \lor_{ℋ} x)$
64	50 61 63	sylc	$⊢ ((B \in HAtoms \land x \in HAtoms) \land (x \subseteq (A \lor_{ℋ} B) \cap ⊥ (A) \land (A \lor_{ℋ} B) \cap ⊥ (A) \neq 0_{ℋ})) \to B \subseteq A \lor_{ℋ} x$
65		chlub	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land A \lor_{ℋ} x \in C_{ℋ}) \to ((A \subseteq A \lor_{ℋ} x \land B \subseteq A \lor_{ℋ} x) \leftrightarrow A \lor_{ℋ} B \subseteq A \lor_{ℋ} x)$
66	1 65	mp3an1	$⊢ (B \in C_{ℋ} \land A \lor_{ℋ} x \in C_{ℋ}) \to ((A \subseteq A \lor_{ℋ} x \land B \subseteq A \lor_{ℋ} x) \leftrightarrow A \lor_{ℋ} B \subseteq A \lor_{ℋ} x)$
67	66	biimpd	$⊢ (B \in C_{ℋ} \land A \lor_{ℋ} x \in C_{ℋ}) \to ((A \subseteq A \lor_{ℋ} x \land B \subseteq A \lor_{ℋ} x) \to A \lor_{ℋ} B \subseteq A \lor_{ℋ} x)$
68	67	expd	$⊢ (B \in C_{ℋ} \land A \lor_{ℋ} x \in C_{ℋ}) \to (A \subseteq A \lor_{ℋ} x \to (B \subseteq A \lor_{ℋ} x \to A \lor_{ℋ} B \subseteq A \lor_{ℋ} x))$
69	45 48 64 68	syl3c	$⊢ ((B \in HAtoms \land x \in HAtoms) \land (x \subseteq (A \lor_{ℋ} B) \cap ⊥ (A) \land (A \lor_{ℋ} B) \cap ⊥ (A) \neq 0_{ℋ})) \to A \lor_{ℋ} B \subseteq A \lor_{ℋ} x$
70	41 69	eqssd	$⊢ ((B \in HAtoms \land x \in HAtoms) \land (x \subseteq (A \lor_{ℋ} B) \cap ⊥ (A) \land (A \lor_{ℋ} B) \cap ⊥ (A) \neq 0_{ℋ})) \to A \lor_{ℋ} x = A \lor_{ℋ} B$
71	70	ineq1d	$⊢ ((B \in HAtoms \land x \in HAtoms) \land (x \subseteq (A \lor_{ℋ} B) \cap ⊥ (A) \land (A \lor_{ℋ} B) \cap ⊥ (A) \neq 0_{ℋ})) \to (A \lor_{ℋ} x) \cap ⊥ (A) = (A \lor_{ℋ} B) \cap ⊥ (A)$
72	24 71	eqtr3d	$⊢ ((B \in HAtoms \land x \in HAtoms) \land (x \subseteq (A \lor_{ℋ} B) \cap ⊥ (A) \land (A \lor_{ℋ} B) \cap ⊥ (A) \neq 0_{ℋ})) \to x = (A \lor_{ℋ} B) \cap ⊥ (A)$
73	72	eleq1d	$⊢ ((B \in HAtoms \land x \in HAtoms) \land (x \subseteq (A \lor_{ℋ} B) \cap ⊥ (A) \land (A \lor_{ℋ} B) \cap ⊥ (A) \neq 0_{ℋ})) \to (x \in HAtoms \leftrightarrow (A \lor_{ℋ} B) \cap ⊥ (A) \in HAtoms)$
74	73	exp43	$⊢ B \in HAtoms \to (x \in HAtoms \to (x \subseteq (A \lor_{ℋ} B) \cap ⊥ (A) \to ((A \lor_{ℋ} B) \cap ⊥ (A) \neq 0_{ℋ} \to (x \in HAtoms \leftrightarrow (A \lor_{ℋ} B) \cap ⊥ (A) \in HAtoms))))$
75	74	com24	$⊢ B \in HAtoms \to ((A \lor_{ℋ} B) \cap ⊥ (A) \neq 0_{ℋ} \to (x \subseteq (A \lor_{ℋ} B) \cap ⊥ (A) \to (x \in HAtoms \to (x \in HAtoms \leftrightarrow (A \lor_{ℋ} B) \cap ⊥ (A) \in HAtoms))))$
76	75	imp31	$⊢ ((B \in HAtoms \land (A \lor_{ℋ} B) \cap ⊥ (A) \neq 0_{ℋ}) \land x \subseteq (A \lor_{ℋ} B) \cap ⊥ (A)) \to (x \in HAtoms \to (x \in HAtoms \leftrightarrow (A \lor_{ℋ} B) \cap ⊥ (A) \in HAtoms))$
77	76	ibd	$⊢ ((B \in HAtoms \land (A \lor_{ℋ} B) \cap ⊥ (A) \neq 0_{ℋ}) \land x \subseteq (A \lor_{ℋ} B) \cap ⊥ (A)) \to (x \in HAtoms \to (A \lor_{ℋ} B) \cap ⊥ (A) \in HAtoms)$
78	77	ex	$⊢ (B \in HAtoms \land (A \lor_{ℋ} B) \cap ⊥ (A) \neq 0_{ℋ}) \to (x \subseteq (A \lor_{ℋ} B) \cap ⊥ (A) \to (x \in HAtoms \to (A \lor_{ℋ} B) \cap ⊥ (A) \in HAtoms))$
79	78	com23	$⊢ (B \in HAtoms \land (A \lor_{ℋ} B) \cap ⊥ (A) \neq 0_{ℋ}) \to (x \in HAtoms \to (x \subseteq (A \lor_{ℋ} B) \cap ⊥ (A) \to (A \lor_{ℋ} B) \cap ⊥ (A) \in HAtoms))$
80	79	rexlimdv	$⊢ (B \in HAtoms \land (A \lor_{ℋ} B) \cap ⊥ (A) \neq 0_{ℋ}) \to (\exists x \in HAtoms x \subseteq (A \lor_{ℋ} B) \cap ⊥ (A) \to (A \lor_{ℋ} B) \cap ⊥ (A) \in HAtoms)$
81	9 80	mpd	$⊢ (B \in HAtoms \land (A \lor_{ℋ} B) \cap ⊥ (A) \neq 0_{ℋ}) \to (A \lor_{ℋ} B) \cap ⊥ (A) \in HAtoms$
82	81	ex	$⊢ B \in HAtoms \to ((A \lor_{ℋ} B) \cap ⊥ (A) \neq 0_{ℋ} \to (A \lor_{ℋ} B) \cap ⊥ (A) \in HAtoms)$
83	82	necon1bd	$⊢ B \in HAtoms \to (\neg (A \lor_{ℋ} B) \cap ⊥ (A) \in HAtoms \to (A \lor_{ℋ} B) \cap ⊥ (A) = 0_{ℋ})$
84	83	orrd	$⊢ B \in HAtoms \to ((A \lor_{ℋ} B) \cap ⊥ (A) \in HAtoms \lor (A \lor_{ℋ} B) \cap ⊥ (A) = 0_{ℋ})$
85		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_{ℋ}\})$
86		fvex	$⊢ ⊥ (A) \in V$
87	86	inex2	$⊢ (A \lor_{ℋ} B) \cap ⊥ (A) \in V$
88	87	elsn	$⊢ (A \lor_{ℋ} B) \cap ⊥ (A) \in \{0_{ℋ}\} \leftrightarrow (A \lor_{ℋ} B) \cap ⊥ (A) = 0_{ℋ}$
89	88	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_{ℋ})$
90	85 89	bitri	$⊢ (A \lor_{ℋ} B) \cap ⊥ (A) \in (HAtoms \cup \{0_{ℋ}\}) \leftrightarrow ((A \lor_{ℋ} B) \cap ⊥ (A) \in HAtoms \lor (A \lor_{ℋ} B) \cap ⊥ (A) = 0_{ℋ})$
91	84 90	sylibr	$⊢ B \in HAtoms \to (A \lor_{ℋ} B) \cap ⊥ (A) \in (HAtoms \cup \{0_{ℋ}\})$

Metamath Proof Explorer

Theorem atomli

Proof