Theorem ltrnfset

Description: The set of all lattice translations for a lattice K . (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)$$
Assertion	ltrnfset	$$⊢K\in C\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)$$

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		elex	$$⊢K\in C\to K\in \mathrm{V}$$
7		fveq2	$$⊢k=K\to \mathrm{LHyp}\left(k\right)=\mathrm{LHyp}\left(K\right)$$
8	7 5	eqtr4di	$$⊢k=K\to \mathrm{LHyp}\left(k\right)=H$$
9		fveq2	$$⊢k=K\to \mathrm{LDil}\left(k\right)=\mathrm{LDil}\left(K\right)$$
10	9	fveq1d	$$⊢k=K\to \mathrm{LDil}\left(k\right)\left(w\right)=\mathrm{LDil}\left(K\right)\left(w\right)$$
11		fveq2	$$⊢k=K\to \mathrm{Atoms}\left(k\right)=\mathrm{Atoms}\left(K\right)$$
12	11 4	eqtr4di	$$⊢k=K\to \mathrm{Atoms}\left(k\right)=A$$
13		fveq2	$$⊢k=K\to {\le }_k={\le }_K$$
14	13 1	eqtr4di	$$⊢k=K\to {\le }_k=\underset{\dot{}}{\le }$$
15	14	breqd	$$⊢k=K\to \left(p{\le }_{k}w\leftrightarrow p\underset{\dot{}}{\le }w\right)$$
16	15	notbid	$$⊢k=K\to \left(\neg p{\le }_{k}w\leftrightarrow \neg p\underset{\dot{}}{\le }w\right)$$
17	14	breqd	$$⊢k=K\to \left(q{\le }_{k}w\leftrightarrow q\underset{\dot{}}{\le }w\right)$$
18	17	notbid	$$⊢k=K\to \left(\neg q{\le }_{k}w\leftrightarrow \neg q\underset{\dot{}}{\le }w\right)$$
19	16 18	anbi12d	$$⊢k=K\to \left(\left(\neg p{\le }_{k}w\wedge \neg q{\le }_{k}w\right)\leftrightarrow \left(\neg p\underset{\dot{}}{\le }w\wedge \neg q\underset{\dot{}}{\le }w\right)\right)$$
20		fveq2	$$⊢k=K\to \mathrm{meet}\left(k\right)=\mathrm{meet}\left(K\right)$$
21	20 3	eqtr4di	$$⊢k=K\to \mathrm{meet}\left(k\right)=\underset{\dot{}}{\wedge }$$
22		fveq2	$$⊢k=K\to \mathrm{join}\left(k\right)=\mathrm{join}\left(K\right)$$
23	22 2	eqtr4di	$$⊢k=K\to \mathrm{join}\left(k\right)=\underset{\dot{}}{\vee }$$
24	23	oveqd	$$⊢k=K\to p\mathrm{join}\left(k\right)f\left(p\right)=p\underset{\dot{}}{\vee }f\left(p\right)$$
25		eqidd	$$⊢k=K\to w=w$$
26	21 24 25	oveq123d	$$⊢k=K\to \left(p\mathrm{join}\left(k\right)f\left(p\right)\right)\mathrm{meet}\left(k\right)w=\left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }w$$
27	23	oveqd	$$⊢k=K\to q\mathrm{join}\left(k\right)f\left(q\right)=q\underset{\dot{}}{\vee }f\left(q\right)$$
28	21 27 25	oveq123d	$$⊢k=K\to \left(q\mathrm{join}\left(k\right)f\left(q\right)\right)\mathrm{meet}\left(k\right)w=\left(q\underset{\dot{}}{\vee }f\left(q\right)\right)\underset{\dot{}}{\wedge }w$$
29	26 28	eqeq12d	$$⊢k=K\to \left(\left(p\mathrm{join}\left(k\right)f\left(p\right)\right)\mathrm{meet}\left(k\right)w=\left(q\mathrm{join}\left(k\right)f\left(q\right)\right)\mathrm{meet}\left(k\right)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)$$
30	19 29	imbi12d	$$⊢k=K\to \left(\left(\left(\neg p{\le }_{k}w\wedge \neg q{\le }_{k}w\right)\to \left(p\mathrm{join}\left(k\right)f\left(p\right)\right)\mathrm{meet}\left(k\right)w=\left(q\mathrm{join}\left(k\right)f\left(q\right)\right)\mathrm{meet}\left(k\right)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)$$
31	12 30	raleqbidv	$$⊢k=K\to \left(\forall q\in \mathrm{Atoms}\left(k\right)\left(\left(\neg p{\le }_{k}w\wedge \neg q{\le }_{k}w\right)\to \left(p\mathrm{join}\left(k\right)f\left(p\right)\right)\mathrm{meet}\left(k\right)w=\left(q\mathrm{join}\left(k\right)f\left(q\right)\right)\mathrm{meet}\left(k\right)w\right)\leftrightarrow \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)$$
32	12 31	raleqbidv	$$⊢k=K\to \left(\forall p\in \mathrm{Atoms}\left(k\right)\forall q\in \mathrm{Atoms}\left(k\right)\left(\left(\neg p{\le }_{k}w\wedge \neg q{\le }_{k}w\right)\to \left(p\mathrm{join}\left(k\right)f\left(p\right)\right)\mathrm{meet}\left(k\right)w=\left(q\mathrm{join}\left(k\right)f\left(q\right)\right)\mathrm{meet}\left(k\right)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)$$
33	10 32	rabeqbidv	$$⊢k=K\to \left\{f\in \mathrm{LDil}\left(k\right)\left(w\right)|\forall p\in \mathrm{Atoms}\left(k\right)\forall q\in \mathrm{Atoms}\left(k\right)\left(\left(\neg p{\le }_{k}w\wedge \neg q{\le }_{k}w\right)\to \left(p\mathrm{join}\left(k\right)f\left(p\right)\right)\mathrm{meet}\left(k\right)w=\left(q\mathrm{join}\left(k\right)f\left(q\right)\right)\mathrm{meet}\left(k\right)w\right)\right\}=\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\}$$
34	8 33	mpteq12dv	$$⊢k=K\to \left(w\in \mathrm{LHyp}\left(k\right)⟼\left\{f\in \mathrm{LDil}\left(k\right)\left(w\right)|\forall p\in \mathrm{Atoms}\left(k\right)\forall q\in \mathrm{Atoms}\left(k\right)\left(\left(\neg p{\le }_{k}w\wedge \neg q{\le }_{k}w\right)\to \left(p\mathrm{join}\left(k\right)f\left(p\right)\right)\mathrm{meet}\left(k\right)w=\left(q\mathrm{join}\left(k\right)f\left(q\right)\right)\mathrm{meet}\left(k\right)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)$$
35		df-ltrn	$$⊢\mathrm{LTrn}=\left(k\in \mathrm{V}⟼\left(w\in \mathrm{LHyp}\left(k\right)⟼\left\{f\in \mathrm{LDil}\left(k\right)\left(w\right)|\forall p\in \mathrm{Atoms}\left(k\right)\forall q\in \mathrm{Atoms}\left(k\right)\left(\left(\neg p{\le }_{k}w\wedge \neg q{\le }_{k}w\right)\to \left(p\mathrm{join}\left(k\right)f\left(p\right)\right)\mathrm{meet}\left(k\right)w=\left(q\mathrm{join}\left(k\right)f\left(q\right)\right)\mathrm{meet}\left(k\right)w\right)\right\}\right)\right)$$
36	34 35 5	mptfvmpt	$$⊢K\in \mathrm{V}\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)$$
37	6 36	syl	$$⊢K\in C\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)$$