Definition df-trl

Description: Define trace of a lattice translation. (Contributed by NM, 20-May-2012)

	Ref	Expression
Assertion	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)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctrl	$$class\mathrm{trL}$$
1		vk	$$setvark$$
2		cvv	$$class\mathrm{V}$$
3		vw	$$setvarw$$
4		clh	$$class\mathrm{LHyp}$$
5	1	cv	$$setvark$$
6	5 4	cfv	$$class\mathrm{LHyp}\left(k\right)$$
7		vf	$$setvarf$$
8		cltrn	$$class\mathrm{LTrn}$$
9	5 8	cfv	$$class\mathrm{LTrn}\left(k\right)$$
10	3	cv	$$setvarw$$
11	10 9	cfv	$$class\mathrm{LTrn}\left(k\right)\left(w\right)$$
12		vx	$$setvarx$$
13		cbs	$$class\mathrm{Base}$$
14	5 13	cfv	$$class{\mathrm{Base}}_k$$
15		vp	$$setvarp$$
16		catm	$$class\mathrm{Atoms}$$
17	5 16	cfv	$$class\mathrm{Atoms}\left(k\right)$$
18	15	cv	$$setvarp$$
19		cple	$$class\mathrm{le}$$
20	5 19	cfv	$$class{\le }_k$$
21	18 10 20	wbr	$$wffp{\le }_{k}w$$
22	21	wn	$$wff\neg p{\le }_{k}w$$
23	12	cv	$$setvarx$$
24		cjn	$$class\mathrm{join}$$
25	5 24	cfv	$$class\mathrm{join}\left(k\right)$$
26	7	cv	$$setvarf$$
27	18 26	cfv	$$classf\left(p\right)$$
28	18 27 25	co	$$class\left(p\mathrm{join}\left(k\right)f\left(p\right)\right)$$
29		cmee	$$class\mathrm{meet}$$
30	5 29	cfv	$$class\mathrm{meet}\left(k\right)$$
31	28 10 30	co	$$class\left(\left(p\mathrm{join}\left(k\right)f\left(p\right)\right)\mathrm{meet}\left(k\right)w\right)$$
32	23 31	wceq	$$wffx=\left(p\mathrm{join}\left(k\right)f\left(p\right)\right)\mathrm{meet}\left(k\right)w$$
33	22 32	wi	$$wff\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)$$
34	33 15 17	wral	$$wff\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)$$
35	34 12 14	crio	$$class\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)$$
36	7 11 35	cmpt	$$class\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)$$
37	3 6 36	cmpt	$$class\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)$$
38	1 2 37	cmpt	$$class\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)$$
39	0 38	wceq	$$wff\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)$$