Theorem lhpexnle

Description: There exists an atom not under a co-atom. (Contributed by NM, 12-Apr-2013)

	Ref	Expression
Hypotheses	lhp2a.l	⊢ ≤ = ( le ‘ 𝐾 )
	lhp2a.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	lhp2a.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion	lhpexnle	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ 𝐴 ¬ 𝑝 ≤ 𝑊 )

Proof

Step	Hyp	Ref	Expression
1		lhp2a.l	⊢ ≤ = ( le ‘ 𝐾 )
2		lhp2a.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3		lhp2a.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4		eqid	⊢ ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
5		eqid	⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
6	4 5 3	lhp1cvr	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑊 ( ⋖ ‘ 𝐾 ) ( 1. ‘ 𝐾 ) )
7		simpl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐾 ∈ HL )
8		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
9	8 3	lhpbase	⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
10	9	adantl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
11		hlop	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
12	8 4	op1cl	⊢ ( 𝐾 ∈ OP → ( 1. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
13	11 12	syl	⊢ ( 𝐾 ∈ HL → ( 1. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
14	13	adantr	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 1. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
15		eqid	⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
16	8 1 15 5 2	cvrval3	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ∧ ( 1. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑊 ( ⋖ ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ↔ ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝑊 ( join ‘ 𝐾 ) 𝑝 ) = ( 1. ‘ 𝐾 ) ) ) )
17	7 10 14 16	syl3anc	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑊 ( ⋖ ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ↔ ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝑊 ( join ‘ 𝐾 ) 𝑝 ) = ( 1. ‘ 𝐾 ) ) ) )
18	6 17	mpbid	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝑊 ( join ‘ 𝐾 ) 𝑝 ) = ( 1. ‘ 𝐾 ) ) )
19		simpl	⊢ ( ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝑊 ( join ‘ 𝐾 ) 𝑝 ) = ( 1. ‘ 𝐾 ) ) → ¬ 𝑝 ≤ 𝑊 )
20	19	reximi	⊢ ( ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝑊 ( join ‘ 𝐾 ) 𝑝 ) = ( 1. ‘ 𝐾 ) ) → ∃ 𝑝 ∈ 𝐴 ¬ 𝑝 ≤ 𝑊 )
21	18 20	syl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ 𝐴 ¬ 𝑝 ≤ 𝑊 )