Theorem dihvalb

Description: Value of isomorphism H for a lattice K when X .<_ W . (Contributed by NM, 4-Mar-2014)

	Ref	Expression
Hypotheses	dihvalb.b	$$⊢B={\mathrm{Base}}_K$$
	dihvalb.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	dihvalb.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dihvalb.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
	dihvalb.d	$$⊢D=\mathrm{DIsoB}\left(K\right)\left(W\right)$$
Assertion	dihvalb	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge \left(X\in B\wedge X\underset{\dot{}}{\le }W\right)\right)\to I\left(X\right)=D\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		dihvalb.b	$$⊢B={\mathrm{Base}}_K$$
2		dihvalb.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		dihvalb.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
4		dihvalb.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
5		dihvalb.d	$$⊢D=\mathrm{DIsoB}\left(K\right)\left(W\right)$$
6		eqid	$$⊢\mathrm{join}\left(K\right)=\mathrm{join}\left(K\right)$$
7		eqid	$$⊢\mathrm{meet}\left(K\right)=\mathrm{meet}\left(K\right)$$
8		eqid	$$⊢\mathrm{Atoms}\left(K\right)=\mathrm{Atoms}\left(K\right)$$
9		eqid	$$⊢\mathrm{DIsoC}\left(K\right)\left(W\right)=\mathrm{DIsoC}\left(K\right)\left(W\right)$$
10		eqid	$$⊢\mathrm{DVecH}\left(K\right)\left(W\right)=\mathrm{DVecH}\left(K\right)\left(W\right)$$
11		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)$$
12		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)$$
13	1 2 6 7 8 3 4 5 9 10 11 12	dihval	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge X\in B\right)\to I\left(X\right)=if\left(X\underset{\dot{}}{\le }W,D\left(X\right),\left(\iota u\in \mathrm{LSubSp}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)|\forall q\in \mathrm{Atoms}\left(K\right)\left(\left(\neg q\underset{\dot{}}{\le }W\wedge q\mathrm{join}\left(K\right)\left(X\mathrm{meet}\left(K\right)W\right)=X\right)\to u=\mathrm{DIsoC}\left(K\right)\left(W\right)\left(q\right)\mathrm{LSSum}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)D\left(X\mathrm{meet}\left(K\right)W\right)\right)\right)\right)$$
14		iftrue	$$⊢X\underset{\dot{}}{\le }W\to if\left(X\underset{\dot{}}{\le }W,D\left(X\right),\left(\iota u\in \mathrm{LSubSp}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)|\forall q\in \mathrm{Atoms}\left(K\right)\left(\left(\neg q\underset{\dot{}}{\le }W\wedge q\mathrm{join}\left(K\right)\left(X\mathrm{meet}\left(K\right)W\right)=X\right)\to u=\mathrm{DIsoC}\left(K\right)\left(W\right)\left(q\right)\mathrm{LSSum}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)D\left(X\mathrm{meet}\left(K\right)W\right)\right)\right)\right)=D\left(X\right)$$
15	13 14	sylan9eq	$$⊢\left(\left(\left(K\in V\wedge W\in H\right)\wedge X\in B\right)\wedge X\underset{\dot{}}{\le }W\right)\to I\left(X\right)=D\left(X\right)$$
16	15	anasss	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge \left(X\in B\wedge X\underset{\dot{}}{\le }W\right)\right)\to I\left(X\right)=D\left(X\right)$$