set PNR = Polynom-Ring n,R;
set CPNR = the carrier of (Polynom-Ring n,R);
set CR = the carrier of R;
set P = upm n,R;
thus
upm n,R is multiplicative
:: thesis: verumproof
let x',
y' be
Element of the
carrier of
(Polynom-Ring (Polynom-Ring n,R));
:: according to GROUP_6:def 7 :: thesis: (upm n,R) . (x' * y') = ((upm n,R) . x') * ((upm n,R) . y')
reconsider x =
x',
y =
y',
xy =
x' * y' as
Polynomial of
(Polynom-Ring n,R) by POLYNOM3:def 12;
reconsider Pxy =
(upm n,R) . (x' * y'),
PxPy =
((upm n,R) . x') * ((upm n,R) . y'),
Px =
(upm n,R) . x',
Py =
(upm n,R) . y' as
Polynomial of
(n + 1),
R by POLYNOM1:def 27;
A4:
PxPy = Px *' Py
by POLYNOM1:def 27;
A5:
xy = x *' y
by POLYNOM3:def 12;
now let b' be
set ;
:: thesis: ( b' in Bags (n + 1) implies Pxy . b' = PxPy . b' )assume
b' in Bags (n + 1)
;
:: thesis: Pxy . b' = PxPy . b'then reconsider b =
b' as
Element of
Bags (n + 1) ;
consider r being
FinSequence of the
carrier of
(Polynom-Ring n,R) such that A6:
(
len r = (b . n) + 1 &
xy . (b . n) = Sum r & ( for
k being
Element of
NAT st
k in dom r holds
r . k = (x . (k -' 1)) * (y . (((b . n) + 1) -' k)) ) )
by A5, POLYNOM3:def 11;
n < n + 1
by NAT_1:13;
then reconsider bn =
b | n as
Element of
Bags n by Th3;
reconsider xybn =
xy . (b . n) as
Polynomial of
n,
R by POLYNOM1:def 27;
consider g being
Function of the
carrier of
(Polynom-Ring n,R),the
carrier of
R such that A7:
( ( for
p being
Polynomial of
n,
R holds
g . p = p . bn ) &
xybn . bn = Sum (g * r) )
by A6, Th29;
A8:
Sum (g * r) = Pxy . b
by A7, Def6;
defpred S1[
set ,
set ]
means for
p,
q being
Polynomial of
n,
R for
fcr being
FinSequence of the
carrier of
R for
i being
Element of
NAT st
i = R &
p = x . (i -' 1) &
q = y . (((b . n) + 1) -' i) &
fcr = n holds
(
(p *' q) . bn = Sum fcr &
len fcr = len (decomp bn) & ( for
k being
Element of
NAT st
k in dom fcr holds
ex
b1,
b2 being
bag of st
(
(decomp bn) /. k = <*b1,b2*> &
fcr /. k = (p . b1) * (q . b2) ) ) );
consider s being
Function of
(dom r),
(the carrier of R * ) such that A12:
for
e being
set st
e in dom r holds
S1[
e,
s . e]
from FUNCT_2:sch 1(A9);
A13:
dom s = dom r
by FUNCT_2:def 1;
then
ex
n being
Nat st
dom s = Seg n
by FINSEQ_1:def 2;
then A14:
s is
FinSequence-like
by FINSEQ_1:def 2;
rng s c= the
carrier of
R *
;
then reconsider s =
s as
FinSequence of the
carrier of
R * by A14, FINSEQ_1:def 4;
len (Sum s) = len s
by MATRLIN:def 8;
then A15:
dom (Sum s) = dom r
by A13, FINSEQ_3:31;
A16:
dom r = dom (g * r)
by ALG_1:1;
now let k be
Nat;
:: thesis: ( k in dom r implies (Sum s) . k = (g * r) . k )assume A17:
k in dom r
;
:: thesis: (Sum s) . k = (g * r) . kthen A18:
(Sum s) /. k = (Sum s) . k
by A15, PARTFUN1:def 8;
A19:
s /. k = s . k
by A13, A17, PARTFUN1:def 8;
reconsider sk =
s . k as
Element of the
carrier of
R * by A17, FUNCT_2:7;
reconsider sk =
sk as
FinSequence of the
carrier of
R ;
reconsider p =
x . (k -' 1),
q =
y . (((b . n) + 1) -' k) as
Polynomial of
n,
R by POLYNOM1:def 27;
reconsider pq' =
p *' q as
Element of the
carrier of
(Polynom-Ring n,R) by POLYNOM1:def 27;
A20:
r . k =
(x . (k -' 1)) * (y . (((b . n) + 1) -' k))
by A6, A17
.=
pq'
by POLYNOM1:def 27
;
thus (Sum s) . k =
Sum sk
by A15, A17, A18, A19, MATRLIN:def 8
.=
(p *' q) . bn
by A12, A17
.=
g . (r . k)
by A7, A20
.=
(g * r) . k
by A17, FUNCT_1:23
;
:: thesis: verum end; then A21:
Sum s = g * r
by A15, A16, FINSEQ_1:17;
set t =
FlattenSeq s;
A22:
Sum (FlattenSeq s) = Pxy . b
by A8, A21, POLYNOM1:34;
consider u being
FinSequence of the
carrier of
R such that A23:
(
PxPy . b = Sum u &
len u = len (decomp b) & ( for
k being
Element of
NAT st
k in dom u holds
ex
b1,
b2 being
bag of st
(
(decomp b) /. k = <*b1,b2*> &
u /. k = (Px . b1) * (Py . b2) ) ) )
by A4, POLYNOM1:def 26;
defpred S2[
set ,
set ]
means for
i,
n1 being
Element of
NAT for
b1 being
bag of st
n1 = R &
b1 = (divisors b) . n1 &
i in dom (divisors bn) &
(divisors bn) . i = b1 | n holds
(
(b1 . n) + 1
in dom s &
i in dom (s . ((b1 . n) + 1)) &
n = (Sum (Card (s | (((b1 . n) + 1) -' 1)))) + i );
A24:
now let n1' be
set ;
:: thesis: ( n1' in dom u implies ex n2' being set st
( n2' in dom (FlattenSeq s) & S2[n1',n2'] ) )assume A25:
n1' in dom u
;
:: thesis: ex n2' being set st
( n2' in dom (FlattenSeq s) & S2[n1',n2'] )then reconsider n1 =
n1' as
Element of
NAT ;
dom u =
dom (decomp b)
by A23, FINSEQ_3:31
.=
dom (divisors b)
by POLYNOM1:def 19
;
then A26:
(divisors b) . n1 in rng (divisors b)
by A25, FUNCT_1:def 5;
then reconsider b1 =
(divisors b) . n1 as
bag of
by POLYNOM1:def 14;
n < n + 1
by NAT_1:13;
then reconsider b1n =
b1 | n as
Element of
Bags n by Th3;
A27:
b1 divides b
by A26, Th7;
then
b1n divides bn
by Th4;
then
b1n in rng (divisors bn)
by Th7;
then consider i being
set such that A28:
(
i in dom (divisors bn) &
b1n = (divisors bn) . i )
by FUNCT_1:def 5;
reconsider i =
i as
Element of
NAT by A28;
set n2 =
(Sum (Card (s | (((b1 . n) + 1) -' 1)))) + i;
b1 . n <= b . n
by A27, POLYNOM1:def 13;
then A29:
(b1 . n) + 1
<= (b . n) + 1
by XREAL_1:8;
A30:
(b1 . n) + 1
>= 1
+ 0
by XREAL_1:8;
then A31:
(b1 . n) + 1
in dom s
by A6, A13, A29, FINSEQ_3:27;
reconsider p =
x . (((b1 . n) + 1) -' 1),
q =
y . (((b . n) + 1) -' ((b1 . n) + 1)) as
Polynomial of
n,
R by POLYNOM1:def 27;
s . ((b1 . n) + 1) is
Element of the
carrier of
R *
by A13, A31, FUNCT_2:7;
then
(
p = x . (((b1 . n) + 1) -' 1) &
q = y . (((b . n) + 1) -' ((b1 . n) + 1)) &
s . ((b1 . n) + 1) is
FinSequence of the
carrier of
R )
;
then
len (s . ((b1 . n) + 1)) = len (decomp bn)
by A12, A13, A31;
then A32:
dom (s . ((b1 . n) + 1)) =
dom (decomp bn)
by FINSEQ_3:31
.=
dom (divisors bn)
by POLYNOM1:def 19
;
then A33:
(Sum (Card (s | (((b1 . n) + 1) -' 1)))) + i in dom (FlattenSeq s)
by A28, A31, POLYNOM1:33;
for
i',
n1' being
Element of
NAT for
b1' being
bag of st
n1' = n1 &
b1' = (divisors b) . n1' &
i' in dom (divisors bn) &
(divisors bn) . i' = b1' | n holds
(
(b1' . n) + 1
in dom s &
i' in dom (s . ((b1' . n) + 1)) &
(Sum (Card (s | (((b1 . n) + 1) -' 1)))) + i = (Sum (Card (s | (((b1' . n) + 1) -' 1)))) + i' )
by A6, A13, A28, A29, A30, A32, FINSEQ_3:27, FUNCT_1:def 8;
hence
ex
n2' being
set st
(
n2' in dom (FlattenSeq s) &
S2[
n1',
n2'] )
by A33;
:: thesis: verum end; consider p being
Function of
(dom u),
(dom (FlattenSeq s)) such that A34:
for
x being
set st
x in dom u holds
S2[
x,
p . x]
from FUNCT_2:sch 1(A24);
A35:
now let n1 be
Element of
NAT ;
:: thesis: ( n1 in dom u implies u . n1 = (FlattenSeq s) . (p . n1) )assume A36:
n1 in dom u
;
:: thesis: u . n1 = (FlattenSeq s) . (p . n1)then consider b1,
b2 being
bag of
such that A37:
(
(decomp b) /. n1 = <*b1,b2*> &
u /. n1 = (Px . b1) * (Py . b2) )
by A23;
reconsider xb1n =
x . (b1 . n),
yb2n =
y . (b2 . n) as
Polynomial of
n,
R by POLYNOM1:def 27;
n < n + 1
by NAT_1:13;
then reconsider b1n =
b1 | n,
b2n =
b2 | n as
Element of
Bags n by Th3;
A38:
u . n1 =
(Px . b1) * (Py . b2)
by A36, A37, PARTFUN1:def 8
.=
(xb1n . b1n) * (Py . b2)
by Def6
.=
(xb1n . b1n) * (yb2n . b2n)
by Def6
;
(divisors b) /. n1 is
Element of
Bags (n + 1)
;
then reconsider b1' =
(divisors b) /. n1 as
bag of ;
A39:
dom u = dom (decomp b)
by A23, FINSEQ_3:31;
then
<*b1,b2*> = <*b1',(b -' b1')*>
by A36, A37, POLYNOM1:def 19;
then A40:
(
b1 = b1' &
b2 = b -' b1' )
by GROUP_7:2;
A41:
n1 in dom (divisors b)
by A36, A39, POLYNOM1:def 19;
then A42:
b1 = (divisors b) . n1
by A40, PARTFUN1:def 8;
then
b1 in rng (divisors b)
by A41, FUNCT_1:def 5;
then A43:
b1 divides b
by Th7;
then
b1n divides bn
by Th4;
then
b1n in rng (divisors bn)
by Th7;
then consider i being
set such that A44:
(
i in dom (divisors bn) &
b1n = (divisors bn) . i )
by FUNCT_1:def 5;
reconsider i =
i as
Element of
NAT by A44;
A45:
(
(b1 . n) + 1
in dom s &
i in dom (s . ((b1 . n) + 1)) &
p . n1 = (Sum (Card (s | (((b1 . n) + 1) -' 1)))) + i )
by A34, A36, A42, A44;
then A46:
(FlattenSeq s) . (p . n1) = (s . ((b1 . n) + 1)) . i
by POLYNOM1:33;
A47:
((b1 . n) + 1) -' 1 =
((b1 . n) + 1) - 1
by NAT_D:37
.=
b1 . n
;
A48:
b1 . n <= b . n
by A43, POLYNOM1:def 13;
then
(b1 . n) + 1
<= (b . n) + 1
by XREAL_1:8;
then A49:
((b . n) + 1) -' ((b1 . n) + 1) =
((b . n) + 1) - ((b1 . n) + 1)
by XREAL_1:235
.=
(((b . n) - (b1 . n)) + 1) - 1
.=
(b . n) -' (b1 . n)
by A48, XREAL_1:235
.=
b2 . n
by A40, POLYNOM1:def 6
;
s . ((b1 . n) + 1) is
Element of the
carrier of
R *
by A13, A45, FUNCT_2:7;
then reconsider sb1n1 =
s . ((b1 . n) + 1) as
FinSequence of the
carrier of
R ;
(
xb1n = x . (((b1 . n) + 1) -' 1) &
yb2n = y . (((b . n) + 1) -' ((b1 . n) + 1)) &
s . ((b1 . n) + 1) = sb1n1 )
by A47, A49;
then A50:
(
(xb1n *' yb2n) . bn = Sum sb1n1 &
len sb1n1 = len (decomp bn) & ( for
k being
Element of
NAT st
k in dom sb1n1 holds
ex
b1,
b2 being
bag of st
(
(decomp bn) /. k = <*b1,b2*> &
sb1n1 /. k = (xb1n . b1) * (yb2n . b2) ) ) )
by A12, A13, A45;
consider B1,
B2 being
bag of
such that A51:
(
(decomp bn) /. i = <*B1,B2*> &
sb1n1 /. i = (xb1n . B1) * (yb2n . B2) )
by A12, A13, A45, A47, A49;
(divisors bn) /. i is
Element of
Bags n
;
then reconsider B1' =
(divisors bn) /. i as
bag of ;
A52:
dom (divisors bn) = dom (decomp bn)
by POLYNOM1:def 19;
then
<*B1,B2*> = <*B1',(bn -' B1')*>
by A44, A51, POLYNOM1:def 19;
then A53:
(
B1 = B1' &
B2 = bn -' B1' )
by GROUP_7:2;
then A54:
B1 = b1n
by A44, PARTFUN1:def 8;
then A55:
B2 = b2n
by A40, A53, Th5;
dom sb1n1 = dom (divisors bn)
by A50, A52, FINSEQ_3:31;
hence
u . n1 = (FlattenSeq s) . (p . n1)
by A38, A44, A46, A51, A54, A55, PARTFUN1:def 8;
:: thesis: verum end; A56:
dom (decomp b) <> {}
;
( 1
<= 1 &
0 + 1
<= len r )
by A6, XREAL_1:8;
then A57:
1
in dom s
by A13, FINSEQ_3:27;
then
1
in dom (Card s)
by CARD_3:def 2;
then
Sum (Card s) >= (Card s) . 1
by POLYNOM3:4;
then A58:
Sum (Card s) >= len (s . 1)
by A57, CARD_3:def 2;
then
Sum (Card s) > 0
by A58;
then
len (FlattenSeq s) > 0
by POLYNOM1:30;
then
FlattenSeq s <> {}
;
then A60:
(
dom u <> {} &
dom (FlattenSeq s) <> {} )
by A23, A56, FINSEQ_3:31;
now let n1',
n2' be
set ;
:: thesis: ( n1' in dom p & n2' in dom p & p . n1' = p . n2' implies n1' = n2' )assume A61:
(
n1' in dom p &
n2' in dom p &
p . n1' = p . n2' )
;
:: thesis: n1' = n2'
dom p = dom u
by A60, FUNCT_2:def 1;
then reconsider n1 =
n1',
n2 =
n2' as
Element of
NAT by A61;
A62:
dom u =
dom (decomp b)
by A23, FINSEQ_3:31
.=
dom (divisors b)
by POLYNOM1:def 19
;
then A63:
(divisors b) . n1 in rng (divisors b)
by A61, FUNCT_1:def 5;
then reconsider b1 =
(divisors b) . n1 as
bag of
by POLYNOM1:def 14;
A64:
(divisors b) . n2 in rng (divisors b)
by A61, A62, FUNCT_1:def 5;
then reconsider b2 =
(divisors b) . n2 as
bag of
by POLYNOM1:def 14;
n < n + 1
by NAT_1:13;
then reconsider b1n =
b1 | n,
b2n =
b2 | n as
Element of
Bags n by Th3;
b1 divides b
by A63, Th7;
then
b1n divides bn
by Th4;
then
b1n in rng (divisors bn)
by Th7;
then consider i1 being
set such that A65:
(
i1 in dom (divisors bn) &
b1n = (divisors bn) . i1 )
by FUNCT_1:def 5;
reconsider i1 =
i1 as
Element of
NAT by A65;
b2 divides b
by A64, Th7;
then
b2n divides bn
by Th4;
then
b2n in rng (divisors bn)
by Th7;
then consider i2 being
set such that A66:
(
i2 in dom (divisors bn) &
b2n = (divisors bn) . i2 )
by FUNCT_1:def 5;
reconsider i2 =
i2 as
Element of
NAT by A66;
A67:
(
(b1 . n) + 1
in dom s &
i1 in dom (s . ((b1 . n) + 1)) &
p . n1 = (Sum (Card (s | (((b1 . n) + 1) -' 1)))) + i1 )
by A34, A61, A65;
A68:
(
(b2 . n) + 1
in dom s &
i2 in dom (s . ((b2 . n) + 1)) &
p . n2 = (Sum (Card (s | (((b2 . n) + 1) -' 1)))) + i2 )
by A34, A61, A66;
(
(Card s) | (((b1 . n) + 1) -' 1) = Card (s | (((b1 . n) + 1) -' 1)) &
(Card s) | (((b2 . n) + 1) -' 1) = Card (s | (((b2 . n) + 1) -' 1)) )
by POLYNOM3:16;
then A69:
(
(b1 . n) + 1
= (b2 . n) + 1 &
i1 = i2 )
by A61, A67, A68, POLYNOM3:22;
A70:
(
b1 is
Element of
Bags (n + 1) &
b2 is
Element of
Bags (n + 1) )
by POLYNOM1:def 14;
then b1 =
b1n bag_extend (b1 . n)
by Def1
.=
b2
by A65, A66, A69, A70, Def1
;
hence
n1' = n2'
by A61, A62, FUNCT_1:def 8;
:: thesis: verum end; then A71:
p is
one-to-one
by FUNCT_1:def 8;
dom (FlattenSeq s) c= rng p
proof
let n1' be
set ;
:: according to TARSKI:def 3 :: thesis: ( not n1' in dom (FlattenSeq s) or n1' in rng p )
assume A72:
n1' in dom (FlattenSeq s)
;
:: thesis: n1' in rng p
then reconsider n1 =
n1' as
Element of
NAT ;
consider i,
j being
Element of
NAT such that A73:
(
i in dom s &
j in dom (s . i) &
n1 = (Sum (Card (s | (i -' 1)))) + j &
(s . i) . j = (FlattenSeq s) . n1 )
by A72, POLYNOM1:32;
reconsider p' =
x . (i -' 1),
q' =
y . (((b . n) + 1) -' i) as
Polynomial of
n,
R by POLYNOM1:def 27;
reconsider bj =
(divisors bn) /. j as
bag of
by POLYNOM1:def 14;
s . i in the
carrier of
R *
by A13, A73, FUNCT_2:7;
then
(
i is
Element of
NAT &
p' = x . (i -' 1) &
q' = y . (((b . n) + 1) -' i) &
s . i is
FinSequence of the
carrier of
R )
by FINSEQ_1:def 11;
then
len (s . i) = len (decomp bn)
by A12, A13, A73;
then A74:
dom (s . i) =
dom (decomp bn)
by FINSEQ_3:31
.=
dom (divisors bn)
by POLYNOM1:def 19
;
then A75:
bj = (divisors bn) . j
by A73, PARTFUN1:def 8;
then
bj in rng (divisors bn)
by A73, A74, FUNCT_1:def 5;
then A76:
bj divides bn
by Th7;
set bij =
bj bag_extend (i -' 1);
then
bj bag_extend (i -' 1) divides b
by POLYNOM1:def 13;
then
bj bag_extend (i -' 1) in rng (divisors b)
by Th7;
then consider k being
set such that A85:
(
k in dom (divisors b) &
bj bag_extend (i -' 1) = (divisors b) . k )
by FUNCT_1:def 5;
A86:
dom p = dom u
by A60, FUNCT_2:def 1;
A87:
dom u =
dom (decomp b)
by A23, FINSEQ_3:31
.=
dom (divisors b)
by POLYNOM1:def 19
;
(
k is
Element of
NAT &
bj bag_extend (i -' 1) = (divisors b) . k &
j in dom (divisors bn) &
(divisors bn) . j = (bj bag_extend (i -' 1)) | n )
by A73, A74, A75, A85, Def1;
then A88:
(
((bj bag_extend (i -' 1)) . n) + 1
in dom s &
j in dom (s . (((bj bag_extend (i -' 1)) . n) + 1)) &
p . k = (Sum (Card (s | ((((bj bag_extend (i -' 1)) . n) + 1) -' 1)))) + j )
by A34, A85, A87;
A89:
( 1
<= i &
i <= (b . n) + 1 )
by A6, A13, A73, FINSEQ_3:27;
(bj bag_extend (i -' 1)) . n = i -' 1
by Def1;
then
((bj bag_extend (i -' 1)) . n) + 1
= i
by A89, XREAL_1:237;
hence
n1' in rng p
by A73, A85, A86, A87, A88, FUNCT_1:def 5;
:: thesis: verum
end; then A90:
rng p = dom (FlattenSeq s)
by XBOOLE_0:def 10;
A91:
dom p = dom u
by A60, FUNCT_2:def 1;
A92:
len u =
card (dom u)
by CARD_1:104
.=
card p
by A91, CARD_1:104
.=
card (dom (FlattenSeq s))
by A71, A90, POLYNOM1:7
.=
len (FlattenSeq s)
by CARD_1:104
;
then A93:
dom u = dom (FlattenSeq s)
by FINSEQ_3:31;
then
p is
Permutation of
(dom u)
by A71, A90, FUNCT_2:83;
hence
Pxy . b' = PxPy . b'
by A22, A23, A35, A92, A93, RLVECT_2:8;
:: thesis: verum end;
hence
(upm n,R) . (x' * y') = ((upm n,R) . x') * ((upm n,R) . y')
by FUNCT_2:18;
:: thesis: verum
end;