# 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
dihvalcqat.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
dihvalcqat.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dihvalcqat.j ${⊢}{J}=\mathrm{DIsoC}\left({K}\right)\left({W}\right)$
dihvalcqat.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
Assertion dihvalcqat

### Proof

Step Hyp Ref Expression
1 dihvalcqat.l
2 dihvalcqat.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
3 dihvalcqat.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
4 dihvalcqat.j ${⊢}{J}=\mathrm{DIsoC}\left({K}\right)\left({W}\right)$
5 dihvalcqat.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
6 simpl
7 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
8 7 2 atbase ${⊢}{Q}\in {A}\to {Q}\in {\mathrm{Base}}_{{K}}$
10 simprr
11 simpr
12 eqid ${⊢}\mathrm{meet}\left({K}\right)=\mathrm{meet}\left({K}\right)$
13 eqid ${⊢}\mathrm{0.}\left({K}\right)=\mathrm{0.}\left({K}\right)$
14 1 12 13 2 3 lhpmat
15 14 oveq2d
16 hlol ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{OL}$
18 eqid ${⊢}\mathrm{join}\left({K}\right)=\mathrm{join}\left({K}\right)$
19 7 18 13 olj01 ${⊢}\left({K}\in \mathrm{OL}\wedge {Q}\in {\mathrm{Base}}_{{K}}\right)\to {Q}\mathrm{join}\left({K}\right)\mathrm{0.}\left({K}\right)={Q}$
20 17 9 19 syl2anc
21 15 20 eqtrd
22 eqid ${⊢}\mathrm{DIsoB}\left({K}\right)\left({W}\right)=\mathrm{DIsoB}\left({K}\right)\left({W}\right)$
23 eqid ${⊢}\mathrm{DVecH}\left({K}\right)\left({W}\right)=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
24 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)$
25 7 1 18 12 2 3 5 22 4 23 24 dihvalcq
26 6 9 10 11 21 25 syl122anc
27 14 fveq2d
28 eqid ${⊢}{0}_{\mathrm{DVecH}\left({K}\right)\left({W}\right)}={0}_{\mathrm{DVecH}\left({K}\right)\left({W}\right)}$
29 13 3 22 23 28 dib0 ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \mathrm{DIsoB}\left({K}\right)\left({W}\right)\left(\mathrm{0.}\left({K}\right)\right)=\left\{{0}_{\mathrm{DVecH}\left({K}\right)\left({W}\right)}\right\}$
34 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)$
36 34 lsssubg ${⊢}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\in \mathrm{LMod}\wedge {J}\left({Q}\right)\in \mathrm{LSubSp}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)\right)\to {J}\left({Q}\right)\in \mathrm{SubGrp}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)$
38 28 24 lsm01 ${⊢}{J}\left({Q}\right)\in \mathrm{SubGrp}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)\to {J}\left({Q}\right)\mathrm{LSSum}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)\left\{{0}_{\mathrm{DVecH}\left({K}\right)\left({W}\right)}\right\}={J}\left({Q}\right)$