set ZS = Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #);
A1: for v, w being Element of Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #) holds v + w = w + v

proof

let v, w be Element of Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #); :: thesis: v + w = w + v
reconsider v1 = v, w1 = w as G_INTEG by Th2;
thus v + w = v1 + w1 by Th4
.= w + v by Th4 ; :: thesis: verum

end;

A2: for u, v, w being Element of Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #) holds (u + v) + w = u + (v + w)

proof

let u, v, w be Element of Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #); :: thesis: (u + v) + w = u + (v + w)
reconsider u1 = u, v1 = v, w1 = w as G_INTEG by Th2;
A3: u + v = u1 + v1 by Th4;
A4: v + w = v1 + w1 by Th4;
thus (u + v) + w = (u1 + v1) + w1 by Th4, A3
.= u1 + (v1 + w1)
.= u + (v + w) by Th4, A4 ; :: thesis: verum

end;

A5: for v being Element of Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #) holds v + (0. Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #)) = v

proof

let v be Element of Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #); :: thesis: v + (0. Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #)) = v
reconsider v1 = v as G_INTEG by Th2;
thus v + (0. Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #)) = v1 + 0 by Th4
.= v ; :: thesis: verum

end;

A6: for v being VECTOR of Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #) holds v is right_complementable

proof

let v be VECTOR of Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #); :: thesis: v is right_complementable
take (- 1) * v ; :: according to ALGSTR_0:def 11 :: thesis: v + ((- 1) * v) = 0. Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #)
reconsider v1 = v as G_INTEG by Th2;
A7: (- 1) * v = (- 1) * v1 by Th5
.= - v1 ;
thus v + ((- 1) * v) = v1 + (- v1) by A7, Th4
.= 0. Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #) ; :: thesis: verum

end;

A8: for a, b being Integer
for v being VECTOR of Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #) holds (a + b) * v = (a * v) + (b * v)

proof

let a, b be Integer; :: thesis: for v being VECTOR of Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #) holds (a + b) * v = (a * v) + (b * v)
let v be VECTOR of Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #); :: thesis: (a + b) * v = (a * v) + (b * v)
reconsider v1 = v as G_INTEG by Th2;
A9: ( a * v1 = a * v & b * v1 = b * v ) by Th5;
thus (a + b) * v = (a + b) * v1 by Th5
.= (a * v1) + (b * v1)
.= (a * v) + (b * v) by A9, Th4 ; :: thesis: verum

end;

A10: for a being Integer
for v, w being VECTOR of Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #) holds a * (v + w) = (a * v) + (a * w)

proof

let a be Integer; :: thesis: for v, w being VECTOR of Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #) holds a * (v + w) = (a * v) + (a * w)
let v, w be VECTOR of Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #); :: thesis: a * (v + w) = (a * v) + (a * w)
reconsider v1 = v, w1 = w as G_INTEG by Th2;
A11: v + w = v1 + w1 by Th4;
A12: ( a * v1 = a * v & a * w1 = a * w ) by Th5;
thus a * (v + w) = a * (v1 + w1) by A11, Th5
.= (a * v1) + (a * w1)
.= (a * v) + (a * w) by A12, Th4 ; :: thesis: verum

end;

A13: for a, b being Integer
for v being VECTOR of Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #) holds (a * b) * v = a * (b * v)

proof

let a, b be Integer; :: thesis: for v being VECTOR of Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #) holds (a * b) * v = a * (b * v)
let v be VECTOR of Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #); :: thesis: (a * b) * v = a * (b * v)
reconsider v1 = v as G_INTEG by Th2;
A14: b * v1 = b * v by Th5;
thus (a * b) * v = (a * b) * v1 by Th5
.= a * (b * v1)
.= a * (b * v) by A14, Th5 ; :: thesis: verum

end;

A15: for v, w being VECTOR of Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #)
for a being Integer holds a * (v * w) = (a * v) * w

proof

let v, w be VECTOR of Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #); :: thesis: for a being Integer holds a * (v * w) = (a * v) * w
let a be Integer; :: thesis: a * (v * w) = (a * v) * w
reconsider v1 = v, w1 = w as G_INTEG by Th2;
A16: a * v = a * v1 by Th5;
reconsider vw = v * w as G_INTEG by Th2;
thus a * (v * w) = a * vw by Th5
.= a * (v1 * w1) by Th6
.= (a * v1) * w1
.= (a * v) * w by Th6, A16 ; :: thesis: verum

end;

A17: for v, w being Element of Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #) holds v * w = w * v

proof

let v, w be Element of Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #); :: thesis: v * w = w * v
reconsider v1 = v, w1 = w as G_INTEG by Th2;
thus v * w = v1 * w1 by Th6
.= w * v by Th6 ; :: thesis: verum

end;

A18: for a, b, v being Element of Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #) holds (a + b) * v = (a * v) + (b * v)

proof

let a, b, v be Element of Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #); :: thesis: (a + b) * v = (a * v) + (b * v)
reconsider a1 = a, b1 = b, v1 = v as G_INTEG by Th2;
reconsider ab = a + b as G_INTEG by Th2;
A19: ( a1 * v1 = a * v & b1 * v1 = b * v ) by Th6;
thus (a + b) * v = ab * v1 by Th6
.= (a1 + b1) * v1 by Th4
.= (a1 * v1) + (b1 * v1)
.= (a * v) + (b * v) by A19, Th4 ; :: thesis: verum

end;

A20: for a, v, w being Element of Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #) holds
( a * (v + w) = (a * v) + (a * w) & (v + w) * a = (v * a) + (w * a) )

proof

let a, v, w be Element of Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #); :: thesis: ( a * (v + w) = (a * v) + (a * w) & (v + w) * a = (v * a) + (w * a) )
reconsider a1 = a, v1 = v, w1 = w as G_INTEG by Th2;
reconsider vw = v + w as G_INTEG by Th2;
A21: ( a1 * v1 = a * v & a1 * w1 = a * w ) by Th6;
thus a * (v + w) = a1 * vw by Th6
.= a1 * (v1 + w1) by Th4
.= (a1 * v1) + (a1 * w1)
.= (a * v) + (a * w) by A21, Th4 ; :: thesis: (v + w) * a = (v * a) + (w * a)
thus (v + w) * a = (v * a) + (w * a) by A18; :: thesis: verum

end;

A22: for a, b, v being Element of Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #) holds (a * b) * v = a * (b * v)

proof

let a, b, v be Element of Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #); :: thesis: (a * b) * v = a * (b * v)
reconsider a1 = a, b1 = b, v1 = v as G_INTEG by Th2;
reconsider ab = a * b, bv = b * v as G_INTEG by Th2;
thus (a * b) * v = ab * v1 by Th6
.= (a1 * b1) * v1 by Th6
.= a1 * (b1 * v1)
.= a1 * bv by Th6
.= a * (b * v) by Th6 ; :: thesis: verum

end;

for v being Element of Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #) holds
( v * (1. Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #)) = v & (1. Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #)) * v = v )

proof

let v be Element of Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #); :: thesis: ( v * (1. Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #)) = v & (1. Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #)) * v = v )
reconsider v1 = v as G_INTEG by Th2;
thus v * (1. Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #)) = v1 * 1 by Th6
.= v ; :: thesis: (1. Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #)) * v = v
thus (1. Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #)) * v = 1 * v1 by Th6
.= v ; :: thesis: verum

end;

hence ( Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #) is strict & Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #) is Abelian & Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #) is add-associative & Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #) is right_zeroed & Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #) is right_complementable & Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #) is commutative & Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #) is associative & Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #) is right_unital & Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #) is right-distributive & Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #) is vector-associative & Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #) is scalar-associative & Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #) is vector-distributive & Z_AlgebraStr(# G_INT_SET,g_int_mult,g_int_add,Sc_Mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #) is scalar-distributive ) by A1, A2, A5, A6, A8, A10, A13, GROUP_1:def 3, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, A17, A22, A20, A15, GROUP_1:def 12; :: thesis: verum