:: Ordered Rings - Part I
:: by Micha{\l} Muzalewski and Les{\l}aw W. Szczerba
::
:: Received October 11, 1990
:: Copyright (c) 1990 Association of Mizar Users
Lm1:
for R being non empty doubleLoopStr
for h, f, g being FinSequence of R holds
( h = f ^ g iff ( dom h = Seg ((len f) + (len g)) & ( for k being Nat st k in dom f holds
h /. k = f /. k ) & ( for k being Nat st k in dom g holds
h /. ((len f) + k) = g /. k ) ) )
Lm2:
for R being non empty doubleLoopStr
for x being Scalar of R
for f being FinSequence of R holds
( f = <*x*> iff ( len f = 1 & f /. 1 = x ) )
Lm3:
for R being non empty doubleLoopStr
for x being Scalar of R
for f being FinSequence of R holds (f ^ <*x*>) /. ((len f) + 1) = x
Lm4:
for i being Nat
for R being non empty doubleLoopStr
for f, g being FinSequence of R st i <> 0 & i <= len f holds
(f ^ g) /. i = f /. i
Lm5:
for i being Nat
for R being non empty doubleLoopStr
for g, f being FinSequence of R st i <> 0 & i <= len g holds
(f ^ g) /. ((len f) + i) = g /. i
:: deftheorem O_RING_1:def 1 :
canceled;
:: deftheorem defines ^2 O_RING_1:def 2 :
:: deftheorem defines being_a_square O_RING_1:def 3 :
:: deftheorem Def4 defines being_a_Sum_of_squares O_RING_1:def 4 :
:: deftheorem Def5 defines being_a_sum_of_squares O_RING_1:def 5 :
Lm6:
for R being non empty doubleLoopStr
for x being Scalar of R st x is being_a_square holds
<*x*> is being_a_Sum_of_squares
Lm7:
for R being non empty doubleLoopStr
for x being Scalar of R st x is being_a_square holds
x is being_a_sum_of_squares
:: deftheorem Def6 defines being_a_Product_of_squares O_RING_1:def 6 :
:: deftheorem Def7 defines being_a_product_of_squares O_RING_1:def 7 :
Lm8:
for R being non empty doubleLoopStr
for x being Scalar of R st x is being_a_square holds
<*x*> is being_a_Product_of_squares
Lm9:
for R being non empty doubleLoopStr
for x being Scalar of R st x is being_a_square holds
x is being_a_product_of_squares
:: deftheorem Def8 defines being_a_Sum_of_products_of_squares O_RING_1:def 8 :
:: deftheorem Def9 defines being_a_sum_of_products_of_squares O_RING_1:def 9 :
Lm10:
for R being non empty doubleLoopStr
for x being Scalar of R st x is being_a_square holds
<*x*> is being_a_Sum_of_products_of_squares
Lm11:
for R being non empty doubleLoopStr
for x being Scalar of R st x is being_a_square holds
x is being_a_sum_of_products_of_squares
Lm12:
for R being non empty doubleLoopStr
for x being Scalar of R st x is being_a_product_of_squares holds
<*x*> is being_a_Sum_of_products_of_squares
Lm13:
for R being non empty doubleLoopStr
for x being Scalar of R st x is being_a_product_of_squares holds
x is being_a_sum_of_products_of_squares
Lm14:
for R being non empty doubleLoopStr
for f being FinSequence of R st f is being_a_Sum_of_squares holds
f is being_a_Sum_of_products_of_squares
Lm15:
for R being non empty doubleLoopStr
for x being Scalar of R st x is being_a_sum_of_squares holds
x is being_a_sum_of_products_of_squares
:: deftheorem Def10 defines being_an_Amalgam_of_squares O_RING_1:def 10 :
:: deftheorem Def11 defines being_an_amalgam_of_squares O_RING_1:def 11 :
Lm16:
for R being non empty doubleLoopStr
for x being Scalar of R st x is being_a_square holds
<*x*> is being_an_Amalgam_of_squares
Lm17:
for R being non empty doubleLoopStr
for x being Scalar of R st x is being_a_square holds
x is being_an_amalgam_of_squares
Lm18:
for R being non empty doubleLoopStr
for x being Scalar of R st x is being_a_product_of_squares holds
<*x*> is being_an_Amalgam_of_squares
Lm19:
for R being non empty doubleLoopStr
for x being Scalar of R st x is being_a_product_of_squares holds
x is being_an_amalgam_of_squares
:: deftheorem Def12 defines being_a_Sum_of_amalgams_of_squares O_RING_1:def 12 :
:: deftheorem Def13 defines being_a_sum_of_amalgams_of_squares O_RING_1:def 13 :
Lm20:
for R being non empty doubleLoopStr
for x being Scalar of R st x is being_a_square holds
<*x*> is being_a_Sum_of_amalgams_of_squares
Lm21:
for R being non empty doubleLoopStr
for x being Scalar of R st x is being_a_square holds
x is being_a_sum_of_amalgams_of_squares
Lm22:
for R being non empty doubleLoopStr
for f being FinSequence of R st f is being_a_Sum_of_squares holds
f is being_a_Sum_of_amalgams_of_squares
Lm23:
for R being non empty doubleLoopStr
for x being Scalar of R st x is being_a_sum_of_squares holds
x is being_a_sum_of_amalgams_of_squares
Lm24:
for R being non empty doubleLoopStr
for x being Scalar of R st x is being_a_product_of_squares holds
<*x*> is being_a_Sum_of_amalgams_of_squares
Lm25:
for R being non empty doubleLoopStr
for x being Scalar of R st x is being_a_product_of_squares holds
x is being_a_sum_of_amalgams_of_squares
Lm26:
for R being non empty doubleLoopStr
for f being FinSequence of R st f is being_a_Sum_of_products_of_squares holds
f is being_a_Sum_of_amalgams_of_squares
Lm27:
for R being non empty doubleLoopStr
for x being Scalar of R st x is being_a_sum_of_products_of_squares holds
x is being_a_sum_of_amalgams_of_squares
Lm28:
for R being non empty doubleLoopStr
for x being Scalar of R st x is being_an_amalgam_of_squares holds
<*x*> is being_a_Sum_of_amalgams_of_squares
Lm29:
for R being non empty doubleLoopStr
for x being Scalar of R st x is being_an_amalgam_of_squares holds
x is being_a_sum_of_amalgams_of_squares
:: deftheorem Def14 defines being_a_generation_from_squares O_RING_1:def 14 :
:: deftheorem Def15 defines generated_from_squares O_RING_1:def 15 :
Lm30:
for R being non empty doubleLoopStr
for x being Scalar of R st x is being_a_square holds
<*x*> is being_a_generation_from_squares
Lm31:
for R being non empty doubleLoopStr
for x being Scalar of R st x is being_a_square holds
x is generated_from_squares
Lm32:
for i, j being Nat
for R being non empty doubleLoopStr
for f being FinSequence of R st f is being_a_generation_from_squares & i <> 0 & i <= len f & j <> 0 & j <= len f holds
f ^ <*((f /. i) + (f /. j))*> is being_a_generation_from_squares
Lm33:
for R being non empty doubleLoopStr
for f, g being FinSequence of R st f is being_a_generation_from_squares & g is being_a_generation_from_squares holds
f ^ g is being_a_generation_from_squares
Lm34:
for R being non empty doubleLoopStr
for x being Scalar of R
for f being FinSequence of R st f is being_a_generation_from_squares & x is being_a_square holds
f ^ <*x*> is being_a_generation_from_squares
Lm35:
for R being non empty doubleLoopStr
for x being Scalar of R
for f being FinSequence of R st f is being_a_generation_from_squares & x is being_a_square holds
(f ^ <*x*>) ^ <*((f /. (len f)) + x)*> is being_a_generation_from_squares
Lm36:
for R being non empty doubleLoopStr
for x, y being Scalar of R st x is generated_from_squares & y is being_a_square holds
x + y is generated_from_squares
Lm37:
for i being Nat
for R being non empty doubleLoopStr
for f being FinSequence of R st f is being_a_Sum_of_squares & 0 <> i & i <= len f holds
f /. i is generated_from_squares
Lm38:
for R being non empty doubleLoopStr
for x being Scalar of R st x is being_a_sum_of_squares holds
x is generated_from_squares
Lm39:
for R being non empty doubleLoopStr
for f being FinSequence of R st f is being_an_Amalgam_of_squares holds
f is being_a_generation_from_squares
Lm40:
for R being non empty doubleLoopStr
for x being Scalar of R st x is being_an_amalgam_of_squares holds
x is generated_from_squares
Lm41:
for R being non empty doubleLoopStr
for x being Scalar of R st x is being_an_amalgam_of_squares holds
<*x*> is being_a_generation_from_squares
Lm42:
for R being non empty doubleLoopStr
for x being Scalar of R
for f being FinSequence of R st f is being_a_generation_from_squares & x is being_an_amalgam_of_squares holds
(f ^ <*x*>) ^ <*((f /. (len f)) + x)*> is being_a_generation_from_squares
Lm43:
for R being non empty doubleLoopStr
for x, y being Scalar of R st x is generated_from_squares & y is being_an_amalgam_of_squares holds
x + y is generated_from_squares
Lm44:
for R being non empty doubleLoopStr
for f being FinSequence of R st f is being_a_Sum_of_amalgams_of_squares holds
for i being Nat st i <> 0 & i <= len f holds
f /. i is generated_from_squares
theorem Th1: :: O_RING_1:1
Lm45:
for i, j being Nat
for R being non empty doubleLoopStr
for f being FinSequence of R st f is being_a_generation_from_squares & i <> 0 & i <= len f & j <> 0 & j <= len f holds
f ^ <*((f /. i) * (f /. j))*> is being_a_generation_from_squares
Lm46:
for R being non empty doubleLoopStr
for x being Scalar of R
for f being FinSequence of R st f is being_a_generation_from_squares & x is being_a_square holds
(f ^ <*x*>) ^ <*((f /. (len f)) * x)*> is being_a_generation_from_squares
Lm47:
for R being non empty doubleLoopStr
for x, y being Scalar of R st x is generated_from_squares & y is being_a_square holds
x * y is generated_from_squares
Lm48:
for i being Nat
for R being non empty doubleLoopStr
for f being FinSequence of R st f is being_a_Product_of_squares & 0 <> i & i <= len f holds
f /. i is generated_from_squares
Lm49:
for R being non empty doubleLoopStr
for x being Scalar of R st x is being_a_product_of_squares holds
x is generated_from_squares
Lm50:
for R being non empty doubleLoopStr
for x being Scalar of R st x is being_a_product_of_squares holds
<*x*> is being_a_generation_from_squares
Lm51:
for R being non empty doubleLoopStr
for x being Scalar of R
for f being FinSequence of R st f is being_a_generation_from_squares & x is being_a_product_of_squares holds
(f ^ <*x*>) ^ <*((f /. (len f)) + x)*> is being_a_generation_from_squares
Lm52:
for R being non empty doubleLoopStr
for x, y being Scalar of R st x is generated_from_squares & y is being_a_product_of_squares holds
x + y is generated_from_squares
Lm53:
for i being Nat
for R being non empty doubleLoopStr
for f being FinSequence of R st f is being_a_Sum_of_products_of_squares & 0 <> i & i <= len f holds
f /. i is generated_from_squares
Lm54:
for R being non empty doubleLoopStr
for x being Scalar of R st x is being_a_sum_of_products_of_squares holds
x is generated_from_squares
theorem :: O_RING_1:2
theorem :: O_RING_1:3
theorem :: O_RING_1:4
theorem :: O_RING_1:5
theorem :: O_RING_1:6
Lm55:
for R being non empty doubleLoopStr
for x being Scalar of R
for f being FinSequence of R st f is being_a_Sum_of_squares & x is being_a_square holds
f ^ <*((f /. (len f)) + x)*> is being_a_Sum_of_squares
Lm56:
for R being non empty doubleLoopStr
for x, y being Scalar of R st x is being_a_sum_of_squares & y is being_a_square holds
x + y is being_a_sum_of_squares
Lm57:
for R being non empty doubleLoopStr
for x being Scalar of R
for f being FinSequence of R st f is being_a_Sum_of_products_of_squares & x is being_a_product_of_squares holds
f ^ <*((f /. (len f)) + x)*> is being_a_Sum_of_products_of_squares
Lm58:
for R being non empty doubleLoopStr
for x, y being Scalar of R st x is being_a_sum_of_products_of_squares & y is being_a_product_of_squares holds
x + y is being_a_sum_of_products_of_squares
Lm59:
for R being non empty doubleLoopStr
for x being Scalar of R
for f being FinSequence of R st f is being_a_Sum_of_amalgams_of_squares & x is being_an_amalgam_of_squares holds
f ^ <*((f /. (len f)) + x)*> is being_a_Sum_of_amalgams_of_squares
Lm60:
for R being non empty doubleLoopStr
for x, y being Scalar of R st x is being_a_sum_of_amalgams_of_squares & y is being_an_amalgam_of_squares holds
x + y is being_a_sum_of_amalgams_of_squares
Lm61:
for i, j being Nat
for R being non empty doubleLoopStr
for f being FinSequence of R st f is being_a_generation_from_squares & i <> 0 & i <= len f & j <> 0 & j <= len f holds
f ^ <*((f /. i) + (f /. j))*> is being_a_generation_from_squares
Lm62:
for R being non empty doubleLoopStr
for x, y being Scalar of R st x is being_a_square & y is being_a_square holds
x + y is being_a_sum_of_squares
Lm63:
for R being non empty doubleLoopStr
for f, g being FinSequence of R st f is being_a_generation_from_squares & g is being_a_generation_from_squares holds
(f ^ g) ^ <*((f /. (len f)) + (g /. (len g)))*> is being_a_generation_from_squares
Lm64:
for R being non empty doubleLoopStr
for x, y being Scalar of R st x is generated_from_squares & y is generated_from_squares holds
x + y is generated_from_squares
theorem :: O_RING_1:7
Lm65:
for R being non empty doubleLoopStr
for x, y being Scalar of R st x is being_a_sum_of_products_of_squares & y is being_a_square holds
x + y is being_a_sum_of_products_of_squares
theorem :: O_RING_1:8
Lm66:
for R being non empty doubleLoopStr
for x, y being Scalar of R st x is being_an_amalgam_of_squares & y is being_a_product_of_squares holds
x + y is being_a_sum_of_amalgams_of_squares
Lm67:
for R being non empty doubleLoopStr
for x, y being Scalar of R st x is being_an_amalgam_of_squares & y is being_an_amalgam_of_squares holds
x + y is being_a_sum_of_amalgams_of_squares
Lm68:
for R being non empty doubleLoopStr
for x, y being Scalar of R st x is being_a_sum_of_amalgams_of_squares & y is being_a_product_of_squares holds
x + y is being_a_sum_of_amalgams_of_squares
Lm69:
for R being non empty doubleLoopStr
for x, y being Scalar of R st x is being_a_sum_of_amalgams_of_squares & y is being_a_square holds
x + y is being_a_sum_of_amalgams_of_squares
theorem :: O_RING_1:9
Lm70:
for R being non empty doubleLoopStr
for x, y being Scalar of R st x is being_a_square & y is being_a_sum_of_squares holds
x + y is generated_from_squares
Lm71:
for R being non empty doubleLoopStr
for x, y being Scalar of R st x is being_a_square & y is being_a_product_of_squares holds
x + y is generated_from_squares
Lm72:
for R being non empty doubleLoopStr
for x, y being Scalar of R st x is being_a_square & y is generated_from_squares holds
x + y is generated_from_squares
Lm73:
for R being non empty doubleLoopStr
for x, y being Scalar of R st x is being_a_square & y is being_a_sum_of_products_of_squares holds
x + y is generated_from_squares
Lm74:
for R being non empty doubleLoopStr
for x, y being Scalar of R st x is being_a_square & y is being_an_amalgam_of_squares holds
x + y is generated_from_squares
by Lm40, Lm72;
Lm75:
for R being non empty doubleLoopStr
for x, y being Scalar of R st x is being_a_square & y is being_a_sum_of_amalgams_of_squares holds
x + y is generated_from_squares
by Lm72, Th1;
theorem :: O_RING_1:10
theorem :: O_RING_1:11
theorem :: O_RING_1:12
theorem :: O_RING_1:13
theorem :: O_RING_1:14
theorem :: O_RING_1:15
theorem :: O_RING_1:16
theorem :: O_RING_1:17
theorem :: O_RING_1:18
theorem :: O_RING_1:19
theorem :: O_RING_1:20
theorem :: O_RING_1:21
theorem :: O_RING_1:22
theorem :: O_RING_1:23
theorem :: O_RING_1:24
theorem :: O_RING_1:25
theorem :: O_RING_1:26
theorem :: O_RING_1:27
theorem :: O_RING_1:28
theorem :: O_RING_1:29
theorem :: O_RING_1:30
theorem :: O_RING_1:31
theorem :: O_RING_1:32
theorem :: O_RING_1:33
theorem :: O_RING_1:34
theorem :: O_RING_1:35
theorem :: O_RING_1:36
theorem :: O_RING_1:37
Lm76:
for R being non empty doubleLoopStr
for x, y being Scalar of R st x is generated_from_squares & y is being_a_sum_of_squares holds
x + y is generated_from_squares
Lm77:
for R being non empty doubleLoopStr
for x, y being Scalar of R st x is generated_from_squares & y is being_a_product_of_squares holds
x + y is generated_from_squares
Lm78:
for R being non empty doubleLoopStr
for x, y being Scalar of R st x is generated_from_squares & y is being_a_sum_of_products_of_squares holds
x + y is generated_from_squares
Lm79:
for R being non empty doubleLoopStr
for x, y being Scalar of R st x is generated_from_squares & y is being_a_sum_of_amalgams_of_squares holds
x + y is generated_from_squares
theorem :: O_RING_1:38
Lm80:
for R being non empty doubleLoopStr
for f, g being FinSequence of R st f is being_an_Amalgam_of_squares & g is being_an_Amalgam_of_squares holds
f ^ g is being_an_Amalgam_of_squares
Lm81:
for i, j being Nat
for R being non empty doubleLoopStr
for f being FinSequence of R st f is being_an_Amalgam_of_squares & i <> 0 & i <= len f & j <> 0 & j <= len f holds
f ^ <*((f /. i) * (f /. j))*> is being_an_Amalgam_of_squares
Lm82:
for i, j being Nat
for R being non empty doubleLoopStr
for f being FinSequence of R st f is being_a_generation_from_squares & i <> 0 & i <= len f & j <> 0 & j <= len f holds
f ^ <*((f /. i) * (f /. j))*> is being_a_generation_from_squares
Lm83:
for R being non empty doubleLoopStr
for x being Scalar of R
for f being FinSequence of R st f is being_a_Product_of_squares & x is being_a_square holds
f ^ <*((f /. (len f)) * x)*> is being_a_Product_of_squares
Lm84:
for R being non empty doubleLoopStr
for f, g being FinSequence of R st f is being_an_Amalgam_of_squares & g is being_an_Amalgam_of_squares holds
(f ^ g) ^ <*((f /. (len f)) * (g /. (len g)))*> is being_an_Amalgam_of_squares
Lm85:
for R being non empty doubleLoopStr
for f, g being FinSequence of R st f is being_a_generation_from_squares & g is being_a_generation_from_squares holds
(f ^ g) ^ <*((f /. (len f)) * (g /. (len g)))*> is being_a_generation_from_squares
theorem :: O_RING_1:39
theorem :: O_RING_1:40
Lm86:
for R being non empty doubleLoopStr
for x, y being Scalar of R st x is being_an_amalgam_of_squares & y is being_an_amalgam_of_squares holds
x * y is being_an_amalgam_of_squares
theorem :: O_RING_1:41
theorem :: O_RING_1:42
theorem :: O_RING_1:43
theorem :: O_RING_1:44
theorem :: O_RING_1:45
theorem :: O_RING_1:46
theorem :: O_RING_1:47
Lm87:
for R being non empty doubleLoopStr
for x, y being Scalar of R st x is generated_from_squares & y is generated_from_squares holds
x * y is generated_from_squares
theorem :: O_RING_1:48
theorem :: O_RING_1:49
theorem :: O_RING_1:50
theorem :: O_RING_1:51
theorem :: O_RING_1:52
theorem :: O_RING_1:53
theorem :: O_RING_1:54
theorem :: O_RING_1:55
theorem :: O_RING_1:56
theorem :: O_RING_1:57
theorem :: O_RING_1:58
theorem :: O_RING_1:59
theorem :: O_RING_1:60
theorem :: O_RING_1:61
theorem :: O_RING_1:62
theorem :: O_RING_1:63
theorem :: O_RING_1:64
theorem :: O_RING_1:65
theorem :: O_RING_1:66
theorem :: O_RING_1:67
theorem :: O_RING_1:68
theorem :: O_RING_1:69
theorem :: O_RING_1:70
theorem :: O_RING_1:71
theorem :: O_RING_1:72
theorem :: O_RING_1:73
theorem :: O_RING_1:74
theorem :: O_RING_1:75
theorem :: O_RING_1:76
theorem :: O_RING_1:77
theorem :: O_RING_1:78
theorem :: O_RING_1:79
theorem :: O_RING_1:80
theorem :: O_RING_1:81
theorem :: O_RING_1:82
theorem :: O_RING_1:83
theorem :: O_RING_1:84
theorem :: O_RING_1:85
theorem :: O_RING_1:86