reconsider ZS = doubleLoopStr(# G_INT_SET,g_int_add,g_int_mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #) as non empty doubleLoopStr ;
A1:
for v, w being Element of ZS holds v + w = w + v
A2:
for u, v, w being Element of ZS holds (u + v) + w = u + (v + w)
A5:
for v being Element of ZS holds v + (0. ZS) = v
A6:
for v being Element of ZS holds v is right_complementable
A8:
for a, b, v being Element of ZS holds (a + b) * v = (a * v) + (b * v)
A10:
for a, v, w being Element of ZS holds
( a * (v + w) = (a * v) + (a * w) & (v + w) * a = (v * a) + (w * a) )
proof
let a,
v,
w be
Element of
ZS;
( 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;
A11:
(
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 A11, Th4
;
(v + w) * a = (v * a) + (w * a)
thus
(v + w) * a = (v * a) + (w * a)
by A8;
verum
end;
A12:
for a, b, v being Element of ZS holds (a * b) * v = a * (b * v)
for v being Element of ZS holds
( v * (1. ZS) = v & (1. ZS) * v = v )
hence
Gauss_INT_Ring is Ring
by A1, A2, A5, A6, A10, A12, VECTSP_1:def 6, VECTSP_1:def 7, GROUP_1:def 3, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, ALGSTR_0:def 16; verum