Metamath Proof Explorer

Theorem lhple

Description: Property of a lattice element under a co-atom. (Contributed by NM, 28-Feb-2014)

Ref Expression
Hypotheses lhple.b ⊢B=BaseK
lhple.l ⊢≤˙=≤K
lhple.j ⊢∨˙=join⁡K
lhple.m ⊢∧˙=meet⁡K
lhple.a ⊢A=Atoms⁡K
lhple.h ⊢H=LHyp⁡K
Assertion lhple ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧X∈B∧X≤˙W→P∨˙X∧˙W=X

Proof

Step Hyp Ref Expression
1 lhple.b ⊢B=BaseK
2 lhple.l ⊢≤˙=≤K
3 lhple.j ⊢∨˙=join⁡K
4 lhple.m ⊢∧˙=meet⁡K
5 lhple.a ⊢A=Atoms⁡K
6 lhple.h ⊢H=LHyp⁡K
7 simp1l ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧X∈B∧X≤˙W→K∈HL
8 7 hllatd ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧X∈B∧X≤˙W→K∈Lat
9 simp2l ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧X∈B∧X≤˙W→P∈A
10 1 5 atbase ⊢P∈A→P∈B
11 9 10 syl ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧X∈B∧X≤˙W→P∈B
12 simp3l ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧X∈B∧X≤˙W→X∈B
13 1 3 latjcom ⊢K∈Lat∧P∈B∧X∈B→P∨˙X=X∨˙P
14 8 11 12 13 syl3anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧X∈B∧X≤˙W→P∨˙X=X∨˙P
15 14 oveq1d ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧X∈B∧X≤˙W→P∨˙X∧˙W=X∨˙P∧˙W
16 simp1 ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧X∈B∧X≤˙W→K∈HL∧W∈H
17 simp3r ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧X∈B∧X≤˙W→X≤˙W
18 1 2 3 4 6 lhpmod6i1 ⊢K∈HL∧W∈H∧X∈B∧P∈B∧X≤˙W→X∨˙P∧˙W=X∨˙P∧˙W
19 16 12 11 17 18 syl121anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧X∈B∧X≤˙W→X∨˙P∧˙W=X∨˙P∧˙W
20 eqid ⊢0.⁡K=0.⁡K
21 2 4 20 5 6 lhpmat ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W→P∧˙W=0.⁡K
22 21 3adant3 ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧X∈B∧X≤˙W→P∧˙W=0.⁡K
23 22 oveq2d ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧X∈B∧X≤˙W→X∨˙P∧˙W=X∨˙0.⁡K
24 hlol ⊢K∈HL→K∈OL
25 7 24 syl ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧X∈B∧X≤˙W→K∈OL
26 1 3 20 olj01 ⊢K∈OL∧X∈B→X∨˙0.⁡K=X
27 25 12 26 syl2anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧X∈B∧X≤˙W→X∨˙0.⁡K=X
28 23 27 eqtrd ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧X∈B∧X≤˙W→X∨˙P∧˙W=X
29 15 19 28 3eqtr2d ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧X∈B∧X≤˙W→P∨˙X∧˙W=X