Metamath Proof Explorer

Theorem lhpocnle

Description: The orthocomplement of a co-atom is not under it. (Contributed by NM, 22-May-2012)

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

Proof

Step Hyp Ref Expression
1 lhpocnle.l ⊢ ≤ = ( le ‘ 𝐾 )
2 lhpocnle.o ⊢ ⊥ = ( oc ‘ 𝐾 )
3 lhpocnle.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4 hlatl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
5 4 adantr ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐾 ∈ AtLat )
6 simpr ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑊 ∈ 𝐻 )
7 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
8 7 3 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
9 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
10 7 2 9 3 lhpoc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑊 ∈ 𝐻 ↔ ( ⊥ ‘ 𝑊 ) ∈ ( Atoms ‘ 𝐾 ) ) )
11 8 10 sylan2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑊 ∈ 𝐻 ↔ ( ⊥ ‘ 𝑊 ) ∈ ( Atoms ‘ 𝐾 ) ) )
12 6 11 mpbid ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ⊥ ‘ 𝑊 ) ∈ ( Atoms ‘ 𝐾 ) )
13 eqid ⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
14 13 9 atn0 ⊢ ( ( 𝐾 ∈ AtLat ∧ ( ⊥ ‘ 𝑊 ) ∈ ( Atoms ‘ 𝐾 ) ) → ( ⊥ ‘ 𝑊 ) ≠ ( 0. ‘ 𝐾 ) )
15 5 12 14 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ⊥ ‘ 𝑊 ) ≠ ( 0. ‘ 𝐾 ) )
16 15 neneqd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ¬ ( ⊥ ‘ 𝑊 ) = ( 0. ‘ 𝐾 ) )
17 simpr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ 𝑊 ) ≤ 𝑊 ) → ( ⊥ ‘ 𝑊 ) ≤ 𝑊 )
18 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
19 18 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ 𝑊 ) ≤ 𝑊 ) → 𝐾 ∈ Lat )
20 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
21 20 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ 𝑊 ) ≤ 𝑊 ) → 𝐾 ∈ OP )
22 8 ad2antlr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ 𝑊 ) ≤ 𝑊 ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
23 7 2 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ⊥ ‘ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
24 21 22 23 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ 𝑊 ) ≤ 𝑊 ) → ( ⊥ ‘ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
25 7 1 latref ⊢ ( ( 𝐾 ∈ Lat ∧ ( ⊥ ‘ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) → ( ⊥ ‘ 𝑊 ) ≤ ( ⊥ ‘ 𝑊 ) )
26 19 24 25 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ 𝑊 ) ≤ 𝑊 ) → ( ⊥ ‘ 𝑊 ) ≤ ( ⊥ ‘ 𝑊 ) )
27 eqid ⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
28 7 1 27 latlem12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( ⊥ ‘ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ∧ ( ⊥ ‘ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( ⊥ ‘ 𝑊 ) ≤ 𝑊 ∧ ( ⊥ ‘ 𝑊 ) ≤ ( ⊥ ‘ 𝑊 ) ) ↔ ( ⊥ ‘ 𝑊 ) ≤ ( 𝑊 ( meet ‘ 𝐾 ) ( ⊥ ‘ 𝑊 ) ) ) )
29 19 24 22 24 28 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ 𝑊 ) ≤ 𝑊 ) → ( ( ( ⊥ ‘ 𝑊 ) ≤ 𝑊 ∧ ( ⊥ ‘ 𝑊 ) ≤ ( ⊥ ‘ 𝑊 ) ) ↔ ( ⊥ ‘ 𝑊 ) ≤ ( 𝑊 ( meet ‘ 𝐾 ) ( ⊥ ‘ 𝑊 ) ) ) )
30 17 26 29 mpbi2and ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ 𝑊 ) ≤ 𝑊 ) → ( ⊥ ‘ 𝑊 ) ≤ ( 𝑊 ( meet ‘ 𝐾 ) ( ⊥ ‘ 𝑊 ) ) )
31 7 2 27 13 opnoncon ⊢ ( ( 𝐾 ∈ OP ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑊 ( meet ‘ 𝐾 ) ( ⊥ ‘ 𝑊 ) ) = ( 0. ‘ 𝐾 ) )
32 21 22 31 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ 𝑊 ) ≤ 𝑊 ) → ( 𝑊 ( meet ‘ 𝐾 ) ( ⊥ ‘ 𝑊 ) ) = ( 0. ‘ 𝐾 ) )
33 30 32 breqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ 𝑊 ) ≤ 𝑊 ) → ( ⊥ ‘ 𝑊 ) ≤ ( 0. ‘ 𝐾 ) )
34 7 1 13 ople0 ⊢ ( ( 𝐾 ∈ OP ∧ ( ⊥ ‘ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( ⊥ ‘ 𝑊 ) ≤ ( 0. ‘ 𝐾 ) ↔ ( ⊥ ‘ 𝑊 ) = ( 0. ‘ 𝐾 ) ) )
35 21 24 34 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ 𝑊 ) ≤ 𝑊 ) → ( ( ⊥ ‘ 𝑊 ) ≤ ( 0. ‘ 𝐾 ) ↔ ( ⊥ ‘ 𝑊 ) = ( 0. ‘ 𝐾 ) ) )
36 33 35 mpbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ 𝑊 ) ≤ 𝑊 ) → ( ⊥ ‘ 𝑊 ) = ( 0. ‘ 𝐾 ) )
37 16 36 mtand ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ¬ ( ⊥ ‘ 𝑊 ) ≤ 𝑊 )