:: POLYNOM6 semantic presentation

notation
let c1, c2 be non empty doubleLoopStr ;
synonym c1,c2 are_isomorphic for c1 is_ringisomorph_to c2;
end;

definition
let c1, c2 be non empty doubleLoopStr ;
redefine pred are_isomorphic as c1 is_ringisomorph_to c2;
reflexivity
for b1 being non empty doubleLoopStr holds b1,b1 are_isomorphic
proof end;
end;

theorem Th1: :: POLYNOM6:1
for b1, b2 being Ordinal
for b3 being set st ( for b4 being set holds
( b4 in b3 iff ex b5 being Ordinal st
( b4 = b1 +^ b5 & b5 in b2 ) ) ) holds
b1 +^ b2 = b1 \/ b3
proof end;

registration
let c1 be Ordinal;
let c2 be non empty Ordinal;
cluster a1 +^ a2 -> non empty ;
coherence
not c1 +^ c2 is empty by ORDINAL3:29;
cluster a2 +^ a1 -> non empty ;
coherence
not c2 +^ c1 is empty by ORDINAL3:29;
end;

theorem Th2: :: POLYNOM6:2
for b1 being Ordinal
for b2, b3 being bag of b1 st b2 < b3 holds
ex b4 being Ordinal st
( b4 in b1 & b2 . b4 < b3 . b4 & ( for b5 being Ordinal st b5 in b4 holds
b2 . b5 = b3 . b5 ) )
proof end;

definition
let c1, c2 be Ordinal;
let c3 be Element of Bags c1;
let c4 be Element of Bags c2;
func c3 +^ c4 -> Element of Bags (a1 +^ a2) means :Def1: :: POLYNOM6:def 1
for b1 being Ordinal holds
( ( b1 in a1 implies a5 . b1 = a3 . b1 ) & ( b1 in (a1 +^ a2) \ a1 implies a5 . b1 = a4 . (b1 -^ a1) ) );
existence
ex b1 being Element of Bags (c1 +^ c2) st
for b2 being Ordinal holds
( ( b2 in c1 implies b1 . b2 = c3 . b2 ) & ( b2 in (c1 +^ c2) \ c1 implies b1 . b2 = c4 . (b2 -^ c1) ) )
proof end;
uniqueness
for b1, b2 being Element of Bags (c1 +^ c2) st ( for b3 being Ordinal holds
( ( b3 in c1 implies b1 . b3 = c3 . b3 ) & ( b3 in (c1 +^ c2) \ c1 implies b1 . b3 = c4 . (b3 -^ c1) ) ) ) & ( for b3 being Ordinal holds
( ( b3 in c1 implies b2 . b3 = c3 . b3 ) & ( b3 in (c1 +^ c2) \ c1 implies b2 . b3 = c4 . (b3 -^ c1) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines +^ POLYNOM6:def 1 :
for b1, b2 being Ordinal
for b3 being Element of Bags b1
for b4 being Element of Bags b2
for b5 being Element of Bags (b1 +^ b2) holds
( b5 = b3 +^ b4 iff for b6 being Ordinal holds
( ( b6 in b1 implies b5 . b6 = b3 . b6 ) & ( b6 in (b1 +^ b2) \ b1 implies b5 . b6 = b4 . (b6 -^ b1) ) ) );

theorem Th3: :: POLYNOM6:3
for b1, b2 being Ordinal
for b3 being Element of Bags b1
for b4 being Element of Bags b2 st b2 = {} holds
b3 +^ b4 = b3
proof end;

theorem Th4: :: POLYNOM6:4
for b1, b2 being Ordinal
for b3 being Element of Bags b1
for b4 being Element of Bags b2 st b1 = {} holds
b3 +^ b4 = b4
proof end;

theorem Th5: :: POLYNOM6:5
for b1, b2 being Ordinal
for b3 being Element of Bags b1
for b4 being Element of Bags b2 holds
( b3 +^ b4 = EmptyBag (b1 +^ b2) iff ( b3 = EmptyBag b1 & b4 = EmptyBag b2 ) )
proof end;

theorem Th6: :: POLYNOM6:6
for b1, b2 being Ordinal
for b3 being Element of Bags (b1 +^ b2) ex b4 being Element of Bags b1ex b5 being Element of Bags b2 st b3 = b4 +^ b5
proof end;

theorem Th7: :: POLYNOM6:7
for b1, b2 being Ordinal
for b3, b4 being Element of Bags b1
for b5, b6 being Element of Bags b2 st b3 +^ b5 = b4 +^ b6 holds
( b3 = b4 & b5 = b6 )
proof end;

theorem Th8: :: POLYNOM6:8
for b1 being Ordinal
for b2 being non empty Abelian add-associative right_zeroed right_complementable associative distributive doubleLoopStr
for b3, b4, b5 being Series of b1,b2 holds (b3 + b4) *' b5 = (b3 *' b5) + (b4 *' b5)
proof end;

registration
let c1 be Ordinal;
let c2 be non empty Abelian add-associative right_zeroed right_complementable unital associative distributive non trivial doubleLoopStr ;
cluster Polynom-Ring a1,a2 -> distributive non trivial ;
coherence
( not Polynom-Ring c1,c2 is trivial & Polynom-Ring c1,c2 is distributive )
proof end;
end;

definition
let c1, c2 be non empty Ordinal;
let c3 be non empty add-associative right_zeroed right_complementable unital distributive non trivial doubleLoopStr ;
let c4 be Polynomial of c1,(Polynom-Ring c2,c3);
func Compress c4 -> Polynomial of (a1 +^ a2),a3 means :Def2: :: POLYNOM6:def 2
for b1 being Element of Bags (a1 +^ a2) ex b2 being Element of Bags a1ex b3 being Element of Bags a2ex b4 being Polynomial of a2,a3 st
( b4 = a4 . b2 & b1 = b2 +^ b3 & a5 . b1 = b4 . b3 );
existence
ex b1 being Polynomial of (c1 +^ c2),c3 st
for b2 being Element of Bags (c1 +^ c2) ex b3 being Element of Bags c1ex b4 being Element of Bags c2ex b5 being Polynomial of c2,c3 st
( b5 = c4 . b3 & b2 = b3 +^ b4 & b1 . b2 = b5 . b4 )
proof end;
uniqueness
for b1, b2 being Polynomial of (c1 +^ c2),c3 st ( for b3 being Element of Bags (c1 +^ c2) ex b4 being Element of Bags c1ex b5 being Element of Bags c2ex b6 being Polynomial of c2,c3 st
( b6 = c4 . b4 & b3 = b4 +^ b5 & b1 . b3 = b6 . b5 ) ) & ( for b3 being Element of Bags (c1 +^ c2) ex b4 being Element of Bags c1ex b5 being Element of Bags c2ex b6 being Polynomial of c2,c3 st
( b6 = c4 . b4 & b3 = b4 +^ b5 & b2 . b3 = b6 . b5 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines Compress POLYNOM6:def 2 :
for b1, b2 being non empty Ordinal
for b3 being non empty add-associative right_zeroed right_complementable unital distributive non trivial doubleLoopStr
for b4 being Polynomial of b1,(Polynom-Ring b2,b3)
for b5 being Polynomial of (b1 +^ b2),b3 holds
( b5 = Compress b4 iff for b6 being Element of Bags (b1 +^ b2) ex b7 being Element of Bags b1ex b8 being Element of Bags b2ex b9 being Polynomial of b2,b3 st
( b9 = b4 . b7 & b6 = b7 +^ b8 & b5 . b6 = b9 . b8 ) );

theorem Th9: :: POLYNOM6:9
for b1, b2 being Ordinal
for b3, b4 being Element of Bags b1
for b5, b6 being Element of Bags b2 st b3 divides b4 & b5 divides b6 holds
b3 +^ b5 divides b4 +^ b6
proof end;

theorem Th10: :: POLYNOM6:10
for b1, b2 being Ordinal
for b3 being bag of b1 +^ b2
for b4 being Element of Bags b1
for b5 being Element of Bags b2 st b3 divides b4 +^ b5 holds
ex b6 being Element of Bags b1ex b7 being Element of Bags b2 st
( b6 divides b4 & b7 divides b5 & b3 = b6 +^ b7 )
proof end;

theorem Th11: :: POLYNOM6:11
for b1, b2 being Ordinal
for b3, b4 being Element of Bags b1
for b5, b6 being Element of Bags b2 holds
( b3 +^ b5 < b4 +^ b6 iff ( b3 < b4 or ( b3 = b4 & b5 < b6 ) ) )
proof end;

theorem Th12: :: POLYNOM6:12
for b1, b2 being Ordinal
for b3 being Element of Bags b1
for b4 being Element of Bags b2
for b5 being FinSequence of (Bags (b1 +^ b2)) * st dom b5 = dom (divisors b3) & ( for b6 being Nat st b6 in dom (divisors b3) holds
ex b7 being Element of Bags b1ex b8 being FinSequence of Bags (b1 +^ b2) st
( b8 = b5 /. b6 & (divisors b3) /. b6 = b7 & len b8 = len (divisors b4) & ( for b9 being Nat st b9 in dom b8 holds
ex b10 being Element of Bags b2 st
( (divisors b4) /. b9 = b10 & b8 /. b9 = b7 +^ b10 ) ) ) ) holds
divisors (b3 +^ b4) = FlattenSeq b5
proof end;

theorem Th13: :: POLYNOM6:13
for b1, b2 being Ordinal
for b3, b4, b5 being Element of Bags b1
for b6, b7, b8 being Element of Bags b2 st b5 = b4 -' b3 & b8 = b7 -' b6 holds
(b4 +^ b7) -' (b3 +^ b6) = b5 +^ b8
proof end;

theorem Th14: :: POLYNOM6:14
for b1, b2 being Ordinal
for b3 being Element of Bags b1
for b4 being Element of Bags b2
for b5 being FinSequence of (2 -tuples_on (Bags (b1 +^ b2))) * st dom b5 = dom (decomp b3) & ( for b6 being Nat st b6 in dom (decomp b3) holds
ex b7, b8 being Element of Bags b1ex b9 being FinSequence of 2 -tuples_on (Bags (b1 +^ b2)) st
( b9 = b5 /. b6 & (decomp b3) /. b6 = <*b7,b8*> & len b9 = len (decomp b4) & ( for b10 being Nat st b10 in dom b9 holds
ex b11, b12 being Element of Bags b2 st
( (decomp b4) /. b10 = <*b11,b12*> & b9 /. b10 = <*(b7 +^ b11),(b8 +^ b12)*> ) ) ) ) holds
decomp (b3 +^ b4) = FlattenSeq b5
proof end;

theorem Th15: :: POLYNOM6:15
for b1, b2 being non empty Ordinal
for b3 being non empty Abelian add-associative right_zeroed right_complementable unital associative distributive non trivial doubleLoopStr holds Polynom-Ring b1,(Polynom-Ring b2,b3), Polynom-Ring (b1 +^ b2),b3 are_isomorphic
proof end;