# Metamath Proof Explorer

## Theorem dihmeetlem16N

Description: Lemma for isomorphism H of a lattice meet. (Contributed by NM, 7-Apr-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dihmeetlem14.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
dihmeetlem14.l
dihmeetlem14.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dihmeetlem14.j
dihmeetlem14.m
dihmeetlem14.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
dihmeetlem14.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
dihmeetlem14.s
dihmeetlem14.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
Assertion dihmeetlem16N

### Proof

Step Hyp Ref Expression
1 dihmeetlem14.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 dihmeetlem14.l
3 dihmeetlem14.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
4 dihmeetlem14.j
5 dihmeetlem14.m
6 dihmeetlem14.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
7 dihmeetlem14.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
8 dihmeetlem14.s
9 dihmeetlem14.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
10 eqid ${⊢}{0}_{{U}}={0}_{{U}}$
11 1 2 3 4 5 6 7 8 9 10 dihmeetlem15N
12 11 oveq2d
13 simpl1
14 simpl2
15 simpl3l
16 1 6 atbase ${⊢}{p}\in {A}\to {p}\in {B}$
17 15 16 syl
18 simpr1
19 simpr2
20 simpr3
21 1 2 3 4 5 6 7 8 9 dihmeetlem14N
22 13 14 17 18 19 20 21 syl33anc
23 3 7 13 dvhlmod
24 simpl1l
25 24 hllatd
26 1 5 latmcl
27 25 14 17 26 syl3anc
28 eqid ${⊢}\mathrm{LSubSp}\left({U}\right)=\mathrm{LSubSp}\left({U}\right)$
29 1 3 9 7 28 dihlss
30 13 27 29 syl2anc
31 28 lsssubg
32 23 30 31 syl2anc
33 10 8 lsm01
34 32 33 syl
35 12 22 34 3eqtr3rd