set g = the addF of (R / I);
set E = EqRel (R,I);
hereby :: according to RLVECT_1:def 2 :: thesis: ( 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); :: thesis: x + y = y + x
consider 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 ; :: thesis: verum
end;
hereby :: according to RLVECT_1:def 3 :: thesis: ( 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); :: thesis: (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 ;
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 ;
then A9: (ab - (a + b)) - (bc - (b + c)) in I by ;
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 ; :: thesis: verum
end;
hereby :: according to RLVECT_1:def 4 :: thesis: ( 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); :: thesis: v + (0. (R / I)) = v
consider 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 ;
hence v + (0. (R / I)) = v by A11, A13, A14, A15, Th6; :: thesis: verum
end;
thus R / I is right_complementable :: thesis: ( R / I is associative & R / I is well-unital & R / I is distributive )
proof
let v be Element of (R / I); :: according to ALGSTR_0:def 16 :: thesis:
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 ; :: according to ALGSTR_0:def 11 :: thesis: 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
.= 0. (R / I) by ; :: thesis: verum
end;
hereby :: according to GROUP_1:def 3 :: thesis: ( R / I is well-unital & R / I is distributive )
let x, y, z be Element of (R / I); :: thesis: (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 ;
then ab - (a * b) in I by ;
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 ;
then bc - (b * c) in I by ;
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 ;
( a * (b * c) = (a * b) * c & ((ab * c) - ((a * b) * c)) - ((a * bc) - ((a * b) * c)) = (ab * c) - (a * bc) ) by ;
then A26: (ab * c) - (a * bc) in I by ;
thus (x * y) * z = Class ((EqRel (R,I)),(ab * c)) by
.= Class ((EqRel (R,I)),(a * bc)) by
.= x * (y * z) by ; :: thesis: 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; :: according to VECTSP_1:def 6 :: thesis: R / I is distributive
let x, y, z be Element of (R / I); :: according to VECTSP_1:def 7 :: thesis: ( 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 ;
then A31: (c * a) - ca in I by ;
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 ;
then A33: ab - (a * b) in I by ;
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 ;
then A35: ac - (a * c) in I by ;
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 ;
then A37: bc - (b + c) in I by ;
then A38: (bc - (b + c)) * a in I by IDEAL_1:def 3;
a * (bc - (b + c)) in I by ;
then (a * (bc - (b + c))) - (ab - (a * b)) in I by ;
then A39: ((a * (bc - (b + c))) - (ab - (a * b))) - (ac - (a * c)) in I by ;
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
.= Class ((EqRel (R,I)),(ab + ac)) by
.= (x * y) + (x * z) by ; :: thesis: (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 ;
then (b * a) - ba in I by ;
then ((bc - (b + c)) * a) + ((b * a) - ba) in I by ;
then A42: (((bc - (b + c)) * a) + ((b * a) - ba)) + ((c * a) - ca) in I by ;
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
.= Class ((EqRel (R,I)),(ba + ca)) by
.= (y * x) + (z * x) by ; :: thesis: verum