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

Definition df-ltrn 37123
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
StepHypRef Expression
1 cltrn 37119 . 2 class LTrn
2 vk . . 3 setvar 𝑘
3 cvv 3495 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1527 . . . . 5 class 𝑘
6 clh 37002 . . . . 5 class LHyp
75, 6cfv 6349 . . . 4 class (LHyp‘𝑘)
8 vp . . . . . . . . . . . 12 setvar 𝑝
98cv 1527 . . . . . . . . . . 11 class 𝑝
104cv 1527 . . . . . . . . . . 11 class 𝑤
11 cple 16562 . . . . . . . . . . . 12 class le
125, 11cfv 6349 . . . . . . . . . . 11 class (le‘𝑘)
139, 10, 12wbr 5058 . . . . . . . . . 10 wff 𝑝(le‘𝑘)𝑤
1413wn 3 . . . . . . . . 9 wff ¬ 𝑝(le‘𝑘)𝑤
15 vq . . . . . . . . . . . 12 setvar 𝑞
1615cv 1527 . . . . . . . . . . 11 class 𝑞
1716, 10, 12wbr 5058 . . . . . . . . . 10 wff 𝑞(le‘𝑘)𝑤
1817wn 3 . . . . . . . . 9 wff ¬ 𝑞(le‘𝑘)𝑤
1914, 18wa 396 . . . . . . . 8 wff 𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤)
20 vf . . . . . . . . . . . . 13 setvar 𝑓
2120cv 1527 . . . . . . . . . . . 12 class 𝑓
229, 21cfv 6349 . . . . . . . . . . 11 class (𝑓𝑝)
23 cjn 17544 . . . . . . . . . . . 12 class join
245, 23cfv 6349 . . . . . . . . . . 11 class (join‘𝑘)
259, 22, 24co 7145 . . . . . . . . . 10 class (𝑝(join‘𝑘)(𝑓𝑝))
26 cmee 17545 . . . . . . . . . . 11 class meet
275, 26cfv 6349 . . . . . . . . . 10 class (meet‘𝑘)
2825, 10, 27co 7145 . . . . . . . . 9 class ((𝑝(join‘𝑘)(𝑓𝑝))(meet‘𝑘)𝑤)
2916, 21cfv 6349 . . . . . . . . . . 11 class (𝑓𝑞)
3016, 29, 24co 7145 . . . . . . . . . 10 class (𝑞(join‘𝑘)(𝑓𝑞))
3130, 10, 27co 7145 . . . . . . . . 9 class ((𝑞(join‘𝑘)(𝑓𝑞))(meet‘𝑘)𝑤)
3228, 31wceq 1528 . . . . . . . 8 wff ((𝑝(join‘𝑘)(𝑓𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓𝑞))(meet‘𝑘)𝑤)
3319, 32wi 4 . . . . . . 7 wff ((¬ 𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤) → ((𝑝(join‘𝑘)(𝑓𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓𝑞))(meet‘𝑘)𝑤))
34 catm 36281 . . . . . . . 8 class Atoms
355, 34cfv 6349 . . . . . . 7 class (Atoms‘𝑘)
3633, 15, 35wral 3138 . . . . . 6 wff 𝑞 ∈ (Atoms‘𝑘)((¬ 𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤) → ((𝑝(join‘𝑘)(𝑓𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓𝑞))(meet‘𝑘)𝑤))
3736, 8, 35wral 3138 . . . . 5 wff 𝑝 ∈ (Atoms‘𝑘)∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤) → ((𝑝(join‘𝑘)(𝑓𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓𝑞))(meet‘𝑘)𝑤))
38 cldil 37118 . . . . . . 7 class LDil
395, 38cfv 6349 . . . . . 6 class (LDil‘𝑘)
4010, 39cfv 6349 . . . . 5 class ((LDil‘𝑘)‘𝑤)
4137, 20, 40crab 3142 . . . 4 class {𝑓 ∈ ((LDil‘𝑘)‘𝑤) ∣ ∀𝑝 ∈ (Atoms‘𝑘)∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤) → ((𝑝(join‘𝑘)(𝑓𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓𝑞))(meet‘𝑘)𝑤))}
424, 7, 41cmpt 5138 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑓 ∈ ((LDil‘𝑘)‘𝑤) ∣ ∀𝑝 ∈ (Atoms‘𝑘)∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤) → ((𝑝(join‘𝑘)(𝑓𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓𝑞))(meet‘𝑘)𝑤))})
432, 3, 42cmpt 5138 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑓 ∈ ((LDil‘𝑘)‘𝑤) ∣ ∀𝑝 ∈ (Atoms‘𝑘)∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤) → ((𝑝(join‘𝑘)(𝑓𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓𝑞))(meet‘𝑘)𝑤))}))
441, 43wceq 1528 1 wff LTrn = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑓 ∈ ((LDil‘𝑘)‘𝑤) ∣ ∀𝑝 ∈ (Atoms‘𝑘)∀𝑞 ∈ (Atoms‘𝑘)((¬ 𝑝(le‘𝑘)𝑤 ∧ ¬ 𝑞(le‘𝑘)𝑤) → ((𝑝(join‘𝑘)(𝑓𝑝))(meet‘𝑘)𝑤) = ((𝑞(join‘𝑘)(𝑓𝑞))(meet‘𝑘)𝑤))}))
Colors of variables: wff setvar class
This definition is referenced by:  ltrnfset  37135
  Copyright terms: Public domain W3C validator