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. ‘ 𝐾 )
	lhp1cvr.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
	lhp1cvr.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion	lhp1cvr	⊢ ( ( 𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻 ) → 𝑊 𝐶 1 )

Proof

Step	Hyp	Ref	Expression
1		lhp1cvr.u	⊢ 1 = ( 1. ‘ 𝐾 )
2		lhp1cvr.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
3		lhp1cvr.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
5	4 1 2 3	islhp	⊢ ( 𝐾 ∈ 𝐴 → ( 𝑊 ∈ 𝐻 ↔ ( 𝑊 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 𝐶 1 ) ) )
6	5	simplbda	⊢ ( ( 𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻 ) → 𝑊 𝐶 1 )