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 that
A1: a,b are_congruent_mod I and
A2: c,d are_congruent_mod I ; :: thesis: a * c,b * d are_congruent_mod I
c - d in I by A2, Def14;
then A3: (c - d) * b in I by IDEAL_1:def 3;
A4: (c - d) * b = (c + (- d)) * b by RLVECT_1:def 14
.= (c * b) + ((- d) * b) by VECTSP_1:def 12 ;
(a - b) * c = (a + (- b)) * c by RLVECT_1:def 14
.= (a * c) + ((- b) * c) by VECTSP_1:def 12 ;
then A5: ((a - b) * c) + ((c - d) * b) = (a * c) + (((- b) * c) + ((c * b) + ((- d) * b))) by A4, 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 14 ;
a - b in I by A1, Def14;
then (a - b) * c in I by IDEAL_1:def 3;
then ((a - b) * c) + ((c - d) * b) in I by A3, IDEAL_1:def 1;
hence a * c,b * d are_congruent_mod I by A5, Def14; :: thesis: verum