let R be non empty right_complementable distributive add-associative right_zeroed commutative doubleLoopStr ; 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; 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; ( 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
; a * c,b * d are_congruent_mod I
c - d in I
by A2;
then A3:
(c - d) * b in I
by IDEAL_1:def 3;
A4: (c - d) * b =
(c + (- d)) * b
.=
(c * b) + ((- d) * b)
by VECTSP_1:def 3
;
(a - b) * c =
(a + (- b)) * c
.=
(a * c) + ((- b) * c)
by VECTSP_1:def 3
;
then A5: ((a - b) * c) + ((c - d) * b) =
(a * c) + (((- b) * c) + ((c * b) + ((- d) * b)))
by A4, RLVECT_1:def 3
.=
(a * c) + ((((- b) * c) + (c * b)) + ((- d) * b))
by RLVECT_1:def 3
.=
(a * c) + (((- (b * c)) + (c * b)) + ((- d) * b))
by VECTSP_1:9
.=
(a * c) + ((0. R) + ((- d) * b))
by RLVECT_1:5
.=
(a * c) + ((- d) * b)
by ALGSTR_1:def 2
.=
(a * c) + (- (d * b))
by VECTSP_1:9
.=
(a * c) - (b * d)
;
a - b in I
by A1;
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; verum