Users' Mathboxes 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 34247
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 34246 . 2 class trL
2 vk . . 3 setvar 𝑘
3 cvv 3172 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1473 . . . . 5 class 𝑘
6 clh 34071 . . . . 5 class LHyp
75, 6cfv 5789 . . . 4 class (LHyp‘𝑘)
8 vf . . . . 5 setvar 𝑓
94cv 1473 . . . . . 6 class 𝑤
10 cltrn 34188 . . . . . . 7 class LTrn
115, 10cfv 5789 . . . . . 6 class (LTrn‘𝑘)
129, 11cfv 5789 . . . . 5 class ((LTrn‘𝑘)‘𝑤)
13 vp . . . . . . . . . . 11 setvar 𝑝
1413cv 1473 . . . . . . . . . 10 class 𝑝
15 cple 15723 . . . . . . . . . . 11 class le
165, 15cfv 5789 . . . . . . . . . 10 class (le‘𝑘)
1714, 9, 16wbr 4577 . . . . . . . . 9 wff 𝑝(le‘𝑘)𝑤
1817wn 3 . . . . . . . 8 wff ¬ 𝑝(le‘𝑘)𝑤
19 vx . . . . . . . . . 10 setvar 𝑥
2019cv 1473 . . . . . . . . 9 class 𝑥
218cv 1473 . . . . . . . . . . . 12 class 𝑓
2214, 21cfv 5789 . . . . . . . . . . 11 class (𝑓𝑝)
23 cjn 16715 . . . . . . . . . . . 12 class join
245, 23cfv 5789 . . . . . . . . . . 11 class (join‘𝑘)
2514, 22, 24co 6526 . . . . . . . . . 10 class (𝑝(join‘𝑘)(𝑓𝑝))
26 cmee 16716 . . . . . . . . . . 11 class meet
275, 26cfv 5789 . . . . . . . . . 10 class (meet‘𝑘)
2825, 9, 27co 6526 . . . . . . . . 9 class ((𝑝(join‘𝑘)(𝑓𝑝))(meet‘𝑘)𝑤)
2920, 28wceq 1474 . . . . . . . 8 wff 𝑥 = ((𝑝(join‘𝑘)(𝑓𝑝))(meet‘𝑘)𝑤)
3018, 29wi 4 . . . . . . 7 wff 𝑝(le‘𝑘)𝑤𝑥 = ((𝑝(join‘𝑘)(𝑓𝑝))(meet‘𝑘)𝑤))
31 catm 33351 . . . . . . . 8 class Atoms
325, 31cfv 5789 . . . . . . 7 class (Atoms‘𝑘)
3330, 13, 32wral 2895 . . . . . 6 wff 𝑝 ∈ (Atoms‘𝑘)(¬ 𝑝(le‘𝑘)𝑤𝑥 = ((𝑝(join‘𝑘)(𝑓𝑝))(meet‘𝑘)𝑤))
34 cbs 15643 . . . . . . 7 class Base
355, 34cfv 5789 . . . . . 6 class (Base‘𝑘)
3633, 19, 35crio 6487 . . . . 5 class (𝑥 ∈ (Base‘𝑘)∀𝑝 ∈ (Atoms‘𝑘)(¬ 𝑝(le‘𝑘)𝑤𝑥 = ((𝑝(join‘𝑘)(𝑓𝑝))(meet‘𝑘)𝑤)))
378, 12, 36cmpt 4637 . . . 4 class (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑥 ∈ (Base‘𝑘)∀𝑝 ∈ (Atoms‘𝑘)(¬ 𝑝(le‘𝑘)𝑤𝑥 = ((𝑝(join‘𝑘)(𝑓𝑝))(meet‘𝑘)𝑤))))
384, 7, 37cmpt 4637 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑥 ∈ (Base‘𝑘)∀𝑝 ∈ (Atoms‘𝑘)(¬ 𝑝(le‘𝑘)𝑤𝑥 = ((𝑝(join‘𝑘)(𝑓𝑝))(meet‘𝑘)𝑤)))))
392, 3, 38cmpt 4637 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑥 ∈ (Base‘𝑘)∀𝑝 ∈ (Atoms‘𝑘)(¬ 𝑝(le‘𝑘)𝑤𝑥 = ((𝑝(join‘𝑘)(𝑓𝑝))(meet‘𝑘)𝑤))))))
401, 39wceq 1474 1 wff trL = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑥 ∈ (Base‘𝑘)∀𝑝 ∈ (Atoms‘𝑘)(¬ 𝑝(le‘𝑘)𝑤𝑥 = ((𝑝(join‘𝑘)(𝑓𝑝))(meet‘𝑘)𝑤))))))
Colors of variables: wff setvar class
This definition is referenced by:  trlfset  34248
  Copyright terms: Public domain W3C validator