This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑘 ) 𝑤 ) ) ) ) ) )