Theorem dicval2

Description: The partial isomorphism C for a lattice K . (Contributed by NM, 20-Feb-2014)

	Ref	Expression
Hypotheses	dicval.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	dicval.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	dicval.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dicval.p	$$⊢P=\mathrm{oc}\left(K\right)\left(W\right)$$
	dicval.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	dicval.e	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
	dicval.i	$$⊢I=\mathrm{DIsoC}\left(K\right)\left(W\right)$$
	dicval2.g	$$⊢G=\left(\iota g\in T|g\left(P\right)=Q\right)$$
Assertion	dicval2	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\to I\left(Q\right)=\left\{⟨f,s⟩|\left(f=s\left(G\right)\wedge s\in E\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dicval.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		dicval.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
3		dicval.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
4		dicval.p	$$⊢P=\mathrm{oc}\left(K\right)\left(W\right)$$
5		dicval.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
6		dicval.e	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
7		dicval.i	$$⊢I=\mathrm{DIsoC}\left(K\right)\left(W\right)$$
8		dicval2.g	$$⊢G=\left(\iota g\in T|g\left(P\right)=Q\right)$$
9	1 2 3 4 5 6 7	dicval	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\to I\left(Q\right)=\left\{⟨f,s⟩|\left(f=s\left(\left(\iota g\in T|g\left(P\right)=Q\right)\right)\wedge s\in E\right)\right\}$$
10	8	fveq2i	$$⊢s\left(G\right)=s\left(\left(\iota g\in T|g\left(P\right)=Q\right)\right)$$
11	10	eqeq2i	$$⊢f=s\left(G\right)\leftrightarrow f=s\left(\left(\iota g\in T|g\left(P\right)=Q\right)\right)$$
12	11	anbi1i	$$⊢\left(f=s\left(G\right)\wedge s\in E\right)\leftrightarrow \left(f=s\left(\left(\iota g\in T|g\left(P\right)=Q\right)\right)\wedge s\in E\right)$$
13	12	opabbii	$$⊢\left\{⟨f,s⟩|\left(f=s\left(G\right)\wedge s\in E\right)\right\}=\left\{⟨f,s⟩|\left(f=s\left(\left(\iota g\in T|g\left(P\right)=Q\right)\right)\wedge s\in E\right)\right\}$$
14	9 13	eqtr4di	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\to I\left(Q\right)=\left\{⟨f,s⟩|\left(f=s\left(G\right)\wedge s\in E\right)\right\}$$