let n be Ordinal; :: thesis: for L being non empty right_complementable associative right_unital distributive Abelian add-associative right_zeroed doubleLoopStr
for p, q, r being Series of n,L holds (p *' q) *' r = p *' (q *' r)
let L be non empty right_complementable associative right_unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for p, q, r being Series of n,L holds (p *' q) *' r = p *' (q *' r)
let p, q, r be Series of n,L; :: thesis: (p *' q) *' r = p *' (q *' r)
set cL = the carrier of L;
reconsider pqra = (p *' q) *' r, pqrb = p *' (q *' r) as Function of (Bags n),the carrier of L ;
set pq = p *' q;
set qr = q *' r;
now let b be
Element of
Bags n;
:: thesis: pqra . b = pqrb . bset db =
decomp b;
consider ls being
FinSequence of the
carrier of
L such that A1:
pqra . b = Sum ls
and A2:
len ls = len (decomp b)
and A3:
for
k being
Element of
NAT st
k in dom ls holds
ex
b1,
b2 being
bag of st
(
(decomp b) /. k = <*b1,b2*> &
ls /. k = ((p *' q) . b1) * (r . b2) )
by Def26;
consider rs being
FinSequence of the
carrier of
L such that A4:
pqrb . b = Sum rs
and A5:
len rs = len (decomp b)
and A6:
for
k being
Element of
NAT st
k in dom rs holds
ex
b1,
b2 being
bag of st
(
(decomp b) /. k = <*b1,b2*> &
rs /. k = (p . b1) * ((q *' r) . b2) )
by Def26;
deffunc H1(
Nat)
-> FinSequence-yielding FinSequence =
(decomp (((decomp b) /. $1) /. 1)) ^^ ((len (decomp (((decomp b) /. $1) /. 1))) |-> <*(((decomp b) /. $1) /. 2)*>);
consider dbl being
FinSequence such that A7:
len dbl = len (decomp b)
and A8:
for
k being
Nat st
k in dom dbl holds
dbl . k = H1(
k)
from FINSEQ_1:sch 2();
deffunc H2(
Nat)
-> FinSequence-yielding FinSequence =
((len (decomp (((decomp b) /. $1) /. 2))) |-> <*(((decomp b) /. $1) /. 1)*>) ^^ (decomp (((decomp b) /. $1) /. 2));
consider dbr being
FinSequence such that A9:
len dbr = len (decomp b)
and A10:
for
k being
Nat st
k in dom dbr holds
dbr . k = H2(
k)
from FINSEQ_1:sch 2();
A11:
rng dbl c= (3 -tuples_on (Bags n)) *
rng dbr c= (3 -tuples_on (Bags n)) *
then reconsider dbl =
dbl,
dbr =
dbr as
FinSequence of
(3 -tuples_on (Bags n)) * by A11, FINSEQ_1:def 4;
deffunc H3(
Element of 3
-tuples_on (Bags n))
-> Element of the
carrier of
L =
((p . ($1 /. 1)) * (q . ($1 /. 2))) * (r . ($1 /. 3));
consider v being
Function of
(3 -tuples_on (Bags n)),the
carrier of
L such that A24:
for
b being
Element of 3
-tuples_on (Bags n) holds
v . b = H3(
b)
from FUNCT_2:sch 4();
A25:
dom v = 3
-tuples_on (Bags n)
by FUNCT_2:def 1;
set fdbl =
FlattenSeq dbl;
set fdbr =
FlattenSeq dbr;
reconsider vfdbl =
v * (FlattenSeq dbl),
vfdbr =
v * (FlattenSeq dbr) as
FinSequence of the
carrier of
L by FINSEQ_2:36;
consider vdbl being
FinSequence of the
carrier of
L * such that A26:
vdbl = ((dom dbl) --> v) ** dbl
and A27:
vfdbl = FlattenSeq vdbl
by Th36;
A28:
Sum vfdbl = Sum (Sum vdbl)
by A27, Th34;
now set f =
Sum vdbl;
A29:
dom (Sum vdbl) = dom vdbl
by Th15;
A30:
dom vdbl =
(dom ((dom dbl) --> v)) /\ (dom dbl)
by A26, PBOOLE:def 24
.=
(dom dbl) /\ (dom dbl)
by FUNCOP_1:19
.=
dom dbl
;
hence
len (Sum vdbl) = len ls
by A2, A7, A29, FINSEQ_3:31;
:: thesis: for k being Nat st 1 <= k & k <= len ls holds
(Sum vdbl) . k = ls . klet k be
Nat;
:: thesis: ( 1 <= k & k <= len ls implies (Sum vdbl) . k = ls . k )assume A31:
( 1
<= k &
k <= len ls )
;
:: thesis: (Sum vdbl) . k = ls . kA32:
dom ls = dom (Sum vdbl)
by A2, A7, A29, A30, FINSEQ_3:31;
A33:
k in dom (Sum vdbl)
by A2, A7, A29, A30, A31, FINSEQ_3:27;
then consider b1,
b2 being
bag of
such that A34:
(decomp b) /. k = <*b1,b2*>
and A35:
ls /. k = ((p *' q) . b1) * (r . b2)
by A3, A32;
reconsider b2' =
b2 as
Element of
Bags n by Def14;
consider pqs being
FinSequence of the
carrier of
L such that A36:
(p *' q) . b1 = Sum pqs
and A37:
len pqs = len (decomp b1)
and A38:
for
i being
Element of
NAT st
i in dom pqs holds
ex
b11,
b12 being
bag of st
(
(decomp b1) /. i = <*b11,b12*> &
pqs /. i = (p . b11) * (q . b12) )
by Def26;
A39:
Sum (pqs * (r . b2)) = (Sum pqs) * (r . b2)
by Th29;
A40:
k in dom vdbl
by A2, A7, A30, A31, FINSEQ_3:27;
set vdblk =
v * (dbl . k);
set ddbk1 =
decomp (((decomp b) /. k) /. 1);
set dbk2 =
((decomp b) /. k) /. 2;
len <*b1,b2*> = 2
by FINSEQ_1:61;
then A41:
( 1
in dom <*b1,b2*> & 2
in dom <*b1,b2*> )
by FINSEQ_3:27;
then A42:
((decomp b) /. k) /. 2 =
<*b1,b2*> . 2
by A34, PARTFUN1:def 8
.=
b2
by FINSEQ_1:61
;
A43:
((decomp b) /. k) /. 1 =
<*b1,b2*> . 1
by A34, A41, PARTFUN1:def 8
.=
b1
by FINSEQ_1:61
;
A44:
dbl . k = (decomp (((decomp b) /. k) /. 1)) ^^ ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>)
by A8, A30, A40;
set dblk =
dbl . k;
A45:
dom (dbl . k) =
(dom (decomp (((decomp b) /. k) /. 1))) /\ (dom ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>))
by A44, MATRLIN:def 2
.=
(dom (decomp (((decomp b) /. k) /. 1))) /\ (Seg (len (decomp (((decomp b) /. k) /. 1))))
by FUNCOP_1:19
.=
(dom (decomp (((decomp b) /. k) /. 1))) /\ (dom (decomp (((decomp b) /. k) /. 1)))
by FINSEQ_1:def 3
.=
dom (decomp (((decomp b) /. k) /. 1))
;
k in dom dbl
by A2, A7, A31, FINSEQ_3:27;
then
dbl . k in rng dbl
by FUNCT_1:def 5;
then
dbl . k is
Element of
(3 -tuples_on (Bags n)) *
;
then reconsider dblk =
dbl . k as
FinSequence of 3
-tuples_on (Bags n) ;
A46:
dom (decomp (((decomp b) /. k) /. 1)) = Seg (len (decomp (((decomp b) /. k) /. 1)))
by FINSEQ_1:def 3;
rng dblk c= 3
-tuples_on (Bags n)
;
then A47:
dom (v * (dbl . k)) = dom dblk
by A25, RELAT_1:46;
then
dom (v * (dbl . k)) = Seg (len (decomp (((decomp b) /. k) /. 1)))
by A45, FINSEQ_1:def 3;
then reconsider vdblk =
v * (dbl . k) as
FinSequence by FINSEQ_1:def 2;
A48:
dom pqs = dom (pqs * (r . b2))
by Def3;
now thus len vdblk =
len pqs
by A37, A43, A45, A47, FINSEQ_3:31
.=
len (pqs * (r . b2))
by A48, FINSEQ_3:31
;
:: thesis: for i being Nat st 1 <= i & i <= len (pqs * (r . b2)) holds
(v * (dbl . k)) . i = (pqs * (r . b2)) . ithen A49:
dom vdblk = dom (pqs * (r . b2))
by FINSEQ_3:31;
let i be
Nat;
:: thesis: ( 1 <= i & i <= len (pqs * (r . b2)) implies (v * (dbl . k)) . i = (pqs * (r . b2)) . i )assume A50:
( 1
<= i &
i <= len (pqs * (r . b2)) )
;
:: thesis: (v * (dbl . k)) . i = (pqs * (r . b2)) . ithen A51:
i in dom (pqs * (r . b2))
by FINSEQ_3:27;
then consider b11,
b12 being
bag of
such that A52:
(decomp b1) /. i = <*b11,b12*>
and A53:
pqs /. i = (p . b11) * (q . b12)
by A38, A48;
reconsider i' =
i as
Element of
NAT by ORDINAL1:def 13;
A54:
((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>) . i' = <*(((decomp b) /. k) /. 2)*>
by A45, A46, A47, A49, A51, FUNCOP_1:13;
(decomp b1) /. i = (decomp b1) . i
by A43, A45, A47, A49, A51, PARTFUN1:def 8;
then A55:
dblk . i =
<*b11,b12*> ^ <*b2*>
by A42, A43, A44, A47, A49, A51, A52, A54, MATRLIN:def 2
.=
<*b11,b12,b2*>
by FINSEQ_1:60
;
reconsider b11' =
b11,
b12' =
b12 as
Element of
Bags n by Def14;
reconsider B =
<*b11',b12',b2'*> as
Element of 3
-tuples_on (Bags n) by FINSEQ_2:124;
A56:
i in dom pqs
by A48, A50, FINSEQ_3:27;
A57:
dom pqs = dom (pqs * (r . b2))
by Def3;
thus (v * (dbl . k)) . i =
v . (dblk . i)
by A49, A51, FUNCT_1:22
.=
((p . (B /. 1)) * (q . (B /. 2))) * (r . (B /. 3))
by A24, A55
.=
((p . b11') * (q . (B /. 2))) * (r . (B /. 3))
by FINSEQ_4:27
.=
((p . b11) * (q . b12)) * (r . (B /. 3))
by FINSEQ_4:27
.=
(pqs /. i) * (r . b2)
by A53, FINSEQ_4:27
.=
(pqs * (r . b2)) /. i
by A56, Def3
.=
(pqs * (r . b2)) . i
by A56, A57, PARTFUN1:def 8
;
:: thesis: verum end; then A58:
vdblk = pqs * (r . b2)
by FINSEQ_1:18;
A59:
vdbl /. k =
vdbl . k
by A40, PARTFUN1:def 8
.=
(((dom dbl) --> v) . k) * (dbl . k)
by A26, A40, PBOOLE:def 24
.=
pqs * (r . b2)
by A30, A40, A58, FUNCOP_1:13
;
A60:
ls /. k = ls . k
by A32, A33, PARTFUN1:def 8;
(Sum vdbl) /. k = (Sum vdbl) . k
by A33, PARTFUN1:def 8;
hence
(Sum vdbl) . k = ls . k
by A33, A35, A36, A39, A59, A60, MATRLIN:def 8;
:: thesis: verum end; then A61:
Sum vdbl = ls
by FINSEQ_1:18;
consider vdbr being
FinSequence of the
carrier of
L * such that A62:
vdbr = ((dom dbr) --> v) ** dbr
and A63:
vfdbr = FlattenSeq vdbr
by Th36;
A64:
Sum vfdbr = Sum (Sum vdbr)
by A63, Th34;
now set f =
Sum vdbr;
A65:
dom (Sum vdbr) = dom vdbr
by Th15;
A66:
dom vdbr =
(dom ((dom dbr) --> v)) /\ (dom dbr)
by A62, PBOOLE:def 24
.=
(dom dbr) /\ (dom dbr)
by FUNCOP_1:19
.=
dom dbr
;
hence
len (Sum vdbr) = len rs
by A5, A9, A65, FINSEQ_3:31;
:: thesis: for k being Nat st 1 <= k & k <= len rs holds
(Sum vdbr) . k = rs . klet k be
Nat;
:: thesis: ( 1 <= k & k <= len rs implies (Sum vdbr) . k = rs . k )assume A67:
( 1
<= k &
k <= len rs )
;
:: thesis: (Sum vdbr) . k = rs . kA68:
dom rs = dom (Sum vdbr)
by A5, A9, A65, A66, FINSEQ_3:31;
A69:
k in dom (Sum vdbr)
by A5, A9, A65, A66, A67, FINSEQ_3:27;
then consider b1,
b2 being
bag of
such that A70:
(decomp b) /. k = <*b1,b2*>
and A71:
rs /. k = (p . b1) * ((q *' r) . b2)
by A6, A68;
reconsider b1' =
b1 as
Element of
Bags n by Def14;
consider qrs being
FinSequence of the
carrier of
L such that A72:
(q *' r) . b2 = Sum qrs
and A73:
len qrs = len (decomp b2)
and A74:
for
i being
Element of
NAT st
i in dom qrs holds
ex
b11,
b12 being
bag of st
(
(decomp b2) /. i = <*b11,b12*> &
qrs /. i = (q . b11) * (r . b12) )
by Def26;
A75:
Sum ((p . b1) * qrs) = (p . b1) * (Sum qrs)
by Th28;
A76:
k in dom vdbr
by A5, A9, A66, A67, FINSEQ_3:27;
set vdbrk =
v * (dbr . k);
set ddbk1 =
decomp (((decomp b) /. k) /. 2);
set dbk2 =
((decomp b) /. k) /. 1;
len <*b1,b2*> = 2
by FINSEQ_1:61;
then A77:
( 1
in dom <*b1,b2*> & 2
in dom <*b1,b2*> )
by FINSEQ_3:27;
then A78:
((decomp b) /. k) /. 1 =
<*b1,b2*> . 1
by A70, PARTFUN1:def 8
.=
b1
by FINSEQ_1:61
;
A79:
((decomp b) /. k) /. 2 =
<*b1,b2*> . 2
by A70, A77, PARTFUN1:def 8
.=
b2
by FINSEQ_1:61
;
A80:
dbr . k = ((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) ^^ (decomp (((decomp b) /. k) /. 2))
by A10, A66, A76;
set dbrk =
dbr . k;
A81:
dom (dbr . k) =
(dom (decomp (((decomp b) /. k) /. 2))) /\ (dom ((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>))
by A80, MATRLIN:def 2
.=
(dom (decomp (((decomp b) /. k) /. 2))) /\ (Seg (len (decomp (((decomp b) /. k) /. 2))))
by FUNCOP_1:19
.=
(dom (decomp (((decomp b) /. k) /. 2))) /\ (dom (decomp (((decomp b) /. k) /. 2)))
by FINSEQ_1:def 3
.=
dom (decomp (((decomp b) /. k) /. 2))
;
k in dom dbr
by A5, A9, A67, FINSEQ_3:27;
then
dbr . k in rng dbr
by FUNCT_1:def 5;
then
dbr . k is
Element of
(3 -tuples_on (Bags n)) *
;
then reconsider dbrk =
dbr . k as
FinSequence of 3
-tuples_on (Bags n) ;
A82:
dom (decomp (((decomp b) /. k) /. 2)) = Seg (len (decomp (((decomp b) /. k) /. 2)))
by FINSEQ_1:def 3;
rng dbrk c= 3
-tuples_on (Bags n)
;
then A83:
dom (v * (dbr . k)) = dom dbrk
by A25, RELAT_1:46;
then
dom (v * (dbr . k)) = Seg (len (decomp (((decomp b) /. k) /. 2)))
by A81, FINSEQ_1:def 3;
then reconsider vdbrk =
v * (dbr . k) as
FinSequence by FINSEQ_1:def 2;
A84:
dom qrs = dom ((p . b1) * qrs)
by Def2;
then A85:
len qrs = len ((p . b1) * qrs)
by FINSEQ_3:31;
then A86:
len vdbrk = len ((p . b1) * qrs)
by A73, A79, A81, A83, FINSEQ_3:31;
A87:
dom vdbrk = dom ((p . b1) * qrs)
by A73, A79, A81, A83, A84, FINSEQ_3:31;
now let i be
Nat;
:: thesis: ( 1 <= i & i <= len ((p . b1) * qrs) implies (v * (dbr . k)) . i = ((p . b1) * qrs) . i )assume A88:
( 1
<= i &
i <= len ((p . b1) * qrs) )
;
:: thesis: (v * (dbr . k)) . i = ((p . b1) * qrs) . ithen A89:
i in dom dbrk
by A73, A79, A81, A85, FINSEQ_3:27;
then consider b11,
b12 being
bag of
such that A90:
(decomp b2) /. i = <*b11,b12*>
and A91:
qrs /. i = (q . b11) * (r . b12)
by A74, A83, A84, A87;
reconsider i' =
i as
Element of
NAT by ORDINAL1:def 13;
A92:
((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) . i' = <*(((decomp b) /. k) /. 1)*>
by A81, A82, A89, FUNCOP_1:13;
(decomp b2) /. i = (decomp b2) . i
by A79, A81, A89, PARTFUN1:def 8;
then A93:
dbrk . i =
<*b1*> ^ <*b11,b12*>
by A78, A79, A80, A89, A90, A92, MATRLIN:def 2
.=
<*b1,b11,b12*>
by FINSEQ_1:60
;
reconsider b11' =
b11,
b12' =
b12 as
Element of
Bags n by Def14;
reconsider B =
<*b1',b11',b12'*> as
Element of 3
-tuples_on (Bags n) by FINSEQ_2:124;
A94:
i in dom qrs
by A84, A88, FINSEQ_3:27;
thus (v * (dbr . k)) . i =
v . (dbrk . i)
by A83, A89, FUNCT_1:22
.=
((p . (B /. 1)) * (q . (B /. 2))) * (r . (B /. 3))
by A24, A93
.=
((p . b1) * (q . (B /. 2))) * (r . (B /. 3))
by FINSEQ_4:27
.=
((p . b1) * (q . b11)) * (r . (B /. 3))
by FINSEQ_4:27
.=
((p . b1) * (q . b11)) * (r . b12)
by FINSEQ_4:27
.=
(p . b1) * (qrs /. i)
by A91, GROUP_1:def 4
.=
((p . b1) * qrs) /. i
by A94, Def2
.=
((p . b1) * qrs) . i
by A84, A94, PARTFUN1:def 8
;
:: thesis: verum end; then A95:
vdbrk = (p . b1) * qrs
by A86, FINSEQ_1:18;
A96:
vdbr /. k =
vdbr . k
by A76, PARTFUN1:def 8
.=
(((dom dbr) --> v) . k) * (dbr . k)
by A62, A76, PBOOLE:def 24
.=
(p . b1) * qrs
by A66, A76, A95, FUNCOP_1:13
;
A97:
rs /. k = rs . k
by A68, A69, PARTFUN1:def 8;
(Sum vdbr) /. k = (Sum vdbr) . k
by A69, PARTFUN1:def 8;
hence
(Sum vdbr) . k = rs . k
by A69, A71, A72, A75, A96, A97, MATRLIN:def 8;
:: thesis: verum end; then A98:
Sum vdbr = rs
by FINSEQ_1:18;
(
dom dbl = dom (decomp b) &
dom dbr = dom (decomp b) )
by A7, A9, FINSEQ_3:31;
then consider P being
Permutation of
(dom (FlattenSeq dbl)) such that A99:
FlattenSeq dbr = (FlattenSeq dbl) * P
by A8, A10, Th78;
rng (FlattenSeq dbl) c= 3
-tuples_on (Bags n)
;
then
dom vfdbl = dom (FlattenSeq dbl)
by A25, RELAT_1:46;
then reconsider P =
P as
Permutation of
(dom vfdbl) ;
vfdbr = vfdbl * P
by A99, RELAT_1:55;
hence
pqra . b = pqrb . b
by A1, A4, A28, A61, A64, A98, RLVECT_2:9;
:: thesis: verum end;
hence
(p *' q) *' r = p *' (q *' r)
by FUNCT_2:113; :: thesis: verum