set g = the addF of (R / I);

set E = EqRel (R,I);

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 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 ; :: 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 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 ; :: thesis: verum

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;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

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 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 ; :: thesis: verum

end;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 ; :: thesis: verum

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 )

thus
R / I is right_complementable
:: thesis: ( 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 A12, Th6;

hence v + (0. (R / I)) = v by A11, A13, A14, A15, Th6; :: thesis: verum

end;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 A12, Th6;

hence v + (0. (R / I)) = v by A11, A13, A14, A15, Th6; :: thesis: verum

proof

let v be Element of (R / I); :: according to ALGSTR_0:def 16 :: thesis: 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 ; :: 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 A16, Th13

.= 0. (R / I) by A17, RLVECT_1:def 10 ; :: thesis: verum

end;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 A16, Th13

.= 0. (R / I) by A17, RLVECT_1:def 10 ; :: thesis: verum

hereby :: according to GROUP_1:def 3 :: thesis: ( R / I is well-unital & R / I is distributive )

( 1. R = 1_ R & Class ((EqRel (R,I)),(1. R)) = 1. (R / I) )
by Def6;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 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 ; :: thesis: verum

end;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 ; :: thesis: verum

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 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 ; :: 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 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 ; :: thesis: verum