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

Metamath Proof Explorer

Theorem lhp1cvr

Description: The lattice unity covers a co-atom (lattice hyperplane). (Contributed by NM, 18-May-2012)

Ref Expression
Hypotheses lhp1cvr.u ⊢ 1 ˙ = 1. ⁡ K
lhp1cvr.c ⊢ C = ⋖ K
lhp1cvr.h ⊢ H = LHyp ⁡ K
Assertion lhp1cvr ⊢ K ∈ A ∧ W ∈ H → W C 1 ˙

Proof

Step Hyp Ref Expression
1 lhp1cvr.u ⊢ 1 ˙ = 1. ⁡ K
2 lhp1cvr.c ⊢ C = ⋖ K
3 lhp1cvr.h ⊢ H = LHyp ⁡ K
4 eqid ⊢ Base K = Base K
5 4 1 2 3 islhp ⊢ K ∈ A → W ∈ H ↔ W ∈ Base K ∧ W C 1 ˙
6 5 simplbda ⊢ K ∈ A ∧ W ∈ H → W C 1 ˙