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

Metamath Proof Explorer

Theorem lhpocnel

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, 25-May-2012)

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

Proof

Step	Hyp	Ref	Expression
1		lhpocnel.l	⊢ ≤ = ( le ‘ 𝐾 )
2		lhpocnel.o	⊢ ⊥ = ( oc ‘ 𝐾 )
3		lhpocnel.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		lhpocnel.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
5	2 3 4	lhpocat	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ⊥ ‘ 𝑊 ) ∈ 𝐴 )
6	1 2 4	lhpocnle	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ¬ ( ⊥ ‘ 𝑊 ) ≤ 𝑊 )
7	5 6	jca	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( ⊥ ‘ 𝑊 ) ∈ 𝐴 ∧ ¬ ( ⊥ ‘ 𝑊 ) ≤ 𝑊 ) )