This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = Base K
hlatmstc.l ⊢ ≤ ˙ = ≤ K
hlatmstc.u ⊢ U = lub ⁡ K
hlatmstc.a ⊢ A = Atoms ⁡ K
Assertion hlatmstcOLDN ⊢ K ∈ HL ∧ X ∈ B → U ⁡ y ∈ A | y ≤ ˙ X = X

Proof

Step Hyp Ref Expression
1 hlatmstc.b ⊢ B = Base K
2 hlatmstc.l ⊢ ≤ ˙ = ≤ K
3 hlatmstc.u ⊢ U = lub ⁡ K
4 hlatmstc.a ⊢ A = Atoms ⁡ K
5 hlomcmat ⊢ K ∈ HL → K ∈ OML ∧ K ∈ CLat ∧ K ∈ AtLat
6 1 2 3 4 atlatmstc ⊢ K ∈ OML ∧ K ∈ CLat ∧ K ∈ AtLat ∧ X ∈ B → U ⁡ y ∈ A | y ≤ ˙ X = X
7 5 6 sylan ⊢ K ∈ HL ∧ X ∈ B → U ⁡ y ∈ A | y ≤ ˙ X = X