set cR = the carrier of R;
set ccs = { x where x is Element of : x * s = s * x } ;
(0. R) * s =
0. R
by VECTSP_1:39
.=
s * (0. R)
by VECTSP_1:36
;
then
0. R in { x where x is Element of : x * s = s * x }
;
then reconsider ccs = { x where x is Element of : 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:38;
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 5;
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
a' being
Element of the
carrier of
R st
(
a' = a &
a' * s = s * a' )
by A6;
A10:
ex
b' being
Element of the
carrier of
R st
(
b' = b &
b' * s = s * b' )
by A7;
[a,b] in [:ccs,ccs:]
by A6, A7, ZFMISC_1:def 2;
then A11:
a + b = acs . x
by A8, FUNCT_1:72;
(a + b) * s =
(s * a) + (s * b)
by A9, A10, VECTSP_1:def 12
.=
s * (a + b)
by VECTSP_1:def 11
;
hence
y in ccs
by A5, A11;
verum
end;
then reconsider acs = acs as BinOp of ccs by FUNCT_2:8;
reconsider mcs = the multF of R || ccs as Function of [:ccs,ccs:],the carrier of R by A3, FUNCT_2:38;
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 5;
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
a' being
Element of the
carrier of
R st
(
a' = a &
a' * s = s * a' )
by A14;
A18:
ex
b' being
Element of the
carrier of
R st
(
b' = b &
b' * s = s * b' )
by A15;
[a,b] in [:ccs,ccs:]
by A14, A15, ZFMISC_1:def 2;
then A19:
a * b = mcs . x
by A16, FUNCT_1:72;
(a * b) * s =
a * (s * b)
by A18, GROUP_1:def 4
.=
(a * s) * b
by GROUP_1:def 4
.=
s * (a * b)
by A17, GROUP_1:def 4
;
hence
y in ccs
by A13, A19;
verum
end;
then reconsider mcs = mcs as BinOp of ccs by FUNCT_2:8;
(0. R) * s =
0. R
by VECTSP_1:39
.=
s * (0. R)
by VECTSP_1:36
;
then
0. R in ccs
;
then reconsider Zs = 0. R as Element of ccs ;
(1. R) * s =
s
by VECTSP_1:def 19
.=
s * (1. R)
by VECTSP_1:def 13
;
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
;
A21:
1. cs = Us
;
A22:
now let x,
e be
Element of ;
( e = 1. R implies ( x * e = x & e * x = x ) )assume A23:
e = 1. R
;
( x * e = x & e * x = x )A24:
[x,e] in [:ccs,ccs:]
by ZFMISC_1:106;
A25:
[e,x] in [:ccs,ccs:]
by ZFMISC_1:106;
x in ccs
;
then reconsider y =
x as
Element of
by A2;
thus x * e =
y * (1. R)
by A23, A24, FUNCT_1:72
.=
x
by A1, GROUP_1:def 5
;
e * x = xthus e * x =
(1. R) * y
by A23, A25, FUNCT_1:72
.=
x
by A1, GROUP_1:def 5
;
verum end;
A26:
cs is well-unital
A27:
1. cs = 1. R
;
set ccs1 = the carrier of cs;
A32:
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
A35:
cs is Abelian
A37:
cs is add-associative
A42:
cs is right_zeroed
A43:
cs is right_complementable
A46:
cs is associative
A51:
cs is distributive
proof
let x,
y,
z be
Element of the
carrier of
cs;
VECTSP_1:def 18 ( 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 x' =
x,
y' =
y,
z' =
z as
Element of the
carrier of
R by A2, A52, A53;
A54:
y + z = y' + z'
by A32;
A55:
x' * y' = x * y
by A29;
A56:
x' * z' = x * z
by A29;
A57:
y' * x' = y * x
by A29;
A58:
z' * x' = z * x
by A29;
thus x * (y + z) =
x' * (y' + z')
by A29, A54
.=
(x' * y') + (x' * z')
by VECTSP_1:def 18
.=
(x * y) + (x * z)
by A32, A55, A56
;
(y + z) * x = (y * x) + (z * x)
thus (y + z) * x =
(y' + z') * x'
by A29, A54
.=
(y' * x') + (z' * x')
by VECTSP_1:def 18
.=
(y * x) + (z * x)
by A32, A57, A58
;
verum
end;
A59:
cs is almost_left_invertible
not cs is degenerated
by A20, A27, STRUCT_0:def 8;
hence
ex b1 being strict Skew-Field st
( the carrier of b1 = { x where x is Element of : 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 A20, A21, A26, A35, A37, A42, A43, A46, A51, A59; verum