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 ⊢ ≤ ˙ = ≤ K
lhpocnle.o ⊢ ⊥ ˙ = oc ⁡ K
lhpocnle.h ⊢ H = LHyp ⁡ K
Assertion lhpocnle ⊢ K ∈ HL ∧ W ∈ H → ¬ ⊥ ˙ ⁡ W ≤ ˙ W

Proof

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