Metamath Proof Explorer

Definition df-tendo

Description: Define trace-preserving endomorphisms on the set of translations. (Contributed by NM, 8-Jun-2013)

Ref Expression
Assertion df-tendo ⊢TEndo=k∈V⟼w∈LHyp⁡k⟼f|f:LTrn⁡k⁡w⟶LTrn⁡k⁡w∧∀x∈LTrn⁡k⁡w∀y∈LTrn⁡k⁡wf⁡x∘y=f⁡x∘f⁡y∧∀x∈LTrn⁡k⁡wtrL⁡k⁡w⁡f⁡x≤ktrL⁡k⁡w⁡x

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctendo classTEndo
1 vk setvark
2 cvv classV
3 vw setvarw
4 clh classLHyp
5 1 cv setvark
6 5 4 cfv classLHyp⁡k
7 vf setvarf
8 7 cv setvarf
9 cltrn classLTrn
10 5 9 cfv classLTrn⁡k
11 3 cv setvarw
12 11 10 cfv classLTrn⁡k⁡w
13 12 12 8 wf wfff:LTrn⁡k⁡w⟶LTrn⁡k⁡w
14 vx setvarx
15 vy setvary
16 14 cv setvarx
17 15 cv setvary
18 16 17 ccom classx∘y
19 18 8 cfv classf⁡x∘y
20 16 8 cfv classf⁡x
21 17 8 cfv classf⁡y
22 20 21 ccom classf⁡x∘f⁡y
23 19 22 wceq wfff⁡x∘y=f⁡x∘f⁡y
24 23 15 12 wral wff∀y∈LTrn⁡k⁡wf⁡x∘y=f⁡x∘f⁡y
25 24 14 12 wral wff∀x∈LTrn⁡k⁡w∀y∈LTrn⁡k⁡wf⁡x∘y=f⁡x∘f⁡y
26 ctrl classtrL
27 5 26 cfv classtrL⁡k
28 11 27 cfv classtrL⁡k⁡w
29 20 28 cfv classtrL⁡k⁡w⁡f⁡x
30 cple classle
31 5 30 cfv class≤k
32 16 28 cfv classtrL⁡k⁡w⁡x
33 29 32 31 wbr wfftrL⁡k⁡w⁡f⁡x≤ktrL⁡k⁡w⁡x
34 33 14 12 wral wff∀x∈LTrn⁡k⁡wtrL⁡k⁡w⁡f⁡x≤ktrL⁡k⁡w⁡x
35 13 25 34 w3a wfff:LTrn⁡k⁡w⟶LTrn⁡k⁡w∧∀x∈LTrn⁡k⁡w∀y∈LTrn⁡k⁡wf⁡x∘y=f⁡x∘f⁡y∧∀x∈LTrn⁡k⁡wtrL⁡k⁡w⁡f⁡x≤ktrL⁡k⁡w⁡x
36 35 7 cab classf|f:LTrn⁡k⁡w⟶LTrn⁡k⁡w∧∀x∈LTrn⁡k⁡w∀y∈LTrn⁡k⁡wf⁡x∘y=f⁡x∘f⁡y∧∀x∈LTrn⁡k⁡wtrL⁡k⁡w⁡f⁡x≤ktrL⁡k⁡w⁡x
37 3 6 36 cmpt classw∈LHyp⁡k⟼f|f:LTrn⁡k⁡w⟶LTrn⁡k⁡w∧∀x∈LTrn⁡k⁡w∀y∈LTrn⁡k⁡wf⁡x∘y=f⁡x∘f⁡y∧∀x∈LTrn⁡k⁡wtrL⁡k⁡w⁡f⁡x≤ktrL⁡k⁡w⁡x
38 1 2 37 cmpt classk∈V⟼w∈LHyp⁡k⟼f|f:LTrn⁡k⁡w⟶LTrn⁡k⁡w∧∀x∈LTrn⁡k⁡w∀y∈LTrn⁡k⁡wf⁡x∘y=f⁡x∘f⁡y∧∀x∈LTrn⁡k⁡wtrL⁡k⁡w⁡f⁡x≤ktrL⁡k⁡w⁡x
39 0 38 wceq wffTEndo=k∈V⟼w∈LHyp⁡k⟼f|f:LTrn⁡k⁡w⟶LTrn⁡k⁡w∧∀x∈LTrn⁡k⁡w∀y∈LTrn⁡k⁡wf⁡x∘y=f⁡x∘f⁡y∧∀x∈LTrn⁡k⁡wtrL⁡k⁡w⁡f⁡x≤ktrL⁡k⁡w⁡x