df-ltrn - Mathbox for Norm Megill

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

Definition df-ltrn 35391

Description: Define set of all lattice translations. Similar to definition of translation in [Crawley] p. 111. (Contributed by NM, 11-May-2012.)

**Assertion**
Ref	Expression
df-ltrn	$/\$

**Detailed syntax breakdown of Definition df-ltrn**
Step	Hyp	Ref	Expression
1		cltrn 35387	. 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		vp	. . . . . . . . . . . 12
9	8	cv 1482	. . . . . . . . . . 11
10	4	cv 1482	. . . . . . . . . . 11
11		cple 15948	. . . . . . . . . . . 12
12	5, 11	cfv 5888	. . . . . . . . . . 11
13	9, 10, 12	wbr 4653	. . . . . . . . . 10
14	13	wn 3	. . . . . . . . 9
15		vq	. . . . . . . . . . . 12
16	15	cv 1482	. . . . . . . . . . 11
17	16, 10, 12	wbr 4653	. . . . . . . . . 10
18	17	wn 3	. . . . . . . . 9
19	14, 18	wa 384	. . . . . . . 8 $/\$
20		vf	. . . . . . . . . . . . 13
21	20	cv 1482	. . . . . . . . . . . 12
22	9, 21	cfv 5888	. . . . . . . . . . 11
23		cjn 16944	. . . . . . . . . . . 12
24	5, 23	cfv 5888	. . . . . . . . . . 11
25	9, 22, 24	co 6650	. . . . . . . . . 10
26		cmee 16945	. . . . . . . . . . 11
27	5, 26	cfv 5888	. . . . . . . . . 10
28	25, 10, 27	co 6650	. . . . . . . . 9
29	16, 21	cfv 5888	. . . . . . . . . . 11
30	16, 29, 24	co 6650	. . . . . . . . . 10
31	30, 10, 27	co 6650	. . . . . . . . 9
32	28, 31	wceq 1483	. . . . . . . 8
33	19, 32	wi 4	. . . . . . 7 $/\$
34		catm 34550	. . . . . . . 8
35	5, 34	cfv 5888	. . . . . . 7
36	33, 15, 35	wral 2912	. . . . . 6 $/\$
37	36, 8, 35	wral 2912	. . . . 5 $/\$
38		cldil 35386	. . . . . . 7
39	5, 38	cfv 5888	. . . . . 6
40	10, 39	cfv 5888	. . . . 5
41	37, 20, 40	crab 2916	. . . 4 $/\$
42	4, 7, 41	cmpt 4729	. . 3 $/\$
43	2, 3, 42	cmpt 4729	. 2 $/\$
44	1, 43	wceq 1483	1 $/\$

Colors of variables: wff setvar class

This definition is referenced by: ltrnfset 35403