Metamath Proof Explorer


Theorem hlatmstcOLDN

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, 21-Oct-2011) (New usage is discouraged.)

Ref Expression
Hypotheses hlatmstc.b B=BaseK
hlatmstc.l ˙=K
hlatmstc.u U=lubK
hlatmstc.a A=AtomsK
Assertion hlatmstcOLDN KHLXBUyA|y˙X=X

Proof

Step Hyp Ref Expression
1 hlatmstc.b B=BaseK
2 hlatmstc.l ˙=K
3 hlatmstc.u U=lubK
4 hlatmstc.a A=AtomsK
5 hlomcmat KHLKOMLKCLatKAtLat
6 1 2 3 4 atlatmstc KOMLKCLatKAtLatXBUyA|y˙X=X
7 5 6 sylan KHLXBUyA|y˙X=X