Theorem dihopelvalc

Description: Member of value of isomorphism H for a lattice K when -. X .<_ W , given auxiliary atom Q . (Contributed by NM, 13-Mar-2014)

	Ref	Expression
Hypotheses	dihopelvalcp.b	$$⊢B={\mathrm{Base}}_K$$
	dihopelvalcp.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	dihopelvalcp.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	dihopelvalcp.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	dihopelvalcp.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	dihopelvalcp.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dihopelvalcp.p	$$⊢P=\mathrm{oc}\left(K\right)\left(W\right)$$
	dihopelvalcp.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	dihopelvalcp.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
	dihopelvalcp.e	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
	dihopelvalcp.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
	dihopelvalcp.g	$$⊢G=\left(\iota g\in T|g\left(P\right)=Q\right)$$
	dihopelvalcp.f	$$⊢F\in \mathrm{V}$$
	dihopelvalcp.s	$$⊢S\in \mathrm{V}$$
Assertion	dihopelvalc	$$⊢\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 \left(⟨F,S⟩\in I\left(X\right)\leftrightarrow \left(\left(F\in T\wedge S\in E\right)\wedge R\left(F\circ {S\left(G\right)}^{-1}\right)\underset{\dot{}}{\le }X\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dihopelvalcp.b	$$⊢B={\mathrm{Base}}_K$$
2		dihopelvalcp.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		dihopelvalcp.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		dihopelvalcp.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
5		dihopelvalcp.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
6		dihopelvalcp.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
7		dihopelvalcp.p	$$⊢P=\mathrm{oc}\left(K\right)\left(W\right)$$
8		dihopelvalcp.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
9		dihopelvalcp.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
10		dihopelvalcp.e	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
11		dihopelvalcp.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
12		dihopelvalcp.g	$$⊢G=\left(\iota g\in T|g\left(P\right)=Q\right)$$
13		dihopelvalcp.f	$$⊢F\in \mathrm{V}$$
14		dihopelvalcp.s	$$⊢S\in \mathrm{V}$$
15		eqid	$$⊢\left(h\in T⟼{\mathrm{I}\upharpoonright }_B\right)=\left(h\in T⟼{\mathrm{I}\upharpoonright }_B\right)$$
16		eqid	$$⊢\mathrm{DIsoB}\left(K\right)\left(W\right)=\mathrm{DIsoB}\left(K\right)\left(W\right)$$
17		eqid	$$⊢\mathrm{DIsoC}\left(K\right)\left(W\right)=\mathrm{DIsoC}\left(K\right)\left(W\right)$$
18		eqid	$$⊢\mathrm{DVecH}\left(K\right)\left(W\right)=\mathrm{DVecH}\left(K\right)\left(W\right)$$
19		eqid	$$⊢{+}_{\mathrm{DVecH}\left(K\right)\left(W\right)}={+}_{\mathrm{DVecH}\left(K\right)\left(W\right)}$$
20		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)$$
21		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)$$
22		eqid	$$⊢\left(a\in E,b\in E⟼\left(h\in T⟼a\left(h\right)\circ b\left(h\right)\right)\right)=\left(a\in E,b\in E⟼\left(h\in T⟼a\left(h\right)\circ b\left(h\right)\right)\right)$$
23	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22	dihopelvalcpre	$$⊢\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 \left(⟨F,S⟩\in I\left(X\right)\leftrightarrow \left(\left(F\in T\wedge S\in E\right)\wedge R\left(F\circ {S\left(G\right)}^{-1}\right)\underset{\dot{}}{\le }X\right)\right)$$