Definition df-mend

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

	Ref	Expression
Assertion	df-mend	⊢ MEndo = ( 𝑚 ∈ V ↦ ⦋ ( 𝑚 LMHom 𝑚 ) / 𝑏 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 ∘f ( +g ‘ 𝑚 ) 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 ∘ 𝑦 ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑚 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑚 ) ) , 𝑦 ∈ 𝑏 ↦ ( ( ( Base ‘ 𝑚 ) × { 𝑥 } ) ∘f ( ·𝑠 ‘ 𝑚 ) 𝑦 ) ) ⟩ } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmend	⊢ MEndo
1		vm	⊢ 𝑚
2		cvv	⊢ V
3	1	cv	⊢ 𝑚
4		clmhm	⊢ LMHom
5	3 3 4	co	⊢ ( 𝑚 LMHom 𝑚 )
6		vb	⊢ 𝑏
7		cbs	⊢ Base
8		cnx	⊢ ndx
9	8 7	cfv	⊢ ( Base ‘ ndx )
10	6	cv	⊢ 𝑏
11	9 10	cop	⊢ ⟨ ( Base ‘ ndx ) , 𝑏 ⟩
12		cplusg	⊢ +g
13	8 12	cfv	⊢ ( +g ‘ ndx )
14		vx	⊢ 𝑥
15		vy	⊢ 𝑦
16	14	cv	⊢ 𝑥
17	3 12	cfv	⊢ ( +g ‘ 𝑚 )
18	17	cof	⊢ ∘f ( +g ‘ 𝑚 )
19	15	cv	⊢ 𝑦
20	16 19 18	co	⊢ ( 𝑥 ∘f ( +g ‘ 𝑚 ) 𝑦 )
21	14 15 10 10 20	cmpo	⊢ ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 ∘f ( +g ‘ 𝑚 ) 𝑦 ) )
22	13 21	cop	⊢ ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 ∘f ( +g ‘ 𝑚 ) 𝑦 ) ) ⟩
23		cmulr	⊢ .r
24	8 23	cfv	⊢ ( .r ‘ ndx )
25	16 19	ccom	⊢ ( 𝑥 ∘ 𝑦 )
26	14 15 10 10 25	cmpo	⊢ ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 ∘ 𝑦 ) )
27	24 26	cop	⊢ ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 ∘ 𝑦 ) ) ⟩
28	11 22 27	ctp	⊢ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 ∘f ( +g ‘ 𝑚 ) 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 ∘ 𝑦 ) ) ⟩ }
29		csca	⊢ Scalar
30	8 29	cfv	⊢ ( Scalar ‘ ndx )
31	3 29	cfv	⊢ ( Scalar ‘ 𝑚 )
32	30 31	cop	⊢ ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑚 ) ⟩
33		cvsca	⊢ ·𝑠
34	8 33	cfv	⊢ ( ·𝑠 ‘ ndx )
35	31 7	cfv	⊢ ( Base ‘ ( Scalar ‘ 𝑚 ) )
36	3 7	cfv	⊢ ( Base ‘ 𝑚 )
37	16	csn	⊢ { 𝑥 }
38	36 37	cxp	⊢ ( ( Base ‘ 𝑚 ) × { 𝑥 } )
39	3 33	cfv	⊢ ( ·𝑠 ‘ 𝑚 )
40	39	cof	⊢ ∘f ( ·𝑠 ‘ 𝑚 )
41	38 19 40	co	⊢ ( ( ( Base ‘ 𝑚 ) × { 𝑥 } ) ∘f ( ·𝑠 ‘ 𝑚 ) 𝑦 )
42	14 15 35 10 41	cmpo	⊢ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑚 ) ) , 𝑦 ∈ 𝑏 ↦ ( ( ( Base ‘ 𝑚 ) × { 𝑥 } ) ∘f ( ·𝑠 ‘ 𝑚 ) 𝑦 ) )
43	34 42	cop	⊢ ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑚 ) ) , 𝑦 ∈ 𝑏 ↦ ( ( ( Base ‘ 𝑚 ) × { 𝑥 } ) ∘f ( ·𝑠 ‘ 𝑚 ) 𝑦 ) ) ⟩
44	32 43	cpr	⊢ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑚 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑚 ) ) , 𝑦 ∈ 𝑏 ↦ ( ( ( Base ‘ 𝑚 ) × { 𝑥 } ) ∘f ( ·𝑠 ‘ 𝑚 ) 𝑦 ) ) ⟩ }
45	28 44	cun	⊢ ( { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 ∘f ( +g ‘ 𝑚 ) 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 ∘ 𝑦 ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑚 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑚 ) ) , 𝑦 ∈ 𝑏 ↦ ( ( ( Base ‘ 𝑚 ) × { 𝑥 } ) ∘f ( ·𝑠 ‘ 𝑚 ) 𝑦 ) ) ⟩ } )
46	6 5 45	csb	⊢ ⦋ ( 𝑚 LMHom 𝑚 ) / 𝑏 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 ∘f ( +g ‘ 𝑚 ) 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 ∘ 𝑦 ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑚 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑚 ) ) , 𝑦 ∈ 𝑏 ↦ ( ( ( Base ‘ 𝑚 ) × { 𝑥 } ) ∘f ( ·𝑠 ‘ 𝑚 ) 𝑦 ) ) ⟩ } )
47	1 2 46	cmpt	⊢ ( 𝑚 ∈ V ↦ ⦋ ( 𝑚 LMHom 𝑚 ) / 𝑏 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 ∘f ( +g ‘ 𝑚 ) 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 ∘ 𝑦 ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑚 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑚 ) ) , 𝑦 ∈ 𝑏 ↦ ( ( ( Base ‘ 𝑚 ) × { 𝑥 } ) ∘f ( ·𝑠 ‘ 𝑚 ) 𝑦 ) ) ⟩ } ) )
48	0 47	wceq	⊢ MEndo = ( 𝑚 ∈ V ↦ ⦋ ( 𝑚 LMHom 𝑚 ) / 𝑏 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 ∘f ( +g ‘ 𝑚 ) 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 ∘ 𝑦 ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑚 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑚 ) ) , 𝑦 ∈ 𝑏 ↦ ( ( ( Base ‘ 𝑚 ) × { 𝑥 } ) ∘f ( ·𝑠 ‘ 𝑚 ) 𝑦 ) ) ⟩ } ) )