POLYALGX: {O}n {B}ag of 1. {P}art {I}

for b1, b2 being bag of 1 holds
( ( b2 in rng (divisors b1) implies b2 . 0 <= b1 . 0 ) & ( b2 . 0 <= b1 . 0 implies b2 in rng (divisors b1) ) & ( b2 in rng (divisors b1) implies b2 divides b1 ) & ( b2 divides b1 implies b2 in rng (divisors b1) ) )

proof end;

theorem Th13: :: POLYALGX:13

for b being bag of 1 holds rng (divisors b) = { x where x is bag of 1 : x . 0 <= b . 0 }

proof end;

theorem Th14: :: POLYALGX:14

for b being bag of 1 holds rng (NBag1 | (Segm ((b . 0) + 1))) = { x where x is bag of 1 : x . 0 <= b . 0 }

proof end;

theorem Th15: :: POLYALGX:15

for b being bag of 1 holds len (divisors b) = (b . 0) + 1

proof end;

:: Construct mutlivariable Formal Series
:: same manner as POLYALG1:def 2

definition

let n be Ordinal;
let L be non degenerated comRing;

func Formal-Series (n,L) -> non empty strict AlgebraStr over L means :Def3: :: POLYALGX:def 3
( ( for x being set holds
( x in the carrier of it iff x is Series of n,L ) ) & ( for x, y being Element of it
for p, q being Series of n,L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of it
for p, q being Series of n,L st x = p & y = q holds
x * y = p *' q ) & ( for a being Element of L
for x being Element of it
for p being Series of n,L st x = p holds
a * x = a * p ) & 0. it = 0_ (n,L) & 1. it = 1_ (n,L) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines Formal-Series POLYALGX:def 3 :

registration

let n be Ordinal;
let L be non degenerated comRing;

cluster Formal-Series (n,L) -> non empty Abelian strict ;

coherence

proof end;

cluster Formal-Series (n,L) -> non empty add-associative strict ;

coherence

proof end;

cluster Formal-Series (n,L) -> non empty right_zeroed strict ;

coherence

proof end;

cluster Formal-Series (n,L) -> non empty right_complementable strict ;

coherence

proof end;

cluster Formal-Series (n,L) -> non empty commutative strict ;

coherence

proof end;

cluster Formal-Series (n,L) -> non empty associative strict ;

coherence

proof end;

end;

registration

cluster non empty right_complementable add-associative right_zeroed associative well-unital distributive left_zeroed for doubleLoopStr ;

existence

proof end;

end;

Lm2: now :: thesis:

let n be Ordinal; :: thesis:
let L be non degenerated comRing; :: thesis:
set F = Formal-Series (n,L);
let x, e be Element of (Formal-Series (n,L)); :: thesis:
reconsider a = x, b = e as Series of n,L by Def3;
assume A1: e = 1_ (n,L) ; :: thesis:
thus x * e = a *' b by Def3
.= x by A1, POLYNOM1:29 ; :: thesis:
thus e * x = b *' a by Def3
.= x by A1, POLYNOM1:30 ; :: thesis:

end;

registration

let n be Ordinal;
let L be non degenerated comRing;

cluster Formal-Series (n,L) -> non empty well-unital strict ;

coherence

proof end;

cluster Formal-Series (n,L) -> non empty right-distributive strict ;

coherence

proof end;

cluster Formal-Series (n,L) -> non empty left-distributive strict ;

coherence ;

end;

theorem Th16: :: POLYALGX:16

for n being Ordinal
for L being non degenerated comRing
for a being Element of L
for p, q being Series of n,L holds a * (p + q) = (a * p) + (a * q)

proof end;

theorem Th17: :: POLYALGX:17

for n being Ordinal
for L being non degenerated comRing
for a, b being Element of L
for p being Series of n,L holds (a + b) * p = (a * p) + (b * p)

proof end;

theorem Th18: :: POLYALGX:18

for n being Ordinal
for L being non degenerated comRing
for a, b being Element of L
for p being Series of n,L holds (a * b) * p = a * (b * p)

proof end;

theorem Th19: :: POLYALGX:19

for n being Ordinal
for L being non degenerated comRing
for p being Series of n,L holds (1. L) * p = p

proof end;

registration

let n be Ordinal;
let L be non degenerated comRing;

cluster Formal-Series (n,L) -> non empty vector-distributive scalar-distributive scalar-associative scalar-unital strict ;

coherence

proof end;

end;

theorem Th20: :: POLYALGX:20

for n being Ordinal
for L being non degenerated comRing holds Formal-Series (n,L) is mix-associative

proof end;

registration

let n be Ordinal;
let L be non degenerated comRing;

cluster Formal-Series (n,L) -> non empty strict mix-associative ;

coherence by Th20;

end;

theorem Th21: :: POLYALGX:21

for n being Ordinal
for R being non degenerated comRing holds Polynom-Ring (n,R) is Subring of Formal-Series (n,R)

proof end;

Lm3: for V being Ring
for V1 being Subring of V holds
( ( for v1, w1 being Element of V1
for v, w being Element of V st v1 = v & w1 = w holds
v1 + w1 = v + w ) & ( for v1, w1 being Element of V1
for v, w being Element of V st v1 = v & w1 = w holds
v1 * w1 = v * w ) & 1_ V1 = 1_ V & 0. V1 = 0. V )

proof end;

theorem :: POLYALGX:22

for R being non degenerated comRing holds (0_ (1,R)) * NBag1 = 0_. R

proof end;

theorem Th23: :: POLYALGX:23

for R being non degenerated comRing holds ((0_ (1,R)) +* ((EmptyBag 1),(1. R))) * NBag1 = (0_. R) +* (0,(1. R))

proof end;

theorem :: POLYALGX:24

for R being non degenerated comRing holds ((0_ (1,R)) +* ((1 --> 1),(1. R))) * NBag1 = (0_. R) +* (1,(1. R))

proof end;

theorem Th25: :: POLYALGX:25

for b being bag of 1 holds
( SgmX ((BagOrder 1),(rng (divisors b))) = XFS2FS (NBag1 | (Segm ((b . 0) + 1))) & divisors b = XFS2FS (NBag1 | (Segm ((b . 0) + 1))) )

proof end;

definition

let R be non degenerated comRing;

func BSFSeri R -> Function of (Formal-Series (1,R)),(Formal-Series R) means :Def4: :: POLYALGX:def 4
for x being object st x in the carrier of (Formal-Series (1,R)) holds
ex x1 being Series of 1,R st
( x1 = x & it . x = x1 * NBag1 );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines BSFSeri POLYALGX:def 4 :

Lm4: for R being non degenerated comRing holds
( BSFSeri R is one-to-one & BSFSeri R is onto )

proof end;

registration

let R be non degenerated comRing;

cluster BSFSeri R -> one-to-one onto ;

coherence by Lm4;

end;

theorem Th26: :: POLYALGX:26

for R being Ring
for f, g being Series of 1,R holds (f + g) * NBag1 = (f * NBag1) + (g * NBag1)

proof end;

theorem Th27: :: POLYALGX:27

for R being non degenerated comRing
for f, g being Element of (Formal-Series (1,R)) holds (BSFSeri R) . (f + g) = ((BSFSeri R) . f) + ((BSFSeri R) . g)

proof end;

theorem Th28: :: POLYALGX:28

for R being non degenerated comRing
for f, g being Series of 1,R holds (f *' g) * NBag1 = (f * NBag1) *' (g * NBag1)

proof end;

theorem Th29: :: POLYALGX:29

for R being non degenerated comRing
for f, g being Element of (Formal-Series (1,R)) holds (BSFSeri R) . (f * g) = ((BSFSeri R) . f) * ((BSFSeri R) . g)

proof end;

theorem Th30: :: POLYALGX:30

for R being non degenerated comRing holds (BSFSeri R) . (1. (Formal-Series (1,R))) = 1. (Formal-Series R)

proof end;

registration

let R be non degenerated comRing;

cluster BSFSeri R -> unity-preserving additive multiplicative ;

coherence by Th27, Th29, Th30;

end;

theorem :: POLYALGX:31

for R being non degenerated comRing holds
( BSFSeri R is RingIsomorphism & Formal-Series R is Formal-Series (1,R) -isomorphic )

proof end;

registration

let R be non degenerated comRing;

cluster Formal-Series R -> Formal-Series (1,R) -homomorphic Formal-Series (1,R) -monomorphic Formal-Series (1,R) -isomorphic ;

coherence

proof end;

end;

definition

let R be non degenerated comRing;

func SBFSeri R -> Function of (Formal-Series R),(Formal-Series (1,R)) means :Def5: :: POLYALGX:def 5
for x being object st x in the carrier of (Formal-Series R) holds
ex x1 being sequence of R st
( x1 = x & it . x = x1 * BagN1 );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines SBFSeri POLYALGX:def 5 :

theorem Th32: :: POLYALGX:32

for R being non degenerated comRing holds (BSFSeri R) " = SBFSeri R

proof end;

Lm5: for R being non degenerated comRing holds SBFSeri R is one-to-one

proof end;

Lm6: for R being non degenerated comRing holds SBFSeri R is onto

proof end;

registration

let R be non degenerated comRing;

cluster SBFSeri R -> one-to-one onto ;

coherence by Lm5, Lm6;

end;

theorem Th33: :: POLYALGX:33

for R being non degenerated comRing holds SBFSeri R is RingHomomorphism

proof end;

registration

let R be non degenerated comRing;

cluster SBFSeri R -> unity-preserving additive multiplicative ;

coherence

proof end;

end;

theorem :: POLYALGX:34

for R being non degenerated comRing holds
( SBFSeri R is RingIsomorphism & Formal-Series (1,R) is Formal-Series R -isomorphic )

proof end;

registration

let R be non degenerated comRing;

cluster Formal-Series (1,R) -> non empty strict Formal-Series R -homomorphic Formal-Series R -monomorphic Formal-Series R -isomorphic ;

coherence

proof end;

end;

theorem Th35: :: POLYALGX:35

for R being non degenerated comRing holds Polynom-Ring R is Subring of Formal-Series R

proof end;

theorem :: POLYALGX:36

for R being non degenerated comRing
for f1, g1 being sequence of R holds (f1 + g1) * BagN1 = (f1 * BagN1) + (g1 * BagN1)

proof end;

theorem Th37: :: POLYALGX:37

for R being non degenerated comRing
for f being sequence of the carrier of R holds f = (f * BagN1) * NBag1

proof end;

theorem Th38: :: POLYALGX:38

for R being non degenerated comRing
for f being Series of 1,R holds f = (f * NBag1) * BagN1

proof end;

theorem Th39: :: POLYALGX:39

for R being non degenerated comRing
for f being sequence of R holds NBag1 .: (Support f) = Support (f * BagN1)

proof end;

theorem Th40: :: POLYALGX:40

for B being Subset of NAT holds card B = card (NBag1 .: B)

proof end;

theorem Th41: :: POLYALGX:41

for R being non degenerated comRing
for f being sequence of R holds card (Support f) = card (Support (f * BagN1))

proof end;

theorem Th42: :: POLYALGX:42

for R being non degenerated comRing
for f being Series of 1,R holds BagN1 .: (Support f) = Support (f * NBag1)

proof end;

theorem Th43: :: POLYALGX:43

for B being Subset of (Bags 1) holds card B = card (BagN1 .: B)

proof end;

theorem Th44: :: POLYALGX:44

for R being non degenerated comRing
for f being Series of 1,R holds card (Support f) = card (Support (f * NBag1))

proof end;

Lm7: for R being non degenerated comRing holds the carrier of (Polynom-Ring (1,R)) c= the carrier of (Formal-Series (1,R))

proof end;

definition

let R be non degenerated comRing;

func BSPoly R -> Function of (Polynom-Ring (1,R)),(Polynom-Ring R) equals :: POLYALGX:def 6
(BSFSeri R) | ([#] (Polynom-Ring (1,R)));

coherence

proof end;

end;

:: deftheorem defines BSPoly POLYALGX:def 6 :

theorem Th45: :: POLYALGX:45

for R being non degenerated comRing holds
( BSPoly R is one-to-one & BSPoly R is onto )

proof end;

registration

let R be non degenerated comRing;

cluster BSPoly R -> one-to-one onto ;

coherence by Th45;

end;

theorem Th46: :: POLYALGX:46

for R being non degenerated comRing
for p, q being Element of (Polynom-Ring (1,R))
for f, g being Element of (Formal-Series (1,R)) st p = f & q = g holds
p + q = f + g

proof end;

theorem Th47: :: POLYALGX:47

for R being non degenerated comRing
for p, q being Element of (Polynom-Ring (1,R))
for f, g being Element of (Formal-Series (1,R)) st p = f & q = g holds
p * q = f * g

proof end;

theorem Th48: :: POLYALGX:48

for R being non degenerated comRing
for f, g being Element of (Polynom-Ring (1,R)) holds (BSPoly R) . (f + g) = ((BSPoly R) . f) + ((BSPoly R) . g)

proof end;

theorem Th49: :: POLYALGX:49

for R being non degenerated comRing
for f, g being Element of (Polynom-Ring (1,R)) holds (BSPoly R) . (f * g) = ((BSPoly R) . f) * ((BSPoly R) . g)

proof end;

theorem Th50: :: POLYALGX:50

for R being non degenerated comRing holds (BSPoly R) . (1. (Polynom-Ring (1,R))) = 1. (Polynom-Ring R)

proof end;

registration

let R be non degenerated comRing;

cluster BSPoly R -> unity-preserving additive multiplicative ;

coherence by Th48, Th49, Th50;

end;

theorem :: POLYALGX:51

for R being non degenerated comRing holds
( BSPoly R is RingIsomorphism & Polynom-Ring R is Polynom-Ring (1,R) -isomorphic )

proof end;

registration

let R be non degenerated comRing;

cluster Polynom-Ring R -> Polynom-Ring (1,R) -homomorphic Polynom-Ring (1,R) -monomorphic Polynom-Ring (1,R) -isomorphic ;

coherence

proof end;

end;