Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-tendo Structured version   Visualization version   GIF version

Definition df-tendo 35061
Description: Define trace-preserving endomorphisms on the set of translations. (Contributed by NM, 8-Jun-2013.)
Assertion
Ref Expression
df-tendo TEndo = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑓 ∣ (𝑓:((LTrn‘𝑘)‘𝑤)⟶((LTrn‘𝑘)‘𝑤) ∧ ∀𝑥 ∈ ((LTrn‘𝑘)‘𝑤)∀𝑦 ∈ ((LTrn‘𝑘)‘𝑤)(𝑓‘(𝑥𝑦)) = ((𝑓𝑥) ∘ (𝑓𝑦)) ∧ ∀𝑥 ∈ ((LTrn‘𝑘)‘𝑤)(((trL‘𝑘)‘𝑤)‘(𝑓𝑥))(le‘𝑘)(((trL‘𝑘)‘𝑤)‘𝑥))}))
Distinct variable group:   𝑤,𝑘,𝑓,𝑥,𝑦

Detailed syntax breakdown of Definition df-tendo
StepHypRef Expression
1 ctendo 35058 . 2 class TEndo
2 vk . . 3 setvar 𝑘
3 cvv 3173 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1474 . . . . 5 class 𝑘
6 clh 34288 . . . . 5 class LHyp
75, 6cfv 5804 . . . 4 class (LHyp‘𝑘)
84cv 1474 . . . . . . . 8 class 𝑤
9 cltrn 34405 . . . . . . . . 9 class LTrn
105, 9cfv 5804 . . . . . . . 8 class (LTrn‘𝑘)
118, 10cfv 5804 . . . . . . 7 class ((LTrn‘𝑘)‘𝑤)
12 vf . . . . . . . 8 setvar 𝑓
1312cv 1474 . . . . . . 7 class 𝑓
1411, 11, 13wf 5800 . . . . . 6 wff 𝑓:((LTrn‘𝑘)‘𝑤)⟶((LTrn‘𝑘)‘𝑤)
15 vx . . . . . . . . . . . 12 setvar 𝑥
1615cv 1474 . . . . . . . . . . 11 class 𝑥
17 vy . . . . . . . . . . . 12 setvar 𝑦
1817cv 1474 . . . . . . . . . . 11 class 𝑦
1916, 18ccom 5042 . . . . . . . . . 10 class (𝑥𝑦)
2019, 13cfv 5804 . . . . . . . . 9 class (𝑓‘(𝑥𝑦))
2116, 13cfv 5804 . . . . . . . . . 10 class (𝑓𝑥)
2218, 13cfv 5804 . . . . . . . . . 10 class (𝑓𝑦)
2321, 22ccom 5042 . . . . . . . . 9 class ((𝑓𝑥) ∘ (𝑓𝑦))
2420, 23wceq 1475 . . . . . . . 8 wff (𝑓‘(𝑥𝑦)) = ((𝑓𝑥) ∘ (𝑓𝑦))
2524, 17, 11wral 2896 . . . . . . 7 wff 𝑦 ∈ ((LTrn‘𝑘)‘𝑤)(𝑓‘(𝑥𝑦)) = ((𝑓𝑥) ∘ (𝑓𝑦))
2625, 15, 11wral 2896 . . . . . 6 wff 𝑥 ∈ ((LTrn‘𝑘)‘𝑤)∀𝑦 ∈ ((LTrn‘𝑘)‘𝑤)(𝑓‘(𝑥𝑦)) = ((𝑓𝑥) ∘ (𝑓𝑦))
27 ctrl 34463 . . . . . . . . . . 11 class trL
285, 27cfv 5804 . . . . . . . . . 10 class (trL‘𝑘)
298, 28cfv 5804 . . . . . . . . 9 class ((trL‘𝑘)‘𝑤)
3021, 29cfv 5804 . . . . . . . 8 class (((trL‘𝑘)‘𝑤)‘(𝑓𝑥))
3116, 29cfv 5804 . . . . . . . 8 class (((trL‘𝑘)‘𝑤)‘𝑥)
32 cple 15775 . . . . . . . . 9 class le
335, 32cfv 5804 . . . . . . . 8 class (le‘𝑘)
3430, 31, 33wbr 4583 . . . . . . 7 wff (((trL‘𝑘)‘𝑤)‘(𝑓𝑥))(le‘𝑘)(((trL‘𝑘)‘𝑤)‘𝑥)
3534, 15, 11wral 2896 . . . . . 6 wff 𝑥 ∈ ((LTrn‘𝑘)‘𝑤)(((trL‘𝑘)‘𝑤)‘(𝑓𝑥))(le‘𝑘)(((trL‘𝑘)‘𝑤)‘𝑥)
3614, 26, 35w3a 1031 . . . . 5 wff (𝑓:((LTrn‘𝑘)‘𝑤)⟶((LTrn‘𝑘)‘𝑤) ∧ ∀𝑥 ∈ ((LTrn‘𝑘)‘𝑤)∀𝑦 ∈ ((LTrn‘𝑘)‘𝑤)(𝑓‘(𝑥𝑦)) = ((𝑓𝑥) ∘ (𝑓𝑦)) ∧ ∀𝑥 ∈ ((LTrn‘𝑘)‘𝑤)(((trL‘𝑘)‘𝑤)‘(𝑓𝑥))(le‘𝑘)(((trL‘𝑘)‘𝑤)‘𝑥))
3736, 12cab 2596 . . . 4 class {𝑓 ∣ (𝑓:((LTrn‘𝑘)‘𝑤)⟶((LTrn‘𝑘)‘𝑤) ∧ ∀𝑥 ∈ ((LTrn‘𝑘)‘𝑤)∀𝑦 ∈ ((LTrn‘𝑘)‘𝑤)(𝑓‘(𝑥𝑦)) = ((𝑓𝑥) ∘ (𝑓𝑦)) ∧ ∀𝑥 ∈ ((LTrn‘𝑘)‘𝑤)(((trL‘𝑘)‘𝑤)‘(𝑓𝑥))(le‘𝑘)(((trL‘𝑘)‘𝑤)‘𝑥))}
384, 7, 37cmpt 4643 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑓 ∣ (𝑓:((LTrn‘𝑘)‘𝑤)⟶((LTrn‘𝑘)‘𝑤) ∧ ∀𝑥 ∈ ((LTrn‘𝑘)‘𝑤)∀𝑦 ∈ ((LTrn‘𝑘)‘𝑤)(𝑓‘(𝑥𝑦)) = ((𝑓𝑥) ∘ (𝑓𝑦)) ∧ ∀𝑥 ∈ ((LTrn‘𝑘)‘𝑤)(((trL‘𝑘)‘𝑤)‘(𝑓𝑥))(le‘𝑘)(((trL‘𝑘)‘𝑤)‘𝑥))})
392, 3, 38cmpt 4643 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑓 ∣ (𝑓:((LTrn‘𝑘)‘𝑤)⟶((LTrn‘𝑘)‘𝑤) ∧ ∀𝑥 ∈ ((LTrn‘𝑘)‘𝑤)∀𝑦 ∈ ((LTrn‘𝑘)‘𝑤)(𝑓‘(𝑥𝑦)) = ((𝑓𝑥) ∘ (𝑓𝑦)) ∧ ∀𝑥 ∈ ((LTrn‘𝑘)‘𝑤)(((trL‘𝑘)‘𝑤)‘(𝑓𝑥))(le‘𝑘)(((trL‘𝑘)‘𝑤)‘𝑥))}))
401, 39wceq 1475 1 wff TEndo = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑓 ∣ (𝑓:((LTrn‘𝑘)‘𝑤)⟶((LTrn‘𝑘)‘𝑤) ∧ ∀𝑥 ∈ ((LTrn‘𝑘)‘𝑤)∀𝑦 ∈ ((LTrn‘𝑘)‘𝑤)(𝑓‘(𝑥𝑦)) = ((𝑓𝑥) ∘ (𝑓𝑦)) ∧ ∀𝑥 ∈ ((LTrn‘𝑘)‘𝑤)(((trL‘𝑘)‘𝑤)‘(𝑓𝑥))(le‘𝑘)(((trL‘𝑘)‘𝑤)‘𝑥))}))
Colors of variables: wff setvar class
This definition is referenced by:  tendofset  35064
  Copyright terms: Public domain W3C validator