set P = upm (n,R);
set CR = the carrier of R;
set PNR = Polynom-Ring (n,R);
set CPNR = the carrier of (Polynom-Ring (n,R));
thus
upm (n,R) is multiplicative
verumproof
let x9,
y9 be
Element of the
carrier of
(Polynom-Ring (Polynom-Ring (n,R)));
GROUP_6:def 6 (upm (n,R)) . (x9 * y9) = ((upm (n,R)) . x9) * ((upm (n,R)) . y9)
reconsider x =
x9,
y =
y9,
xy =
x9 * y9 as
Polynomial of
(Polynom-Ring (n,R)) by POLYNOM3:def 10;
reconsider Pxy =
(upm (n,R)) . (x9 * y9),
PxPy =
((upm (n,R)) . x9) * ((upm (n,R)) . y9),
Px =
(upm (n,R)) . x9,
Py =
(upm (n,R)) . y9 as
Polynomial of
(n + 1),
R by POLYNOM1:def 11;
A3:
xy = x *' y
by POLYNOM3:def 10;
A4:
PxPy = Px *' Py
by POLYNOM1:def 11;
now for b9 being object st b9 in Bags (n + 1) holds
Pxy . b9 = PxPy . b9let b9 be
object ;
( b9 in Bags (n + 1) implies Pxy . b9 = PxPy . b9 )assume
b9 in Bags (n + 1)
;
Pxy . b9 = PxPy . b9then reconsider b =
b9 as
Element of
Bags (n + 1) ;
consider r being
FinSequence of the
carrier of
(Polynom-Ring (n,R)) such that A5:
len r = (b . n) + 1
and A6:
xy . (b . n) = Sum r
and A7:
for
k being
Element of
NAT st
k in dom r holds
r . k = (x . (k -' 1)) * (y . (((b . n) + 1) -' k))
by A3, POLYNOM3:def 9;
n < n + 1
by NAT_1:13;
then reconsider bn =
b | n as
Element of
Bags n by Th3;
defpred S1[
object ,
object ]
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
n st
(
(decomp bn) /. k = <*b1,b2*> &
fcr /. k = (p . b1) * (q . b2) ) ) );
reconsider xybn =
xy . (b . n) as
Polynomial of
n,
R by POLYNOM1:def 11;
consider u being
FinSequence of the
carrier of
R such that A8:
PxPy . b = Sum u
and A9:
len u = len (decomp b)
and A10:
for
k being
Element of
NAT st
k in dom u holds
ex
b1,
b2 being
bag of
n + 1 st
(
(decomp b) /. k = <*b1,b2*> &
u /. k = (Px . b1) * (Py . b2) )
by A4, POLYNOM1:def 10;
consider s being
Function of
(dom r),
( the carrier of R *) such that A14:
for
e being
object st
e in dom r holds
S1[
e,
s . e]
from FUNCT_2:sch 1(A11);
A15:
rng s c= the
carrier of
R *
;
A16:
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
s is
FinSequence-like
by FINSEQ_1:def 2;
then reconsider s =
s as
FinSequence of the
carrier of
R * by A15, FINSEQ_1:def 4;
consider g being
Function of the
carrier of
(Polynom-Ring (n,R)), the
carrier of
R such that A17:
for
p being
Polynomial of
n,
R holds
g . p = p . bn
and A18:
xybn . bn = Sum (g * r)
by A6, Th29;
A19:
Sum (g * r) = Pxy . b
by A18, Def6;
0 + 1
<= len r
by A5, XREAL_1:6;
then A20:
1
in dom s
by A16, FINSEQ_3:25;
defpred S2[
object ,
object ]
means for
i,
n1 being
Element of
NAT for
b1 being
bag of
n + 1 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 );
set t =
FlattenSeq s;
A23:
now for n19 being object st n19 in dom u holds
ex n29 being object st
( n29 in dom (FlattenSeq s) & S2[n19,n29] )let n19 be
object ;
( n19 in dom u implies ex n29 being object st
( n29 in dom (FlattenSeq s) & S2[n19,n29] ) )assume A24:
n19 in dom u
;
ex n29 being object st
( n29 in dom (FlattenSeq s) & S2[n19,n29] )then reconsider n1 =
n19 as
Element of
NAT ;
dom u =
dom (decomp b)
by A9, FINSEQ_3:29
.=
dom (divisors b)
by PRE_POLY:def 17
;
then A25:
(divisors b) . n1 in rng (divisors b)
by A24, FUNCT_1:def 3;
then reconsider b1 =
(divisors b) . n1 as
bag of
n + 1 ;
A26:
b1 divides b
by A25, Th7;
then
b1 . n <= b . n
by PRE_POLY:def 11;
then A27:
(b1 . n) + 1
<= (b . n) + 1
by XREAL_1:6;
n < n + 1
by NAT_1:13;
then reconsider b1n =
b1 | n as
Element of
Bags n by Th3;
reconsider p =
x . (((b1 . n) + 1) -' 1),
q =
y . (((b . n) + 1) -' ((b1 . n) + 1)) as
Polynomial of
n,
R by POLYNOM1:def 11;
A28:
(
p = x . (((b1 . n) + 1) -' 1) &
q = y . (((b . n) + 1) -' ((b1 . n) + 1)) )
;
b1n divides bn
by A26, Th4;
then
b1n in rng (divisors bn)
by Th7;
then consider i being
object such that A29:
i in dom (divisors bn)
and A30:
b1n = (divisors bn) . i
by FUNCT_1:def 3;
reconsider i =
i as
Element of
NAT by A29;
set n2 =
(Sum (Card (s | (((b1 . n) + 1) -' 1)))) + i;
A31:
(b1 . n) + 1
>= 1
+ 0
by XREAL_1:6;
then A32:
(b1 . n) + 1
in dom s
by A5, A16, A27, FINSEQ_3:25;
then
s . ((b1 . n) + 1) is
Element of the
carrier of
R *
by A16, FUNCT_2:5;
then
len (s . ((b1 . n) + 1)) = len (decomp bn)
by A14, A16, A32, A28;
then A33:
dom (s . ((b1 . n) + 1)) =
dom (decomp bn)
by FINSEQ_3:29
.=
dom (divisors bn)
by PRE_POLY:def 17
;
then A34:
(Sum (Card (s | (((b1 . n) + 1) -' 1)))) + i in dom (FlattenSeq s)
by A29, A32, PRE_POLY:30;
for
i9,
n19 being
Element of
NAT for
b19 being
bag of
n + 1 st
n19 = n1 &
b19 = (divisors b) . n19 &
i9 in dom (divisors bn) &
(divisors bn) . i9 = b19 | n holds
(
(b19 . n) + 1
in dom s &
i9 in dom (s . ((b19 . n) + 1)) &
(Sum (Card (s | (((b1 . n) + 1) -' 1)))) + i = (Sum (Card (s | (((b19 . n) + 1) -' 1)))) + i9 )
by A5, A16, A29, A30, A27, A31, A33, FINSEQ_3:25, FUNCT_1:def 4;
hence
ex
n29 being
object st
(
n29 in dom (FlattenSeq s) &
S2[
n19,
n29] )
by A34;
verum end; consider p being
Function of
(dom u),
(dom (FlattenSeq s)) such that A35:
for
x being
object st
x in dom u holds
S2[
x,
p . x]
from FUNCT_2:sch 1(A23);
1
in dom (Card s)
by A20, CARD_3:def 2;
then
Sum (Card s) >= (Card s) . 1
by POLYNOM3:4;
then
Sum (Card s) > 0
by A20, A21, CARD_3:def 2;
then
len (FlattenSeq s) > 0
by PRE_POLY:27;
then A36:
FlattenSeq s <> {}
;
then A37:
dom p = dom u
by FUNCT_2:def 1;
now for n19, n29 being object st n19 in dom p & n29 in dom p & p . n19 = p . n29 holds
n19 = n29let n19,
n29 be
object ;
( n19 in dom p & n29 in dom p & p . n19 = p . n29 implies n19 = n29 )assume that A38:
n19 in dom p
and A39:
n29 in dom p
and A40:
p . n19 = p . n29
;
n19 = n29
dom p = dom u
by A36, FUNCT_2:def 1;
then reconsider n1 =
n19,
n2 =
n29 as
Element of
NAT by A38, A39;
A41:
dom u =
dom (decomp b)
by A9, FINSEQ_3:29
.=
dom (divisors b)
by PRE_POLY:def 17
;
then A42:
(divisors b) . n1 in rng (divisors b)
by A38, FUNCT_1:def 3;
then reconsider b1 =
(divisors b) . n1 as
bag of
n + 1 ;
A43:
(divisors b) . n2 in rng (divisors b)
by A39, A41, FUNCT_1:def 3;
then reconsider b2 =
(divisors b) . n2 as
bag of
n + 1 ;
n < n + 1
by NAT_1:13;
then reconsider b1n =
b1 | n,
b2n =
b2 | n as
Element of
Bags n by Th3;
A44:
(
(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;
b2 divides b
by A43, Th7;
then
b2n divides bn
by Th4;
then
b2n in rng (divisors bn)
by Th7;
then consider i2 being
object such that A45:
i2 in dom (divisors bn)
and A46:
b2n = (divisors bn) . i2
by FUNCT_1:def 3;
reconsider i2 =
i2 as
Element of
NAT by A45;
A47:
(
(b2 . n) + 1
in dom s &
i2 in dom (s . ((b2 . n) + 1)) )
by A35, A39, A45, A46;
b1 divides b
by A42, Th7;
then
b1n divides bn
by Th4;
then
b1n in rng (divisors bn)
by Th7;
then consider i1 being
object such that A48:
i1 in dom (divisors bn)
and A49:
b1n = (divisors bn) . i1
by FUNCT_1:def 3;
reconsider i1 =
i1 as
Element of
NAT by A48;
A50:
p . n1 = (Sum (Card (s | (((b1 . n) + 1) -' 1)))) + i1
by A35, A38, A48, A49;
A51:
p . n2 = (Sum (Card (s | (((b2 . n) + 1) -' 1)))) + i2
by A35, A39, A45, A46;
A52:
b2 is
Element of
Bags (n + 1)
by PRE_POLY:def 12;
(
(b1 . n) + 1
in dom s &
i1 in dom (s . ((b1 . n) + 1)) )
by A35, A38, A48, A49;
then A53:
(
(b1 . n) + 1
= (b2 . n) + 1 &
i1 = i2 )
by A40, A50, A47, A51, A44, POLYNOM3:22;
b1 is
Element of
Bags (n + 1)
by PRE_POLY:def 12;
then b1 =
b1n bag_extend (b1 . n)
by Def1
.=
b2
by A49, A46, A53, A52, Def1
;
hence
n19 = n29
by A38, A39, A41, FUNCT_1:def 4;
verum end; then A54:
p is
one-to-one
by FUNCT_1:def 4;
dom (FlattenSeq s) c= rng p
proof
let n19 be
object ;
TARSKI:def 3 ( not n19 in dom (FlattenSeq s) or n19 in rng p )
assume A55:
n19 in dom (FlattenSeq s)
;
n19 in rng p
then reconsider n1 =
n19 as
Element of
NAT ;
consider i,
j being
Nat such that A56:
i in dom s
and A57:
j in dom (s . i)
and A58:
n1 = (Sum (Card (s | (i -' 1)))) + j
and
(s . i) . j = (FlattenSeq s) . n1
by A55, PRE_POLY:29;
s . i in the
carrier of
R *
by A16, A56, FUNCT_2:5;
then A59:
s . i is
FinSequence of the
carrier of
R
by FINSEQ_1:def 11;
reconsider bj =
(divisors bn) /. j as
bag of
n ;
set bij =
bj bag_extend (i -' 1);
reconsider p9 =
x . (i -' 1),
q9 =
y . (((b . n) + 1) -' i) as
Polynomial of
n,
R by POLYNOM1:def 11;
A60:
(bj bag_extend (i -' 1)) . n = i -' 1
by Def1;
1
<= i
by A56, FINSEQ_3:25;
then A61:
((bj bag_extend (i -' 1)) . n) + 1
= i
by A60, XREAL_1:235;
A62:
dom u =
dom (decomp b)
by A9, FINSEQ_3:29
.=
dom (divisors b)
by PRE_POLY:def 17
;
(
p9 = x . (i -' 1) &
q9 = y . (((b . n) + 1) -' i) )
;
then
len (s . i) = len (decomp bn)
by A14, A16, A56, A59;
then A63:
dom (s . i) =
dom (decomp bn)
by FINSEQ_3:29
.=
dom (divisors bn)
by PRE_POLY:def 17
;
then A64:
bj = (divisors bn) . j
by A57, PARTFUN1:def 6;
then
bj in rng (divisors bn)
by A57, A63, FUNCT_1:def 3;
then A65:
bj divides bn
by Th7;
then
bj bag_extend (i -' 1) divides b
by PRE_POLY:def 11;
then
bj bag_extend (i -' 1) in rng (divisors b)
by Th7;
then consider k being
object such that A74:
k in dom (divisors b)
and A75:
bj bag_extend (i -' 1) = (divisors b) . k
by FUNCT_1:def 3;
A76:
dom p = dom u
by A36, FUNCT_2:def 1;
(divisors bn) . j = (bj bag_extend (i -' 1)) | n
by A64, Def1;
then
p . k = (Sum (Card (s | ((((bj bag_extend (i -' 1)) . n) + 1) -' 1)))) + j
by A35, A57, A63, A74, A75, A62;
hence
n19 in rng p
by A58, A74, A76, A62, A61, FUNCT_1:def 3;
verum
end; then A77:
rng p = dom (FlattenSeq s)
by XBOOLE_0:def 10;
len (Sum s) = len s
by MATRLIN:def 6;
then A78:
dom (Sum s) = dom r
by A16, FINSEQ_3:29;
A79:
now for k being Nat st k in dom r holds
(Sum s) . k = (g * r) . klet k be
Nat;
( k in dom r implies (Sum s) . k = (g * r) . k )reconsider p =
x . (k -' 1),
q =
y . (((b . n) + 1) -' k) as
Polynomial of
n,
R by POLYNOM1:def 11;
reconsider pq9 =
p *' q as
Element of the
carrier of
(Polynom-Ring (n,R)) by POLYNOM1:def 11;
assume A80:
k in dom r
;
(Sum s) . k = (g * r) . kthen reconsider sk =
s . k as
Element of the
carrier of
R * by FUNCT_2:5;
reconsider sk =
sk as
FinSequence of the
carrier of
R ;
A81:
r . k =
(x . (k -' 1)) * (y . (((b . n) + 1) -' k))
by A7, A80
.=
pq9
by POLYNOM1:def 11
;
(
(Sum s) /. k = (Sum s) . k &
s /. k = s . k )
by A16, A78, A80, PARTFUN1:def 6;
hence (Sum s) . k =
Sum sk
by A78, A80, MATRLIN:def 6
.=
(p *' q) . bn
by A14, A80
.=
g . (r . k)
by A17, A81
.=
(g * r) . k
by A80, FUNCT_1:13
;
verum end; A82:
now for n1 being Nat st n1 in dom u holds
u . n1 = (FlattenSeq s) . (p . n1)let n1 be
Nat;
( n1 in dom u implies u . n1 = (FlattenSeq s) . (p . n1) )reconsider b19 =
(divisors b) /. n1 as
bag of
n + 1 ;
assume A83:
n1 in dom u
;
u . n1 = (FlattenSeq s) . (p . n1)then consider b1,
b2 being
bag of
n + 1
such that A84:
(decomp b) /. n1 = <*b1,b2*>
and A85:
u /. n1 = (Px . b1) * (Py . b2)
by A10;
A86:
dom u = dom (decomp b)
by A9, FINSEQ_3:29;
then A87:
<*b1,b2*> = <*b19,(b -' b19)*>
by A83, A84, PRE_POLY:def 17;
then A88:
b1 = b19
by FINSEQ_1:77;
reconsider xb1n =
x . (b1 . n),
yb2n =
y . (b2 . n) as
Polynomial of
n,
R by POLYNOM1:def 11;
n < n + 1
by NAT_1:13;
then reconsider b1n =
b1 | n,
b2n =
b2 | n as
Element of
Bags n by Th3;
A89:
u . n1 =
(Px . b1) * (Py . b2)
by A83, A85, PARTFUN1:def 6
.=
(xb1n . b1n) * (Py . b2)
by Def6
.=
(xb1n . b1n) * (yb2n . b2n)
by Def6
;
A90:
b2 = b -' b19
by A87, FINSEQ_1:77;
A91:
n1 in dom (divisors b)
by A83, A86, PRE_POLY:def 17;
then A92:
b1 = (divisors b) . n1
by A88, PARTFUN1:def 6;
then
b1 in rng (divisors b)
by A91, FUNCT_1:def 3;
then A93:
b1 divides b
by Th7;
then
b1n divides bn
by Th4;
then
b1n in rng (divisors bn)
by Th7;
then consider i being
object such that A94:
i in dom (divisors bn)
and A95:
b1n = (divisors bn) . i
by FUNCT_1:def 3;
reconsider i =
i as
Element of
NAT by A94;
A96:
b1 . n <= b . n
by A93, PRE_POLY:def 11;
then
(b1 . n) + 1
<= (b . n) + 1
by XREAL_1:6;
then A97:
((b . n) + 1) -' ((b1 . n) + 1) =
((b . n) + 1) - ((b1 . n) + 1)
by XREAL_1:233
.=
(((b . n) - (b1 . n)) + 1) - 1
.=
(b . n) -' (b1 . n)
by A96, XREAL_1:233
.=
b2 . n
by A88, A90, PRE_POLY:def 6
;
A98:
((b1 . n) + 1) -' 1 =
((b1 . n) + 1) - 1
by NAT_D:37
.=
b1 . n
;
then A99:
xb1n = x . (((b1 . n) + 1) -' 1)
;
A100:
(b1 . n) + 1
in dom s
by A35, A83, A92, A94, A95;
then
s . ((b1 . n) + 1) is
Element of the
carrier of
R *
by A16, FUNCT_2:5;
then reconsider sb1n1 =
s . ((b1 . n) + 1) as
FinSequence of the
carrier of
R ;
A101:
i in dom (s . ((b1 . n) + 1))
by A35, A83, A92, A94, A95;
then consider B1,
B2 being
bag of
n such that A102:
(decomp bn) /. i = <*B1,B2*>
and A103:
sb1n1 /. i = (xb1n . B1) * (yb2n . B2)
by A14, A16, A100, A98, A97;
p . n1 = (Sum (Card (s | (((b1 . n) + 1) -' 1)))) + i
by A35, A83, A92, A94, A95;
then A104:
(FlattenSeq s) . (p . n1) = (s . ((b1 . n) + 1)) . i
by A100, A101, PRE_POLY:30;
reconsider B19 =
(divisors bn) /. i as
bag of
n ;
A105:
dom (divisors bn) = dom (decomp bn)
by PRE_POLY:def 17;
then A106:
<*B1,B2*> = <*B19,(bn -' B19)*>
by A94, A102, PRE_POLY:def 17;
then A107:
B1 = B19
by FINSEQ_1:77;
then A108:
B1 = b1n
by A94, A95, PARTFUN1:def 6;
yb2n = y . (((b . n) + 1) -' ((b1 . n) + 1))
by A97;
then
len sb1n1 = len (decomp bn)
by A14, A16, A100, A99;
then A109:
dom sb1n1 = dom (divisors bn)
by A105, FINSEQ_3:29;
B2 = bn -' B19
by A106, FINSEQ_1:77;
then
B2 = b2n
by A88, A90, A107, A108, Th5;
hence
u . n1 = (FlattenSeq s) . (p . n1)
by A89, A94, A104, A103, A108, A109, PARTFUN1:def 6;
verum end;
dom r = dom (g * r)
by FINSEQ_3:120;
then
Sum s = g * r
by A78, A79, FINSEQ_1:13;
then A110:
Sum (FlattenSeq s) = Pxy . b
by A19, POLYNOM1:14;
A111:
len u =
card (dom u)
by CARD_1:62
.=
card p
by A37, CARD_1:62
.=
card (dom (FlattenSeq s))
by A54, A77, PRE_POLY:19
.=
len (FlattenSeq s)
by CARD_1:62
;
then A112:
dom u = dom (FlattenSeq s)
by FINSEQ_3:29;
then
p is
Permutation of
(dom u)
by A54, A77, FUNCT_2:57;
hence
Pxy . b9 = PxPy . b9
by A110, A8, A82, A111, A112, RLVECT_2:6;
verum end;
hence
(upm (n,R)) . (x9 * y9) = ((upm (n,R)) . x9) * ((upm (n,R)) . y9)
by FUNCT_2:12;
verum
end;