set c = NonNegElements v;
set a = the addF of K | [:(NonNegElements v),(NonNegElements v):];
set m = the multF of K | [:(NonNegElements v),(NonNegElements v):];
set j = 1. K;
set z = 0. K;
A2:
NonNegElements v c= the carrier of K
by Th48;
now for x being set st x in [:(NonNegElements v),(NonNegElements v):] holds
the addF of K . x in NonNegElements vlet x be
set ;
( x in [:(NonNegElements v),(NonNegElements v):] implies the addF of K . x in NonNegElements v )assume A3:
x in [:(NonNegElements v),(NonNegElements v):]
;
the addF of K . x in NonNegElements vset q = the
addF of
K . x;
consider x1,
x2 being
object such that A4:
x1 in NonNegElements v
and A5:
x2 in NonNegElements v
and A6:
x = [x1,x2]
by A3, ZFMISC_1:def 2;
consider y1 being
Element of
K such that A7:
y1 = x1
and A8:
0 <= v . y1
by A4;
consider y2 being
Element of
K such that A9:
y2 = x2
and A10:
0 <= v . y2
by A5;
A11:
min (
(v . y1),
(v . y2))
<= v . (y1 + y2)
by A1, Th27;
0 <= min (
(v . y1),
(v . y2))
by A8, A10, XXREAL_0:20;
hence
the
addF of
K . x in NonNegElements v
by A6, A7, A11, A9;
verum end;
then reconsider ca = NonNegElements v as Preserv of the addF of K by A2, REALSET1:def 1;
the addF of K || ca is BinOp of (NonNegElements v)
;
then reconsider a = the addF of K | [:(NonNegElements v),(NonNegElements v):] as BinOp of (NonNegElements v) ;
then reconsider cm = NonNegElements v as Preserv of the multF of K by A2, REALSET1:def 1;
the multF of K || cm is BinOp of (NonNegElements v)
;
then reconsider m = the multF of K | [:(NonNegElements v),(NonNegElements v):] as BinOp of (NonNegElements v) ;
A20:
v . (0. K) = +infty
by A1, Def8;
reconsider j = 1. K, z = 0. K as Element of NonNegElements v by A1, Th49, Th50;
set R = doubleLoopStr(# (NonNegElements v),a,m,j,z #);
z in NonNegElements v
by A20;
then reconsider R = doubleLoopStr(# (NonNegElements v),a,m,j,z #) as non empty doubleLoopStr ;
A21:
now for x, y being Element of R
for x1, y1 being Element of K st x = x1 & y = y1 holds
x + y = x1 + y1end;
A23:
now for x, y being Element of R
for x1, y1 being Element of K st x = x1 & y = y1 holds
x * y = x1 * y1end;
A25:
now for x, e being Element of R st e = j holds
( x * e = x & e * x = x )let x,
e be
Element of
R;
( e = j implies ( x * e = x & e * x = x ) )assume A26:
e = j
;
( x * e = x & e * x = x )reconsider x1 =
x,
e1 =
e as
Element of
K by A2;
thus x * e =
x1 * e1
by A23
.=
x
by A26
;
e * x = xthus e * x =
e1 * x1
by A23
.=
x
by A26
;
verum end;
R is well-unital
by A25;
then reconsider R = R as non empty well-unital doubleLoopStr ;
( R is Abelian & R is add-associative & R is right_zeroed & R is right_complementable & R is commutative & R is associative & R is distributive & not R is degenerated )
proof
thus
R is
right_complementable
( R is commutative & R is associative & R is distributive & not R is degenerated )
hereby VECTSP_1:def 7 not R is degenerated
let x,
y,
z be
Element of
R;
( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )reconsider x1 =
x,
y1 =
y,
z1 =
z as
Element of
K by A2;
A32:
y + z = y1 + z1
by A21;
A33:
x * y = x1 * y1
by A23;
A34:
x * z = x1 * z1
by A23;
A35:
y * x = y1 * x1
by A23;
A36:
z * x = z1 * x1
by A23;
thus x * (y + z) =
x1 * (y1 + z1)
by A32, A23
.=
(x1 * y1) + (x1 * z1)
by VECTSP_1:def 2
.=
(x * y) + (x * z)
by A21, A33, A34
;
(y + z) * x = (y * x) + (z * x)thus (y + z) * x =
(y1 + z1) * x1
by A32, A23
.=
(y1 * x1) + (z1 * x1)
by VECTSP_1:def 2
.=
(y * x) + (z * x)
by A21, A35, A36
;
verum
end;
thus
0. R <> 1. R
;
STRUCT_0:def 8 verum
end;
hence
ex b1 being non degenerated strict commutative Ring st
( the carrier of b1 = NonNegElements v & the addF of b1 = the addF of K | [:(NonNegElements v),(NonNegElements v):] & the multF of b1 = the multF of K | [:(NonNegElements v),(NonNegElements v):] & the ZeroF of b1 = 0. K & the OneF of b1 = 1. K )
; verum