:: O_RING_3 semantic presentation

Lemma1: for b₁ being Nat st b₁ < 1 holds
b₁ = 0

proof end;

Lemma2: for b₁ being Nat st b₁ <> 0 holds
1 <= b₁

proof end;

Lemma3: for b₁ being Nat holds
( not b₁ <= 1 or b₁ = 0 or b₁ = 1 )

proof end;

Lemma4: for b₁ being non empty doubleLoopStr
for b₂, b₃, b₄ being FinSequence of the carrier of b₁ holds
( b₂ = b₃ ^ b₄ iff ( dom b₂ = Seg ((len b₃) + (len b₄)) & ( for b₅ being Nat st b₅ in dom b₃ holds
b₂ .: b₅ = b₃ .: b₅ ) & ( for b₅ being Nat st b₅ in dom b₄ holds
b₂ .: ((len b₃) + b₅) = b₄ .: b₅ ) ) )

proof end;

Lemma5: for b₁ being non empty doubleLoopStr
for b₂ being Scalar of b₁
for b₃ being FinSequence of the carrier of b₁ holds
( b₃ = <*b₂*> iff ( len b₃ = 1 & b₃ .: 1 = b₂ ) )

proof end;

Lemma6: for b₁ being non empty doubleLoopStr
for b₂ being Scalar of b₁
for b₃ being FinSequence of the carrier of b₁ holds (b₃ ^ <*b₂*>) .: ((len b₃) + 1) = b₂

proof end;

Lemma7: for b₁ being Nat
for b₂ being non empty doubleLoopStr
for b₃, b₄ being FinSequence of the carrier of b₂ st b₁ <> 0 & b₁ <= len b₃ holds
(b₃ ^ b₄) .: b₁ = b₃ .: b₁

proof end;

Lemma8: for b₁ being Nat
for b₂ being non empty doubleLoopStr
for b₃, b₄ being FinSequence of the carrier of b₂ st b₁ <> 0 & b₁ <= len b₃ holds
(b₄ ^ b₃) .: ((len b₄) + b₁) = b₃ .: b₁

proof end;

Lemma9: for b₁ being non empty doubleLoopStr
for b₂ being Scalar of b₁ st b₂ is_a_square holds
<*b₂*> is_a_Product_of_squares

proof end;

Lemma10: for b₁ being non empty doubleLoopStr
for b₂ being Scalar of b₁ st b₂ is_a_square holds
b₂ is_a_product_of_squares

proof end;

Lemma11: for b₁ being non empty doubleLoopStr
for b₂ being Scalar of b₁ st b₂ is_a_square holds
<*b₂*> is_an_Amalgam_of_squares

proof end;

Lemma12: for b₁ being non empty doubleLoopStr
for b₂ being Scalar of b₁ st b₂ is_a_square holds
b₂ is_an_amalgam_of_squares

proof end;

Lemma13: for b₁ being non empty doubleLoopStr
for b₂, b₃ being FinSequence of the carrier of b₁ st b₂ is_an_Amalgam_of_squares & b₃ is_an_Amalgam_of_squares holds
b₂ ^ b₃ is_an_Amalgam_of_squares

proof end;

Lemma14: for b₁ being non empty doubleLoopStr
for b₂, b₃ being FinSequence of the carrier of b₁ st b₂ is_a_generation_from_squares & b₃ is_a_generation_from_squares holds
b₂ ^ b₃ is_a_generation_from_squares

proof end;

Lemma15: for b₁ being non empty doubleLoopStr
for b₂ being Scalar of b₁
for b₃ being FinSequence of the carrier of b₁ st b₃ is_a_generation_from_squares & b₂ is_a_square holds
b₃ ^ <*b₂*> is_a_generation_from_squares

proof end;

Lemma16: for b₁ being non empty doubleLoopStr
for b₂ being Scalar of b₁
for b₃ being FinSequence of the carrier of b₁ st b₃ is_a_generation_from_squares & b₂ is_an_amalgam_of_squares holds
b₃ ^ <*b₂*> is_a_generation_from_squares

proof end;

Lemma17: for b₁, b₂ being Nat
for b₃ being non empty doubleLoopStr
for b₄ being FinSequence of the carrier of b₃ st b₄ is_an_Amalgam_of_squares & b₁ <> 0 & b₁ <= len b₄ & b₂ <> 0 & b₂ <= len b₄ holds
b₄ ^ <*((b₄ .: b₁) * (b₄ .: b₂))*> is_an_Amalgam_of_squares

proof end;

Lemma18: for b₁, b₂ being Nat
for b₃ being non empty doubleLoopStr
for b₄ being FinSequence of the carrier of b₃ st b₄ is_a_generation_from_squares & b₁ <> 0 & b₁ <= len b₄ & b₂ <> 0 & b₂ <= len b₄ holds
b₄ ^ <*((b₄ .: b₁) * (b₄ .: b₂))*> is_a_generation_from_squares

proof end;

Lemma19: for b₁ being non empty doubleLoopStr
for b₂ being Scalar of b₁
for b₃ being FinSequence of the carrier of b₁ st b₃ is_a_Product_of_squares & b₂ is_a_square holds
b₃ ^ <*((b₃ .: (len b₃)) * b₂)*> is_a_Product_of_squares

proof end;

Lemma20: for b₁ being non empty doubleLoopStr
for b₂ being Scalar of b₁
for b₃ being FinSequence of the carrier of b₁ st b₃ is_a_generation_from_squares & b₂ is_a_square holds
(b₃ ^ <*b₂*>) ^ <*((b₃ .: (len b₃)) * b₂)*> is_a_generation_from_squares

proof end;

Lemma21: for b₁ being non empty doubleLoopStr
for b₂ being Scalar of b₁
for b₃ being FinSequence of the carrier of b₁ st b₃ is_a_generation_from_squares & b₂ is_an_amalgam_of_squares holds
(b₃ ^ <*b₂*>) ^ <*((b₃ .: (len b₃)) * b₂)*> is_a_generation_from_squares

proof end;

Lemma22: for b₁ being non empty doubleLoopStr
for b₂, b₃ being FinSequence of the carrier of b₁ st b₂ is_an_Amalgam_of_squares & b₃ is_an_Amalgam_of_squares holds
(b₂ ^ b₃) ^ <*((b₂ .: (len b₂)) * (b₃ .: (len b₃)))*> is_an_Amalgam_of_squares

proof end;

Lemma23: for b₁ being non empty doubleLoopStr
for b₂, b₃ being FinSequence of the carrier of b₁ st b₂ is_a_generation_from_squares & b₃ is_a_generation_from_squares holds
(b₂ ^ b₃) ^ <*((b₂ .: (len b₂)) * (b₃ .: (len b₃)))*> is_a_generation_from_squares

proof end;

theorem Th1: :: O_RING_3:1

for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_a_square & b₃ is_a_square holds
b₂ * b₃ is_a_product_of_squares

proof end;

theorem Th2: :: O_RING_3:2

for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_a_product_of_squares & b₃ is_a_square holds
b₂ * b₃ is_a_product_of_squares

proof end;

Lemma24: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_a_square & b₃ is_a_product_of_squares holds
b₂ * b₃ is_an_amalgam_of_squares

proof end;

Lemma25: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_a_square & b₃ is_an_amalgam_of_squares holds
b₂ * b₃ is_an_amalgam_of_squares

proof end;

theorem Th3: :: O_RING_3:3

for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st ( ( b₂ is_a_square & b₃ is_a_product_of_squares ) or ( b₂ is_a_square & b₃ is_an_amalgam_of_squares ) ) holds
b₂ * b₃ is_an_amalgam_of_squares by Lemma24, Lemma25;

Lemma26: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_a_product_of_squares & b₃ is_a_product_of_squares holds
b₂ * b₃ is_an_amalgam_of_squares

proof end;

Lemma27: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_a_product_of_squares & b₃ is_an_amalgam_of_squares holds
b₂ * b₃ is_an_amalgam_of_squares

proof end;

theorem Th4: :: O_RING_3:4

for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st ( ( b₂ is_a_product_of_squares & b₃ is_a_product_of_squares ) or ( b₂ is_a_product_of_squares & b₃ is_an_amalgam_of_squares ) ) holds
b₂ * b₃ is_an_amalgam_of_squares by Lemma26, Lemma27;

Lemma28: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_an_amalgam_of_squares & b₃ is_a_square holds
b₂ * b₃ is_an_amalgam_of_squares

proof end;

Lemma29: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_an_amalgam_of_squares & b₃ is_a_product_of_squares holds
b₂ * b₃ is_an_amalgam_of_squares

proof end;

Lemma30: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_an_amalgam_of_squares & b₃ is_an_amalgam_of_squares holds
b₂ * b₃ is_an_amalgam_of_squares

proof end;

theorem Th5: :: O_RING_3:5

for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st ( ( b₂ is_an_amalgam_of_squares & b₃ is_a_square ) or ( b₂ is_an_amalgam_of_squares & b₃ is_a_product_of_squares ) or ( b₂ is_an_amalgam_of_squares & b₃ is_an_amalgam_of_squares ) ) holds
b₂ * b₃ is_an_amalgam_of_squares by Lemma28, Lemma29, Lemma30;

Lemma31: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_a_square & b₃ is_a_sum_of_squares holds
b₂ * b₃ is_generated_from_squares

proof end;

Lemma32: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_a_square & b₃ is_a_sum_of_products_of_squares holds
b₂ * b₃ is_generated_from_squares

proof end;

Lemma33: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_a_square & b₃ is_a_sum_of_amalgams_of_squares holds
b₂ * b₃ is_generated_from_squares

proof end;

Lemma34: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_a_square & b₃ is_generated_from_squares holds
b₂ * b₃ is_generated_from_squares

proof end;

theorem Th6: :: O_RING_3:6

for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st ( ( b₂ is_a_square & b₃ is_a_sum_of_squares ) or ( b₂ is_a_square & b₃ is_a_sum_of_products_of_squares ) or ( b₂ is_a_square & b₃ is_a_sum_of_amalgams_of_squares ) or ( b₂ is_a_square & b₃ is_generated_from_squares ) ) holds
b₂ * b₃ is_generated_from_squares by Lemma31, Lemma32, Lemma33, Lemma34;

Lemma35: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_a_sum_of_squares & b₃ is_a_square holds
b₂ * b₃ is_generated_from_squares

proof end;

Lemma36: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_a_sum_of_squares & b₃ is_a_sum_of_squares holds
b₂ * b₃ is_generated_from_squares

proof end;

Lemma37: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_a_sum_of_squares & b₃ is_a_product_of_squares holds
b₂ * b₃ is_generated_from_squares

proof end;

Lemma38: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_a_sum_of_squares & b₃ is_a_sum_of_products_of_squares holds
b₂ * b₃ is_generated_from_squares

proof end;

Lemma39: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_a_sum_of_squares & b₃ is_an_amalgam_of_squares holds
b₂ * b₃ is_generated_from_squares

proof end;

Lemma40: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_a_sum_of_squares & b₃ is_a_sum_of_amalgams_of_squares holds
b₂ * b₃ is_generated_from_squares

proof end;

Lemma41: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_a_sum_of_squares & b₃ is_generated_from_squares holds
b₂ * b₃ is_generated_from_squares

proof end;

theorem Th7: :: O_RING_3:7

Lemma42: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_a_product_of_squares & b₃ is_a_sum_of_squares holds
b₂ * b₃ is_generated_from_squares

proof end;

Lemma43: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_a_product_of_squares & b₃ is_a_sum_of_products_of_squares holds
b₂ * b₃ is_generated_from_squares

proof end;

Lemma44: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_a_product_of_squares & b₃ is_a_sum_of_amalgams_of_squares holds
b₂ * b₃ is_generated_from_squares

proof end;

Lemma45: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_a_product_of_squares & b₃ is_generated_from_squares holds
b₂ * b₃ is_generated_from_squares

proof end;

theorem Th8: :: O_RING_3:8

for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st ( ( b₂ is_a_product_of_squares & b₃ is_a_sum_of_squares ) or ( b₂ is_a_product_of_squares & b₃ is_a_sum_of_products_of_squares ) or ( b₂ is_a_product_of_squares & b₃ is_a_sum_of_amalgams_of_squares ) or ( b₂ is_a_product_of_squares & b₃ is_generated_from_squares ) ) holds
b₂ * b₃ is_generated_from_squares by Lemma42, Lemma43, Lemma44, Lemma45;

Lemma46: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_a_sum_of_products_of_squares & b₃ is_a_square holds
b₂ * b₃ is_generated_from_squares

proof end;

Lemma47: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_a_sum_of_products_of_squares & b₃ is_a_sum_of_squares holds
b₂ * b₃ is_generated_from_squares

proof end;

Lemma48: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_a_sum_of_products_of_squares & b₃ is_a_product_of_squares holds
b₂ * b₃ is_generated_from_squares

proof end;

Lemma49: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_a_sum_of_products_of_squares & b₃ is_a_sum_of_products_of_squares holds
b₂ * b₃ is_generated_from_squares

proof end;

Lemma50: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_a_sum_of_products_of_squares & b₃ is_an_amalgam_of_squares holds
b₂ * b₃ is_generated_from_squares

proof end;

Lemma51: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_a_sum_of_products_of_squares & b₃ is_a_sum_of_amalgams_of_squares holds
b₂ * b₃ is_generated_from_squares

proof end;

Lemma52: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_a_sum_of_products_of_squares & b₃ is_generated_from_squares holds
b₂ * b₃ is_generated_from_squares

proof end;

theorem Th9: :: O_RING_3:9

Lemma53: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_an_amalgam_of_squares & b₃ is_a_sum_of_squares holds
b₂ * b₃ is_generated_from_squares

proof end;

Lemma54: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_an_amalgam_of_squares & b₃ is_a_sum_of_products_of_squares holds
b₂ * b₃ is_generated_from_squares

proof end;

Lemma55: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_an_amalgam_of_squares & b₃ is_a_sum_of_amalgams_of_squares holds
b₂ * b₃ is_generated_from_squares

proof end;

Lemma56: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_an_amalgam_of_squares & b₃ is_generated_from_squares holds
b₂ * b₃ is_generated_from_squares

proof end;

theorem Th10: :: O_RING_3:10

for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st ( ( b₂ is_an_amalgam_of_squares & b₃ is_a_sum_of_squares ) or ( b₂ is_an_amalgam_of_squares & b₃ is_a_sum_of_products_of_squares ) or ( b₂ is_an_amalgam_of_squares & b₃ is_a_sum_of_amalgams_of_squares ) or ( b₂ is_an_amalgam_of_squares & b₃ is_generated_from_squares ) ) holds
b₂ * b₃ is_generated_from_squares by Lemma53, Lemma54, Lemma55, Lemma56;

Lemma57: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_a_sum_of_amalgams_of_squares & b₃ is_a_square holds
b₂ * b₃ is_generated_from_squares

proof end;

Lemma58: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_a_sum_of_amalgams_of_squares & b₃ is_a_sum_of_squares holds
b₂ * b₃ is_generated_from_squares

proof end;

Lemma59: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_a_sum_of_amalgams_of_squares & b₃ is_a_product_of_squares holds
b₂ * b₃ is_generated_from_squares

proof end;

Lemma60: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_a_sum_of_amalgams_of_squares & b₃ is_a_sum_of_products_of_squares holds
b₂ * b₃ is_generated_from_squares

proof end;

Lemma61: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_a_sum_of_amalgams_of_squares & b₃ is_an_amalgam_of_squares holds
b₂ * b₃ is_generated_from_squares

proof end;

Lemma62: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_a_sum_of_amalgams_of_squares & b₃ is_a_sum_of_amalgams_of_squares holds
b₂ * b₃ is_generated_from_squares

proof end;

Lemma63: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_a_sum_of_amalgams_of_squares & b₃ is_generated_from_squares holds
b₂ * b₃ is_generated_from_squares

proof end;

theorem Th11: :: O_RING_3:11

for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st ( ( b₂ is_a_sum_of_amalgams_of_squares & b₃ is_a_square ) or ( b₂ is_a_sum_of_amalgams_of_squares & b₃ is_a_sum_of_squares ) or ( b₂ is_a_sum_of_amalgams_of_squares & b₃ is_a_product_of_squares ) or ( b₂ is_a_sum_of_amalgams_of_squares & b₃ is_a_sum_of_products_of_squares ) or ( b₂ is_a_sum_of_amalgams_of_squares & b₃ is_an_amalgam_of_squares ) or ( b₂ is_a_sum_of_amalgams_of_squares & b₃ is_a_sum_of_amalgams_of_squares ) or ( b₂ is_a_sum_of_amalgams_of_squares & b₃ is_generated_from_squares ) ) holds
b₂ * b₃ is_generated_from_squares by Lemma57, Lemma58, Lemma59, Lemma60, Lemma61, Lemma62, Lemma63;

Lemma64: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_generated_from_squares & b₃ is_a_square holds
b₂ * b₃ is_generated_from_squares

proof end;

Lemma65: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_generated_from_squares & b₃ is_an_amalgam_of_squares holds
b₂ * b₃ is_generated_from_squares

proof end;

Lemma66: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_generated_from_squares & b₃ is_generated_from_squares holds
b₂ * b₃ is_generated_from_squares

proof end;

Lemma67: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_generated_from_squares & b₃ is_a_sum_of_squares holds
b₂ * b₃ is_generated_from_squares

proof end;

Lemma68: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_generated_from_squares & b₃ is_a_product_of_squares holds
b₂ * b₃ is_generated_from_squares

proof end;

Lemma69: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_generated_from_squares & b₃ is_a_sum_of_products_of_squares holds
b₂ * b₃ is_generated_from_squares

proof end;

Lemma70: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Scalar of b₁ st b₂ is_generated_from_squares & b₃ is_a_sum_of_amalgams_of_squares holds
b₂ * b₃ is_generated_from_squares

proof end;

theorem Th12: :: O_RING_3:12