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 37266
 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), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑓 (+g𝑚)𝑦))⟩, ⟨(.r‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑦))⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑚)⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘𝑓 ( ·𝑠𝑚)𝑦))⟩}))
Distinct variable group:   𝑚,𝑏,𝑥,𝑦

Detailed syntax breakdown of Definition df-mend
StepHypRef Expression
1 cmend 37265 . 2 class MEndo
2 vm . . 3 setvar 𝑚
3 cvv 3190 . . 3 class V
4 vb . . . 4 setvar 𝑏
52cv 1479 . . . . 5 class 𝑚
6 clmhm 18959 . . . . 5 class LMHom
75, 5, 6co 6615 . . . 4 class (𝑚 LMHom 𝑚)
8 cnx 15797 . . . . . . . 8 class ndx
9 cbs 15800 . . . . . . . 8 class Base
108, 9cfv 5857 . . . . . . 7 class (Base‘ndx)
114cv 1479 . . . . . . 7 class 𝑏
1210, 11cop 4161 . . . . . 6 class ⟨(Base‘ndx), 𝑏
13 cplusg 15881 . . . . . . . 8 class +g
148, 13cfv 5857 . . . . . . 7 class (+g‘ndx)
15 vx . . . . . . . 8 setvar 𝑥
16 vy . . . . . . . 8 setvar 𝑦
1715cv 1479 . . . . . . . . 9 class 𝑥
1816cv 1479 . . . . . . . . 9 class 𝑦
195, 13cfv 5857 . . . . . . . . . 10 class (+g𝑚)
2019cof 6860 . . . . . . . . 9 class 𝑓 (+g𝑚)
2117, 18, 20co 6615 . . . . . . . 8 class (𝑥𝑓 (+g𝑚)𝑦)
2215, 16, 11, 11, 21cmpt2 6617 . . . . . . 7 class (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑓 (+g𝑚)𝑦))
2314, 22cop 4161 . . . . . 6 class ⟨(+g‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑓 (+g𝑚)𝑦))⟩
24 cmulr 15882 . . . . . . . 8 class .r
258, 24cfv 5857 . . . . . . 7 class (.r‘ndx)
2617, 18ccom 5088 . . . . . . . 8 class (𝑥𝑦)
2715, 16, 11, 11, 26cmpt2 6617 . . . . . . 7 class (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑦))
2825, 27cop 4161 . . . . . 6 class ⟨(.r‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑦))⟩
2912, 23, 28ctp 4159 . . . . 5 class {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑓 (+g𝑚)𝑦))⟩, ⟨(.r‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑦))⟩}
30 csca 15884 . . . . . . . 8 class Scalar
318, 30cfv 5857 . . . . . . 7 class (Scalar‘ndx)
325, 30cfv 5857 . . . . . . 7 class (Scalar‘𝑚)
3331, 32cop 4161 . . . . . 6 class ⟨(Scalar‘ndx), (Scalar‘𝑚)⟩
34 cvsca 15885 . . . . . . . 8 class ·𝑠
358, 34cfv 5857 . . . . . . 7 class ( ·𝑠 ‘ndx)
3632, 9cfv 5857 . . . . . . . 8 class (Base‘(Scalar‘𝑚))
375, 9cfv 5857 . . . . . . . . . 10 class (Base‘𝑚)
3817csn 4155 . . . . . . . . . 10 class {𝑥}
3937, 38cxp 5082 . . . . . . . . 9 class ((Base‘𝑚) × {𝑥})
405, 34cfv 5857 . . . . . . . . . 10 class ( ·𝑠𝑚)
4140cof 6860 . . . . . . . . 9 class 𝑓 ( ·𝑠𝑚)
4239, 18, 41co 6615 . . . . . . . 8 class (((Base‘𝑚) × {𝑥}) ∘𝑓 ( ·𝑠𝑚)𝑦)
4315, 16, 36, 11, 42cmpt2 6617 . . . . . . 7 class (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘𝑓 ( ·𝑠𝑚)𝑦))
4435, 43cop 4161 . . . . . 6 class ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘𝑓 ( ·𝑠𝑚)𝑦))⟩
4533, 44cpr 4157 . . . . 5 class {⟨(Scalar‘ndx), (Scalar‘𝑚)⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘𝑓 ( ·𝑠𝑚)𝑦))⟩}
4629, 45cun 3558 . . . 4 class ({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑓 (+g𝑚)𝑦))⟩, ⟨(.r‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑦))⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑚)⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘𝑓 ( ·𝑠𝑚)𝑦))⟩})
474, 7, 46csb 3519 . . 3 class (𝑚 LMHom 𝑚) / 𝑏({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑓 (+g𝑚)𝑦))⟩, ⟨(.r‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑦))⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑚)⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘𝑓 ( ·𝑠𝑚)𝑦))⟩})
482, 3, 47cmpt 4683 . 2 class (𝑚 ∈ V ↦ (𝑚 LMHom 𝑚) / 𝑏({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑓 (+g𝑚)𝑦))⟩, ⟨(.r‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑦))⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑚)⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘𝑓 ( ·𝑠𝑚)𝑦))⟩}))
491, 48wceq 1480 1 wff MEndo = (𝑚 ∈ V ↦ (𝑚 LMHom 𝑚) / 𝑏({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑓 (+g𝑚)𝑦))⟩, ⟨(.r‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑦))⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑚)⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘𝑓 ( ·𝑠𝑚)𝑦))⟩}))
 Colors of variables: wff setvar class This definition is referenced by:  mendval  37273
 Copyright terms: Public domain W3C validator