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

Metamath Proof Explorer

Theorem lvolneatN

Description: No lattice volume is an atom. (Contributed by NM, 15-Jul-2012) (New usage is discouraged.)

Ref Expression
Hypotheses lvolneat.a ⊢ A = Atoms ⁡ K
lvolneat.v ⊢ V = LVols ⁡ K
Assertion lvolneatN ⊢ K ∈ HL ∧ X ∈ V → ¬ X ∈ A

Proof

Step Hyp Ref Expression
1 lvolneat.a ⊢ A = Atoms ⁡ K
2 lvolneat.v ⊢ V = LVols ⁡ K
3 hllat ⊢ K ∈ HL → K ∈ Lat
4 eqid ⊢ Base K = Base K
5 4 2 lvolbase ⊢ X ∈ V → X ∈ Base K
6 eqid ⊢ ≤ K = ≤ K
7 4 6 latref ⊢ K ∈ Lat ∧ X ∈ Base K → X ≤ K X
8 3 5 7 syl2an ⊢ K ∈ HL ∧ X ∈ V → X ≤ K X
9 6 1 2 lvolnleat ⊢ K ∈ HL ∧ X ∈ V ∧ X ∈ A → ¬ X ≤ K X
10 9 3expia ⊢ K ∈ HL ∧ X ∈ V → X ∈ A → ¬ X ≤ K X
11 8 10 mt2d ⊢ K ∈ HL ∧ X ∈ V → ¬ X ∈ A