Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-mend Structured version   Visualization version   GIF version

Definition df-mend 39654
Description: Define the endomorphism algebra of a module. (Contributed by Stefan O'Rear, 2-Sep-2015.)
Assertion
Ref Expression
df-mend MEndo = (𝑚 ∈ V ↦ (𝑚 LMHom 𝑚) / 𝑏({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥f (+g𝑚)𝑦))⟩, ⟨(.r‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑦))⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑚)⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f ( ·𝑠𝑚)𝑦))⟩}))
Distinct variable group:   𝑚,𝑏,𝑥,𝑦

Detailed syntax breakdown of Definition df-mend
StepHypRef Expression
1 cmend 39653 . 2 class MEndo
2 vm . . 3 setvar 𝑚
3 cvv 3492 . . 3 class V
4 vb . . . 4 setvar 𝑏
52cv 1527 . . . . 5 class 𝑚
6 clmhm 19720 . . . . 5 class LMHom
75, 5, 6co 7145 . . . 4 class (𝑚 LMHom 𝑚)
8 cnx 16468 . . . . . . . 8 class ndx
9 cbs 16471 . . . . . . . 8 class Base
108, 9cfv 6348 . . . . . . 7 class (Base‘ndx)
114cv 1527 . . . . . . 7 class 𝑏
1210, 11cop 4563 . . . . . 6 class ⟨(Base‘ndx), 𝑏
13 cplusg 16553 . . . . . . . 8 class +g
148, 13cfv 6348 . . . . . . 7 class (+g‘ndx)
15 vx . . . . . . . 8 setvar 𝑥
16 vy . . . . . . . 8 setvar 𝑦
1715cv 1527 . . . . . . . . 9 class 𝑥
1816cv 1527 . . . . . . . . 9 class 𝑦
195, 13cfv 6348 . . . . . . . . . 10 class (+g𝑚)
2019cof 7396 . . . . . . . . 9 class f (+g𝑚)
2117, 18, 20co 7145 . . . . . . . 8 class (𝑥f (+g𝑚)𝑦)
2215, 16, 11, 11, 21cmpo 7147 . . . . . . 7 class (𝑥𝑏, 𝑦𝑏 ↦ (𝑥f (+g𝑚)𝑦))
2314, 22cop 4563 . . . . . 6 class ⟨(+g‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥f (+g𝑚)𝑦))⟩
24 cmulr 16554 . . . . . . . 8 class .r
258, 24cfv 6348 . . . . . . 7 class (.r‘ndx)
2617, 18ccom 5552 . . . . . . . 8 class (𝑥𝑦)
2715, 16, 11, 11, 26cmpo 7147 . . . . . . 7 class (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑦))
2825, 27cop 4563 . . . . . 6 class ⟨(.r‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑦))⟩
2912, 23, 28ctp 4561 . . . . 5 class {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥f (+g𝑚)𝑦))⟩, ⟨(.r‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑦))⟩}
30 csca 16556 . . . . . . . 8 class Scalar
318, 30cfv 6348 . . . . . . 7 class (Scalar‘ndx)
325, 30cfv 6348 . . . . . . 7 class (Scalar‘𝑚)
3331, 32cop 4563 . . . . . 6 class ⟨(Scalar‘ndx), (Scalar‘𝑚)⟩
34 cvsca 16557 . . . . . . . 8 class ·𝑠
358, 34cfv 6348 . . . . . . 7 class ( ·𝑠 ‘ndx)
3632, 9cfv 6348 . . . . . . . 8 class (Base‘(Scalar‘𝑚))
375, 9cfv 6348 . . . . . . . . . 10 class (Base‘𝑚)
3817csn 4557 . . . . . . . . . 10 class {𝑥}
3937, 38cxp 5546 . . . . . . . . 9 class ((Base‘𝑚) × {𝑥})
405, 34cfv 6348 . . . . . . . . . 10 class ( ·𝑠𝑚)
4140cof 7396 . . . . . . . . 9 class f ( ·𝑠𝑚)
4239, 18, 41co 7145 . . . . . . . 8 class (((Base‘𝑚) × {𝑥}) ∘f ( ·𝑠𝑚)𝑦)
4315, 16, 36, 11, 42cmpo 7147 . . . . . . 7 class (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f ( ·𝑠𝑚)𝑦))
4435, 43cop 4563 . . . . . 6 class ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f ( ·𝑠𝑚)𝑦))⟩
4533, 44cpr 4559 . . . . 5 class {⟨(Scalar‘ndx), (Scalar‘𝑚)⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f ( ·𝑠𝑚)𝑦))⟩}
4629, 45cun 3931 . . . 4 class ({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥f (+g𝑚)𝑦))⟩, ⟨(.r‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑦))⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑚)⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f ( ·𝑠𝑚)𝑦))⟩})
474, 7, 46csb 3880 . . 3 class (𝑚 LMHom 𝑚) / 𝑏({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥f (+g𝑚)𝑦))⟩, ⟨(.r‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑦))⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑚)⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f ( ·𝑠𝑚)𝑦))⟩})
482, 3, 47cmpt 5137 . 2 class (𝑚 ∈ V ↦ (𝑚 LMHom 𝑚) / 𝑏({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥f (+g𝑚)𝑦))⟩, ⟨(.r‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑦))⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑚)⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f ( ·𝑠𝑚)𝑦))⟩}))
491, 48wceq 1528 1 wff MEndo = (𝑚 ∈ V ↦ (𝑚 LMHom 𝑚) / 𝑏({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥f (+g𝑚)𝑦))⟩, ⟨(.r‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑦))⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑚)⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f ( ·𝑠𝑚)𝑦))⟩}))
Colors of variables: wff setvar class
This definition is referenced by:  mendval  39661
  Copyright terms: Public domain W3C validator