Definition df-trl 39019

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

Step	Hyp	Ref	Expression
1		ctrl 39018	. 2 class trL
2		vk	. . 3 setvar 𝑘
3		cvv 3475	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5	2	cv 1541	. . . . 5 class 𝑘
6		clh 38844	. . . . 5 class LHyp
7	5, 6	cfv 6541	. . . 4 class (LHyp‘𝑘)
8		vf	. . . . 5 setvar 𝑓
9	4	cv 1541	. . . . . 6 class 𝑤
10		cltrn 38961	. . . . . . 7 class LTrn
11	5, 10	cfv 6541	. . . . . 6 class (LTrn‘𝑘)
12	9, 11	cfv 6541	. . . . 5 class ((LTrn‘𝑘)‘𝑤)
13		vp	. . . . . . . . . . 11 setvar 𝑝
14	13	cv 1541	. . . . . . . . . 10 class 𝑝
15		cple 17201	. . . . . . . . . . 11 class le
16	5, 15	cfv 6541	. . . . . . . . . 10 class (le‘𝑘)
17	14, 9, 16	wbr 5148	. . . . . . . . 9 wff 𝑝(le‘𝑘)𝑤
18	17	wn 3	. . . . . . . 8 wff ¬ 𝑝(le‘𝑘)𝑤
19		vx	. . . . . . . . . 10 setvar 𝑥
20	19	cv 1541	. . . . . . . . 9 class 𝑥
21	8	cv 1541	. . . . . . . . . . . 12 class 𝑓
22	14, 21	cfv 6541	. . . . . . . . . . 11 class (𝑓‘𝑝)
23		cjn 18261	. . . . . . . . . . . 12 class join
24	5, 23	cfv 6541	. . . . . . . . . . 11 class (join‘𝑘)
25	14, 22, 24	co 7406	. . . . . . . . . 10 class (𝑝(join‘𝑘)(𝑓‘𝑝))
26		cmee 18262	. . . . . . . . . . 11 class meet
27	5, 26	cfv 6541	. . . . . . . . . 10 class (meet‘𝑘)
28	25, 9, 27	co 7406	. . . . . . . . 9 class ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤)
29	20, 28	wceq 1542	. . . . . . . 8 wff 𝑥 = ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤)
30	18, 29	wi 4	. . . . . . 7 wff (¬ 𝑝(le‘𝑘)𝑤 → 𝑥 = ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤))
31		catm 38122	. . . . . . . 8 class Atoms
32	5, 31	cfv 6541	. . . . . . 7 class (Atoms‘𝑘)
33	30, 13, 32	wral 3062	. . . . . 6 wff ∀𝑝 ∈ (Atoms‘𝑘)(¬ 𝑝(le‘𝑘)𝑤 → 𝑥 = ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤))
34		cbs 17141	. . . . . . 7 class Base
35	5, 34	cfv 6541	. . . . . 6 class (Base‘𝑘)
36	33, 19, 35	crio 7361	. . . . 5 class (℩𝑥 ∈ (Base‘𝑘)∀𝑝 ∈ (Atoms‘𝑘)(¬ 𝑝(le‘𝑘)𝑤 → 𝑥 = ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤)))
37	8, 12, 36	cmpt 5231	. . . 4 class (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (℩𝑥 ∈ (Base‘𝑘)∀𝑝 ∈ (Atoms‘𝑘)(¬ 𝑝(le‘𝑘)𝑤 → 𝑥 = ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤))))
38	4, 7, 37	cmpt 5231	. . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (℩𝑥 ∈ (Base‘𝑘)∀𝑝 ∈ (Atoms‘𝑘)(¬ 𝑝(le‘𝑘)𝑤 → 𝑥 = ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤)))))
39	2, 3, 38	cmpt 5231	. 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (℩𝑥 ∈ (Base‘𝑘)∀𝑝 ∈ (Atoms‘𝑘)(¬ 𝑝(le‘𝑘)𝑤 → 𝑥 = ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤))))))
40	1, 39	wceq 1542	1 wff trL = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (℩𝑥 ∈ (Base‘𝑘)∀𝑝 ∈ (Atoms‘𝑘)(¬ 𝑝(le‘𝑘)𝑤 → 𝑥 = ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤))))))

This definition is referenced by:  trlfset  39020