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