Theorem trlfset

Description: The set of all traces of lattice translations for a lattice K . (Contributed by NM, 20-May-2012)

	Ref	Expression
Hypotheses	trlset.b	$$⊢B={\mathrm{Base}}_K$$
	trlset.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	trlset.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	trlset.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	trlset.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	trlset.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
Assertion	trlfset	$$⊢K\in C\to \mathrm{trL}\left(K\right)=\left(w\in H⟼\left(f\in \mathrm{LTrn}\left(K\right)\left(w\right)⟼\left(\iota x\in B|\forall p\in A\left(\neg p\underset{\dot{}}{\le }w\to x=\left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }w\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		trlset.b	$$⊢B={\mathrm{Base}}_K$$
2		trlset.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		trlset.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		trlset.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
5		trlset.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
6		trlset.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
7		elex	$$⊢K\in C\to K\in \mathrm{V}$$
8		fveq2	$$⊢k=K\to \mathrm{LHyp}\left(k\right)=\mathrm{LHyp}\left(K\right)$$
9	8 6	eqtr4di	$$⊢k=K\to \mathrm{LHyp}\left(k\right)=H$$
10		fveq2	$$⊢k=K\to \mathrm{LTrn}\left(k\right)=\mathrm{LTrn}\left(K\right)$$
11	10	fveq1d	$$⊢k=K\to \mathrm{LTrn}\left(k\right)\left(w\right)=\mathrm{LTrn}\left(K\right)\left(w\right)$$
12		fveq2	$$⊢k=K\to {\mathrm{Base}}_k={\mathrm{Base}}_K$$
13	12 1	eqtr4di	$$⊢k=K\to {\mathrm{Base}}_k=B$$
14		fveq2	$$⊢k=K\to \mathrm{Atoms}\left(k\right)=\mathrm{Atoms}\left(K\right)$$
15	14 5	eqtr4di	$$⊢k=K\to \mathrm{Atoms}\left(k\right)=A$$
16		fveq2	$$⊢k=K\to {\le }_k={\le }_K$$
17	16 2	eqtr4di	$$⊢k=K\to {\le }_k=\underset{\dot{}}{\le }$$
18	17	breqd	$$⊢k=K\to \left(p{\le }_{k}w\leftrightarrow p\underset{\dot{}}{\le }w\right)$$
19	18	notbid	$$⊢k=K\to \left(\neg p{\le }_{k}w\leftrightarrow \neg p\underset{\dot{}}{\le }w\right)$$
20		fveq2	$$⊢k=K\to \mathrm{meet}\left(k\right)=\mathrm{meet}\left(K\right)$$
21	20 4	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 3	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	26	eqeq2d	$$⊢k=K\to \left(x=\left(p\mathrm{join}\left(k\right)f\left(p\right)\right)\mathrm{meet}\left(k\right)w\leftrightarrow x=\left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }w\right)$$
28	19 27	imbi12d	$$⊢k=K\to \left(\left(\neg p{\le }_{k}w\to x=\left(p\mathrm{join}\left(k\right)f\left(p\right)\right)\mathrm{meet}\left(k\right)w\right)\leftrightarrow \left(\neg p\underset{\dot{}}{\le }w\to x=\left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }w\right)\right)$$
29	15 28	raleqbidv	$$⊢k=K\to \left(\forall p\in \mathrm{Atoms}\left(k\right)\left(\neg p{\le }_{k}w\to x=\left(p\mathrm{join}\left(k\right)f\left(p\right)\right)\mathrm{meet}\left(k\right)w\right)\leftrightarrow \forall p\in A\left(\neg p\underset{\dot{}}{\le }w\to x=\left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }w\right)\right)$$
30	13 29	riotaeqbidv	$$⊢k=K\to \left(\iota x\in {\mathrm{Base}}_k|\forall p\in \mathrm{Atoms}\left(k\right)\left(\neg p{\le }_{k}w\to x=\left(p\mathrm{join}\left(k\right)f\left(p\right)\right)\mathrm{meet}\left(k\right)w\right)\right)=\left(\iota x\in B|\forall p\in A\left(\neg p\underset{\dot{}}{\le }w\to x=\left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }w\right)\right)$$
31	11 30	mpteq12dv	$$⊢k=K\to \left(f\in \mathrm{LTrn}\left(k\right)\left(w\right)⟼\left(\iota x\in {\mathrm{Base}}_k|\forall p\in \mathrm{Atoms}\left(k\right)\left(\neg p{\le }_{k}w\to x=\left(p\mathrm{join}\left(k\right)f\left(p\right)\right)\mathrm{meet}\left(k\right)w\right)\right)\right)=\left(f\in \mathrm{LTrn}\left(K\right)\left(w\right)⟼\left(\iota x\in B|\forall p\in A\left(\neg p\underset{\dot{}}{\le }w\to x=\left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }w\right)\right)\right)$$
32	9 31	mpteq12dv	$$⊢k=K\to \left(w\in \mathrm{LHyp}\left(k\right)⟼\left(f\in \mathrm{LTrn}\left(k\right)\left(w\right)⟼\left(\iota x\in {\mathrm{Base}}_k|\forall p\in \mathrm{Atoms}\left(k\right)\left(\neg p{\le }_{k}w\to x=\left(p\mathrm{join}\left(k\right)f\left(p\right)\right)\mathrm{meet}\left(k\right)w\right)\right)\right)\right)=\left(w\in H⟼\left(f\in \mathrm{LTrn}\left(K\right)\left(w\right)⟼\left(\iota x\in B|\forall p\in A\left(\neg p\underset{\dot{}}{\le }w\to x=\left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }w\right)\right)\right)\right)$$
33		df-trl	$$⊢\mathrm{trL}=\left(k\in \mathrm{V}⟼\left(w\in \mathrm{LHyp}\left(k\right)⟼\left(f\in \mathrm{LTrn}\left(k\right)\left(w\right)⟼\left(\iota x\in {\mathrm{Base}}_k|\forall p\in \mathrm{Atoms}\left(k\right)\left(\neg p{\le }_{k}w\to x=\left(p\mathrm{join}\left(k\right)f\left(p\right)\right)\mathrm{meet}\left(k\right)w\right)\right)\right)\right)\right)$$
34	32 33 6	mptfvmpt	$$⊢K\in \mathrm{V}\to \mathrm{trL}\left(K\right)=\left(w\in H⟼\left(f\in \mathrm{LTrn}\left(K\right)\left(w\right)⟼\left(\iota x\in B|\forall p\in A\left(\neg p\underset{\dot{}}{\le }w\to x=\left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }w\right)\right)\right)\right)$$
35	7 34	syl	$$⊢K\in C\to \mathrm{trL}\left(K\right)=\left(w\in H⟼\left(f\in \mathrm{LTrn}\left(K\right)\left(w\right)⟼\left(\iota x\in B|\forall p\in A\left(\neg p\underset{\dot{}}{\le }w\to x=\left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }w\right)\right)\right)\right)$$