Theorem isltrn

Description: The predicate "is a lattice translation". Similar to definition of translation in Crawley p. 111. (Contributed by NM, 11-May-2012)

	Ref	Expression
Hypotheses	ltrnset.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	ltrnset.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	ltrnset.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	ltrnset.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	ltrnset.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	ltrnset.d	$$⊢D=\mathrm{LDil}\left(K\right)\left(W\right)$$
	ltrnset.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
Assertion	isltrn	$$⊢\left(K\in B\wedge W\in H\right)\to \left(F\in T\leftrightarrow \left(F\in D\wedge \forall p\in A\forall q\in A\left(\left(\neg p\underset{\dot{}}{\le }W\wedge \neg q\underset{\dot{}}{\le }W\right)\to \left(p\underset{\dot{}}{\vee }F\left(p\right)\right)\underset{\dot{}}{\wedge }W=\left(q\underset{\dot{}}{\vee }F\left(q\right)\right)\underset{\dot{}}{\wedge }W\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ltrnset.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		ltrnset.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		ltrnset.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
4		ltrnset.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		ltrnset.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
6		ltrnset.d	$$⊢D=\mathrm{LDil}\left(K\right)\left(W\right)$$
7		ltrnset.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
8	1 2 3 4 5 6 7	ltrnset	$$⊢\left(K\in B\wedge W\in H\right)\to T=\left\{f\in D|\forall p\in A\forall q\in A\left(\left(\neg p\underset{\dot{}}{\le }W\wedge \neg q\underset{\dot{}}{\le }W\right)\to \left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }W=\left(q\underset{\dot{}}{\vee }f\left(q\right)\right)\underset{\dot{}}{\wedge }W\right)\right\}$$
9	8	eleq2d	$$⊢\left(K\in B\wedge W\in H\right)\to \left(F\in T\leftrightarrow F\in \left\{f\in D|\forall p\in A\forall q\in A\left(\left(\neg p\underset{\dot{}}{\le }W\wedge \neg q\underset{\dot{}}{\le }W\right)\to \left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }W=\left(q\underset{\dot{}}{\vee }f\left(q\right)\right)\underset{\dot{}}{\wedge }W\right)\right\}\right)$$
10		fveq1	$$⊢f=F\to f\left(p\right)=F\left(p\right)$$
11	10	oveq2d	$$⊢f=F\to p\underset{\dot{}}{\vee }f\left(p\right)=p\underset{\dot{}}{\vee }F\left(p\right)$$
12	11	oveq1d	$$⊢f=F\to \left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }W=\left(p\underset{\dot{}}{\vee }F\left(p\right)\right)\underset{\dot{}}{\wedge }W$$
13		fveq1	$$⊢f=F\to f\left(q\right)=F\left(q\right)$$
14	13	oveq2d	$$⊢f=F\to q\underset{\dot{}}{\vee }f\left(q\right)=q\underset{\dot{}}{\vee }F\left(q\right)$$
15	14	oveq1d	$$⊢f=F\to \left(q\underset{\dot{}}{\vee }f\left(q\right)\right)\underset{\dot{}}{\wedge }W=\left(q\underset{\dot{}}{\vee }F\left(q\right)\right)\underset{\dot{}}{\wedge }W$$
16	12 15	eqeq12d	$$⊢f=F\to \left(\left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }W=\left(q\underset{\dot{}}{\vee }f\left(q\right)\right)\underset{\dot{}}{\wedge }W\leftrightarrow \left(p\underset{\dot{}}{\vee }F\left(p\right)\right)\underset{\dot{}}{\wedge }W=\left(q\underset{\dot{}}{\vee }F\left(q\right)\right)\underset{\dot{}}{\wedge }W\right)$$
17	16	imbi2d	$$⊢f=F\to \left(\left(\left(\neg p\underset{\dot{}}{\le }W\wedge \neg q\underset{\dot{}}{\le }W\right)\to \left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }W=\left(q\underset{\dot{}}{\vee }f\left(q\right)\right)\underset{\dot{}}{\wedge }W\right)\leftrightarrow \left(\left(\neg p\underset{\dot{}}{\le }W\wedge \neg q\underset{\dot{}}{\le }W\right)\to \left(p\underset{\dot{}}{\vee }F\left(p\right)\right)\underset{\dot{}}{\wedge }W=\left(q\underset{\dot{}}{\vee }F\left(q\right)\right)\underset{\dot{}}{\wedge }W\right)\right)$$
18	17	2ralbidv	$$⊢f=F\to \left(\forall p\in A\forall q\in A\left(\left(\neg p\underset{\dot{}}{\le }W\wedge \neg q\underset{\dot{}}{\le }W\right)\to \left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }W=\left(q\underset{\dot{}}{\vee }f\left(q\right)\right)\underset{\dot{}}{\wedge }W\right)\leftrightarrow \forall p\in A\forall q\in A\left(\left(\neg p\underset{\dot{}}{\le }W\wedge \neg q\underset{\dot{}}{\le }W\right)\to \left(p\underset{\dot{}}{\vee }F\left(p\right)\right)\underset{\dot{}}{\wedge }W=\left(q\underset{\dot{}}{\vee }F\left(q\right)\right)\underset{\dot{}}{\wedge }W\right)\right)$$
19	18	elrab	$$⊢F\in \left\{f\in D|\forall p\in A\forall q\in A\left(\left(\neg p\underset{\dot{}}{\le }W\wedge \neg q\underset{\dot{}}{\le }W\right)\to \left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }W=\left(q\underset{\dot{}}{\vee }f\left(q\right)\right)\underset{\dot{}}{\wedge }W\right)\right\}\leftrightarrow \left(F\in D\wedge \forall p\in A\forall q\in A\left(\left(\neg p\underset{\dot{}}{\le }W\wedge \neg q\underset{\dot{}}{\le }W\right)\to \left(p\underset{\dot{}}{\vee }F\left(p\right)\right)\underset{\dot{}}{\wedge }W=\left(q\underset{\dot{}}{\vee }F\left(q\right)\right)\underset{\dot{}}{\wedge }W\right)\right)$$
20	9 19	bitrdi	$$⊢\left(K\in B\wedge W\in H\right)\to \left(F\in T\leftrightarrow \left(F\in D\wedge \forall p\in A\forall q\in A\left(\left(\neg p\underset{\dot{}}{\le }W\wedge \neg q\underset{\dot{}}{\le }W\right)\to \left(p\underset{\dot{}}{\vee }F\left(p\right)\right)\underset{\dot{}}{\wedge }W=\left(q\underset{\dot{}}{\vee }F\left(q\right)\right)\underset{\dot{}}{\wedge }W\right)\right)\right)$$