:: HILBASIS semantic presentation

theorem Th1: :: HILBASIS:1

for b₁, b₂ being FinSequence
for b₃ being Function st (rng b₁) \/ (rng b₂) c= dom b₃ holds
ex b₄, b₅ being FinSequence st
( b₄ = b₃ * b₁ & b₅ = b₃ * b₂ & b₃ * (b₁ ^ b₂) = b₄ ^ b₅ )

proof end;

theorem Th2: :: HILBASIS:2

for b₁ being bag of 0 holds decomp b₁ = <*<*{} ,{} *>*>

proof end;

theorem Th3: :: HILBASIS:3

for b₁, b₂ being Nat
for b₃ being bag of b₂ st b₁ <= b₂ holds
b₃ | b₁ is Element of Bags b₁

proof end;

theorem Th4: :: HILBASIS:4

for b₁, b₂ being set
for b₃, b₄ being bag of b₂
for b₅, b₆ being bag of b₁ st b₅ = b₃ | b₁ & b₆ = b₄ | b₁ & b₃ divides b₄ holds
b₅ divides b₆

proof end;

theorem Th5: :: HILBASIS:5

for b₁, b₂ being set
for b₃, b₄ being bag of b₂
for b₅, b₆ being bag of b₁ st b₅ = b₃ | b₁ & b₆ = b₄ | b₁ holds
( (b₃ -' b₄) | b₁ = b₅ -' b₆ & (b₃ + b₄) | b₁ = b₅ + b₆ )

proof end;

definition

let c₁, c₂ be Nat;
let c₃ be bag of c₁;
func c₃ bag_extend c₂ -> Element of Bags (a₁ + 1) means :Def1: :: HILBASIS:def 1
( a₄ | a₁ = a₃ & a₄ . a₁ = a₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines bag_extend HILBASIS:def 1 :

theorem Th6: :: HILBASIS:6

for b₁ being Nat holds EmptyBag (b₁ + 1) = (EmptyBag b₁) bag_extend 0

proof end;

theorem Th7: :: HILBASIS:7

for b₁ being Ordinal
for b₂, b₃ being bag of b₁ holds
( b₃ in rng (divisors b₂) iff b₃ divides b₂ )

proof end;

definition

let c₁ be set ;
let c₂ be Element of c₁;
func UnitBag c₂ -> Element of Bags a₁ equals :: HILBASIS:def 2
(EmptyBag a₁) +* a₂,1;
coherence by POLYNOM1:def 14;

end;

:: deftheorem Def2 defines UnitBag HILBASIS:def 2 :

theorem Th8: :: HILBASIS:8

for b₁ being non empty set
for b₂ being Element of b₁ holds support (UnitBag b₂) = {b₂}

proof end;

theorem Th9: :: HILBASIS:9

for b₁ being non empty set
for b₂ being Element of b₁ holds
( (UnitBag b₂) . b₂ = 1 & ( for b₃ being Element of b₁ st b₂ <> b₃ holds
(UnitBag b₂) . b₃ = 0 ) )

proof end;

theorem Th10: :: HILBASIS:10

for b₁ being non empty set
for b₂, b₃ being Element of b₁ st UnitBag b₂ = UnitBag b₃ holds
b₂ = b₃

proof end;

theorem Th11: :: HILBASIS:11

for b₁ being non empty Ordinal
for b₂ being Element of b₁
for b₃ being non empty unital non trivial doubleLoopStr
for b₄ being Function of b₁,b₃ holds eval (UnitBag b₂),b₄ = b₄ . b₂

proof end;

definition

let c₁ be set ;
let c₂ be Element of c₁;
let c₃ be non empty unital multLoopStr_0 ;
func 1_1 c₂,c₃ -> Series of a₁,a₃ equals :: HILBASIS:def 3
(0_ a₁,a₃) +* (UnitBag a₂),(1. a₃);
coherence ;

end;

:: deftheorem Def3 defines 1_1 HILBASIS:def 3 :

theorem Th12: :: HILBASIS:12

for b₁ being set
for b₂ being non empty unital non trivial doubleLoopStr
for b₃ being Element of b₁ holds
( (1_1 b₃,b₂) . (UnitBag b₃) = 1. b₂ & ( for b₄ being bag of b₁ st b₄ <> UnitBag b₃ holds
(1_1 b₃,b₂) . b₄ = 0. b₂ ) )

proof end;

theorem Th13: :: HILBASIS:13

for b₁ being set
for b₂ being Element of b₁
for b₃ being non empty unital add-associative right_zeroed right_complementable right-distributive non trivial doubleLoopStr holds Support (1_1 b₂,b₃) = {(UnitBag b₂)}

proof end;

registration

let c₁ be Ordinal;
let c₂ be Element of c₁;
let c₃ be non empty unital add-associative right_zeroed right_complementable right-distributive non trivial doubleLoopStr ;
cluster 1_1 a₂,a₃ -> finite-Support ;
coherence

proof end;

end;

theorem Th14: :: HILBASIS:14

for b₁ being non empty unital add-associative right_zeroed right_complementable right-distributive non trivial doubleLoopStr
for b₂ being non empty set
for b₃, b₄ being Element of b₂ st 1_1 b₃,b₁ = 1_1 b₄,b₁ holds
b₃ = b₄

proof end;

theorem Th15: :: HILBASIS:15

for b₁ being non empty add-associative right_zeroed right_complementable distributive doubleLoopStr
for b₂ being Element of (Polynom-Ring b₁)
for b₃ being sequence of b₁ st b₂ = b₃ holds
- b₂ = - b₃

proof end;

theorem Th16: :: HILBASIS:16

for b₁ being non empty add-associative right_zeroed right_complementable distributive doubleLoopStr
for b₂, b₃ being Element of (Polynom-Ring b₁)
for b₄, b₅ being sequence of b₁ st b₂ = b₄ & b₃ = b₅ holds
b₂ - b₃ = b₄ - b₅

proof end;

definition

let c₁ be non empty unital add-associative right_zeroed right_complementable distributive doubleLoopStr ;
let c₂ be non empty Subset of (Polynom-Ring c₁);
func minlen c₂ -> non empty Subset of a₂ equals :: HILBASIS:def 4
{ b₁ where B is Element of a₂ : for b₁, b₂ being Polynomial of a₁ st b₂ = b₁ & b₃ in a₂ holds
len b₂ <= len b₃ } ;
coherence

proof end;

end;

:: deftheorem Def4 defines minlen HILBASIS:def 4 :

theorem Th17: :: HILBASIS:17

for b₁ being non empty unital add-associative right_zeroed right_complementable distributive doubleLoopStr
for b₂ being non empty Subset of (Polynom-Ring b₁)
for b₃, b₄ being Polynomial of b₁ st b₃ in minlen b₂ & b₄ in b₂ holds
( b₃ in b₂ & len b₃ <= len b₄ )

proof end;

definition

let c₁ be non empty unital add-associative right_zeroed right_complementable distributive doubleLoopStr ;
let c₂ be Nat;
let c₃ be Element of c₁;
func monomial c₃,c₂ -> Polynomial of a₁ means :Def5: :: HILBASIS:def 5
for b₁ being Nat holds
( ( b₁ = a₂ implies a₄ . b₁ = a₃ ) & ( b₁ <> a₂ implies a₄ . b₁ = 0. a₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines monomial HILBASIS:def 5 :

theorem Th18: :: HILBASIS:18

for b₁ being non empty unital add-associative right_zeroed right_complementable distributive doubleLoopStr
for b₂ being Nat
for b₃ being Element of b₁ holds
( ( b₃ <> 0. b₁ implies len (monomial b₃,b₂) = b₂ + 1 ) & ( b₃ = 0. b₁ implies len (monomial b₃,b₂) = 0 ) & len (monomial b₃,b₂) <= b₂ + 1 )

proof end;

theorem Th19: :: HILBASIS:19

for b₁ being non empty unital add-associative right_zeroed right_complementable distributive doubleLoopStr
for b₂, b₃ being Nat
for b₄ being Element of b₁
for b₅ being Polynomial of b₁ holds ((monomial b₄,b₂) *' b₅) . (b₃ + b₂) = b₄ * (b₅ . b₃)

proof end;

theorem Th20: :: HILBASIS:20

for b₁ being non empty unital add-associative right_zeroed right_complementable distributive doubleLoopStr
for b₂, b₃ being Nat
for b₄ being Element of b₁
for b₅ being Polynomial of b₁ holds (b₅ *' (monomial b₄,b₂)) . (b₃ + b₂) = (b₅ . b₃) * b₄

proof end;

theorem Th21: :: HILBASIS:21

for b₁ being non empty unital add-associative right_zeroed right_complementable distributive doubleLoopStr
for b₂, b₃ being Polynomial of b₁ holds len (b₂ *' b₃) <= ((len b₂) + (len b₃)) -' 1

proof end;

theorem Th22: :: HILBASIS:22

for b₁, b₂ being non empty doubleLoopStr
for b₃ being Ideal of b₁
for b₄ being Function of b₁,b₂ st b₄ is RingIsomorphism holds
b₄ .: b₃ is Ideal of b₂

proof end;

theorem Th23: :: HILBASIS:23

for b₁, b₂ being non empty add-associative right_zeroed right_complementable doubleLoopStr
for b₃ being Function of b₁,b₂ st b₃ is RingHomomorphism holds
b₃ . (0. b₁) = 0. b₂

proof end;

theorem Th24: :: HILBASIS:24

for b₁, b₂ being non empty add-associative right_zeroed right_complementable doubleLoopStr
for b₃ being non empty Subset of b₁
for b₄ being non empty Subset of b₂
for b₅ being Function of b₁,b₂
for b₆ being LinearCombination of b₃
for b₇ being LinearCombination of b₄
for b₈ being FinSequence of [:the carrier of b₁,the carrier of b₁,the carrier of b₁:] st b₅ is RingHomomorphism & len b₆ = len b₇ & b₈ represents b₆ & ( for b₉ being set st b₉ in dom b₇ holds
b₇ . b₉ = ((b₅ . ((b₈ /. b₉) `1 )) * (b₅ . ((b₈ /. b₉) `2 ))) * (b₅ . ((b₈ /. b₉) `3 )) ) holds
b₅ . (Sum b₆) = Sum b₇

proof end;

theorem Th25: :: HILBASIS:25

for b₁, b₂ being non empty doubleLoopStr
for b₃ being Function of b₁,b₂ st b₃ is RingIsomorphism holds
ex b₄ being Function of b₂,b₁ st
( b₄ is RingIsomorphism & b₄ = b₃ " )

proof end;

theorem Th26: :: HILBASIS:26

for b₁, b₂ being non empty unital associative Abelian add-associative right_zeroed right_complementable distributive doubleLoopStr
for b₃ being non empty Subset of b₁
for b₄ being Function of b₁,b₂ st b₄ is RingIsomorphism holds
b₄ .: (b₃ -Ideal ) = (b₄ .: b₃) -Ideal

proof end;

theorem Th27: :: HILBASIS:27

for b₁, b₂ being non empty unital associative Abelian add-associative right_zeroed right_complementable distributive doubleLoopStr
for b₃ being Function of b₁,b₂ st b₃ is RingIsomorphism & b₁ is Noetherian holds
b₂ is Noetherian

proof end;

theorem Th28: :: HILBASIS:28

for b₁ being non empty unital associative Abelian add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr ex b₂ being Function of b₁,(Polynom-Ring 0,b₁) st b₂ is RingIsomorphism

proof end;

theorem Th29: :: HILBASIS:29

for b₁ being non empty unital add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for b₂ being Nat
for b₃ being bag of b₂
for b₄ being Polynomial of b₂,b₁
for b₅ being FinSequence of the carrier of (Polynom-Ring b₂,b₁) st b₄ = Sum b₅ holds
ex b₆ being Function of the carrier of (Polynom-Ring b₂,b₁),the carrier of b₁ st
( ( for b₇ being Polynomial of b₂,b₁ holds b₆ . b₇ = b₇ . b₃ ) & b₄ . b₃ = Sum (b₆ * b₅) )

proof end;

definition