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 𝐵 = ( Base ‘ 𝐾 )
hlatmstc.l = ( le ‘ 𝐾 )
hlatmstc.u 𝑈 = ( lub ‘ 𝐾 )
hlatmstc.a 𝐴 = ( Atoms ‘ 𝐾 )
Assertion hlatmstcOLDN ( ( 𝐾 ∈ HL ∧ 𝑋𝐵 ) → ( 𝑈 ‘ { 𝑦𝐴𝑦 𝑋 } ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 hlatmstc.b 𝐵 = ( Base ‘ 𝐾 )
2 hlatmstc.l = ( le ‘ 𝐾 )
3 hlatmstc.u 𝑈 = ( lub ‘ 𝐾 )
4 hlatmstc.a 𝐴 = ( Atoms ‘ 𝐾 )
5 hlomcmat ( 𝐾 ∈ HL → ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) )
6 1 2 3 4 atlatmstc ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋𝐵 ) → ( 𝑈 ‘ { 𝑦𝐴𝑦 𝑋 } ) = 𝑋 )
7 5 6 sylan ( ( 𝐾 ∈ HL ∧ 𝑋𝐵 ) → ( 𝑈 ‘ { 𝑦𝐴𝑦 𝑋 } ) = 𝑋 )