# Metamath Proof Explorer

## Theorem dihvalb

Description: Value of isomorphism H for a lattice K when X .<_ W . (Contributed by NM, 4-Mar-2014)

Ref Expression
Hypotheses dihvalb.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
dihvalb.l
dihvalb.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dihvalb.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
dihvalb.d ${⊢}{D}=\mathrm{DIsoB}\left({K}\right)\left({W}\right)$
Assertion dihvalb

### Proof

Step Hyp Ref Expression
1 dihvalb.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 dihvalb.l
3 dihvalb.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
4 dihvalb.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
5 dihvalb.d ${⊢}{D}=\mathrm{DIsoB}\left({K}\right)\left({W}\right)$
6 eqid ${⊢}\mathrm{join}\left({K}\right)=\mathrm{join}\left({K}\right)$
7 eqid ${⊢}\mathrm{meet}\left({K}\right)=\mathrm{meet}\left({K}\right)$
8 eqid ${⊢}\mathrm{Atoms}\left({K}\right)=\mathrm{Atoms}\left({K}\right)$
9 eqid ${⊢}\mathrm{DIsoC}\left({K}\right)\left({W}\right)=\mathrm{DIsoC}\left({K}\right)\left({W}\right)$
10 eqid ${⊢}\mathrm{DVecH}\left({K}\right)\left({W}\right)=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
11 eqid ${⊢}\mathrm{LSubSp}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)=\mathrm{LSubSp}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)$
12 eqid ${⊢}\mathrm{LSSum}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)=\mathrm{LSSum}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)$
13 1 2 6 7 8 3 4 5 9 10 11 12 dihval
14 iftrue
15 13 14 sylan9eq
16 15 anasss