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 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 ) )
14 eqid 
 |-  ( Base ` M ) = ( Base ` M )
15 14 14 lmhmf 
 |-  ( z e. ( M LMHom M ) -> z : ( Base ` M ) --> ( Base ` M ) )
16 13 15 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 ) )
17 16 ffvelcdmda 
 |-  ( ( ( ( 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 ) )
18 16 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 ) ) )
19 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 ) )
20 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 ) )
21 eqid 
 |-  ( .s ` M ) = ( .s ` M )
22 eqid 
 |-  ( Base ` S ) = ( Base ` S )
23 eqid 
 |-  ( .s ` A ) = ( .s ` A )
24 1 21 3 2 22 14 23 mendvsca 
 |-  ( ( x e. ( Base ` S ) /\ y e. ( M LMHom M ) ) -> ( x ( .s ` A ) y ) = ( ( ( Base ` M ) X. { x } ) oF ( .s ` M ) y ) )
25 19 20 24 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 ) )
26 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 )
27 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 ) )
28 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 )
29 fconstmpt 
 |-  ( ( Base ` M ) X. { x } ) = ( w e. ( Base ` M ) |-> x )
30 29 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 ) )
31 14 14 lmhmf 
 |-  ( y e. ( M LMHom M ) -> y : ( Base ` M ) --> ( Base ` M ) )
32 20 31 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 ) )
33 32 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 ) ) )
34 26 27 28 30 33 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 ) ) ) )
35 25 34 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 ) ) ) )
36 fveq2 
 |-  ( w = ( z ` v ) -> ( y ` w ) = ( y ` ( z ` v ) ) )
37 36 oveq2d 
 |-  ( w = ( z ` v ) -> ( x ( .s ` M ) ( y ` w ) ) = ( x ( .s ` M ) ( y ` ( z ` v ) ) ) )
38 17 18 35 37 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 ) ) ) ) )
39 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 ) )
40 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 )
41 fconstmpt 
 |-  ( ( Base ` M ) X. { x } ) = ( v e. ( Base ` M ) |-> x )
42 41 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 ) )
43 eqid 
 |-  ( .r ` A ) = ( .r ` A )
44 1 3 43 mendmulr 
 |-  ( ( y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) -> ( y ( .r ` A ) z ) = ( y o. z ) )
45 20 13 44 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 ) )
46 fcompt 
 |-  ( ( y : ( Base ` M ) --> ( Base ` M ) /\ z : ( Base ` M ) --> ( Base ` M ) ) -> ( y o. z ) = ( v e. ( Base ` M ) |-> ( y ` ( z ` v ) ) ) )
47 32 16 46 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 ) ) ) )
48 45 47 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 ) ) ) )
49 26 39 40 42 48 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 ) ) ) ) )
50 38 49 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 ) ) )
51 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 )
52 3 5 23 22 lmodvscl 
 |-  ( ( A e. LMod /\ x e. ( Base ` S ) /\ y e. ( M LMHom M ) ) -> ( x ( .s ` A ) y ) e. ( M LMHom M ) )
53 51 19 20 52 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 ) )
54 1 3 43 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 ) )
55 53 13 54 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 ) )
56 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 )
57 3 43 ringcl 
 |-  ( ( A e. Ring /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) -> ( y ( .r ` A ) z ) e. ( M LMHom M ) )
58 56 20 13 57 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 ) )
59 1 21 3 2 22 14 23 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 ) ) )
60 19 58 59 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 ) ) )
61 50 55 60 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 ) ) )
62 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 ) )
63 2 22 14 21 21 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 ) ) ) )
64 62 39 17 63 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 ) ) ) )
65 64 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 ) ) ) ) )
66 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 )
67 14 2 21 22 lmodvscl 
 |-  ( ( M e. LMod /\ x e. ( Base ` S ) /\ ( z ` v ) e. ( Base ` M ) ) -> ( x ( .s ` M ) ( z ` v ) ) e. ( Base ` M ) )
68 66 39 17 67 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 ) )
69 1 21 3 2 22 14 23 mendvsca 
 |-  ( ( x e. ( Base ` S ) /\ z e. ( M LMHom M ) ) -> ( x ( .s ` A ) z ) = ( ( ( Base ` M ) X. { x } ) oF ( .s ` M ) z ) )
70 19 13 69 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 ) )
71 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 )
72 26 39 71 42 18 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 ) ) ) )
73 70 72 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 ) ) ) )
74 fveq2 
 |-  ( w = ( x ( .s ` M ) ( z ` v ) ) -> ( y ` w ) = ( y ` ( x ( .s ` M ) ( z ` v ) ) ) )
75 68 73 33 74 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 ) ) ) ) )
76 65 75 49 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 ) ) )
77 3 5 23 22 lmodvscl 
 |-  ( ( A e. LMod /\ x e. ( Base ` S ) /\ z e. ( M LMHom M ) ) -> ( x ( .s ` A ) z ) e. ( M LMHom M ) )
78 51 19 13 77 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 ) )
79 1 3 43 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 ) ) )
80 20 78 79 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 ) ) )
81 76 80 60 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 ) ) )
82 4 6 7 8 9 10 12 61 81 isassad 
 |-  ( ( M e. LMod /\ S e. CRing ) -> A e. AssAlg )