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)$$