Definition df-trl 38100

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 38099	. 2 class trL
2		vk	. . 3 setvar 𝑘
3		cvv 3422	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5	2	cv 1538	. . . . 5 class 𝑘
6		clh 37925	. . . . 5 class LHyp
7	5, 6	cfv 6418	. . . 4 class (LHyp‘𝑘)
8		vf	. . . . 5 setvar 𝑓
9	4	cv 1538	. . . . . 6 class 𝑤
10		cltrn 38042	. . . . . . 7 class LTrn
11	5, 10	cfv 6418	. . . . . 6 class (LTrn‘𝑘)
12	9, 11	cfv 6418	. . . . 5 class ((LTrn‘𝑘)‘𝑤)
13		vp	. . . . . . . . . . 11 setvar 𝑝
14	13	cv 1538	. . . . . . . . . 10 class 𝑝
15		cple 16895	. . . . . . . . . . 11 class le
16	5, 15	cfv 6418	. . . . . . . . . 10 class (le‘𝑘)
17	14, 9, 16	wbr 5070	. . . . . . . . 9 wff 𝑝(le‘𝑘)𝑤
18	17	wn 3	. . . . . . . 8 wff ¬ 𝑝(le‘𝑘)𝑤
19		vx	. . . . . . . . . 10 setvar 𝑥
20	19	cv 1538	. . . . . . . . 9 class 𝑥
21	8	cv 1538	. . . . . . . . . . . 12 class 𝑓
22	14, 21	cfv 6418	. . . . . . . . . . 11 class (𝑓‘𝑝)
23		cjn 17944	. . . . . . . . . . . 12 class join
24	5, 23	cfv 6418	. . . . . . . . . . 11 class (join‘𝑘)
25	14, 22, 24	co 7255	. . . . . . . . . 10 class (𝑝(join‘𝑘)(𝑓‘𝑝))
26		cmee 17945	. . . . . . . . . . 11 class meet
27	5, 26	cfv 6418	. . . . . . . . . 10 class (meet‘𝑘)
28	25, 9, 27	co 7255	. . . . . . . . 9 class ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤)
29	20, 28	wceq 1539	. . . . . . . 8 wff 𝑥 = ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤)
30	18, 29	wi 4	. . . . . . 7 wff (¬ 𝑝(le‘𝑘)𝑤 → 𝑥 = ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤))
31		catm 37204	. . . . . . . 8 class Atoms
32	5, 31	cfv 6418	. . . . . . 7 class (Atoms‘𝑘)
33	30, 13, 32	wral 3063	. . . . . 6 wff ∀𝑝 ∈ (Atoms‘𝑘)(¬ 𝑝(le‘𝑘)𝑤 → 𝑥 = ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤))
34		cbs 16840	. . . . . . 7 class Base
35	5, 34	cfv 6418	. . . . . 6 class (Base‘𝑘)
36	33, 19, 35	crio 7211	. . . . 5 class (℩𝑥 ∈ (Base‘𝑘)∀𝑝 ∈ (Atoms‘𝑘)(¬ 𝑝(le‘𝑘)𝑤 → 𝑥 = ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤)))
37	8, 12, 36	cmpt 5153	. . . 4 class (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (℩𝑥 ∈ (Base‘𝑘)∀𝑝 ∈ (Atoms‘𝑘)(¬ 𝑝(le‘𝑘)𝑤 → 𝑥 = ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤))))
38	4, 7, 37	cmpt 5153	. . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (℩𝑥 ∈ (Base‘𝑘)∀𝑝 ∈ (Atoms‘𝑘)(¬ 𝑝(le‘𝑘)𝑤 → 𝑥 = ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤)))))
39	2, 3, 38	cmpt 5153	. 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (℩𝑥 ∈ (Base‘𝑘)∀𝑝 ∈ (Atoms‘𝑘)(¬ 𝑝(le‘𝑘)𝑤 → 𝑥 = ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤))))))
40	1, 39	wceq 1539	1 wff trL = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (℩𝑥 ∈ (Base‘𝑘)∀𝑝 ∈ (Atoms‘𝑘)(¬ 𝑝(le‘𝑘)𝑤 → 𝑥 = ((𝑝(join‘𝑘)(𝑓‘𝑝))(meet‘𝑘)𝑤))))))

This definition is referenced by:  trlfset  38101