let n be Ordinal; for L being non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for p, q being Polynomial of n,L
for b1, b2 being bag of n st Support p = {b1} & Support q = {b2} holds
for x being Function of n,L holds eval ((p *' q),x) = (eval (p,x)) * (eval (q,x))
let L be non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ; for p, q being Polynomial of n,L
for b1, b2 being bag of n st Support p = {b1} & Support q = {b2} holds
for x being Function of n,L holds eval ((p *' q),x) = (eval (p,x)) * (eval (q,x))
let p, q be Polynomial of n,L; for b1, b2 being bag of n st Support p = {b1} & Support q = {b2} holds
for x being Function of n,L holds eval ((p *' q),x) = (eval (p,x)) * (eval (q,x))
let b1, b2 be bag of n; ( Support p = {b1} & Support q = {b2} implies for x being Function of n,L holds eval ((p *' q),x) = (eval (p,x)) * (eval (q,x)) )
assume that
A1:
Support p = {b1}
and
A2:
Support q = {b2}
; for x being Function of n,L holds eval ((p *' q),x) = (eval (p,x)) * (eval (q,x))
consider s being FinSequence of the carrier of L such that
A3:
(p *' q) . (b1 + b2) = Sum s
and
A4:
len s = len (decomp (b1 + b2))
and
A5:
for k being Element of NAT st k in dom s holds
ex u1, u2 being bag of n st
( (decomp (b1 + b2)) /. k = <*u1,u2*> & s /. k = (p . u1) * (q . u2) )
by POLYNOM1:def 10;
A6:
b1 + b2 is Element of Bags n
by PRE_POLY:def 12;
let x be Function of n,L; eval ((p *' q),x) = (eval (p,x)) * (eval (q,x))
A7: ((p . b1) * (q . b2)) * ((eval (b1,x)) * (eval (b2,x))) =
(((p . b1) * (q . b2)) * (eval (b1,x))) * (eval (b2,x))
by GROUP_1:def 3
.=
(((p . b1) * (eval (b1,x))) * (q . b2)) * (eval (b2,x))
by GROUP_1:def 3
.=
((p . b1) * (eval (b1,x))) * ((q . b2) * (eval (b2,x)))
by GROUP_1:def 3
.=
(eval (p,x)) * ((q . b2) * (eval (b2,x)))
by A1, Th11
.=
(eval (p,x)) * (eval (q,x))
by A2, Th11
;
A8:
for b being bag of n st b <> b2 holds
q . b = 0. L
A10:
for b being bag of n st b <> b1 holds
p . b = 0. L
A12:
for u being object st u in Support (p *' q) holds
u in {(b1 + b2)}
proof
let u be
object ;
( u in Support (p *' q) implies u in {(b1 + b2)} )
assume A13:
u in Support (p *' q)
;
u in {(b1 + b2)}
assume A14:
not
u in {(b1 + b2)}
;
contradiction
reconsider u =
u as
bag of
n by A13;
consider t being
FinSequence of the
carrier of
L such that A15:
(p *' q) . u = Sum t
and A16:
len t = len (decomp u)
and A17:
for
k being
Element of
NAT st
k in dom t holds
ex
b19,
b29 being
bag of
n st
(
(decomp u) /. k = <*b19,b29*> &
t /. k = (p . b19) * (q . b29) )
by POLYNOM1:def 10;
1
<= len t
by A16, NAT_1:14;
then A18:
1
in dom t
by FINSEQ_3:25;
A19:
dom t =
Seg (len t)
by FINSEQ_1:def 3
.=
dom (decomp u)
by A16, FINSEQ_1:def 3
;
A20:
for
i being
Element of
NAT st
i in dom t holds
t /. i = 0. L
proof
let i be
Element of
NAT ;
( i in dom t implies t /. i = 0. L )
consider S being non
empty finite Subset of
(Bags n) such that A21:
divisors u = SgmX (
(BagOrder n),
S)
and A22:
for
b being
bag of
n holds
(
b in S iff
b divides u )
by PRE_POLY:def 16;
BagOrder n linearly_orders S
by Lm3;
then A23:
S = rng (divisors u)
by A21, PRE_POLY:def 2;
assume A24:
i in dom t
;
t /. i = 0. L
then consider b19,
b29 being
bag of
n such that A25:
(decomp u) /. i = <*b19,b29*>
and A26:
t /. i = (p . b19) * (q . b29)
by A17;
A27:
b19 = (divisors u) /. i
by A19, A24, A25, PRE_POLY:70;
A28:
i in dom (divisors u)
by A19, A24, PRE_POLY:def 17;
then
b19 = (divisors u) . i
by A27, PARTFUN1:def 6;
then
b19 in rng (divisors u)
by A28, FUNCT_1:def 3;
then A29:
b19 divides u
by A22, A23;
per cases
( ( b19 = b1 & b29 = b2 ) or b19 <> b1 or b29 <> b2 )
;
suppose A30:
(
b19 = b1 &
b29 = b2 )
;
t /. i = 0. Lb2 =
<*b1,b2*> . 2
by FINSEQ_1:44
.=
<*b1,(u -' b1)*> . 2
by A19, A24, A25, A27, A30, PRE_POLY:def 17
.=
u -' b1
by FINSEQ_1:44
;
then
b1 + b2 = u
by A29, A30, PRE_POLY:47;
hence
t /. i = 0. L
by A14, TARSKI:def 1;
verum end; end;
end;
then
for
i being
Element of
NAT st
i in dom t &
i <> 1 holds
t /. i = 0. L
;
then Sum t =
t /. 1
by A18, Th2
.=
0. L
by A18, A20
;
hence
contradiction
by A13, A15, POLYNOM1:def 4;
verum
end;
consider k being Element of NAT such that
A31:
k in dom (decomp (b1 + b2))
and
A32:
(decomp (b1 + b2)) /. k = <*b1,b2*>
by PRE_POLY:69;
A33: dom s =
Seg (len s)
by FINSEQ_1:def 3
.=
dom (decomp (b1 + b2))
by A4, FINSEQ_1:def 3
;
then consider b19, b29 being bag of n such that
A34:
(decomp (b1 + b2)) /. k = <*b19,b29*>
and
A35:
s /. k = (p . b19) * (q . b29)
by A5, A31;
A36: b2 =
<*b1,b2*> . 2
by FINSEQ_1:44
.=
b29
by A32, A34, FINSEQ_1:44
;
A37:
for k9 being Element of NAT st k9 in dom s & k9 <> k holds
s /. k9 = 0. L
proof
let k9 be
Element of
NAT ;
( k9 in dom s & k9 <> k implies s /. k9 = 0. L )
assume that A38:
k9 in dom s
and A39:
k9 <> k
;
s /. k9 = 0. L
consider b19,
b29 being
bag of
n such that A40:
(decomp (b1 + b2)) /. k9 = <*b19,b29*>
and A41:
s /. k9 = (p . b19) * (q . b29)
by A5, A38;
per cases
( ( b19 = b1 & b29 = b2 ) or b19 <> b1 or b29 <> b2 )
;
suppose A42:
(
b19 = b1 &
b29 = b2 )
;
s /. k9 = 0. L(decomp (b1 + b2)) . k9 =
(decomp (b1 + b2)) /. k9
by A33, A38, PARTFUN1:def 6
.=
(decomp (b1 + b2)) . k
by A31, A32, A40, A42, PARTFUN1:def 6
;
hence
s /. k9 = 0. L
by A33, A31, A38, A39, FUNCT_1:def 4;
verum end; end;
end;
b1 =
<*b19,b29*> . 1
by A32, A34, FINSEQ_1:44
.=
b19
by FINSEQ_1:44
;
then A43:
(p *' q) . (b1 + b2) = (p . b1) * (q . b2)
by A3, A33, A31, A35, A36, A37, Th2;