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

Metamath Proof Explorer

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 ∧ 𝑊 ∈ 𝐻 ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )