Definition df-mend 37746

Description: Define the endomorphism algebra of a module. (Contributed by Stefan O'Rear, 2-Sep-2015.)

Assertion

Ref	Expression
df-mend	|- MEndo = ( m e. _V |-> [_ ( m LMHom m ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( x e. b , y e. b |-> ( x oF ( +g ` m ) y ) ) >. , <. ( .r ` ndx ) , ( x e. b , y e. b |-> ( x o. y ) ) >. } u. { <. (Scalar ` ndx ) , (Scalar ` m ) >. , <. ( .s ` ndx ) , ( x e. ( Base ` (Scalar ` m ) ) , y e. b |-> ( ( ( Base ` m ) X. { x } ) oF ( .s ` m ) y ) ) >. } ) )

Distinct variable group:   m, b, x, y

Detailed syntax breakdown of Definition df-mend

Step	Hyp	Ref	Expression
1		cmend 37745	. 2 class MEndo
2		vm	. . 3 setvar m
3		cvv 3200	. . 3 class _V
4		vb	. . . 4 setvar b
5	2	cv 1482	. . . . 5 class m
6		clmhm 19019	. . . . 5 class LMHom
7	5, 5, 6	co 6650	. . . 4 class ( m LMHom m )
8		cnx 15854	. . . . . . . 8 class ndx
9		cbs 15857	. . . . . . . 8 class Base
10	8, 9	cfv 5888	. . . . . . 7 class ( Base ` ndx )
11	4	cv 1482	. . . . . . 7 class b
12	10, 11	cop 4183	. . . . . 6 class <. ( Base ` ndx ) , b >.
13		cplusg 15941	. . . . . . . 8 class +g
14	8, 13	cfv 5888	. . . . . . 7 class ( +g ` ndx )
15		vx	. . . . . . . 8 setvar x
16		vy	. . . . . . . 8 setvar y
17	15	cv 1482	. . . . . . . . 9 class x
18	16	cv 1482	. . . . . . . . 9 class y
19	5, 13	cfv 5888	. . . . . . . . . 10 class ( +g ` m )
20	19	cof 6895	. . . . . . . . 9 class oF ( +g ` m )
21	17, 18, 20	co 6650	. . . . . . . 8 class ( x oF ( +g ` m ) y )
22	15, 16, 11, 11, 21	cmpt2 6652	. . . . . . 7 class ( x e. b , y e. b |-> ( x oF ( +g ` m ) y ) )
23	14, 22	cop 4183	. . . . . 6 class <. ( +g ` ndx ) , ( x e. b , y e. b |-> ( x oF ( +g ` m ) y ) ) >.
24		cmulr 15942	. . . . . . . 8 class .r
25	8, 24	cfv 5888	. . . . . . 7 class ( .r ` ndx )
26	17, 18	ccom 5118	. . . . . . . 8 class ( x o. y )
27	15, 16, 11, 11, 26	cmpt2 6652	. . . . . . 7 class ( x e. b , y e. b |-> ( x o. y ) )
28	25, 27	cop 4183	. . . . . 6 class <. ( .r ` ndx ) , ( x e. b , y e. b |-> ( x o. y ) ) >.
29	12, 23, 28	ctp 4181	. . . . 5 class { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( x e. b , y e. b |-> ( x oF ( +g ` m ) y ) ) >. , <. ( .r ` ndx ) , ( x e. b , y e. b |-> ( x o. y ) ) >. }
30		csca 15944	. . . . . . . 8 class Scalar
31	8, 30	cfv 5888	. . . . . . 7 class (Scalar ` ndx )
32	5, 30	cfv 5888	. . . . . . 7 class (Scalar ` m )
33	31, 32	cop 4183	. . . . . 6 class <. (Scalar ` ndx ) , (Scalar ` m ) >.
34		cvsca 15945	. . . . . . . 8 class .s
35	8, 34	cfv 5888	. . . . . . 7 class ( .s ` ndx )
36	32, 9	cfv 5888	. . . . . . . 8 class ( Base ` (Scalar ` m ) )
37	5, 9	cfv 5888	. . . . . . . . . 10 class ( Base ` m )
38	17	csn 4177	. . . . . . . . . 10 class { x }
39	37, 38	cxp 5112	. . . . . . . . 9 class ( ( Base ` m ) X. { x } )
40	5, 34	cfv 5888	. . . . . . . . . 10 class ( .s ` m )
41	40	cof 6895	. . . . . . . . 9 class oF ( .s ` m )
42	39, 18, 41	co 6650	. . . . . . . 8 class ( ( ( Base ` m ) X. { x } ) oF ( .s ` m ) y )
43	15, 16, 36, 11, 42	cmpt2 6652	. . . . . . 7 class ( x e. ( Base ` (Scalar ` m ) ) , y e. b |-> ( ( ( Base ` m ) X. { x } ) oF ( .s ` m ) y ) )
44	35, 43	cop 4183	. . . . . 6 class <. ( .s ` ndx ) , ( x e. ( Base ` (Scalar ` m ) ) , y e. b |-> ( ( ( Base ` m ) X. { x } ) oF ( .s ` m ) y ) ) >.
45	33, 44	cpr 4179	. . . . 5 class { <. (Scalar ` ndx ) , (Scalar ` m ) >. , <. ( .s ` ndx ) , ( x e. ( Base ` (Scalar ` m ) ) , y e. b |-> ( ( ( Base ` m ) X. { x } ) oF ( .s ` m ) y ) ) >. }
46	29, 45	cun 3572	. . . 4 class ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( x e. b , y e. b |-> ( x oF ( +g ` m ) y ) ) >. , <. ( .r ` ndx ) , ( x e. b , y e. b |-> ( x o. y ) ) >. } u. { <. (Scalar ` ndx ) , (Scalar ` m ) >. , <. ( .s ` ndx ) , ( x e. ( Base ` (Scalar ` m ) ) , y e. b |-> ( ( ( Base ` m ) X. { x } ) oF ( .s ` m ) y ) ) >. } )
47	4, 7, 46	csb 3533	. . 3 class [_ ( m LMHom m ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( x e. b , y e. b |-> ( x oF ( +g ` m ) y ) ) >. , <. ( .r ` ndx ) , ( x e. b , y e. b |-> ( x o. y ) ) >. } u. { <. (Scalar ` ndx ) , (Scalar ` m ) >. , <. ( .s ` ndx ) , ( x e. ( Base ` (Scalar ` m ) ) , y e. b |-> ( ( ( Base ` m ) X. { x } ) oF ( .s ` m ) y ) ) >. } )
48	2, 3, 47	cmpt 4729	. 2 class ( m e. _V |-> [_ ( m LMHom m ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( x e. b , y e. b |-> ( x oF ( +g ` m ) y ) ) >. , <. ( .r ` ndx ) , ( x e. b , y e. b |-> ( x o. y ) ) >. } u. { <. (Scalar ` ndx ) , (Scalar ` m ) >. , <. ( .s ` ndx ) , ( x e. ( Base ` (Scalar ` m ) ) , y e. b |-> ( ( ( Base ` m ) X. { x } ) oF ( .s ` m ) y ) ) >. } ) )
49	1, 48	wceq 1483	1 wff MEndo = ( m e. _V |-> [_ ( m LMHom m ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( x e. b , y e. b |-> ( x oF ( +g ` m ) y ) ) >. , <. ( .r ` ndx ) , ( x e. b , y e. b |-> ( x o. y ) ) >. } u. { <. (Scalar ` ndx ) , (Scalar ` m ) >. , <. ( .s ` ndx ) , ( x e. ( Base ` (Scalar ` m ) ) , y e. b |-> ( ( ( Base ` m ) X. { x } ) oF ( .s ` m ) y ) ) >. } ) )

This definition is referenced by:  mendval  37753