Metamath Proof Explorer

Theorem mendring

Description: The module endomorphism algebra is a ring. (Contributed by Stefan O'Rear, 5-Sep-2015)

Ref Expression
Hypothesis mendassa.a 
|- A = ( MEndo ` M )
Assertion mendring 
|- ( M e. LMod -> A e. Ring )

Proof

Step Hyp Ref Expression
1 mendassa.a 
 |-  A = ( MEndo ` M )
2 1 mendbas 
 |-  ( M LMHom M ) = ( Base ` A )
3 2 a1i 
 |-  ( M e. LMod -> ( M LMHom M ) = ( Base ` A ) )
4 eqidd 
 |-  ( M e. LMod -> ( +g ` A ) = ( +g ` A ) )
5 eqidd 
 |-  ( M e. LMod -> ( .r ` A ) = ( .r ` A ) )
6 eqid 
 |-  ( +g ` M ) = ( +g ` M )
7 eqid 
 |-  ( +g ` A ) = ( +g ` A )
8 1 2 6 7 mendplusg 
 |-  ( ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) ) -> ( x ( +g ` A ) y ) = ( x oF ( +g ` M ) y ) )
9 6 lmhmplusg 
 |-  ( ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) ) -> ( x oF ( +g ` M ) y ) e. ( M LMHom M ) )
10 8 9 eqeltrd 
 |-  ( ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) ) -> ( x ( +g ` A ) y ) e. ( M LMHom M ) )
11 10 3adant1 
 |-  ( ( M e. LMod /\ x e. ( M LMHom M ) /\ y e. ( M LMHom M ) ) -> ( x ( +g ` A ) y ) e. ( M LMHom M ) )
12 simpr1 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> x e. ( M LMHom M ) )
13 simpr2 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> y e. ( M LMHom M ) )
14 12 13 9 syl2anc 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( x oF ( +g ` M ) y ) e. ( M LMHom M ) )
15 simpr3 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> z e. ( M LMHom M ) )
16 1 2 6 7 mendplusg 
 |-  ( ( ( x oF ( +g ` M ) y ) e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) -> ( ( x oF ( +g ` M ) y ) ( +g ` A ) z ) = ( ( x oF ( +g ` M ) y ) oF ( +g ` M ) z ) )
17 14 15 16 syl2anc 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( ( x oF ( +g ` M ) y ) ( +g ` A ) z ) = ( ( x oF ( +g ` M ) y ) oF ( +g ` M ) z ) )
18 12 13 8 syl2anc 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( x ( +g ` A ) y ) = ( x oF ( +g ` M ) y ) )
19 18 oveq1d 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( ( x ( +g ` A ) y ) ( +g ` A ) z ) = ( ( x oF ( +g ` M ) y ) ( +g ` A ) z ) )
20 6 lmhmplusg 
 |-  ( ( y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) -> ( y oF ( +g ` M ) z ) e. ( M LMHom M ) )
21 13 15 20 syl2anc 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( y oF ( +g ` M ) z ) e. ( M LMHom M ) )
22 1 2 6 7 mendplusg 
 |-  ( ( x e. ( M LMHom M ) /\ ( y oF ( +g ` M ) z ) e. ( M LMHom M ) ) -> ( x ( +g ` A ) ( y oF ( +g ` M ) z ) ) = ( x oF ( +g ` M ) ( y oF ( +g ` M ) z ) ) )
23 12 21 22 syl2anc 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( x ( +g ` A ) ( y oF ( +g ` M ) z ) ) = ( x oF ( +g ` M ) ( y oF ( +g ` M ) z ) ) )
24 1 2 6 7 mendplusg 
 |-  ( ( y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) -> ( y ( +g ` A ) z ) = ( y oF ( +g ` M ) z ) )
25 13 15 24 syl2anc 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( y ( +g ` A ) z ) = ( y oF ( +g ` M ) z ) )
26 25 oveq2d 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( x ( +g ` A ) ( y ( +g ` A ) z ) ) = ( x ( +g ` A ) ( y oF ( +g ` M ) z ) ) )
27 lmodgrp 
 |-  ( M e. LMod -> M e. Grp )
28 27 grpmndd 
 |-  ( M e. LMod -> M e. Mnd )
29 28 adantr 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> M e. Mnd )
30 eqid 
 |-  ( Base ` M ) = ( Base ` M )
31 30 30 lmhmf 
 |-  ( x e. ( M LMHom M ) -> x : ( Base ` M ) --> ( Base ` M ) )
32 12 31 syl 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> x : ( Base ` M ) --> ( Base ` M ) )
33 fvex 
 |-  ( Base ` M ) e. _V
34 33 33 elmap 
 |-  ( x e. ( ( Base ` M ) ^m ( Base ` M ) ) <-> x : ( Base ` M ) --> ( Base ` M ) )
35 32 34 sylibr 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> x e. ( ( Base ` M ) ^m ( Base ` M ) ) )
36 30 30 lmhmf 
 |-  ( y e. ( M LMHom M ) -> y : ( Base ` M ) --> ( Base ` M ) )
37 13 36 syl 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> y : ( Base ` M ) --> ( Base ` M ) )
38 33 33 elmap 
 |-  ( y e. ( ( Base ` M ) ^m ( Base ` M ) ) <-> y : ( Base ` M ) --> ( Base ` M ) )
39 37 38 sylibr 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> y e. ( ( Base ` M ) ^m ( Base ` M ) ) )
40 30 30 lmhmf 
 |-  ( z e. ( M LMHom M ) -> z : ( Base ` M ) --> ( Base ` M ) )
41 15 40 syl 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> z : ( Base ` M ) --> ( Base ` M ) )
42 33 33 elmap 
 |-  ( z e. ( ( Base ` M ) ^m ( Base ` M ) ) <-> z : ( Base ` M ) --> ( Base ` M ) )
43 41 42 sylibr 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> z e. ( ( Base ` M ) ^m ( Base ` M ) ) )
44 30 6 mndvass 
 |-  ( ( M e. Mnd /\ ( x e. ( ( Base ` M ) ^m ( Base ` M ) ) /\ y e. ( ( Base ` M ) ^m ( Base ` M ) ) /\ z e. ( ( Base ` M ) ^m ( Base ` M ) ) ) ) -> ( ( x oF ( +g ` M ) y ) oF ( +g ` M ) z ) = ( x oF ( +g ` M ) ( y oF ( +g ` M ) z ) ) )
45 29 35 39 43 44 syl13anc 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( ( x oF ( +g ` M ) y ) oF ( +g ` M ) z ) = ( x oF ( +g ` M ) ( y oF ( +g ` M ) z ) ) )
46 23 26 45 3eqtr4d 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( x ( +g ` A ) ( y ( +g ` A ) z ) ) = ( ( x oF ( +g ` M ) y ) oF ( +g ` M ) z ) )
47 17 19 46 3eqtr4d 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( ( x ( +g ` A ) y ) ( +g ` A ) z ) = ( x ( +g ` A ) ( y ( +g ` A ) z ) ) )
48 id 
 |-  ( M e. LMod -> M e. LMod )
49 eqidd 
 |-  ( M e. LMod -> ( Scalar ` M ) = ( Scalar ` M ) )
50 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
51 eqid 
 |-  ( Scalar ` M ) = ( Scalar ` M )
52 50 30 51 51 0lmhm 
 |-  ( ( M e. LMod /\ M e. LMod /\ ( Scalar ` M ) = ( Scalar ` M ) ) -> ( ( Base ` M ) X. { ( 0g ` M ) } ) e. ( M LMHom M ) )
53 48 48 49 52 syl3anc 
 |-  ( M e. LMod -> ( ( Base ` M ) X. { ( 0g ` M ) } ) e. ( M LMHom M ) )
54 1 2 6 7 mendplusg 
 |-  ( ( ( ( Base ` M ) X. { ( 0g ` M ) } ) e. ( M LMHom M ) /\ x e. ( M LMHom M ) ) -> ( ( ( Base ` M ) X. { ( 0g ` M ) } ) ( +g ` A ) x ) = ( ( ( Base ` M ) X. { ( 0g ` M ) } ) oF ( +g ` M ) x ) )
55 53 54 sylan 
 |-  ( ( M e. LMod /\ x e. ( M LMHom M ) ) -> ( ( ( Base ` M ) X. { ( 0g ` M ) } ) ( +g ` A ) x ) = ( ( ( Base ` M ) X. { ( 0g ` M ) } ) oF ( +g ` M ) x ) )
56 31 34 sylibr 
 |-  ( x e. ( M LMHom M ) -> x e. ( ( Base ` M ) ^m ( Base ` M ) ) )
57 30 6 50 mndvlid 
 |-  ( ( M e. Mnd /\ x e. ( ( Base ` M ) ^m ( Base ` M ) ) ) -> ( ( ( Base ` M ) X. { ( 0g ` M ) } ) oF ( +g ` M ) x ) = x )
58 28 56 57 syl2an 
 |-  ( ( M e. LMod /\ x e. ( M LMHom M ) ) -> ( ( ( Base ` M ) X. { ( 0g ` M ) } ) oF ( +g ` M ) x ) = x )
59 55 58 eqtrd 
 |-  ( ( M e. LMod /\ x e. ( M LMHom M ) ) -> ( ( ( Base ` M ) X. { ( 0g ` M ) } ) ( +g ` A ) x ) = x )
60 eqid 
 |-  ( invg ` M ) = ( invg ` M )
61 60 invlmhm 
 |-  ( M e. LMod -> ( invg ` M ) e. ( M LMHom M ) )
62 lmhmco 
 |-  ( ( ( invg ` M ) e. ( M LMHom M ) /\ x e. ( M LMHom M ) ) -> ( ( invg ` M ) o. x ) e. ( M LMHom M ) )
63 61 62 sylan 
 |-  ( ( M e. LMod /\ x e. ( M LMHom M ) ) -> ( ( invg ` M ) o. x ) e. ( M LMHom M ) )
64 1 2 6 7 mendplusg 
 |-  ( ( ( ( invg ` M ) o. x ) e. ( M LMHom M ) /\ x e. ( M LMHom M ) ) -> ( ( ( invg ` M ) o. x ) ( +g ` A ) x ) = ( ( ( invg ` M ) o. x ) oF ( +g ` M ) x ) )
65 63 64 sylancom 
 |-  ( ( M e. LMod /\ x e. ( M LMHom M ) ) -> ( ( ( invg ` M ) o. x ) ( +g ` A ) x ) = ( ( ( invg ` M ) o. x ) oF ( +g ` M ) x ) )
66 30 6 60 50 grpvlinv 
 |-  ( ( M e. Grp /\ x e. ( ( Base ` M ) ^m ( Base ` M ) ) ) -> ( ( ( invg ` M ) o. x ) oF ( +g ` M ) x ) = ( ( Base ` M ) X. { ( 0g ` M ) } ) )
67 27 56 66 syl2an 
 |-  ( ( M e. LMod /\ x e. ( M LMHom M ) ) -> ( ( ( invg ` M ) o. x ) oF ( +g ` M ) x ) = ( ( Base ` M ) X. { ( 0g ` M ) } ) )
68 65 67 eqtrd 
 |-  ( ( M e. LMod /\ x e. ( M LMHom M ) ) -> ( ( ( invg ` M ) o. x ) ( +g ` A ) x ) = ( ( Base ` M ) X. { ( 0g ` M ) } ) )
69 3 4 11 47 53 59 63 68 isgrpd 
 |-  ( M e. LMod -> A e. Grp )
70 eqid 
 |-  ( .r ` A ) = ( .r ` A )
71 1 2 70 mendmulr 
 |-  ( ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) ) -> ( x ( .r ` A ) y ) = ( x o. y ) )
72 lmhmco 
 |-  ( ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) ) -> ( x o. y ) e. ( M LMHom M ) )
73 71 72 eqeltrd 
 |-  ( ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) ) -> ( x ( .r ` A ) y ) e. ( M LMHom M ) )
74 73 3adant1 
 |-  ( ( M e. LMod /\ x e. ( M LMHom M ) /\ y e. ( M LMHom M ) ) -> ( x ( .r ` A ) y ) e. ( M LMHom M ) )
75 coass 
 |-  ( ( x o. y ) o. z ) = ( x o. ( y o. z ) )
76 12 13 71 syl2anc 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( x ( .r ` A ) y ) = ( x o. y ) )
77 76 oveq1d 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( ( x ( .r ` A ) y ) ( .r ` A ) z ) = ( ( x o. y ) ( .r ` A ) z ) )
78 12 13 72 syl2anc 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( x o. y ) e. ( M LMHom M ) )
79 1 2 70 mendmulr 
 |-  ( ( ( x o. y ) e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) -> ( ( x o. y ) ( .r ` A ) z ) = ( ( x o. y ) o. z ) )
80 78 15 79 syl2anc 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( ( x o. y ) ( .r ` A ) z ) = ( ( x o. y ) o. z ) )
81 77 80 eqtrd 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( ( x ( .r ` A ) y ) ( .r ` A ) z ) = ( ( x o. y ) o. z ) )
82 1 2 70 mendmulr 
 |-  ( ( y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) -> ( y ( .r ` A ) z ) = ( y o. z ) )
83 13 15 82 syl2anc 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( y ( .r ` A ) z ) = ( y o. z ) )
84 83 oveq2d 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( x ( .r ` A ) ( y ( .r ` A ) z ) ) = ( x ( .r ` A ) ( y o. z ) ) )
85 lmhmco 
 |-  ( ( y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) -> ( y o. z ) e. ( M LMHom M ) )
86 13 15 85 syl2anc 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( y o. z ) e. ( M LMHom M ) )
87 1 2 70 mendmulr 
 |-  ( ( x e. ( M LMHom M ) /\ ( y o. z ) e. ( M LMHom M ) ) -> ( x ( .r ` A ) ( y o. z ) ) = ( x o. ( y o. z ) ) )
88 12 86 87 syl2anc 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( x ( .r ` A ) ( y o. z ) ) = ( x o. ( y o. z ) ) )
89 84 88 eqtrd 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( x ( .r ` A ) ( y ( .r ` A ) z ) ) = ( x o. ( y o. z ) ) )
90 75 81 89 3eqtr4a 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( ( x ( .r ` A ) y ) ( .r ` A ) z ) = ( x ( .r ` A ) ( y ( .r ` A ) z ) ) )
91 1 2 70 mendmulr 
 |-  ( ( x e. ( M LMHom M ) /\ ( y oF ( +g ` M ) z ) e. ( M LMHom M ) ) -> ( x ( .r ` A ) ( y oF ( +g ` M ) z ) ) = ( x o. ( y oF ( +g ` M ) z ) ) )
92 12 21 91 syl2anc 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( x ( .r ` A ) ( y oF ( +g ` M ) z ) ) = ( x o. ( y oF ( +g ` M ) z ) ) )
93 25 oveq2d 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( x ( .r ` A ) ( y ( +g ` A ) z ) ) = ( x ( .r ` A ) ( y oF ( +g ` M ) z ) ) )
94 lmhmco 
 |-  ( ( x e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) -> ( x o. z ) e. ( M LMHom M ) )
95 12 15 94 syl2anc 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( x o. z ) e. ( M LMHom M ) )
96 1 2 6 7 mendplusg 
 |-  ( ( ( x o. y ) e. ( M LMHom M ) /\ ( x o. z ) e. ( M LMHom M ) ) -> ( ( x o. y ) ( +g ` A ) ( x o. z ) ) = ( ( x o. y ) oF ( +g ` M ) ( x o. z ) ) )
97 78 95 96 syl2anc 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( ( x o. y ) ( +g ` A ) ( x o. z ) ) = ( ( x o. y ) oF ( +g ` M ) ( x o. z ) ) )
98 1 2 70 mendmulr 
 |-  ( ( x e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) -> ( x ( .r ` A ) z ) = ( x o. z ) )
99 12 15 98 syl2anc 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( x ( .r ` A ) z ) = ( x o. z ) )
100 76 99 oveq12d 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( ( x ( .r ` A ) y ) ( +g ` A ) ( x ( .r ` A ) z ) ) = ( ( x o. y ) ( +g ` A ) ( x o. z ) ) )
101 lmghm 
 |-  ( x e. ( M LMHom M ) -> x e. ( M GrpHom M ) )
102 ghmmhm 
 |-  ( x e. ( M GrpHom M ) -> x e. ( M MndHom M ) )
103 12 101 102 3syl 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> x e. ( M MndHom M ) )
104 30 6 6 mhmvlin 
 |-  ( ( x e. ( M MndHom M ) /\ y e. ( ( Base ` M ) ^m ( Base ` M ) ) /\ z e. ( ( Base ` M ) ^m ( Base ` M ) ) ) -> ( x o. ( y oF ( +g ` M ) z ) ) = ( ( x o. y ) oF ( +g ` M ) ( x o. z ) ) )
105 103 39 43 104 syl3anc 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( x o. ( y oF ( +g ` M ) z ) ) = ( ( x o. y ) oF ( +g ` M ) ( x o. z ) ) )
106 97 100 105 3eqtr4d 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( ( x ( .r ` A ) y ) ( +g ` A ) ( x ( .r ` A ) z ) ) = ( x o. ( y oF ( +g ` M ) z ) ) )
107 92 93 106 3eqtr4d 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( x ( .r ` A ) ( y ( +g ` A ) z ) ) = ( ( x ( .r ` A ) y ) ( +g ` A ) ( x ( .r ` A ) z ) ) )
108 1 2 70 mendmulr 
 |-  ( ( ( x oF ( +g ` M ) y ) e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) -> ( ( x oF ( +g ` M ) y ) ( .r ` A ) z ) = ( ( x oF ( +g ` M ) y ) o. z ) )
109 14 15 108 syl2anc 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( ( x oF ( +g ` M ) y ) ( .r ` A ) z ) = ( ( x oF ( +g ` M ) y ) o. z ) )
110 18 oveq1d 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( ( x ( +g ` A ) y ) ( .r ` A ) z ) = ( ( x oF ( +g ` M ) y ) ( .r ` A ) z ) )
111 1 2 6 7 mendplusg 
 |-  ( ( ( x o. z ) e. ( M LMHom M ) /\ ( y o. z ) e. ( M LMHom M ) ) -> ( ( x o. z ) ( +g ` A ) ( y o. z ) ) = ( ( x o. z ) oF ( +g ` M ) ( y o. z ) ) )
112 95 86 111 syl2anc 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( ( x o. z ) ( +g ` A ) ( y o. z ) ) = ( ( x o. z ) oF ( +g ` M ) ( y o. z ) ) )
113 99 83 oveq12d 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( ( x ( .r ` A ) z ) ( +g ` A ) ( y ( .r ` A ) z ) ) = ( ( x o. z ) ( +g ` A ) ( y o. z ) ) )
114 ffn 
 |-  ( x : ( Base ` M ) --> ( Base ` M ) -> x Fn ( Base ` M ) )
115 12 31 114 3syl 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> x Fn ( Base ` M ) )
116 ffn 
 |-  ( y : ( Base ` M ) --> ( Base ` M ) -> y Fn ( Base ` M ) )
117 13 36 116 3syl 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> y Fn ( Base ` M ) )
118 33 a1i 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( Base ` M ) e. _V )
119 inidm 
 |-  ( ( Base ` M ) i^i ( Base ` M ) ) = ( Base ` M )
120 115 117 41 118 118 118 119 ofco 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( ( x oF ( +g ` M ) y ) o. z ) = ( ( x o. z ) oF ( +g ` M ) ( y o. z ) ) )
121 112 113 120 3eqtr4d 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( ( x ( .r ` A ) z ) ( +g ` A ) ( y ( .r ` A ) z ) ) = ( ( x oF ( +g ` M ) y ) o. z ) )
122 109 110 121 3eqtr4d 
 |-  ( ( M e. LMod /\ ( x e. ( M LMHom M ) /\ y e. ( M LMHom M ) /\ z e. ( M LMHom M ) ) ) -> ( ( x ( +g ` A ) y ) ( .r ` A ) z ) = ( ( x ( .r ` A ) z ) ( +g ` A ) ( y ( .r ` A ) z ) ) )
123 30 idlmhm 
 |-  ( M e. LMod -> ( _I |` ( Base ` M ) ) e. ( M LMHom M ) )
124 1 2 70 mendmulr 
 |-  ( ( ( _I |` ( Base ` M ) ) e. ( M LMHom M ) /\ x e. ( M LMHom M ) ) -> ( ( _I |` ( Base ` M ) ) ( .r ` A ) x ) = ( ( _I |` ( Base ` M ) ) o. x ) )
125 123 124 sylan 
 |-  ( ( M e. LMod /\ x e. ( M LMHom M ) ) -> ( ( _I |` ( Base ` M ) ) ( .r ` A ) x ) = ( ( _I |` ( Base ` M ) ) o. x ) )
126 31 adantl 
 |-  ( ( M e. LMod /\ x e. ( M LMHom M ) ) -> x : ( Base ` M ) --> ( Base ` M ) )
127 fcoi2 
 |-  ( x : ( Base ` M ) --> ( Base ` M ) -> ( ( _I |` ( Base ` M ) ) o. x ) = x )
128 126 127 syl 
 |-  ( ( M e. LMod /\ x e. ( M LMHom M ) ) -> ( ( _I |` ( Base ` M ) ) o. x ) = x )
129 125 128 eqtrd 
 |-  ( ( M e. LMod /\ x e. ( M LMHom M ) ) -> ( ( _I |` ( Base ` M ) ) ( .r ` A ) x ) = x )
130 id 
 |-  ( x e. ( M LMHom M ) -> x e. ( M LMHom M ) )
131 1 2 70 mendmulr 
 |-  ( ( x e. ( M LMHom M ) /\ ( _I |` ( Base ` M ) ) e. ( M LMHom M ) ) -> ( x ( .r ` A ) ( _I |` ( Base ` M ) ) ) = ( x o. ( _I |` ( Base ` M ) ) ) )
132 130 123 131 syl2anr 
 |-  ( ( M e. LMod /\ x e. ( M LMHom M ) ) -> ( x ( .r ` A ) ( _I |` ( Base ` M ) ) ) = ( x o. ( _I |` ( Base ` M ) ) ) )
133 fcoi1 
 |-  ( x : ( Base ` M ) --> ( Base ` M ) -> ( x o. ( _I |` ( Base ` M ) ) ) = x )
134 126 133 syl 
 |-  ( ( M e. LMod /\ x e. ( M LMHom M ) ) -> ( x o. ( _I |` ( Base ` M ) ) ) = x )
135 132 134 eqtrd 
 |-  ( ( M e. LMod /\ x e. ( M LMHom M ) ) -> ( x ( .r ` A ) ( _I |` ( Base ` M ) ) ) = x )
136 3 4 5 69 74 90 107 122 123 129 135 isringd 
 |-  ( M e. LMod -> A e. Ring )