Theorem dihvalc

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

	Ref	Expression
Hypotheses	dihval.b	$$⊢B={\mathrm{Base}}_K$$
	dihval.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	dihval.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	dihval.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	dihval.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	dihval.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dihval.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
	dihval.d	$$⊢D=\mathrm{DIsoB}\left(K\right)\left(W\right)$$
	dihval.c	$$⊢C=\mathrm{DIsoC}\left(K\right)\left(W\right)$$
	dihval.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	dihval.s	$$⊢S=\mathrm{LSubSp}\left(U\right)$$
	dihval.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
Assertion	dihvalc	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\to I\left(X\right)=\left(\iota u\in S|\forall q\in A\left(\left(\neg q\underset{\dot{}}{\le }W\wedge q\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\to u=C\left(q\right)\underset{\dot{}}{\oplus }D\left(X\underset{\dot{}}{\wedge }W\right)\right)\right)$$

Proof

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