atlatmstc

Description: An atomic, complete, orthomodular lattice is atomistic i.e. every element is the join of the atoms under it. See remark before Proposition 1 in Kalmbach p. 140; also remark in BeltramettiCassinelli p. 98. ( hatomistici analog.) (Contributed by NM, 5-Nov-2012)

	Ref	Expression
Hypotheses	atlatmstc.b	$⊢ B = {Base}_{K}$
	atlatmstc.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	atlatmstc.u	$⊢ \underset{˙}{1} = lub (K)$
	atlatmstc.a	$⊢ A = Atoms (K)$
Assertion	atlatmstc	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \to \underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}) = X$

Proof

Step	Hyp	Ref	Expression
1		atlatmstc.b	$⊢ B = {Base}_{K}$
2		atlatmstc.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		atlatmstc.u	$⊢ \underset{˙}{1} = lub (K)$
4		atlatmstc.a	$⊢ A = Atoms (K)$
5		simpl2	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \to K \in CLat$
6		ssrab2	$⊢ \{y \in B \| y \underset{˙}{\leq} X\} \subseteq B$
7	1 4	atssbase	$⊢ A \subseteq B$
8		rabss2	$⊢ A \subseteq B \to \{y \in A \| y \underset{˙}{\leq} X\} \subseteq \{y \in B \| y \underset{˙}{\leq} X\}$
9	7 8	ax-mp	$⊢ \{y \in A \| y \underset{˙}{\leq} X\} \subseteq \{y \in B \| y \underset{˙}{\leq} X\}$
10	1 2 3	lubss	$⊢ (K \in CLat \land \{y \in B \| y \underset{˙}{\leq} X\} \subseteq B \land \{y \in A \| y \underset{˙}{\leq} X\} \subseteq \{y \in B \| y \underset{˙}{\leq} X\}) \to \underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}) \underset{˙}{\leq} \underset{˙}{1} (\{y \in B \| y \underset{˙}{\leq} X\})$
11	6 9 10	mp3an23	$⊢ K \in CLat \to \underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}) \underset{˙}{\leq} \underset{˙}{1} (\{y \in B \| y \underset{˙}{\leq} X\})$
12	5 11	syl	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \to \underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}) \underset{˙}{\leq} \underset{˙}{1} (\{y \in B \| y \underset{˙}{\leq} X\})$
13		atlpos	$⊢ K \in AtLat \to K \in Poset$
14	13	3ad2ant3	$⊢ (K \in OML \land K \in CLat \land K \in AtLat) \to K \in Poset$
15		simpl	$⊢ (K \in Poset \land X \in B) \to K \in Poset$
16		simpr	$⊢ (K \in Poset \land X \in B) \to X \in B$
17	1 2 3 15 16	lubid	$⊢ (K \in Poset \land X \in B) \to \underset{˙}{1} (\{y \in B \| y \underset{˙}{\leq} X\}) = X$
18	14 17	sylan	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \to \underset{˙}{1} (\{y \in B \| y \underset{˙}{\leq} X\}) = X$
19	12 18	breqtrd	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \to \underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}) \underset{˙}{\leq} X$
20		breq1	$⊢ y = x \to (y \underset{˙}{\leq} X \leftrightarrow x \underset{˙}{\leq} X)$
21	20	elrab	$⊢ x \in \{y \in A \| y \underset{˙}{\leq} X\} \leftrightarrow (x \in A \land x \underset{˙}{\leq} X)$
22		simpll2	$⊢ (((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \land x \in \{y \in A \| y \underset{˙}{\leq} X\}) \to K \in CLat$
23		ssrab2	$⊢ \{y \in A \| y \underset{˙}{\leq} X\} \subseteq A$
24	23 7	sstri	$⊢ \{y \in A \| y \underset{˙}{\leq} X\} \subseteq B$
25	1 2 3	lubel	$⊢ (K \in CLat \land x \in \{y \in A \| y \underset{˙}{\leq} X\} \land \{y \in A \| y \underset{˙}{\leq} X\} \subseteq B) \to x \underset{˙}{\leq} \underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})$
26	24 25	mp3an3	$⊢ (K \in CLat \land x \in \{y \in A \| y \underset{˙}{\leq} X\}) \to x \underset{˙}{\leq} \underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})$
27	22 26	sylancom	$⊢ (((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \land x \in \{y \in A \| y \underset{˙}{\leq} X\}) \to x \underset{˙}{\leq} \underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})$
28	27	ex	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \to (x \in \{y \in A \| y \underset{˙}{\leq} X\} \to x \underset{˙}{\leq} \underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}))$
29	21 28	syl5bir	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \to ((x \in A \land x \underset{˙}{\leq} X) \to x \underset{˙}{\leq} \underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}))$
30	29	expdimp	$⊢ (((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \land x \in A) \to (x \underset{˙}{\leq} X \to x \underset{˙}{\leq} \underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}))$
31		simpll3	$⊢ (((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \land x \in A) \to K \in AtLat$
32		eqid	$⊢ 0. (K) = 0. (K)$
33	32 4	atn0	$⊢ (K \in AtLat \land x \in A) \to x \neq 0. (K)$
34	31 33	sylancom	$⊢ (((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \land x \in A) \to x \neq 0. (K)$
35	34	adantr	$⊢ ((((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \land x \in A) \land x \underset{˙}{\leq} \underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})) \to x \neq 0. (K)$
36		simpl3	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \to K \in AtLat$
37		atllat	$⊢ K \in AtLat \to K \in Lat$
38	36 37	syl	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \to K \in Lat$
39	38	adantr	$⊢ (((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \land x \in A) \to K \in Lat$
40	1 4	atbase	$⊢ x \in A \to x \in B$
41	40	adantl	$⊢ (((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \land x \in A) \to x \in B$
42	1 3	clatlubcl	$⊢ (K \in CLat \land \{y \in A \| y \underset{˙}{\leq} X\} \subseteq B) \to \underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}) \in B$
43	5 24 42	sylancl	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \to \underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}) \in B$
44	43	adantr	$⊢ (((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \land x \in A) \to \underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}) \in B$
45		simpl1	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \to K \in OML$
46		omlop	$⊢ K \in OML \to K \in OP$
47	45 46	syl	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \to K \in OP$
48		eqid	$⊢ oc (K) = oc (K)$
49	1 48	opoccl	$⊢ (K \in OP \land \underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}) \in B) \to oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})) \in B$
50	47 43 49	syl2anc	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \to oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})) \in B$
51	50	adantr	$⊢ (((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \land x \in A) \to oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})) \in B$
52		eqid	$⊢ meet (K) = meet (K)$
53	1 2 52	latlem12	$⊢ (K \in Lat \land (x \in B \land \underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}) \in B \land oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})) \in B)) \to ((x \underset{˙}{\leq} \underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}) \land x \underset{˙}{\leq} oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}))) \leftrightarrow x \underset{˙}{\leq} (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}) meet (K) oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}))))$
54	39 41 44 51 53	syl13anc	$⊢ (((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \land x \in A) \to ((x \underset{˙}{\leq} \underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}) \land x \underset{˙}{\leq} oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}))) \leftrightarrow x \underset{˙}{\leq} (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}) meet (K) oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}))))$
55	1 48 52 32	opnoncon	$⊢ (K \in OP \land \underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}) \in B) \to \underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}) meet (K) oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})) = 0. (K)$
56	47 43 55	syl2anc	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \to \underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}) meet (K) oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})) = 0. (K)$
57	56	breq2d	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \to (x \underset{˙}{\leq} (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}) meet (K) oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}))) \leftrightarrow x \underset{˙}{\leq} 0. (K))$
58	57	adantr	$⊢ (((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \land x \in A) \to (x \underset{˙}{\leq} (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}) meet (K) oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}))) \leftrightarrow x \underset{˙}{\leq} 0. (K))$
59	1 2 32	ople0	$⊢ (K \in OP \land x \in B) \to (x \underset{˙}{\leq} 0. (K) \leftrightarrow x = 0. (K))$
60	47 40 59	syl2an	$⊢ (((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \land x \in A) \to (x \underset{˙}{\leq} 0. (K) \leftrightarrow x = 0. (K))$
61	54 58 60	3bitrd	$⊢ (((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \land x \in A) \to ((x \underset{˙}{\leq} \underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}) \land x \underset{˙}{\leq} oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}))) \leftrightarrow x = 0. (K))$
62	61	biimpa	$⊢ ((((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \land x \in A) \land (x \underset{˙}{\leq} \underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}) \land x \underset{˙}{\leq} oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})))) \to x = 0. (K)$
63	62	expr	$⊢ ((((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \land x \in A) \land x \underset{˙}{\leq} \underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})) \to (x \underset{˙}{\leq} oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})) \to x = 0. (K))$
64	63	necon3ad	$⊢ ((((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \land x \in A) \land x \underset{˙}{\leq} \underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})) \to (x \neq 0. (K) \to \neg x \underset{˙}{\leq} oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})))$
65	35 64	mpd	$⊢ ((((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \land x \in A) \land x \underset{˙}{\leq} \underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})) \to \neg x \underset{˙}{\leq} oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}))$
66	65	ex	$⊢ (((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \land x \in A) \to (x \underset{˙}{\leq} \underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}) \to \neg x \underset{˙}{\leq} oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})))$
67	30 66	syld	$⊢ (((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \land x \in A) \to (x \underset{˙}{\leq} X \to \neg x \underset{˙}{\leq} oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})))$
68		imnan	$⊢ (x \underset{˙}{\leq} X \to \neg x \underset{˙}{\leq} oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}))) \leftrightarrow \neg (x \underset{˙}{\leq} X \land x \underset{˙}{\leq} oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})))$
69	67 68	sylib	$⊢ (((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \land x \in A) \to \neg (x \underset{˙}{\leq} X \land x \underset{˙}{\leq} oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})))$
70		simplr	$⊢ (((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \land x \in A) \to X \in B$
71	1 2 52	latlem12	$⊢ (K \in Lat \land (x \in B \land X \in B \land oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})) \in B)) \to ((x \underset{˙}{\leq} X \land x \underset{˙}{\leq} oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}))) \leftrightarrow x \underset{˙}{\leq} (X meet (K) oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}))))$
72	39 41 70 51 71	syl13anc	$⊢ (((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \land x \in A) \to ((x \underset{˙}{\leq} X \land x \underset{˙}{\leq} oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}))) \leftrightarrow x \underset{˙}{\leq} (X meet (K) oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}))))$
73	69 72	mtbid	$⊢ (((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \land x \in A) \to \neg x \underset{˙}{\leq} (X meet (K) oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})))$
74	73	nrexdv	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \to \neg \exists x \in A x \underset{˙}{\leq} (X meet (K) oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})))$
75		simpll3	$⊢ (((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \land X meet (K) oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})) \neq 0. (K)) \to K \in AtLat$
76		simpr	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \to X \in B$
77	1 52	latmcl	$⊢ (K \in Lat \land X \in B \land oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})) \in B) \to X meet (K) oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})) \in B$
78	38 76 50 77	syl3anc	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \to X meet (K) oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})) \in B$
79	78	adantr	$⊢ (((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \land X meet (K) oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})) \neq 0. (K)) \to X meet (K) oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})) \in B$
80		simpr	$⊢ (((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \land X meet (K) oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})) \neq 0. (K)) \to X meet (K) oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})) \neq 0. (K)$
81	1 2 32 4	atlex	$⊢ (K \in AtLat \land X meet (K) oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})) \in B \land X meet (K) oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})) \neq 0. (K)) \to \exists x \in A x \underset{˙}{\leq} (X meet (K) oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})))$
82	75 79 80 81	syl3anc	$⊢ (((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \land X meet (K) oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})) \neq 0. (K)) \to \exists x \in A x \underset{˙}{\leq} (X meet (K) oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})))$
83	82	ex	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \to (X meet (K) oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})) \neq 0. (K) \to \exists x \in A x \underset{˙}{\leq} (X meet (K) oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}))))$
84	83	necon1bd	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \to (\neg \exists x \in A x \underset{˙}{\leq} (X meet (K) oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}))) \to X meet (K) oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})) = 0. (K))$
85	74 84	mpd	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \to X meet (K) oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})) = 0. (K)$
86	1 2 52 48 32	omllaw3	$⊢ (K \in OML \land \underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}) \in B \land X \in B) \to ((\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}) \underset{˙}{\leq} X \land X meet (K) oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})) = 0. (K)) \to \underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}) = X)$
87	45 43 76 86	syl3anc	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \to ((\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}) \underset{˙}{\leq} X \land X meet (K) oc (K) (\underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\})) = 0. (K)) \to \underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}) = X)$
88	19 85 87	mp2and	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land X \in B) \to \underset{˙}{1} (\{y \in A \| y \underset{˙}{\leq} X\}) = X$

Metamath Proof Explorer

Theorem atlatmstc

Proof