set n = card (nonConstantPolys F);
set q = Poly (m,(LM p));
per cases ( m in card (nonConstantPolys F) or not m in card (nonConstantPolys F) ) ;
suppose m in card (nonConstantPolys F) ; :: thesis: Poly (m,(LM p)) is monomial-like
then for o being object st o in {m} holds
o in card (nonConstantPolys F) by TARSKI:def 1;
then reconsider S = {m} as finite Subset of (card (nonConstantPolys F)) by TARSKI:def 3;
per cases ( not p is constant or p is constant ) ;
suppose not p is constant ; :: thesis: Poly (m,(LM p)) is monomial-like
then deg p > 0 by RATFUNC1:def 2;
then Z2: (len p) - 1 > 0 by HURWITZ:def 2;
then Z3: (len p) - 1 = (len p) -' 1 by XREAL_0:def 2;
set c = (S,((len p) -' 1)) -bag ;
E: {m} = support ((S,((len p) -' 1)) -bag) by Z2, Z3, UPROOTS:8;
X: now :: thesis: for b being bag of card (nonConstantPolys F) st (Poly (m,(LM p))) . b <> 0. F holds
b = (S,((len p) -' 1)) -bag
let b be bag of card (nonConstantPolys F); :: thesis: ( (Poly (m,(LM p))) . b <> 0. F implies b = (S,((len p) -' 1)) -bag )
assume AS: (Poly (m,(LM p))) . b <> 0. F ; :: thesis: b = (S,((len p) -' 1)) -bag
A: now :: thesis: not support b = {}
assume support b = {} ; :: thesis: contradiction
then b = EmptyBag (card (nonConstantPolys F)) by PRE_POLY:81;
then (Poly (m,(LM p))) . b = (LM p) . 0 by defPg
.= 0. F by Z2, Z3, POLYNOM4:def 1 ;
hence contradiction by AS; :: thesis: verum
end;
B: ( support b = {} or support b = {m} ) by AS, defPg;
then (Poly (m,(LM p))) . b = (LM p) . (b . m) by A, defPg;
then C: b . m = (len p) -' 1 by AS, POLYNOM4:def 1;
thus b = (S,((len p) -' 1)) -bag :: thesis: verum
proof
now :: thesis: for o being object st o in card (nonConstantPolys F) holds
b . o = ((S,((len p) -' 1)) -bag) . o
let o be object ; :: thesis: ( o in card (nonConstantPolys F) implies b . b1 = ((S,((len p) -' 1)) -bag) . b1 )
assume o in card (nonConstantPolys F) ; :: thesis: b . b1 = ((S,((len p) -' 1)) -bag) . b1
per cases ( o in support b or not o in support b ) ;
suppose D: o in support b ; :: thesis: b . b1 = ((S,((len p) -' 1)) -bag) . b1
then o = m by B, TARSKI:def 1;
hence b . o = ((S,((len p) -' 1)) -bag) . o by B, C, D, UPROOTS:7; :: thesis: verum
end;
suppose D: not o in support b ; :: thesis: b . b1 = ((S,((len p) -' 1)) -bag) . b1
hence b . o = 0 by PRE_POLY:def 7
.= ((S,((len p) -' 1)) -bag) . o by A, B, D, E, PRE_POLY:def 7 ;
:: thesis: verum
end;
end;
end;
hence b = (S,((len p) -' 1)) -bag by PBOOLE:3; :: thesis: verum
end;
end;
ex b being bag of card (nonConstantPolys F) st
for b1 being bag of card (nonConstantPolys F) st b1 <> b holds
(Poly (m,(LM p))) . b1 = 0. F
proof
take (S,((len p) -' 1)) -bag ; :: thesis: for b1 being bag of card (nonConstantPolys F) st b1 <> (S,((len p) -' 1)) -bag holds
(Poly (m,(LM p))) . b1 = 0. F
thus for b1 being bag of card (nonConstantPolys F) st b1 <> (S,((len p) -' 1)) -bag holds
(Poly (m,(LM p))) . b1 = 0. F by X; :: thesis: verum
end;
hence Poly (m,(LM p)) is monomial-like by POLYNOM7:def 3; :: thesis: verum
end;
suppose Z: p is constant ; :: thesis: Poly (m,(LM p)) is monomial-like
reconsider p1 = p as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
Z2: deg p <= 0 by Z, RATFUNC1:def 2;
Z1: (len p) -' 1 = 0
proof
per cases ( (len p) - 1 = 0 or (len p) - 1 < 0 ) by Z2, HURWITZ:def 2;
suppose (len p) - 1 = 0 ; :: thesis: (len p) -' 1 = 0
hence (len p) -' 1 = 0 by XREAL_0:def 2; :: thesis: verum
end;
suppose (len p) - 1 < 0 ; :: thesis: (len p) -' 1 = 0
hence (len p) -' 1 = 0 by XREAL_0:def 2; :: thesis: verum
end;
end;
end;
X: now :: thesis: for b being bag of card (nonConstantPolys F) st (Poly (m,(LM p))) . b <> 0. F holds
b = EmptyBag (card (nonConstantPolys F))
let b be bag of card (nonConstantPolys F); :: thesis: ( (Poly (m,(LM p))) . b <> 0. F implies b = EmptyBag (card (nonConstantPolys F)) )
assume AS: (Poly (m,(LM p))) . b <> 0. F ; :: thesis: b = EmptyBag (card (nonConstantPolys F))
A: now :: thesis: not support b = {m}
assume B: support b = {m} ; :: thesis: contradiction
m in {m} by TARSKI:def 1;
then C: b . m <> 0 by B, PRE_POLY:def 7;
(Poly (m,(LM p))) . b = (LM p) . (b . m) by B, defPg
.= 0. F by C, Z1, POLYNOM4:def 1 ;
hence contradiction by AS; :: thesis: verum
end;
( support b = {} or support b = {m} ) by AS, defPg;
then for i being object st i in card (nonConstantPolys F) holds
b . i = {} by A, PRE_POLY:def 7;
hence b = EmptyBag (card (nonConstantPolys F)) by PBOOLE:6; :: thesis: verum
end;
ex b being bag of card (nonConstantPolys F) st
for b1 being bag of card (nonConstantPolys F) st b1 <> b holds
(Poly (m,(LM p))) . b1 = 0. F
proof
take EmptyBag (card (nonConstantPolys F)) ; :: thesis: for b1 being bag of card (nonConstantPolys F) st b1 <> EmptyBag (card (nonConstantPolys F)) holds
(Poly (m,(LM p))) . b1 = 0. F
thus for b1 being bag of card (nonConstantPolys F) st b1 <> EmptyBag (card (nonConstantPolys F)) holds
(Poly (m,(LM p))) . b1 = 0. F by X; :: thesis: verum
end;
hence Poly (m,(LM p)) is monomial-like by POLYNOM7:def 3; :: thesis: verum
end;
end;
end;
suppose Y: not m in card (nonConstantPolys F) ; :: thesis: Poly (m,(LM p)) is monomial-like
ex b being bag of card (nonConstantPolys F) st
for b1 being bag of card (nonConstantPolys F) st b1 <> b holds
(Poly (m,(LM p))) . b1 = 0. F
proof
take EmptyBag (card (nonConstantPolys F)) ; :: thesis: for b1 being bag of card (nonConstantPolys F) st b1 <> EmptyBag (card (nonConstantPolys F)) holds
(Poly (m,(LM p))) . b1 = 0. F
thus for b1 being bag of card (nonConstantPolys F) st b1 <> EmptyBag (card (nonConstantPolys F)) holds
(Poly (m,(LM p))) . b1 = 0. F by X; :: thesis: verum
end;
hence Poly (m,(LM p)) is monomial-like by POLYNOM7:def 3; :: thesis: verum
end;
end;