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 } ;
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
set ;
TARSKI:def 3 ( not y in rng acs or y in ccs )
assume
y in rng acs
;
y in ccs
then consider x being
set such that A4:
x in dom acs
and A5:
y = acs . x
by FUNCT_1:def 3;
consider a,
b being
set 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
set ;
TARSKI:def 3 ( not y in rng mcs or y in ccs )
assume
y in rng mcs
;
y in ccs
then consider x being
set such that A12:
x in dom mcs
and A13:
y = mcs . x
by FUNCT_1:def 3;
consider a,
b being
set 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;
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 ;
A20:
0. cs = Zs
;
set ccs1 = the carrier of cs;
A25:
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
A28:
cs is Abelian
A30:
cs is add-associative
A35:
cs is right_zeroed
A36:
cs is right_complementable
A39:
cs is associative
A44:
cs is commutative
A49:
cs is well-unital
A50:
1. cs = 1. R
;
A51:
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) )
A52:
x in the
carrier of
cs
;
A53:
y in the
carrier of
cs
;
z in the
carrier of
cs
;
then reconsider x9 =
x,
y9 =
y,
z9 =
z as
Element of the
carrier of
R by A2, A52, A53;
A54:
y + z = y9 + z9
by A25;
A55:
x9 * y9 = x * y
by A22;
A56:
x9 * z9 = x * z
by A22;
A57:
y9 * x9 = y * x
by A22;
A58:
z9 * x9 = z * x
by A22;
thus x * (y + z) =
x9 * (y9 + z9)
by A22, A54
.=
(x9 * y9) + (x9 * z9)
by VECTSP_1:def 7
.=
(x * y) + (x * z)
by A25, A55, A56
;
(y + z) * x = (y * x) + (z * x)
thus (y + z) * x =
(y9 + z9) * x9
by A22, A54
.=
(y9 * x9) + (z9 * x9)
by VECTSP_1:def 7
.=
(y * x) + (z * x)
by A25, A57, A58
;
verum
end;
cs is almost_left_invertible
then reconsider cs = cs as strict Field by A20, A28, A30, A35, A36, A39, A44, A49, A50, A51, 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