:: HILBASIS semantic presentation :: Showing IDV graph ... (Click the Palm Trees again to close it)
theorem Th1: :: HILBASIS:1 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th2: :: HILBASIS:2 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th3: :: HILBASIS:3 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th4: :: HILBASIS:4 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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'
theorem Th5: :: HILBASIS:5 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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' )
:: deftheorem Def1 defines bag_extend HILBASIS:def 1 :
theorem Th6: :: HILBASIS:6 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th7: :: HILBASIS:7 :: Showing IDV graph ... (Click the Palm Tree again to close it)
:: deftheorem defines UnitBag HILBASIS:def 2 :
theorem Th8: :: HILBASIS:8 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th9: :: HILBASIS:9 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th10: :: HILBASIS:10 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th11: :: HILBASIS:11 :: Showing IDV graph ... (Click the Palm Tree again to close it)
:: deftheorem defines 1_1 HILBASIS:def 3 :
theorem Th12: :: HILBASIS:12 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th13: :: HILBASIS:13 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th14: :: HILBASIS:14 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th15: :: HILBASIS:15 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th16: :: HILBASIS:16 :: Showing IDV graph ... (Click the Palm Tree again to close it)
:: deftheorem defines minlen HILBASIS:def 4 :
theorem Th17: :: HILBASIS:17 :: Showing IDV graph ... (Click the Palm Tree again to close it)
:: deftheorem Def5 defines monomial HILBASIS:def 5 :
theorem Th18: :: HILBASIS:18 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th19: :: HILBASIS:19 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th20: :: HILBASIS:20 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th21: :: HILBASIS:21 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th22: :: HILBASIS:22 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th23: :: HILBASIS:23 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th24: :: HILBASIS:24 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th25: :: HILBASIS:25 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th26: :: HILBASIS:26 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th27: :: HILBASIS:27 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th28: :: HILBASIS:28 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th29: :: HILBASIS:29 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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)
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
end;
:: deftheorem Def6 defines upm HILBASIS:def 6 :
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)
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
end;
:: deftheorem Def7 defines mpu HILBASIS:def 7 :
theorem Th30: :: HILBASIS:30 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th31: :: HILBASIS:31 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem Th33: :: HILBASIS:33 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th34: :: HILBASIS:34 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: HILBASIS:35 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: HILBASIS:36 :: Showing IDV graph ... (Click the Palm Tree again to close it)