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 41546
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 41545 . 2 class MEndo
2 vm . . 3 setvar π‘š
3 cvv 3444 . . 3 class V
4 vb . . . 4 setvar 𝑏
52cv 1541 . . . . 5 class π‘š
6 clmhm 20495 . . . . 5 class LMHom
75, 5, 6co 7358 . . . 4 class (π‘š LMHom π‘š)
8 cnx 17070 . . . . . . . 8 class ndx
9 cbs 17088 . . . . . . . 8 class Base
108, 9cfv 6497 . . . . . . 7 class (Baseβ€˜ndx)
114cv 1541 . . . . . . 7 class 𝑏
1210, 11cop 4593 . . . . . 6 class ⟨(Baseβ€˜ndx), π‘βŸ©
13 cplusg 17138 . . . . . . . 8 class +g
148, 13cfv 6497 . . . . . . 7 class (+gβ€˜ndx)
15 vx . . . . . . . 8 setvar π‘₯
16 vy . . . . . . . 8 setvar 𝑦
1715cv 1541 . . . . . . . . 9 class π‘₯
1816cv 1541 . . . . . . . . 9 class 𝑦
195, 13cfv 6497 . . . . . . . . . 10 class (+gβ€˜π‘š)
2019cof 7616 . . . . . . . . 9 class ∘f (+gβ€˜π‘š)
2117, 18, 20co 7358 . . . . . . . 8 class (π‘₯ ∘f (+gβ€˜π‘š)𝑦)
2215, 16, 11, 11, 21cmpo 7360 . . . . . . 7 class (π‘₯ ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (π‘₯ ∘f (+gβ€˜π‘š)𝑦))
2314, 22cop 4593 . . . . . 6 class ⟨(+gβ€˜ndx), (π‘₯ ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (π‘₯ ∘f (+gβ€˜π‘š)𝑦))⟩
24 cmulr 17139 . . . . . . . 8 class .r
258, 24cfv 6497 . . . . . . 7 class (.rβ€˜ndx)
2617, 18ccom 5638 . . . . . . . 8 class (π‘₯ ∘ 𝑦)
2715, 16, 11, 11, 26cmpo 7360 . . . . . . 7 class (π‘₯ ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (π‘₯ ∘ 𝑦))
2825, 27cop 4593 . . . . . 6 class ⟨(.rβ€˜ndx), (π‘₯ ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (π‘₯ ∘ 𝑦))⟩
2912, 23, 28ctp 4591 . . . . 5 class {⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(+gβ€˜ndx), (π‘₯ ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (π‘₯ ∘f (+gβ€˜π‘š)𝑦))⟩, ⟨(.rβ€˜ndx), (π‘₯ ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (π‘₯ ∘ 𝑦))⟩}
30 csca 17141 . . . . . . . 8 class Scalar
318, 30cfv 6497 . . . . . . 7 class (Scalarβ€˜ndx)
325, 30cfv 6497 . . . . . . 7 class (Scalarβ€˜π‘š)
3331, 32cop 4593 . . . . . 6 class ⟨(Scalarβ€˜ndx), (Scalarβ€˜π‘š)⟩
34 cvsca 17142 . . . . . . . 8 class ·𝑠
358, 34cfv 6497 . . . . . . 7 class ( ·𝑠 β€˜ndx)
3632, 9cfv 6497 . . . . . . . 8 class (Baseβ€˜(Scalarβ€˜π‘š))
375, 9cfv 6497 . . . . . . . . . 10 class (Baseβ€˜π‘š)
3817csn 4587 . . . . . . . . . 10 class {π‘₯}
3937, 38cxp 5632 . . . . . . . . 9 class ((Baseβ€˜π‘š) Γ— {π‘₯})
405, 34cfv 6497 . . . . . . . . . 10 class ( ·𝑠 β€˜π‘š)
4140cof 7616 . . . . . . . . 9 class ∘f ( ·𝑠 β€˜π‘š)
4239, 18, 41co 7358 . . . . . . . 8 class (((Baseβ€˜π‘š) Γ— {π‘₯}) ∘f ( ·𝑠 β€˜π‘š)𝑦)
4315, 16, 36, 11, 42cmpo 7360 . . . . . . 7 class (π‘₯ ∈ (Baseβ€˜(Scalarβ€˜π‘š)), 𝑦 ∈ 𝑏 ↦ (((Baseβ€˜π‘š) Γ— {π‘₯}) ∘f ( ·𝑠 β€˜π‘š)𝑦))
4435, 43cop 4593 . . . . . 6 class ⟨( ·𝑠 β€˜ndx), (π‘₯ ∈ (Baseβ€˜(Scalarβ€˜π‘š)), 𝑦 ∈ 𝑏 ↦ (((Baseβ€˜π‘š) Γ— {π‘₯}) ∘f ( ·𝑠 β€˜π‘š)𝑦))⟩
4533, 44cpr 4589 . . . . 5 class {⟨(Scalarβ€˜ndx), (Scalarβ€˜π‘š)⟩, ⟨( ·𝑠 β€˜ndx), (π‘₯ ∈ (Baseβ€˜(Scalarβ€˜π‘š)), 𝑦 ∈ 𝑏 ↦ (((Baseβ€˜π‘š) Γ— {π‘₯}) ∘f ( ·𝑠 β€˜π‘š)𝑦))⟩}
4629, 45cun 3909 . . . 4 class ({⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(+gβ€˜ndx), (π‘₯ ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (π‘₯ ∘f (+gβ€˜π‘š)𝑦))⟩, ⟨(.rβ€˜ndx), (π‘₯ ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (π‘₯ ∘ 𝑦))⟩} βˆͺ {⟨(Scalarβ€˜ndx), (Scalarβ€˜π‘š)⟩, ⟨( ·𝑠 β€˜ndx), (π‘₯ ∈ (Baseβ€˜(Scalarβ€˜π‘š)), 𝑦 ∈ 𝑏 ↦ (((Baseβ€˜π‘š) Γ— {π‘₯}) ∘f ( ·𝑠 β€˜π‘š)𝑦))⟩})
474, 7, 46csb 3856 . . 3 class ⦋(π‘š LMHom π‘š) / π‘β¦Œ({⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(+gβ€˜ndx), (π‘₯ ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (π‘₯ ∘f (+gβ€˜π‘š)𝑦))⟩, ⟨(.rβ€˜ndx), (π‘₯ ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (π‘₯ ∘ 𝑦))⟩} βˆͺ {⟨(Scalarβ€˜ndx), (Scalarβ€˜π‘š)⟩, ⟨( ·𝑠 β€˜ndx), (π‘₯ ∈ (Baseβ€˜(Scalarβ€˜π‘š)), 𝑦 ∈ 𝑏 ↦ (((Baseβ€˜π‘š) Γ— {π‘₯}) ∘f ( ·𝑠 β€˜π‘š)𝑦))⟩})
482, 3, 47cmpt 5189 . 2 class (π‘š ∈ V ↦ ⦋(π‘š LMHom π‘š) / π‘β¦Œ({⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(+gβ€˜ndx), (π‘₯ ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (π‘₯ ∘f (+gβ€˜π‘š)𝑦))⟩, ⟨(.rβ€˜ndx), (π‘₯ ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (π‘₯ ∘ 𝑦))⟩} βˆͺ {⟨(Scalarβ€˜ndx), (Scalarβ€˜π‘š)⟩, ⟨( ·𝑠 β€˜ndx), (π‘₯ ∈ (Baseβ€˜(Scalarβ€˜π‘š)), 𝑦 ∈ 𝑏 ↦ (((Baseβ€˜π‘š) Γ— {π‘₯}) ∘f ( ·𝑠 β€˜π‘š)𝑦))⟩}))
491, 48wceq 1542 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  41553
  Copyright terms: Public domain W3C validator