let R be Ring; :: thesis: for I being Ideal of R
for a, b being Element of R
for x, y being Element of (R / I) st x = Class (EqRel R,I),a & y = Class (EqRel R,I),b holds
x * y = Class (EqRel R,I),(a * b)
let I be Ideal of R; :: thesis: for a, b being Element of R
for x, y being Element of (R / I) st x = Class (EqRel R,I),a & y = Class (EqRel R,I),b holds
x * y = Class (EqRel R,I),(a * b)
let a, b be Element of R; :: thesis: for x, y being Element of (R / I) st x = Class (EqRel R,I),a & y = Class (EqRel R,I),b holds
x * y = Class (EqRel R,I),(a * b)
let x, y be Element of (R / I); :: thesis: ( x = Class (EqRel R,I),a & y = Class (EqRel R,I),b implies x * y = Class (EqRel R,I),(a * b) )
assume A1: ( x = Class (EqRel R,I),a & y = Class (EqRel R,I),b ) ; :: thesis: x * y = Class (EqRel R,I),(a * b)
consider a1, b1 being Element of R such that
A2: ( x = Class (EqRel R,I),a1 & y = Class (EqRel R,I),b1 ) and
A3: the multF of (R / I) . x,y = Class (EqRel R,I),(a1 * b1) by Def6;
( a1 - a in I & b1 - b in I ) by A1, A2, Th6;
then ( (a1 - a) * b in I & a1 * (b1 - b) in I ) by IDEAL_1:def 2, IDEAL_1:def 3;
then A4: ((a1 - a) * b) + (a1 * (b1 - b)) in I by IDEAL_1:def 1;
( (a1 - a) * b = (a1 * b) - (a * b) & a1 * (b1 - b) = (a1 * b1) - (a1 * b) ) by VECTSP_1:43, VECTSP_1:45;
then (a1 * (b1 - b)) + ((a1 - a) * b) = (((a1 * b1) - (a1 * b)) + (a1 * b)) - (a * b) by RLVECT_1:42
.= (a1 * b1) - (a * b) by Th1 ;
hence x * y = Class (EqRel R,I),(a * b) by A3, A4, Th6; :: thesis: verum