set cR = the carrier of R;
set ccs = { x where x is Element of R : for s being Element of R holds x * s = s * x } ;
for s being Element of the carrier of R holds (0. R) * s = s * (0. R)
;
then A1:
0. R in { x where x is Element of R : for s being Element of R holds x * s = s * x }
;
then reconsider ccs = { x where x is Element of R : for s being Element of R holds x * s = s * x } as non empty set ;
A2:
ccs c= the carrier of R
set acs = the addF of R || ccs;
set mcs = the multF of R || ccs;
set Zs = 0. R;
set Us = 1_ R;
A3:
[:ccs,ccs:] c= [: the carrier of R, the carrier of R:]
then reconsider acs = the addF of R || ccs as Function of [:ccs,ccs:], the carrier of R by FUNCT_2:32;
rng acs c= ccs
proof
let y be
object ;
TARSKI:def 3 ( not y in rng acs or y in ccs )
assume
y in rng acs
;
y in ccs
then consider x being
object such that A4:
x in dom acs
and A5:
y = acs . x
by FUNCT_1:def 3;
consider a,
b being
object such that A6:
a in ccs
and A7:
b in ccs
and A8:
x = [a,b]
by A4, ZFMISC_1:def 2;
reconsider a =
a,
b =
b as
Element of the
carrier of
R by A2, A6, A7;
A9:
ex
a9 being
Element of the
carrier of
R st
(
a9 = a & ( for
s being
Element of
R holds
a9 * s = s * a9 ) )
by A6;
A10:
ex
b9 being
Element of the
carrier of
R st
(
b9 = b & ( for
s being
Element of
R holds
b9 * s = s * b9 ) )
by A7;
[a,b] in [:ccs,ccs:]
by A6, A7, ZFMISC_1:def 2;
then A11:
a + b = acs . x
by A8, FUNCT_1:49;
hence
y in ccs
by A5, A11;
verum
end;
then reconsider acs = acs as BinOp of ccs by FUNCT_2:6;
reconsider mcs = the multF of R || ccs as Function of [:ccs,ccs:], the carrier of R by A3, FUNCT_2:32;
rng mcs c= ccs
proof
let y be
object ;
TARSKI:def 3 ( not y in rng mcs or y in ccs )
assume
y in rng mcs
;
y in ccs
then consider x being
object such that A12:
x in dom mcs
and A13:
y = mcs . x
by FUNCT_1:def 3;
consider a,
b being
object such that A14:
a in ccs
and A15:
b in ccs
and A16:
x = [a,b]
by A12, ZFMISC_1:def 2;
reconsider a =
a,
b =
b as
Element of the
carrier of
R by A2, A14, A15;
A17:
ex
a9 being
Element of the
carrier of
R st
(
a9 = a & ( for
s being
Element of
R holds
a9 * s = s * a9 ) )
by A14;
A18:
ex
b9 being
Element of the
carrier of
R st
(
b9 = b & ( for
s being
Element of
R holds
b9 * s = s * b9 ) )
by A15;
[a,b] in [:ccs,ccs:]
by A14, A15, ZFMISC_1:def 2;
then A19:
a * b = mcs . x
by A16, FUNCT_1:49;
hence
y in ccs
by A13, A19;
verum
end;
then reconsider mcs = mcs as BinOp of ccs by FUNCT_2:6;
reconsider Zs = 0. R as Element of ccs by A1;
for s being Element of the carrier of R holds (1_ R) * s = s * (1_ R)
;
then
1_ R in ccs
;
then reconsider Us = 1_ R as Element of ccs ;
reconsider cs = doubleLoopStr(# ccs,acs,mcs,Us,Zs #) as non empty doubleLoopStr ;
set ccs1 = the carrier of cs;
A24:
for a, b being Element of the carrier of R
for c, d being Element of the carrier of cs st a = c & b = d holds
a + b = c + d
A27:
cs is Abelian
A28:
cs is add-associative
A31:
cs is right_zeroed
A32:
cs is right_complementable
A35:
cs is associative
A38:
cs is commutative
A39:
now for x, e being Element of cs st e = 1_ R holds
( x * e = x & e * x = x )end;
A42:
cs is well-unital
by A39;
A43:
cs is distributive
proof
let x,
y,
z be
Element of the
carrier of
cs;
VECTSP_1:def 7 ( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
reconsider x9 =
x,
y9 =
y,
z9 =
z as
Element of the
carrier of
R by A2;
A44:
y + z = y9 + z9
by A24;
A45:
x9 * y9 = x * y
by A21;
A46:
x9 * z9 = x * z
by A21;
A47:
y9 * x9 = y * x
by A21;
A48:
z9 * x9 = z * x
by A21;
thus x * (y + z) =
x9 * (y9 + z9)
by A21, A44
.=
(x9 * y9) + (x9 * z9)
by VECTSP_1:def 7
.=
(x * y) + (x * z)
by A24, A45, A46
;
(y + z) * x = (y * x) + (z * x)
thus (y + z) * x =
(y9 + z9) * x9
by A21, A44
.=
(y9 * x9) + (z9 * x9)
by VECTSP_1:def 7
.=
(y * x) + (z * x)
by A24, A47, A48
;
verum
end;
cs is almost_left_invertible
then reconsider cs = cs as strict Field by A27, A28, A31, A32, A35, A38, A42, A43, STRUCT_0:def 8;
take
cs
; ( the carrier of cs = { x where x is Element of R : for s being Element of R holds x * s = s * x } & the addF of cs = the addF of R || the carrier of cs & the multF of cs = the multF of R || the carrier of cs & 0. cs = 0. R & 1. cs = 1. R )
thus
( the carrier of cs = { x where x is Element of R : for s being Element of R holds x * s = s * x } & the addF of cs = the addF of R || the carrier of cs & the multF of cs = the multF of R || the carrier of cs & 0. cs = 0. R & 1. cs = 1. R )
; verum