# Metamath Proof Explorer

## Theorem dihvalcq

Description: Value of isomorphism H for a lattice K when -. X .<_ W , given auxiliary atom Q . TODO: Use dihvalcq2 (with lhpmcvr3 for ( Q .\/ ( X ./\ W ) ) = X simplification) that changes C and D to I and make this obsolete. Do to other theorems as well. (Contributed by NM, 6-Mar-2014)

Ref Expression
Hypotheses dihvalcq.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
dihvalcq.l
dihvalcq.j
dihvalcq.m
dihvalcq.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
dihvalcq.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dihvalcq.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
dihvalcq.d ${⊢}{D}=\mathrm{DIsoB}\left({K}\right)\left({W}\right)$
dihvalcq.c ${⊢}{C}=\mathrm{DIsoC}\left({K}\right)\left({W}\right)$
dihvalcq.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
dihvalcq.p
Assertion dihvalcq

### Proof

Step Hyp Ref Expression
1 dihvalcq.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 dihvalcq.l
3 dihvalcq.j
4 dihvalcq.m
5 dihvalcq.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
6 dihvalcq.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
7 dihvalcq.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
8 dihvalcq.d ${⊢}{D}=\mathrm{DIsoB}\left({K}\right)\left({W}\right)$
9 dihvalcq.c ${⊢}{C}=\mathrm{DIsoC}\left({K}\right)\left({W}\right)$
10 dihvalcq.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
11 dihvalcq.p
12 eqid ${⊢}\mathrm{LSubSp}\left({U}\right)=\mathrm{LSubSp}\left({U}\right)$
13 1 2 3 4 5 6 7 8 9 10 12 11 dihvalcqpre