:: HILBASIS semantic presentation
begin
theorem Th1: :: HILBASIS:1
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
let A, B be FinSequence; ::_thesis: 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 )
let f be Function; ::_thesis: ( (rng A) \/ (rng B) c= dom f implies ex fA, fB being FinSequence st
( fA = f * A & fB = f * B & f * (A ^ B) = fA ^ fB ) )
assume A1: (rng A) \/ (rng B) c= dom f ; ::_thesis: ex fA, fB being FinSequence st
( fA = f * A & fB = f * B & f * (A ^ B) = fA ^ fB )
then A2: rng (A ^ B) c= dom f by FINSEQ_1:31;
then reconsider fAB = f * (A ^ B) as FinSequence by FINSEQ_1:16;
A3: rng B c= (rng A) \/ (rng B) by XBOOLE_1:7;
then reconsider fB = f * B as FinSequence by A1, FINSEQ_1:16, XBOOLE_1:1;
A4: dom (f * B) = dom B by A1, A3, RELAT_1:27, XBOOLE_1:1;
then A5: len fB = len B by FINSEQ_3:29;
A6: rng A c= (rng A) \/ (rng B) by XBOOLE_1:7;
then reconsider fA = f * A as FinSequence by A1, FINSEQ_1:16, XBOOLE_1:1;
take fA ; ::_thesis: ex fB being FinSequence st
( fA = f * A & fB = f * B & f * (A ^ B) = fA ^ fB )
take fB ; ::_thesis: ( fA = f * A & fB = f * B & f * (A ^ B) = fA ^ fB )
A7: dom (f * (A ^ B)) = dom (A ^ B) by A2, RELAT_1:27;
A8: dom (f * A) = dom A by A1, A6, RELAT_1:27, XBOOLE_1:1;
then A9: len fA = len A by FINSEQ_3:29;
A10: now__::_thesis:_for_k_being_Nat_st_1_<=_k_&_k_<=_len_fAB_holds_
(fA_^_fB)_._k_=_fAB_._k
let k be Nat; ::_thesis: ( 1 <= k & k <= len fAB implies (fA ^ fB) . b1 = fAB . b1 )
assume ( 1 <= k & k <= len fAB ) ; ::_thesis: (fA ^ fB) . b1 = fAB . b1
then A11: k in dom fAB by FINSEQ_3:25;
percases ( k in dom fA or not k in dom fA ) ;
supposeA12: k in dom fA ; ::_thesis: (fA ^ fB) . b1 = fAB . b1
hence (fA ^ fB) . k = fA . k by FINSEQ_1:def_7
.= f . (A . k) by A12, FUNCT_1:12
.= f . ((A ^ B) . k) by A8, A12, FINSEQ_1:def_7
.= fAB . k by A11, FUNCT_1:12 ;
::_thesis: verum
end;
suppose not k in dom fA ; ::_thesis: fAB . b1 = (fA ^ fB) . b1
then consider n being Nat such that
A13: n in dom B and
A14: k = (len A) + n by A8, A7, A11, FINSEQ_1:25;
thus fAB . k = f . ((A ^ B) . k) by A11, FUNCT_1:12
.= f . (B . n) by A13, A14, FINSEQ_1:def_7
.= fB . n by A4, A13, FUNCT_1:12
.= (fA ^ fB) . k by A9, A4, A13, A14, FINSEQ_1:def_7 ; ::_thesis: verum
end;
end;
end;
len fAB = len (A ^ B) by A7, FINSEQ_3:29
.= (len fA) + (len fB) by A9, A5, FINSEQ_1:22
.= len (fA ^ fB) by FINSEQ_1:22 ;
hence ( fA = f * A & fB = f * B & f * (A ^ B) = fA ^ fB ) by A10, FINSEQ_1:14; ::_thesis: verum
end;
theorem Th2: :: HILBASIS:2
for b being bag of 0 holds decomp b = <*<*{},{}*>*>
proof
let b be bag of 0 ; ::_thesis: decomp b = <*<*{},{}*>*>
A1: EmptyBag {} = {} --> 0 ;
then divisors b = <*{}*> by PRE_POLY:67;
then A2: len (divisors b) = 1 by FINSEQ_1:39;
A3: dom (divisors b) = dom (decomp b) by PRE_POLY:def_17;
then 1 in dom (decomp b) by A2, FINSEQ_3:25;
then A4: (decomp b) . 1 = (decomp b) /. 1 by PARTFUN1:def_6
.= <*{},{}*> by A1, PRE_POLY:71 ;
len (decomp b) = 1 by A2, A3, FINSEQ_3:29;
hence decomp b = <*<*{},{}*>*> by A4, FINSEQ_1:40; ::_thesis: verum
end;
theorem Th3: :: HILBASIS:3
for i, j being Element of NAT
for b being bag of j st i <= j holds
b | i is Element of Bags i
proof
let i, j be Element of NAT ; ::_thesis: for b being bag of j st i <= j holds
b | i is Element of Bags i
let b be bag of j; ::_thesis: ( i <= j implies b | i is Element of Bags i )
assume A1: i <= j ; ::_thesis: b | i is Element of Bags i
i c= j
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in i or x in j )
assume x in i ; ::_thesis: x in j
then x in { y where y is Element of NAT : y < i } by AXIOMS:4;
then consider x9 being Element of NAT such that
A2: x9 = x and
A3: x9 < i ;
x9 < j by A1, A3, XXREAL_0:2;
then x9 in { y where y is Element of NAT : y < j } ;
hence x in j by A2, AXIOMS:4; ::_thesis: verum
end;
hence b | i is Element of Bags i by PRE_POLY:def_12; ::_thesis: verum
end;
theorem Th4: :: HILBASIS:4
for i, j being set
for b1, b2 being bag of j
for b19, b29 being bag of i st b19 = b1 | i & b29 = b2 | i & b1 divides b2 holds
b19 divides b29
proof
let i, j be set ; ::_thesis: for b1, b2 being bag of j
for b19, b29 being bag of i st b19 = b1 | i & b29 = b2 | i & b1 divides b2 holds
b19 divides b29
let b1, b2 be bag of j; ::_thesis: for b19, b29 being bag of i st b19 = b1 | i & b29 = b2 | i & b1 divides b2 holds
b19 divides b29
let b19, b29 be bag of i; ::_thesis: ( b19 = b1 | i & b29 = b2 | i & b1 divides b2 implies b19 divides b29 )
assume that
A1: ( b19 = b1 | i & b29 = b2 | i ) and
A2: b1 divides b2 ; ::_thesis: b19 divides b29
now__::_thesis:_for_k_being_set_holds_b19_._k_<=_b29_._k
let k be set ; ::_thesis: b19 . b1 <= b29 . b1
A3: dom b19 = i by PARTFUN1:def_2
.= dom b29 by PARTFUN1:def_2 ;
percases ( not k in dom b19 or k in dom b19 ) ;
supposeA4: not k in dom b19 ; ::_thesis: b19 . b1 <= b29 . b1
then b19 . k = {} by FUNCT_1:def_2
.= b29 . k by A3, A4, FUNCT_1:def_2 ;
hence b19 . k <= b29 . k ; ::_thesis: verum
end;
suppose k in dom b19 ; ::_thesis: b19 . b1 <= b29 . b1
then ( b19 . k = b1 . k & b29 . k = b2 . k ) by A1, A3, FUNCT_1:47;
hence b19 . k <= b29 . k by A2, PRE_POLY:def_11; ::_thesis: verum
end;
end;
end;
hence b19 divides b29 by PRE_POLY:def_11; ::_thesis: verum
end;
theorem Th5: :: HILBASIS:5
for i, j being set
for b1, b2 being bag of j
for b19, b29 being bag of i st b19 = b1 | i & b29 = b2 | i holds
( (b1 -' b2) | i = b19 -' b29 & (b1 + b2) | i = b19 + b29 )
proof
let i, j be set ; ::_thesis: for b1, b2 being bag of j
for b19, b29 being bag of i st b19 = b1 | i & b29 = b2 | i holds
( (b1 -' b2) | i = b19 -' b29 & (b1 + b2) | i = b19 + b29 )
let b1, b2 be bag of j; ::_thesis: for b19, b29 being bag of i st b19 = b1 | i & b29 = b2 | i holds
( (b1 -' b2) | i = b19 -' b29 & (b1 + b2) | i = b19 + b29 )
let b19, b29 be bag of i; ::_thesis: ( b19 = b1 | i & b29 = b2 | i implies ( (b1 -' b2) | i = b19 -' b29 & (b1 + b2) | i = b19 + b29 ) )
assume that
A1: b19 = b1 | i and
A2: b29 = b2 | i ; ::_thesis: ( (b1 -' b2) | i = b19 -' b29 & (b1 + b2) | i = b19 + b29 )
dom b1 = j by PARTFUN1:def_2;
then A3: dom (b1 | i) = j /\ i by RELAT_1:61;
dom b2 = j by PARTFUN1:def_2;
then A4: dom (b2 | i) = j /\ i by RELAT_1:61;
dom (b1 + b2) = j by PARTFUN1:def_2;
then A5: dom ((b1 + b2) | i) = j /\ i by RELAT_1:61;
A6: now__::_thesis:_for_x_being_set_st_x_in_j_/\_i_holds_
((b1_+_b2)_|_i)_._x_=_(b19_+_b29)_._x
let x be set ; ::_thesis: ( x in j /\ i implies ((b1 + b2) | i) . x = (b19 + b29) . x )
assume A7: x in j /\ i ; ::_thesis: ((b1 + b2) | i) . x = (b19 + b29) . x
hence ((b1 + b2) | i) . x = (b1 + b2) . x by A5, FUNCT_1:47
.= (b1 . x) + (b2 . x) by PRE_POLY:def_5
.= (b19 . x) + (b2 . x) by A1, A3, A7, FUNCT_1:47
.= (b19 . x) + (b29 . x) by A2, A4, A7, FUNCT_1:47
.= (b19 + b29) . x by PRE_POLY:def_5 ;
::_thesis: verum
end;
dom (b1 -' b2) = j by PARTFUN1:def_2;
then A8: dom ((b1 -' b2) | i) = j /\ i by RELAT_1:61;
A9: now__::_thesis:_for_x_being_set_st_x_in_j_/\_i_holds_
((b1_-'_b2)_|_i)_._x_=_(b19_-'_b29)_._x
let x be set ; ::_thesis: ( x in j /\ i implies ((b1 -' b2) | i) . x = (b19 -' b29) . x )
assume A10: x in j /\ i ; ::_thesis: ((b1 -' b2) | i) . x = (b19 -' b29) . x
hence ((b1 -' b2) | i) . x = (b1 -' b2) . x by A8, FUNCT_1:47
.= (b1 . x) -' (b2 . x) by PRE_POLY:def_6
.= (b19 . x) -' (b2 . x) by A1, A3, A10, FUNCT_1:47
.= (b19 . x) -' (b29 . x) by A2, A4, A10, FUNCT_1:47
.= (b19 -' b29) . x by PRE_POLY:def_6 ;
::_thesis: verum
end;
dom (b19 -' b29) = i by PARTFUN1:def_2
.= j /\ i by A1, A3, PARTFUN1:def_2 ;
hence (b1 -' b2) | i = b19 -' b29 by A8, A9, FUNCT_1:2; ::_thesis: (b1 + b2) | i = b19 + b29
dom (b19 + b29) = i by PARTFUN1:def_2
.= j /\ i by A1, A3, PARTFUN1:def_2 ;
hence (b1 + b2) | i = b19 + b29 by A5, A6, FUNCT_1:2; ::_thesis: verum
end;
definition
let n, k be Nat;
let b be bag of n;
funcb 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
set b1 = b +* (n .--> k);
A1: dom b = n by PARTFUN1:def_2;
A2: dom (b +* (n .--> k)) = (dom b) \/ (dom (n .--> k)) by FUNCT_4:def_1
.= (dom b) \/ {n} by FUNCOP_1:13
.= n \/ {n} by PARTFUN1:def_2
.= succ n by ORDINAL1:def_1
.= n + 1 by NAT_1:38 ;
then b +* (n .--> k) is ManySortedSet of n + 1 by PARTFUN1:def_2, RELAT_1:def_18;
then reconsider b1 = b +* (n .--> k) as Element of Bags (n + 1) by PRE_POLY:def_12;
take b1 ; ::_thesis: ( b1 | n = b & b1 . n = k )
A3: dom (b1 | n) = (n + 1) /\ n by A2, RELAT_1:61
.= (succ n) /\ n by NAT_1:38
.= (n \/ {n}) /\ n by ORDINAL1:def_1
.= n by XBOOLE_1:21 ;
now__::_thesis:_for_x_being_set_st_x_in_n_holds_
(b1_|_n)_._x_=_b_._x
let x be set ; ::_thesis: ( x in n implies (b1 | n) . x = b . x )
assume A4: x in n ; ::_thesis: (b1 | n) . x = b . x
then A5: x in (dom b) \/ (dom (n .--> k)) by A1, XBOOLE_0:def_3;
A6: now__::_thesis:_not_x_in_dom_(n_.-->_k)
assume x in dom (n .--> k) ; ::_thesis: contradiction
then x in {n} ;
then x = n by TARSKI:def_1;
hence contradiction by A4; ::_thesis: verum
end;
thus (b1 | n) . x = b1 . x by A3, A4, FUNCT_1:47
.= b . x by A5, A6, FUNCT_4:def_1 ; ::_thesis: verum
end;
hence b1 | n = b by A3, A1, FUNCT_1:2; ::_thesis: b1 . n = k
n in {n} by TARSKI:def_1;
then A7: n in dom (n .--> k) by FUNCOP_1:13;
then n in (dom b) \/ (dom (n .--> k)) by XBOOLE_0:def_3;
hence b1 . n = (n .--> k) . n by A7, FUNCT_4:def_1
.= k by FUNCOP_1:72 ;
::_thesis: verum
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
let b1, b2 be Element of Bags (n + 1); ::_thesis: ( b1 | n = b & b1 . n = k & b2 | n = b & b2 . n = k implies b1 = b2 )
assume that
A8: b1 | n = b and
A9: b1 . n = k and
A10: b2 | n = b and
A11: b2 . n = k ; ::_thesis: b1 = b2
A12: dom b1 = n + 1 by PARTFUN1:def_2;
A13: now__::_thesis:_for_x_being_set_st_x_in_n_+_1_holds_
b1_._x_=_b2_._x
let x be set ; ::_thesis: ( x in n + 1 implies b1 . b1 = b2 . b1 )
assume A14: x in n + 1 ; ::_thesis: b1 . b1 = b2 . b1
then x in succ n by NAT_1:38;
then A15: x in n \/ {n} by ORDINAL1:def_1;
percases ( x in {n} or not x in {n} ) ;
suppose x in {n} ; ::_thesis: b1 . b1 = b2 . b1
then x = n by TARSKI:def_1;
hence b1 . x = b2 . x by A9, A11; ::_thesis: verum
end;
suppose not x in {n} ; ::_thesis: b1 . b1 = b2 . b1
then x in n by A15, XBOOLE_0:def_3;
then x in (n + 1) /\ n by A14, XBOOLE_0:def_4;
then A16: x in dom b by A8, A12, RELAT_1:61;
hence b1 . x = b . x by A8, FUNCT_1:47
.= b2 . x by A10, A16, FUNCT_1:47 ;
::_thesis: verum
end;
end;
end;
dom b2 = n + 1 by PARTFUN1:def_2;
hence b1 = b2 by A12, A13, FUNCT_1:2; ::_thesis: verum
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
for n being Element of NAT holds EmptyBag (n + 1) = (EmptyBag n) bag_extend 0
proof
let n be Element of NAT ; ::_thesis: EmptyBag (n + 1) = (EmptyBag n) bag_extend 0
A1: now__::_thesis:_for_x_being_set_st_x_in_n_+_1_holds_
(EmptyBag_(n_+_1))_._x_=_((EmptyBag_n)_bag_extend_0)_._x
let x be set ; ::_thesis: ( x in n + 1 implies (EmptyBag (n + 1)) . b1 = ((EmptyBag n) bag_extend 0) . b1 )
assume x in n + 1 ; ::_thesis: (EmptyBag (n + 1)) . b1 = ((EmptyBag n) bag_extend 0) . b1
then x in succ n by NAT_1:38;
then A2: x in n \/ {n} by ORDINAL1:def_1;
percases ( x in n or x in {n} ) by A2, XBOOLE_0:def_3;
supposeA3: x in n ; ::_thesis: (EmptyBag (n + 1)) . b1 = ((EmptyBag n) bag_extend 0) . b1
thus (EmptyBag (n + 1)) . x = 0 by PRE_POLY:52
.= (EmptyBag n) . x by PRE_POLY:52
.= (((EmptyBag n) bag_extend 0) | n) . x by Def1
.= ((EmptyBag n) bag_extend 0) . x by A3, FUNCT_1:49 ; ::_thesis: verum
end;
supposeA4: x in {n} ; ::_thesis: (EmptyBag (n + 1)) . b1 = ((EmptyBag n) bag_extend 0) . b1
thus (EmptyBag (n + 1)) . x = 0 by PRE_POLY:52
.= ((EmptyBag n) bag_extend 0) . n by Def1
.= ((EmptyBag n) bag_extend 0) . x by A4, TARSKI:def_1 ; ::_thesis: verum
end;
end;
end;
( dom (EmptyBag (n + 1)) = n + 1 & dom ((EmptyBag n) bag_extend 0) = n + 1 ) by PARTFUN1:def_2;
hence EmptyBag (n + 1) = (EmptyBag n) bag_extend 0 by A1, FUNCT_1:2; ::_thesis: verum
end;
theorem Th7: :: HILBASIS:7
for n being Ordinal
for b, b1 being bag of n holds
( b1 in rng (divisors b) iff b1 divides b )
proof
let n be Ordinal; ::_thesis: for b, b1 being bag of n holds
( b1 in rng (divisors b) iff b1 divides b )
let b, b1 be bag of n; ::_thesis: ( b1 in rng (divisors b) iff b1 divides b )
consider S being non empty finite Subset of (Bags n) such that
A1: divisors b = SgmX ((BagOrder n),S) and
A2: for p being bag of n holds
( p in S iff p divides b ) by PRE_POLY:def_16;
field (BagOrder n) = Bags n by ORDERS_1:15;
then A3: BagOrder n linearly_orders S by ORDERS_1:37, ORDERS_1:38;
hereby ::_thesis: ( b1 divides b implies b1 in rng (divisors b) )
assume b1 in rng (divisors b) ; ::_thesis: b1 divides b
then b1 in S by A1, A3, PRE_POLY:def_2;
hence b1 divides b by A2; ::_thesis: verum
end;
assume b1 divides b ; ::_thesis: b1 in rng (divisors b)
then b1 in S by A2;
hence b1 in rng (divisors b) by A1, A3, PRE_POLY:def_2; ::_thesis: verum
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 PRE_POLY:def_12;
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
for X being non empty set
for x being Element of X holds support (UnitBag x) = {x}
proof
let X be non empty set ; ::_thesis: for x being Element of X holds support (UnitBag x) = {x}
let x be Element of X; ::_thesis: support (UnitBag x) = {x}
now__::_thesis:_for_a_being_set_holds_
(_(_a_in_support_(UnitBag_x)_implies_a_in_{x}_)_&_(_a_in_{x}_implies_a_in_support_(UnitBag_x)_)_)
let a be set ; ::_thesis: ( ( a in support (UnitBag x) implies a in {x} ) & ( a in {x} implies a in support (UnitBag x) ) )
hereby ::_thesis: ( a in {x} implies a in support (UnitBag x) )
assume A1: a in support (UnitBag x) ; ::_thesis: a in {x}
now__::_thesis:_not_a_<>_x
assume a <> x ; ::_thesis: contradiction
then ((EmptyBag X) +* (x,1)) . a = (EmptyBag X) . a by FUNCT_7:32
.= 0 by PRE_POLY:52 ;
hence contradiction by A1, PRE_POLY:def_7; ::_thesis: verum
end;
hence a in {x} by TARSKI:def_1; ::_thesis: verum
end;
EmptyBag X = X --> 0 by PRE_POLY:def_13;
then A2: dom (EmptyBag X) = X by FUNCOP_1:13;
assume a in {x} ; ::_thesis: a in support (UnitBag x)
then a = x by TARSKI:def_1;
then (UnitBag x) . a = 1 by A2, FUNCT_7:31;
hence a in support (UnitBag x) by PRE_POLY:def_7; ::_thesis: verum
end;
hence support (UnitBag x) = {x} by TARSKI:1; ::_thesis: verum
end;
theorem Th9: :: HILBASIS:9
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
let X be non empty set ; ::_thesis: 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 ) )
let x be Element of X; ::_thesis: ( (UnitBag x) . x = 1 & ( for y being Element of X st x <> y holds
(UnitBag x) . y = 0 ) )
A1: dom (X --> 0) = X by FUNCOP_1:13;
thus (UnitBag x) . x = ((X --> 0) +* (x,1)) . x by PRE_POLY:def_13
.= 1 by A1, FUNCT_7:31 ; ::_thesis: for y being Element of X st x <> y holds
(UnitBag x) . y = 0
let y be Element of X; ::_thesis: ( x <> y implies (UnitBag x) . y = 0 )
assume x <> y ; ::_thesis: (UnitBag x) . y = 0
hence (UnitBag x) . y = (EmptyBag X) . y by FUNCT_7:32
.= 0 by PRE_POLY:52 ;
::_thesis: verum
end;
theorem Th10: :: HILBASIS:10
for X being non empty set
for x1, x2 being Element of X st UnitBag x1 = UnitBag x2 holds
x1 = x2
proof
let X be non empty set ; ::_thesis: for x1, x2 being Element of X st UnitBag x1 = UnitBag x2 holds
x1 = x2
let x1, x2 be Element of X; ::_thesis: ( UnitBag x1 = UnitBag x2 implies x1 = x2 )
assume that
A1: UnitBag x1 = UnitBag x2 and
A2: x1 <> x2 ; ::_thesis: contradiction
1 = (UnitBag x2) . x1 by A1, Th9
.= 0 by A2, Th9 ;
hence contradiction ; ::_thesis: verum
end;
theorem Th11: :: HILBASIS:11
for X being non empty Ordinal
for x being Element of X
for L being non trivial well-unital doubleLoopStr
for e being Function of X,L holds eval ((UnitBag x),e) = e . x
proof
let X be non empty Ordinal; ::_thesis: for x being Element of X
for L being non trivial well-unital doubleLoopStr
for e being Function of X,L holds eval ((UnitBag x),e) = e . x
let x be Element of X; ::_thesis: for L being non trivial well-unital doubleLoopStr
for e being Function of X,L holds eval ((UnitBag x),e) = e . x
let L be non trivial well-unital doubleLoopStr ; ::_thesis: for e being Function of X,L holds eval ((UnitBag x),e) = e . x
let e be Function of X,L; ::_thesis: eval ((UnitBag x),e) = e . x
reconsider edx = e . x as Element of L ;
support (UnitBag x) = {x} by Th8;
hence eval ((UnitBag x),e) = (power L) . ((e . x),((UnitBag x) . x)) by POLYNOM2:15
.= (power L) . ((e . x),(0 + 1)) by Th9
.= ((power L) . (edx,0)) * edx by GROUP_1:def_7
.= (1_ L) * edx by GROUP_1:def_7
.= e . x by GROUP_1:def_4 ;
::_thesis: verum
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
for X being set
for L being non trivial unital 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
let X be set ; ::_thesis: for L being non trivial unital 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 ) )
let L be non trivial unital doubleLoopStr ; ::_thesis: 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 ) )
let x be Element of X; ::_thesis: ( (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 ) )
dom (0_ (X,L)) = dom ((Bags X) --> (0. L)) by POLYNOM1:def_7
.= Bags X by FUNCOP_1:13 ;
hence (1_1 (x,L)) . (UnitBag x) = 1_ L by FUNCT_7:31; ::_thesis: for b being bag of X st b <> UnitBag x holds
(1_1 (x,L)) . b = 0. L
let b be bag of X; ::_thesis: ( b <> UnitBag x implies (1_1 (x,L)) . b = 0. L )
assume b <> UnitBag x ; ::_thesis: (1_1 (x,L)) . b = 0. L
hence (1_1 (x,L)) . b = (0_ (X,L)) . b by FUNCT_7:32
.= 0. L by POLYNOM1:22 ;
::_thesis: verum
end;
theorem Th13: :: HILBASIS:13
for X being set
for x being Element of X
for L being non trivial right_complementable add-associative right_zeroed right-distributive well-unital doubleLoopStr holds Support (1_1 (x,L)) = {(UnitBag x)}
proof
let X be set ; ::_thesis: for x being Element of X
for L being non trivial right_complementable add-associative right_zeroed right-distributive well-unital doubleLoopStr holds Support (1_1 (x,L)) = {(UnitBag x)}
let x be Element of X; ::_thesis: for L being non trivial right_complementable add-associative right_zeroed right-distributive well-unital doubleLoopStr holds Support (1_1 (x,L)) = {(UnitBag x)}
let L be non trivial right_complementable add-associative right_zeroed right-distributive well-unital doubleLoopStr ; ::_thesis: Support (1_1 (x,L)) = {(UnitBag x)}
now__::_thesis:_for_a_being_set_holds_
(_(_a_in_Support_(1_1_(x,L))_implies_a_in_{(UnitBag_x)}_)_&_(_a_in_{(UnitBag_x)}_implies_a_in_Support_(1_1_(x,L))_)_)
let a be set ; ::_thesis: ( ( a in Support (1_1 (x,L)) implies a in {(UnitBag x)} ) & ( a in {(UnitBag x)} implies a in Support (1_1 (x,L)) ) )
hereby ::_thesis: ( a in {(UnitBag x)} implies a in Support (1_1 (x,L)) )
assume A1: a in Support (1_1 (x,L)) ; ::_thesis: a in {(UnitBag x)}
then reconsider b = a as Element of Bags X ;
now__::_thesis:_not_a_<>_UnitBag_x
assume a <> UnitBag x ; ::_thesis: contradiction
then (1_1 (x,L)) . b = (0_ (X,L)) . b by FUNCT_7:32
.= 0. L by POLYNOM1:22 ;
hence contradiction by A1, POLYNOM1:def_3; ::_thesis: verum
end;
hence a in {(UnitBag x)} by TARSKI:def_1; ::_thesis: verum
end;
assume A2: a in {(UnitBag x)} ; ::_thesis: a in Support (1_1 (x,L))
then a = UnitBag x by TARSKI:def_1;
then (1_1 (x,L)) . a <> 0. L by Th12;
hence a in Support (1_1 (x,L)) by A2, POLYNOM1:def_3; ::_thesis: verum
end;
hence Support (1_1 (x,L)) = {(UnitBag x)} by TARSKI:1; ::_thesis: verum
end;
registration
let X be Ordinal;
let x be Element of X;
let L be non trivial right_complementable add-associative right_zeroed right-distributive well-unital doubleLoopStr ;
cluster 1_1 (x,L) -> finite-Support ;
coherence
1_1 (x,L) is finite-Support
proof
Support (1_1 (x,L)) = {(UnitBag x)} by Th13;
hence 1_1 (x,L) is finite-Support by POLYNOM1:def_4; ::_thesis: verum
end;
end;
theorem Th14: :: HILBASIS:14
for L being non trivial right_complementable add-associative right_zeroed right-distributive well-unital 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
let L be non trivial right_complementable add-associative right_zeroed right-distributive well-unital doubleLoopStr ; ::_thesis: 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
let X be non empty set ; ::_thesis: for x1, x2 being Element of X st 1_1 (x1,L) = 1_1 (x2,L) holds
x1 = x2
let x1, x2 be Element of X; ::_thesis: ( 1_1 (x1,L) = 1_1 (x2,L) implies x1 = x2 )
assume that
A1: 1_1 (x1,L) = 1_1 (x2,L) and
A2: x1 <> x2 ; ::_thesis: contradiction
1_ L = (1_1 (x2,L)) . (UnitBag x1) by A1, Th12
.= 0. L by A2, Th10, Th12 ;
hence contradiction ; ::_thesis: verum
end;
theorem Th15: :: HILBASIS:15
for L being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr
for x being Element of (Polynom-Ring L)
for p being sequence of L st x = p holds
- x = - p
proof
let L be non empty right_complementable add-associative right_zeroed distributive doubleLoopStr ; ::_thesis: for x being Element of (Polynom-Ring L)
for p being sequence of L st x = p holds
- x = - p
let x be Element of (Polynom-Ring L); ::_thesis: for p being sequence of L st x = p holds
- x = - p
let p be sequence of L; ::_thesis: ( x = p implies - x = - p )
assume A1: x = p ; ::_thesis: - x = - p
reconsider x9 = x as Polynomial of L by POLYNOM3:def_10;
A2: now__::_thesis:_for_i_being_set_st_i_in_NAT_holds_
(p_-_p)_._i_=_(0_._L)_._i
let i be set ; ::_thesis: ( i in NAT implies (p - p) . i = (0_. L) . i )
assume A3: i in NAT ; ::_thesis: (p - p) . i = (0_. L) . i
then reconsider i9 = i as Element of NAT ;
thus (p - p) . i = (p . i9) - (p . i9) by POLYNOM3:27
.= 0. L by RLVECT_1:15
.= (0_. L) . i by A3, FUNCOP_1:7 ; ::_thesis: verum
end;
reconsider mx = - x9 as Element of (Polynom-Ring L) by POLYNOM3:def_10;
( dom (0_. L) = NAT & dom (p - p) = NAT ) by FUNCT_2:def_1;
then A4: p - p = 0_. L by A2, FUNCT_1:2;
x + mx = x9 + (- x9) by POLYNOM3:def_10
.= 0. (Polynom-Ring L) by A1, A4, POLYNOM3:def_10 ;
then x = - mx by RLVECT_1:6;
hence - x = - p by A1, RLVECT_1:17; ::_thesis: verum
end;
theorem Th16: :: HILBASIS:16
for L being non empty right_complementable add-associative right_zeroed 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
let L be non empty right_complementable add-associative right_zeroed distributive doubleLoopStr ; ::_thesis: 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
let x, y be Element of (Polynom-Ring L); ::_thesis: for p, q being sequence of L st x = p & y = q holds
x - y = p - q
let p, q be sequence of L; ::_thesis: ( x = p & y = q implies x - y = p - q )
assume that
A1: x = p and
A2: y = q ; ::_thesis: x - y = p - q
A3: - y = - q by A2, Th15;
thus x - y = x + (- y) by RLVECT_1:def_11
.= p - q by A1, A3, POLYNOM3:def_10 ; ::_thesis: verum
end;
definition
let L be non empty right_complementable add-associative right_zeroed well-unital 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 x9, y9 being Polynomial of L st x9 = x & y9 in I holds
len x9 <= len y9 } ;
coherence
{ x where x is Element of I : for x9, y9 being Polynomial of L st x9 = x & y9 in I holds
len x9 <= len y9 } is non empty Subset of I
proof
I c= I ;
then reconsider I9 = I as non empty Subset of I ;
defpred S1[ Element of I, Element of NAT ] means for p being Polynomial of L st $1 = p holds
$2 = len p;
set u = { x where x is Element of I : for x9, y9 being Polynomial of L st x9 = x & y9 in I holds
len x9 <= len y9 } ;
A1: now__::_thesis:_for_x_being_Element_of_I_ex_y_being_Element_of_NAT_st_S1[x,y]
let x be Element of I; ::_thesis: ex y being Element of NAT st S1[x,y]
reconsider x9 = x as Polynomial of L by POLYNOM3:def_10;
for p being Polynomial of L st x = p holds
len x9 = len p ;
hence ex y being Element of NAT st S1[x,y] ; ::_thesis: verum
end;
consider f being Function of I,NAT such that
A2: for x being Element of I holds S1[x,f . x] from FUNCT_2:sch_3(A1);
min (f .: I9) in f .: I by XXREAL_2:def_7;
then consider x being set such that
A3: x in dom f and
x in I and
A4: min (f .: I9) = f . x by FUNCT_1:def_6;
reconsider x = x as Element of I by A3;
now__::_thesis:_for_x9,_y9_being_Polynomial_of_L_st_x9_=_x_&_y9_in_I_holds_
len_x9_<=_len_y9
let x9, y9 be Polynomial of L; ::_thesis: ( x9 = x & y9 in I implies len x9 <= len y9 )
assume that
A5: x9 = x and
A6: y9 in I ; ::_thesis: len x9 <= len y9
dom f = I by FUNCT_2:def_1;
then f . y9 in f .: I by A6, FUNCT_1:def_6;
then f . x <= f . y9 by A4, XXREAL_2:def_7;
then len x9 <= f . y9 by A2, A5;
hence len x9 <= len y9 by A2, A6; ::_thesis: verum
end;
then A7: x in { x where x is Element of I : for x9, y9 being Polynomial of L st x9 = x & y9 in I holds
len x9 <= len y9 } ;
{ x where x is Element of I : for x9, y9 being Polynomial of L st x9 = x & y9 in I holds
len x9 <= len y9 } c= I
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { x where x is Element of I : for x9, y9 being Polynomial of L st x9 = x & y9 in I holds
len x9 <= len y9 } or x in I )
assume x in { x where x is Element of I : for x9, y9 being Polynomial of L st x9 = x & y9 in I holds
len x9 <= len y9 } ; ::_thesis: x in I
then ex x99 being Element of I st
( x99 = x & ( for x9, y9 being Polynomial of L st x9 = x99 & y9 in I holds
len x9 <= len y9 ) ) ;
hence x in I ; ::_thesis: verum
end;
hence { x where x is Element of I : for x9, y9 being Polynomial of L st x9 = x & y9 in I holds
len x9 <= len y9 } is non empty Subset of I by A7; ::_thesis: verum
end;
end;
:: deftheorem defines minlen HILBASIS:def_4_:_
for L being non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for I being non empty Subset of (Polynom-Ring L) holds minlen I = { x where x is Element of I : for x9, y9 being Polynomial of L st x9 = x & y9 in I holds
len x9 <= len y9 } ;
theorem Th17: :: HILBASIS:17
for L being non empty right_complementable add-associative right_zeroed well-unital 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
let L be non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; ::_thesis: 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 )
let I be non empty Subset of (Polynom-Ring L); ::_thesis: for i1, i2 being Polynomial of L st i1 in minlen I & i2 in I holds
( i1 in I & len i1 <= len i2 )
let i1, i2 be Polynomial of L; ::_thesis: ( i1 in minlen I & i2 in I implies ( i1 in I & len i1 <= len i2 ) )
assume that
A1: i1 in minlen I and
A2: i2 in I ; ::_thesis: ( i1 in I & len i1 <= len i2 )
ex i19 being Element of I st
( i19 = i1 & ( for x9, y9 being Polynomial of L st x9 = i19 & y9 in I holds
len x9 <= len y9 ) ) by A1;
hence ( i1 in I & len i1 <= len i2 ) by A2; ::_thesis: verum
end;
definition
let L be non empty right_complementable add-associative right_zeroed well-unital 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
reconsider x = (0_. L) +* (n,a) as sequence of L ;
now__::_thesis:_for_i_being_Nat_st_i_>=_n_+_1_holds_
x_._i_=_0._L
let i be Nat; ::_thesis: ( i >= n + 1 implies x . i = 0. L )
A1: i in NAT by ORDINAL1:def_12;
assume i >= n + 1 ; ::_thesis: x . i = 0. L
then i > n by NAT_1:13;
hence x . i = (NAT --> (0. L)) . i by FUNCT_7:32
.= 0. L by A1, FUNCOP_1:7 ;
::_thesis: verum
end;
then reconsider x = x as Polynomial of L by ALGSEQ_1:def_1;
now__::_thesis:_for_i_being_Nat_holds_
(_(_i_=_n_implies_x_._i_=_a_)_&_(_i_<>_n_implies_x_._i_=_0._L_)_)
let i be Nat; ::_thesis: ( ( i = n implies x . i = a ) & ( i <> n implies x . i = 0. L ) )
A2: i in NAT by ORDINAL1:def_12;
thus ( i = n implies x . i = a ) ::_thesis: ( i <> n implies x . i = 0. L )
proof
A3: dom (0_. L) = NAT by FUNCT_2:def_1;
assume i = n ; ::_thesis: x . i = a
hence x . i = a by A2, A3, FUNCT_7:31; ::_thesis: verum
end;
thus ( i <> n implies x . i = 0. L ) ::_thesis: verum
proof
assume i <> n ; ::_thesis: x . i = 0. L
hence x . i = (NAT --> (0. L)) . i by FUNCT_7:32
.= 0. L by A2, FUNCOP_1:7 ;
::_thesis: verum
end;
end;
hence 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 ) ) ; ::_thesis: verum
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
let u, v be Polynomial of L; ::_thesis: ( ( for x being Nat holds
( ( x = n implies u . x = a ) & ( x <> n implies u . x = 0. L ) ) ) & ( for x being Nat holds
( ( x = n implies v . x = a ) & ( x <> n implies v . x = 0. L ) ) ) implies u = v )
assume that
A4: for x being Nat holds
( ( x = n implies u . x = a ) & ( x <> n implies u . x = 0. L ) ) and
A5: for x being Nat holds
( ( x = n implies v . x = a ) & ( x <> n implies v . x = 0. L ) ) ; ::_thesis: u = v
A6: now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_
u_._x_=_v_._x
let x be set ; ::_thesis: ( x in NAT implies u . b1 = v . b1 )
assume A7: x in NAT ; ::_thesis: u . b1 = v . b1
percases ( x = n or x <> n ) ;
supposeA8: x = n ; ::_thesis: u . b1 = v . b1
hence u . x = a by A4
.= v . x by A5, A8 ;
::_thesis: verum
end;
supposeA9: x <> n ; ::_thesis: u . b1 = v . b1
hence u . x = 0. L by A4, A7
.= v . x by A5, A7, A9 ;
::_thesis: verum
end;
end;
end;
( dom u = NAT & dom v = NAT ) by FUNCT_2:def_1;
hence u = v by A6, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines monomial HILBASIS:def_5_:_
for L being non empty right_complementable add-associative right_zeroed well-unital 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
for L being non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for n being Element of 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
let L be non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; ::_thesis: for n being Element of 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 )
let n be Element of NAT ; ::_thesis: 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 )
let a be Element of L; ::_thesis: ( ( 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 )
A1: now__::_thesis:_(_a_=_0._L_implies_len_(monomial_(a,n))_=_0_)
assume A2: a = 0. L ; ::_thesis: len (monomial (a,n)) = 0
now__::_thesis:_for_i_being_Nat_st_i_>=_0_holds_
(monomial_(a,n))_._i_=_0._L
let i be Nat; ::_thesis: ( i >= 0 implies (monomial (a,n)) . b1 = 0. L )
assume i >= 0 ; ::_thesis: (monomial (a,n)) . b1 = 0. L
percases ( i = n or i <> n ) ;
suppose i = n ; ::_thesis: (monomial (a,n)) . b1 = 0. L
thus (monomial (a,n)) . i = 0. L by A2, Def5; ::_thesis: verum
end;
suppose i <> n ; ::_thesis: (monomial (a,n)) . b1 = 0. L
hence (monomial (a,n)) . i = 0. L by Def5; ::_thesis: verum
end;
end;
end;
then 0 is_at_least_length_of monomial (a,n) by ALGSEQ_1:def_2;
hence len (monomial (a,n)) = 0 by ALGSEQ_1:def_3; ::_thesis: verum
end;
now__::_thesis:_(_a_<>_0._L_implies_len_(monomial_(a,n))_=_n_+_1_)
now__::_thesis:_for_i_being_Nat_st_i_>=_n_+_1_holds_
(monomial_(a,n))_._i_=_0._L
let i be Nat; ::_thesis: ( i >= n + 1 implies (monomial (a,n)) . i = 0. L )
assume i >= n + 1 ; ::_thesis: (monomial (a,n)) . i = 0. L
then i > n by NAT_1:13;
hence (monomial (a,n)) . i = 0. L by Def5; ::_thesis: verum
end;
then n + 1 is_at_least_length_of monomial (a,n) by ALGSEQ_1:def_2;
then A3: len (monomial (a,n)) <= n + 1 by ALGSEQ_1:def_3;
assume a <> 0. L ; ::_thesis: len (monomial (a,n)) = n + 1
then (monomial (a,n)) . n <> 0. L by Def5;
then len (monomial (a,n)) > n by ALGSEQ_1:8;
then len (monomial (a,n)) >= n + 1 by NAT_1:13;
hence len (monomial (a,n)) = n + 1 by A3, XXREAL_0:1; ::_thesis: verum
end;
hence ( ( 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 ) by A1; ::_thesis: verum
end;
theorem Th19: :: HILBASIS:19
for L being non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for n, x being Element of NAT
for a being Element of L
for p being Polynomial of L holds ((monomial (a,n)) *' p) . (x + n) = a * (p . x)
proof
let L be non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; ::_thesis: for n, x being Element of NAT
for a being Element of L
for p being Polynomial of L holds ((monomial (a,n)) *' p) . (x + n) = a * (p . x)
let n, x be Element of NAT ; ::_thesis: for a being Element of L
for p being Polynomial of L holds ((monomial (a,n)) *' p) . (x + n) = a * (p . x)
let a be Element of L; ::_thesis: for p being Polynomial of L holds ((monomial (a,n)) *' p) . (x + n) = a * (p . x)
let p be Polynomial of L; ::_thesis: ((monomial (a,n)) *' p) . (x + n) = a * (p . x)
consider r being FinSequence of the carrier of L such that
A1: len r = (x + n) + 1 and
A2: ((monomial (a,n)) *' p) . (x + n) = Sum r and
A3: for k being Element of NAT st k in dom r holds
r . k = ((monomial (a,n)) . (k -' 1)) * (p . (((x + n) + 1) -' k)) by POLYNOM3:def_9;
len r = n + (1 + x) by A1;
then consider b, c being FinSequence of the carrier of L such that
A4: len b = n and
A5: len c = 1 + x and
A6: r = b ^ c by FINSEQ_2:23;
consider d, e being FinSequence of the carrier of L such that
A7: len d = 1 and
len e = x and
A8: c = d ^ e by A5, FINSEQ_2:23;
A9: dom d c= dom c by A8, FINSEQ_1:26;
now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_b_holds_
b_._i_=_0._L
A10: dom b c= dom r by A6, FINSEQ_1:26;
let i be Element of NAT ; ::_thesis: ( i in dom b implies b . i = 0. L )
A11: i - 1 < i by XREAL_1:146;
assume A12: i in dom b ; ::_thesis: b . i = 0. L
then A13: i <= n by A4, FINSEQ_3:25;
1 <= i by A12, FINSEQ_3:25;
then A14: i -' 1 = i - 1 by XREAL_1:233;
thus b . i = r . i by A6, A12, FINSEQ_1:def_7
.= ((monomial (a,n)) . (i -' 1)) * (p . (((x + n) + 1) -' i)) by A3, A12, A10
.= (0. L) * (p . (((x + n) + 1) -' i)) by A13, A14, A11, Def5
.= 0. L by VECTSP_1:7 ; ::_thesis: verum
end;
then A15: Sum b = 0. L by POLYNOM3:1;
now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_e_holds_
e_._i_=_0._L
let i be Element of NAT ; ::_thesis: ( i in dom e implies e . i = 0. L )
A16: (n + (1 + i)) -' 1 = ((n + i) + 1) -' 1
.= n + i by NAT_D:34 ;
assume A17: i in dom e ; ::_thesis: e . i = 0. L
then A18: 1 + i in dom c by A7, A8, FINSEQ_1:28;
i >= 1 by A17, FINSEQ_3:25;
then n + i >= n + 1 by XREAL_1:6;
then A19: n + i > n by NAT_1:13;
thus e . i = c . (1 + i) by A7, A8, A17, FINSEQ_1:def_7
.= r . (n + (1 + i)) by A4, A6, A18, FINSEQ_1:def_7
.= ((monomial (a,n)) . ((n + (1 + i)) -' 1)) * (p . (((x + n) + 1) -' (n + (1 + i)))) by A3, A4, A6, A18, FINSEQ_1:28
.= (0. L) * (p . (((x + n) + 1) -' (n + (1 + i)))) by A19, A16, Def5
.= 0. L by VECTSP_1:7 ; ::_thesis: verum
end;
then A20: Sum e = 0. L by POLYNOM3:1;
A21: 1 in dom d by A7, FINSEQ_3:25;
then d . 1 = c . 1 by A8, FINSEQ_1:def_7
.= r . (n + 1) by A4, A6, A21, A9, FINSEQ_1:def_7
.= ((monomial (a,n)) . ((n + 1) -' 1)) * (p . (((x + n) + 1) -' (n + 1))) by A3, A4, A6, A21, A9, FINSEQ_1:28
.= ((monomial (a,n)) . n) * (p . ((x + (n + 1)) -' (n + 1))) by NAT_D:34
.= ((monomial (a,n)) . n) * (p . x) by NAT_D:34
.= a * (p . x) by Def5 ;
then d = <*(a * (p . x))*> by A7, FINSEQ_1:40;
then Sum d = a * (p . x) by RLVECT_1:44;
then Sum c = (a * (p . x)) + (0. L) by A8, A20, RLVECT_1:41
.= a * (p . x) by RLVECT_1:4 ;
hence ((monomial (a,n)) *' p) . (x + n) = (0. L) + (a * (p . x)) by A2, A6, A15, RLVECT_1:41
.= a * (p . x) by RLVECT_1:4 ;
::_thesis: verum
end;
theorem Th20: :: HILBASIS:20
for L being non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for n, x being Element of NAT
for a being Element of L
for p being Polynomial of L holds (p *' (monomial (a,n))) . (x + n) = (p . x) * a
proof
let L be non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; ::_thesis: for n, x being Element of NAT
for a being Element of L
for p being Polynomial of L holds (p *' (monomial (a,n))) . (x + n) = (p . x) * a
let n, x be Element of NAT ; ::_thesis: for a being Element of L
for p being Polynomial of L holds (p *' (monomial (a,n))) . (x + n) = (p . x) * a
let a be Element of L; ::_thesis: for p being Polynomial of L holds (p *' (monomial (a,n))) . (x + n) = (p . x) * a
let p be Polynomial of L; ::_thesis: (p *' (monomial (a,n))) . (x + n) = (p . x) * a
consider r being FinSequence of the carrier of L such that
A1: len r = (x + n) + 1 and
A2: (p *' (monomial (a,n))) . (x + n) = Sum r and
A3: for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * ((monomial (a,n)) . (((x + n) + 1) -' k)) by POLYNOM3:def_9;
len r = x + (n + 1) by A1;
then consider b, c being FinSequence of the carrier of L such that
A4: len b = x and
A5: len c = n + 1 and
A6: r = b ^ c by FINSEQ_2:23;
consider d, e being FinSequence of the carrier of L such that
A7: len d = 1 and
A8: len e = n and
A9: c = d ^ e by A5, FINSEQ_2:23;
A10: dom d c= dom c by A9, FINSEQ_1:26;
now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_e_holds_
e_._i_=_0._L
let i be Element of NAT ; ::_thesis: ( i in dom e implies e . i = 0. L )
A11: n > n - 1 by XREAL_1:146;
assume A12: i in dom e ; ::_thesis: e . i = 0. L
then A13: 1 + i in dom c by A7, A9, FINSEQ_1:28;
i <= n by A8, A12, FINSEQ_3:25;
then x + i <= x + n by XREAL_1:6;
then (x + i) + 1 <= (x + n) + 1 by XREAL_1:6;
then A14: ((x + n) + 1) -' (x + (1 + i)) = ((x + n) + 1) - (x + (1 + i)) by XREAL_1:233;
1 <= i by A12, FINSEQ_3:25;
then A15: n - i <= n - 1 by XREAL_1:13;
thus e . i = c . (1 + i) by A7, A9, A12, FINSEQ_1:def_7
.= r . (x + (1 + i)) by A4, A6, A13, FINSEQ_1:def_7
.= (p . ((x + (1 + i)) -' 1)) * ((monomial (a,n)) . (((x + n) + 1) -' (x + (1 + i)))) by A3, A4, A6, A13, FINSEQ_1:28
.= (p . ((x + (1 + i)) -' 1)) * (0. L) by A14, A15, A11, Def5
.= 0. L by VECTSP_1:6 ; ::_thesis: verum
end;
then A16: Sum e = 0. L by POLYNOM3:1;
now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_b_holds_
b_._i_=_0._L
let i be Element of NAT ; ::_thesis: ( i in dom b implies b . i = 0. L )
A17: dom b c= dom r by A6, FINSEQ_1:26;
assume A18: i in dom b ; ::_thesis: b . i = 0. L
then i <= x by A4, FINSEQ_3:25;
then i + n <= x + n by XREAL_1:6;
then i + n < (x + n) + 1 by NAT_1:13;
then A19: n < ((x + n) + 1) - i by XREAL_1:20;
then A20: ((x + n) + 1) - i = ((x + n) + 1) -' i by XREAL_0:def_2;
thus b . i = r . i by A6, A18, FINSEQ_1:def_7
.= (p . (i -' 1)) * ((monomial (a,n)) . (((x + n) + 1) -' i)) by A3, A18, A17
.= (p . (i -' 1)) * (0. L) by A19, A20, Def5
.= 0. L by VECTSP_1:6 ; ::_thesis: verum
end;
then A21: Sum b = 0. L by POLYNOM3:1;
A22: 1 in dom d by A7, FINSEQ_3:25;
then d . 1 = c . 1 by A9, FINSEQ_1:def_7
.= r . (x + 1) by A4, A6, A22, A10, FINSEQ_1:def_7
.= (p . ((x + 1) -' 1)) * ((monomial (a,n)) . (((x + n) + 1) -' (x + 1))) by A3, A4, A6, A22, A10, FINSEQ_1:28
.= (p . x) * ((monomial (a,n)) . ((n + (x + 1)) -' (x + 1))) by NAT_D:34
.= (p . x) * ((monomial (a,n)) . n) by NAT_D:34
.= (p . x) * a by Def5 ;
then d = <*((p . x) * a)*> by A7, FINSEQ_1:40;
then Sum d = (p . x) * a by RLVECT_1:44;
then Sum c = ((p . x) * a) + (0. L) by A9, A16, RLVECT_1:41
.= (p . x) * a by RLVECT_1:4 ;
hence (p *' (monomial (a,n))) . (x + n) = (0. L) + ((p . x) * a) by A2, A6, A21, RLVECT_1:41
.= (p . x) * a by RLVECT_1:4 ;
::_thesis: verum
end;
theorem Th21: :: HILBASIS:21
for L being non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for p, q being Polynomial of L holds len (p *' q) <= ((len p) + (len q)) -' 1
proof
let L be non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; ::_thesis: for p, q being Polynomial of L holds len (p *' q) <= ((len p) + (len q)) -' 1
let p, q be Polynomial of L; ::_thesis: len (p *' q) <= ((len p) + (len q)) -' 1
now__::_thesis:_for_i_being_Nat_st_i_>=_((len_p)_+_(len_q))_-'_1_holds_
(p_*'_q)_._i_=_0._L
let i be Nat; ::_thesis: ( i >= ((len p) + (len q)) -' 1 implies (p *' q) . i = 0. L )
A1: ((len p) + (len q)) -' 1 >= ((len p) + (len q)) - 1 by XREAL_0:def_2;
i in NAT by ORDINAL1:def_12;
then consider r being FinSequence of the carrier of L such that
A2: len r = i + 1 and
A3: (p *' q) . i = Sum r and
A4: for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by POLYNOM3:def_9;
assume i >= ((len p) + (len q)) -' 1 ; ::_thesis: (p *' q) . i = 0. L
then i >= (len p) + ((len q) - 1) by A1, XXREAL_0:2;
then len p <= i - ((len q) - 1) by XREAL_1:19;
then A5: - (len p) >= - ((i - (len q)) + 1) by XREAL_1:24;
now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_r_holds_
r_._k_=_0._L
let k be Element of NAT ; ::_thesis: ( k in dom r implies r . b1 = 0. L )
assume A6: k in dom r ; ::_thesis: r . b1 = 0. L
then A7: r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by A4;
k in Seg (len r) by A6, FINSEQ_1:def_3;
then k <= i + 1 by A2, FINSEQ_1:1;
then A8: (i + 1) - k >= 0 by XREAL_1:48;
percases ( k -' 1 < len p or k -' 1 >= len p ) ;
suppose k -' 1 < len p ; ::_thesis: r . b1 = 0. L
then k - 1 < len p by XREAL_0:def_2;
then - (k - 1) > - (len p) by XREAL_1:24;
then 1 - k > ((len q) - 1) - i by A5, XXREAL_0:2;
then i + (1 - k) > (len q) - 1 by XREAL_1:19;
then (i + 1) -' k > (len q) - 1 by A8, XREAL_0:def_2;
then (i + 1) -' k >= ((len q) - 1) + 1 by INT_1:7;
then q . ((i + 1) -' k) = 0. L by ALGSEQ_1:8;
hence r . k = 0. L by A7, VECTSP_1:6; ::_thesis: verum
end;
suppose k -' 1 >= len p ; ::_thesis: r . b1 = 0. L
then p . (k -' 1) = 0. L by ALGSEQ_1:8;
hence r . k = 0. L by A7, VECTSP_1:7; ::_thesis: verum
end;
end;
end;
hence (p *' q) . i = 0. L by A3, POLYNOM3:1; ::_thesis: verum
end;
then ((len p) + (len q)) -' 1 is_at_least_length_of p *' q by ALGSEQ_1:def_2;
hence len (p *' q) <= ((len p) + (len q)) -' 1 by ALGSEQ_1:def_3; ::_thesis: verum
end;
begin
theorem Th22: :: HILBASIS:22
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
let R, S be non empty doubleLoopStr ; ::_thesis: for I being Ideal of R
for P being Function of R,S st P is RingIsomorphism holds
P .: I is Ideal of S
let I be Ideal of R; ::_thesis: for P being Function of R,S st P is RingIsomorphism holds
P .: I is Ideal of S
let P be Function of R,S; ::_thesis: ( P is RingIsomorphism implies P .: I is Ideal of S )
set Q = P .: I;
assume A1: P is RingIsomorphism ; ::_thesis: P .: I is Ideal of S
A2: now__::_thesis:_for_p,_x_being_Element_of_S_st_x_in_P_.:_I_holds_
p_*_x_in_P_.:_I
let p, x be Element of S; ::_thesis: ( x in P .: I implies p * x in P .: I )
assume x in P .: I ; ::_thesis: p * x in P .: I
then consider x9 being set such that
A3: x9 in the carrier of R and
A4: x9 in I and
A5: x = P . x9 by FUNCT_2:64;
reconsider x9 = x9 as Element of R by A3;
A6: ( P is RingMonomorphism & P is RingEpimorphism ) by A1, QUOFIELD:def_21;
then rng P = the carrier of S by QUOFIELD:def_19;
then consider p9 being set such that
A7: p9 in dom P and
A8: p = P . p9 by FUNCT_1:def_3;
reconsider p9 = p9 as Element of R by A7;
A9: p9 * x9 in I by A4, IDEAL_1:def_2;
P is RingHomomorphism by A6, QUOFIELD:def_19;
then P is multiplicative by QUOFIELD:def_18;
then p * x = P . (p9 * x9) by A5, A8, GROUP_6:def_6;
hence p * x in P .: I by A9, FUNCT_2:35; ::_thesis: verum
end;
A10: now__::_thesis:_for_p,_x_being_Element_of_S_st_x_in_P_.:_I_holds_
x_*_p_in_P_.:_I
let p, x be Element of S; ::_thesis: ( x in P .: I implies x * p in P .: I )
assume x in P .: I ; ::_thesis: x * p in P .: I
then consider x9 being set such that
A11: x9 in the carrier of R and
A12: x9 in I and
A13: x = P . x9 by FUNCT_2:64;
reconsider x9 = x9 as Element of R by A11;
A14: ( P is RingMonomorphism & P is RingEpimorphism ) by A1, QUOFIELD:def_21;
then rng P = the carrier of S by QUOFIELD:def_19;
then consider p9 being set such that
A15: p9 in dom P and
A16: p = P . p9 by FUNCT_1:def_3;
reconsider p9 = p9 as Element of R by A15;
A17: x9 * p9 in I by A12, IDEAL_1:def_3;
P is RingHomomorphism by A14, QUOFIELD:def_19;
then P is multiplicative by QUOFIELD:def_18;
then x * p = P . (x9 * p9) by A13, A16, GROUP_6:def_6;
hence x * p in P .: I by A17, FUNCT_2:35; ::_thesis: verum
end;
now__::_thesis:_for_x,_y_being_Element_of_S_st_x_in_P_.:_I_&_y_in_P_.:_I_holds_
x_+_y_in_P_.:_I
let x, y be Element of S; ::_thesis: ( x in P .: I & y in P .: I implies x + y in P .: I )
assume that
A18: x in P .: I and
A19: y in P .: I ; ::_thesis: x + y in P .: I
consider x9 being set such that
A20: x9 in the carrier of R and
A21: x9 in I and
A22: x = P . x9 by A18, FUNCT_2:64;
consider y9 being set such that
A23: y9 in the carrier of R and
A24: y9 in I and
A25: y = P . y9 by A19, FUNCT_2:64;
reconsider x9 = x9, y9 = y9 as Element of R by A20, A23;
A26: x9 + y9 in I by A21, A24, IDEAL_1:def_1;
( P is RingMonomorphism & P is RingEpimorphism ) by A1, QUOFIELD:def_21;
then P is RingHomomorphism by QUOFIELD:def_19;
then P is additive by QUOFIELD:def_18;
then x + y = P . (x9 + y9) by A22, A25, VECTSP_1:def_20;
hence x + y in P .: I by A26, FUNCT_2:35; ::_thesis: verum
end;
hence P .: I is Ideal of S by A2, A10, IDEAL_1:def_1, IDEAL_1:def_2, IDEAL_1:def_3; ::_thesis: verum
end;
theorem Th23: :: HILBASIS:23
for R, S being non empty right_complementable add-associative right_zeroed doubleLoopStr
for f being Function of R,S st f is RingHomomorphism holds
f . (0. R) = 0. S
proof
let R, S be non empty right_complementable add-associative right_zeroed doubleLoopStr ; ::_thesis: for f being Function of R,S st f is RingHomomorphism holds
f . (0. R) = 0. S
let f be Function of R,S; ::_thesis: ( f is RingHomomorphism implies f . (0. R) = 0. S )
assume f is RingHomomorphism ; ::_thesis: f . (0. R) = 0. S
then A1: f is additive by QUOFIELD:def_18;
f . (0. R) = f . ((0. R) + (0. R)) by RLVECT_1:4
.= (f . (0. R)) + (f . (0. R)) by A1, VECTSP_1:def_20 ;
then 0. S = ((f . (0. R)) + (f . (0. R))) + (- (f . (0. R))) by RLVECT_1:def_10
.= (f . (0. R)) + ((f . (0. R)) + (- (f . (0. R)))) by RLVECT_1:def_3
.= (f . (0. R)) + (0. S) by RLVECT_1:def_10
.= f . (0. R) by RLVECT_1:4 ;
hence f . (0. R) = 0. S ; ::_thesis: verum
end;
theorem Th24: :: HILBASIS:24
for R, S being non empty right_complementable add-associative right_zeroed 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_3)) * (P . ((E /. i) `2_3))) * (P . ((E /. i) `3_3)) ) holds
P . (Sum lc) = Sum LC
proof
let R, S be non empty right_complementable add-associative right_zeroed doubleLoopStr ; ::_thesis: 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_3)) * (P . ((E /. i) `2_3))) * (P . ((E /. i) `3_3)) ) holds
P . (Sum lc) = Sum LC
let F be non empty Subset of R; ::_thesis: 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_3)) * (P . ((E /. i) `2_3))) * (P . ((E /. i) `3_3)) ) holds
P . (Sum lc) = Sum LC
let G be non empty Subset of S; ::_thesis: 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_3)) * (P . ((E /. i) `2_3))) * (P . ((E /. i) `3_3)) ) holds
P . (Sum lc) = Sum LC
let P be Function of R,S; ::_thesis: 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_3)) * (P . ((E /. i) `2_3))) * (P . ((E /. i) `3_3)) ) holds
P . (Sum lc) = Sum LC
let lc be LinearCombination of F; ::_thesis: 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_3)) * (P . ((E /. i) `2_3))) * (P . ((E /. i) `3_3)) ) holds
P . (Sum lc) = Sum LC
let LC be LinearCombination of G; ::_thesis: 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_3)) * (P . ((E /. i) `2_3))) * (P . ((E /. i) `3_3)) ) holds
P . (Sum lc) = Sum LC
let E be FinSequence of [: the carrier of R, the carrier of R, the carrier of R:]; ::_thesis: ( 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_3)) * (P . ((E /. i) `2_3))) * (P . ((E /. i) `3_3)) ) implies P . (Sum lc) = Sum LC )
assume that
A1: P is RingHomomorphism and
A2: len lc = len LC and
A3: E represents lc and
A4: for i being set st i in dom LC holds
LC . i = ((P . ((E /. i) `1_3)) * (P . ((E /. i) `2_3))) * (P . ((E /. i) `3_3)) ; ::_thesis: P . (Sum lc) = Sum LC
defpred S1[ Element of NAT ] means for lc9 being LinearCombination of F
for LC9 being LinearCombination of G st lc9 = lc | (Seg $1) & LC9 = LC | (Seg $1) holds
P . (Sum lc9) = Sum LC9;
A5: ( P is additive & P is multiplicative ) by A1, QUOFIELD:def_18;
A6: dom lc = dom LC by A2, FINSEQ_3:29;
A7: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A8: S1[k] ; ::_thesis: S1[k + 1]
thus S1[k + 1] ::_thesis: verum
proof
let lc9 be LinearCombination of F; ::_thesis: for LC9 being LinearCombination of G st lc9 = lc | (Seg (k + 1)) & LC9 = LC | (Seg (k + 1)) holds
P . (Sum lc9) = Sum LC9
let LC9 be LinearCombination of G; ::_thesis: ( lc9 = lc | (Seg (k + 1)) & LC9 = LC | (Seg (k + 1)) implies P . (Sum lc9) = Sum LC9 )
assume that
A9: lc9 = lc | (Seg (k + 1)) and
A10: LC9 = LC | (Seg (k + 1)) ; ::_thesis: P . (Sum lc9) = Sum LC9
percases ( len lc < k + 1 or len lc >= k + 1 ) ;
supposeA11: len lc < k + 1 ; ::_thesis: P . (Sum lc9) = Sum LC9
then A12: len lc <= k by NAT_1:13;
A13: lc9 = lc by A9, A11, FINSEQ_3:49
.= lc | (Seg k) by A12, FINSEQ_3:49 ;
LC9 = LC by A2, A10, A11, FINSEQ_3:49
.= LC | (Seg k) by A2, A12, FINSEQ_3:49 ;
hence P . (Sum lc9) = Sum LC9 by A8, A13; ::_thesis: verum
end;
supposeA14: len lc >= k + 1 ; ::_thesis: P . (Sum lc9) = Sum LC9
set i = k + 1;
reconsider LCk = LC | (Seg k) as LinearCombination of G by IDEAL_1:41;
reconsider lck = lc | (Seg k) as LinearCombination of F by IDEAL_1:41;
1 <= k + 1 by NAT_1:11;
then A15: k + 1 in dom lc by A14, FINSEQ_3:25;
then A16: lc . (k + 1) = lc /. (k + 1) by PARTFUN1:def_6;
A17: LC . (k + 1) = LC /. (k + 1) by A6, A15, PARTFUN1:def_6;
lc | (Seg (k + 1)) = lck ^ <*(lc . (k + 1))*> by A15, FINSEQ_5:10;
hence P . (Sum lc9) = P . ((Sum lck) + (lc /. (k + 1))) by A9, A16, FVSUM_1:71
.= (P . (Sum lck)) + (P . (lc /. (k + 1))) by A5, VECTSP_1:def_20
.= (Sum LCk) + (P . (lc /. (k + 1))) by A8
.= (Sum LCk) + (P . ((((E /. (k + 1)) `1_3) * ((E /. (k + 1)) `2_3)) * ((E /. (k + 1)) `3_3))) by A3, A15, A16, IDEAL_1:def_11
.= (Sum LCk) + ((P . (((E /. (k + 1)) `1_3) * ((E /. (k + 1)) `2_3))) * (P . ((E /. (k + 1)) `3_3))) by A5, GROUP_6:def_6
.= (Sum LCk) + (((P . ((E /. (k + 1)) `1_3)) * (P . ((E /. (k + 1)) `2_3))) * (P . ((E /. (k + 1)) `3_3))) by A5, GROUP_6:def_6
.= (Sum LCk) + (LC /. (k + 1)) by A4, A6, A15, A17
.= Sum (LCk ^ <*(LC /. (k + 1))*>) by FVSUM_1:71
.= Sum LC9 by A6, A10, A15, A17, FINSEQ_5:10 ;
::_thesis: verum
end;
end;
end;
end;
A18: ( lc = lc | (Seg (len lc)) & LC = LC | (Seg (len LC)) ) by FINSEQ_3:49;
A19: S1[ 0 ]
proof
let lc9 be LinearCombination of F; ::_thesis: for LC9 being LinearCombination of G st lc9 = lc | (Seg 0) & LC9 = LC | (Seg 0) holds
P . (Sum lc9) = Sum LC9
let LC9 be LinearCombination of G; ::_thesis: ( lc9 = lc | (Seg 0) & LC9 = LC | (Seg 0) implies P . (Sum lc9) = Sum LC9 )
assume that
A20: lc9 = lc | (Seg 0) and
A21: LC9 = LC | (Seg 0) ; ::_thesis: P . (Sum lc9) = Sum LC9
thus P . (Sum lc9) = P . (Sum (<*> the carrier of R)) by A20
.= P . (0. R) by RLVECT_1:43
.= 0. S by A1, Th23
.= Sum (<*> the carrier of S) by RLVECT_1:43
.= Sum LC9 by A21 ; ::_thesis: verum
end;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(A19, A7);
hence P . (Sum lc) = Sum LC by A2, A18; ::_thesis: verum
end;
theorem Th25: :: HILBASIS:25
for R, S being non empty doubleLoopStr
for P being Function of R,S st P is RingIsomorphism holds
P " is RingIsomorphism
proof
let R, S be non empty doubleLoopStr ; ::_thesis: for P being Function of R,S st P is RingIsomorphism holds
P " is RingIsomorphism
let P be Function of R,S; ::_thesis: ( P is RingIsomorphism implies P " is RingIsomorphism )
assume A1: P is RingIsomorphism ; ::_thesis: P " is RingIsomorphism
then A2: P is RingEpimorphism by QUOFIELD:def_21;
then A3: rng P = the carrier of S by QUOFIELD:def_19;
P is RingMonomorphism by A1, QUOFIELD:def_21;
then A4: P is one-to-one by QUOFIELD:def_20;
P is RingHomomorphism by A2, QUOFIELD:def_19;
then A5: ( P is additive & P is multiplicative & P is unity-preserving ) by QUOFIELD:def_18;
for x, y being Element of S holds
( (P ") . (x + y) = ((P ") . x) + ((P ") . y) & (P ") . (x * y) = ((P ") . x) * ((P ") . y) & (P ") . (1_ S) = 1_ R )
proof
A6: P is onto by A3, FUNCT_2:def_3;
A7: (P ") . (1_ S) = (P ") . (P . (1_ R)) by A5, GROUP_1:def_13
.= (P ") . (P . (1_ R)) by A4, A6, TOPS_2:def_4
.= 1_ R by A4, FUNCT_2:26 ;
let x, y be Element of S; ::_thesis: ( (P ") . (x + y) = ((P ") . x) + ((P ") . y) & (P ") . (x * y) = ((P ") . x) * ((P ") . y) & (P ") . (1_ S) = 1_ R )
consider x9 being set such that
A8: x9 in the carrier of R and
A9: P . x9 = x by A3, FUNCT_2:11;
reconsider x9 = x9 as Element of R by A8;
A10: x9 = (P ") . (P . x9) by A4, FUNCT_2:26
.= (P ") . x by A4, A9, A6, TOPS_2:def_4 ;
consider y9 being set such that
A11: y9 in the carrier of R and
A12: P . y9 = y by A3, FUNCT_2:11;
reconsider y9 = y9 as Element of R by A11;
A13: y9 = (P ") . (P . y9) by A4, FUNCT_2:26
.= (P ") . y by A6, A4, A12, TOPS_2:def_4 ;
A14: (P ") . (x * y) = (P ") . (P . (x9 * y9)) by A5, A9, A12, GROUP_6:def_6
.= (P ") . (P . (x9 * y9)) by A4, A6, TOPS_2:def_4
.= ((P ") . x) * ((P ") . y) by A4, A10, A13, FUNCT_2:26 ;
(P ") . (x + y) = (P ") . (P . (x9 + y9)) by A5, A9, A12, VECTSP_1:def_20
.= (P ") . (P . (x9 + y9)) by A4, A6, TOPS_2:def_4
.= ((P ") . x) + ((P ") . y) by A4, A10, A13, FUNCT_2:26 ;
hence ( (P ") . (x + y) = ((P ") . x) + ((P ") . y) & (P ") . (x * y) = ((P ") . x) * ((P ") . y) & (P ") . (1_ S) = 1_ R ) by A14, A7; ::_thesis: verum
end;
then ( P " is additive & P " is multiplicative & P " is unity-preserving ) by VECTSP_1:def_20, GROUP_1:def_13, GROUP_6:def_6;
then A15: P " is RingHomomorphism by QUOFIELD:def_18;
A16: rng P = [#] S by A2, QUOFIELD:def_19;
then rng (P ") = [#] R by A4, TOPS_2:49
.= the carrier of R ;
then A17: P " is RingEpimorphism by A15, QUOFIELD:def_19;
P " is one-to-one by A4, A16, TOPS_2:50;
then P " is RingMonomorphism by A15, QUOFIELD:def_20;
hence P " is RingIsomorphism by A17, QUOFIELD:def_21; ::_thesis: verum
end;
theorem Th26: :: HILBASIS:26
for R, S being non empty right_complementable Abelian add-associative right_zeroed associative well-unital 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
let R, S be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: 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
let F be non empty Subset of R; ::_thesis: for P being Function of R,S st P is RingIsomorphism holds
P .: (F -Ideal) = (P .: F) -Ideal
let P be Function of R,S; ::_thesis: ( P is RingIsomorphism implies P .: (F -Ideal) = (P .: F) -Ideal )
assume A1: P is RingIsomorphism ; ::_thesis: P .: (F -Ideal) = (P .: F) -Ideal
now__::_thesis:_for_x_being_set_st_x_in_(P_.:_F)_-Ideal_holds_
x_in_P_.:_(F_-Ideal)
let x be set ; ::_thesis: ( x in (P .: F) -Ideal implies x in P .: (F -Ideal) )
A2: dom P = the carrier of R by FUNCT_2:def_1;
assume A3: x in (P .: F) -Ideal ; ::_thesis: x in P .: (F -Ideal)
then consider lc being LinearCombination of P .: F such that
A4: x = Sum lc by IDEAL_1:60;
consider E being FinSequence of [: the carrier of S, the carrier of S, the carrier of S:] such that
A5: E represents lc by IDEAL_1:35;
P is RingMonomorphism by A1, QUOFIELD:def_21;
then A6: P is one-to-one by QUOFIELD:def_20;
P is RingEpimorphism by A1, QUOFIELD:def_21;
then A7: rng P = the carrier of S by QUOFIELD:def_19;
then P is onto by FUNCT_2:def_3;
then A8: P " = P " by A6, TOPS_2:def_4;
(P ") .: (P .: F) = P " (P .: F) by A6, FUNCT_1:85;
then consider lc9 being LinearCombination of F such that
A9: ( len lc = len lc9 & ( for i being set st i in dom lc9 holds
lc9 . i = (((P ") . ((E /. i) `1_3)) * ((P ") . ((E /. i) `2_3))) * ((P ") . ((E /. i) `3_3)) ) ) by A6, A8, A5, FUNCT_1:82, IDEAL_1:36;
P " is RingIsomorphism by A1, Th25;
then P " is RingMonomorphism by QUOFIELD:def_21;
then P " is RingHomomorphism by QUOFIELD:def_20;
then (P ") . x = Sum lc9 by A4, A5, A9, Th24;
then (P ") . x in F -Ideal by IDEAL_1:60;
then P . ((P ") . x) in P .: (F -Ideal) by A2, FUNCT_1:def_6;
hence x in P .: (F -Ideal) by A3, A6, A7, A8, FUNCT_1:35; ::_thesis: verum
end;
then A10: (P .: F) -Ideal c= P .: (F -Ideal) by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_P_.:_(F_-Ideal)_holds_
x_in_(P_.:_F)_-Ideal
let x be set ; ::_thesis: ( x in P .: (F -Ideal) implies x in (P .: F) -Ideal )
assume x in P .: (F -Ideal) ; ::_thesis: x in (P .: F) -Ideal
then consider x9 being set such that
x9 in the carrier of R and
A11: x9 in F -Ideal and
A12: x = P . x9 by FUNCT_2:64;
consider lc9 being LinearCombination of F such that
A13: x9 = Sum lc9 by A11, IDEAL_1:60;
consider E being FinSequence of [: the carrier of R, the carrier of R, the carrier of R:] such that
A14: E represents lc9 by IDEAL_1:35;
consider lc being LinearCombination of P .: F such that
A15: ( len lc9 = len lc & ( for i being set st i in dom lc holds
lc . i = ((P . ((E /. i) `1_3)) * (P . ((E /. i) `2_3))) * (P . ((E /. i) `3_3)) ) ) by A14, IDEAL_1:36;
P is RingMonomorphism by A1, QUOFIELD:def_21;
then P is RingHomomorphism by QUOFIELD:def_20;
then x = Sum lc by A12, A13, A14, A15, Th24;
hence x in (P .: F) -Ideal by IDEAL_1:60; ::_thesis: verum
end;
then P .: (F -Ideal) c= (P .: F) -Ideal by TARSKI:def_3;
hence P .: (F -Ideal) = (P .: F) -Ideal by A10, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th27: :: HILBASIS:27
for R, S being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for P being Function of R,S st P is RingIsomorphism & R is Noetherian holds
S is Noetherian
proof
let R, S be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for P being Function of R,S st P is RingIsomorphism & R is Noetherian holds
S is Noetherian
let P be Function of R,S; ::_thesis: ( P is RingIsomorphism & R is Noetherian implies S is Noetherian )
assume that
A1: P is RingIsomorphism and
A2: R is Noetherian ; ::_thesis: S is Noetherian
now__::_thesis:_for_I_being_Ideal_of_S_holds_I_is_finitely_generated
P is RingEpimorphism by A1, QUOFIELD:def_21;
then A3: rng P = the carrier of S by QUOFIELD:def_19;
let I be Ideal of S; ::_thesis: I is finitely_generated
P is RingMonomorphism by A1, QUOFIELD:def_21;
then A4: P is one-to-one by QUOFIELD:def_20;
reconsider PI = (P ") .: I as Ideal of R by A1, Th22, Th25;
PI is finitely_generated by A2, IDEAL_1:def_26;
then consider F being non empty finite Subset of R such that
A5: (P ") .: I = F -Ideal by IDEAL_1:def_25;
P is onto by A3, FUNCT_2:def_3;
then P " = P " by A4, TOPS_2:def_4;
then P .: ((P ") .: I) = P .: (P " I) by A4, FUNCT_1:85;
then P .: ((P ") .: I) = I by A3, FUNCT_1:77;
then I = (P .: F) -Ideal by A1, A5, Th26;
hence I is finitely_generated ; ::_thesis: verum
end;
hence S is Noetherian by IDEAL_1:def_26; ::_thesis: verum
end;
theorem Th28: :: HILBASIS:28
for R being non trivial right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ex P being Function of R,(Polynom-Ring (0,R)) st P is RingIsomorphism
proof
deffunc H1( set ) -> Element of bool [:(Bags {}),{$1}:] = (Bags {}) --> $1;
let R be non trivial right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: ex P being Function of R,(Polynom-Ring (0,R)) st P is RingIsomorphism
consider P being Function such that
A1: dom P = the carrier of R and
A2: for x being set st x in the carrier of R holds
P . x = H1(x) from FUNCT_1:sch_3();
now__::_thesis:_for_y_being_set_holds_
(_(_y_in_rng_P_implies_y_in_the_carrier_of_(Polynom-Ring_(0,R))_)_&_(_y_in_the_carrier_of_(Polynom-Ring_(0,R))_implies_y_in_rng_P_)_)
let y be set ; ::_thesis: ( ( y in rng P implies y in the carrier of (Polynom-Ring (0,R)) ) & ( y in the carrier of (Polynom-Ring (0,R)) implies y in rng P ) )
hereby ::_thesis: ( y in the carrier of (Polynom-Ring (0,R)) implies y in rng P )
assume y in rng P ; ::_thesis: y in the carrier of (Polynom-Ring (0,R))
then consider x being set such that
A3: x in the carrier of R and
A4: y = P . x by A1, FUNCT_1:def_3;
reconsider x = x as Element of R by A3;
reconsider y9 = (Bags {}) --> x as Function of (Bags {}),R ;
Support y9 is finite by PRE_POLY:51;
then y9 is finite-Support Series of 0,R by POLYNOM1:def_4;
then y9 in the carrier of (Polynom-Ring (0,R)) by POLYNOM1:def_10;
hence y in the carrier of (Polynom-Ring (0,R)) by A2, A4; ::_thesis: verum
end;
assume y in the carrier of (Polynom-Ring (0,R)) ; ::_thesis: y in rng P
then reconsider y9 = y as Function of (Bags {}),R by POLYNOM1:def_10;
A5: dom y9 = Bags {} by FUNCT_2:def_1;
then A6: rng y9 = {(y9 . {})} by FUNCT_1:4, PRE_POLY:51;
then y9 . {} in rng y9 by TARSKI:def_1;
then reconsider x = y9 . {} as Element of R ;
y9 = (Bags {}) --> (y9 . {}) by A5, A6, FUNCOP_1:9;
then y = P . x by A2;
hence y in rng P by A1, FUNCT_1:def_3; ::_thesis: verum
end;
then A7: rng P = the carrier of (Polynom-Ring (0,R)) by TARSKI:1;
then reconsider P = P as Function of R,(Polynom-Ring (0,R)) by A1, FUNCT_2:1;
A8: EmptyBag {} = {} --> 0 ;
now__::_thesis:_for_x,_y_being_Element_of_R_holds_(P_._x)_+_(P_._y)_=_P_._(x_+_y)
let x, y be Element of R; ::_thesis: (P . x) + (P . y) = P . (x + y)
reconsider Px = P . x, Py = P . y, Pxy = P . (x + y) as Polynomial of 0,R by POLYNOM1:def_10;
now__::_thesis:_for_z_being_bag_of_0_holds_Pxy_._z_=_(Px_._z)_+_(Py_._z)
let z be bag of 0 ; ::_thesis: Pxy . z = (Px . z) + (Py . z)
A9: z in Bags {} by PRE_POLY:def_12;
A10: Py . z = ((Bags {}) --> y) . z by A2
.= y by A9, FUNCOP_1:7 ;
A11: Px . z = ((Bags {}) --> x) . z by A2
.= x by A9, FUNCOP_1:7 ;
Pxy . z = ((Bags {}) --> (x + y)) . z by A2
.= x + y by A9, FUNCOP_1:7 ;
hence Pxy . z = (Px . z) + (Py . z) by A11, A10; ::_thesis: verum
end;
then Pxy = Px + Py by POLYNOM1:16;
hence (P . x) + (P . y) = P . (x + y) by POLYNOM1:def_10; ::_thesis: verum
end;
then A12: P is additive by VECTSP_1:def_20;
now__::_thesis:_for_x,_y_being_Element_of_R_holds_(P_._x)_*_(P_._y)_=_P_._(x_*_y)
let x, y be Element of R; ::_thesis: (P . x) * (P . y) = P . (x * y)
reconsider Px = P . x, Py = P . y, Pxy = P . (x * y) as Polynomial of 0,R by POLYNOM1:def_10;
now__::_thesis:_for_b_being_bag_of_0_ex_s_being_FinSequence_of_the_carrier_of_R_st_
(_Pxy_._b_=_Sum_s_&_len_s_=_len_(decomp_b)_&_(_for_k_being_Element_of_NAT_st_k_in_dom_s_holds_
ex_b1,_b2_being_bag_of_0_st_
(_(decomp_b)_/._k_=_<*b1,b2*>_&_s_/._k_=_(Px_._b1)_*_(Py_._b2)_)_)_)
reconsider s = <*(x * y)*> as FinSequence of the carrier of R ;
let b be bag of 0 ; ::_thesis: ex s being FinSequence of the carrier of R st
( Pxy . b = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of 0 st
( (decomp b) /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) ) ) )
take s = s; ::_thesis: ( Pxy . b = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of 0 st
( (decomp b) /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) ) ) )
A13: b in Bags {} by PRE_POLY:def_12;
thus Pxy . b = ((Bags {}) --> (x * y)) . b by A2
.= x * y by A13, FUNCOP_1:7
.= Sum s by RLVECT_1:44 ; ::_thesis: ( len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of 0 st
( (decomp b) /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) ) ) )
A14: decomp b = <*<*{},{}*>*> by Th2;
A15: len s = 1 by FINSEQ_1:39;
hence len s = len (decomp b) by A14, FINSEQ_1:39; ::_thesis: for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of 0 st
( (decomp b) /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) )
A16: len (decomp b) = 1 by A14, FINSEQ_1:39;
now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_s_holds_
ex_b1,_b2_being_bag_of_0_st_
(_(decomp_b)_/._k_=_<*b1,b2*>_&_s_/._k_=_(Px_._b1)_*_(Py_._b2)_)
set b1 = {} ;
set b2 = {} ;
let k be Element of NAT ; ::_thesis: ( k in dom s implies ex b1, b2 being bag of 0 st
( (decomp b) /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) ) )
A17: {} in Bags {} by PRE_POLY:51, TARSKI:def_1;
then reconsider b1 = {} , b2 = {} as bag of 0 ;
A18: Px . b1 = ((Bags {}) --> x) . b1 by A2
.= x by A17, FUNCOP_1:7 ;
A19: Py . b2 = ((Bags {}) --> y) . b2 by A2
.= y by A17, FUNCOP_1:7 ;
assume A20: k in dom s ; ::_thesis: ex b1, b2 being bag of 0 st
( (decomp b) /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) )
then A21: ( 1 <= k & k <= 1 ) by A15, FINSEQ_3:25;
then A22: k = 1 by XXREAL_0:1;
take b1 = b1; ::_thesis: ex b2 being bag of 0 st
( (decomp b) /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) )
take b2 = b2; ::_thesis: ( (decomp b) /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) )
k in dom (decomp b) by A16, A21, FINSEQ_3:25;
hence (decomp b) /. k = (decomp b) . 1 by A22, PARTFUN1:def_6
.= <*b1,b2*> by A14, FINSEQ_1:40 ;
::_thesis: s /. k = (Px . b1) * (Py . b2)
thus s /. k = s . 1 by A20, A22, PARTFUN1:def_6
.= (Px . b1) * (Py . b2) by A18, A19, FINSEQ_1:40 ; ::_thesis: verum
end;
hence for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of 0 st
( (decomp b) /. k = <*b1,b2*> & s /. k = (Px . b1) * (Py . b2) ) ; ::_thesis: verum
end;
then Pxy = Px *' Py by POLYNOM1:def_9;
hence (P . x) * (P . y) = P . (x * y) by POLYNOM1:def_10; ::_thesis: verum
end;
then A23: P is multiplicative by GROUP_6:def_6;
take P ; ::_thesis: P is RingIsomorphism
reconsider f0 = {{}} --> (0. R), f1 = {{}} --> (1_ R) as Function of {{}}, the carrier of R ;
A24: dom f1 = {{}} by FUNCT_2:def_1;
A25: dom f0 = {{}} by FUNCT_2:def_1;
then A26: {} in dom ({{}} --> (0. R)) by TARSKI:def_1;
1_ (Polynom-Ring (0,R)) = 1_ (0,R) by POLYNOM1:31
.= (0_ (0,R)) +* ({},(1_ R)) by A8, POLYNOM1:def_8
.= ({{}} --> (0. R)) +* ({},(1_ R)) by POLYNOM1:def_7, PRE_POLY:51
.= ({{}} --> (0. R)) +* ({} .--> (1_ R)) by A26, FUNCT_7:def_3
.= {{}} --> (1_ R) by A25, A24, FUNCT_4:19
.= P . (1_ R) by A2, PRE_POLY:51 ;
then P is unity-preserving by GROUP_1:def_13;
then A27: P is RingHomomorphism by A12, A23, QUOFIELD:def_18;
then A28: P is RingEpimorphism by A7, QUOFIELD:def_19;
now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_P_&_x2_in_dom_P_&_P_._x1_=_P_._x2_holds_
x1_=_x2
let x1, x2 be set ; ::_thesis: ( x1 in dom P & x2 in dom P & P . x1 = P . x2 implies x1 = x2 )
assume that
A29: x1 in dom P and
A30: x2 in dom P ; ::_thesis: ( P . x1 = P . x2 implies x1 = x2 )
assume P . x1 = P . x2 ; ::_thesis: x1 = x2
then (Bags {}) --> x1 = P . x2 by A2, A29;
then (Bags {}) --> x1 = (Bags {}) --> x2 by A2, A30;
hence x1 = x2 by FUNCT_4:6; ::_thesis: verum
end;
then P is one-to-one by FUNCT_1:def_4;
then P is RingMonomorphism by A27, QUOFIELD:def_20;
hence P is RingIsomorphism by A28, QUOFIELD:def_21; ::_thesis: verum
end;
theorem Th29: :: HILBASIS:29
for R being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for n being Element of 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
let R be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; ::_thesis: for n being Element of 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) )
let n be Element of NAT ; ::_thesis: 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) )
let b be bag of n; ::_thesis: 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) )
let p1 be Polynomial of n,R; ::_thesis: 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) )
let F be FinSequence of the carrier of (Polynom-Ring (n,R)); ::_thesis: ( p1 = Sum F implies 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) ) )
assume A1: p1 = Sum F ; ::_thesis: 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) )
set CR = the carrier of R;
set PNR = Polynom-Ring (n,R);
set CPNR = the carrier of (Polynom-Ring (n,R));
defpred S1[ Element of the carrier of (Polynom-Ring (n,R)), Element of the carrier of R] means for p being Polynomial of n,R st p = $1 holds
$2 = p . b;
A2: now__::_thesis:_for_x_being_Element_of_the_carrier_of_(Polynom-Ring_(n,R))_ex_y_being_Element_of_the_carrier_of_R_st_S1[x,y]
let x be Element of the carrier of (Polynom-Ring (n,R)); ::_thesis: ex y being Element of the carrier of R st S1[x,y]
reconsider x9 = x as Polynomial of n,R by POLYNOM1:def_10;
S1[x,x9 . b] ;
hence ex y being Element of the carrier of R st S1[x,y] ; ::_thesis: verum
end;
consider g being Function of the carrier of (Polynom-Ring (n,R)), the carrier of R such that
A3: for x being Element of the carrier of (Polynom-Ring (n,R)) holds S1[x,g . x] from FUNCT_2:sch_3(A2);
take g ; ::_thesis: ( ( for p being Polynomial of n,R holds g . p = p . b ) & p1 . b = Sum (g * F) )
now__::_thesis:_for_p_being_Polynomial_of_n,R_holds_g_._p_=_p_._b
let p be Polynomial of n,R; ::_thesis: g . p = p . b
reconsider p9 = p as Element of the carrier of (Polynom-Ring (n,R)) by POLYNOM1:def_10;
S1[p9,g . p9] by A3;
hence g . p = p . b ; ::_thesis: verum
end;
hence for p being Polynomial of n,R holds g . p = p . b ; ::_thesis: p1 . b = Sum (g * F)
defpred S2[ Nat] means for F9 being FinSequence of the carrier of (Polynom-Ring (n,R))
for p19 being Polynomial of n,R st len F9 <= $1 & p19 = Sum F9 holds
p19 . b = Sum (g * F9);
A4: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] )
assume A5: S2[k] ; ::_thesis: S2[k + 1]
now__::_thesis:_for_F9_being_FinSequence_of_the_carrier_of_(Polynom-Ring_(n,R))
for_p19_being_Polynomial_of_n,R_st_len_F9_<=_k_+_1_&_p19_=_Sum_F9_holds_
p19_._b_=_Sum_(g_*_F9)
let F9 be FinSequence of the carrier of (Polynom-Ring (n,R)); ::_thesis: for p19 being Polynomial of n,R st len F9 <= k + 1 & p19 = Sum F9 holds
b3 . b = Sum (g * b2)
let p19 be Polynomial of n,R; ::_thesis: ( len F9 <= k + 1 & p19 = Sum F9 implies b2 . b = Sum (g * b1) )
assume that
A6: len F9 <= k + 1 and
A7: p19 = Sum F9 ; ::_thesis: b2 . b = Sum (g * b1)
percases ( len F9 < k + 1 or len F9 >= k + 1 ) ;
suppose len F9 < k + 1 ; ::_thesis: b2 . b = Sum (g * b1)
then len F9 <= k by NAT_1:13;
hence p19 . b = Sum (g * F9) by A5, A7; ::_thesis: verum
end;
suppose len F9 >= k + 1 ; ::_thesis: b2 . b = Sum (g * b1)
then len F9 = k + 1 by A6, XXREAL_0:1;
then consider p, q being FinSequence such that
A8: len p = k and
A9: len q = 1 and
A10: F9 = p ^ q by FINSEQ_2:22;
rng q c= rng F9 by A10, FINSEQ_1:30;
then rng q c= the carrier of (Polynom-Ring (n,R)) by XBOOLE_1:1;
then reconsider q = q as FinSequence of the carrier of (Polynom-Ring (n,R)) by FINSEQ_1:def_4;
rng p c= rng F9 by A10, FINSEQ_1:29;
then rng p c= the carrier of (Polynom-Ring (n,R)) by XBOOLE_1:1;
then reconsider p = p as FinSequence of the carrier of (Polynom-Ring (n,R)) by FINSEQ_1:def_4;
A11: Sum F9 = (Sum p) + (Sum q) by A10, RLVECT_1:41;
reconsider p9 = Sum p as Polynomial of n,R by POLYNOM1:def_10;
A12: g * F9 = (g * p) ^ (g * q) by A10, FINSEQOP:9;
1 in dom q by A9, FINSEQ_3:25;
then q . 1 in rng q by FUNCT_1:def_3;
then reconsider q9 = q . 1 as Element of the carrier of (Polynom-Ring (n,R)) ;
reconsider q99 = q9 as Polynomial of n,R by POLYNOM1:def_10;
A13: q = <*q9*> by A9, FINSEQ_1:40;
then g * q = <*(g . q9)*> by FINSEQ_2:35
.= <*(q99 . b)*> by A3 ;
then A14: Sum (g * q) = q99 . b by RLVECT_1:44;
q9 = Sum q by A13, RLVECT_1:44;
then A15: p19 = p9 + q99 by A7, A11, POLYNOM1:def_10;
p9 . b = Sum (g * p) by A5, A8;
hence p19 . b = (Sum (g * p)) + (Sum (g * q)) by A14, A15, POLYNOM1:15
.= Sum (g * F9) by A12, RLVECT_1:41 ;
::_thesis: verum
end;
end;
end;
hence S2[k + 1] ; ::_thesis: verum
end;
A16: S2[ 0 ]
proof
let F9 be FinSequence of the carrier of (Polynom-Ring (n,R)); ::_thesis: for p19 being Polynomial of n,R st len F9 <= 0 & p19 = Sum F9 holds
p19 . b = Sum (g * F9)
let p19 be Polynomial of n,R; ::_thesis: ( len F9 <= 0 & p19 = Sum F9 implies p19 . b = Sum (g * F9) )
assume that
A17: len F9 <= 0 and
A18: p19 = Sum F9 ; ::_thesis: p19 . b = Sum (g * F9)
A19: F9 = <*> the carrier of (Polynom-Ring (n,R)) by A17;
then g * F9 = <*> the carrier of R ;
then A20: Sum (g * F9) = 0. R by RLVECT_1:43;
p19 = 0. (Polynom-Ring (n,R)) by A18, A19, RLVECT_1:43
.= 0_ (n,R) by POLYNOM1:def_10 ;
hence p19 . b = Sum (g * F9) by A20, POLYNOM1:22; ::_thesis: verum
end;
for k being Element of NAT holds S2[k] from NAT_1:sch_1(A16, A4);
then S2[ len F] ;
hence p1 . b = Sum (g * F) by A1; ::_thesis: verum
end;
definition
let R be non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ;
let n be Element of 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
set CR = the carrier of R;
set PNR = Polynom-Ring (n,R);
set PN1R = Polynom-Ring ((n + 1),R);
set PRPNR = Polynom-Ring (Polynom-Ring (n,R));
set CPRPNR = the carrier of (Polynom-Ring (Polynom-Ring (n,R)));
set CPN1R = the carrier of (Polynom-Ring ((n + 1),R));
defpred S1[ Element of the carrier of (Polynom-Ring (Polynom-Ring (n,R))), Element of the carrier of (Polynom-Ring ((n + 1),R))] means 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 p1 = $1 & p3 = $2 & p2 = p1 . (b . n) holds
p3 . b = p2 . (b | n);
A1: now__::_thesis:_for_x_being_Element_of_the_carrier_of_(Polynom-Ring_(Polynom-Ring_(n,R)))_ex_y_being_Element_of_the_carrier_of_(Polynom-Ring_((n_+_1),R))_st_S1[x,y]
let x be Element of the carrier of (Polynom-Ring (Polynom-Ring (n,R))); ::_thesis: ex y being Element of the carrier of (Polynom-Ring ((n + 1),R)) st S1[x,y]
reconsider p1 = x as Polynomial of (Polynom-Ring (n,R)) by POLYNOM3:def_10;
defpred S2[ Element of Bags (n + 1), Element of the carrier of R] means for p2 being Polynomial of n,R st p2 = p1 . ($1 . n) holds
$2 = p2 . ($1 | n);
deffunc H1( set ) -> set = { b where b is Element of Bags (n + 1) : ( b . n = $1 & ( for p2 being Polynomial of n,R st p2 = p1 . $1 holds
b | n in Support p2 ) ) } ;
A2: now__::_thesis:_for_k_being_set_st_k_in_NAT_holds_
H1(k)_in_bool_(Bags_(n_+_1))
let k be set ; ::_thesis: ( k in NAT implies H1(k) in bool (Bags (n + 1)) )
assume k in NAT ; ::_thesis: H1(k) in bool (Bags (n + 1))
set Ak = H1(k);
H1(k) c= Bags (n + 1)
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in H1(k) or b in Bags (n + 1) )
assume b in H1(k) ; ::_thesis: b in Bags (n + 1)
then ex b9 being Element of Bags (n + 1) st
( b9 = b & b9 . n = k & ( for p2 being Polynomial of n,R st p2 = p1 . k holds
b9 | n in Support p2 ) ) ;
hence b in Bags (n + 1) ; ::_thesis: verum
end;
hence H1(k) in bool (Bags (n + 1)) ; ::_thesis: verum
end;
consider A being Function of NAT,(bool (Bags (n + 1))) such that
A3: for k being set st k in NAT holds
A . k = H1(k) from FUNCT_2:sch_2(A2);
now__::_thesis:_for_X_being_set_st_X_in_A_.:_(len_p1)_holds_
X_is_finite
let X be set ; ::_thesis: ( X in A .: (len p1) implies b1 is finite )
assume X in A .: (len p1) ; ::_thesis: b1 is finite
then consider k being Element of NAT such that
k in len p1 and
A4: X = A . k by FUNCT_2:65;
reconsider p2 = p1 . k as Polynomial of n,R by POLYNOM1:def_10;
A5: A . k = { b where b is Element of Bags (n + 1) : ( b . n = k & ( for p2 being Polynomial of n,R st p2 = p1 . k holds
b | n in Support p2 ) ) } by A3;
percases ( Support p2 = {} or Support p2 <> {} ) ;
supposeA6: Support p2 = {} ; ::_thesis: b1 is finite
now__::_thesis:_not_A_._k_<>_{}
assume A . k <> {} ; ::_thesis: contradiction
then consider b being set such that
A7: b in A . k by XBOOLE_0:def_1;
ex b9 being Element of Bags (n + 1) st
( b9 = b & b9 . n = k & ( for p2 being Polynomial of n,R st p2 = p1 . k holds
b9 | n in Support p2 ) ) by A5, A7;
hence contradiction by A6; ::_thesis: verum
end;
hence X is finite by A4; ::_thesis: verum
end;
supposeA8: Support p2 <> {} ; ::_thesis: b1 is finite
then consider b2 being set such that
A9: b2 in Support p2 by XBOOLE_0:def_1;
reconsider b2 = b2 as Element of Bags n by A9;
A10: (b2 bag_extend k) . n = k by Def1;
for p2 being Polynomial of n,R st p2 = p1 . k holds
(b2 bag_extend k) | n in Support p2 by A9, Def1;
then b2 bag_extend k in A . k by A5, A10;
then reconsider Ak = A . k as non empty set ;
reconsider Supportp2 = Support p2 as non empty set by A8;
defpred S3[ Element of Ak, Element of Supportp2] means for b being Element of Bags (n + 1) st $1 = b holds
$2 = b | n;
A11: now__::_thesis:_for_x_being_Element_of_Ak_ex_y_being_Element_of_Supportp2_st_S3[x,y]
let x be Element of Ak; ::_thesis: ex y being Element of Supportp2 st S3[x,y]
x in A . k ;
then consider b being Element of Bags (n + 1) such that
A12: b = x and
b . n = k and
A13: for p2 being Polynomial of n,R st p2 = p1 . k holds
b | n in Support p2 by A5;
reconsider bn = b | n as Element of Supportp2 by A13;
S3[x,bn] by A12;
hence ex y being Element of Supportp2 st S3[x,y] ; ::_thesis: verum
end;
consider f being Function of Ak,Supportp2 such that
A14: for x being Element of Ak holds S3[x,f . x] from FUNCT_2:sch_3(A11);
A15: dom f = Ak by FUNCT_2:def_1;
now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_f_&_x2_in_dom_f_&_f_._x1_=_f_._x2_holds_
x1_=_x2
let x1, x2 be set ; ::_thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A16: x1 in dom f and
A17: x2 in dom f and
A18: f . x1 = f . x2 ; ::_thesis: x1 = x2
f . x1 in Supportp2 by A16, FUNCT_2:5;
then reconsider fx1 = f . x1 as Element of Bags n ;
consider b1 being Element of Bags (n + 1) such that
A19: b1 = x1 and
A20: b1 . n = k and
for p2 being Polynomial of n,R st p2 = p1 . k holds
b1 | n in Support p2 by A5, A15, A16;
b1 | n = f . x1 by A14, A16, A19;
then A21: b1 = fx1 bag_extend k by A20, Def1;
consider b2 being Element of Bags (n + 1) such that
A22: b2 = x2 and
A23: b2 . n = k and
for p2 being Polynomial of n,R st p2 = p1 . k holds
b2 | n in Support p2 by A5, A15, A17;
b2 | n = f . x1 by A14, A17, A18, A22;
hence x1 = x2 by A19, A21, A22, A23, Def1; ::_thesis: verum
end;
then A24: f is one-to-one by FUNCT_1:def_4;
rng f c= Supportp2 ;
then card Ak c= card Supportp2 by A15, A24, CARD_1:10;
hence X is finite by A4; ::_thesis: verum
end;
end;
end;
then A25: union (A .: (len p1)) is finite by FINSET_1:7;
A26: now__::_thesis:_for_b_being_Element_of_Bags_(n_+_1)_ex_r_being_Element_of_the_carrier_of_R_st_S2[b,r]
let b be Element of Bags (n + 1); ::_thesis: ex r being Element of the carrier of R st S2[b,r]
reconsider p2 = p1 . (b . n) as Polynomial of n,R by POLYNOM1:def_10;
n < n + 1 by XREAL_1:29;
then reconsider bn = b | n as bag of n by Th3;
S2[b,p2 . bn] ;
hence ex r being Element of the carrier of R st S2[b,r] ; ::_thesis: verum
end;
consider y being Function of (Bags (n + 1)), the carrier of R such that
A27: for b being Element of Bags (n + 1) holds S2[b,y . b] from FUNCT_2:sch_3(A26);
reconsider y = y as Function of (Bags (n + 1)),R ;
reconsider y = y as Series of (n + 1),R ;
Support y c= union (A .: (len p1))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Support y or x in union (A .: (len p1)) )
A28: dom A = NAT by FUNCT_2:def_1;
assume A29: x in Support y ; ::_thesis: x in union (A .: (len p1))
then reconsider x9 = x as Element of Bags (n + 1) ;
reconsider p2 = p1 . (x9 . n) as Polynomial of n,R by POLYNOM1:def_10;
n < n + 1 by XREAL_1:29;
then reconsider xn = x9 | n as Element of Bags n by Th3;
y . x9 <> 0. R by A29, POLYNOM1:def_3;
then A30: p2 . xn <> 0. R by A27;
then p2 <> 0_ (n,R) by POLYNOM1:22;
then p2 <> 0. (Polynom-Ring (n,R)) by POLYNOM1:def_10;
then A31: x9 . n < len p1 by ALGSEQ_1:8;
len p1 = { i where i is Element of NAT : i < len p1 } by AXIOMS:4;
then x9 . n in len p1 by A31;
then A32: A . (x9 . n) in A .: (len p1) by A28, FUNCT_1:def_6;
A33: A . (x9 . n) = { b where b is Element of Bags (n + 1) : ( b . n = x9 . n & ( for p2 being Polynomial of n,R st p2 = p1 . (x9 . n) holds
b | n in Support p2 ) ) } by A3;
for p2 being Polynomial of n,R st p2 = p1 . (x9 . n) holds
xn in Support p2 by A30, POLYNOM1:def_3;
then x in A . (x9 . n) by A33;
hence x in union (A .: (len p1)) by A32, TARSKI:def_4; ::_thesis: verum
end;
then y is finite-Support by A25, POLYNOM1:def_4;
then reconsider y9 = y as Element of the carrier of (Polynom-Ring ((n + 1),R)) by POLYNOM1:def_10;
now__::_thesis:_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_p1_=_x_&_p3_=_y9_&_p2_=_p1_._(b_._n)_holds_
p3_._b_=_p2_._(b_|_n)
let p1 be Polynomial of (Polynom-Ring (n,R)); ::_thesis: for p2 being Polynomial of n,R
for p3 being Polynomial of (n + 1),R
for b being bag of n + 1 st p1 = x & p3 = y9 & p2 = p1 . (b . n) holds
p3 . b = p2 . (b | n)
let p2 be Polynomial of n,R; ::_thesis: for p3 being Polynomial of (n + 1),R
for b being bag of n + 1 st p1 = x & p3 = y9 & p2 = p1 . (b . n) holds
p3 . b = p2 . (b | n)
let p3 be Polynomial of (n + 1),R; ::_thesis: for b being bag of n + 1 st p1 = x & p3 = y9 & p2 = p1 . (b . n) holds
p3 . b = p2 . (b | n)
let b be bag of n + 1; ::_thesis: ( p1 = x & p3 = y9 & p2 = p1 . (b . n) implies p3 . b = p2 . (b | n) )
A34: b is Element of Bags (n + 1) by PRE_POLY:def_12;
assume ( p1 = x & p3 = y9 & p2 = p1 . (b . n) ) ; ::_thesis: p3 . b = p2 . (b | n)
hence p3 . b = p2 . (b | n) by A27, A34; ::_thesis: verum
end;
hence ex y being Element of the carrier of (Polynom-Ring ((n + 1),R)) st S1[x,y] ; ::_thesis: verum
end;
consider P being Function of the carrier of (Polynom-Ring (Polynom-Ring (n,R))), the carrier of (Polynom-Ring ((n + 1),R)) such that
A35: for x being Element of the carrier of (Polynom-Ring (Polynom-Ring (n,R))) holds S1[x,P . x] from FUNCT_2:sch_3(A1);
reconsider P = P as Function of (Polynom-Ring (Polynom-Ring (n,R))),(Polynom-Ring ((n + 1),R)) ;
take P ; ::_thesis: 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 = P . p1 & p2 = p1 . (b . n) holds
p3 . b = p2 . (b | n)
now__::_thesis:_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_=_P_._p1_&_p2_=_p1_._(b_._n)_holds_
p3_._b_=_p2_._(b_|_n)
let p1 be Polynomial of (Polynom-Ring (n,R)); ::_thesis: for p2 being Polynomial of n,R
for p3 being Polynomial of (n + 1),R
for b being bag of n + 1 st p3 = P . p1 & p2 = p1 . (b . n) holds
p3 . b = p2 . (b | n)
let p2 be Polynomial of n,R; ::_thesis: for p3 being Polynomial of (n + 1),R
for b being bag of n + 1 st p3 = P . p1 & p2 = p1 . (b . n) holds
p3 . b = p2 . (b | n)
let p3 be Polynomial of (n + 1),R; ::_thesis: for b being bag of n + 1 st p3 = P . p1 & p2 = p1 . (b . n) holds
p3 . b = p2 . (b | n)
let b be bag of n + 1; ::_thesis: ( p3 = P . p1 & p2 = p1 . (b . n) implies p3 . b = p2 . (b | n) )
A36: p1 in the carrier of (Polynom-Ring (Polynom-Ring (n,R))) by POLYNOM3:def_10;
assume ( p3 = P . p1 & p2 = p1 . (b . n) ) ; ::_thesis: p3 . b = p2 . (b | n)
hence p3 . b = p2 . (b | n) by A35, A36; ::_thesis: verum
end;
hence 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 = P . p1 & p2 = p1 . (b . n) holds
p3 . b = p2 . (b | n) ; ::_thesis: verum
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
let A, B be Function of (Polynom-Ring (Polynom-Ring (n,R))),(Polynom-Ring ((n + 1),R)); ::_thesis: ( ( 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 = A . 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 = B . p1 & p2 = p1 . (b . n) holds
p3 . b = p2 . (b | n) ) implies A = B )
set CPN1R = the carrier of (Polynom-Ring ((n + 1),R));
set CPRPNR = the carrier of (Polynom-Ring (Polynom-Ring (n,R)));
set PNR = Polynom-Ring (n,R);
assume A37: 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 = A . p1 & p2 = p1 . (b . n) holds
p3 . b = p2 . (b | n) ; ::_thesis: ( ex p1 being Polynomial of (Polynom-Ring (n,R)) ex p2 being Polynomial of n,R ex p3 being Polynomial of (n + 1),R ex b being bag of n + 1 st
( p3 = B . p1 & p2 = p1 . (b . n) & not p3 . b = p2 . (b | n) ) or A = B )
assume A38: 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 = B . p1 & p2 = p1 . (b . n) holds
p3 . b = p2 . (b | n) ; ::_thesis: A = B
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(Polynom-Ring_(Polynom-Ring_(n,R)))_holds_
A_._x_=_B_._x
let x be set ; ::_thesis: ( x in the carrier of (Polynom-Ring (Polynom-Ring (n,R))) implies A . x = B . x )
assume A39: x in the carrier of (Polynom-Ring (Polynom-Ring (n,R))) ; ::_thesis: A . x = B . x
then reconsider x9 = x as Polynomial of (Polynom-Ring (n,R)) by POLYNOM3:def_10;
( A . x in the carrier of (Polynom-Ring ((n + 1),R)) & B . x in the carrier of (Polynom-Ring ((n + 1),R)) ) by A39, FUNCT_2:5;
then reconsider Ax = A . x, Bx = B . x as Polynomial of (n + 1),R by POLYNOM1:def_10;
now__::_thesis:_for_b_being_set_st_b_in_Bags_(n_+_1)_holds_
Ax_._b_=_Bx_._b
let b be set ; ::_thesis: ( b in Bags (n + 1) implies Ax . b = Bx . b )
assume b in Bags (n + 1) ; ::_thesis: Ax . b = Bx . b
then reconsider b9 = b as Element of Bags (n + 1) ;
reconsider p2 = x9 . (b9 . n) as Polynomial of n,R by POLYNOM1:def_10;
n < n + 1 by NAT_1:13;
then reconsider bn = b9 | n as Element of Bags n by Th3;
thus Ax . b = p2 . bn by A37
.= Bx . b by A38 ; ::_thesis: verum
end;
hence A . x = B . x by FUNCT_2:12; ::_thesis: verum
end;
hence A = B by FUNCT_2:12; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines upm HILBASIS:def_6_:_
for R being non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for n being Element of 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 trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ;
let n be Element of NAT ;
cluster upm (n,R) -> additive ;
coherence
upm (n,R) is additive
proof
set P = upm (n,R);
set PNR = Polynom-Ring (n,R);
thus upm (n,R) is additive ::_thesis: verum
proof
let x, y be Element of (Polynom-Ring (Polynom-Ring (n,R))); :: according to VECTSP_1:def_20 ::_thesis: (upm (n,R)) . (x + y) = ((upm (n,R)) . x) + ((upm (n,R)) . y)
reconsider x9 = x, y9 = y, xy9 = x + y as Polynomial of (Polynom-Ring (n,R)) by POLYNOM3:def_10;
reconsider Pxy = (upm (n,R)) . (x + y), Px = (upm (n,R)) . x, Py = (upm (n,R)) . y as Polynomial of (n + 1),R by POLYNOM1:def_10;
A1: xy9 = x9 + y9 by POLYNOM3:def_10;
now__::_thesis:_for_b_being_set_st_b_in_Bags_(n_+_1)_holds_
Pxy_._b_=_(Px_+_Py)_._b
let b be set ; ::_thesis: ( b in Bags (n + 1) implies Pxy . b = (Px + Py) . b )
assume b in Bags (n + 1) ; ::_thesis: Pxy . b = (Px + Py) . b
then reconsider b9 = b as bag of n + 1 ;
reconsider xybn = (x9 + y9) . (b9 . n) as Polynomial of n,R by POLYNOM1:def_10;
reconsider xbn = x9 . (b9 . n), ybn = y9 . (b9 . n) as Polynomial of n,R by POLYNOM1:def_10;
n < n + 1 by XREAL_1:29;
then reconsider bn = b9 | n as bag of n by Th3;
A2: ( xbn . bn = Px . b9 & ybn . bn = Py . b9 ) by Def6;
(x9 + y9) . (b9 . n) = (x9 . (b9 . n)) + (y9 . (b9 . n)) by NORMSP_1:def_2;
then xybn = xbn + ybn by POLYNOM1:def_10;
hence Pxy . b = (xbn + ybn) . bn by A1, Def6
.= (Px . b9) + (Py . b9) by A2, POLYNOM1:15
.= (Px + Py) . b by POLYNOM1:15 ;
::_thesis: verum
end;
hence (upm (n,R)) . (x + y) = Px + Py by FUNCT_2:12
.= ((upm (n,R)) . x) + ((upm (n,R)) . y) by POLYNOM1:def_10 ;
::_thesis: verum
end;
end;
cluster upm (n,R) -> multiplicative ;
coherence
upm (n,R) is multiplicative
proof
set P = upm (n,R);
set CR = the carrier of R;
set PNR = Polynom-Ring (n,R);
set CPNR = the carrier of (Polynom-Ring (n,R));
thus upm (n,R) is multiplicative ::_thesis: verum
proof
let x9, y9 be Element of the carrier of (Polynom-Ring (Polynom-Ring (n,R))); :: according to GROUP_6:def_6 ::_thesis: (upm (n,R)) . (x9 * y9) = ((upm (n,R)) . x9) * ((upm (n,R)) . y9)
reconsider x = x9, y = y9, xy = x9 * y9 as Polynomial of (Polynom-Ring (n,R)) by POLYNOM3:def_10;
reconsider Pxy = (upm (n,R)) . (x9 * y9), PxPy = ((upm (n,R)) . x9) * ((upm (n,R)) . y9), Px = (upm (n,R)) . x9, Py = (upm (n,R)) . y9 as Polynomial of (n + 1),R by POLYNOM1:def_10;
A3: xy = x *' y by POLYNOM3:def_10;
A4: PxPy = Px *' Py by POLYNOM1:def_10;
now__::_thesis:_for_b9_being_set_st_b9_in_Bags_(n_+_1)_holds_
Pxy_._b9_=_PxPy_._b9
let b9 be set ; ::_thesis: ( b9 in Bags (n + 1) implies Pxy . b9 = PxPy . b9 )
assume b9 in Bags (n + 1) ; ::_thesis: Pxy . b9 = PxPy . b9
then reconsider b = b9 as Element of Bags (n + 1) ;
consider r being FinSequence of the carrier of (Polynom-Ring (n,R)) such that
A5: len r = (b . n) + 1 and
A6: xy . (b . n) = Sum r and
A7: for k being Element of NAT st k in dom r holds
r . k = (x . (k -' 1)) * (y . (((b . n) + 1) -' k)) by A3, POLYNOM3:def_9;
n < n + 1 by NAT_1:13;
then reconsider bn = b | n as Element of Bags n by Th3;
defpred S1[ set , set ] means for p, q being Polynomial of n,R
for fcr being FinSequence of the carrier of R
for i being Element of NAT st i = R & p = x . (i -' 1) & q = y . (((b . n) + 1) -' i) & fcr = n holds
( (p *' q) . bn = Sum fcr & len fcr = len (decomp bn) & ( for k being Element of NAT st k in dom fcr holds
ex b1, b2 being bag of n st
( (decomp bn) /. k = <*b1,b2*> & fcr /. k = (p . b1) * (q . b2) ) ) );
reconsider xybn = xy . (b . n) as Polynomial of n,R by POLYNOM1:def_10;
consider u being FinSequence of the carrier of R such that
A8: PxPy . b = Sum u and
A9: len u = len (decomp b) and
A10: for k being Element of NAT st k in dom u holds
ex b1, b2 being bag of n + 1 st
( (decomp b) /. k = <*b1,b2*> & u /. k = (Px . b1) * (Py . b2) ) by A4, POLYNOM1:def_9;
A11: now__::_thesis:_for_e9_being_set_st_e9_in_dom_r_holds_
ex_u_being_set_st_
(_u_in_the_carrier_of_R_*_&_S1[e9,u]_)
let e9 be set ; ::_thesis: ( e9 in dom r implies ex u being set st
( u in the carrier of R * & S1[e9,u] ) )
assume e9 in dom r ; ::_thesis: ex u being set st
( u in the carrier of R * & S1[e9,u] )
then reconsider e = e9 as Element of NAT ;
reconsider p = x . (e -' 1), q = y . (((b . n) + 1) -' e) as Polynomial of n,R by POLYNOM1:def_10;
consider fcr being FinSequence of the carrier of R such that
A12: ( (p *' q) . bn = Sum fcr & len fcr = len (decomp bn) & ( for k being Element of NAT st k in dom fcr holds
ex b1, b2 being bag of n st
( (decomp bn) /. k = <*b1,b2*> & fcr /. k = (p . b1) * (q . b2) ) ) ) by POLYNOM1:def_9;
A13: fcr in the carrier of R * by FINSEQ_1:def_11;
S1[e,fcr] by A12;
hence ex u being set st
( u in the carrier of R * & S1[e9,u] ) by A13; ::_thesis: verum
end;
consider s being Function of (dom r),( the carrier of R *) such that
A14: for e being set st e in dom r holds
S1[e,s . e] from FUNCT_2:sch_1(A11);
A15: rng s c= the carrier of R * ;
A16: dom s = dom r by FUNCT_2:def_1;
then ex n being Nat st dom s = Seg n by FINSEQ_1:def_2;
then s is FinSequence-like by FINSEQ_1:def_2;
then reconsider s = s as FinSequence of the carrier of R * by A15, FINSEQ_1:def_4;
consider g being Function of the carrier of (Polynom-Ring (n,R)), the carrier of R such that
A17: for p being Polynomial of n,R holds g . p = p . bn and
A18: xybn . bn = Sum (g * r) by A6, Th29;
A19: Sum (g * r) = Pxy . b by A18, Def6;
0 + 1 <= len r by A5, XREAL_1:6;
then A20: 1 in dom s by A16, FINSEQ_3:25;
A21: now__::_thesis:_len_(s_._1)_<>_0
reconsider p9 = x . (1 -' 1), q9 = y . (((b . n) + 1) -' 1) as Polynomial of n,R by POLYNOM1:def_10;
s /. 1 is FinSequence of the carrier of R ;
then A22: s . 1 is FinSequence of the carrier of R by A20, PARTFUN1:def_6;
( p9 = x . (1 -' 1) & q9 = y . (((b . n) + 1) -' 1) ) ;
hence len (s . 1) <> 0 by A14, A16, A20, A22; ::_thesis: verum
end;
defpred S2[ set , set ] means for i, n1 being Element of NAT
for b1 being bag of n + 1 st n1 = R & b1 = (divisors b) . n1 & i in dom (divisors bn) & (divisors bn) . i = b1 | n holds
( (b1 . n) + 1 in dom s & i in dom (s . ((b1 . n) + 1)) & n = (Sum (Card (s | (((b1 . n) + 1) -' 1)))) + i );
set t = FlattenSeq s;
A23: now__::_thesis:_for_n19_being_set_st_n19_in_dom_u_holds_
ex_n29_being_set_st_
(_n29_in_dom_(FlattenSeq_s)_&_S2[n19,n29]_)
let n19 be set ; ::_thesis: ( n19 in dom u implies ex n29 being set st
( n29 in dom (FlattenSeq s) & S2[n19,n29] ) )
assume A24: n19 in dom u ; ::_thesis: ex n29 being set st
( n29 in dom (FlattenSeq s) & S2[n19,n29] )
then reconsider n1 = n19 as Element of NAT ;
dom u = dom (decomp b) by A9, FINSEQ_3:29
.= dom (divisors b) by PRE_POLY:def_17 ;
then A25: (divisors b) . n1 in rng (divisors b) by A24, FUNCT_1:def_3;
then reconsider b1 = (divisors b) . n1 as bag of n + 1 ;
A26: b1 divides b by A25, Th7;
then b1 . n <= b . n by PRE_POLY:def_11;
then A27: (b1 . n) + 1 <= (b . n) + 1 by XREAL_1:6;
n < n + 1 by NAT_1:13;
then reconsider b1n = b1 | n as Element of Bags n by Th3;
reconsider p = x . (((b1 . n) + 1) -' 1), q = y . (((b . n) + 1) -' ((b1 . n) + 1)) as Polynomial of n,R by POLYNOM1:def_10;
A28: ( p = x . (((b1 . n) + 1) -' 1) & q = y . (((b . n) + 1) -' ((b1 . n) + 1)) ) ;
b1n divides bn by A26, Th4;
then b1n in rng (divisors bn) by Th7;
then consider i being set such that
A29: i in dom (divisors bn) and
A30: b1n = (divisors bn) . i by FUNCT_1:def_3;
reconsider i = i as Element of NAT by A29;
set n2 = (Sum (Card (s | (((b1 . n) + 1) -' 1)))) + i;
A31: (b1 . n) + 1 >= 1 + 0 by XREAL_1:6;
then A32: (b1 . n) + 1 in dom s by A5, A16, A27, FINSEQ_3:25;
then s . ((b1 . n) + 1) is Element of the carrier of R * by A16, FUNCT_2:5;
then len (s . ((b1 . n) + 1)) = len (decomp bn) by A14, A16, A32, A28;
then A33: dom (s . ((b1 . n) + 1)) = dom (decomp bn) by FINSEQ_3:29
.= dom (divisors bn) by PRE_POLY:def_17 ;
then A34: (Sum (Card (s | (((b1 . n) + 1) -' 1)))) + i in dom (FlattenSeq s) by A29, A32, PRE_POLY:30;
for i9, n19 being Element of NAT
for b19 being bag of n + 1 st n19 = n1 & b19 = (divisors b) . n19 & i9 in dom (divisors bn) & (divisors bn) . i9 = b19 | n holds
( (b19 . n) + 1 in dom s & i9 in dom (s . ((b19 . n) + 1)) & (Sum (Card (s | (((b1 . n) + 1) -' 1)))) + i = (Sum (Card (s | (((b19 . n) + 1) -' 1)))) + i9 ) by A5, A16, A29, A30, A27, A31, A33, FINSEQ_3:25, FUNCT_1:def_4;
hence ex n29 being set st
( n29 in dom (FlattenSeq s) & S2[n19,n29] ) by A34; ::_thesis: verum
end;
consider p being Function of (dom u),(dom (FlattenSeq s)) such that
A35: for x being set st x in dom u holds
S2[x,p . x] from FUNCT_2:sch_1(A23);
1 in dom (Card s) by A20, CARD_3:def_2;
then Sum (Card s) >= (Card s) . 1 by POLYNOM3:4;
then Sum (Card s) > 0 by A20, A21, CARD_3:def_2;
then len (FlattenSeq s) > 0 by PRE_POLY:27;
then A36: FlattenSeq s <> {} ;
then A37: dom p = dom u by FUNCT_2:def_1;
now__::_thesis:_for_n19,_n29_being_set_st_n19_in_dom_p_&_n29_in_dom_p_&_p_._n19_=_p_._n29_holds_
n19_=_n29
let n19, n29 be set ; ::_thesis: ( n19 in dom p & n29 in dom p & p . n19 = p . n29 implies n19 = n29 )
assume that
A38: n19 in dom p and
A39: n29 in dom p and
A40: p . n19 = p . n29 ; ::_thesis: n19 = n29
dom p = dom u by A36, FUNCT_2:def_1;
then reconsider n1 = n19, n2 = n29 as Element of NAT by A38, A39;
A41: dom u = dom (decomp b) by A9, FINSEQ_3:29
.= dom (divisors b) by PRE_POLY:def_17 ;
then A42: (divisors b) . n1 in rng (divisors b) by A38, FUNCT_1:def_3;
then reconsider b1 = (divisors b) . n1 as bag of n + 1 ;
A43: (divisors b) . n2 in rng (divisors b) by A39, A41, FUNCT_1:def_3;
then reconsider b2 = (divisors b) . n2 as bag of n + 1 ;
n < n + 1 by NAT_1:13;
then reconsider b1n = b1 | n, b2n = b2 | n as Element of Bags n by Th3;
A44: ( (Card s) | (((b1 . n) + 1) -' 1) = Card (s | (((b1 . n) + 1) -' 1)) & (Card s) | (((b2 . n) + 1) -' 1) = Card (s | (((b2 . n) + 1) -' 1)) ) by POLYNOM3:16;
b2 divides b by A43, Th7;
then b2n divides bn by Th4;
then b2n in rng (divisors bn) by Th7;
then consider i2 being set such that
A45: i2 in dom (divisors bn) and
A46: b2n = (divisors bn) . i2 by FUNCT_1:def_3;
reconsider i2 = i2 as Element of NAT by A45;
A47: ( (b2 . n) + 1 in dom s & i2 in dom (s . ((b2 . n) + 1)) ) by A35, A39, A45, A46;
b1 divides b by A42, Th7;
then b1n divides bn by Th4;
then b1n in rng (divisors bn) by Th7;
then consider i1 being set such that
A48: i1 in dom (divisors bn) and
A49: b1n = (divisors bn) . i1 by FUNCT_1:def_3;
reconsider i1 = i1 as Element of NAT by A48;
A50: p . n1 = (Sum (Card (s | (((b1 . n) + 1) -' 1)))) + i1 by A35, A38, A48, A49;
A51: p . n2 = (Sum (Card (s | (((b2 . n) + 1) -' 1)))) + i2 by A35, A39, A45, A46;
A52: b2 is Element of Bags (n + 1) by PRE_POLY:def_12;
( (b1 . n) + 1 in dom s & i1 in dom (s . ((b1 . n) + 1)) ) by A35, A38, A48, A49;
then A53: ( (b1 . n) + 1 = (b2 . n) + 1 & i1 = i2 ) by A40, A50, A47, A51, A44, POLYNOM3:22;
b1 is Element of Bags (n + 1) by PRE_POLY:def_12;
then b1 = b1n bag_extend (b1 . n) by Def1
.= b2 by A49, A46, A53, A52, Def1 ;
hence n19 = n29 by A38, A39, A41, FUNCT_1:def_4; ::_thesis: verum
end;
then A54: p is one-to-one by FUNCT_1:def_4;
dom (FlattenSeq s) c= rng p
proof
let n19 be set ; :: according to TARSKI:def_3 ::_thesis: ( not n19 in dom (FlattenSeq s) or n19 in rng p )
assume A55: n19 in dom (FlattenSeq s) ; ::_thesis: n19 in rng p
then reconsider n1 = n19 as Element of NAT ;
consider i, j being Element of NAT such that
A56: i in dom s and
A57: j in dom (s . i) and
A58: n1 = (Sum (Card (s | (i -' 1)))) + j and
(s . i) . j = (FlattenSeq s) . n1 by A55, PRE_POLY:29;
s . i in the carrier of R * by A16, A56, FUNCT_2:5;
then A59: s . i is FinSequence of the carrier of R by FINSEQ_1:def_11;
reconsider bj = (divisors bn) /. j as bag of n ;
set bij = bj bag_extend (i -' 1);
reconsider p9 = x . (i -' 1), q9 = y . (((b . n) + 1) -' i) as Polynomial of n,R by POLYNOM1:def_10;
A60: (bj bag_extend (i -' 1)) . n = i -' 1 by Def1;
1 <= i by A56, FINSEQ_3:25;
then A61: ((bj bag_extend (i -' 1)) . n) + 1 = i by A60, XREAL_1:235;
A62: dom u = dom (decomp b) by A9, FINSEQ_3:29
.= dom (divisors b) by PRE_POLY:def_17 ;
( p9 = x . (i -' 1) & q9 = y . (((b . n) + 1) -' i) ) ;
then len (s . i) = len (decomp bn) by A14, A16, A56, A59;
then A63: dom (s . i) = dom (decomp bn) by FINSEQ_3:29
.= dom (divisors bn) by PRE_POLY:def_17 ;
then A64: bj = (divisors bn) . j by A57, PARTFUN1:def_6;
then bj in rng (divisors bn) by A57, A63, FUNCT_1:def_3;
then A65: bj divides bn by Th7;
now__::_thesis:_for_k_being_set_holds_(bj_bag_extend_(i_-'_1))_._k_<=_b_._k
let k be set ; ::_thesis: (bj bag_extend (i -' 1)) . b1 <= b . b1
percases ( k in n + 1 or not k in n + 1 ) ;
supposeA66: k in n + 1 ; ::_thesis: (bj bag_extend (i -' 1)) . b1 <= b . b1
now__::_thesis:_(bj_bag_extend_(i_-'_1))_._k_<=_b_._k
percases ( k in n or not k in n ) ;
supposeA67: k in n ; ::_thesis: (bj bag_extend (i -' 1)) . k <= b . k
then A68: b . k = bn . k by FUNCT_1:49;
(bj bag_extend (i -' 1)) . k = ((bj bag_extend (i -' 1)) | n) . k by A67, FUNCT_1:49
.= bj . k by Def1 ;
hence (bj bag_extend (i -' 1)) . k <= b . k by A65, A68, PRE_POLY:def_11; ::_thesis: verum
end;
supposeA69: not k in n ; ::_thesis: (bj bag_extend (i -' 1)) . k <= b . k
A70: 1 <= i by A56, FINSEQ_3:25;
i <= (b . n) + 1 by A5, A16, A56, FINSEQ_3:25;
then A71: i - 1 <= ((b . n) + 1) - 1 by XREAL_1:9;
n + 1 = succ n by NAT_1:38
.= n \/ {n} by ORDINAL1:def_1 ;
then k in {n} by A66, A69, XBOOLE_0:def_3;
then A72: k = n by TARSKI:def_1;
then (bj bag_extend (i -' 1)) . k = i -' 1 by Def1;
hence (bj bag_extend (i -' 1)) . k <= b . k by A72, A70, A71, XREAL_1:233; ::_thesis: verum
end;
end;
end;
hence (bj bag_extend (i -' 1)) . k <= b . k ; ::_thesis: verum
end;
supposeA73: not k in n + 1 ; ::_thesis: (bj bag_extend (i -' 1)) . b1 <= b . b1
dom (bj bag_extend (i -' 1)) = n + 1 by PARTFUN1:def_2;
hence (bj bag_extend (i -' 1)) . k <= b . k by A73, FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
then bj bag_extend (i -' 1) divides b by PRE_POLY:def_11;
then bj bag_extend (i -' 1) in rng (divisors b) by Th7;
then consider k being set such that
A74: k in dom (divisors b) and
A75: bj bag_extend (i -' 1) = (divisors b) . k by FUNCT_1:def_3;
A76: dom p = dom u by A36, FUNCT_2:def_1;
(divisors bn) . j = (bj bag_extend (i -' 1)) | n by A64, Def1;
then p . k = (Sum (Card (s | ((((bj bag_extend (i -' 1)) . n) + 1) -' 1)))) + j by A35, A57, A63, A74, A75, A62;
hence n19 in rng p by A58, A74, A76, A62, A61, FUNCT_1:def_3; ::_thesis: verum
end;
then A77: rng p = dom (FlattenSeq s) by XBOOLE_0:def_10;
len (Sum s) = len s by MATRLIN:def_6;
then A78: dom (Sum s) = dom r by A16, FINSEQ_3:29;
A79: now__::_thesis:_for_k_being_Nat_st_k_in_dom_r_holds_
(Sum_s)_._k_=_(g_*_r)_._k
let k be Nat; ::_thesis: ( k in dom r implies (Sum s) . k = (g * r) . k )
reconsider p = x . (k -' 1), q = y . (((b . n) + 1) -' k) as Polynomial of n,R by POLYNOM1:def_10;
reconsider pq9 = p *' q as Element of the carrier of (Polynom-Ring (n,R)) by POLYNOM1:def_10;
assume A80: k in dom r ; ::_thesis: (Sum s) . k = (g * r) . k
then reconsider sk = s . k as Element of the carrier of R * by FUNCT_2:5;
reconsider sk = sk as FinSequence of the carrier of R ;
A81: r . k = (x . (k -' 1)) * (y . (((b . n) + 1) -' k)) by A7, A80
.= pq9 by POLYNOM1:def_10 ;
( (Sum s) /. k = (Sum s) . k & s /. k = s . k ) by A16, A78, A80, PARTFUN1:def_6;
hence (Sum s) . k = Sum sk by A78, A80, MATRLIN:def_6
.= (p *' q) . bn by A14, A80
.= g . (r . k) by A17, A81
.= (g * r) . k by A80, FUNCT_1:13 ;
::_thesis: verum
end;
A82: now__::_thesis:_for_n1_being_Element_of_NAT_st_n1_in_dom_u_holds_
u_._n1_=_(FlattenSeq_s)_._(p_._n1)
let n1 be Element of NAT ; ::_thesis: ( n1 in dom u implies u . n1 = (FlattenSeq s) . (p . n1) )
reconsider b19 = (divisors b) /. n1 as bag of n + 1 ;
assume A83: n1 in dom u ; ::_thesis: u . n1 = (FlattenSeq s) . (p . n1)
then consider b1, b2 being bag of n + 1 such that
A84: (decomp b) /. n1 = <*b1,b2*> and
A85: u /. n1 = (Px . b1) * (Py . b2) by A10;
A86: dom u = dom (decomp b) by A9, FINSEQ_3:29;
then A87: <*b1,b2*> = <*b19,(b -' b19)*> by A83, A84, PRE_POLY:def_17;
then A88: b1 = b19 by FINSEQ_1:77;
reconsider xb1n = x . (b1 . n), yb2n = y . (b2 . n) as Polynomial of n,R by POLYNOM1:def_10;
n < n + 1 by NAT_1:13;
then reconsider b1n = b1 | n, b2n = b2 | n as Element of Bags n by Th3;
A89: u . n1 = (Px . b1) * (Py . b2) by A83, A85, PARTFUN1:def_6
.= (xb1n . b1n) * (Py . b2) by Def6
.= (xb1n . b1n) * (yb2n . b2n) by Def6 ;
A90: b2 = b -' b19 by A87, FINSEQ_1:77;
A91: n1 in dom (divisors b) by A83, A86, PRE_POLY:def_17;
then A92: b1 = (divisors b) . n1 by A88, PARTFUN1:def_6;
then b1 in rng (divisors b) by A91, FUNCT_1:def_3;
then A93: b1 divides b by Th7;
then b1n divides bn by Th4;
then b1n in rng (divisors bn) by Th7;
then consider i being set such that
A94: i in dom (divisors bn) and
A95: b1n = (divisors bn) . i by FUNCT_1:def_3;
reconsider i = i as Element of NAT by A94;
A96: b1 . n <= b . n by A93, PRE_POLY:def_11;
then (b1 . n) + 1 <= (b . n) + 1 by XREAL_1:6;
then A97: ((b . n) + 1) -' ((b1 . n) + 1) = ((b . n) + 1) - ((b1 . n) + 1) by XREAL_1:233
.= (((b . n) - (b1 . n)) + 1) - 1
.= (b . n) -' (b1 . n) by A96, XREAL_1:233
.= b2 . n by A88, A90, PRE_POLY:def_6 ;
A98: ((b1 . n) + 1) -' 1 = ((b1 . n) + 1) - 1 by NAT_D:37
.= b1 . n ;
then A99: xb1n = x . (((b1 . n) + 1) -' 1) ;
A100: (b1 . n) + 1 in dom s by A35, A83, A92, A94, A95;
then s . ((b1 . n) + 1) is Element of the carrier of R * by A16, FUNCT_2:5;
then reconsider sb1n1 = s . ((b1 . n) + 1) as FinSequence of the carrier of R ;
A101: i in dom (s . ((b1 . n) + 1)) by A35, A83, A92, A94, A95;
then consider B1, B2 being bag of n such that
A102: (decomp bn) /. i = <*B1,B2*> and
A103: sb1n1 /. i = (xb1n . B1) * (yb2n . B2) by A14, A16, A100, A98, A97;
p . n1 = (Sum (Card (s | (((b1 . n) + 1) -' 1)))) + i by A35, A83, A92, A94, A95;
then A104: (FlattenSeq s) . (p . n1) = (s . ((b1 . n) + 1)) . i by A100, A101, PRE_POLY:30;
reconsider B19 = (divisors bn) /. i as bag of n ;
A105: dom (divisors bn) = dom (decomp bn) by PRE_POLY:def_17;
then A106: <*B1,B2*> = <*B19,(bn -' B19)*> by A94, A102, PRE_POLY:def_17;
then A107: B1 = B19 by FINSEQ_1:77;
then A108: B1 = b1n by A94, A95, PARTFUN1:def_6;
yb2n = y . (((b . n) + 1) -' ((b1 . n) + 1)) by A97;
then len sb1n1 = len (decomp bn) by A14, A16, A100, A99;
then A109: dom sb1n1 = dom (divisors bn) by A105, FINSEQ_3:29;
B2 = bn -' B19 by A106, FINSEQ_1:77;
then B2 = b2n by A88, A90, A107, A108, Th5;
hence u . n1 = (FlattenSeq s) . (p . n1) by A89, A94, A104, A103, A108, A109, PARTFUN1:def_6; ::_thesis: verum
end;
dom r = dom (g * r) by FINSEQ_3:120;
then Sum s = g * r by A78, A79, FINSEQ_1:13;
then A110: Sum (FlattenSeq s) = Pxy . b by A19, POLYNOM1:14;
A111: len u = card (dom u) by CARD_1:62
.= card p by A37, CARD_1:62
.= card (dom (FlattenSeq s)) by A54, A77, PRE_POLY:19
.= len (FlattenSeq s) by CARD_1:62 ;
then A112: dom u = dom (FlattenSeq s) by FINSEQ_3:29;
then p is Permutation of (dom u) by A54, A77, FUNCT_2:57;
hence Pxy . b9 = PxPy . b9 by A110, A8, A82, A111, A112, RLVECT_2:6; ::_thesis: verum
end;
hence (upm (n,R)) . (x9 * y9) = ((upm (n,R)) . x9) * ((upm (n,R)) . y9) by FUNCT_2:12; ::_thesis: verum
end;
end;
cluster upm (n,R) -> unity-preserving ;
coherence
upm (n,R) is unity-preserving
proof
set P = upm (n,R);
set PNR = Polynom-Ring (n,R);
set PN1R = Polynom-Ring ((n + 1),R);
set PRPNR = Polynom-Ring (Polynom-Ring (n,R));
set CPN1R = the carrier of (Polynom-Ring ((n + 1),R));
reconsider p1 = 1_ (Polynom-Ring (Polynom-Ring (n,R))) as Polynomial of (Polynom-Ring (n,R)) by POLYNOM3:def_10;
reconsider p19 = 1_ (Polynom-Ring ((n + 1),R)) as Polynomial of (n + 1),R by POLYNOM1:def_10;
(upm (n,R)) . (1_ (Polynom-Ring (Polynom-Ring (n,R)))) in the carrier of (Polynom-Ring ((n + 1),R)) ;
then reconsider p3 = (upm (n,R)) . p1 as Polynomial of (n + 1),R by POLYNOM1:def_10;
now__::_thesis:_for_x_being_set_st_x_in_Bags_(n_+_1)_holds_
p3_._x_=_p19_._x
let x be set ; ::_thesis: ( x in Bags (n + 1) implies p3 . x = p19 . x )
assume x in Bags (n + 1) ; ::_thesis: p3 . x = p19 . x
then reconsider b = x as Element of Bags (n + 1) ;
reconsider p2 = p1 . (b . n) as Polynomial of n,R by POLYNOM1:def_10;
A113: p3 . b = p2 . (b | n) by Def6;
now__::_thesis:_p3_._b_=_p19_._b
percases ( ( b | n = EmptyBag n & b . n = 0 ) or b | n <> EmptyBag n or b . n <> 0 ) ;
supposeA114: ( b | n = EmptyBag n & b . n = 0 ) ; ::_thesis: p3 . b = p19 . b
then A115: b = (EmptyBag n) bag_extend 0 by Def1
.= EmptyBag (n + 1) by Th6 ;
p2 = (1_. (Polynom-Ring (n,R))) . 0 by A114, POLYNOM3:def_10
.= 1_ (Polynom-Ring (n,R)) by POLYNOM3:30
.= 1_ (n,R) by POLYNOM1:31 ;
hence p3 . b = 1_ R by A113, A114, POLYNOM1:25
.= (1_ ((n + 1),R)) . b by A115, POLYNOM1:25
.= p19 . b by POLYNOM1:31 ;
::_thesis: verum
end;
supposeA116: ( b | n <> EmptyBag n or b . n <> 0 ) ; ::_thesis: p3 . b = p19 . b
A117: now__::_thesis:_p3_._b_=_0._R
n < n + 1 by NAT_1:13;
then A118: b | n is bag of n by Th3;
A119: p2 = (1_. (Polynom-Ring (n,R))) . (b . n) by POLYNOM3:def_10;
percases ( b . n = 0 or b . n <> 0 ) ;
supposeA120: b . n = 0 ; ::_thesis: p3 . b = 0. R
then p2 = 1_ (Polynom-Ring (n,R)) by A119, POLYNOM3:30
.= 1_ (n,R) by POLYNOM1:31 ;
hence p3 . b = 0. R by A113, A116, A118, A120, POLYNOM1:25; ::_thesis: verum
end;
suppose b . n <> 0 ; ::_thesis: p3 . b = 0. R
then p2 = 0. (Polynom-Ring (n,R)) by A119, POLYNOM3:30
.= 0_ (n,R) by POLYNOM1:def_10 ;
hence p3 . b = 0. R by A113, A118, POLYNOM1:22; ::_thesis: verum
end;
end;
end;
b <> (EmptyBag n) bag_extend 0 by A116, Def1;
then b <> EmptyBag (n + 1) by Th6;
hence p3 . b = (1_ ((n + 1),R)) . b by A117, POLYNOM1:25
.= p19 . b by POLYNOM1:31 ;
::_thesis: verum
end;
end;
end;
hence p3 . x = p19 . x ; ::_thesis: verum
end;
then p19 = p3 by FUNCT_2:12;
hence upm (n,R) is unity-preserving by GROUP_1:def_13; ::_thesis: verum
end;
cluster upm (n,R) -> one-to-one ;
coherence
upm (n,R) is one-to-one
proof
set P = upm (n,R);
set PNR = Polynom-Ring (n,R);
set PRPNR = Polynom-Ring (Polynom-Ring (n,R));
now__::_thesis:_for_x9,_y9_being_Element_of_(Polynom-Ring_(Polynom-Ring_(n,R)))_st_(upm_(n,R))_._x9_=_(upm_(n,R))_._y9_holds_
x9_=_y9
let x9, y9 be Element of (Polynom-Ring (Polynom-Ring (n,R))); ::_thesis: ( (upm (n,R)) . x9 = (upm (n,R)) . y9 implies x9 = y9 )
reconsider x = x9, y = y9 as Polynomial of (Polynom-Ring (n,R)) by POLYNOM3:def_10;
reconsider Py = (upm (n,R)) . y9 as Polynomial of (n + 1),R by POLYNOM1:def_10;
assume A121: (upm (n,R)) . x9 = (upm (n,R)) . y9 ; ::_thesis: x9 = y9
now__::_thesis:_for_bn9_being_set_st_bn9_in_NAT_holds_
x_._bn9_=_y_._bn9
let bn9 be set ; ::_thesis: ( bn9 in NAT implies x . bn9 = y . bn9 )
assume bn9 in NAT ; ::_thesis: x . bn9 = y . bn9
then reconsider bn = bn9 as Element of NAT ;
reconsider xbn = x . bn, ybn = y . bn as Polynomial of n,R by POLYNOM1:def_10;
now__::_thesis:_for_b9_being_set_st_b9_in_Bags_n_holds_
xbn_._b9_=_ybn_._b9
let b9 be set ; ::_thesis: ( b9 in Bags n implies xbn . b9 = ybn . b9 )
assume b9 in Bags n ; ::_thesis: xbn . b9 = ybn . b9
then reconsider b = b9 as bag of n ;
set bn1 = b bag_extend bn;
A122: ( (b bag_extend bn) | n = b & (b bag_extend bn) . n = bn ) by Def1;
then xbn . b = Py . (b bag_extend bn) by A121, Def6
.= ybn . b by A122, Def6 ;
hence xbn . b9 = ybn . b9 ; ::_thesis: verum
end;
hence x . bn9 = y . bn9 by FUNCT_2:12; ::_thesis: verum
end;
hence x9 = y9 by FUNCT_2:12; ::_thesis: verum
end;
hence upm (n,R) is one-to-one by WAYBEL_1:def_1; ::_thesis: verum
end;
end;
definition
let R be non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ;
let n be Element of 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 Element of 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 Element of NAT
for b being bag of n st p3 = b1 . p1 & p2 = p3 . i holds
p2 . b = p1 . (b bag_extend i)
proof
set CR = the carrier of R;
set PNR = Polynom-Ring (n,R);
set PN1R = Polynom-Ring ((n + 1),R);
set PRPNR = Polynom-Ring (Polynom-Ring (n,R));
set CPRPNR = the carrier of (Polynom-Ring (Polynom-Ring (n,R)));
set CPN1R = the carrier of (Polynom-Ring ((n + 1),R));
set CPNR = the carrier of (Polynom-Ring (n,R));
defpred S1[ Element of the carrier of (Polynom-Ring ((n + 1),R)), Element of the carrier of (Polynom-Ring (Polynom-Ring (n,R)))] means 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 Element of NAT
for b being bag of n st p1 = $1 & p3 = $2 & p2 = p3 . i holds
p2 . b = p1 . (b bag_extend i);
A1: now__::_thesis:_for_x_being_Element_of_the_carrier_of_(Polynom-Ring_((n_+_1),R))_ex_y_being_Element_of_the_carrier_of_(Polynom-Ring_(Polynom-Ring_(n,R)))_st_S1[x,y]
let x be Element of the carrier of (Polynom-Ring ((n + 1),R)); ::_thesis: ex y being Element of the carrier of (Polynom-Ring (Polynom-Ring (n,R))) st S1[x,y]
reconsider p1 = x as Polynomial of (n + 1),R by POLYNOM1:def_10;
defpred S2[ Element of NAT , Element of the carrier of (Polynom-Ring (n,R))] means for p2 being Polynomial of n,R
for b being bag of n st p2 = $2 holds
p2 . b = p1 . (b bag_extend $1);
A2: now__::_thesis:_for_i_being_Element_of_NAT_ex_p29_being_Element_of_the_carrier_of_(Polynom-Ring_(n,R))_st_S2[i,p29]
let i be Element of NAT ; ::_thesis: ex p29 being Element of the carrier of (Polynom-Ring (n,R)) st S2[i,p29]
deffunc H1( Element of Bags n) -> Element of the carrier of R = p1 . ($1 bag_extend i);
consider p2 being Function of (Bags n), the carrier of R such that
A3: for b being Element of Bags n holds p2 . b = H1(b) from FUNCT_2:sch_4();
reconsider p2 = p2 as Function of (Bags n),R ;
reconsider p2 = p2 as Series of n,R ;
now__::_thesis:_Support_p2_is_finite
percases ( Support p1 = {} or Support p2 = {} or ( Support p1 <> {} & Support p2 <> {} ) ) ;
supposeA4: Support p1 = {} ; ::_thesis: Support p2 is finite
now__::_thesis:_(_Support_p2_<>_{}_implies_Support_p1_<>_{}_)
assume Support p2 <> {} ; ::_thesis: Support p1 <> {}
then consider b being set such that
A5: b in Support p2 by XBOOLE_0:def_1;
reconsider b = b as Element of Bags n by A5;
p2 . b <> 0. R by A5, POLYNOM1:def_3;
then p1 . (b bag_extend i) <> 0. R by A3;
hence Support p1 <> {} by POLYNOM1:def_3; ::_thesis: verum
end;
hence Support p2 is finite by A4; ::_thesis: verum
end;
suppose Support p2 = {} ; ::_thesis: Support p2 is finite
hence Support p2 is finite ; ::_thesis: verum
end;
supposeA6: ( Support p1 <> {} & Support p2 <> {} ) ; ::_thesis: Support p2 is finite
then reconsider Supportp2 = Support p2 as non empty Subset of (Bags n) ;
reconsider Supportp1 = Support p1 as non empty Subset of (Bags (n + 1)) by A6;
defpred S3[ Element of Supportp2, set ] means $2 = $1 bag_extend i;
A7: now__::_thesis:_for_x_being_Element_of_Supportp2_ex_y_being_Element_of_Supportp1_st_S3[x,y]
let x be Element of Supportp2; ::_thesis: ex y being Element of Supportp1 st S3[x,y]
( x is Element of Bags n & p2 . x <> 0. R ) by POLYNOM1:def_3;
then p1 . (x bag_extend i) <> 0. R by A3;
then x bag_extend i in Support p1 by POLYNOM1:def_3;
hence ex y being Element of Supportp1 st S3[x,y] ; ::_thesis: verum
end;
consider f being Function of Supportp2,Supportp1 such that
A8: for x being Element of Supportp2 holds S3[x,f . x] from FUNCT_2:sch_3(A7);
A9: dom f = Supportp2 by FUNCT_2:def_1;
now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_f_&_x2_in_dom_f_&_f_._x1_=_f_._x2_holds_
x1_=_x2
let x1, x2 be set ; ::_thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A10: x1 in dom f and
A11: x2 in dom f and
A12: f . x1 = f . x2 ; ::_thesis: x1 = x2
reconsider x19 = x1, x29 = x2 as Element of Bags n by A9, A10, A11;
A13: x19 bag_extend i = f . x1 by A8, A10
.= x29 bag_extend i by A8, A11, A12 ;
x19 = (x19 bag_extend i) | n by Def1
.= x29 by A13, Def1 ;
hence x1 = x2 ; ::_thesis: verum
end;
then A14: f is one-to-one by FUNCT_1:def_4;
rng f c= Supportp1 ;
then card Supportp2 c= card Supportp1 by A9, A14, CARD_1:10;
hence Support p2 is finite ; ::_thesis: verum
end;
end;
end;
then p2 is finite-Support by POLYNOM1:def_4;
then reconsider p29 = p2 as Element of the carrier of (Polynom-Ring (n,R)) by POLYNOM1:def_10;
take p29 = p29; ::_thesis: S2[i,p29]
now__::_thesis:_for_p299_being_Polynomial_of_n,R
for_b_being_bag_of_n_st_p299_=_p29_holds_
p299_._b_=_p1_._(b_bag_extend_i)
let p299 be Polynomial of n,R; ::_thesis: for b being bag of n st p299 = p29 holds
p299 . b = p1 . (b bag_extend i)
let b be bag of n; ::_thesis: ( p299 = p29 implies p299 . b = p1 . (b bag_extend i) )
A15: b is Element of Bags n by PRE_POLY:def_12;
assume p299 = p29 ; ::_thesis: p299 . b = p1 . (b bag_extend i)
hence p299 . b = p1 . (b bag_extend i) by A3, A15; ::_thesis: verum
end;
hence S2[i,p29] ; ::_thesis: verum
end;
consider p3 being Function of NAT, the carrier of (Polynom-Ring (n,R)) such that
A16: for x being Element of NAT holds S2[x,p3 . x] from FUNCT_2:sch_3(A2);
reconsider p3 = p3 as sequence of (Polynom-Ring (n,R)) ;
now__::_thesis:_p3_is_finite-Support
percases ( Support p1 = {} or Support p1 <> {} ) ;
supposeA17: Support p1 = {} ; ::_thesis: p3 is finite-Support
now__::_thesis:_for_i_being_Nat_st_i_>=_0_holds_
p3_._i_=_0._(Polynom-Ring_(n,R))
let i be Nat; ::_thesis: ( i >= 0 implies p3 . i = 0. (Polynom-Ring (n,R)) )
assume i >= 0 ; ::_thesis: p3 . i = 0. (Polynom-Ring (n,R))
reconsider i1 = i as Element of NAT by ORDINAL1:def_12;
reconsider p2 = p3 . i1 as Polynomial of n,R by POLYNOM1:def_10;
A18: now__::_thesis:_for_x_being_set_st_x_in_Bags_n_holds_
p2_._x_=_((Bags_n)_-->_(0._R))_._x
let x be set ; ::_thesis: ( x in Bags n implies p2 . x = ((Bags n) --> (0. R)) . x )
assume x in Bags n ; ::_thesis: p2 . x = ((Bags n) --> (0. R)) . x
then reconsider x9 = x as Element of Bags n ;
p1 . (x9 bag_extend i) = 0. R by A17, POLYNOM1:def_3;
then p2 . x9 = 0. R by A16;
hence p2 . x = ((Bags n) --> (0. R)) . x by FUNCOP_1:7; ::_thesis: verum
end;
( dom ((Bags n) --> (0. R)) = Bags n & dom p2 = Bags n ) by FUNCT_2:def_1;
then p2 = (Bags n) --> (0. R) by A18, FUNCT_1:2;
hence p3 . i = 0_ (n,R) by POLYNOM1:def_7
.= 0. (Polynom-Ring (n,R)) by POLYNOM1:def_10 ;
::_thesis: verum
end;
hence p3 is finite-Support by ALGSEQ_1:def_1; ::_thesis: verum
end;
suppose Support p1 <> {} ; ::_thesis: p3 is finite-Support
then reconsider Supportp1 = Support p1 as non empty finite Subset of (Bags (n + 1)) ;
deffunc H1( Element of Bags (n + 1)) -> Element of NAT = $1 . n;
consider f being Function of (Bags (n + 1)),NAT such that
A19: for x being Element of Bags (n + 1) holds f . x = H1(x) from FUNCT_2:sch_4();
reconsider j = max (f .: Supportp1) as Element of NAT by ORDINAL1:def_12;
now__::_thesis:_for_i_being_Nat_st_i_>=_j_+_1_holds_
p3_._i_=_0._(Polynom-Ring_(n,R))
let i be Nat; ::_thesis: ( i >= j + 1 implies p3 . i = 0. (Polynom-Ring (n,R)) )
reconsider i1 = i as Element of NAT by ORDINAL1:def_12;
reconsider p2 = p3 . i1 as Polynomial of n,R by POLYNOM1:def_10;
assume A20: i >= j + 1 ; ::_thesis: p3 . i = 0. (Polynom-Ring (n,R))
A21: now__::_thesis:_for_x_being_set_st_x_in_Bags_n_holds_
p2_._x_=_((Bags_n)_-->_(0._R))_._x
let x be set ; ::_thesis: ( x in Bags n implies p2 . x = ((Bags n) --> (0. R)) . x )
assume x in Bags n ; ::_thesis: p2 . x = ((Bags n) --> (0. R)) . x
then reconsider x9 = x as Element of Bags n ;
i > j by A20, NAT_1:13;
then A22: not i in f .: Supportp1 by XXREAL_2:def_8;
f . (x9 bag_extend i) = (x9 bag_extend i) . n by A19
.= i by Def1 ;
then not x9 bag_extend i in Supportp1 by A22, FUNCT_2:35;
then p1 . (x9 bag_extend i) = 0. R by POLYNOM1:def_3;
then p2 . x9 = 0. R by A16;
hence p2 . x = ((Bags n) --> (0. R)) . x by FUNCOP_1:7; ::_thesis: verum
end;
( dom ((Bags n) --> (0. R)) = Bags n & dom p2 = Bags n ) by FUNCT_2:def_1;
then p2 = (Bags n) --> (0. R) by A21, FUNCT_1:2;
hence p3 . i = 0_ (n,R) by POLYNOM1:def_7
.= 0. (Polynom-Ring (n,R)) by POLYNOM1:def_10 ;
::_thesis: verum
end;
hence p3 is finite-Support by ALGSEQ_1:def_1; ::_thesis: verum
end;
end;
end;
then reconsider y = p3 as Element of the carrier of (Polynom-Ring (Polynom-Ring (n,R))) by POLYNOM3:def_10;
take y = y; ::_thesis: S1[x,y]
thus S1[x,y] by A16; ::_thesis: verum
end;
consider P being Function of the carrier of (Polynom-Ring ((n + 1),R)), the carrier of (Polynom-Ring (Polynom-Ring (n,R))) such that
A23: for x being Element of the carrier of (Polynom-Ring ((n + 1),R)) holds S1[x,P . x] from FUNCT_2:sch_3(A1);
reconsider P = P as Function of (Polynom-Ring ((n + 1),R)),(Polynom-Ring (Polynom-Ring (n,R))) ;
take P ; ::_thesis: 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 Element of NAT
for b being bag of n st p3 = P . p1 & p2 = p3 . i holds
p2 . b = p1 . (b bag_extend i)
now__::_thesis:_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_Element_of_NAT_
for_b_being_bag_of_n_st_p3_=_P_._p1_&_p2_=_p3_._i_holds_
p2_._b_=_p1_._(b_bag_extend_i)
let p1 be Polynomial of (n + 1),R; ::_thesis: for p2 being Polynomial of n,R
for p3 being Polynomial of (Polynom-Ring (n,R))
for i being Element of NAT
for b being bag of n st p3 = P . p1 & p2 = p3 . i holds
p2 . b = p1 . (b bag_extend i)
let p2 be Polynomial of n,R; ::_thesis: for p3 being Polynomial of (Polynom-Ring (n,R))
for i being Element of NAT
for b being bag of n st p3 = P . p1 & p2 = p3 . i holds
p2 . b = p1 . (b bag_extend i)
let p3 be Polynomial of (Polynom-Ring (n,R)); ::_thesis: for i being Element of NAT
for b being bag of n st p3 = P . p1 & p2 = p3 . i holds
p2 . b = p1 . (b bag_extend i)
let i be Element of NAT ; ::_thesis: for b being bag of n st p3 = P . p1 & p2 = p3 . i holds
p2 . b = p1 . (b bag_extend i)
let b be bag of n; ::_thesis: ( p3 = P . p1 & p2 = p3 . i implies p2 . b = p1 . (b bag_extend i) )
A24: p1 in the carrier of (Polynom-Ring ((n + 1),R)) by POLYNOM1:def_10;
assume ( p3 = P . p1 & p2 = p3 . i ) ; ::_thesis: p2 . b = p1 . (b bag_extend i)
hence p2 . b = p1 . (b bag_extend i) by A23, A24; ::_thesis: verum
end;
hence 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 Element of NAT
for b being bag of n st p3 = P . p1 & p2 = p3 . i holds
p2 . b = p1 . (b bag_extend i) ; ::_thesis: verum
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 Element of 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 Element of 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
set PNR = Polynom-Ring (n,R);
set PN1R = Polynom-Ring ((n + 1),R);
set PRPNR = Polynom-Ring (Polynom-Ring (n,R));
set CPN1R = the carrier of (Polynom-Ring ((n + 1),R));
let A, B be Function of (Polynom-Ring ((n + 1),R)),(Polynom-Ring (Polynom-Ring (n,R))); ::_thesis: ( ( 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 Element of NAT
for b being bag of n st p3 = A . 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 Element of NAT
for b being bag of n st p3 = B . p1 & p2 = p3 . i holds
p2 . b = p1 . (b bag_extend i) ) implies A = B )
assume A25: 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 Element of NAT
for b being bag of n st p3 = A . p1 & p2 = p3 . i holds
p2 . b = p1 . (b bag_extend i) ; ::_thesis: ( ex p1 being Polynomial of (n + 1),R ex p2 being Polynomial of n,R ex p3 being Polynomial of (Polynom-Ring (n,R)) ex i being Element of NAT ex b being bag of n st
( p3 = B . p1 & p2 = p3 . i & not p2 . b = p1 . (b bag_extend i) ) or A = B )
assume A26: 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 Element of NAT
for b being bag of n st p3 = B . p1 & p2 = p3 . i holds
p2 . b = p1 . (b bag_extend i) ; ::_thesis: A = B
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(Polynom-Ring_((n_+_1),R))_holds_
A_._x_=_B_._x
let x be set ; ::_thesis: ( x in the carrier of (Polynom-Ring ((n + 1),R)) implies A . x = B . x )
assume A27: x in the carrier of (Polynom-Ring ((n + 1),R)) ; ::_thesis: A . x = B . x
then reconsider x99 = x as Element of the carrier of (Polynom-Ring ((n + 1),R)) ;
reconsider x9 = x as Polynomial of (n + 1),R by A27, POLYNOM1:def_10;
reconsider Ax = A . x99, Bx = B . x99 as Polynomial of (Polynom-Ring (n,R)) by POLYNOM3:def_10;
now__::_thesis:_for_i_being_set_st_i_in_NAT_holds_
Ax_._i_=_Bx_._i
let i be set ; ::_thesis: ( i in NAT implies Ax . i = Bx . i )
assume i in NAT ; ::_thesis: Ax . i = Bx . i
then reconsider i9 = i as Element of NAT ;
reconsider Axi = Ax . i9, Bxi = Bx . i9 as Polynomial of n,R by POLYNOM1:def_10;
now__::_thesis:_for_b_being_set_st_b_in_Bags_n_holds_
Axi_._b_=_Bxi_._b
let b be set ; ::_thesis: ( b in Bags n implies Axi . b = Bxi . b )
assume b in Bags n ; ::_thesis: Axi . b = Bxi . b
then reconsider b9 = b as bag of n ;
thus Axi . b = x9 . (b9 bag_extend i9) by A25
.= Bxi . b by A26 ; ::_thesis: verum
end;
hence Ax . i = Bx . i by FUNCT_2:12; ::_thesis: verum
end;
hence A . x = B . x by FUNCT_2:12; ::_thesis: verum
end;
hence A = B by FUNCT_2:12; ::_thesis: verum
end;
end;
:: deftheorem Def7 defines mpu HILBASIS:def_7_:_
for R being non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for n being Element of 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 Element of 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
for R being non empty non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for n being Element of NAT
for p being Element of (Polynom-Ring ((n + 1),R)) holds (upm (n,R)) . ((mpu (n,R)) . p) = p
proof
let R be non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for n being Element of NAT
for p being Element of (Polynom-Ring ((n + 1),R)) holds (upm (n,R)) . ((mpu (n,R)) . p) = p
let n be Element of NAT ; ::_thesis: for p being Element of (Polynom-Ring ((n + 1),R)) holds (upm (n,R)) . ((mpu (n,R)) . p) = p
let p be Element of (Polynom-Ring ((n + 1),R)); ::_thesis: (upm (n,R)) . ((mpu (n,R)) . p) = p
set PNR = Polynom-Ring (n,R);
reconsider p9 = p as Polynomial of (n + 1),R by POLYNOM1:def_10;
reconsider upmmpup = (upm (n,R)) . ((mpu (n,R)) . p) as Polynomial of (n + 1),R by POLYNOM1:def_10;
reconsider mpup = (mpu (n,R)) . p as Polynomial of (Polynom-Ring (n,R)) by POLYNOM3:def_10;
now__::_thesis:_for_b9_being_set_st_b9_in_Bags_(n_+_1)_holds_
upmmpup_._b9_=_p9_._b9
let b9 be set ; ::_thesis: ( b9 in Bags (n + 1) implies upmmpup . b9 = p9 . b9 )
assume b9 in Bags (n + 1) ; ::_thesis: upmmpup . b9 = p9 . b9
then reconsider b = b9 as Element of Bags (n + 1) ;
reconsider mpupbn = mpup . (b . n) as Polynomial of n,R by POLYNOM1:def_10;
n < n + 1 by NAT_1:13;
then reconsider bn = b | n as bag of n by Th3;
A1: b = bn bag_extend (b . n) by Def1;
thus upmmpup . b9 = mpupbn . bn by Def6
.= p9 . b9 by A1, Def7 ; ::_thesis: verum
end;
hence (upm (n,R)) . ((mpu (n,R)) . p) = p by FUNCT_2:12; ::_thesis: verum
end;
theorem Th31: :: HILBASIS:31
for R being non empty non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for n being Element of NAT ex P being Function of (Polynom-Ring (Polynom-Ring (n,R))),(Polynom-Ring ((n + 1),R)) st P is RingIsomorphism
proof
let R be non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for n being Element of NAT ex P being Function of (Polynom-Ring (Polynom-Ring (n,R))),(Polynom-Ring ((n + 1),R)) st P is RingIsomorphism
let n be Element of NAT ; ::_thesis: ex P being Function of (Polynom-Ring (Polynom-Ring (n,R))),(Polynom-Ring ((n + 1),R)) st P is RingIsomorphism
set PN1R = Polynom-Ring ((n + 1),R);
set CPRPNR = the carrier of (Polynom-Ring (Polynom-Ring (n,R)));
set CPN1R = the carrier of (Polynom-Ring ((n + 1),R));
set P = upm (n,R);
A1: upm (n,R) is RingHomomorphism by QUOFIELD:def_18;
then A2: upm (n,R) is RingMonomorphism by QUOFIELD:def_20;
now__::_thesis:_for_p_being_set_st_p_in_the_carrier_of_(Polynom-Ring_((n_+_1),R))_holds_
p_in_rng_(upm_(n,R))
let p be set ; ::_thesis: ( p in the carrier of (Polynom-Ring ((n + 1),R)) implies p in rng (upm (n,R)) )
assume p in the carrier of (Polynom-Ring ((n + 1),R)) ; ::_thesis: p in rng (upm (n,R))
then reconsider p9 = p as Element of the carrier of (Polynom-Ring ((n + 1),R)) ;
( dom (upm (n,R)) = the carrier of (Polynom-Ring (Polynom-Ring (n,R))) & (upm (n,R)) . ((mpu (n,R)) . p9) = p9 ) by Th30, FUNCT_2:def_1;
hence p in rng (upm (n,R)) by FUNCT_1:def_3; ::_thesis: verum
end;
then the carrier of (Polynom-Ring ((n + 1),R)) c= rng (upm (n,R)) by TARSKI:def_3;
then rng (upm (n,R)) = the carrier of (Polynom-Ring ((n + 1),R)) by XBOOLE_0:def_10;
then upm (n,R) is RingEpimorphism by A1, QUOFIELD:def_19;
then upm (n,R) is RingIsomorphism by A2, QUOFIELD:def_21;
hence ex P being Function of (Polynom-Ring (Polynom-Ring (n,R))),(Polynom-Ring ((n + 1),R)) st P is RingIsomorphism ; ::_thesis: verum
end;
begin
registration
let R be non empty right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive Noetherian doubleLoopStr ;
cluster Polynom-Ring R -> Noetherian ;
coherence
Polynom-Ring R is Noetherian
proof
set cR = the carrier of R;
set PR = Polynom-Ring R;
set cPR = the carrier of (Polynom-Ring R);
now__::_thesis:_Polynom-Ring_R_is_Noetherian
assume not Polynom-Ring R is Noetherian ; ::_thesis: contradiction
then consider I being Ideal of (Polynom-Ring R) such that
A1: not I is finitely_generated by IDEAL_1:def_26;
defpred S1[ set , set , set ] means ( c2 is non empty finite Subset of I implies ex A, B being non empty Subset of the carrier of (Polynom-Ring R) st
( A = c2 & B = I \ (A -Ideal) & ex r being Element of the carrier of (Polynom-Ring R) st
( r in minlen B & c3 = c2 \/ {r} ) ) );
A2: now__::_thesis:_for_n_being_Element_of_NAT_
for_x_being_Subset_of_the_carrier_of_(Polynom-Ring_R)_ex_y_being_Subset_of_the_carrier_of_(Polynom-Ring_R)_st_S1[n,x,y]
let n be Element of NAT ; ::_thesis: for x being Subset of the carrier of (Polynom-Ring R) ex y being Subset of the carrier of (Polynom-Ring R) st S1[y,b3,b4]
let x be Subset of the carrier of (Polynom-Ring R); ::_thesis: ex y being Subset of the carrier of (Polynom-Ring R) st S1[y,b2,b3]
percases ( not x is non empty finite Subset of I or x is non empty finite Subset of I ) ;
suppose x is not non empty finite Subset of I ; ::_thesis: ex y being Subset of the carrier of (Polynom-Ring R) st S1[y,b2,b3]
hence ex y being Subset of the carrier of (Polynom-Ring R) st S1[n,x,y] ; ::_thesis: verum
end;
supposeA3: x is non empty finite Subset of I ; ::_thesis: ex y being Subset of the carrier of (Polynom-Ring R) st S1[y,b2,b3]
then reconsider x9 = x as non empty Subset of the carrier of (Polynom-Ring R) ;
set B = I \ (x9 -Ideal);
now__::_thesis:_not_I_\_(x9_-Ideal)_=_{}
assume I \ (x9 -Ideal) = {} ; ::_thesis: contradiction
then A4: I c= x9 -Ideal by XBOOLE_1:37;
x9 -Ideal c= I -Ideal by A3, IDEAL_1:57;
then x9 -Ideal c= I by IDEAL_1:44;
hence contradiction by A1, A3, A4, XBOOLE_0:def_10; ::_thesis: verum
end;
then reconsider B = I \ (x9 -Ideal) as non empty Subset of the carrier of (Polynom-Ring R) ;
consider r being set such that
A5: r in minlen B by XBOOLE_0:def_1;
minlen B c= the carrier of (Polynom-Ring R) by XBOOLE_1:1;
then reconsider r = r as Element of the carrier of (Polynom-Ring R) by A5;
S1[n,x,x9 \/ {r}] by A5;
hence ex y being Subset of the carrier of (Polynom-Ring R) st S1[n,x,y] ; ::_thesis: verum
end;
end;
end;
consider F being Function of NAT,(bool the carrier of (Polynom-Ring R)) such that
A6: ( F . 0 = {(0. (Polynom-Ring R))} & ( for n being Element of NAT holds S1[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch_2(A2);
defpred S2[ set , set ] means ex n being Element of NAT ex A, B being non empty Subset of the carrier of (Polynom-Ring R) st
( A = F . n & B = I \ (A -Ideal) & n = R & F . (n + 1) = (F . n) \/ {c2} & c2 in minlen B );
defpred S3[ Element of NAT ] means F . R is non empty finite Subset of I;
A7: now__::_thesis:_for_n_being_Element_of_NAT_st_S3[n]_holds_
S3[n_+_1]
let n be Element of NAT ; ::_thesis: ( S3[n] implies S3[n + 1] )
assume S3[n] ; ::_thesis: S3[n + 1]
then reconsider Fn = F . n as non empty finite Subset of I ;
consider A, B being non empty Subset of the carrier of (Polynom-Ring R) such that
A = Fn and
A8: B = I \ (A -Ideal) and
A9: ex r being Element of the carrier of (Polynom-Ring R) st
( r in minlen B & F . (n + 1) = Fn \/ {r} ) by A6;
consider r being Element of the carrier of (Polynom-Ring R) such that
A10: r in minlen B and
A11: F . (n + 1) = Fn \/ {r} by A9;
r in I by A8, A10, XBOOLE_0:def_5;
then {r} c= I by ZFMISC_1:31;
hence S3[n + 1] by A11, XBOOLE_1:8; ::_thesis: verum
end;
F . 0 c= I
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F . 0 or x in I )
assume x in F . 0 ; ::_thesis: x in I
then x = 0. (Polynom-Ring R) by A6, TARSKI:def_1;
hence x in I by IDEAL_1:2; ::_thesis: verum
end;
then A12: S3[ 0 ] by A6;
A13: for n being Element of NAT holds S3[n] from NAT_1:sch_1(A12, A7);
A14: now__::_thesis:_for_x_being_Element_of_NAT_ex_y_being_Element_of_the_carrier_of_(Polynom-Ring_R)_st_S2[x,y]
let x be Element of NAT ; ::_thesis: ex y being Element of the carrier of (Polynom-Ring R) st S2[x,y]
ex A, B being non empty Subset of the carrier of (Polynom-Ring R) st
( A = F . x & B = I \ (A -Ideal) & ex r being Element of the carrier of (Polynom-Ring R) st
( r in minlen B & F . (x + 1) = (F . x) \/ {r} ) ) by A6, A13;
hence ex y being Element of the carrier of (Polynom-Ring R) st S2[x,y] ; ::_thesis: verum
end;
consider f being Function of NAT, the carrier of (Polynom-Ring R) such that
A15: for x being Element of NAT holds S2[x,f . x] from FUNCT_2:sch_3(A14);
A16: for i, j being Element of NAT st i <= j holds
F . i c= F . j
proof
let i, j be Element of NAT ; ::_thesis: ( i <= j implies F . i c= F . j )
defpred S4[ Element of NAT ] means F . i c= F . (i + R);
assume i <= j ; ::_thesis: F . i c= F . j
then consider m being Nat such that
A17: j = i + m by NAT_1:10;
A18: for m being Element of NAT st S4[m] holds
S4[m + 1]
proof
let m be Element of NAT ; ::_thesis: ( S4[m] implies S4[m + 1] )
ex A, B being non empty Subset of the carrier of (Polynom-Ring R) st
( A = F . (i + m) & B = I \ (A -Ideal) & ex r being Element of the carrier of (Polynom-Ring R) st
( r in minlen B & F . ((i + m) + 1) = (F . (i + m)) \/ {r} ) ) by A6, A13;
then A19: F . (i + m) c= F . ((i + m) + 1) by XBOOLE_1:7;
assume F . i c= F . (i + m) ; ::_thesis: S4[m + 1]
hence S4[m + 1] by A19, XBOOLE_1:1; ::_thesis: verum
end;
A20: S4[ 0 ] ;
A21: for m being Element of NAT holds S4[m] from NAT_1:sch_1(A20, A18);
m in NAT by ORDINAL1:def_12;
hence F . i c= F . j by A17, A21; ::_thesis: verum
end;
A22: for i being Element of NAT holds f . i <> 0. (Polynom-Ring R)
proof
let i be Element of NAT ; ::_thesis: f . i <> 0. (Polynom-Ring R)
consider n being Element of NAT , A, B being non empty Subset of the carrier of (Polynom-Ring R) such that
A23: A = F . n and
A24: B = I \ (A -Ideal) and
n = i and
F . (n + 1) = (F . n) \/ {(f . i)} and
A25: f . i in minlen B by A15;
F . n c= A -Ideal by A23, IDEAL_1:def_14;
then A26: not f . i in F . n by A24, A25, XBOOLE_0:def_5;
( F . 0 c= F . n & 0. (Polynom-Ring R) in F . 0 ) by A6, A16, TARSKI:def_1;
hence f . i <> 0. (Polynom-Ring R) by A26; ::_thesis: verum
end;
A27: now__::_thesis:_for_i_being_Element_of_NAT_
for_fi_being_Polynomial_of_R_st_fi_=_f_._i_holds_
(len_fi)_-_1_>=_0
let i be Element of NAT ; ::_thesis: for fi being Polynomial of R st fi = f . i holds
(len fi) - 1 >= 0
let fi be Polynomial of R; ::_thesis: ( fi = f . i implies (len fi) - 1 >= 0 )
assume fi = f . i ; ::_thesis: (len fi) - 1 >= 0
then fi <> 0. (Polynom-Ring R) by A22;
then fi <> 0_. R by POLYNOM3:def_10;
then len fi <> 0 by POLYNOM4:5;
then len fi >= 0 + 1 by NAT_1:13;
hence (len fi) - 1 >= 0 by XREAL_1:19; ::_thesis: verum
end;
defpred S4[ set , set ] means ex n being Element of NAT ex A being Polynomial of R st
( n = R & A = f . n & c2 = A . ((len A) -' 1) );
A28: now__::_thesis:_for_x_being_Element_of_NAT_ex_y_being_Element_of_the_carrier_of_R_st_S4[x,y]
let x be Element of NAT ; ::_thesis: ex y being Element of the carrier of R st S4[x,y]
reconsider fx = f . x as Polynomial of R by POLYNOM3:def_10;
fx . ((len fx) -' 1) is Element of the carrier of R ;
hence ex y being Element of the carrier of R st S4[x,y] ; ::_thesis: verum
end;
consider a being Function of NAT, the carrier of R such that
A29: for x being Element of NAT holds S4[x,a . x] from FUNCT_2:sch_3(A28);
reconsider a = a as sequence of R ;
for B being non empty Subset of the carrier of R ex C being non empty finite Subset of the carrier of R st
( C c= B & C -Ideal = B -Ideal ) by IDEAL_1:96;
then consider m being Element of NAT such that
A30: a . (m + 1) in (rng (a | (m + 1))) -Ideal by IDEAL_1:97;
reconsider fm1 = f . (m + 1) as Polynomial of R by POLYNOM3:def_10;
defpred S5[ set , set ] means ( ex u, v, w being Element of the carrier of R st
( R = (u * v) * w & v in rng (a | (Segm (m + 1))) ) implies ex x, y, z being Element of the carrier of (Polynom-Ring R) ex p being Polynomial of R st
( c2 = p & p = (x * y) * z & R = p . ((len fm1) -' 1) & len p <= len fm1 & y in F . (m + 1) ) );
A31: ex n being Element of NAT ex A, B being non empty Subset of the carrier of (Polynom-Ring R) st
( A = F . n & B = I \ (A -Ideal) & n = m + 1 & F . (n + 1) = (F . n) \/ {(f . (m + 1))} & f . (m + 1) in minlen B ) by A15;
A32: for i, j being Element of NAT
for fi, fj being Polynomial of R st i <= j & fi = f . i & fj = f . j holds
len fi <= len fj
proof
let i, j be Element of NAT ; ::_thesis: for fi, fj being Polynomial of R st i <= j & fi = f . i & fj = f . j holds
len fi <= len fj
let fi, fj be Polynomial of R; ::_thesis: ( i <= j & fi = f . i & fj = f . j implies len fi <= len fj )
assume that
A33: i <= j and
A34: fi = f . i and
A35: fj = f . j ; ::_thesis: len fi <= len fj
consider k being Nat such that
A36: j = i + k by A33, NAT_1:10;
defpred S6[ Element of NAT ] means for fk being Polynomial of R st fk = f . (i + R) holds
len fi <= len fk;
A37: now__::_thesis:_for_k_being_Element_of_NAT_st_S6[k]_holds_
S6[k_+_1]
let k be Element of NAT ; ::_thesis: ( S6[k] implies S6[k + 1] )
assume A38: S6[k] ; ::_thesis: S6[k + 1]
now__::_thesis:_for_fk1_being_Polynomial_of_R_st_fk1_=_f_._(i_+_(k_+_1))_holds_
len_fi_<=_len_fk1
reconsider fk = f . (i + k) as Polynomial of R by POLYNOM3:def_10;
let fk1 be Polynomial of R; ::_thesis: ( fk1 = f . (i + (k + 1)) implies len fi <= len fk1 )
A39: len fi <= len fk by A38;
consider n being Element of NAT , A, B being non empty Subset of the carrier of (Polynom-Ring R) such that
A40: A = F . n and
A41: B = I \ (A -Ideal) and
A42: n = i + k and
F . (n + 1) = (F . n) \/ {(f . (i + k))} and
A43: f . (i + k) in minlen B by A15;
consider n9 being Element of NAT , A9, B9 being non empty Subset of the carrier of (Polynom-Ring R) such that
A44: A9 = F . n9 and
A45: B9 = I \ (A9 -Ideal) and
A46: n9 = i + (k + 1) and
F . (n9 + 1) = (F . n9) \/ {(f . (i + (k + 1)))} and
A47: f . (i + (k + 1)) in minlen B9 by A15;
A48: f . (i + (k + 1)) in I by A45, A47, XBOOLE_0:def_5;
i + (k + 1) = (i + k) + 1 ;
then i + k < i + (k + 1) by NAT_1:13;
then A -Ideal c= A9 -Ideal by A16, A40, A42, A44, A46, IDEAL_1:57;
then not f . (i + (k + 1)) in A -Ideal by A45, A47, XBOOLE_0:def_5;
then A49: f . (i + (k + 1)) in B by A41, A48, XBOOLE_0:def_5;
assume fk1 = f . (i + (k + 1)) ; ::_thesis: len fi <= len fk1
then len fk <= len fk1 by A43, A49, Th17;
hence len fi <= len fk1 by A39, XXREAL_0:2; ::_thesis: verum
end;
hence S6[k + 1] ; ::_thesis: verum
end;
A50: S6[ 0 ] by A34;
A51: for k being Element of NAT holds S6[k] from NAT_1:sch_1(A50, A37);
k in NAT by ORDINAL1:def_12;
hence len fi <= len fj by A35, A36, A51; ::_thesis: verum
end;
A52: for e being set st e in the carrier of R holds
ex d being set st
( d in the carrier of (Polynom-Ring R) & S5[e,d] )
proof
let e be set ; ::_thesis: ( e in the carrier of R implies ex d being set st
( d in the carrier of (Polynom-Ring R) & S5[e,d] ) )
assume e in the carrier of R ; ::_thesis: ex d being set st
( d in the carrier of (Polynom-Ring R) & S5[e,d] )
percases ( ex u, v, w being Element of the carrier of R st
( e = (u * v) * w & v in rng (a | (Segm (m + 1))) ) or for u, v, w being Element of the carrier of R holds
( not e = (u * v) * w or not v in rng (a | (Segm (m + 1))) ) ) ;
suppose ex u, v, w being Element of the carrier of R st
( e = (u * v) * w & v in rng (a | (Segm (m + 1))) ) ; ::_thesis: ex d being set st
( d in the carrier of (Polynom-Ring R) & S5[e,d] )
then consider u, b9, w being Element of the carrier of R such that
A53: e = (u * b9) * w and
A54: b9 in rng (a | (Segm (m + 1))) ;
consider n being set such that
A55: n in dom (a | (Segm (m + 1))) and
A56: b9 = (a | (Segm (m + 1))) . n by A54, FUNCT_1:def_3;
set c9 = w;
set a9 = u;
set z9 = monomial (w,0);
A57: (len fm1) -' 1 = ((len fm1) -' 1) + 0 ;
reconsider n = n as Element of NAT by A55;
set y = f . n;
reconsider y9 = f . n as Polynomial of R by POLYNOM3:def_10;
set x9 = monomial (u,((len fm1) -' (len y9)));
dom (a | (Segm (m + 1))) = (dom a) /\ (Segm (m + 1)) by RELAT_1:61
.= NAT /\ (Segm (m + 1)) by FUNCT_2:def_1
.= Segm (m + 1) by XBOOLE_1:28 ;
then A58: n < m + 1 by A55, NAT_1:44;
then len y9 <= len fm1 by A32;
then (len y9) - (len y9) <= (len fm1) - (len y9) by XREAL_1:9;
then A59: (len fm1) -' (len y9) = (len fm1) - (len y9) by XREAL_0:def_2;
then len (monomial (u,((len fm1) -' (len y9)))) <= ((len fm1) - (len y9)) + 1 by Th18;
then A60: (len (monomial (u,((len fm1) -' (len y9))))) + ((len y9) - 1) <= ((len fm1) - ((len y9) - 1)) + ((len y9) - 1) by XREAL_1:6;
A61: len ((monomial (u,((len fm1) -' (len y9)))) *' y9) <= ((len (monomial (u,((len fm1) -' (len y9))))) + (len y9)) -' 1 by Th21;
A62: (len y9) - 1 >= 0 by A27;
then 0 + 0 <= ((len y9) - 1) + (len (monomial (u,((len fm1) -' (len y9))))) ;
then len ((monomial (u,((len fm1) -' (len y9)))) *' y9) <= ((len (monomial (u,((len fm1) -' (len y9))))) + (len y9)) - 1 by A61, XREAL_0:def_2;
then A63: len ((monomial (u,((len fm1) -' (len y9)))) *' y9) <= len fm1 by A60, XXREAL_0:2;
(len fm1) - 1 >= 0 by A27;
then A64: (len fm1) -' 1 = ((len fm1) - (len y9)) + ((len y9) - 1) by XREAL_0:def_2
.= ((len y9) -' 1) + ((len fm1) -' (len y9)) by A59, A62, XREAL_0:def_2 ;
reconsider x = monomial (u,((len fm1) -' (len y9))), z = monomial (w,0) as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def_10;
set p = (x * (f . n)) * z;
A65: x * (f . n) = (monomial (u,((len fm1) -' (len y9)))) *' y9 by POLYNOM3:def_10;
then A66: (x * (f . n)) * z = ((monomial (u,((len fm1) -' (len y9)))) *' y9) *' (monomial (w,0)) by POLYNOM3:def_10;
reconsider p = (x * (f . n)) * z as Polynomial of R by POLYNOM3:def_10;
A67: ex n9 being Element of NAT ex A being Polynomial of R st
( n9 = n & A = f . n9 & a . n = A . ((len A) -' 1) ) by A29;
b9 = a . n by A55, A56, FUNCT_1:47;
then ((monomial (u,((len fm1) -' (len y9)))) *' y9) . ((len fm1) -' 1) = u * b9 by A67, A64, Th19;
then A68: (u * b9) * w = p . ((len fm1) -' 1) by A66, A57, Th20;
ex n9 being Element of NAT ex A, B being non empty Subset of the carrier of (Polynom-Ring R) st
( A = F . n9 & B = I \ (A -Ideal) & n9 = n & F . (n9 + 1) = (F . n9) \/ {(f . n)} & f . n in minlen B ) by A15;
then {(f . n)} c= F . (n + 1) by XBOOLE_1:7;
then A69: f . n in F . (n + 1) by ZFMISC_1:31;
len (monomial (w,0)) <= 0 + 1 by Th18;
then (len ((monomial (u,((len fm1) -' (len y9)))) *' y9)) + (len (monomial (w,0))) <= (len fm1) + 1 by A63, XREAL_1:7;
then A70: ((len ((monomial (u,((len fm1) -' (len y9)))) *' y9)) + (len (monomial (w,0)))) -' 1 <= ((len fm1) + 1) -' 1 by NAT_D:42;
len (((monomial (u,((len fm1) -' (len y9)))) *' y9) *' (monomial (w,0))) <= ((len ((monomial (u,((len fm1) -' (len y9)))) *' y9)) + (len (monomial (w,0)))) -' 1 by Th21;
then len (((monomial (u,((len fm1) -' (len y9)))) *' y9) *' (monomial (w,0))) <= ((len fm1) + 1) -' 1 by A70, XXREAL_0:2;
then len (((monomial (u,((len fm1) -' (len y9)))) *' y9) *' (monomial (w,0))) <= ((len fm1) + 1) - 1 by XREAL_0:def_2;
then A71: len p <= (len fm1) + 0 by A65, POLYNOM3:def_10;
n + 1 <= m + 1 by A58, NAT_1:13;
then F . (n + 1) c= F . (m + 1) by A16;
hence ex d being set st
( d in the carrier of (Polynom-Ring R) & S5[e,d] ) by A53, A68, A71, A69; ::_thesis: verum
end;
suppose for u, v, w being Element of the carrier of R holds
( not e = (u * v) * w or not v in rng (a | (Segm (m + 1))) ) ; ::_thesis: ex d being set st
( d in the carrier of (Polynom-Ring R) & S5[e,d] )
hence ex d being set st
( d in the carrier of (Polynom-Ring R) & S5[e,d] ) ; ::_thesis: verum
end;
end;
end;
consider LCT being Function of the carrier of R, the carrier of (Polynom-Ring R) such that
A72: for e being set st e in the carrier of R holds
S5[e,LCT . e] from FUNCT_2:sch_1(A52);
reconsider FM1 = F . (m + 1) as non empty Subset of the carrier of (Polynom-Ring R) by A13;
set raSm1 = rng (a | (Segm (m + 1)));
consider lc being LinearCombination of rng (a | (Segm (m + 1))) such that
A73: a . (m + 1) = Sum lc by A30, IDEAL_1:60;
A74: for lc being LinearCombination of rng (a | (Segm (m + 1))) ex LC being LinearCombination of FM1 st
( LC = LCT * lc & len lc = len LC )
proof
let lc be LinearCombination of rng (a | (Segm (m + 1))); ::_thesis: ex LC being LinearCombination of FM1 st
( LC = LCT * lc & len lc = len LC )
set LC = LCT * lc;
dom LCT = the carrier of R by FUNCT_2:def_1;
then rng lc c= dom LCT ;
then A75: dom lc = dom (LCT * lc) by RELAT_1:27;
then A76: len lc = len (LCT * lc) by FINSEQ_3:29;
LCT * lc is LinearCombination of FM1
proof
let i be set ; :: according to IDEAL_1:def_8 ::_thesis: ( not i in dom (LCT * lc) or ex b1, b2 being Element of the carrier of (Polynom-Ring R) ex b3 being Element of FM1 st (LCT * lc) /. i = (b1 * b3) * b2 )
assume A77: i in dom (LCT * lc) ; ::_thesis: ex b1, b2 being Element of the carrier of (Polynom-Ring R) ex b3 being Element of FM1 st (LCT * lc) /. i = (b1 * b3) * b2
consider u, v being Element of R, a being Element of rng (a | (Segm (m + 1))) such that
A78: lc /. i = (u * a) * v by A75, A77, IDEAL_1:def_8;
A79: lc /. i = lc . i by A75, A77, PARTFUN1:def_6;
consider x, y, z being Element of the carrier of (Polynom-Ring R), p being Polynomial of R such that
A80: ( LCT . (lc /. i) = p & p = (x * y) * z ) and
(u * a) * v = p . ((len fm1) -' 1) and
len p <= len fm1 and
A81: y in F . (m + 1) by A72, A78;
reconsider y = y as Element of FM1 by A81;
reconsider x = x, z = z as Element of (Polynom-Ring R) ;
(LCT * lc) /. i = (LCT * lc) . i by A77, PARTFUN1:def_6
.= (x * y) * z by A75, A77, A79, A80, FUNCT_1:13 ;
hence ex x, z being Element of (Polynom-Ring R) ex y being Element of FM1 st (LCT * lc) /. i = (x * y) * z ; ::_thesis: verum
end;
then reconsider LC = LCT * lc as LinearCombination of FM1 ;
LC = LC ;
hence ex LC being LinearCombination of FM1 st
( LC = LCT * lc & len lc = len LC ) by A76; ::_thesis: verum
end;
for lc being LinearCombination of rng (a | (Segm (m + 1))) ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 )
proof
let lc be LinearCombination of rng (a | (Segm (m + 1))); ::_thesis: ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 )
defpred S6[ Element of NAT ] means for lc being LinearCombination of rng (a | (Segm (m + 1))) st len lc <= R holds
ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 );
A82: ex n being Element of NAT st n = len lc ;
A83: for k being Element of NAT st S6[k] holds
S6[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S6[k] implies S6[k + 1] )
assume A84: S6[k] ; ::_thesis: S6[k + 1]
thus S6[k + 1] ::_thesis: verum
proof
let lc be LinearCombination of rng (a | (Segm (m + 1))); ::_thesis: ( len lc <= k + 1 implies ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 ) )
assume A85: len lc <= k + 1 ; ::_thesis: ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 )
percases ( len lc <= k or len lc > k ) ;
suppose len lc <= k ; ::_thesis: ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 )
hence ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 ) by A84; ::_thesis: verum
end;
supposeA86: len lc > k ; ::_thesis: ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 )
then len lc >= k + 1 by NAT_1:13;
then A87: len lc = k + 1 by A85, XXREAL_0:1;
thus ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 ) ::_thesis: verum
proof
percases ( k = 0 or k > 0 ) ;
supposeA88: k = 0 ; ::_thesis: ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 )
then dom lc = {1} by A87, FINSEQ_1:2, FINSEQ_1:def_3;
then A89: 1 in dom lc by TARSKI:def_1;
then consider u, w being Element of R, v being Element of rng (a | (Segm (m + 1))) such that
A90: lc /. 1 = (u * v) * w by IDEAL_1:def_8;
A91: lc . 1 = lc /. 1 by A89, PARTFUN1:def_6;
then consider x, y, z being Element of the carrier of (Polynom-Ring R), p being Polynomial of R such that
A92: LCT . (lc . 1) = p and
p = (x * y) * z and
A93: (u * v) * w = p . ((len fm1) -' 1) and
A94: len p <= len fm1 and
y in F . (m + 1) by A72, A90;
A95: lc = <*(lc . 1)*> by A87, A88, FINSEQ_1:40;
then A96: Sum lc = p . ((len fm1) -' 1) by A90, A91, A93, RLVECT_1:44;
consider LC being LinearCombination of FM1 such that
A97: LC = LCT * lc and
len LC = len lc by A74;
LC = <*(LCT . ((u * v) * w))*> by A95, A90, A91, A97, FINSEQ_2:35;
then Sum LC = p by A90, A91, A92, RLVECT_1:44;
hence ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 ) by A94, A97, A96; ::_thesis: verum
end;
supposeA98: k > 0 ; ::_thesis: ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 )
consider LC being LinearCombination of FM1 such that
A99: LC = LCT * lc and
len LC = len lc by A74;
not lc is empty by A86;
then consider p being LinearCombination of rng (a | (Segm (m + 1))), e being Element of the carrier of R such that
A100: lc = p ^ <*e*> and
A101: <*e*> is LinearCombination of rng (a | (Segm (m + 1))) by IDEAL_1:32;
len <*e*> = 0 + 1 by FINSEQ_1:39;
then len <*e*> <= k by A98, NAT_1:13;
then consider LCe being LinearCombination of FM1, sLCe being Polynomial of R such that
A102: LCe = LCT * <*e*> and
A103: sLCe = Sum LCe and
A104: sLCe . ((len fm1) -' 1) = Sum <*e*> and
A105: len sLCe <= len fm1 by A84, A101;
len lc = (len p) + (len <*e*>) by A100, FINSEQ_1:22
.= (len p) + 1 by FINSEQ_1:39 ;
then consider LCp being LinearCombination of FM1, sLCp being Polynomial of R such that
A106: LCp = LCT * p and
A107: sLCp = Sum LCp and
A108: sLCp . ((len fm1) -' 1) = Sum p and
A109: len sLCp <= len fm1 by A84, A87;
set sLC = sLCp + sLCe;
A110: Sum lc = (Sum p) + e by A100, FVSUM_1:71
.= (sLCp . ((len fm1) -' 1)) + (sLCe . ((len fm1) -' 1)) by A108, A104, RLVECT_1:44
.= (sLCp + sLCe) . ((len fm1) -' 1) by NORMSP_1:def_2 ;
A111: now__::_thesis:_len_(sLCp_+_sLCe)_<=_len_fm1
percases ( len sLCp < len sLCe or len sLCp >= len sLCe ) ;
suppose len sLCp < len sLCe ; ::_thesis: len (sLCp + sLCe) <= len fm1
then len (sLCp + sLCe) <= len sLCe by POLYNOM4:6;
hence len (sLCp + sLCe) <= len fm1 by A105, XXREAL_0:2; ::_thesis: verum
end;
suppose len sLCp >= len sLCe ; ::_thesis: len (sLCp + sLCe) <= len fm1
then len (sLCp + sLCe) <= len sLCp by POLYNOM4:6;
hence len (sLCp + sLCe) <= len fm1 by A109, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
dom LCT = the carrier of R by FUNCT_2:def_1;
then (rng p) \/ (rng <*e*>) c= dom LCT ;
then ex LCTp, LCTe being FinSequence st
( LCTp = LCT * p & LCTe = LCT * <*e*> & LCT * (p ^ <*e*>) = LCTp ^ LCTe ) by Th1;
then Sum LC = (Sum LCp) + (Sum LCe) by A100, A106, A102, A99, RLVECT_1:41
.= sLCp + sLCe by A107, A103, POLYNOM3:def_10 ;
hence ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 ) by A99, A110, A111; ::_thesis: verum
end;
end;
end;
end;
end;
end;
end;
A112: S6[ 0 ]
proof
let lc be LinearCombination of rng (a | (Segm (m + 1))); ::_thesis: ( len lc <= 0 implies ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 ) )
assume A113: len lc <= 0 ; ::_thesis: ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 )
then A114: lc = <*> the carrier of R ;
consider LC being LinearCombination of FM1 such that
A115: LC = LCT * lc and
A116: len lc = len LC by A74;
take LC ; ::_thesis: ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 )
take p = 0_. R; ::_thesis: ( LC = LCT * lc & p = Sum LC & p . ((len fm1) -' 1) = Sum lc & len p <= len fm1 )
thus LC = LCT * lc by A115; ::_thesis: ( p = Sum LC & p . ((len fm1) -' 1) = Sum lc & len p <= len fm1 )
LC = <*> the carrier of (Polynom-Ring R) by A113, A116;
then Sum LC = 0. (Polynom-Ring R) by RLVECT_1:43
.= p by POLYNOM3:def_10 ;
hence p = Sum LC ; ::_thesis: ( p . ((len fm1) -' 1) = Sum lc & len p <= len fm1 )
thus p . ((len fm1) -' 1) = 0. R by FUNCOP_1:7
.= Sum lc by A114, RLVECT_1:43 ; ::_thesis: len p <= len fm1
thus len p <= len fm1 by POLYNOM4:3; ::_thesis: verum
end;
for k being Element of NAT holds S6[k] from NAT_1:sch_1(A112, A83);
hence ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 ) by A82; ::_thesis: verum
end;
then consider LC being LinearCombination of FM1, sLC being Polynomial of R such that
LC = LCT * lc and
A117: sLC = Sum LC and
A118: sLC . ((len fm1) -' 1) = Sum lc and
A119: len sLC <= len fm1 ;
A120: sLC in FM1 -Ideal by A117, IDEAL_1:60;
set f9 = fm1 - sLC;
A121: now__::_thesis:_not_len_(fm1_-_sLC)_=_len_fm1
ex n being Element of NAT ex A being Polynomial of R st
( n = m + 1 & A = f . n & a . (m + 1) = A . ((len A) -' 1) ) by A29;
then A122: (fm1 - sLC) . ((len fm1) -' 1) = (fm1 . ((len fm1) -' 1)) - (fm1 . ((len fm1) -' 1)) by A73, A118, POLYNOM3:27
.= 0. R by RLVECT_1:15 ;
(len fm1) - 1 >= 0 by A27;
then A123: ((len fm1) -' 1) + 1 = ((len fm1) - 1) + 1 by XREAL_0:def_2
.= len fm1 ;
assume len (fm1 - sLC) = len fm1 ; ::_thesis: contradiction
hence contradiction by A123, A122, ALGSEQ_1:10; ::_thesis: verum
end;
A124: (fm1 - sLC) + sLC = fm1 + (sLC + (- sLC)) by POLYNOM3:26
.= fm1 + (sLC - sLC)
.= fm1 + (0_. R) by POLYNOM3:29
.= fm1 by POLYNOM3:28 ;
A125: now__::_thesis:_not_fm1_-_sLC_in_FM1_-Ideal
reconsider sLC = sLC as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def_10;
assume A126: fm1 - sLC in FM1 -Ideal ; ::_thesis: contradiction
reconsider f9 = fm1 - sLC as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def_10;
f . (m + 1) = f9 + sLC by A124, POLYNOM3:def_10;
then fm1 in FM1 -Ideal by A120, A126, IDEAL_1:def_1;
hence contradiction by A31, XBOOLE_0:def_5; ::_thesis: verum
end;
len (- sLC) <= len fm1 by A119, POLYNOM4:8;
then len (fm1 - sLC) <= len fm1 by POLYNOM4:6;
then A127: len (fm1 - sLC) < len fm1 by A121, XXREAL_0:1;
fm1 - sLC in I
proof
reconsider f9 = fm1 - sLC as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def_10;
reconsider sLC = sLC as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def_10;
FM1 is Subset of I by A13;
then FM1 -Ideal c= I -Ideal by IDEAL_1:57;
then A128: FM1 -Ideal c= I by IDEAL_1:44;
( f . (m + 1) in I & f9 = (f . (m + 1)) - sLC ) by A31, Th16, XBOOLE_0:def_5;
hence fm1 - sLC in I by A120, A128, IDEAL_1:15; ::_thesis: verum
end;
then fm1 - sLC in I \ (FM1 -Ideal) by A125, XBOOLE_0:def_5;
hence contradiction by A127, A31, Th17; ::_thesis: verum
end;
hence Polynom-Ring R is Noetherian ; ::_thesis: verum
end;
end;
theorem Th32: :: HILBASIS:32
for R being non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr st R is Noetherian holds
for n being Element of NAT holds Polynom-Ring (n,R) is Noetherian
proof
let R be non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ; ::_thesis: ( R is Noetherian implies for n being Element of NAT holds Polynom-Ring (n,R) is Noetherian )
assume A1: R is Noetherian ; ::_thesis: for n being Element of NAT holds Polynom-Ring (n,R) is Noetherian
defpred S1[ Element of NAT ] means Polynom-Ring ($1,R) is Noetherian ;
A2: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; ::_thesis: S1[k + 1]
ex P being Function of (Polynom-Ring (Polynom-Ring (k,R))),(Polynom-Ring ((k + 1),R)) st P is RingIsomorphism by Th31;
hence S1[k + 1] by A3, Th27; ::_thesis: verum
end;
ex P being Function of R,(Polynom-Ring (0,R)) st P is RingIsomorphism by Th28;
then A4: S1[ 0 ] by A1, Th27;
thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2); ::_thesis: verum
end;
theorem Th33: :: HILBASIS:33
for F being Field holds F is Noetherian
proof
let F be Field; ::_thesis: F is Noetherian
let I be Ideal of F; :: according to IDEAL_1:def_26 ::_thesis: I is finitely_generated
percases ( I = {(0. F)} or I = the carrier of F ) by IDEAL_1:22;
supposeA1: I = {(0. F)} ; ::_thesis: I is finitely_generated
reconsider s0F = {(0. F)} as non empty finite Subset of F ;
{(0. F)} = s0F -Ideal by IDEAL_1:47;
hence I is finitely_generated by A1; ::_thesis: verum
end;
supposeA2: I = the carrier of F ; ::_thesis: I is finitely_generated
reconsider s1F = {(1_ F)} as non empty finite Subset of F ;
the carrier of F = s1F -Ideal by IDEAL_1:51;
hence I is finitely_generated by A2; ::_thesis: verum
end;
end;
end;
theorem :: HILBASIS:34
for F being Field
for n being Element of NAT holds Polynom-Ring (n,F) is Noetherian
proof
let F be Field; ::_thesis: for n being Element of NAT holds Polynom-Ring (n,F) is Noetherian
let n be Element of NAT ; ::_thesis: Polynom-Ring (n,F) is Noetherian
F is Noetherian by Th33;
hence Polynom-Ring (n,F) is Noetherian by Th32; ::_thesis: verum
end;
theorem :: HILBASIS:35
for R being non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for X being infinite Ordinal holds not Polynom-Ring (X,R) is Noetherian
proof
deffunc H1( set ) -> set = $1;
let R be non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for X being infinite Ordinal holds not Polynom-Ring (X,R) is Noetherian
let X be infinite Ordinal; ::_thesis: not Polynom-Ring (X,R) is Noetherian
assume A1: Polynom-Ring (X,R) is Noetherian ; ::_thesis: contradiction
reconsider f0 = X --> (0. R) as Function of X, the carrier of R ;
deffunc H2( Element of X) -> Series of X,R = 1_1 ($1,R);
set tcR = the carrier of R;
A2: for d1, d2 being Element of X st H2(d1) = H2(d2) holds
d1 = d2 by Th14;
the carrier of R c= the carrier of R ;
then reconsider cR = the carrier of R as non empty Subset of the carrier of R ;
set S = { (1_1 (n,R)) where n is Element of X : n in NAT } ;
set tcPR = the carrier of (Polynom-Ring (X,R));
A3: NAT c= X by CARD_3:85;
0 in NAT ;
then reconsider 0X = 0 as Element of X by A3;
A4: { (1_1 (n,R)) where n is Element of X : n in NAT } c= the carrier of (Polynom-Ring (X,R))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (1_1 (n,R)) where n is Element of X : n in NAT } or x in the carrier of (Polynom-Ring (X,R)) )
assume x in { (1_1 (n,R)) where n is Element of X : n in NAT } ; ::_thesis: x in the carrier of (Polynom-Ring (X,R))
then ex n being Element of X st
( x = 1_1 (n,R) & n in NAT ) ;
hence x in the carrier of (Polynom-Ring (X,R)) by POLYNOM1:def_10; ::_thesis: verum
end;
1_1 (0X,R) in { (1_1 (n,R)) where n is Element of X : n in NAT } ;
then reconsider S = { (1_1 (n,R)) where n is Element of X : n in NAT } as non empty Subset of the carrier of (Polynom-Ring (X,R)) by A4;
consider C being non empty finite Subset of the carrier of (Polynom-Ring (X,R)) such that
A5: C c= S and
A6: C -Ideal = S -Ideal by A1, IDEAL_1:96;
set CN = { H1(n) where n is Element of X : H2(n) in C } ;
A7: C is finite ;
A8: { H1(n) where n is Element of X : H2(n) in C } is finite from FUNCT_7:sch_2(A7, A2);
A9: { H1(n) where n is Element of X : H2(n) in C } c= NAT
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { H1(n) where n is Element of X : H2(n) in C } or x in NAT )
assume x in { H1(n) where n is Element of X : H2(n) in C } ; ::_thesis: x in NAT
then consider n being Element of X such that
A10: x = n and
A11: 1_1 (n,R) in C ;
1_1 (n,R) in S by A5, A11;
then ex m being Element of X st
( 1_1 (n,R) = 1_1 (m,R) & m in NAT ) ;
hence x in NAT by A10, Th14; ::_thesis: verum
end;
set c = the Element of C;
the Element of C in C ;
then the Element of C in S by A5;
then consider cn being Element of X such that
A12: the Element of C = 1_1 (cn,R) and
A13: cn in NAT ;
reconsider cn = cn as Element of NAT by A13;
cn in { H1(n) where n is Element of X : H2(n) in C } by A12;
then reconsider CN = { H1(n) where n is Element of X : H2(n) in C } as non empty finite Subset of NAT by A8, A9;
reconsider mm = max CN as Element of NAT by ORDINAL1:def_12;
reconsider m1 = mm + 1 as Element of NAT ;
m1 in NAT ;
then reconsider m2 = m1 as Element of X by A3;
( 1_1 (m2,R) in S & S c= S -Ideal ) by IDEAL_1:def_14;
then consider lc being LinearCombination of C such that
A14: 1_1 (m2,R) = Sum lc by A6, IDEAL_1:60;
reconsider ev = f0 +* (m2,(1_ R)) as Function of X,R ;
consider E being FinSequence of [: the carrier of (Polynom-Ring (X,R)), the carrier of (Polynom-Ring (X,R)), the carrier of (Polynom-Ring (X,R)):] such that
A15: E represents lc by IDEAL_1:35;
set P = Polynom-Evaluation (X,R,ev);
deffunc H3( Nat) -> Element of the carrier of R = (((Polynom-Evaluation (X,R,ev)) . ((E /. $1) `1_3)) * ((Polynom-Evaluation (X,R,ev)) . ((E /. $1) `2_3))) * ((Polynom-Evaluation (X,R,ev)) . ((E /. $1) `3_3));
consider LC being FinSequence of the carrier of R such that
A16: len LC = len lc and
A17: for k being Nat st k in dom LC holds
LC . k = H3(k) from FINSEQ_2:sch_1();
now__::_thesis:_for_i_being_set_st_i_in_dom_LC_holds_
ex_u,_v_being_Element_of_R_ex_a_being_Element_of_cR_st_LC_/._i_=_(u_*_a)_*_v
let i be set ; ::_thesis: ( i in dom LC implies ex u, v being Element of R ex a being Element of cR st LC /. i = (u * a) * v )
assume A18: i in dom LC ; ::_thesis: ex u, v being Element of R ex a being Element of cR st LC /. i = (u * a) * v
then reconsider k = i as Element of NAT ;
reconsider a = (Polynom-Evaluation (X,R,ev)) . ((E /. k) `2_3) as Element of cR ;
reconsider u = (Polynom-Evaluation (X,R,ev)) . ((E /. k) `1_3), v = (Polynom-Evaluation (X,R,ev)) . ((E /. k) `3_3) as Element of R ;
take u = u; ::_thesis: ex v being Element of R ex a being Element of cR st LC /. i = (u * a) * v
take v = v; ::_thesis: ex a being Element of cR st LC /. i = (u * a) * v
take a = a; ::_thesis: LC /. i = (u * a) * v
thus LC /. i = LC . k by A18, PARTFUN1:def_6
.= (u * a) * v by A17, A18 ; ::_thesis: verum
end;
then reconsider LC = LC as LinearCombination of cR by IDEAL_1:def_8;
A19: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_LC_holds_
LC_._i_=_0._R
let i be Element of NAT ; ::_thesis: ( i in dom LC implies LC . i = 0. R )
A20: now__::_thesis:_not_m2_in_CN
assume m2 in CN ; ::_thesis: contradiction
then (max CN) + 1 <= max CN by XXREAL_2:def_8;
hence contradiction by XREAL_1:29; ::_thesis: verum
end;
assume A21: i in dom LC ; ::_thesis: LC . i = 0. R
then i in dom lc by A16, FINSEQ_3:29;
then reconsider y = (E /. i) `2_3 as Element of C by A15, IDEAL_1:def_11;
y in C ;
then y in S by A5;
then consider n being Element of X such that
A22: y = 1_1 (n,R) and
n in NAT ;
n in CN by A22;
then A23: ev . n = (X --> (0. R)) . n by A20, FUNCT_7:32
.= 0. R by FUNCOP_1:7 ;
A24: Support (1_1 (n,R)) = {(UnitBag n)} by Th13;
A25: (Polynom-Evaluation (X,R,ev)) . (1_1 (n,R)) = eval ((1_1 (n,R)),ev) by POLYNOM2:def_5
.= ((1_1 (n,R)) . (UnitBag n)) * (eval ((UnitBag n),ev)) by A24, POLYNOM2:19
.= (1_ R) * (eval ((UnitBag n),ev)) by Th12
.= (1_ R) * (ev . n) by Th11
.= 0. R by A23, VECTSP_1:6 ;
thus LC . i = (((Polynom-Evaluation (X,R,ev)) . ((E /. i) `1_3)) * ((Polynom-Evaluation (X,R,ev)) . ((E /. i) `2_3))) * ((Polynom-Evaluation (X,R,ev)) . ((E /. i) `3_3)) by A17, A21
.= (0. R) * ((Polynom-Evaluation (X,R,ev)) . ((E /. i) `3_3)) by A22, A25, VECTSP_1:6
.= 0. R by VECTSP_1:6 ; ::_thesis: verum
end;
dom (X --> (0. R)) = X by FUNCOP_1:13;
then A26: ev . m2 = 1_ R by FUNCT_7:31;
A27: Support (1_1 (m2,R)) = {(UnitBag m2)} by Th13;
A28: (Polynom-Evaluation (X,R,ev)) . (1_1 (m2,R)) = eval ((1_1 (m2,R)),ev) by POLYNOM2:def_5
.= ((1_1 (m2,R)) . (UnitBag m2)) * (eval ((UnitBag m2),ev)) by A27, POLYNOM2:19
.= (1_ R) * (eval ((UnitBag m2),ev)) by Th12
.= (1_ R) * (ev . m2) by Th11
.= 1_ R by A26, GROUP_1:def_4 ;
for k being set st k in dom LC holds
LC . k = (((Polynom-Evaluation (X,R,ev)) . ((E /. k) `1_3)) * ((Polynom-Evaluation (X,R,ev)) . ((E /. k) `2_3))) * ((Polynom-Evaluation (X,R,ev)) . ((E /. k) `3_3)) by A17;
then (Polynom-Evaluation (X,R,ev)) . (Sum lc) = Sum LC by A15, A16, Th24
.= 0. R by A19, POLYNOM3:1 ;
hence contradiction by A14, A28; ::_thesis: verum
end;