Metamath Proof Explorer

Theorem mendassa

Description: The module endomorphism algebra is an algebra. (Contributed by Mario Carneiro, 22-Sep-2015)

Ref Expression
Hypotheses mendassa.a 
|- A = ( MEndo ` M )
mendassa.s 
|- S = ( Scalar ` M )
Assertion mendassa 
|- ( ( M e. LMod /\ S e. CRing ) -> A e. AssAlg )

Proof

Step Hyp Ref Expression
1 mendassa.a 
 |-  A = ( MEndo ` M )
2 mendassa.s 
 |-  S = ( Scalar ` M )
3 1 mendbas 
 |-  ( M LMHom M ) = ( Base ` A )
4 3 a1i 
 |-  ( ( M e. LMod /\ S e. CRing ) -> ( M LMHom M ) = ( Base ` A ) )
5 1 2 mendsca 
 |-  S = ( Scalar ` A )
6 5 a1i 
 |-  ( ( M e. LMod /\ S e. CRing ) -> S = ( Scalar ` A ) )
7 eqidd 
 |-  ( ( M e. LMod /\ S e. CRing ) -> ( Base ` S ) = ( Base ` S ) )
8 eqidd 
 |-  ( ( M e. LMod /\ S e. CRing ) -> ( .s ` A ) = ( .s ` A ) )
9 eqidd 
 |-  ( ( M e. LMod /\ S e. CRing ) -> ( .r ` A ) = ( .r ` A ) )
10 1 2 mendlmod 
 |-  ( ( M e. LMod /\ S e. CRing ) -> A e. LMod )
11 1 mendring 
 |-  ( M e. LMod -> A e. Ring )
12 11 adantr 
 |-  ( ( M e. LMod /\ S e. CRing ) -> A e. Ring )
13 simpr 
 |-  ( ( M e. LMod /\ S e. CRing ) -> S e. CRing )
14 simpr3 
 |-  ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> z e. ( M LMHom M ) )
15 eqid 
 |-  ( Base ` M ) = ( Base ` M )
16 15 15 lmhmf 
 |-  ( z e. ( M LMHom M ) -> z : ( Base ` M ) --> ( Base ` M ) )
17 14 16 syl 
 |-  ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> z : ( Base ` M ) --> ( Base ` M ) )
18 17 ffvelrnda 
 |-  ( ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) /\ v e. ( Base ` M ) ) -> ( z ` v ) e. ( Base ` M ) )
19 17 feqmptd 
 |-  ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> z = ( v e. ( Base ` M ) |-> ( z ` v ) ) )
20 simpr1 
 |-  ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> x e. ( Base ` S ) )
21 simpr2 
 |-  ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> y e. ( M LMHom M ) )
22 eqid 
 |-  ( .s ` M ) = ( .s ` M )
23 eqid 
 |-  ( Base ` S ) = ( Base ` S )
24 eqid 
 |-  ( .s ` A ) = ( .s ` A )
25 1 22 3 2 23 15 24 mendvsca 
 |-  ( ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) ) -> ( x ( .s ` A ) y ) = ( ( ( Base ` M ) X. { x } ) oF ( .s ` M ) y ) )
26 20 21 25 syl2anc 
 |-  ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( x ( .s ` A ) y ) = ( ( ( Base ` M ) X. { x } ) oF ( .s ` M ) y ) )
27 fvexd 
 |-  ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( Base ` M ) e. _V )
28 simplr1 
 |-  ( ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) /\ w e. ( Base ` M ) ) -> x e. ( Base ` S ) )
29 fvexd 
 |-  ( ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) /\ w e. ( Base ` M ) ) -> ( y ` w ) e. _V )
30 fconstmpt 
 |-  ( ( Base ` M ) X. { x } ) = ( w e. ( Base ` M ) |-> x )
31 30 a1i 
 |-  ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( ( Base ` M ) X. { x } ) = ( w e. ( Base ` M ) |-> x ) )
32 15 15 lmhmf 
 |-  ( y e. ( M LMHom M ) -> y : ( Base ` M ) --> ( Base ` M ) )
33 21 32 syl 
 |-  ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> y : ( Base ` M ) --> ( Base ` M ) )
34 33 feqmptd 
 |-  ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> y = ( w e. ( Base ` M ) |-> ( y ` w ) ) )
35 27 28 29 31 34 offval2 
 |-  ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( ( ( Base ` M ) X. { x } ) oF ( .s ` M ) y ) = ( w e. ( Base ` M ) |-> ( x ( .s ` M ) ( y ` w ) ) ) )
36 26 35 eqtrd 
 |-  ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( x ( .s ` A ) y ) = ( w e. ( Base ` M ) |-> ( x ( .s ` M ) ( y ` w ) ) ) )
37 fveq2 
 |-  ( w = ( z ` v ) -> ( y ` w ) = ( y ` ( z ` v ) ) )
38 37 oveq2d 
 |-  ( w = ( z ` v ) -> ( x ( .s ` M ) ( y ` w ) ) = ( x ( .s ` M ) ( y ` ( z ` v ) ) ) )
39 18 19 36 38 fmptco 
 |-  ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( ( x ( .s ` A ) y ) o. z ) = ( v e. ( Base ` M ) |-> ( x ( .s ` M ) ( y ` ( z ` v ) ) ) ) )
40 simplr1 
 |-  ( ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) /\ v e. ( Base ` M ) ) -> x e. ( Base ` S ) )
41 fvexd 
 |-  ( ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) /\ v e. ( Base ` M ) ) -> ( y ` ( z ` v ) ) e. _V )
42 fconstmpt 
 |-  ( ( Base ` M ) X. { x } ) = ( v e. ( Base ` M ) |-> x )
43 42 a1i 
 |-  ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( ( Base ` M ) X. { x } ) = ( v e. ( Base ` M ) |-> x ) )
44 eqid 
 |-  ( .r ` A ) = ( .r ` A )
45 1 3 44 mendmulr 
 |-  ( ( y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) -> ( y ( .r ` A ) z ) = ( y o. z ) )
46 21 14 45 syl2anc 
 |-  ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( y ( .r ` A ) z ) = ( y o. z ) )
47 fcompt 
 |-  ( ( y : ( Base ` M ) --> ( Base ` M ) /\ z : ( Base ` M ) --> ( Base ` M ) ) -> ( y o. z ) = ( v e. ( Base ` M ) |-> ( y ` ( z ` v ) ) ) )
48 33 17 47 syl2anc 
 |-  ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( y o. z ) = ( v e. ( Base ` M ) |-> ( y ` ( z ` v ) ) ) )
49 46 48 eqtrd 
 |-  ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( y ( .r ` A ) z ) = ( v e. ( Base ` M ) |-> ( y ` ( z ` v ) ) ) )
50 27 40 41 43 49 offval2 
 |-  ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( ( ( Base ` M ) X. { x } ) oF ( .s ` M ) ( y ( .r ` A ) z ) ) = ( v e. ( Base ` M ) |-> ( x ( .s ` M ) ( y ` ( z ` v ) ) ) ) )
51 39 50 eqtr4d 
 |-  ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( ( x ( .s ` A ) y ) o. z ) = ( ( ( Base ` M ) X. { x } ) oF ( .s ` M ) ( y ( .r ` A ) z ) ) )
52 10 adantr 
 |-  ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> A e. LMod )
53 3 5 24 23 lmodvscl 
 |-  ( ( A e. LMod /\ x e. ( Base ` S ) /\ y e. ( M LMHom M ) ) -> ( x ( .s ` A ) y ) e. ( M LMHom M ) )
54 52 20 21 53 syl3anc 
 |-  ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( x ( .s ` A ) y ) e. ( M LMHom M ) )
55 1 3 44 mendmulr 
 |-  ( ( ( x ( .s ` A ) y ) e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) -> ( ( x ( .s ` A ) y ) ( .r ` A ) z ) = ( ( x ( .s ` A ) y ) o. z ) )
56 54 14 55 syl2anc 
 |-  ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( ( x ( .s ` A ) y ) ( .r ` A ) z ) = ( ( x ( .s ` A ) y ) o. z ) )
57 12 adantr 
 |-  ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> A e. Ring )
58 3 44 ringcl 
 |-  ( ( A e. Ring /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) -> ( y ( .r ` A ) z ) e. ( M LMHom M ) )
59 57 21 14 58 syl3anc 
 |-  ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( y ( .r ` A ) z ) e. ( M LMHom M ) )
60 1 22 3 2 23 15 24 mendvsca 
 |-  ( ( x e. ( Base ` S ) /\ ( y ( .r ` A ) z ) e. ( M LMHom M ) ) -> ( x ( .s ` A ) ( y ( .r ` A ) z ) ) = ( ( ( Base ` M ) X. { x } ) oF ( .s ` M ) ( y ( .r ` A ) z ) ) )
61 20 59 60 syl2anc 
 |-  ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( x ( .s ` A ) ( y ( .r ` A ) z ) ) = ( ( ( Base ` M ) X. { x } ) oF ( .s ` M ) ( y ( .r ` A ) z ) ) )
62 51 56 61 3eqtr4d 
 |-  ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( ( x ( .s ` A ) y ) ( .r ` A ) z ) = ( x ( .s ` A ) ( y ( .r ` A ) z ) ) )
63 simplr2 
 |-  ( ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) /\ v e. ( Base ` M ) ) -> y e. ( M LMHom M ) )
64 2 23 15 22 22 lmhmlin 
 |-  ( ( y e. ( M LMHom M ) /\ x e. ( Base ` S ) /\ ( z ` v ) e. ( Base ` M ) ) -> ( y ` ( x ( .s ` M ) ( z ` v ) ) ) = ( x ( .s ` M ) ( y ` ( z ` v ) ) ) )
65 63 40 18 64 syl3anc 
 |-  ( ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) /\ v e. ( Base ` M ) ) -> ( y ` ( x ( .s ` M ) ( z ` v ) ) ) = ( x ( .s ` M ) ( y ` ( z ` v ) ) ) )
66 65 mpteq2dva 
 |-  ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( v e. ( Base ` M ) |-> ( y ` ( x ( .s ` M ) ( z ` v ) ) ) ) = ( v e. ( Base ` M ) |-> ( x ( .s ` M ) ( y ` ( z ` v ) ) ) ) )
67 simplll 
 |-  ( ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) /\ v e. ( Base ` M ) ) -> M e. LMod )
68 15 2 22 23 lmodvscl 
 |-  ( ( M e. LMod /\ x e. ( Base ` S ) /\ ( z ` v ) e. ( Base ` M ) ) -> ( x ( .s ` M ) ( z ` v ) ) e. ( Base ` M ) )
69 67 40 18 68 syl3anc 
 |-  ( ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) /\ v e. ( Base ` M ) ) -> ( x ( .s ` M ) ( z ` v ) ) e. ( Base ` M ) )
70 1 22 3 2 23 15 24 mendvsca 
 |-  ( ( x e. ( Base ` S ) /\ z e. ( M LMHom M ) ) -> ( x ( .s ` A ) z ) = ( ( ( Base ` M ) X. { x } ) oF ( .s ` M ) z ) )
71 20 14 70 syl2anc 
 |-  ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( x ( .s ` A ) z ) = ( ( ( Base ` M ) X. { x } ) oF ( .s ` M ) z ) )
72 fvexd 
 |-  ( ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) /\ v e. ( Base ` M ) ) -> ( z ` v ) e. _V )
73 27 40 72 43 19 offval2 
 |-  ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( ( ( Base ` M ) X. { x } ) oF ( .s ` M ) z ) = ( v e. ( Base ` M ) |-> ( x ( .s ` M ) ( z ` v ) ) ) )
74 71 73 eqtrd 
 |-  ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( x ( .s ` A ) z ) = ( v e. ( Base ` M ) |-> ( x ( .s ` M ) ( z ` v ) ) ) )
75 fveq2 
 |-  ( w = ( x ( .s ` M ) ( z ` v ) ) -> ( y ` w ) = ( y ` ( x ( .s ` M ) ( z ` v ) ) ) )
76 69 74 34 75 fmptco 
 |-  ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( y o. ( x ( .s ` A ) z ) ) = ( v e. ( Base ` M ) |-> ( y ` ( x ( .s ` M ) ( z ` v ) ) ) ) )
77 66 76 50 3eqtr4d 
 |-  ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( y o. ( x ( .s ` A ) z ) ) = ( ( ( Base ` M ) X. { x } ) oF ( .s ` M ) ( y ( .r ` A ) z ) ) )
78 3 5 24 23 lmodvscl 
 |-  ( ( A e. LMod /\ x e. ( Base ` S ) /\ z e. ( M LMHom M ) ) -> ( x ( .s ` A ) z ) e. ( M LMHom M ) )
79 52 20 14 78 syl3anc 
 |-  ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( x ( .s ` A ) z ) e. ( M LMHom M ) )
80 1 3 44 mendmulr 
 |-  ( ( y e. ( M LMHom M ) /\ ( x ( .s ` A ) z ) e. ( M LMHom M ) ) -> ( y ( .r ` A ) ( x ( .s ` A ) z ) ) = ( y o. ( x ( .s ` A ) z ) ) )
81 21 79 80 syl2anc 
 |-  ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( y ( .r ` A ) ( x ( .s ` A ) z ) ) = ( y o. ( x ( .s ` A ) z ) ) )
82 77 81 61 3eqtr4d 
 |-  ( ( ( M e. LMod /\ S e. CRing ) /\ ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( y ( .r ` A ) ( x ( .s ` A ) z ) ) = ( x ( .s ` A ) ( y ( .r ` A ) z ) ) )
83 4 6 7 8 9 10 12 13 62 82 isassad 
 |-  ( ( M e. LMod /\ S e. CRing ) -> A e. AssAlg )