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 = k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ f ∈ LTrn ⁡ k ⁡ w ⟼ ι x ∈ Base k | ∀ p ∈ Atoms ⁡ k ¬ p ≤ k w → x = p join ⁡ k f ⁡ p meet ⁡ k w

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctrl class trL
1 vk setvar k
2 cvv class V
3 vw setvar w
4 clh class LHyp
5 1 cv setvar k
6 5 4 cfv class LHyp ⁡ k
7 vf setvar f
8 cltrn class LTrn
9 5 8 cfv class LTrn ⁡ k
10 3 cv setvar w
11 10 9 cfv class LTrn ⁡ k ⁡ w
12 vx setvar x
13 cbs class Base
14 5 13 cfv class Base k
15 vp setvar p
16 catm class Atoms
17 5 16 cfv class Atoms ⁡ k
18 15 cv setvar p
19 cple class le
20 5 19 cfv class ≤ k
21 18 10 20 wbr wff p ≤ k w
22 21 wn wff ¬ p ≤ k w
23 12 cv setvar x
24 cjn class join
25 5 24 cfv class join ⁡ k
26 7 cv setvar f
27 18 26 cfv class f ⁡ p
28 18 27 25 co class p join ⁡ k f ⁡ p
29 cmee class meet
30 5 29 cfv class meet ⁡ k
31 28 10 30 co class p join ⁡ k f ⁡ p meet ⁡ k w
32 23 31 wceq wff x = p join ⁡ k f ⁡ p meet ⁡ k w
33 22 32 wi wff ¬ p ≤ k w → x = p join ⁡ k f ⁡ p meet ⁡ k w
34 33 15 17 wral wff ∀ p ∈ Atoms ⁡ k ¬ p ≤ k w → x = p join ⁡ k f ⁡ p meet ⁡ k w
35 34 12 14 crio class ι x ∈ Base k | ∀ p ∈ Atoms ⁡ k ¬ p ≤ k w → x = p join ⁡ k f ⁡ p meet ⁡ k w
36 7 11 35 cmpt class f ∈ LTrn ⁡ k ⁡ w ⟼ ι x ∈ Base k | ∀ p ∈ Atoms ⁡ k ¬ p ≤ k w → x = p join ⁡ k f ⁡ p meet ⁡ k w
37 3 6 36 cmpt class w ∈ LHyp ⁡ k ⟼ f ∈ LTrn ⁡ k ⁡ w ⟼ ι x ∈ Base k | ∀ p ∈ Atoms ⁡ k ¬ p ≤ k w → x = p join ⁡ k f ⁡ p meet ⁡ k w
38 1 2 37 cmpt class k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ f ∈ LTrn ⁡ k ⁡ w ⟼ ι x ∈ Base k | ∀ p ∈ Atoms ⁡ k ¬ p ≤ k w → x = p join ⁡ k f ⁡ p meet ⁡ k w
39 0 38 wceq wff trL = k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ f ∈ LTrn ⁡ k ⁡ w ⟼ ι x ∈ Base k | ∀ p ∈ Atoms ⁡ k ¬ p ≤ k w → x = p join ⁡ k f ⁡ p meet ⁡ k w