# Metamath Proof Explorer

## Theorem dihglb

Description: Isomorphism H of a lattice glb. (Contributed by NM, 11-Apr-2014)

Ref Expression
Hypotheses dihglb.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
dihglb.g ${⊢}{G}=\mathrm{glb}\left({K}\right)$
dihglb.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dihglb.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
Assertion dihglb ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq {B}\wedge {S}\ne \varnothing \right)\right)\to {I}\left({G}\left({S}\right)\right)=\bigcap _{{x}\in {S}}{I}\left({x}\right)$

### Proof

Step Hyp Ref Expression
1 dihglb.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 dihglb.g ${⊢}{G}=\mathrm{glb}\left({K}\right)$
3 dihglb.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
4 dihglb.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
5 eqid ${⊢}{\le }_{{K}}={\le }_{{K}}$
6 eqid ${⊢}\mathrm{meet}\left({K}\right)=\mathrm{meet}\left({K}\right)$
7 eqid ${⊢}\mathrm{Atoms}\left({K}\right)=\mathrm{Atoms}\left({K}\right)$
8 eqid ${⊢}\mathrm{DVecH}\left({K}\right)\left({W}\right)=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
9 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)$
10 eqid ${⊢}\mathrm{LSAtoms}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)=\mathrm{LSAtoms}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)$
11 1 5 6 7 2 3 4 8 9 10 dihglblem6 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\subseteq {B}\wedge {S}\ne \varnothing \right)\right)\to {I}\left({G}\left({S}\right)\right)=\bigcap _{{x}\in {S}}{I}\left({x}\right)$