let R be Ring; :: thesis: for M being AbGroup
for s being Function of R,(End_Ring M)
for a, b being Element of R
for x being Element of (AbGrLMod (M,s)) st s is RingHomomorphism holds
(a + b) * x = (a * x) + (b * x)
let M be AbGroup; :: thesis: for s being Function of R,(End_Ring M)
for a, b being Element of R
for x being Element of (AbGrLMod (M,s)) st s is RingHomomorphism holds
(a + b) * x = (a * x) + (b * x)
let s be Function of R,(End_Ring M); :: thesis: for a, b being Element of R
for x being Element of (AbGrLMod (M,s)) st s is RingHomomorphism holds
(a + b) * x = (a * x) + (b * x)
let a, b be Element of R; :: thesis: for x being Element of (AbGrLMod (M,s)) st s is RingHomomorphism holds
(a + b) * x = (a * x) + (b * x)
let x be Element of (AbGrLMod (M,s)); :: thesis: ( s is RingHomomorphism implies (a + b) * x = (a * x) + (b * x) )
assume A1: s is RingHomomorphism ; :: thesis: (a + b) * x = (a * x) + (b * x)
consider h being Endomorphism of M such that
A2: ( h = s . (a + b) & (a + b) * x = h . x ) by Def12;
s . a in set_End M ;
then consider ha being Function of the carrier of M, the carrier of M such that
A3: ( ha = s . a & ha is Endomorphism of M ) ;
s . b in set_End M ;
then consider hb being Function of the carrier of M, the carrier of M such that
A4: ( hb = s . b & hb is Endomorphism of M ) ;
consider h1 being Endomorphism of M such that
A5: ( h1 = s . a & a * x = h1 . x ) by Def12;
consider h2 being Endomorphism of M such that
A6: ( h2 = s . b & b * x = h2 . x ) by Def12;
reconsider x1 = x as Element of the carrier of M ;
A7: h = (s . a) + (s . b) by A2, VECTSP_1:def 20, A1
.= (ADD (M,M)) . (ha,hb) by A3, A4, Th3 ;
reconsider h = h, ha = ha, hb = hb as Element of Funcs ( the carrier of M, the carrier of M) by FUNCT_2:9;
(a + b) * x = h . x by A2
.= (ha . x1) + (hb . x1) by A7, Th1
.= (a * x) + (b * x) by A3, A5, A4, A6 ;
hence (a + b) * x = (a * x) + (b * x) ; :: thesis: verum