:: HILBASIS semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: HILBASIS:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being FinSequence
for f being Function st (rng A) \/ (rng B) c= dom f holds
ex fA, fB being FinSequence st
( fA = f * A & fB = f * B & f * (A ^ B) = fA ^ fB )
proof end;

theorem Th2: :: HILBASIS:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for b being bag of 0 holds decomp b = <*<*{} ,{} *>*>
proof end;

theorem Th3: :: HILBASIS:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j being Nat
for b being bag of j st i <= j holds
b | i is Element of Bags i
proof end;

theorem Th4: :: HILBASIS:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j being set
for b1, b2 being bag of j
for b1', b2' being bag of i st b1' = b1 | i & b2' = b2 | i & b1 divides b2 holds
b1' divides b2'
proof end;

theorem Th5: :: HILBASIS:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j being set
for b1, b2 being bag of j
for b1', b2' being bag of i st b1' = b1 | i & b2' = b2 | i holds
( (b1 -' b2) | i = b1' -' b2' & (b1 + b2) | i = b1' + b2' )
proof end;

definition
let n, k be Nat;
let b be bag of n;
func b bag_extend k -> Element of Bags (n + 1) means :Def1: :: HILBASIS:def 1
( it | n = b & it . n = k );
existence
ex b1 being Element of Bags (n + 1) st
( b1 | n = b & b1 . n = k )
proof end;
uniqueness
for b1, b2 being Element of Bags (n + 1) st b1 | n = b & b1 . n = k & b2 | n = b & b2 . n = k holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines bag_extend HILBASIS:def 1 :
for n, k being Nat
for b being bag of n
for b4 being Element of Bags (n + 1) holds
( b4 = b bag_extend k iff ( b4 | n = b & b4 . n = k ) );

theorem Th6: :: HILBASIS:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds EmptyBag (n + 1) = (EmptyBag n) bag_extend 0
proof end;

theorem Th7: :: HILBASIS:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for b, b1 being bag of n holds
( b1 in rng (divisors b) iff b1 divides b )
proof end;

definition
let X be set ;
let x be Element of X;
func UnitBag x -> Element of Bags X equals :: HILBASIS:def 2
(EmptyBag X) +* x,1;
coherence
(EmptyBag X) +* x,1 is Element of Bags X
by POLYNOM1:def 14;
end;

:: deftheorem defines UnitBag HILBASIS:def 2 :
for X being set
for x being Element of X holds UnitBag x = (EmptyBag X) +* x,1;

theorem Th8: :: HILBASIS:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for x being Element of X holds support (UnitBag x) = {x}
proof end;

theorem Th9: :: HILBASIS:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for x being Element of X holds
( (UnitBag x) . x = 1 & ( for y being Element of X st x <> y holds
(UnitBag x) . y = 0 ) )
proof end;

theorem Th10: :: HILBASIS:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for x1, x2 being Element of X st UnitBag x1 = UnitBag x2 holds
x1 = x2
proof end;

theorem Th11: :: HILBASIS:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty Ordinal
for x being Element of X
for L being non empty unital non trivial doubleLoopStr
for e being Function of X,L holds eval (UnitBag x),e = e . x
proof end;

definition
let X be set ;
let x be Element of X;
let L be non empty unital multLoopStr_0 ;
func 1_1 x,L -> Series of X,L equals :: HILBASIS:def 3
(0_ X,L) +* (UnitBag x),(1. L);
coherence
(0_ X,L) +* (UnitBag x),(1. L) is Series of X,L
;
end;

:: deftheorem defines 1_1 HILBASIS:def 3 :
for X being set
for x being Element of X
for L being non empty unital multLoopStr_0 holds 1_1 x,L = (0_ X,L) +* (UnitBag x),(1. L);

theorem Th12: :: HILBASIS:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for L being non empty unital non trivial doubleLoopStr
for x being Element of X holds
( (1_1 x,L) . (UnitBag x) = 1. L & ( for b being bag of X st b <> UnitBag x holds
(1_1 x,L) . b = 0. L ) )
proof end;

theorem Th13: :: HILBASIS:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for x being Element of X
for L being non empty unital add-associative right_zeroed right_complementable right-distributive non trivial doubleLoopStr holds Support (1_1 x,L) = {(UnitBag x)}
proof end;

registration
let X be Ordinal;
let x be Element of X;
let L be non empty unital add-associative right_zeroed right_complementable right-distributive non trivial doubleLoopStr ;
cluster 1_1 x,L -> finite-Support ;
coherence
1_1 x,L is finite-Support
proof end;
end;

theorem Th14: :: HILBASIS:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty unital add-associative right_zeroed right_complementable right-distributive non trivial doubleLoopStr
for X being non empty set
for x1, x2 being Element of X st 1_1 x1,L = 1_1 x2,L holds
x1 = x2
proof end;

theorem Th15: :: HILBASIS:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty add-associative right_zeroed right_complementable distributive doubleLoopStr
for x being Element of (Polynom-Ring L)
for p being sequence of L st x = p holds
- x = - p
proof end;

theorem Th16: :: HILBASIS:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty add-associative right_zeroed right_complementable distributive doubleLoopStr
for x, y being Element of (Polynom-Ring L)
for p, q being sequence of L st x = p & y = q holds
x - y = p - q
proof end;

definition
let L be non empty unital add-associative right_zeroed right_complementable distributive doubleLoopStr ;
let I be non empty Subset of (Polynom-Ring L);
func minlen I -> non empty Subset of I equals :: HILBASIS:def 4
{ x where x is Element of I : for x', y' being Polynomial of L st x' = x & y' in I holds
len x' <= len y'
}
;
coherence
{ x where x is Element of I : for x', y' being Polynomial of L st x' = x & y' in I holds
len x' <= len y'
}
is non empty Subset of I
proof end;
end;

:: deftheorem defines minlen HILBASIS:def 4 :
for L being non empty unital add-associative right_zeroed right_complementable distributive doubleLoopStr
for I being non empty Subset of (Polynom-Ring L) holds minlen I = { x where x is Element of I : for x', y' being Polynomial of L st x' = x & y' in I holds
len x' <= len y'
}
;

theorem Th17: :: HILBASIS:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty unital add-associative right_zeroed right_complementable distributive doubleLoopStr
for I being non empty Subset of (Polynom-Ring L)
for i1, i2 being Polynomial of L st i1 in minlen I & i2 in I holds
( i1 in I & len i1 <= len i2 )
proof end;

definition
let L be non empty unital add-associative right_zeroed right_complementable distributive doubleLoopStr ;
let n be Nat;
let a be Element of L;
func monomial a,n -> Polynomial of L means :Def5: :: HILBASIS:def 5
for x being Nat holds
( ( x = n implies it . x = a ) & ( x <> n implies it . x = 0. L ) );
existence
ex b1 being Polynomial of L st
for x being Nat holds
( ( x = n implies b1 . x = a ) & ( x <> n implies b1 . x = 0. L ) )
proof end;
uniqueness
for b1, b2 being Polynomial of L st ( for x being Nat holds
( ( x = n implies b1 . x = a ) & ( x <> n implies b1 . x = 0. L ) ) ) & ( for x being Nat holds
( ( x = n implies b2 . x = a ) & ( x <> n implies b2 . x = 0. L ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines monomial HILBASIS:def 5 :
for L being non empty unital add-associative right_zeroed right_complementable distributive doubleLoopStr
for n being Nat
for a being Element of L
for b4 being Polynomial of L holds
( b4 = monomial a,n iff for x being Nat holds
( ( x = n implies b4 . x = a ) & ( x <> n implies b4 . x = 0. L ) ) );

theorem Th18: :: HILBASIS:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty unital add-associative right_zeroed right_complementable distributive doubleLoopStr
for n being Nat
for a being Element of L holds
( ( a <> 0. L implies len (monomial a,n) = n + 1 ) & ( a = 0. L implies len (monomial a,n) = 0 ) & len (monomial a,n) <= n + 1 )
proof end;

theorem Th19: :: HILBASIS:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty unital add-associative right_zeroed right_complementable distributive doubleLoopStr
for n, x being Nat
for a being Element of L
for p being Polynomial of L holds ((monomial a,n) *' p) . (x + n) = a * (p . x)
proof end;

theorem Th20: :: HILBASIS:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty unital add-associative right_zeroed right_complementable distributive doubleLoopStr
for n, x being Nat
for a being Element of L
for p being Polynomial of L holds (p *' (monomial a,n)) . (x + n) = (p . x) * a
proof end;

theorem Th21: :: HILBASIS:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty unital add-associative right_zeroed right_complementable distributive doubleLoopStr
for p, q being Polynomial of L holds len (p *' q) <= ((len p) + (len q)) -' 1
proof end;

theorem Th22: :: HILBASIS:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S being non empty doubleLoopStr
for I being Ideal of R
for P being Function of R,S st P is RingIsomorphism holds
P .: I is Ideal of S
proof end;

theorem Th23: :: HILBASIS:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S being non empty add-associative right_zeroed right_complementable doubleLoopStr
for f being Function of R,S st f is RingHomomorphism holds
f . (0. R) = 0. S
proof end;

theorem Th24: :: HILBASIS:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S being non empty add-associative right_zeroed right_complementable doubleLoopStr
for F being non empty Subset of R
for G being non empty Subset of S
for P being Function of R,S
for lc being LinearCombination of F
for LC being LinearCombination of G
for E being FinSequence of [:the carrier of R,the carrier of R,the carrier of R:] st P is RingHomomorphism & len lc = len LC & E represents lc & ( for i being set st i in dom LC holds
LC . i = ((P . ((E /. i) `1 )) * (P . ((E /. i) `2 ))) * (P . ((E /. i) `3 )) ) holds
P . (Sum lc) = Sum LC
proof end;

theorem Th25: :: HILBASIS:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S being non empty doubleLoopStr
for P being Function of R,S st P is RingIsomorphism holds
ex P1 being Function of S,R st
( P1 is RingIsomorphism & P1 = P " )
proof end;

theorem Th26: :: HILBASIS:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S being non empty unital associative Abelian add-associative right_zeroed right_complementable distributive doubleLoopStr
for F being non empty Subset of R
for P being Function of R,S st P is RingIsomorphism holds
P .: (F -Ideal ) = (P .: F) -Ideal
proof end;

theorem Th27: :: HILBASIS:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S being non empty unital associative Abelian add-associative right_zeroed right_complementable distributive doubleLoopStr
for P being Function of R,S st P is RingIsomorphism & R is Noetherian holds
S is Noetherian
proof end;

theorem Th28: :: HILBASIS:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty unital associative Abelian add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr ex P being Function of R,(Polynom-Ring 0,R) st P is RingIsomorphism
proof end;

theorem Th29: :: HILBASIS:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty unital add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for n being Nat
for b being bag of n
for p1 being Polynomial of n,R
for F being FinSequence of the carrier of (Polynom-Ring n,R) st p1 = Sum F holds
ex g being Function of the carrier of (Polynom-Ring n,R),the carrier of R st
( ( for p being Polynomial of n,R holds g . p = p . b ) & p1 . b = Sum (g * F) )
proof end;

definition
let R be non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr ;
let n be Nat;
func upm n,R -> Function of (Polynom-Ring (Polynom-Ring n,R)),(Polynom-Ring (n + 1),R) means :Def6: :: HILBASIS:def 6
for p1 being Polynomial of (Polynom-Ring n,R)
for p2 being Polynomial of n,R
for p3 being Polynomial of (n + 1),R
for b being bag of n + 1 st p3 = it . p1 & p2 = p1 . (b . n) holds
p3 . b = p2 . (b | n);
existence
ex b1 being Function of (Polynom-Ring (Polynom-Ring n,R)),(Polynom-Ring (n + 1),R) st
for p1 being Polynomial of (Polynom-Ring n,R)
for p2 being Polynomial of n,R
for p3 being Polynomial of (n + 1),R
for b being bag of n + 1 st p3 = b1 . p1 & p2 = p1 . (b . n) holds
p3 . b = p2 . (b | n)
proof end;
uniqueness
for b1, b2 being Function of (Polynom-Ring (Polynom-Ring n,R)),(Polynom-Ring (n + 1),R) st ( for p1 being Polynomial of (Polynom-Ring n,R)
for p2 being Polynomial of n,R
for p3 being Polynomial of (n + 1),R
for b being bag of n + 1 st p3 = b1 . p1 & p2 = p1 . (b . n) holds
p3 . b = p2 . (b | n) ) & ( for p1 being Polynomial of (Polynom-Ring n,R)
for p2 being Polynomial of n,R
for p3 being Polynomial of (n + 1),R
for b being bag of n + 1 st p3 = b2 . p1 & p2 = p1 . (b . n) holds
p3 . b = p2 . (b | n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines upm HILBASIS:def 6 :
for R being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for n being Nat
for b3 being Function of (Polynom-Ring (Polynom-Ring n,R)),(Polynom-Ring (n + 1),R) holds
( b3 = upm n,R iff for p1 being Polynomial of (Polynom-Ring n,R)
for p2 being Polynomial of n,R
for p3 being Polynomial of (n + 1),R
for b being bag of n + 1 st p3 = b3 . p1 & p2 = p1 . (b . n) holds
p3 . b = p2 . (b | n) );

registration
let R be non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr ;
let n be Nat;
cluster upm n,R -> additive ;
coherence
upm n,R is additive
proof end;
cluster upm n,R -> multiplicative ;
coherence
upm n,R is multiplicative
proof end;
cluster upm n,R -> unity-preserving ;
coherence
upm n,R is unity-preserving
proof end;
cluster upm n,R -> one-to-one ;
coherence
upm n,R is one-to-one
proof end;
end;

definition
let R be non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr ;
let n be Nat;
func mpu n,R -> Function of (Polynom-Ring (n + 1),R),(Polynom-Ring (Polynom-Ring n,R)) means :Def7: :: HILBASIS:def 7
for p1 being Polynomial of (n + 1),R
for p2 being Polynomial of n,R
for p3 being Polynomial of (Polynom-Ring n,R)
for i being Nat
for b being bag of n st p3 = it . p1 & p2 = p3 . i holds
p2 . b = p1 . (b bag_extend i);
existence
ex b1 being Function of (Polynom-Ring (n + 1),R),(Polynom-Ring (Polynom-Ring n,R)) st
for p1 being Polynomial of (n + 1),R
for p2 being Polynomial of n,R
for p3 being Polynomial of (Polynom-Ring n,R)
for i being Nat
for b being bag of n st p3 = b1 . p1 & p2 = p3 . i holds
p2 . b = p1 . (b bag_extend i)
proof end;
uniqueness
for b1, b2 being Function of (Polynom-Ring (n + 1),R),(Polynom-Ring (Polynom-Ring n,R)) st ( for p1 being Polynomial of (n + 1),R
for p2 being Polynomial of n,R
for p3 being Polynomial of (Polynom-Ring n,R)
for i being Nat
for b being bag of n st p3 = b1 . p1 & p2 = p3 . i holds
p2 . b = p1 . (b bag_extend i) ) & ( for p1 being Polynomial of (n + 1),R
for p2 being Polynomial of n,R
for p3 being Polynomial of (Polynom-Ring n,R)
for i being Nat
for b being bag of n st p3 = b2 . p1 & p2 = p3 . i holds
p2 . b = p1 . (b bag_extend i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines mpu HILBASIS:def 7 :
for R being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for n being Nat
for b3 being Function of (Polynom-Ring (n + 1),R),(Polynom-Ring (Polynom-Ring n,R)) holds
( b3 = mpu n,R iff for p1 being Polynomial of (n + 1),R
for p2 being Polynomial of n,R
for p3 being Polynomial of (Polynom-Ring n,R)
for i being Nat
for b being bag of n st p3 = b3 . p1 & p2 = p3 . i holds
p2 . b = p1 . (b bag_extend i) );

theorem Th30: :: HILBASIS:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for n being Nat
for p being Element of (Polynom-Ring (n + 1),R) holds (upm n,R) . ((mpu n,R) . p) = p
proof end;

theorem Th31: :: HILBASIS:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for n being Nat ex P being Function of (Polynom-Ring (Polynom-Ring n,R)),(Polynom-Ring (n + 1),R) st P is RingIsomorphism
proof end;

registration
let R be non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Noetherian doubleLoopStr ;
cluster Polynom-Ring R -> Noetherian ;
coherence
Polynom-Ring R is Noetherian
proof end;
end;

Lm1: for R being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Noetherian doubleLoopStr holds Polynom-Ring R is Noetherian
;

theorem :: HILBASIS:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th33: :: HILBASIS:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr st R is Noetherian holds
for n being Nat holds Polynom-Ring n,R is Noetherian
proof end;

theorem Th34: :: HILBASIS:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field holds F is Noetherian
proof end;

theorem :: HILBASIS:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for n being Nat holds Polynom-Ring n,F is Noetherian
proof end;

theorem :: HILBASIS:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for X being infinite Ordinal holds not Polynom-Ring X,R is Noetherian
proof end;