df-trl - Mathbox for Norm Megill

	Mathbox for Norm Megill		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-trl		Structured version Visualization version Unicode version

Definition df-trl 35446

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

**Assertion**
Ref	Expression
df-trl

**Detailed syntax breakdown of Definition df-trl**
Step	Hyp	Ref	Expression
1		ctrl 35445	. 2
2		vk	. . 3
3		cvv 3200	. . 3
4		vw	. . . 4
5	2	cv 1482	. . . . 5
6		clh 35270	. . . . 5
7	5, 6	cfv 5888	. . . 4
8		vf	. . . . 5
9	4	cv 1482	. . . . . 6
10		cltrn 35387	. . . . . . 7
11	5, 10	cfv 5888	. . . . . 6
12	9, 11	cfv 5888	. . . . 5
13		vp	. . . . . . . . . . 11
14	13	cv 1482	. . . . . . . . . 10
15		cple 15948	. . . . . . . . . . 11
16	5, 15	cfv 5888	. . . . . . . . . 10
17	14, 9, 16	wbr 4653	. . . . . . . . 9
18	17	wn 3	. . . . . . . 8
19		vx	. . . . . . . . . 10
20	19	cv 1482	. . . . . . . . 9
21	8	cv 1482	. . . . . . . . . . . 12
22	14, 21	cfv 5888	. . . . . . . . . . 11
23		cjn 16944	. . . . . . . . . . . 12
24	5, 23	cfv 5888	. . . . . . . . . . 11
25	14, 22, 24	co 6650	. . . . . . . . . 10
26		cmee 16945	. . . . . . . . . . 11
27	5, 26	cfv 5888	. . . . . . . . . 10
28	25, 9, 27	co 6650	. . . . . . . . 9
29	20, 28	wceq 1483	. . . . . . . 8
30	18, 29	wi 4	. . . . . . 7
31		catm 34550	. . . . . . . 8
32	5, 31	cfv 5888	. . . . . . 7
33	30, 13, 32	wral 2912	. . . . . 6
34		cbs 15857	. . . . . . 7
35	5, 34	cfv 5888	. . . . . 6
36	33, 19, 35	crio 6610	. . . . 5
37	8, 12, 36	cmpt 4729	. . . 4
38	4, 7, 37	cmpt 4729	. . 3
39	2, 3, 38	cmpt 4729	. 2
40	1, 39	wceq 1483	1

Colors of variables: wff setvar class

This definition is referenced by: trlfset 35447