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 39929
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 39926 . 2 class TEndo
2 vk . . 3 setvar π‘˜
3 cvv 3472 . . 3 class V
4 vw . . . 4 setvar 𝑀
52cv 1538 . . . . 5 class π‘˜
6 clh 39158 . . . . 5 class LHyp
75, 6cfv 6542 . . . 4 class (LHypβ€˜π‘˜)
84cv 1538 . . . . . . . 8 class 𝑀
9 cltrn 39275 . . . . . . . . 9 class LTrn
105, 9cfv 6542 . . . . . . . 8 class (LTrnβ€˜π‘˜)
118, 10cfv 6542 . . . . . . 7 class ((LTrnβ€˜π‘˜)β€˜π‘€)
12 vf . . . . . . . 8 setvar 𝑓
1312cv 1538 . . . . . . 7 class 𝑓
1411, 11, 13wf 6538 . . . . . 6 wff 𝑓:((LTrnβ€˜π‘˜)β€˜π‘€)⟢((LTrnβ€˜π‘˜)β€˜π‘€)
15 vx . . . . . . . . . . . 12 setvar π‘₯
1615cv 1538 . . . . . . . . . . 11 class π‘₯
17 vy . . . . . . . . . . . 12 setvar 𝑦
1817cv 1538 . . . . . . . . . . 11 class 𝑦
1916, 18ccom 5679 . . . . . . . . . 10 class (π‘₯ ∘ 𝑦)
2019, 13cfv 6542 . . . . . . . . 9 class (π‘“β€˜(π‘₯ ∘ 𝑦))
2116, 13cfv 6542 . . . . . . . . . 10 class (π‘“β€˜π‘₯)
2218, 13cfv 6542 . . . . . . . . . 10 class (π‘“β€˜π‘¦)
2321, 22ccom 5679 . . . . . . . . 9 class ((π‘“β€˜π‘₯) ∘ (π‘“β€˜π‘¦))
2420, 23wceq 1539 . . . . . . . 8 wff (π‘“β€˜(π‘₯ ∘ 𝑦)) = ((π‘“β€˜π‘₯) ∘ (π‘“β€˜π‘¦))
2524, 17, 11wral 3059 . . . . . . 7 wff βˆ€π‘¦ ∈ ((LTrnβ€˜π‘˜)β€˜π‘€)(π‘“β€˜(π‘₯ ∘ 𝑦)) = ((π‘“β€˜π‘₯) ∘ (π‘“β€˜π‘¦))
2625, 15, 11wral 3059 . . . . . 6 wff βˆ€π‘₯ ∈ ((LTrnβ€˜π‘˜)β€˜π‘€)βˆ€π‘¦ ∈ ((LTrnβ€˜π‘˜)β€˜π‘€)(π‘“β€˜(π‘₯ ∘ 𝑦)) = ((π‘“β€˜π‘₯) ∘ (π‘“β€˜π‘¦))
27 ctrl 39332 . . . . . . . . . . 11 class trL
285, 27cfv 6542 . . . . . . . . . 10 class (trLβ€˜π‘˜)
298, 28cfv 6542 . . . . . . . . 9 class ((trLβ€˜π‘˜)β€˜π‘€)
3021, 29cfv 6542 . . . . . . . 8 class (((trLβ€˜π‘˜)β€˜π‘€)β€˜(π‘“β€˜π‘₯))
3116, 29cfv 6542 . . . . . . . 8 class (((trLβ€˜π‘˜)β€˜π‘€)β€˜π‘₯)
32 cple 17208 . . . . . . . . 9 class le
335, 32cfv 6542 . . . . . . . 8 class (leβ€˜π‘˜)
3430, 31, 33wbr 5147 . . . . . . 7 wff (((trLβ€˜π‘˜)β€˜π‘€)β€˜(π‘“β€˜π‘₯))(leβ€˜π‘˜)(((trLβ€˜π‘˜)β€˜π‘€)β€˜π‘₯)
3534, 15, 11wral 3059 . . . . . 6 wff βˆ€π‘₯ ∈ ((LTrnβ€˜π‘˜)β€˜π‘€)(((trLβ€˜π‘˜)β€˜π‘€)β€˜(π‘“β€˜π‘₯))(leβ€˜π‘˜)(((trLβ€˜π‘˜)β€˜π‘€)β€˜π‘₯)
3614, 26, 35w3a 1085 . . . . 5 wff (𝑓:((LTrnβ€˜π‘˜)β€˜π‘€)⟢((LTrnβ€˜π‘˜)β€˜π‘€) ∧ βˆ€π‘₯ ∈ ((LTrnβ€˜π‘˜)β€˜π‘€)βˆ€π‘¦ ∈ ((LTrnβ€˜π‘˜)β€˜π‘€)(π‘“β€˜(π‘₯ ∘ 𝑦)) = ((π‘“β€˜π‘₯) ∘ (π‘“β€˜π‘¦)) ∧ βˆ€π‘₯ ∈ ((LTrnβ€˜π‘˜)β€˜π‘€)(((trLβ€˜π‘˜)β€˜π‘€)β€˜(π‘“β€˜π‘₯))(leβ€˜π‘˜)(((trLβ€˜π‘˜)β€˜π‘€)β€˜π‘₯))
3736, 12cab 2707 . . . 4 class {𝑓 ∣ (𝑓:((LTrnβ€˜π‘˜)β€˜π‘€)⟢((LTrnβ€˜π‘˜)β€˜π‘€) ∧ βˆ€π‘₯ ∈ ((LTrnβ€˜π‘˜)β€˜π‘€)βˆ€π‘¦ ∈ ((LTrnβ€˜π‘˜)β€˜π‘€)(π‘“β€˜(π‘₯ ∘ 𝑦)) = ((π‘“β€˜π‘₯) ∘ (π‘“β€˜π‘¦)) ∧ βˆ€π‘₯ ∈ ((LTrnβ€˜π‘˜)β€˜π‘€)(((trLβ€˜π‘˜)β€˜π‘€)β€˜(π‘“β€˜π‘₯))(leβ€˜π‘˜)(((trLβ€˜π‘˜)β€˜π‘€)β€˜π‘₯))}
384, 7, 37cmpt 5230 . . 3 class (𝑀 ∈ (LHypβ€˜π‘˜) ↦ {𝑓 ∣ (𝑓:((LTrnβ€˜π‘˜)β€˜π‘€)⟢((LTrnβ€˜π‘˜)β€˜π‘€) ∧ βˆ€π‘₯ ∈ ((LTrnβ€˜π‘˜)β€˜π‘€)βˆ€π‘¦ ∈ ((LTrnβ€˜π‘˜)β€˜π‘€)(π‘“β€˜(π‘₯ ∘ 𝑦)) = ((π‘“β€˜π‘₯) ∘ (π‘“β€˜π‘¦)) ∧ βˆ€π‘₯ ∈ ((LTrnβ€˜π‘˜)β€˜π‘€)(((trLβ€˜π‘˜)β€˜π‘€)β€˜(π‘“β€˜π‘₯))(leβ€˜π‘˜)(((trLβ€˜π‘˜)β€˜π‘€)β€˜π‘₯))})
392, 3, 38cmpt 5230 . 2 class (π‘˜ ∈ V ↦ (𝑀 ∈ (LHypβ€˜π‘˜) ↦ {𝑓 ∣ (𝑓:((LTrnβ€˜π‘˜)β€˜π‘€)⟢((LTrnβ€˜π‘˜)β€˜π‘€) ∧ βˆ€π‘₯ ∈ ((LTrnβ€˜π‘˜)β€˜π‘€)βˆ€π‘¦ ∈ ((LTrnβ€˜π‘˜)β€˜π‘€)(π‘“β€˜(π‘₯ ∘ 𝑦)) = ((π‘“β€˜π‘₯) ∘ (π‘“β€˜π‘¦)) ∧ βˆ€π‘₯ ∈ ((LTrnβ€˜π‘˜)β€˜π‘€)(((trLβ€˜π‘˜)β€˜π‘€)β€˜(π‘“β€˜π‘₯))(leβ€˜π‘˜)(((trLβ€˜π‘˜)β€˜π‘€)β€˜π‘₯))}))
401, 39wceq 1539 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  39932
  Copyright terms: Public domain W3C validator