let X be non empty set ; for d1, d2 being Element of X
for A being BinOp of X
for M being Function of [:X,X:],X
for V being Ring
for V1 being Subset of V st V1 = X & A = the addF of V || V1 & M = the multF of V || V1 & d1 = 1. V & d2 = 0. V & V1 is having-inverse holds
doubleLoopStr(# X,A,M,d1,d2 #) is Subring of V
let d1, d2 be Element of X; for A being BinOp of X
for M being Function of [:X,X:],X
for V being Ring
for V1 being Subset of V st V1 = X & A = the addF of V || V1 & M = the multF of V || V1 & d1 = 1. V & d2 = 0. V & V1 is having-inverse holds
doubleLoopStr(# X,A,M,d1,d2 #) is Subring of V
let A be BinOp of X; for M being Function of [:X,X:],X
for V being Ring
for V1 being Subset of V st V1 = X & A = the addF of V || V1 & M = the multF of V || V1 & d1 = 1. V & d2 = 0. V & V1 is having-inverse holds
doubleLoopStr(# X,A,M,d1,d2 #) is Subring of V
let M be Function of [:X,X:],X; for V being Ring
for V1 being Subset of V st V1 = X & A = the addF of V || V1 & M = the multF of V || V1 & d1 = 1. V & d2 = 0. V & V1 is having-inverse holds
doubleLoopStr(# X,A,M,d1,d2 #) is Subring of V
let V be Ring; for V1 being Subset of V st V1 = X & A = the addF of V || V1 & M = the multF of V || V1 & d1 = 1. V & d2 = 0. V & V1 is having-inverse holds
doubleLoopStr(# X,A,M,d1,d2 #) is Subring of V
let V1 be Subset of V; ( V1 = X & A = the addF of V || V1 & M = the multF of V || V1 & d1 = 1. V & d2 = 0. V & V1 is having-inverse implies doubleLoopStr(# X,A,M,d1,d2 #) is Subring of V )
assume that
A1:
V1 = X
and
A2:
A = the addF of V || V1
and
A3:
M = the multF of V || V1
and
A4:
d1 = 1. V
and
A5:
d2 = 0. V
and
A6:
for v being Element of V st v in V1 holds
- v in V1
; C0SP1:def 1 doubleLoopStr(# X,A,M,d1,d2 #) is Subring of V
reconsider W = doubleLoopStr(# X,A,M,d1,d2 #) as non empty doubleLoopStr ;
A9:
( W is Abelian & W is add-associative & W is right_zeroed & W is right_complementable & W is associative & W is well-unital & W is distributive )
proof
set MV = the
multF of
V;
set Av = the
addF of
V;
thus
W is
right_complementable
( W is associative & W is well-unital & W is distributive )
hereby VECTSP_1:def 7 verum
let a,
x,
y be
Element of
W;
( a * (x + y) = (a * x) + (a * y) & (x + y) * a = (x * a) + (y * a) )reconsider x1 =
x,
y1 =
y,
a1 =
a as
Element of
V by A1, TARSKI:def 3;
(x + y) * a = the
multF of
V . (
(x + y),
a)
by A7;
then
(x + y) * a = (x1 + y1) * a1
by A8;
then
(x + y) * a = (x1 * a1) + (y1 * a1)
by VECTSP_1:def 7;
then
(x + y) * a = the
addF of
V . (
( the multF of V . (x1,a1)),
(y * a))
by A7;
then A13:
(x + y) * a = the
addF of
V . (
(x * a),
(y * a))
by A7;
a * (x + y) = the
multF of
V . (
a,
(x + y))
by A7;
then
a * (x + y) = a1 * (x1 + y1)
by A8;
then
a * (x + y) = (a1 * x1) + (a1 * y1)
by VECTSP_1:def 7;
then
a * (x + y) = the
addF of
V . (
( the multF of V . (a,x1)),
(a * y))
by A7;
then
a * (x + y) = the
addF of
V . (
(a * x),
(a * y))
by A7;
hence
(
a * (x + y) = (a * x) + (a * y) &
(x + y) * a = (x * a) + (y * a) )
by A8, A13;
verum
end;
end;
( 0. W = 0. V & 1. W = 1. V )
by A4, A5;
hence
doubleLoopStr(# X,A,M,d1,d2 #) is Subring of V
by A1, A2, A3, A9, Def3; verum