# Metamath Proof Explorer

## Theorem dihvalcq2

Description: Value of isomorphism H for a lattice K when -. X .<_ W , given auxiliary atom Q . (Contributed by NM, 26-Sep-2014)

Ref Expression
Hypotheses dihvalcq2.b
`|- B = ( Base ` K )`
dihvalcq2.l
`|- .<_ = ( le ` K )`
dihvalcq2.j
`|- .\/ = ( join ` K )`
dihvalcq2.m
`|- ./\ = ( meet ` K )`
dihvalcq2.a
`|- A = ( Atoms ` K )`
dihvalcq2.h
`|- H = ( LHyp ` K )`
dihvalcq2.i
`|- I = ( ( DIsoH ` K ) ` W )`
dihvalcq2.u
`|- U = ( ( DVecH ` K ) ` W )`
dihvalcq2.p
`|- .(+) = ( LSSum ` U )`
Assertion dihvalcq2
`|- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ X ) ) -> ( I ` X ) = ( ( I ` Q ) .(+) ( I ` ( X ./\ W ) ) ) )`

### Proof

Step Hyp Ref Expression
1 dihvalcq2.b
` |-  B = ( Base ` K )`
2 dihvalcq2.l
` |-  .<_ = ( le ` K )`
3 dihvalcq2.j
` |-  .\/ = ( join ` K )`
4 dihvalcq2.m
` |-  ./\ = ( meet ` K )`
5 dihvalcq2.a
` |-  A = ( Atoms ` K )`
6 dihvalcq2.h
` |-  H = ( LHyp ` K )`
7 dihvalcq2.i
` |-  I = ( ( DIsoH ` K ) ` W )`
8 dihvalcq2.u
` |-  U = ( ( DVecH ` K ) ` W )`
9 dihvalcq2.p
` |-  .(+) = ( LSSum ` U )`
10 simp1
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ X ) ) -> ( K e. HL /\ W e. H ) )`
11 simp2
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ X ) ) -> ( X e. B /\ -. X .<_ W ) )`
12 simp3l
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ X ) ) -> ( Q e. A /\ -. Q .<_ W ) )`
13 simp3r
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ X ) ) -> Q .<_ X )`
14 1 2 3 4 5 6 lhpmcvr3
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( Q .<_ X <-> ( Q .\/ ( X ./\ W ) ) = X ) )`
15 10 11 12 14 syl3anc
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ X ) ) -> ( Q .<_ X <-> ( Q .\/ ( X ./\ W ) ) = X ) )`
16 13 15 mpbid
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ X ) ) -> ( Q .\/ ( X ./\ W ) ) = X )`
17 eqid
` |-  ( ( DIsoB ` K ) ` W ) = ( ( DIsoB ` K ) ` W )`
18 eqid
` |-  ( ( DIsoC ` K ) ` W ) = ( ( DIsoC ` K ) ` W )`
19 1 2 3 4 5 6 7 17 18 8 9 dihvalcq
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( Q .\/ ( X ./\ W ) ) = X ) ) -> ( I ` X ) = ( ( ( ( DIsoC ` K ) ` W ) ` Q ) .(+) ( ( ( DIsoB ` K ) ` W ) ` ( X ./\ W ) ) ) )`
20 10 11 12 16 19 syl112anc
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ X ) ) -> ( I ` X ) = ( ( ( ( DIsoC ` K ) ` W ) ` Q ) .(+) ( ( ( DIsoB ` K ) ` W ) ` ( X ./\ W ) ) ) )`
21 2 5 6 18 7 dihvalcqat
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) = ( ( ( DIsoC ` K ) ` W ) ` Q ) )`
22 10 12 21 syl2anc
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ X ) ) -> ( I ` Q ) = ( ( ( DIsoC ` K ) ` W ) ` Q ) )`
23 simp1l
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ X ) ) -> K e. HL )`
24 23 hllatd
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ X ) ) -> K e. Lat )`
25 simp2l
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ X ) ) -> X e. B )`
26 simp1r
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ X ) ) -> W e. H )`
27 1 6 lhpbase
` |-  ( W e. H -> W e. B )`
28 26 27 syl
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ X ) ) -> W e. B )`
29 1 4 latmcl
` |-  ( ( K e. Lat /\ X e. B /\ W e. B ) -> ( X ./\ W ) e. B )`
30 24 25 28 29 syl3anc
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ X ) ) -> ( X ./\ W ) e. B )`
31 1 2 4 latmle2
` |-  ( ( K e. Lat /\ X e. B /\ W e. B ) -> ( X ./\ W ) .<_ W )`
32 24 25 28 31 syl3anc
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ X ) ) -> ( X ./\ W ) .<_ W )`
33 1 2 6 7 17 dihvalb
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( X ./\ W ) e. B /\ ( X ./\ W ) .<_ W ) ) -> ( I ` ( X ./\ W ) ) = ( ( ( DIsoB ` K ) ` W ) ` ( X ./\ W ) ) )`
34 10 30 32 33 syl12anc
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ X ) ) -> ( I ` ( X ./\ W ) ) = ( ( ( DIsoB ` K ) ` W ) ` ( X ./\ W ) ) )`
35 22 34 oveq12d
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ X ) ) -> ( ( I ` Q ) .(+) ( I ` ( X ./\ W ) ) ) = ( ( ( ( DIsoC ` K ) ` W ) ` Q ) .(+) ( ( ( DIsoB ` K ) ` W ) ` ( X ./\ W ) ) ) )`
36 20 35 eqtr4d
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ X ) ) -> ( I ` X ) = ( ( I ` Q ) .(+) ( I ` ( X ./\ W ) ) ) )`