Theorem dihglblem3aN

Description: Isomorphism H of a lattice glb. (Contributed by NM, 7-Apr-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dihglblem.b	$$⊢B={\mathrm{Base}}_K$$
	dihglblem.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	dihglblem.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	dihglblem.g	$$⊢G=\mathrm{glb}\left(K\right)$$
	dihglblem.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dihglblem.t	$$⊢T=\left\{u\in B|\exists v\in Su=v\underset{\dot{}}{\wedge }W\right\}$$
	dihglblem.i	$$⊢J=\mathrm{DIsoB}\left(K\right)\left(W\right)$$
	dihglblem.ih	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
Assertion	dihglblem3aN	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(S\subseteq B\wedge S\ne \varnothing \right)\wedge G\left(S\right)\underset{\dot{}}{\le }W\right)\to I\left(G\left(S\right)\right)=\bigcap _{x\in T}I\left(x\right)$$

Proof

Step	Hyp	Ref	Expression
1		dihglblem.b	$$⊢B={\mathrm{Base}}_K$$
2		dihglblem.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		dihglblem.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
4		dihglblem.g	$$⊢G=\mathrm{glb}\left(K\right)$$
5		dihglblem.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
6		dihglblem.t	$$⊢T=\left\{u\in B|\exists v\in Su=v\underset{\dot{}}{\wedge }W\right\}$$
7		dihglblem.i	$$⊢J=\mathrm{DIsoB}\left(K\right)\left(W\right)$$
8		dihglblem.ih	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
9	1 2 3 4 5 6	dihglblem2N	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge S\subseteq B\wedge G\left(S\right)\underset{\dot{}}{\le }W\right)\to G\left(S\right)=G\left(T\right)$$
10	9	3adant2r	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(S\subseteq B\wedge S\ne \varnothing \right)\wedge G\left(S\right)\underset{\dot{}}{\le }W\right)\to G\left(S\right)=G\left(T\right)$$
11	10	fveq2d	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(S\subseteq B\wedge S\ne \varnothing \right)\wedge G\left(S\right)\underset{\dot{}}{\le }W\right)\to I\left(G\left(S\right)\right)=I\left(G\left(T\right)\right)$$
12	1 2 3 4 5 6 7 8	dihglblem3N	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(S\subseteq B\wedge S\ne \varnothing \right)\wedge G\left(S\right)\underset{\dot{}}{\le }W\right)\to I\left(G\left(T\right)\right)=\bigcap _{x\in T}I\left(x\right)$$
13	11 12	eqtrd	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(S\subseteq B\wedge S\ne \varnothing \right)\wedge G\left(S\right)\underset{\dot{}}{\le }W\right)\to I\left(G\left(S\right)\right)=\bigcap _{x\in T}I\left(x\right)$$