Definition df-trl

Description: Define trace of a lattice translation. (Contributed by NM, 20-May-2012)

	Ref	Expression
Assertion	df-trl	⊢ trL = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ℩ 𝑥 ∈ ( Base ‘ 𝑘 ) ∀ 𝑝 ∈ ( Atoms ‘ 𝑘 ) ( ¬ 𝑝 ( le ‘ 𝑘 ) 𝑤 → 𝑥 = ( ( 𝑝 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑝 ) ) ( meet ‘ 𝑘 ) 𝑤 ) ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctrl	⊢ trL
1		vk	⊢ 𝑘
2		cvv	⊢ V
3		vw	⊢ 𝑤
4		clh	⊢ LHyp
5	1	cv	⊢ 𝑘
6	5 4	cfv	⊢ ( LHyp ‘ 𝑘 )
7		vf	⊢ 𝑓
8		cltrn	⊢ LTrn
9	5 8	cfv	⊢ ( LTrn ‘ 𝑘 )
10	3	cv	⊢ 𝑤
11	10 9	cfv	⊢ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 )
12		vx	⊢ 𝑥
13		cbs	⊢ Base
14	5 13	cfv	⊢ ( Base ‘ 𝑘 )
15		vp	⊢ 𝑝
16		catm	⊢ Atoms
17	5 16	cfv	⊢ ( Atoms ‘ 𝑘 )
18	15	cv	⊢ 𝑝
19		cple	⊢ le
20	5 19	cfv	⊢ ( le ‘ 𝑘 )
21	18 10 20	wbr	⊢ 𝑝 ( le ‘ 𝑘 ) 𝑤
22	21	wn	⊢ ¬ 𝑝 ( le ‘ 𝑘 ) 𝑤
23	12	cv	⊢ 𝑥
24		cjn	⊢ join
25	5 24	cfv	⊢ ( join ‘ 𝑘 )
26	7	cv	⊢ 𝑓
27	18 26	cfv	⊢ ( 𝑓 ‘ 𝑝 )
28	18 27 25	co	⊢ ( 𝑝 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑝 ) )
29		cmee	⊢ meet
30	5 29	cfv	⊢ ( meet ‘ 𝑘 )
31	28 10 30	co	⊢ ( ( 𝑝 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑝 ) ) ( meet ‘ 𝑘 ) 𝑤 )
32	23 31	wceq	⊢ 𝑥 = ( ( 𝑝 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑝 ) ) ( meet ‘ 𝑘 ) 𝑤 )
33	22 32	wi	⊢ ( ¬ 𝑝 ( le ‘ 𝑘 ) 𝑤 → 𝑥 = ( ( 𝑝 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑝 ) ) ( meet ‘ 𝑘 ) 𝑤 ) )
34	33 15 17	wral	⊢ ∀ 𝑝 ∈ ( Atoms ‘ 𝑘 ) ( ¬ 𝑝 ( le ‘ 𝑘 ) 𝑤 → 𝑥 = ( ( 𝑝 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑝 ) ) ( meet ‘ 𝑘 ) 𝑤 ) )
35	34 12 14	crio	⊢ ( ℩ 𝑥 ∈ ( Base ‘ 𝑘 ) ∀ 𝑝 ∈ ( Atoms ‘ 𝑘 ) ( ¬ 𝑝 ( le ‘ 𝑘 ) 𝑤 → 𝑥 = ( ( 𝑝 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑝 ) ) ( meet ‘ 𝑘 ) 𝑤 ) ) )
36	7 11 35	cmpt	⊢ ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ℩ 𝑥 ∈ ( Base ‘ 𝑘 ) ∀ 𝑝 ∈ ( Atoms ‘ 𝑘 ) ( ¬ 𝑝 ( le ‘ 𝑘 ) 𝑤 → 𝑥 = ( ( 𝑝 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑝 ) ) ( meet ‘ 𝑘 ) 𝑤 ) ) ) )
37	3 6 36	cmpt	⊢ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ℩ 𝑥 ∈ ( Base ‘ 𝑘 ) ∀ 𝑝 ∈ ( Atoms ‘ 𝑘 ) ( ¬ 𝑝 ( le ‘ 𝑘 ) 𝑤 → 𝑥 = ( ( 𝑝 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑝 ) ) ( meet ‘ 𝑘 ) 𝑤 ) ) ) ) )
38	1 2 37	cmpt	⊢ ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ℩ 𝑥 ∈ ( Base ‘ 𝑘 ) ∀ 𝑝 ∈ ( Atoms ‘ 𝑘 ) ( ¬ 𝑝 ( le ‘ 𝑘 ) 𝑤 → 𝑥 = ( ( 𝑝 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑝 ) ) ( meet ‘ 𝑘 ) 𝑤 ) ) ) ) ) )
39	0 38	wceq	⊢ trL = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ℩ 𝑥 ∈ ( Base ‘ 𝑘 ) ∀ 𝑝 ∈ ( Atoms ‘ 𝑘 ) ( ¬ 𝑝 ( le ‘ 𝑘 ) 𝑤 → 𝑥 = ( ( 𝑝 ( join ‘ 𝑘 ) ( 𝑓 ‘ 𝑝 ) ) ( meet ‘ 𝑘 ) 𝑤 ) ) ) ) ) )