Definition df-ltrn 40107

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	⊢ LTrn = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑓 ∈ ((LDil‘𝑘)‘𝑤) ∣ ∀𝑝 ∈ (Atoms‘𝑘)∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤) → ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓‘𝑞))(meet‘𝑘)𝑤))}))

Distinct variable group:   𝑤,𝑘,𝑓,𝑝,𝑞

Detailed syntax breakdown of Definition df-ltrn

Step	Hyp	Ref	Expression
1		cltrn 40103	. 2 class LTrn
2		vk	. . 3 setvar 𝑘
3		cvv 3480	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5	2	cv 1539	. . . . 5 class 𝑘
6		clh 39986	. . . . 5 class LHyp
7	5, 6	cfv 6561	. . . 4 class (LHyp‘𝑘)
8		vp	. . . . . . . . . . . 12 setvar 𝑝
9	8	cv 1539	. . . . . . . . . . 11 class 𝑝
10	4	cv 1539	. . . . . . . . . . 11 class 𝑤
11		cple 17304	. . . . . . . . . . . 12 class le
12	5, 11	cfv 6561	. . . . . . . . . . 11 class (le‘𝑘)
13	9, 10, 12	wbr 5143	. . . . . . . . . 10 wff 𝑝(le‘𝑘)𝑤
14	13	wn 3	. . . . . . . . 9 wff ¬ 𝑝(le‘𝑘)𝑤
15		vq	. . . . . . . . . . . 12 setvar 𝑞
16	15	cv 1539	. . . . . . . . . . 11 class 𝑞
17	16, 10, 12	wbr 5143	. . . . . . . . . 10 wff 𝑞(le‘𝑘)𝑤
18	17	wn 3	. . . . . . . . 9 wff ¬ 𝑞(le‘𝑘)𝑤
19	14, 18	wa 395	. . . . . . . 8 wff (¬ 𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤)
20		vf	. . . . . . . . . . . . 13 setvar 𝑓
21	20	cv 1539	. . . . . . . . . . . 12 class 𝑓
22	9, 21	cfv 6561	. . . . . . . . . . 11 class (𝑓‘𝑝)
23		cjn 18357	. . . . . . . . . . . 12 class join
24	5, 23	cfv 6561	. . . . . . . . . . 11 class (join‘𝑘)
25	9, 22, 24	co 7431	. . . . . . . . . 10 class (𝑝(join‘𝑘)(𝑓‘𝑝))
26		cmee 18358	. . . . . . . . . . 11 class meet
27	5, 26	cfv 6561	. . . . . . . . . 10 class (meet‘𝑘)
28	25, 10, 27	co 7431	. . . . . . . . 9 class ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤)
29	16, 21	cfv 6561	. . . . . . . . . . 11 class (𝑓‘𝑞)
30	16, 29, 24	co 7431	. . . . . . . . . 10 class (𝑞(join‘𝑘)(𝑓‘𝑞))
31	30, 10, 27	co 7431	. . . . . . . . 9 class ((𝑞(join‘𝑘)(𝑓‘𝑞))(meet‘𝑘)𝑤)
32	28, 31	wceq 1540	. . . . . . . 8 wff ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓‘𝑞))(meet‘𝑘)𝑤)
33	19, 32	wi 4	. . . . . . 7 wff ((¬ 𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤) → ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓‘𝑞))(meet‘𝑘)𝑤))
34		catm 39264	. . . . . . . 8 class Atoms
35	5, 34	cfv 6561	. . . . . . 7 class (Atoms‘𝑘)
36	33, 15, 35	wral 3061	. . . . . 6 wff ∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤) → ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓‘𝑞))(meet‘𝑘)𝑤))
37	36, 8, 35	wral 3061	. . . . 5 wff ∀𝑝 ∈ (Atoms‘𝑘)∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤) → ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓‘𝑞))(meet‘𝑘)𝑤))
38		cldil 40102	. . . . . . 7 class LDil
39	5, 38	cfv 6561	. . . . . 6 class (LDil‘𝑘)
40	10, 39	cfv 6561	. . . . 5 class ((LDil‘𝑘)‘𝑤)
41	37, 20, 40	crab 3436	. . . 4 class {𝑓 ∈ ((LDil‘𝑘)‘𝑤) ∣ ∀𝑝 ∈ (Atoms‘𝑘)∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤) → ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓‘𝑞))(meet‘𝑘)𝑤))}
42	4, 7, 41	cmpt 5225	. . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑓 ∈ ((LDil‘𝑘)‘𝑤) ∣ ∀𝑝 ∈ (Atoms‘𝑘)∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤) → ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓‘𝑞))(meet‘𝑘)𝑤))})
43	2, 3, 42	cmpt 5225	. 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑓 ∈ ((LDil‘𝑘)‘𝑤) ∣ ∀𝑝 ∈ (Atoms‘𝑘)∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤) → ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓‘𝑞))(meet‘𝑘)𝑤))}))
44	1, 43	wceq 1540	1 wff LTrn = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑓 ∈ ((LDil‘𝑘)‘𝑤) ∣ ∀𝑝 ∈ (Atoms‘𝑘)∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤) → ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓‘𝑞))(meet‘𝑘)𝑤))}))

This definition is referenced by:  ltrnfset  40119