let R be non trivial right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for I being non empty add-closed 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 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 ) ;
then A1: (a - b) + (c - d) in I by IDEAL_1:def 1;
(a + c) - (b + d) = (a + c) + (- (b + d))
.= (a + c) + ((- d) + (- b)) by RLVECT_1:31
.= a + (c + ((- d) + (- b))) by RLVECT_1:def 3
.= a + ((c + (- d)) + (- b)) by RLVECT_1:def 3
.= (a + (- b)) + (c + (- d)) by RLVECT_1:def 3
.= (a - b) + (c + (- d))
.= (a - b) + (c - d) ;
hence a + c,b + d are_congruent_mod I by A1; :: thesis: verum