Theorem lhpocnel2

Description: The orthocomplement of a co-atom is an atom not under it. Provides a convenient construction when we need the existence of any object with this property. (Contributed by NM, 20-Feb-2014)

	Ref	Expression
Hypotheses	lhpocnel2.l	⊢ ≤ = ( le ‘ 𝐾 )
	lhpocnel2.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	lhpocnel2.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	lhpocnel2.p	⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
Assertion	lhpocnel2	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )

Proof

Step	Hyp	Ref	Expression
1		lhpocnel2.l	⊢ ≤ = ( le ‘ 𝐾 )
2		lhpocnel2.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3		lhpocnel2.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4		lhpocnel2.p	⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
5		eqid	⊢ ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 )
6	1 5 2 3	lhpocnel	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ 𝐴 ∧ ¬ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ≤ 𝑊 ) )
7	4	eleq1i	⊢ ( 𝑃 ∈ 𝐴 ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ 𝐴 )
8	4	breq1i	⊢ ( 𝑃 ≤ 𝑊 ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ≤ 𝑊 )
9	8	notbii	⊢ ( ¬ 𝑃 ≤ 𝑊 ↔ ¬ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ≤ 𝑊 )
10	7 9	anbi12i	⊢ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ↔ ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ 𝐴 ∧ ¬ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ≤ 𝑊 ) )
11	6 10	sylibr	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )