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;

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) ;

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 ;

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 )_{1} being non degenerated strict commutative Ring st

( the carrier of b_{1} = NonNegElements v & the addF of b_{1} = the addF of K | [:(NonNegElements v),(NonNegElements v):] & the multF of b_{1} = the multF of K | [:(NonNegElements v),(NonNegElements v):] & the ZeroF of b_{1} = 0. K & the OneF of b_{1} = 1. K )
; :: thesis: verum

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 :: thesis: for x being set st x in [:(NonNegElements v),(NonNegElements v):] holds

the addF of K . x in NonNegElements v

then reconsider ca = NonNegElements v as Preserv of the addF of K by A2, REALSET1:def 1;the addF of K . x in NonNegElements v

let x be set ; :: thesis: ( x in [:(NonNegElements v),(NonNegElements v):] implies the addF of K . x in NonNegElements v )

assume A3: x in [:(NonNegElements v),(NonNegElements v):] ; :: thesis: the addF of K . x in NonNegElements v

set 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; :: thesis: verum

end;assume A3: x in [:(NonNegElements v),(NonNegElements v):] ; :: thesis: the addF of K . x in NonNegElements v

set 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; :: thesis: verum

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) ;

now :: thesis: for x being set st x in [:(NonNegElements v),(NonNegElements v):] holds

the multF of K . x in NonNegElements v

then reconsider cm = NonNegElements v as Preserv of the multF of K by A2, REALSET1:def 1;the multF of K . x in NonNegElements v

let x be set ; :: thesis: ( x in [:(NonNegElements v),(NonNegElements v):] implies the multF of K . x in NonNegElements v )

assume A12: x in [:(NonNegElements v),(NonNegElements v):] ; :: thesis: the multF of K . x in NonNegElements v

set q = the multF of K . x;

consider x1, x2 being object such that

A13: x1 in NonNegElements v and

A14: x2 in NonNegElements v and

A15: x = [x1,x2] by A12, ZFMISC_1:def 2;

consider y1 being Element of K such that

A16: y1 = x1 and

A17: 0 <= v . y1 by A13;

consider y2 being Element of K such that

A18: y2 = x2 and

A19: 0 <= v . y2 by A14;

0 + 0 <= (v . y1) + (v . y2) by A17, A19;

then 0 <= v . (y1 * y2) by A1, Def8;

hence the multF of K . x in NonNegElements v by A15, A16, A18; :: thesis: verum

end;assume A12: x in [:(NonNegElements v),(NonNegElements v):] ; :: thesis: the multF of K . x in NonNegElements v

set q = the multF of K . x;

consider x1, x2 being object such that

A13: x1 in NonNegElements v and

A14: x2 in NonNegElements v and

A15: x = [x1,x2] by A12, ZFMISC_1:def 2;

consider y1 being Element of K such that

A16: y1 = x1 and

A17: 0 <= v . y1 by A13;

consider y2 being Element of K such that

A18: y2 = x2 and

A19: 0 <= v . y2 by A14;

0 + 0 <= (v . y1) + (v . y2) by A17, A19;

then 0 <= v . (y1 * y2) by A1, Def8;

hence the multF of K . x in NonNegElements v by A15, A16, A18; :: thesis: verum

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 :: thesis: for x, y being Element of R

for x1, y1 being Element of K st x = x1 & y = y1 holds

x + y = x1 + y1

for x1, y1 being Element of K st x = x1 & y = y1 holds

x + y = x1 + y1

let x, y be Element of R; :: thesis: for x1, y1 being Element of K st x = x1 & y = y1 holds

x + y = x1 + y1

let x1, y1 be Element of K; :: thesis: ( x = x1 & y = y1 implies x + y = x1 + y1 )

assume A22: ( x = x1 & y = y1 ) ; :: thesis: x + y = x1 + y1

[x,y] in [:(NonNegElements v),(NonNegElements v):] ;

hence x + y = x1 + y1 by A22, FUNCT_1:49; :: thesis: verum

end;x + y = x1 + y1

let x1, y1 be Element of K; :: thesis: ( x = x1 & y = y1 implies x + y = x1 + y1 )

assume A22: ( x = x1 & y = y1 ) ; :: thesis: x + y = x1 + y1

[x,y] in [:(NonNegElements v),(NonNegElements v):] ;

hence x + y = x1 + y1 by A22, FUNCT_1:49; :: thesis: verum

A23: now :: thesis: for x, y being Element of R

for x1, y1 being Element of K st x = x1 & y = y1 holds

x * y = x1 * y1

for x1, y1 being Element of K st x = x1 & y = y1 holds

x * y = x1 * y1

let x, y be Element of R; :: thesis: for x1, y1 being Element of K st x = x1 & y = y1 holds

x * y = x1 * y1

let x1, y1 be Element of K; :: thesis: ( x = x1 & y = y1 implies x * y = x1 * y1 )

assume A24: ( x = x1 & y = y1 ) ; :: thesis: x * y = x1 * y1

[x,y] in [:(NonNegElements v),(NonNegElements v):] ;

hence x * y = x1 * y1 by A24, FUNCT_1:49; :: thesis: verum

end;x * y = x1 * y1

let x1, y1 be Element of K; :: thesis: ( x = x1 & y = y1 implies x * y = x1 * y1 )

assume A24: ( x = x1 & y = y1 ) ; :: thesis: x * y = x1 * y1

[x,y] in [:(NonNegElements v),(NonNegElements v):] ;

hence x * y = x1 * y1 by A24, FUNCT_1:49; :: thesis: verum

A25: now :: thesis: for x, e being Element of R st e = j holds

( x * e = x & e * x = x )

R is well-unital
by A25;( x * e = x & e * x = x )

let x, e be Element of R; :: thesis: ( e = j implies ( x * e = x & e * x = x ) )

assume A26: e = j ; :: thesis: ( 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 ; :: thesis: e * x = x

thus e * x = e1 * x1 by A23

.= x by A26 ; :: thesis: verum

end;assume A26: e = j ; :: thesis: ( 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 ; :: thesis: e * x = x

thus e * x = e1 * x1 by A23

.= x by A26 ; :: thesis: verum

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

end;

hence
ex bhereby :: according to RLVECT_1:def 2 :: thesis: ( 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 )

let x, y be Element of R; :: thesis: x + y = y + x

reconsider x1 = x, y1 = y as Element of K by A2;

thus x + y = x1 + y1 by A21

.= y + x by A21 ; :: thesis: verum

end;reconsider x1 = x, y1 = y as Element of K by A2;

thus x + y = x1 + y1 by A21

.= y + x by A21 ; :: thesis: verum

hereby :: according to RLVECT_1:def 3 :: thesis: ( R is right_zeroed & R is right_complementable & R is commutative & R is associative & R is distributive & not R is degenerated )

let x, y, z be Element of R; :: thesis: (x + y) + z = x + (y + z)

reconsider x1 = x, y1 = y, z1 = z as Element of K by A2;

A27: y + z = y1 + z1 by A21;

x + y = x1 + y1 by A21;

hence (x + y) + z = (x1 + y1) + z1 by A21

.= x1 + (y1 + z1) by RLVECT_1:def 3

.= x + (y + z) by A27, A21 ;

:: thesis: verum

end;reconsider x1 = x, y1 = y, z1 = z as Element of K by A2;

A27: y + z = y1 + z1 by A21;

x + y = x1 + y1 by A21;

hence (x + y) + z = (x1 + y1) + z1 by A21

.= x1 + (y1 + z1) by RLVECT_1:def 3

.= x + (y + z) by A27, A21 ;

:: thesis: verum

hereby :: according to RLVECT_1:def 4 :: thesis: ( R is right_complementable & R is commutative & R is associative & R is distributive & not R is degenerated )

thus
R is right_complementable
:: thesis: ( R is commutative & R is associative & R is distributive & not R is degenerated )let x be Element of R; :: thesis: x + (0. R) = x

reconsider x1 = x as Element of K by A2;

thus x + (0. R) = x1 + (0. K) by A21

.= x by RLVECT_1:def 4 ; :: thesis: verum

end;reconsider x1 = x as Element of K by A2;

thus x + (0. R) = x1 + (0. K) by A21

.= x by RLVECT_1:def 4 ; :: thesis: verum

proof

let x be Element of R; :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable

reconsider x1 = x as Element of K by A2;

consider w1 being Element of K such that

A28: x1 + w1 = 0. K by ALGSTR_0:def 11;

A29: v . (x1 + w1) = +infty by A1, A28, Def8;

end;reconsider x1 = x as Element of K by A2;

consider w1 being Element of K such that

A28: x1 + w1 = 0. K by ALGSTR_0:def 11;

A29: v . (x1 + w1) = +infty by A1, A28, Def8;

per cases
( v . w1 < v . x1 or v . x1 <= v . w1 )
;

end;

hereby :: according to GROUP_1:def 12 :: thesis: ( R is associative & R is distributive & not R is degenerated )

let x, y be Element of R; :: thesis: x * y = y * x

reconsider x1 = x, y1 = y as Element of K by A2;

thus x * y = x1 * y1 by A23

.= y * x by A23 ; :: thesis: verum

end;reconsider x1 = x, y1 = y as Element of K by A2;

thus x * y = x1 * y1 by A23

.= y * x by A23 ; :: thesis: verum

hereby :: according to GROUP_1:def 3 :: thesis: ( R is distributive & not R is degenerated )

let x, y, z be Element of R; :: thesis: (x * y) * z = x * (y * z)

reconsider x1 = x, y1 = y, z1 = z as Element of K by A2;

A31: y * z = y1 * z1 by A23;

x * y = x1 * y1 by A23;

hence (x * y) * z = (x1 * y1) * z1 by A23

.= x1 * (y1 * z1) by GROUP_1:def 3

.= x * (y * z) by A31, A23 ;

:: thesis: verum

end;reconsider x1 = x, y1 = y, z1 = z as Element of K by A2;

A31: y * z = y1 * z1 by A23;

x * y = x1 * y1 by A23;

hence (x * y) * z = (x1 * y1) * z1 by A23

.= x1 * (y1 * z1) by GROUP_1:def 3

.= x * (y * z) by A31, A23 ;

:: thesis: verum

hereby :: according to VECTSP_1:def 7 :: thesis: not R is degenerated

thus
0. R <> 1. R
; :: according to STRUCT_0:def 8 :: thesis: verumlet x, y, z be Element of R; :: thesis: ( 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 ; :: thesis: (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 ; :: thesis: verum

end;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 ; :: thesis: (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 ; :: thesis: verum

( the carrier of b