Definition df-mend 41489

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

Step	Hyp	Ref	Expression
1		cmend 41488	. 2 class MEndo
2		vm	. . 3 setvar 𝑚
3		cvv 3445	. . 3 class V
4		vb	. . . 4 setvar 𝑏
5	2	cv 1540	. . . . 5 class 𝑚
6		clmhm 20480	. . . . 5 class LMHom
7	5, 5, 6	co 7357	. . . 4 class (𝑚 LMHom 𝑚)
8		cnx 17065	. . . . . . . 8 class ndx
9		cbs 17083	. . . . . . . 8 class Base
10	8, 9	cfv 6496	. . . . . . 7 class (Base‘ndx)
11	4	cv 1540	. . . . . . 7 class 𝑏
12	10, 11	cop 4592	. . . . . 6 class ⟨(Base‘ndx), 𝑏⟩
13		cplusg 17133	. . . . . . . 8 class +g
14	8, 13	cfv 6496	. . . . . . 7 class (+g‘ndx)
15		vx	. . . . . . . 8 setvar 𝑥
16		vy	. . . . . . . 8 setvar 𝑦
17	15	cv 1540	. . . . . . . . 9 class 𝑥
18	16	cv 1540	. . . . . . . . 9 class 𝑦
19	5, 13	cfv 6496	. . . . . . . . . 10 class (+g‘𝑚)
20	19	cof 7615	. . . . . . . . 9 class ∘f (+g‘𝑚)
21	17, 18, 20	co 7357	. . . . . . . 8 class (𝑥 ∘f (+g‘𝑚)𝑦)
22	15, 16, 11, 11, 21	cmpo 7359	. . . . . . 7 class (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘f (+g‘𝑚)𝑦))
23	14, 22	cop 4592	. . . . . 6 class ⟨(+g‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘f (+g‘𝑚)𝑦))⟩
24		cmulr 17134	. . . . . . . 8 class .r
25	8, 24	cfv 6496	. . . . . . 7 class (.r‘ndx)
26	17, 18	ccom 5637	. . . . . . . 8 class (𝑥 ∘ 𝑦)
27	15, 16, 11, 11, 26	cmpo 7359	. . . . . . 7 class (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦))
28	25, 27	cop 4592	. . . . . 6 class ⟨(.r‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦))⟩
29	12, 23, 28	ctp 4590	. . . . 5 class {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘f (+g‘𝑚)𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦))⟩}
30		csca 17136	. . . . . . . 8 class Scalar
31	8, 30	cfv 6496	. . . . . . 7 class (Scalar‘ndx)
32	5, 30	cfv 6496	. . . . . . 7 class (Scalar‘𝑚)
33	31, 32	cop 4592	. . . . . 6 class ⟨(Scalar‘ndx), (Scalar‘𝑚)⟩
34		cvsca 17137	. . . . . . . 8 class ·𝑠
35	8, 34	cfv 6496	. . . . . . 7 class ( ·𝑠 ‘ndx)
36	32, 9	cfv 6496	. . . . . . . 8 class (Base‘(Scalar‘𝑚))
37	5, 9	cfv 6496	. . . . . . . . . 10 class (Base‘𝑚)
38	17	csn 4586	. . . . . . . . . 10 class {𝑥}
39	37, 38	cxp 5631	. . . . . . . . 9 class ((Base‘𝑚) × {𝑥})
40	5, 34	cfv 6496	. . . . . . . . . 10 class ( ·𝑠 ‘𝑚)
41	40	cof 7615	. . . . . . . . 9 class ∘f ( ·𝑠 ‘𝑚)
42	39, 18, 41	co 7357	. . . . . . . 8 class (((Base‘𝑚) × {𝑥}) ∘f ( ·𝑠 ‘𝑚)𝑦)
43	15, 16, 36, 11, 42	cmpo 7359	. . . . . . 7 class (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f ( ·𝑠 ‘𝑚)𝑦))
44	35, 43	cop 4592	. . . . . 6 class ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f ( ·𝑠 ‘𝑚)𝑦))⟩
45	33, 44	cpr 4588	. . . . 5 class {⟨(Scalar‘ndx), (Scalar‘𝑚)⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f ( ·𝑠 ‘𝑚)𝑦))⟩}
46	29, 45	cun 3908	. . . 4 class ({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘f (+g‘𝑚)𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦))⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑚)⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f ( ·𝑠 ‘𝑚)𝑦))⟩})
47	4, 7, 46	csb 3855	. . 3 class ⦋(𝑚 LMHom 𝑚) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘f (+g‘𝑚)𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦))⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑚)⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f ( ·𝑠 ‘𝑚)𝑦))⟩})
48	2, 3, 47	cmpt 5188	. 2 class (𝑚 ∈ V ↦ ⦋(𝑚 LMHom 𝑚) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘f (+g‘𝑚)𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦))⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑚)⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f ( ·𝑠 ‘𝑚)𝑦))⟩}))
49	1, 48	wceq 1541	1 wff MEndo = (𝑚 ∈ V ↦ ⦋(𝑚 LMHom 𝑚) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘f (+g‘𝑚)𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦))⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑚)⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f ( ·𝑠 ‘𝑚)𝑦))⟩}))

This definition is referenced by:  mendval  41496