Theorem ltrnset

Description: The set of lattice translations for a fiducial co-atom W . (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	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\}$$

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	ltrnfset	$$⊢K\in B\to \mathrm{LTrn}\left(K\right)=\left(w\in H⟼\left\{f\in \mathrm{LDil}\left(K\right)\left(w\right)|\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)$$
9	8	fveq1d	$$⊢K\in B\to \mathrm{LTrn}\left(K\right)\left(W\right)=\left(w\in H⟼\left\{f\in \mathrm{LDil}\left(K\right)\left(w\right)|\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)\left(W\right)$$
10	7 9	eqtrid	$$⊢K\in B\to T=\left(w\in H⟼\left\{f\in \mathrm{LDil}\left(K\right)\left(w\right)|\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)\left(W\right)$$
11		fveq2	$$⊢w=W\to \mathrm{LDil}\left(K\right)\left(w\right)=\mathrm{LDil}\left(K\right)\left(W\right)$$
12	11 6	eqtr4di	$$⊢w=W\to \mathrm{LDil}\left(K\right)\left(w\right)=D$$
13		breq2	$$⊢w=W\to \left(p\underset{\dot{}}{\le }w\leftrightarrow p\underset{\dot{}}{\le }W\right)$$
14	13	notbid	$$⊢w=W\to \left(\neg p\underset{\dot{}}{\le }w\leftrightarrow \neg p\underset{\dot{}}{\le }W\right)$$
15		breq2	$$⊢w=W\to \left(q\underset{\dot{}}{\le }w\leftrightarrow q\underset{\dot{}}{\le }W\right)$$
16	15	notbid	$$⊢w=W\to \left(\neg q\underset{\dot{}}{\le }w\leftrightarrow \neg q\underset{\dot{}}{\le }W\right)$$
17	14 16	anbi12d	$$⊢w=W\to \left(\left(\neg p\underset{\dot{}}{\le }w\wedge \neg q\underset{\dot{}}{\le }w\right)\leftrightarrow \left(\neg p\underset{\dot{}}{\le }W\wedge \neg q\underset{\dot{}}{\le }W\right)\right)$$
18		oveq2	$$⊢w=W\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$$
19		oveq2	$$⊢w=W\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$$
20	18 19	eqeq12d	$$⊢w=W\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)$$
21	17 20	imbi12d	$$⊢w=W\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)$$
22	21	2ralbidv	$$⊢w=W\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)$$
23	12 22	rabeqbidv	$$⊢w=W\to \left\{f\in \mathrm{LDil}\left(K\right)\left(w\right)|\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\}=\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\}$$
24		eqid	$$⊢\left(w\in H⟼\left\{f\in \mathrm{LDil}\left(K\right)\left(w\right)|\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)=\left(w\in H⟼\left\{f\in \mathrm{LDil}\left(K\right)\left(w\right)|\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)$$
25	6	fvexi	$$⊢D\in \mathrm{V}$$
26	25	rabex	$$⊢\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\}\in \mathrm{V}$$
27	23 24 26	fvmpt	$$⊢W\in H\to \left(w\in H⟼\left\{f\in \mathrm{LDil}\left(K\right)\left(w\right)|\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)\left(W\right)=\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\}$$
28	10 27	sylan9eq	$$⊢\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\}$$