# 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 = ( Base ` K )`
dihvalcq.l
`|- .<_ = ( le ` K )`
dihvalcq.j
`|- .\/ = ( join ` K )`
dihvalcq.m
`|- ./\ = ( meet ` K )`
dihvalcq.a
`|- A = ( Atoms ` K )`
dihvalcq.h
`|- H = ( LHyp ` K )`
dihvalcq.i
`|- I = ( ( DIsoH ` K ) ` W )`
dihvalcq.d
`|- D = ( ( DIsoB ` K ) ` W )`
dihvalcq.c
`|- C = ( ( DIsoC ` K ) ` W )`
dihvalcq.u
`|- U = ( ( DVecH ` K ) ` W )`
dihvalcq.p
`|- .(+) = ( LSSum ` U )`
Assertion dihvalcq
`|- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( Q .\/ ( X ./\ W ) ) = X ) ) -> ( I ` X ) = ( ( C ` Q ) .(+) ( D ` ( X ./\ W ) ) ) )`

### Proof

Step Hyp Ref Expression
1 dihvalcq.b
` |-  B = ( Base ` K )`
2 dihvalcq.l
` |-  .<_ = ( le ` K )`
3 dihvalcq.j
` |-  .\/ = ( join ` K )`
4 dihvalcq.m
` |-  ./\ = ( meet ` K )`
5 dihvalcq.a
` |-  A = ( Atoms ` K )`
6 dihvalcq.h
` |-  H = ( LHyp ` K )`
7 dihvalcq.i
` |-  I = ( ( DIsoH ` K ) ` W )`
8 dihvalcq.d
` |-  D = ( ( DIsoB ` K ) ` W )`
9 dihvalcq.c
` |-  C = ( ( DIsoC ` K ) ` W )`
10 dihvalcq.u
` |-  U = ( ( DVecH ` K ) ` W )`
11 dihvalcq.p
` |-  .(+) = ( LSSum ` U )`
12 eqid
` |-  ( LSubSp ` U ) = ( LSubSp ` U )`
13 1 2 3 4 5 6 7 8 9 10 12 11 dihvalcqpre
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( Q .\/ ( X ./\ W ) ) = X ) ) -> ( I ` X ) = ( ( C ` Q ) .(+) ( D ` ( X ./\ W ) ) ) )`