let R be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for a being Element of R
for i, j being Element of INT.Ring st i in NAT & not j in NAT holds
(Int-mult-left R) . ((i + j),a) = ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (j,a))
let a be Element of R; :: thesis: for i, j being Element of INT.Ring st i in NAT & not j in NAT holds
(Int-mult-left R) . ((i + j),a) = ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (j,a))
let i, j be Element of INT.Ring; :: thesis: ( i in NAT & not j in NAT implies (Int-mult-left R) . ((i + j),a) = ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (j,a)) )
reconsider jj = j, ii = i, ij = i + j as Element of INT ;
assume A1: ( i in NAT & not j in NAT ) ; :: thesis: (Int-mult-left R) . ((i + j),a) = ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (j,a))
then reconsider i1 = i as Element of NAT ;
A2: jj < 0 by A1, INT_1:3;
then reconsider j1 = - jj as Element of NAT by INT_1:3;
per cases ( j1 <= i1 or j1 > i1 ) ;
suppose A4: j1 <= i1 ; :: thesis: (Int-mult-left R) . ((i + j),a) = ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (j,a))
reconsider k1 = i1 - j1 as Element of NAT by A4, INT_1:5;
set IT = Int-mult-left R;
W1: (Int-mult-left R) . (jj,a) = (Nat-mult-left R) . ((- j),(- a)) by A2, Def23;
thus (Int-mult-left R) . ((i + j),a) = (Nat-mult-left R) . (k1,a) by Def23
.= ((Nat-mult-left R) . (i1,a)) - ((Nat-mult-left R) . (j1,a)) by Th156, A4
.= ((Nat-mult-left R) . (i1,a)) + ((Nat-mult-left R) . (j1,(- a))) by Th157
.= ((Int-mult-left R) . (i,a)) + ((Nat-mult-left R) . (j1,(- a))) by Def23
.= ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (j,a)) by W1 ; :: thesis: verum
end;
suppose A5: j1 > i1 ; :: thesis: (Int-mult-left R) . ((i + j),a) = ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (j,a))
then reconsider k1 = j1 - i1 as Element of NAT by INT_1:5;
A6: i1 - j1 < 0 by A5, XREAL_1:49;
Z1: (Int-mult-left R) . (j,a) = (Nat-mult-left R) . ((- j),(- a)) by Def23, A2;
thus (Int-mult-left R) . ((i + j),a) = (Nat-mult-left R) . ((- (i + j)),(- a)) by A6, Def23
.= (Nat-mult-left R) . (k1,(- a))
.= ((Nat-mult-left R) . (j1,(- a))) - ((Nat-mult-left R) . (i1,(- a))) by Th156, A5
.= ((Nat-mult-left R) . (j1,(- a))) + ((Nat-mult-left R) . (i1,(- (- a)))) by Th157
.= ((Nat-mult-left R) . (j1,(- a))) + ((Nat-mult-left R) . (i1,a)) by RLVECT_1:17
.= ((Int-mult-left R) . (j,a)) + ((Int-mult-left R) . (i,a)) by Def23, Z1
.= ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (j,a)) ; :: thesis: verum
end;
end;