let R be non empty right_complementable commutative distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for I being non empty add-closed right-ideal Subset of R
for a, b, c, d being Element of R st a,b are_congruent_mod I & c,d are_congruent_mod I holds
a * c,b * d are_congruent_mod I
let I be non empty add-closed right-ideal Subset of R; :: thesis: for a, b, c, d being Element of R st a,b are_congruent_mod I & c,d are_congruent_mod I holds
a * c,b * d are_congruent_mod I
let a, b, c, d be Element of R; :: thesis: ( a,b are_congruent_mod I & c,d are_congruent_mod I implies a * c,b * d are_congruent_mod I )
assume ( a,b are_congruent_mod I & c,d are_congruent_mod I ) ; :: thesis: a * c,b * d are_congruent_mod I
then ( a - b in I & c - d in I ) by Def14;
then ( (a - b) * c in I & (c - d) * b in I ) by IDEAL_1:def 3;
then A1: ((a - b) * c) + ((c - d) * b) in I by IDEAL_1:def 1;
A2: (a - b) * c = (a + (- b)) * c by RLVECT_1:def 12
.= (a * c) + ((- b) * c) by VECTSP_1:def 12 ;
(c - d) * b = (c + (- d)) * b by RLVECT_1:def 12
.= (c * b) + ((- d) * b) by VECTSP_1:def 12 ;
then ((a - b) * c) + ((c - d) * b) = (a * c) + (((- b) * c) + ((c * b) + ((- d) * b))) by A2, RLVECT_1:def 6
.= (a * c) + ((((- b) * c) + (c * b)) + ((- d) * b)) by RLVECT_1:def 6
.= (a * c) + (((- (b * c)) + (c * b)) + ((- d) * b)) by VECTSP_1:41
.= (a * c) + ((0. R) + ((- d) * b)) by RLVECT_1:16
.= (a * c) + ((- d) * b) by ALGSTR_1:def 5
.= (a * c) + (- (d * b)) by VECTSP_1:41
.= (a * c) - (b * d) by RLVECT_1:def 12 ;
hence a * c,b * d are_congruent_mod I by A1, Def14; :: thesis: verum