# Metamath Proof Explorer

## Theorem dihvalcqat

Description: Value of isomorphism H for a lattice K at an atom not under W . (Contributed by NM, 27-Mar-2014)

Ref Expression
Hypotheses dihvalcqat.l
`|- .<_ = ( le ` K )`
dihvalcqat.a
`|- A = ( Atoms ` K )`
dihvalcqat.h
`|- H = ( LHyp ` K )`
dihvalcqat.j
`|- J = ( ( DIsoC ` K ) ` W )`
dihvalcqat.i
`|- I = ( ( DIsoH ` K ) ` W )`
Assertion dihvalcqat
`|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) = ( J ` Q ) )`

### Proof

Step Hyp Ref Expression
1 dihvalcqat.l
` |-  .<_ = ( le ` K )`
2 dihvalcqat.a
` |-  A = ( Atoms ` K )`
3 dihvalcqat.h
` |-  H = ( LHyp ` K )`
4 dihvalcqat.j
` |-  J = ( ( DIsoC ` K ) ` W )`
5 dihvalcqat.i
` |-  I = ( ( DIsoH ` K ) ` W )`
6 simpl
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( K e. HL /\ W e. H ) )`
7 eqid
` |-  ( Base ` K ) = ( Base ` K )`
8 7 2 atbase
` |-  ( Q e. A -> Q e. ( Base ` K ) )`
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> Q e. ( Base ` K ) )`
10 simprr
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> -. Q .<_ W )`
11 simpr
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( Q e. A /\ -. Q .<_ W ) )`
12 eqid
` |-  ( meet ` K ) = ( meet ` K )`
13 eqid
` |-  ( 0. ` K ) = ( 0. ` K )`
14 1 12 13 2 3 lhpmat
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( Q ( meet ` K ) W ) = ( 0. ` K ) )`
15 14 oveq2d
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( Q ( join ` K ) ( Q ( meet ` K ) W ) ) = ( Q ( join ` K ) ( 0. ` K ) ) )`
16 hlol
` |-  ( K e. HL -> K e. OL )`
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> K e. OL )`
18 eqid
` |-  ( join ` K ) = ( join ` K )`
19 7 18 13 olj01
` |-  ( ( K e. OL /\ Q e. ( Base ` K ) ) -> ( Q ( join ` K ) ( 0. ` K ) ) = Q )`
20 17 9 19 syl2anc
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( Q ( join ` K ) ( 0. ` K ) ) = Q )`
21 15 20 eqtrd
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( Q ( join ` K ) ( Q ( meet ` K ) W ) ) = Q )`
22 eqid
` |-  ( ( DIsoB ` K ) ` W ) = ( ( DIsoB ` K ) ` W )`
23 eqid
` |-  ( ( DVecH ` K ) ` W ) = ( ( DVecH ` K ) ` W )`
24 eqid
` |-  ( LSSum ` ( ( DVecH ` K ) ` W ) ) = ( LSSum ` ( ( DVecH ` K ) ` W ) )`
25 7 1 18 12 2 3 5 22 4 23 24 dihvalcq
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. ( Base ` K ) /\ -. Q .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( Q ( join ` K ) ( Q ( meet ` K ) W ) ) = Q ) ) -> ( I ` Q ) = ( ( J ` Q ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( Q ( meet ` K ) W ) ) ) )`
26 6 9 10 11 21 25 syl122anc
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) = ( ( J ` Q ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( Q ( meet ` K ) W ) ) ) )`
27 14 fveq2d
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( ( DIsoB ` K ) ` W ) ` ( Q ( meet ` K ) W ) ) = ( ( ( DIsoB ` K ) ` W ) ` ( 0. ` K ) ) )`
28 eqid
` |-  ( 0g ` ( ( DVecH ` K ) ` W ) ) = ( 0g ` ( ( DVecH ` K ) ` W ) )`
29 13 3 22 23 28 dib0
` |-  ( ( K e. HL /\ W e. H ) -> ( ( ( DIsoB ` K ) ` W ) ` ( 0. ` K ) ) = { ( 0g ` ( ( DVecH ` K ) ` W ) ) } )`
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( ( DIsoB ` K ) ` W ) ` ( 0. ` K ) ) = { ( 0g ` ( ( DVecH ` K ) ` W ) ) } )`
31 27 30 eqtrd
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( ( DIsoB ` K ) ` W ) ` ( Q ( meet ` K ) W ) ) = { ( 0g ` ( ( DVecH ` K ) ` W ) ) } )`
32 31 oveq2d
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( J ` Q ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( Q ( meet ` K ) W ) ) ) = ( ( J ` Q ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) { ( 0g ` ( ( DVecH ` K ) ` W ) ) } ) )`
33 3 23 6 dvhlmod
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( DVecH ` K ) ` W ) e. LMod )`
34 eqid
` |-  ( LSubSp ` ( ( DVecH ` K ) ` W ) ) = ( LSubSp ` ( ( DVecH ` K ) ` W ) )`
35 1 2 3 23 4 34 diclss
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( J ` Q ) e. ( LSubSp ` ( ( DVecH ` K ) ` W ) ) )`
36 34 lsssubg
` |-  ( ( ( ( DVecH ` K ) ` W ) e. LMod /\ ( J ` Q ) e. ( LSubSp ` ( ( DVecH ` K ) ` W ) ) ) -> ( J ` Q ) e. ( SubGrp ` ( ( DVecH ` K ) ` W ) ) )`
37 33 35 36 syl2anc
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( J ` Q ) e. ( SubGrp ` ( ( DVecH ` K ) ` W ) ) )`
38 28 24 lsm01
` |-  ( ( J ` Q ) e. ( SubGrp ` ( ( DVecH ` K ) ` W ) ) -> ( ( J ` Q ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) { ( 0g ` ( ( DVecH ` K ) ` W ) ) } ) = ( J ` Q ) )`
39 37 38 syl
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( J ` Q ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) { ( 0g ` ( ( DVecH ` K ) ` W ) ) } ) = ( J ` Q ) )`
40 32 39 eqtrd
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( J ` Q ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( Q ( meet ` K ) W ) ) ) = ( J ` Q ) )`
41 26 40 eqtrd
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) = ( J ` Q ) )`