:: by Barbara Dzienis

::

:: Received August 10, 2001

:: Copyright (c) 2001-2021 Association of Mizar Users

notation
end;

definition

let L1, L2 be non empty doubleLoopStr ;

:: original: are_isomorphic

redefine pred L1 is_ringisomorph_to L2;

reflexivity

for L1 being non empty doubleLoopStr holds R86(b_{1},b_{1})

end;
:: original: are_isomorphic

redefine pred L1 is_ringisomorph_to L2;

reflexivity

for L1 being non empty doubleLoopStr holds R86(b

proof 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

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;

coherence

not o1 +^ o2 is empty by ORDINAL3:26;

coherence

not o2 +^ o1 is empty by ORDINAL3:26;

end;
let o2 be non empty Ordinal;

coherence

not o1 +^ o2 is empty by ORDINAL3:26;

coherence

not o2 +^ o1 is empty by ORDINAL3:26;

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 ) )

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;

ex b_{1} being Element of Bags (o1 +^ o2) st

for o being Ordinal holds

( ( o in o1 implies b_{1} . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies b_{1} . o = b . (o -^ o1) ) )

for b_{1}, b_{2} being Element of Bags (o1 +^ o2) st ( for o being Ordinal holds

( ( o in o1 implies b_{1} . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies b_{1} . o = b . (o -^ o1) ) ) ) & ( for o being Ordinal holds

( ( o in o1 implies b_{2} . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies b_{2} . o = b . (o -^ o1) ) ) ) holds

b_{1} = b_{2}

end;
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 for o being Ordinal holds

( ( o in o1 implies it . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies it . o = b . (o -^ o1) ) );

ex b

for o being Ordinal holds

( ( o in o1 implies b

proof end;

uniqueness for b

( ( o in o1 implies b

( ( o in o1 implies b

b

proof end;

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

for o1, o2 being Ordinal

for a being Element of Bags o1

for b being Element of Bags o2

for b_{5} being Element of Bags (o1 +^ o2) holds

( b_{5} = a +^ b iff for o being Ordinal holds

( ( o in o1 implies b_{5} . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies b_{5} . o = b . (o -^ o1) ) ) );

for o1, o2 being Ordinal

for a being Element of Bags o1

for b being Element of Bags o2

for b

( b

( ( o in o1 implies b

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

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

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 ) )

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

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 )

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 right_complementable Abelian add-associative right_zeroed associative distributive doubleLoopStr

for p, q, r being Series of n,L holds (p + q) *' r = (p *' r) + (q *' r)

for L being non empty right_complementable Abelian add-associative right_zeroed 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 non trivial right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;

coherence

( not Polynom-Ring (n,L) is trivial & Polynom-Ring (n,L) is distributive )

end;
let L be non empty non trivial right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;

coherence

( not Polynom-Ring (n,L) is trivial & Polynom-Ring (n,L) is distributive )

proof end;

definition

let o1, o2 be non empty Ordinal;

let L be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ;

let P be Polynomial of o1,(Polynom-Ring (o2,L));

ex b_{1} being Polynomial of (o1 +^ o2),L st

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 & b_{1} . b = Q1 . b2 )

for b_{1}, b_{2} being Polynomial of (o1 +^ o2),L st ( 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 & b_{1} . b = Q1 . b2 ) ) & ( 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 & b_{2} . b = Q1 . b2 ) ) holds

b_{1} = b_{2}

end;
let L be non trivial right_complementable add-associative right_zeroed well-unital distributive 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 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 );

ex b

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 & b

proof end;

uniqueness for b

( Q1 = P . b1 & b = b1 +^ b2 & b

( Q1 = P . b1 & b = b1 +^ b2 & b

b

proof end;

:: deftheorem Def2 defines Compress POLYNOM6:def 2 :

for o1, o2 being non empty Ordinal

for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr

for P being Polynomial of o1,(Polynom-Ring (o2,L))

for b_{5} being Polynomial of (o1 +^ o2),L holds

( b_{5} = Compress P iff 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 & b_{5} . b = Q1 . b2 ) );

for o1, o2 being non empty Ordinal

for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr

for P being Polynomial of o1,(Polynom-Ring (o2,L))

for b

( b

( Q1 = P . b1 & b = b1 +^ b2 & b

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

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 )

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 ) ) )

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 a19 being Element of Bags o1 ex Fk being FinSequence of Bags (o1 +^ o2) st

( Fk = G /. i & (divisors b1) /. i = a19 & len Fk = len (divisors b2) & ( for m being Nat st m in dom Fk holds

ex a199 being Element of Bags o2 st

( (divisors b2) /. m = a199 & Fk /. m = a19 +^ a199 ) ) ) ) holds

divisors (b1 +^ b2) = FlattenSeq G

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 a19 being Element of Bags o1 ex Fk being FinSequence of Bags (o1 +^ o2) st

( Fk = G /. i & (divisors b1) /. i = a19 & len Fk = len (divisors b2) & ( for m being Nat st m in dom Fk holds

ex a199 being Element of Bags o2 st

( (divisors b2) /. m = a199 & Fk /. m = a19 +^ a199 ) ) ) ) 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

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 a19, b19 being Element of Bags o1 ex Fk being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) st

( Fk = G /. i & (decomp b1) /. i = <*a19,b19*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds

ex a199, b199 being Element of Bags o2 st

( (decomp b2) /. m = <*a199,b199*> & Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> ) ) ) ) holds

decomp (b1 +^ b2) = FlattenSeq G

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 a19, b19 being Element of Bags o1 ex Fk being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) st

( Fk = G /. i & (decomp b1) /. i = <*a19,b19*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds

ex a199, b199 being Element of Bags o2 st

( (decomp b2) /. m = <*a199,b199*> & Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> ) ) ) ) holds

decomp (b1 +^ b2) = FlattenSeq G

proof end;

theorem :: POLYNOM6:15

for o1, o2 being non empty Ordinal

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

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

proof end;