set g = the addF of (R / I);
set E = EqRel (R,I);
hereby RLVECT_1:def 2 ( R / I is add-associative & R / I is right_zeroed & R / I is right_complementable & R / I is associative & R / I is well-unital & R / I is distributive )
let x,
y be
Element of
(R / I);
x + y = y + xconsider a being
Element of
R such that A1:
x = Class (
(EqRel (R,I)),
a)
by Th11;
consider b being
Element of
R such that A2:
y = Class (
(EqRel (R,I)),
b)
by Th11;
thus x + y =
Class (
(EqRel (R,I)),
(a + b))
by A1, A2, Th13
.=
y + x
by A1, A2, Th13
;
verum
end;
hereby RLVECT_1:def 3 ( R / I is right_zeroed & R / I is right_complementable & R / I is associative & R / I is well-unital & R / I is distributive )
let x,
y,
z be
Element of
(R / I);
(x + y) + z = x + (y + z)consider a being
Element of
R such that A3:
x = Class (
(EqRel (R,I)),
a)
by Th11;
consider b being
Element of
R such that A4:
y = Class (
(EqRel (R,I)),
b)
by Th11;
consider bc being
Element of
R such that A5:
y + z = Class (
(EqRel (R,I)),
bc)
by Th11;
consider c being
Element of
R such that A6:
z = Class (
(EqRel (R,I)),
c)
by Th11;
y + z = Class (
(EqRel (R,I)),
(b + c))
by A4, A6, Th13;
then A7:
bc - (b + c) in I
by A5, Th6;
consider ab being
Element of
R such that A8:
x + y = Class (
(EqRel (R,I)),
ab)
by Th11;
x + y = Class (
(EqRel (R,I)),
(a + b))
by A3, A4, Th13;
then
ab - (a + b) in I
by A8, Th6;
then A9:
(ab - (a + b)) - (bc - (b + c)) in I
by A7, IDEAL_1:15;
A10:
(ab - (a + b)) - (bc - (b + c)) =
((ab - (a + b)) - bc) + (b + c)
by RLVECT_1:29
.=
((ab - (a + b)) + (b + c)) - bc
by RLVECT_1:28
.=
(((ab - a) - b) + (b + c)) - bc
by RLVECT_1:27
.=
((((ab - a) - b) + b) + c) - bc
by RLVECT_1:def 3
.=
((ab - a) + c) - bc
by Th1
.=
((ab + c) - a) - bc
by RLVECT_1:28
.=
(ab + c) - (a + bc)
by RLVECT_1:27
;
thus (x + y) + z =
Class (
(EqRel (R,I)),
(ab + c))
by A6, A8, Th13
.=
Class (
(EqRel (R,I)),
(a + bc))
by A9, A10, Th6
.=
x + (y + z)
by A3, A5, Th13
;
verum
end;
hereby RLVECT_1:def 4 ( R / I is right_complementable & R / I is associative & R / I is well-unital & R / I is distributive )
let v be
Element of
(R / I);
v + (0. (R / I)) = vconsider a,
b being
Element of
R such that A11:
v = Class (
(EqRel (R,I)),
a)
and A12:
0. (R / I) = Class (
(EqRel (R,I)),
b)
and A13:
the
addF of
(R / I) . (
v,
(0. (R / I)))
= Class (
(EqRel (R,I)),
(a + b))
by Def6;
A14:
b - (0. R) = b
by RLVECT_1:13;
A15:
(a + b) - a =
(a - a) + b
by RLVECT_1:28
.=
(0. R) + b
by RLVECT_1:15
.=
b
by RLVECT_1:def 4
;
0. (R / I) = Class (
(EqRel (R,I)),
(0. R))
by Def6;
then
b - (0. R) in I
by A12, Th6;
hence
v + (0. (R / I)) = v
by A11, A13, A14, A15, Th6;
verum
end;
thus
R / I is right_complementable
( R / I is associative & R / I is well-unital & R / I is distributive )proof
let v be
Element of
(R / I);
ALGSTR_0:def 16 v is right_complementable
consider a,
b being
Element of
R such that A16:
v = Class (
(EqRel (R,I)),
a)
and
0. (R / I) = Class (
(EqRel (R,I)),
b)
and
the
addF of
(R / I) . (
v,
(0. (R / I)))
= Class (
(EqRel (R,I)),
(a + b))
by Def6;
reconsider w =
Class (
(EqRel (R,I)),
(- a)) as
Element of
(R / I) by Th12;
take
w
;
ALGSTR_0:def 11 v + w = 0. (R / I)
A17:
0. (R / I) = Class (
(EqRel (R,I)),
(0. R))
by Def6;
thus v + w =
Class (
(EqRel (R,I)),
(a + (- a)))
by A16, Th13
.=
0. (R / I)
by A17, RLVECT_1:def 10
;
verum
end;
hereby GROUP_1:def 3 ( R / I is well-unital & R / I is distributive )
let x,
y,
z be
Element of
(R / I);
(x * y) * z = x * (y * z)consider a being
Element of
R such that A18:
x = Class (
(EqRel (R,I)),
a)
by Th11;
consider ab being
Element of
R such that A19:
x * y = Class (
(EqRel (R,I)),
ab)
by Th11;
consider c being
Element of
R such that A20:
z = Class (
(EqRel (R,I)),
c)
by Th11;
consider b being
Element of
R such that A21:
y = Class (
(EqRel (R,I)),
b)
by Th11;
x * y = Class (
(EqRel (R,I)),
(a * b))
by A18, A21, Th14;
then
ab - (a * b) in I
by A19, Th6;
then A22:
(ab - (a * b)) * c in I
by IDEAL_1:def 3;
consider bc being
Element of
R such that A23:
y * z = Class (
(EqRel (R,I)),
bc)
by Th11;
y * z = Class (
(EqRel (R,I)),
(b * c))
by A21, A20, Th14;
then
bc - (b * c) in I
by A23, Th6;
then A24:
a * (bc - (b * c)) in I
by IDEAL_1:def 2;
A25:
(
(ab - (a * b)) * c = (ab * c) - ((a * b) * c) &
a * (bc - (b * c)) = (a * bc) - (a * (b * c)) )
by VECTSP_1:11, VECTSP_1:13;
(
a * (b * c) = (a * b) * c &
((ab * c) - ((a * b) * c)) - ((a * bc) - ((a * b) * c)) = (ab * c) - (a * bc) )
by Th3, GROUP_1:def 3;
then A26:
(ab * c) - (a * bc) in I
by A22, A24, A25, IDEAL_1:15;
thus (x * y) * z =
Class (
(EqRel (R,I)),
(ab * c))
by A20, A19, Th14
.=
Class (
(EqRel (R,I)),
(a * bc))
by A26, Th6
.=
x * (y * z)
by A18, A23, Th14
;
verum
end;
( 1. R = 1_ R & Class ((EqRel (R,I)),(1. R)) = 1. (R / I) )
by Def6;
hence
for x being Element of (R / I) holds
( x * (1. (R / I)) = x & (1. (R / I)) * x = x )
by Lm2; VECTSP_1:def 6 R / I is distributive
let x, y, z be Element of (R / I); VECTSP_1:def 7 ( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
consider a being Element of R such that
A27:
x = Class ((EqRel (R,I)),a)
by Th11;
consider ab being Element of R such that
A28:
x * y = Class ((EqRel (R,I)),ab)
by Th11;
consider ca being Element of R such that
A29:
z * x = Class ((EqRel (R,I)),ca)
by Th11;
consider c being Element of R such that
A30:
z = Class ((EqRel (R,I)),c)
by Th11;
z * x = Class ((EqRel (R,I)),(c * a))
by A27, A30, Th14;
then A31:
(c * a) - ca in I
by A29, Th6;
consider b being Element of R such that
A32:
y = Class ((EqRel (R,I)),b)
by Th11;
x * y = Class ((EqRel (R,I)),(a * b))
by A27, A32, Th14;
then A33:
ab - (a * b) in I
by A28, Th6;
consider ac being Element of R such that
A34:
x * z = Class ((EqRel (R,I)),ac)
by Th11;
x * z = Class ((EqRel (R,I)),(a * c))
by A27, A30, Th14;
then A35:
ac - (a * c) in I
by A34, Th6;
consider bc being Element of R such that
A36:
y + z = Class ((EqRel (R,I)),bc)
by Th11;
y + z = Class ((EqRel (R,I)),(b + c))
by A32, A30, Th13;
then A37:
bc - (b + c) in I
by A36, Th6;
then A38:
(bc - (b + c)) * a in I
by IDEAL_1:def 3;
a * (bc - (b + c)) in I
by A37, IDEAL_1:def 2;
then
(a * (bc - (b + c))) - (ab - (a * b)) in I
by A33, IDEAL_1:15;
then A39:
((a * (bc - (b + c))) - (ab - (a * b))) - (ac - (a * c)) in I
by A35, IDEAL_1:15;
A40: ((a * (bc - (b + c))) - (ab - (a * b))) - (ac - (a * c)) =
(((a * bc) - (a * (b + c))) - (ab - (a * b))) - (ac - (a * c))
by VECTSP_1:11
.=
(((a * bc) - ((a * b) + (a * c))) - (ab - (a * b))) - (ac - (a * c))
by VECTSP_1:def 2
.=
((((a * bc) - (a * b)) - (a * c)) - (ab - (a * b))) - (ac - (a * c))
by RLVECT_1:27
.=
(((((a * bc) - (a * b)) - (a * c)) - ab) + (a * b)) - (ac - (a * c))
by RLVECT_1:29
.=
((((((a * bc) - (a * b)) - (a * c)) - ab) + (a * b)) - ac) + (a * c)
by RLVECT_1:29
.=
((((((a * bc) - (a * b)) - (a * c)) + (a * b)) - ab) - ac) + (a * c)
by RLVECT_1:28
.=
((((((a * bc) - (a * b)) + (a * b)) - (a * c)) - ab) - ac) + (a * c)
by RLVECT_1:28
.=
((((a * bc) - (a * c)) - ab) - ac) + (a * c)
by Th1
.=
((((a * bc) - (a * c)) - ab) + (a * c)) - ac
by RLVECT_1:28
.=
((((a * bc) - (a * c)) + (a * c)) - ab) - ac
by RLVECT_1:28
.=
((a * bc) - ab) - ac
by Th1
.=
(a * bc) - (ab + ac)
by RLVECT_1:27
;
thus x * (y + z) =
Class ((EqRel (R,I)),(a * bc))
by A27, A36, Th14
.=
Class ((EqRel (R,I)),(ab + ac))
by A39, A40, Th6
.=
(x * y) + (x * z)
by A28, A34, Th13
; (y + z) * x = (y * x) + (z * x)
consider ba being Element of R such that
A41:
y * x = Class ((EqRel (R,I)),ba)
by Th11;
y * x = Class ((EqRel (R,I)),(b * a))
by A27, A32, Th14;
then
(b * a) - ba in I
by A41, Th6;
then
((bc - (b + c)) * a) + ((b * a) - ba) in I
by A38, IDEAL_1:def 1;
then A42:
(((bc - (b + c)) * a) + ((b * a) - ba)) + ((c * a) - ca) in I
by A31, IDEAL_1:def 1;
A43: (((bc - (b + c)) * a) + ((b * a) - ba)) + ((c * a) - ca) =
(((bc * a) - ((b + c) * a)) + ((b * a) - ba)) + ((c * a) - ca)
by VECTSP_1:13
.=
(((bc * a) - ((b * a) + (c * a))) + ((b * a) - ba)) + ((c * a) - ca)
by VECTSP_1:def 3
.=
((((bc * a) - (b * a)) - (c * a)) + ((b * a) - ba)) + ((c * a) - ca)
by RLVECT_1:27
.=
(((((bc * a) - (b * a)) - (c * a)) + (b * a)) - ba) + ((c * a) - ca)
by RLVECT_1:28
.=
((((((bc * a) - (b * a)) - (c * a)) + (b * a)) - ba) + (c * a)) - ca
by RLVECT_1:28
.=
((((((bc * a) - (b * a)) + (b * a)) - (c * a)) - ba) + (c * a)) - ca
by RLVECT_1:28
.=
((((bc * a) - (c * a)) - ba) + (c * a)) - ca
by Th1
.=
((((bc * a) - (c * a)) + (c * a)) - ba) - ca
by RLVECT_1:28
.=
((bc * a) - ba) - ca
by Th1
.=
(bc * a) - (ba + ca)
by RLVECT_1:27
;
thus (y + z) * x =
Class ((EqRel (R,I)),(bc * a))
by A27, A36, Th14
.=
Class ((EqRel (R,I)),(ba + ca))
by A42, A43, Th6
.=
(y * x) + (z * x)
by A41, A29, Th13
; verum