:: POLYNOM6 semantic presentation

notation

let L1, L2 be non empty doubleLoopStr ;
synonym L1,L2 are_isomorphic for L1 is_ringisomorph_to L2;

end;

definition

let L1, L2 be non empty doubleLoopStr ;
:: original: are_isomorphic
redefine pred L1 is_ringisomorph_to L2;
reflexivity

proof end;

end;

theorem Th1: :: POLYNOM6:1

for o1, o2 being Ordinal
for B being set st ( for x being set holds
( x in B iff ex o being Ordinal st
( x = o1 +^ o & o in o2 ) ) ) holds
o1 +^ o2 = o1 \/ B

proof end;

registration

let o1 be Ordinal;
let o2 be non empty Ordinal;
cluster o1 +^ o2 -> non empty ;
coherence by ORDINAL3:29;
cluster o2 +^ o1 -> non empty ;
coherence by ORDINAL3:29;

end;

theorem Th2: :: POLYNOM6:2

for n being Ordinal
for a, b being bag of n st a < b holds
ex o being Ordinal st
( o in n & a . o < b . o & ( for l being Ordinal st l in o holds
a . l = b . l ) )

proof end;

definition

let o1, o2 be Ordinal;
let a be Element of Bags o1;
let b be Element of Bags o2;
func a +^ b -> Element of Bags (o1 +^ o2) means :Def1: :: POLYNOM6:def 1
for o being Ordinal holds
( ( o in o1 implies it . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies it . o = b . (o -^ o1) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines +^ POLYNOM6:def 1 :

theorem Th3: :: POLYNOM6:3

for o1, o2 being Ordinal
for a being Element of Bags o1
for b being Element of Bags o2 st o2 = {} holds
a +^ b = a

proof end;

theorem :: POLYNOM6:4

for o1, o2 being Ordinal
for a being Element of Bags o1
for b being Element of Bags o2 st o1 = {} holds
a +^ b = b

proof end;

theorem Th5: :: POLYNOM6:5

for o1, o2 being Ordinal
for b1 being Element of Bags o1
for b2 being Element of Bags o2 holds
( b1 +^ b2 = EmptyBag (o1 +^ o2) iff ( b1 = EmptyBag o1 & b2 = EmptyBag o2 ) )

proof end;

theorem Th6: :: POLYNOM6:6

for o1, o2 being Ordinal
for c being Element of Bags (o1 +^ o2) ex c1 being Element of Bags o1 ex c2 being Element of Bags o2 st c = c1 +^ c2

proof end;

theorem Th7: :: POLYNOM6:7

for o1, o2 being Ordinal
for b1, c1 being Element of Bags o1
for b2, c2 being Element of Bags o2 st b1 +^ b2 = c1 +^ c2 holds
( b1 = c1 & b2 = c2 )

proof end;

theorem Th8: :: POLYNOM6:8

for n being Ordinal
for L being non empty Abelian add-associative right_zeroed right_complementable associative distributive doubleLoopStr
for p, q, r being Series of n,L holds (p + q) *' r = (p *' r) + (q *' r)

proof end;

registration

let n be Ordinal;
let L be non empty Abelian add-associative right_zeroed right_complementable unital associative distributive non trivial doubleLoopStr ;
cluster Polynom-Ring n,L -> distributive non trivial ;
coherence

proof end;

end;

definition

let o1, o2 be non empty Ordinal;
let L be non empty add-associative right_zeroed right_complementable unital distributive non trivial doubleLoopStr ;
let P be Polynomial of o1,(Polynom-Ring o2,L);
func Compress P -> Polynomial of (o1 +^ o2),L means :Def2: :: POLYNOM6:def 2
for b being Element of Bags (o1 +^ o2) ex b1 being Element of Bags o1 ex b2 being Element of Bags o2 ex Q1 being Polynomial of o2,L st
( Q1 = P . b1 & b = b1 +^ b2 & it . b = Q1 . b2 );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines Compress POLYNOM6:def 2 :

theorem Th9: :: POLYNOM6:9

for o1, o2 being Ordinal
for b1, c1 being Element of Bags o1
for b2, c2 being Element of Bags o2 st b1 divides c1 & b2 divides c2 holds
b1 +^ b2 divides c1 +^ c2

proof end;

theorem Th10: :: POLYNOM6:10

for o1, o2 being Ordinal
for b being bag of o1 +^ o2
for b1 being Element of Bags o1
for b2 being Element of Bags o2 st b divides b1 +^ b2 holds
ex c1 being Element of Bags o1 ex c2 being Element of Bags o2 st
( c1 divides b1 & c2 divides b2 & b = c1 +^ c2 )

proof end;

theorem Th11: :: POLYNOM6:11

for o1, o2 being Ordinal
for a1, b1 being Element of Bags o1
for a2, b2 being Element of Bags o2 holds
( a1 +^ a2 < b1 +^ b2 iff ( a1 < b1 or ( a1 = b1 & a2 < b2 ) ) )

proof end;

theorem Th12: :: POLYNOM6:12

for o1, o2 being Ordinal
for b1 being Element of Bags o1
for b2 being Element of Bags o2
for G being FinSequence of (Bags (o1 +^ o2)) * st dom G = dom (divisors b1) & ( for i being Nat st i in dom (divisors b1) holds
ex a1' being Element of Bags o1 ex Fk being FinSequence of Bags (o1 +^ o2) st
( Fk = G /. i & (divisors b1) /. i = a1' & len Fk = len (divisors b2) & ( for m being Nat st m in dom Fk holds
ex a1'' being Element of Bags o2 st
( (divisors b2) /. m = a1'' & Fk /. m = a1' +^ a1'' ) ) ) ) holds
divisors (b1 +^ b2) = FlattenSeq G

proof end;

theorem Th13: :: POLYNOM6:13

for o1, o2 being Ordinal
for a1, b1, c1 being Element of Bags o1
for a2, b2, c2 being Element of Bags o2 st c1 = b1 -' a1 & c2 = b2 -' a2 holds
(b1 +^ b2) -' (a1 +^ a2) = c1 +^ c2

proof end;

theorem Th14: :: POLYNOM6:14

for o1, o2 being Ordinal
for b1 being Element of Bags o1
for b2 being Element of Bags o2
for G being FinSequence of (2 -tuples_on (Bags (o1 +^ o2))) * st dom G = dom (decomp b1) & ( for i being Nat st i in dom (decomp b1) holds
ex a1', b1' being Element of Bags o1 ex Fk being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) st
( Fk = G /. i & (decomp b1) /. i = <*a1',b1'*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a1'', b1'' being Element of Bags o2 st
( (decomp b2) /. m = <*a1'',b1''*> & Fk /. m = <*(a1' +^ a1''),(b1' +^ b1'')*> ) ) ) ) holds
decomp (b1 +^ b2) = FlattenSeq G

proof end;

theorem :: POLYNOM6:15

for o1, o2 being non empty Ordinal
for L being non empty Abelian add-associative right_zeroed right_complementable unital associative distributive non trivial doubleLoopStr holds Polynom-Ring o1,(Polynom-Ring o2,L), Polynom-Ring (o1 +^ o2),L are_isomorphic

proof end;