set cR = the carrier of R;
set ccs = { x where x is Element of R : x * s = s * x } ;
(0. R) * s = s * (0. R)
;
then
0. R in { x where x is Element of R : x * s = s * x }
;
then reconsider ccs = { x where x is Element of R : 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 &
a9 * s = s * a9 )
by A6;
A10:
ex
b9 being
Element of the
carrier of
R st
(
b9 = b &
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;
(a + b) * s =
(s * a) + (s * b)
by A9, A10, VECTSP_1:def 3
.=
s * (a + b)
by VECTSP_1:def 2
;
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 &
a9 * s = s * a9 )
by A14;
A18:
ex
b9 being
Element of the
carrier of
R st
(
b9 = b &
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;
(a * b) * s =
a * (s * b)
by A18, GROUP_1:def 3
.=
(a * s) * b
by GROUP_1:def 3
.=
s * (a * b)
by A17, GROUP_1:def 3
;
hence
y in ccs
by A13, A19;
verum
end;
then reconsider mcs = mcs as BinOp of ccs by FUNCT_2:6;
(0. R) * s = s * (0. R)
;
then
0. R in ccs
;
then reconsider Zs = 0. R as Element of ccs ;
(1. R) * s =
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 ;
A20:
now for x, e being Element of cs st e = 1. R holds
( x * e = x & e * x = x )end;
A24:
cs is well-unital
by A20;
set ccs1 = the carrier of cs;
A29:
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
A32:
cs is Abelian
A33:
cs is add-associative
A36:
cs is right_zeroed
A37:
cs is right_complementable
A40:
cs is associative
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 A29;
A45:
x9 * y9 = x * y
by A26;
A46:
x9 * z9 = x * z
by A26;
A47:
y9 * x9 = y * x
by A26;
A48:
z9 * x9 = z * x
by A26;
thus x * (y + z) =
x9 * (y9 + z9)
by A26, A44
.=
(x9 * y9) + (x9 * z9)
by VECTSP_1:def 7
.=
(x * y) + (x * z)
by A29, A45, A46
;
(y + z) * x = (y * x) + (z * x)
thus (y + z) * x =
(y9 + z9) * x9
by A26, A44
.=
(y9 * x9) + (z9 * x9)
by VECTSP_1:def 7
.=
(y * x) + (z * x)
by A29, A47, A48
;
verum
end;
A49:
cs is almost_left_invertible
not cs is degenerated
;
hence
ex b1 being strict Skew-Field st
( the carrier of b1 = { x where x is Element of R : x * s = s * x } & the addF of b1 = the addF of R || the carrier of b1 & the multF of b1 = the multF of R || the carrier of b1 & 0. b1 = 0. R & 1. b1 = 1. R )
by A24, A32, A33, A36, A37, A40, A43, A49; verum