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 36545
 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 36542 . 2 class TEndo
2 vk . . 3 setvar 𝑘
3 cvv 3340 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1631 . . . . 5 class 𝑘
6 clh 35773 . . . . 5 class LHyp
75, 6cfv 6049 . . . 4 class (LHyp‘𝑘)
84cv 1631 . . . . . . . 8 class 𝑤
9 cltrn 35890 . . . . . . . . 9 class LTrn
105, 9cfv 6049 . . . . . . . 8 class (LTrn‘𝑘)
118, 10cfv 6049 . . . . . . 7 class ((LTrn‘𝑘)‘𝑤)
12 vf . . . . . . . 8 setvar 𝑓
1312cv 1631 . . . . . . 7 class 𝑓
1411, 11, 13wf 6045 . . . . . 6 wff 𝑓:((LTrn‘𝑘)‘𝑤)⟶((LTrn‘𝑘)‘𝑤)
15 vx . . . . . . . . . . . 12 setvar 𝑥
1615cv 1631 . . . . . . . . . . 11 class 𝑥
17 vy . . . . . . . . . . . 12 setvar 𝑦
1817cv 1631 . . . . . . . . . . 11 class 𝑦
1916, 18ccom 5270 . . . . . . . . . 10 class (𝑥𝑦)
2019, 13cfv 6049 . . . . . . . . 9 class (𝑓‘(𝑥𝑦))
2116, 13cfv 6049 . . . . . . . . . 10 class (𝑓𝑥)
2218, 13cfv 6049 . . . . . . . . . 10 class (𝑓𝑦)
2321, 22ccom 5270 . . . . . . . . 9 class ((𝑓𝑥) ∘ (𝑓𝑦))
2420, 23wceq 1632 . . . . . . . 8 wff (𝑓‘(𝑥𝑦)) = ((𝑓𝑥) ∘ (𝑓𝑦))
2524, 17, 11wral 3050 . . . . . . 7 wff 𝑦 ∈ ((LTrn‘𝑘)‘𝑤)(𝑓‘(𝑥𝑦)) = ((𝑓𝑥) ∘ (𝑓𝑦))
2625, 15, 11wral 3050 . . . . . 6 wff 𝑥 ∈ ((LTrn‘𝑘)‘𝑤)∀𝑦 ∈ ((LTrn‘𝑘)‘𝑤)(𝑓‘(𝑥𝑦)) = ((𝑓𝑥) ∘ (𝑓𝑦))
27 ctrl 35948 . . . . . . . . . . 11 class trL
285, 27cfv 6049 . . . . . . . . . 10 class (trL‘𝑘)
298, 28cfv 6049 . . . . . . . . 9 class ((trL‘𝑘)‘𝑤)
3021, 29cfv 6049 . . . . . . . 8 class (((trL‘𝑘)‘𝑤)‘(𝑓𝑥))
3116, 29cfv 6049 . . . . . . . 8 class (((trL‘𝑘)‘𝑤)‘𝑥)
32 cple 16150 . . . . . . . . 9 class le
335, 32cfv 6049 . . . . . . . 8 class (le‘𝑘)
3430, 31, 33wbr 4804 . . . . . . 7 wff (((trL‘𝑘)‘𝑤)‘(𝑓𝑥))(le‘𝑘)(((trL‘𝑘)‘𝑤)‘𝑥)
3534, 15, 11wral 3050 . . . . . 6 wff 𝑥 ∈ ((LTrn‘𝑘)‘𝑤)(((trL‘𝑘)‘𝑤)‘(𝑓𝑥))(le‘𝑘)(((trL‘𝑘)‘𝑤)‘𝑥)
3614, 26, 35w3a 1072 . . . . 5 wff (𝑓:((LTrn‘𝑘)‘𝑤)⟶((LTrn‘𝑘)‘𝑤) ∧ ∀𝑥 ∈ ((LTrn‘𝑘)‘𝑤)∀𝑦 ∈ ((LTrn‘𝑘)‘𝑤)(𝑓‘(𝑥𝑦)) = ((𝑓𝑥) ∘ (𝑓𝑦)) ∧ ∀𝑥 ∈ ((LTrn‘𝑘)‘𝑤)(((trL‘𝑘)‘𝑤)‘(𝑓𝑥))(le‘𝑘)(((trL‘𝑘)‘𝑤)‘𝑥))
3736, 12cab 2746 . . . 4 class {𝑓 ∣ (𝑓:((LTrn‘𝑘)‘𝑤)⟶((LTrn‘𝑘)‘𝑤) ∧ ∀𝑥 ∈ ((LTrn‘𝑘)‘𝑤)∀𝑦 ∈ ((LTrn‘𝑘)‘𝑤)(𝑓‘(𝑥𝑦)) = ((𝑓𝑥) ∘ (𝑓𝑦)) ∧ ∀𝑥 ∈ ((LTrn‘𝑘)‘𝑤)(((trL‘𝑘)‘𝑤)‘(𝑓𝑥))(le‘𝑘)(((trL‘𝑘)‘𝑤)‘𝑥))}
384, 7, 37cmpt 4881 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑓 ∣ (𝑓:((LTrn‘𝑘)‘𝑤)⟶((LTrn‘𝑘)‘𝑤) ∧ ∀𝑥 ∈ ((LTrn‘𝑘)‘𝑤)∀𝑦 ∈ ((LTrn‘𝑘)‘𝑤)(𝑓‘(𝑥𝑦)) = ((𝑓𝑥) ∘ (𝑓𝑦)) ∧ ∀𝑥 ∈ ((LTrn‘𝑘)‘𝑤)(((trL‘𝑘)‘𝑤)‘(𝑓𝑥))(le‘𝑘)(((trL‘𝑘)‘𝑤)‘𝑥))})
392, 3, 38cmpt 4881 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑓 ∣ (𝑓:((LTrn‘𝑘)‘𝑤)⟶((LTrn‘𝑘)‘𝑤) ∧ ∀𝑥 ∈ ((LTrn‘𝑘)‘𝑤)∀𝑦 ∈ ((LTrn‘𝑘)‘𝑤)(𝑓‘(𝑥𝑦)) = ((𝑓𝑥) ∘ (𝑓𝑦)) ∧ ∀𝑥 ∈ ((LTrn‘𝑘)‘𝑤)(((trL‘𝑘)‘𝑤)‘(𝑓𝑥))(le‘𝑘)(((trL‘𝑘)‘𝑤)‘𝑥))}))
401, 39wceq 1632 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  36548
 Copyright terms: Public domain W3C validator