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

Definition df-trl 34464
 Description: Define trace of a lattice translation. (Contributed by NM, 20-May-2012.)
Assertion
Ref Expression
df-trl trL = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑥 ∈ (Base‘𝑘)∀𝑝 ∈ (Atoms‘𝑘)(¬ 𝑝(le‘𝑘)𝑤𝑥 = ((𝑝(join‘𝑘)(𝑓𝑝))(meet‘𝑘)𝑤))))))
Distinct variable group:   𝑤,𝑘,𝑓,𝑥,𝑝

Detailed syntax breakdown of Definition df-trl
StepHypRef Expression
1 ctrl 34463 . 2 class trL
2 vk . . 3 setvar 𝑘
3 cvv 3173 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1474 . . . . 5 class 𝑘
6 clh 34288 . . . . 5 class LHyp
75, 6cfv 5804 . . . 4 class (LHyp‘𝑘)
8 vf . . . . 5 setvar 𝑓
94cv 1474 . . . . . 6 class 𝑤
10 cltrn 34405 . . . . . . 7 class LTrn
115, 10cfv 5804 . . . . . 6 class (LTrn‘𝑘)
129, 11cfv 5804 . . . . 5 class ((LTrn‘𝑘)‘𝑤)
13 vp . . . . . . . . . . 11 setvar 𝑝
1413cv 1474 . . . . . . . . . 10 class 𝑝
15 cple 15775 . . . . . . . . . . 11 class le
165, 15cfv 5804 . . . . . . . . . 10 class (le‘𝑘)
1714, 9, 16wbr 4583 . . . . . . . . 9 wff 𝑝(le‘𝑘)𝑤
1817wn 3 . . . . . . . 8 wff ¬ 𝑝(le‘𝑘)𝑤
19 vx . . . . . . . . . 10 setvar 𝑥
2019cv 1474 . . . . . . . . 9 class 𝑥
218cv 1474 . . . . . . . . . . . 12 class 𝑓
2214, 21cfv 5804 . . . . . . . . . . 11 class (𝑓𝑝)
23 cjn 16767 . . . . . . . . . . . 12 class join
245, 23cfv 5804 . . . . . . . . . . 11 class (join‘𝑘)
2514, 22, 24co 6549 . . . . . . . . . 10 class (𝑝(join‘𝑘)(𝑓𝑝))
26 cmee 16768 . . . . . . . . . . 11 class meet
275, 26cfv 5804 . . . . . . . . . 10 class (meet‘𝑘)
2825, 9, 27co 6549 . . . . . . . . 9 class ((𝑝(join‘𝑘)(𝑓𝑝))(meet‘𝑘)𝑤)
2920, 28wceq 1475 . . . . . . . 8 wff 𝑥 = ((𝑝(join‘𝑘)(𝑓𝑝))(meet‘𝑘)𝑤)
3018, 29wi 4 . . . . . . 7 wff 𝑝(le‘𝑘)𝑤𝑥 = ((𝑝(join‘𝑘)(𝑓𝑝))(meet‘𝑘)𝑤))
31 catm 33568 . . . . . . . 8 class Atoms
325, 31cfv 5804 . . . . . . 7 class (Atoms‘𝑘)
3330, 13, 32wral 2896 . . . . . 6 wff 𝑝 ∈ (Atoms‘𝑘)(¬ 𝑝(le‘𝑘)𝑤𝑥 = ((𝑝(join‘𝑘)(𝑓𝑝))(meet‘𝑘)𝑤))
34 cbs 15695 . . . . . . 7 class Base
355, 34cfv 5804 . . . . . 6 class (Base‘𝑘)
3633, 19, 35crio 6510 . . . . 5 class (𝑥 ∈ (Base‘𝑘)∀𝑝 ∈ (Atoms‘𝑘)(¬ 𝑝(le‘𝑘)𝑤𝑥 = ((𝑝(join‘𝑘)(𝑓𝑝))(meet‘𝑘)𝑤)))
378, 12, 36cmpt 4643 . . . 4 class (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑥 ∈ (Base‘𝑘)∀𝑝 ∈ (Atoms‘𝑘)(¬ 𝑝(le‘𝑘)𝑤𝑥 = ((𝑝(join‘𝑘)(𝑓𝑝))(meet‘𝑘)𝑤))))
384, 7, 37cmpt 4643 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑥 ∈ (Base‘𝑘)∀𝑝 ∈ (Atoms‘𝑘)(¬ 𝑝(le‘𝑘)𝑤𝑥 = ((𝑝(join‘𝑘)(𝑓𝑝))(meet‘𝑘)𝑤)))))
392, 3, 38cmpt 4643 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑥 ∈ (Base‘𝑘)∀𝑝 ∈ (Atoms‘𝑘)(¬ 𝑝(le‘𝑘)𝑤𝑥 = ((𝑝(join‘𝑘)(𝑓𝑝))(meet‘𝑘)𝑤))))))
401, 39wceq 1475 1 wff trL = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑥 ∈ (Base‘𝑘)∀𝑝 ∈ (Atoms‘𝑘)(¬ 𝑝(le‘𝑘)𝑤𝑥 = ((𝑝(join‘𝑘)(𝑓𝑝))(meet‘𝑘)𝑤))))))
 Colors of variables: wff setvar class This definition is referenced by:  trlfset  34465
 Copyright terms: Public domain W3C validator