Metamath Proof Explorer

Theorem lvolnleat

Description: An atom cannot majorize a lattice volume. (Contributed by NM, 14-Jul-2012)

Ref Expression
Hypotheses lvolnleat.l ⊢ ≤ ˙ = ≤ K
lvolnleat.a ⊢ A = Atoms ⁡ K
lvolnleat.v ⊢ V = LVols ⁡ K
Assertion lvolnleat ⊢ K ∈ HL ∧ X ∈ V ∧ P ∈ A → ¬ X ≤ ˙ P

Proof

Step Hyp Ref Expression
1 lvolnleat.l ⊢ ≤ ˙ = ≤ K
2 lvolnleat.a ⊢ A = Atoms ⁡ K
3 lvolnleat.v ⊢ V = LVols ⁡ K
4 3simpa ⊢ K ∈ HL ∧ X ∈ V ∧ P ∈ A → K ∈ HL ∧ X ∈ V
5 simp3 ⊢ K ∈ HL ∧ X ∈ V ∧ P ∈ A → P ∈ A
6 eqid ⊢ join ⁡ K = join ⁡ K
7 1 6 2 3 lvolnle3at ⊢ K ∈ HL ∧ X ∈ V ∧ P ∈ A ∧ P ∈ A ∧ P ∈ A → ¬ X ≤ ˙ P join ⁡ K P join ⁡ K P
8 4 5 5 5 7 syl13anc ⊢ K ∈ HL ∧ X ∈ V ∧ P ∈ A → ¬ X ≤ ˙ P join ⁡ K P join ⁡ K P
9 6 2 hlatjidm ⊢ K ∈ HL ∧ P ∈ A → P join ⁡ K P = P
10 9 3adant2 ⊢ K ∈ HL ∧ X ∈ V ∧ P ∈ A → P join ⁡ K P = P
11 10 oveq1d ⊢ K ∈ HL ∧ X ∈ V ∧ P ∈ A → P join ⁡ K P join ⁡ K P = P join ⁡ K P
12 11 10 eqtrd ⊢ K ∈ HL ∧ X ∈ V ∧ P ∈ A → P join ⁡ K P join ⁡ K P = P
13 12 breq2d ⊢ K ∈ HL ∧ X ∈ V ∧ P ∈ A → X ≤ ˙ P join ⁡ K P join ⁡ K P ↔ X ≤ ˙ P
14 8 13 mtbid ⊢ K ∈ HL ∧ X ∈ V ∧ P ∈ A → ¬ X ≤ ˙ P