# Metamath Proof Explorer

## Theorem 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}={\mathrm{Base}}_{{K}}$
atlatmstc.l
atlatmstc.u
atlatmstc.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
Assertion atlatmstc

### Proof

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