# Metamath Proof Explorer

## Theorem lhp2at0

Description: Join and meet with different atoms under co-atom W . (Contributed by NM, 15-Jun-2013)

Ref Expression
Hypotheses lhp2at0.l
lhp2at0.j
lhp2at0.m
lhp2at0.z
lhp2at0.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
lhp2at0.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
Assertion lhp2at0

### Proof

Step Hyp Ref Expression
1 lhp2at0.l
2 lhp2at0.j
3 lhp2at0.m
4 lhp2at0.z
5 lhp2at0.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
6 lhp2at0.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
7 simp11l
8 hlol ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{OL}$
9 7 8 syl
10 simp12l
11 simp2l
12 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
13 12 2 5 hlatjcl
14 7 10 11 13 syl3anc
15 simp11r
16 12 6 lhpbase ${⊢}{W}\in {H}\to {W}\in {\mathrm{Base}}_{{K}}$
17 15 16 syl
18 simp3l
19 12 5 atbase ${⊢}{V}\in {A}\to {V}\in {\mathrm{Base}}_{{K}}$
20 18 19 syl
21 12 3 latmassOLD
22 9 14 17 20 21 syl13anc
23 1 3 4 5 6 lhpmat
26 25 oveq1d
27 12 5 atbase ${⊢}{U}\in {A}\to {U}\in {\mathrm{Base}}_{{K}}$
28 11 27 syl
29 simp2r
30 12 1 2 3 5 atmod4i2
31 7 10 28 17 29 30 syl131anc
32 12 2 4 olj02
33 9 28 32 syl2anc
34 26 31 33 3eqtr3d
35 34 oveq1d
36 22 35 eqtr3d
37 simp3r
38 7 hllatd
39 12 1 3 latleeqm2
40 38 20 17 39 syl3anc
41 37 40 mpbid
42 41 oveq2d
43 simp13
44 hlatl ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{AtLat}$
45 7 44 syl
46 3 4 5 atnem0
47 45 11 18 46 syl3anc
48 43 47 mpbid
49 36 42 48 3eqtr3d