Theorem dihvalcq

Description: Value of isomorphism H for a lattice K when -. X .<_ W , given auxiliary atom Q . TODO: Use dihvalcq2 (with lhpmcvr3 for ( Q .\/ ( X ./\ W ) ) = X simplification) that changes C and D to I and make this obsolete. Do to other theorems as well. (Contributed by NM, 6-Mar-2014)

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

Proof

Step	Hyp	Ref	Expression
1		dihvalcq.b	$$⊢B={\mathrm{Base}}_K$$
2		dihvalcq.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		dihvalcq.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		dihvalcq.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
5		dihvalcq.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
6		dihvalcq.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
7		dihvalcq.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
8		dihvalcq.d	$$⊢D=\mathrm{DIsoB}\left(K\right)\left(W\right)$$
9		dihvalcq.c	$$⊢C=\mathrm{DIsoC}\left(K\right)\left(W\right)$$
10		dihvalcq.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
11		dihvalcq.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
12		eqid	$$⊢\mathrm{LSubSp}\left(U\right)=\mathrm{LSubSp}\left(U\right)$$
13	1 2 3 4 5 6 7 8 9 10 12 11	dihvalcqpre	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\wedge \left(\left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge Q\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\right)\to I\left(X\right)=C\left(Q\right)\underset{\dot{}}{\oplus }D\left(X\underset{\dot{}}{\wedge }W\right)$$