let R be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; for a, b being Element of R
for i being Element of INT.Ring holds (Int-mult-left R) . (i,(a + b)) = ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (i,b))
let a, b be Element of R; for i being Element of INT.Ring holds (Int-mult-left R) . (i,(a + b)) = ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (i,b))
let i be Element of INT.Ring; (Int-mult-left R) . (i,(a + b)) = ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (i,b))
reconsider ii = i as Element of INT ;
per cases
( 0 <= i or 0 > i )
;
suppose A1:
0 > i
;
(Int-mult-left R) . (i,(a + b)) = ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (i,b))then reconsider i1 =
- ii as
Element of
NAT by INT_1:3;
(a + b) + ((- a) + (- b)) =
((b + a) + (- a)) + (- b)
by RLVECT_1:def 3
.=
(b + (a + (- a))) + (- b)
by RLVECT_1:def 3
.=
(b + (0. R)) + (- b)
by RLVECT_1:5
.=
b + (- b)
by RLVECT_1:4
.=
0. R
by RLVECT_1:5
;
then A2:
- (a + b) = (- a) + (- b)
by RLVECT_1:6;
S1:
i1 * (- a) =
(Nat-mult-left R) . (
(- i),
(- a))
.=
(Int-mult-left R) . (
i,
a)
by A1, Def23
;
S2:
i1 * (- b) = (Nat-mult-left R) . (
(- i),
(- b))
;
thus (Int-mult-left R) . (
i,
(a + b)) =
(Nat-mult-left R) . (
(- i),
(- (a + b)))
by Def23, A1
.=
(i1 * (- a)) + (i1 * (- b))
by A2, Th160
.=
((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (i,b))
by A1, Def23, S1, S2
;
verum end; end;