per cases ( Support (m1 *' m2) = {} or Support (m1 *' m2) <> {} ) ;
suppose Support (m1 *' m2) = {} ; :: thesis: m1 *' m2 is monomial-like
hence m1 *' m2 is monomial-like by POLYNOM7:6; :: thesis: verum
end;
suppose A1: Support (m1 *' m2) <> {} ; :: thesis: m1 *' m2 is monomial-like
now
per cases ( ( Support m1 <> {} & Support m2 <> {} ) or Support m1 = {} or Support m2 = {} ) ;
case A2: ( Support m1 <> {} & Support m2 <> {} ) ; :: thesis: m1 *' m2 is monomial-like
then consider mb1 being bag of such that
A3: Support m1 = {mb1} by POLYNOM7:6;
mb1 in Support m1 by A3, TARSKI:def 1;
then A4: m1 . mb1 <> 0. L by POLYNOM1:def 9;
A5: now
let b be bag of ; :: thesis: ( b <> mb1 implies m1 . b = 0. L )
assume A6: b <> mb1 ; :: thesis: m1 . b = 0. L
consider b' being bag of such that
A7: for b being bag of st b <> b' holds
m1 . b = 0. L by POLYNOM7:def 4;
b' = mb1 by A4, A7;
hence m1 . b = 0. L by A6, A7; :: thesis: verum
end;
consider mb2 being bag of such that
A8: Support m2 = {mb2} by A2, POLYNOM7:6;
mb2 in Support m2 by A8, TARSKI:def 1;
then A9: m2 . mb2 <> 0. L by POLYNOM1:def 9;
A10: now
let b be bag of ; :: thesis: ( b <> mb2 implies m2 . b = 0. L )
assume A11: b <> mb2 ; :: thesis: m2 . b = 0. L
consider b' being bag of such that
A12: for b being bag of st b <> b' holds
m2 . b = 0. L by POLYNOM7:def 4;
b' = mb2 by A9, A12;
hence m2 . b = 0. L by A11, A12; :: thesis: verum
end;
consider b being Element of Support (m1 *' m2);
A13: b in Support (m1 *' m2) by A1;
then b is Element of Bags n ;
then reconsider b = b as bag of ;
consider s being FinSequence of L such that
A14: ( (m1 *' m2) . 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 st
( (decomp b) /. k = <*b1,b2*> & s /. k = (m1 . b1) * (m2 . b2) ) ) ) by POLYNOM1:def 26;
A15: dom s = Seg (len (decomp b)) by A14, FINSEQ_1:def 3
.= dom (decomp b) by FINSEQ_1:def 3 ;
A16: now
assume A17: b <> mb1 + mb2 ; :: thesis: contradiction
A18: now
let k be Element of NAT ; :: thesis: ( k in dom s implies s /. k = 0. L )
assume A19: k in dom s ; :: thesis: s /. k = 0. L
then consider b1, b2 being bag of such that
A20: ( (decomp b) /. k = <*b1,b2*> & s /. k = (m1 . b1) * (m2 . b2) ) by A14;
consider b1', b2' being bag of such that
A21: ( (decomp b) /. k = <*b1',b2'*> & b = b1' + b2' ) by A15, A19, POLYNOM1:72;
A22: b1 = <*b1',b2'*> . 1 by A20, A21, FINSEQ_1:61
.= b1' by FINSEQ_1:61 ;
A23: b2 = <*b1',b2'*> . 2 by A20, A21, FINSEQ_1:61
.= b2' by FINSEQ_1:61 ;
now
per cases ( b1 <> mb1 or b2 <> mb2 ) by A17, A21, A22, A23;
case b1 <> mb1 ; :: thesis: (m1 . b1) * (m2 . b2) = 0. L
then m1 . b1 = 0. L by A5;
hence (m1 . b1) * (m2 . b2) = 0. L by BINOM:1; :: thesis: verum
end;
case b2 <> mb2 ; :: thesis: (m1 . b1) * (m2 . b2) = 0. L
then m2 . b2 = 0. L by A10;
hence (m1 . b1) * (m2 . b2) = 0. L by BINOM:2; :: thesis: verum
end;
end;
end;
hence s /. k = 0. L by A20; :: thesis: verum
end;
now
per cases ( dom s = {} or dom s <> {} ) ;
case dom s = {} ; :: thesis: (m1 *' m2) . b = 0. L
then s = <*> the carrier of L by RELAT_1:64;
hence (m1 *' m2) . b = 0. L by A14; :: thesis: verum
end;
case A24: dom s <> {} ; :: thesis: (m1 *' m2) . b = 0. L
consider k being Element of dom s;
A25: k in dom s by A24;
for k' being Element of NAT st k' in dom s & k' <> k holds
s /. k' = 0. L by A18;
then s /. k = (m1 *' m2) . b by A14, A25, POLYNOM2:5;
hence (m1 *' m2) . b = 0. L by A18, A25; :: thesis: verum
end;
end;
end;
hence contradiction by A13, POLYNOM1:def 9; :: thesis: verum
end;
now
let b' be bag of ; :: thesis: ( b' <> b implies (m1 *' m2) . b' = 0. L )
assume A26: b' <> b ; :: thesis: (m1 *' m2) . b' = 0. L
consider s being FinSequence of L such that
A27: ( (m1 *' m2) . 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 st
( (decomp b') /. k = <*b1,b2*> & s /. k = (m1 . b1) * (m2 . b2) ) ) ) by POLYNOM1:def 26;
A28: dom s = Seg (len (decomp b')) by A27, FINSEQ_1:def 3
.= dom (decomp b') by FINSEQ_1:def 3 ;
A29: now
let k be Element of NAT ; :: thesis: ( k in dom s implies s /. k = 0. L )
assume A30: k in dom s ; :: thesis: s /. k = 0. L
then consider b1, b2 being bag of such that
A31: ( (decomp b') /. k = <*b1,b2*> & s /. k = (m1 . b1) * (m2 . b2) ) by A27;
consider b1', b2' being bag of such that
A32: ( (decomp b') /. k = <*b1',b2'*> & b' = b1' + b2' ) by A28, A30, POLYNOM1:72;
A33: b1 = <*b1',b2'*> . 1 by A31, A32, FINSEQ_1:61
.= b1' by FINSEQ_1:61 ;
A34: b2 = <*b1',b2'*> . 2 by A31, A32, FINSEQ_1:61
.= b2' by FINSEQ_1:61 ;
now
per cases ( b1 <> mb1 or b2 <> mb2 ) by A16, A26, A32, A33, A34;
case b1 <> mb1 ; :: thesis: (m1 . b1) * (m2 . b2) = 0. L
then m1 . b1 = 0. L by A5;
hence (m1 . b1) * (m2 . b2) = 0. L by BINOM:1; :: thesis: verum
end;
case b2 <> mb2 ; :: thesis: (m1 . b1) * (m2 . b2) = 0. L
then m2 . b2 = 0. L by A10;
hence (m1 . b1) * (m2 . b2) = 0. L by BINOM:2; :: thesis: verum
end;
end;
end;
hence s /. k = 0. L by A31; :: thesis: verum
end;
now
per cases ( dom s = {} or dom s <> {} ) ;
case dom s = {} ; :: thesis: (m1 *' m2) . b' = 0. L
then s = <*> the carrier of L by RELAT_1:64;
hence (m1 *' m2) . b' = 0. L by A27; :: thesis: verum
end;
case A35: dom s <> {} ; :: thesis: (m1 *' m2) . b' = 0. L
consider k being Element of dom s;
A36: k in dom s by A35;
for k' being Element of NAT st k' in dom s & k' <> k holds
s /. k' = 0. L by A29;
then s /. k = (m1 *' m2) . b' by A27, A36, POLYNOM2:5;
hence (m1 *' m2) . b' = 0. L by A29, A36; :: thesis: verum
end;
end;
end;
hence (m1 *' m2) . b' = 0. L ; :: thesis: verum
end;
hence m1 *' m2 is monomial-like by POLYNOM7:def 4; :: thesis: verum
end;
end;
end;
hence m1 *' m2 is monomial-like ; :: thesis: verum
end;
end;