let n be Ordinal; for L being non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for f being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring (n,L))
for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f holds
Support f c= union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A & A /. i = m *' p ) }
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ; for f being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring (n,L))
for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f holds
Support f c= union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A & A /. i = m *' p ) }
let f be Polynomial of n,L; for P being non empty Subset of (Polynom-Ring (n,L))
for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f holds
Support f c= union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A & A /. i = m *' p ) }
let P be non empty Subset of (Polynom-Ring (n,L)); for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f holds
Support f c= union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A & A /. i = m *' p ) }
let A be LeftLinearCombination of P; ( A is_MonomialRepresentation_of f implies Support f c= union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A & A /. i = m *' p ) } )
assume A1:
A is_MonomialRepresentation_of f
; Support f c= union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A & A /. i = m *' p ) }
defpred S1[ Nat] means for f being Polynomial of n,L
for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f & len A = $1 holds
Support f c= union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A & A /. i = m *' p ) } ;
A2:
ex n being Element of NAT st len A = n
;
A3:
now for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume A4:
S1[
k]
;
S1[k + 1]
for
f being
Polynomial of
n,
L for
A being
LeftLinearCombination of
P st
A is_MonomialRepresentation_of f &
len A = k + 1 holds
Support f c= union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A & A /. i = m *' p ) }
proof
A5:
k <= k + 1
by NAT_1:11;
let f be
Polynomial of
n,
L;
for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f & len A = k + 1 holds
Support f c= union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A & A /. i = m *' p ) } let A be
LeftLinearCombination of
P;
( A is_MonomialRepresentation_of f & len A = k + 1 implies Support f c= union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A & A /. i = m *' p ) } )
assume that A6:
A is_MonomialRepresentation_of f
and A7:
len A = k + 1
;
Support f c= union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A & A /. i = m *' p ) }
A8:
A <> <*> the
carrier of
(Polynom-Ring (n,L))
by A7;
A9:
Sum A = f
by A6;
reconsider A =
A as non
empty LeftLinearCombination of
P by A8;
consider A9 being
LeftLinearCombination of
P,
e being
Element of
(Polynom-Ring (n,L)) such that A10:
A = A9 ^ <*e*>
and
<*e*> is
LeftLinearCombination of
P
by IDEAL_1:33;
A11:
dom A = Seg (k + 1)
by A7, FINSEQ_1:def 3;
reconsider ep =
Sum <*e*> as
Polynomial of
n,
L by POLYNOM1:def 11;
reconsider g =
Sum A9 as
Polynomial of
n,
L by POLYNOM1:def 11;
f =
(Sum A9) + (Sum <*e*>)
by A9, A10, RLVECT_1:41
.=
g + ep
by POLYNOM1:def 11
;
then A12:
Support f c= (Support g) \/ (Support ep)
by POLYNOM1:20;
A13:
len A =
(len A9) + (len <*e*>)
by A10, FINSEQ_1:22
.=
(len A9) + 1
by FINSEQ_1:39
;
then
dom A9 = Seg k
by A7, FINSEQ_1:def 3;
then A14:
dom A9 c= dom A
by A11, A5, FINSEQ_1:5;
now for i being Element of NAT st i in dom A9 holds
ex m being Monomial of n,L ex p being Polynomial of n,L st
( p in P & A9 /. i = m *' p )let i be
Element of
NAT ;
( i in dom A9 implies ex m being Monomial of n,L ex p being Polynomial of n,L st
( p in P & A9 /. i = m *' p ) )assume A15:
i in dom A9
;
ex m being Monomial of n,L ex p being Polynomial of n,L st
( p in P & A9 /. i = m *' p )then A /. i =
A . i
by A14, PARTFUN1:def 6
.=
A9 . i
by A10, A15, FINSEQ_1:def 7
.=
A9 /. i
by A15, PARTFUN1:def 6
;
hence
ex
m being
Monomial of
n,
L ex
p being
Polynomial of
n,
L st
(
p in P &
A9 /. i = m *' p )
by A6, A14, A15;
verum end;
then
A9 is_MonomialRepresentation_of g
;
then A16:
Support g c= union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A9 & A9 /. i = m *' p ) }
by A4, A7, A13;
now for x being object st x in Support f holds
x in union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A & A /. i = m *' p ) } let x be
object ;
( x in Support f implies x in union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A & A /. i = m *' p ) } )assume A17:
x in Support f
;
x in union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A & A /. i = m *' p ) } then reconsider u =
x as
Element of
Bags n ;
now ( ( u in Support g & u in union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A & A /. i = m *' p ) } ) or ( u in Support ep & u in union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A & A /. i = m *' p ) } ) )per cases
( u in Support g or u in Support ep )
by A12, A17, XBOOLE_0:def 3;
case
u in Support g
;
u in union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A & A /. i = m *' p ) } then consider Y being
set such that A18:
u in Y
and A19:
Y in { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A9 & A9 /. i = m *' p ) }
by A16, TARSKI:def 4;
consider m9 being
Monomial of
n,
L,
p9 being
Polynomial of
n,
L such that A20:
Y = Support (m9 *' p9)
and A21:
ex
i being
Element of
NAT st
(
i in dom A9 &
A9 /. i = m9 *' p9 )
by A19;
consider i being
Element of
NAT such that A22:
i in dom A9
and A23:
A9 /. i = m9 *' p9
by A21;
A /. i =
A . i
by A14, A22, PARTFUN1:def 6
.=
A9 . i
by A10, A22, FINSEQ_1:def 7
.=
A9 /. i
by A22, PARTFUN1:def 6
;
then
Y in { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A & A /. i = m *' p ) }
by A14, A20, A22, A23;
hence
u in union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A & A /. i = m *' p ) }
by A18, TARSKI:def 4;
verum end; case A24:
u in Support ep
;
u in union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A & A /. i = m *' p ) }
1
<= len A
by A7, NAT_1:11;
then A25:
len A in Seg (len A)
by FINSEQ_1:1;
dom A = Seg (len A)
by FINSEQ_1:def 3;
then A26:
ex
m9 being
Monomial of
n,
L ex
p9 being
Polynomial of
n,
L st
(
p9 in P &
A /. (len A) = m9 *' p9 )
by A6, A25;
A27:
(
A . (len A) = e &
e = Sum <*e*> )
by A10, A13, FINSEQ_1:42, RLVECT_1:44;
A28:
len A in dom A
by A25, FINSEQ_1:def 3;
then
A /. (len A) = A . (len A)
by PARTFUN1:def 6;
then
Support ep in { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A & A /. i = m *' p ) }
by A28, A26, A27;
hence
u in union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A & A /. i = m *' p ) }
by A24, TARSKI:def 4;
verum hence
x in union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A & A /. i = m *' p ) }
;
verum end;
hence
Support f c= union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A & A /. i = m *' p ) }
by TARSKI:def 3;
verum
end; hence
S1[
k + 1]
;
verum end;
A29:
S1[ 0 ]
proof
let f be
Polynomial of
n,
L;
for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f & len A = 0 holds
Support f c= union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A & A /. i = m *' p ) } let A be
LeftLinearCombination of
P;
( A is_MonomialRepresentation_of f & len A = 0 implies Support f c= union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A & A /. i = m *' p ) } )
assume that A30:
A is_MonomialRepresentation_of f
and A31:
len A = 0
;
Support f c= union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A & A /. i = m *' p ) }
A = <*> the
carrier of
(Polynom-Ring (n,L))
by A31;
then
Sum A = 0. (Polynom-Ring (n,L))
by RLVECT_1:43;
then
f = 0. (Polynom-Ring (n,L))
by A30;
then
f = 0_ (
n,
L)
by POLYNOM1:def 11;
then
Support f = {}
by POLYNOM7:1;
hence
Support f c= union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A & A /. i = m *' p ) }
by XBOOLE_1:2;
verum
end;
for k being Nat holds S1[k]
from NAT_1:sch 2(A29, A3);
hence
Support f c= union { (Support (m *' p)) where m is Monomial of n,L, p is Polynomial of n,L : ex i being Element of NAT st
( i in dom A & A /. i = m *' p ) }
by A1, A2; verum