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
:: 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;
A3:
xy = x *' y
by POLYNOM3:def 12;
A4:
PxPy = Px *' Py
by POLYNOM1:def 27;
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 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 11;
n < n + 1
by NAT_1:13;
then reconsider bn =
b | n as
Element of
Bags n by Th3;
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) ) ) );
reconsider xybn =
xy . (b . n) as
Polynomial of
n,
R by POLYNOM1:def 27;
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 st
(
(decomp b) /. k = <*b1,b2*> &
u /. k = (Px . b1) * (Py . b2) )
by A4, POLYNOM1:def 26;
consider s being
Function of
(dom r),
(the carrier of R * ) such that A14:
for
e being
set 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:8;
then A20:
1
in dom s
by A16, FINSEQ_3:27;
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 );
set t =
FlattenSeq s;
A23:
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 A24:
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 A9, FINSEQ_3:31
.=
dom (divisors b)
by PRE_POLY:def 17
;
then A25:
(divisors b) . n1 in rng (divisors b)
by A24, FUNCT_1:def 5;
then reconsider b1 =
(divisors b) . n1 as
bag of
by PRE_POLY:def 12;
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:8;
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 27;
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
set such that A29:
i in dom (divisors bn)
and A30:
b1n = (divisors bn) . i
by FUNCT_1:def 5;
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:8;
then A32:
(b1 . n) + 1
in dom s
by A5, A16, A27, FINSEQ_3:27;
then
s . ((b1 . n) + 1) is
Element of the
carrier of
R *
by A16, FUNCT_2:7;
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:31
.=
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
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 A5, A16, A29, A30, A27, A31, A33, FINSEQ_3:27, FUNCT_1:def 8;
hence
ex
n2' being
set st
(
n2' in dom (FlattenSeq s) &
S2[
n1',
n2'] )
by A34;
:: thesis: verum end; consider p being
Function of
(dom u),
(dom (FlattenSeq s)) such that A35:
for
x being
set 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 let n1',
n2' be
set ;
:: thesis: ( n1' in dom p & n2' in dom p & p . n1' = p . n2' implies n1' = n2' )assume that A38:
n1' in dom p
and A39:
n2' in dom p
and A40:
p . n1' = p . n2'
;
:: thesis: n1' = n2'
dom p = dom u
by A36, FUNCT_2:def 1;
then reconsider n1 =
n1',
n2 =
n2' as
Element of
NAT by A38, A39;
A41:
dom u =
dom (decomp b)
by A9, FINSEQ_3:31
.=
dom (divisors b)
by PRE_POLY:def 17
;
then A42:
(divisors b) . n1 in rng (divisors b)
by A38, FUNCT_1:def 5;
then reconsider b1 =
(divisors b) . n1 as
bag of
by PRE_POLY:def 12;
A43:
(divisors b) . n2 in rng (divisors b)
by A39, A41, FUNCT_1:def 5;
then reconsider b2 =
(divisors b) . n2 as
bag of
by PRE_POLY:def 12;
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
set such that A45:
i2 in dom (divisors bn)
and A46:
b2n = (divisors bn) . i2
by FUNCT_1:def 5;
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
set such that A48:
i1 in dom (divisors bn)
and A49:
b1n = (divisors bn) . i1
by FUNCT_1:def 5;
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
n1' = n2'
by A38, A39, A41, FUNCT_1:def 8;
:: thesis: verum end; then A54:
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 A55:
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 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:7;
then A59:
s . i is
FinSequence of the
carrier of
R
by FINSEQ_1:def 11;
reconsider bj =
(divisors bn) /. j as
bag of
by PRE_POLY:def 12;
set bij =
bj bag_extend (i -' 1);
reconsider p' =
x . (i -' 1),
q' =
y . (((b . n) + 1) -' i) as
Polynomial of
n,
R by POLYNOM1:def 27;
A60:
(bj bag_extend (i -' 1)) . n = i -' 1
by Def1;
1
<= i
by A56, FINSEQ_3:27;
then A61:
((bj bag_extend (i -' 1)) . n) + 1
= i
by A60, XREAL_1:237;
A62:
dom u =
dom (decomp b)
by A9, FINSEQ_3:31
.=
dom (divisors b)
by PRE_POLY:def 17
;
(
p' = x . (i -' 1) &
q' = 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:31
.=
dom (divisors bn)
by PRE_POLY:def 17
;
then A64:
bj = (divisors bn) . j
by A57, PARTFUN1:def 8;
then
bj in rng (divisors bn)
by A57, A63, FUNCT_1:def 5;
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
set such that A74:
k in dom (divisors b)
and A75:
bj bag_extend (i -' 1) = (divisors b) . k
by FUNCT_1:def 5;
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
n1' in rng p
by A58, A74, A76, A62, A61, FUNCT_1:def 5;
:: thesis: verum
end; then A77:
rng p = dom (FlattenSeq s)
by XBOOLE_0:def 10;
len (Sum s) = len s
by MATRLIN:def 8;
then A78:
dom (Sum s) = dom r
by A16, FINSEQ_3:31;
A79:
now let k be
Nat;
:: thesis: ( 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 27;
reconsider pq' =
p *' q as
Element of the
carrier of
(Polynom-Ring n,R) by POLYNOM1:def 27;
assume A80:
k in dom r
;
:: thesis: (Sum s) . k = (g * r) . kthen reconsider sk =
s . k as
Element of the
carrier of
R * by FUNCT_2:7;
reconsider sk =
sk as
FinSequence of the
carrier of
R ;
A81:
r . k =
(x . (k -' 1)) * (y . (((b . n) + 1) -' k))
by A7, A80
.=
pq'
by POLYNOM1:def 27
;
(
(Sum s) /. k = (Sum s) . k &
s /. k = s . k )
by A16, A78, A80, PARTFUN1:def 8;
hence (Sum s) . k =
Sum sk
by A78, A80, MATRLIN:def 8
.=
(p *' q) . bn
by A14, A80
.=
g . (r . k)
by A17, A81
.=
(g * r) . k
by A80, FUNCT_1:23
;
:: thesis: verum end; A82:
now let n1 be
Element of
NAT ;
:: thesis: ( n1 in dom u implies u . n1 = (FlattenSeq s) . (p . n1) )
(divisors b) /. n1 is
Element of
Bags (n + 1)
;
then reconsider b1' =
(divisors b) /. n1 as
bag of ;
assume A83:
n1 in dom u
;
:: thesis: u . n1 = (FlattenSeq s) . (p . n1)then consider b1,
b2 being
bag of
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:31;
then A87:
<*b1,b2*> = <*b1',(b -' b1')*>
by A83, A84, PRE_POLY:def 17;
then A88:
b1 = b1'
by FINSEQ_1:98;
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;
A89:
u . n1 =
(Px . b1) * (Py . b2)
by A83, A85, PARTFUN1:def 8
.=
(xb1n . b1n) * (Py . b2)
by Def6
.=
(xb1n . b1n) * (yb2n . b2n)
by Def6
;
A90:
b2 = b -' b1'
by A87, FINSEQ_1:98;
A91:
n1 in dom (divisors b)
by A83, A86, PRE_POLY:def 17;
then A92:
b1 = (divisors b) . n1
by A88, PARTFUN1:def 8;
then
b1 in rng (divisors b)
by A91, FUNCT_1:def 5;
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
set such that A94:
i in dom (divisors bn)
and A95:
b1n = (divisors bn) . i
by FUNCT_1:def 5;
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:8;
then A97:
((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 A96, XREAL_1:235
.=
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:7;
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
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;
(divisors bn) /. i is
Element of
Bags n
;
then reconsider B1' =
(divisors bn) /. i as
bag of ;
A105:
dom (divisors bn) = dom (decomp bn)
by PRE_POLY:def 17;
then A106:
<*B1,B2*> = <*B1',(bn -' B1')*>
by A94, A102, PRE_POLY:def 17;
then A107:
B1 = B1'
by FINSEQ_1:98;
then A108:
B1 = b1n
by A94, A95, PARTFUN1:def 8;
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:31;
B2 = bn -' B1'
by A106, FINSEQ_1:98;
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 8;
:: thesis: verum end;
dom r = dom (g * r)
by ALG_1:1;
then
Sum s = g * r
by A78, A79, FINSEQ_1:17;
then A110:
Sum (FlattenSeq s) = Pxy . b
by A19, POLYNOM1:34;
A111:
len u =
card (dom u)
by CARD_1:104
.=
card p
by A37, CARD_1:104
.=
card (dom (FlattenSeq s))
by A54, A77, PRE_POLY:19
.=
len (FlattenSeq s)
by CARD_1:104
;
then A112:
dom u = dom (FlattenSeq s)
by FINSEQ_3:31;
then
p is
Permutation of
(dom u)
by A54, A77, FUNCT_2:83;
hence
Pxy . b' = PxPy . b'
by A110, A8, A82, A111, A112, 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;