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 ⁡ w f ⁡ x ∘ y = f ⁡ x ∘ f ⁡ y ∧ ∀ x ∈ LTrn ⁡ k ⁡ w trL ⁡ k ⁡ w ⁡ f ⁡ x ≤ k trL ⁡ k ⁡ w ⁡ x

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctendo class TEndo
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 7 cv setvar f
9 cltrn class LTrn
10 5 9 cfv class LTrn ⁡ k
11 3 cv setvar w
12 11 10 cfv class LTrn ⁡ k ⁡ w
13 12 12 8 wf wff f : LTrn ⁡ k ⁡ w ⟶ LTrn ⁡ k ⁡ w
14 vx setvar x
15 vy setvar y
16 14 cv setvar x
17 15 cv setvar y
18 16 17 ccom class x ∘ y
19 18 8 cfv class f ⁡ x ∘ y
20 16 8 cfv class f ⁡ x
21 17 8 cfv class f ⁡ y
22 20 21 ccom class f ⁡ x ∘ f ⁡ y
23 19 22 wceq wff f ⁡ x ∘ y = f ⁡ x ∘ f ⁡ y
24 23 15 12 wral wff ∀ y ∈ LTrn ⁡ k ⁡ w f ⁡ x ∘ y = f ⁡ x ∘ f ⁡ y
25 24 14 12 wral wff ∀ x ∈ LTrn ⁡ k ⁡ w ∀ y ∈ LTrn ⁡ k ⁡ w f ⁡ x ∘ y = f ⁡ x ∘ f ⁡ y
26 ctrl class trL
27 5 26 cfv class trL ⁡ k
28 11 27 cfv class trL ⁡ k ⁡ w
29 20 28 cfv class trL ⁡ k ⁡ w ⁡ f ⁡ x
30 cple class le
31 5 30 cfv class ≤ k
32 16 28 cfv class trL ⁡ k ⁡ w ⁡ x
33 29 32 31 wbr wff trL ⁡ k ⁡ w ⁡ f ⁡ x ≤ k trL ⁡ k ⁡ w ⁡ x
34 33 14 12 wral wff ∀ x ∈ LTrn ⁡ k ⁡ w trL ⁡ k ⁡ w ⁡ f ⁡ x ≤ k trL ⁡ k ⁡ w ⁡ x
35 13 25 34 w3a wff f : LTrn ⁡ k ⁡ w ⟶ LTrn ⁡ k ⁡ w ∧ ∀ x ∈ LTrn ⁡ k ⁡ w ∀ y ∈ LTrn ⁡ k ⁡ w f ⁡ x ∘ y = f ⁡ x ∘ f ⁡ y ∧ ∀ x ∈ LTrn ⁡ k ⁡ w trL ⁡ k ⁡ w ⁡ f ⁡ x ≤ k trL ⁡ k ⁡ w ⁡ x
36 35 7 cab class f | f : LTrn ⁡ k ⁡ w ⟶ LTrn ⁡ k ⁡ w ∧ ∀ x ∈ LTrn ⁡ k ⁡ w ∀ y ∈ LTrn ⁡ k ⁡ w f ⁡ x ∘ y = f ⁡ x ∘ f ⁡ y ∧ ∀ x ∈ LTrn ⁡ k ⁡ w trL ⁡ k ⁡ w ⁡ f ⁡ x ≤ k trL ⁡ k ⁡ w ⁡ x
37 3 6 36 cmpt class w ∈ LHyp ⁡ k ⟼ f | f : LTrn ⁡ k ⁡ w ⟶ LTrn ⁡ k ⁡ w ∧ ∀ x ∈ LTrn ⁡ k ⁡ w ∀ y ∈ LTrn ⁡ k ⁡ w f ⁡ x ∘ y = f ⁡ x ∘ f ⁡ y ∧ ∀ x ∈ LTrn ⁡ k ⁡ w trL ⁡ k ⁡ w ⁡ f ⁡ x ≤ k trL ⁡ k ⁡ w ⁡ x
38 1 2 37 cmpt class k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ f | f : LTrn ⁡ k ⁡ w ⟶ LTrn ⁡ k ⁡ w ∧ ∀ x ∈ LTrn ⁡ k ⁡ w ∀ y ∈ LTrn ⁡ k ⁡ w f ⁡ x ∘ y = f ⁡ x ∘ f ⁡ y ∧ ∀ x ∈ LTrn ⁡ k ⁡ w trL ⁡ k ⁡ w ⁡ f ⁡ x ≤ k trL ⁡ k ⁡ w ⁡ x
39 0 38 wceq wff TEndo = k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ f | f : LTrn ⁡ k ⁡ w ⟶ LTrn ⁡ k ⁡ w ∧ ∀ x ∈ LTrn ⁡ k ⁡ w ∀ y ∈ LTrn ⁡ k ⁡ w f ⁡ x ∘ y = f ⁡ x ∘ f ⁡ y ∧ ∀ x ∈ LTrn ⁡ k ⁡ w trL ⁡ k ⁡ w ⁡ f ⁡ x ≤ k trL ⁡ k ⁡ w ⁡ x