let n be Ordinal; for L being non empty right_complementable right_unital distributive Abelian add-associative right_zeroed associative doubleLoopStr
for p, q, r being Series of n,L holds (p *' q) *' r = p *' (q *' r)
let L be non empty right_complementable right_unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; 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; (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 for b being Element of Bags n holds pqra . b = pqrb . blet b be
Element of
Bags n;
pqra . b = pqrb . bset db =
decomp b;
deffunc H1(
Nat)
-> set =
(decomp (((decomp b) /. $1) /. 1)) ^^ ((len (decomp (((decomp b) /. $1) /. 1))) |-> <*(((decomp b) /. $1) /. 2)*>);
consider dbl being
FinSequence such that A1:
len dbl = len (decomp b)
and A2:
for
k being
Nat st
k in dom dbl holds
dbl . k = H1(
k)
from FINSEQ_1:sch 2();
A3:
rng dbl c= (3 -tuples_on (Bags n)) *
deffunc H2(
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 A11:
for
b being
Element of 3
-tuples_on (Bags n) holds
v . b = H2(
b)
from FUNCT_2:sch 4();
deffunc H3(
Nat)
-> set =
((len (decomp (((decomp b) /. $1) /. 2))) |-> <*(((decomp b) /. $1) /. 1)*>) ^^ (decomp (((decomp b) /. $1) /. 2));
consider dbr being
FinSequence such that A12:
len dbr = len (decomp b)
and A13:
for
k being
Nat st
k in dom dbr holds
dbr . k = H3(
k)
from FINSEQ_1:sch 2();
rng dbr c= (3 -tuples_on (Bags n)) *
then reconsider dbl =
dbl,
dbr =
dbr as
FinSequence of
(3 -tuples_on (Bags n)) * by A3, FINSEQ_1:def 4;
set fdbl =
FlattenSeq dbl;
set fdbr =
FlattenSeq dbr;
consider ls being
FinSequence of the
carrier of
L such that A21:
pqra . b = Sum ls
and A22:
len ls = len (decomp b)
and A23:
for
k being
Element of
NAT st
k in dom ls holds
ex
b1,
b2 being
bag of
n st
(
(decomp b) /. k = <*b1,b2*> &
ls /. k = ((p *' q) . b1) * (r . b2) )
by Def10;
A24:
dom dbr = dom (decomp b)
by A12, FINSEQ_3:29;
reconsider vfdbl =
v * (FlattenSeq dbl),
vfdbr =
v * (FlattenSeq dbr) as
FinSequence of the
carrier of
L by FINSEQ_2:32;
consider vdbl being
FinSequence of the
carrier of
L * such that A25:
vdbl = ((dom dbl) --> v) ** dbl
and A26:
vfdbl = FlattenSeq vdbl
by PRE_POLY:32;
A27:
dom v = 3
-tuples_on (Bags n)
by FUNCT_2:def 1;
now ( len (Sum vdbl) = len ls & ( for k being Nat st 1 <= k & k <= len ls holds
(Sum vdbl) . k = ls . k ) )set f =
Sum vdbl;
A28:
dom vdbl =
(dom ((dom dbl) --> v)) /\ (dom dbl)
by A25, PBOOLE:def 19
.=
(dom dbl) /\ (dom dbl)
.=
dom dbl
;
A29:
dom (Sum vdbl) = dom vdbl
by Th2;
hence
len (Sum vdbl) = len ls
by A22, A1, A28, FINSEQ_3:29;
for k being Nat st 1 <= k & k <= len ls holds
(Sum vdbl) . k = ls . klet k be
Nat;
( 1 <= k & k <= len ls implies (Sum vdbl) . k = ls . k )assume A30:
( 1
<= k &
k <= len ls )
;
(Sum vdbl) . k = ls . kA31:
k in dom (Sum vdbl)
by A22, A1, A29, A28, A30, FINSEQ_3:25;
A32:
(Sum vdbl) /. k = (Sum vdbl) . k
by A22, A1, A29, A28, A30, FINSEQ_3:25, PARTFUN1:def 6;
A33:
dom ls = dom (Sum vdbl)
by A22, A1, A29, A28, FINSEQ_3:29;
then A34:
ls /. k = ls . k
by A30, FINSEQ_3:25, PARTFUN1:def 6;
consider b1,
b2 being
bag of
n such that A35:
(decomp b) /. k = <*b1,b2*>
and A36:
ls /. k = ((p *' q) . b1) * (r . b2)
by A23, A33, A31;
A37:
len <*b1,b2*> = 2
by FINSEQ_1:44;
then
1
in dom <*b1,b2*>
by FINSEQ_3:25;
then A38:
((decomp b) /. k) /. 1 =
<*b1,b2*> . 1
by A35, PARTFUN1:def 6
.=
b1
;
set dblk =
dbl . k;
set dbk2 =
((decomp b) /. k) /. 2;
set ddbk1 =
decomp (((decomp b) /. k) /. 1);
A39:
k in dom vdbl
by A22, A1, A28, A30, FINSEQ_3:25;
then A40:
dbl . k = (decomp (((decomp b) /. k) /. 1)) ^^ ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>)
by A2, A28;
then A41:
dom (dbl . k) =
(dom (decomp (((decomp b) /. k) /. 1))) /\ (dom ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>))
by PRE_POLY:def 4
.=
(dom (decomp (((decomp b) /. k) /. 1))) /\ (Seg (len (decomp (((decomp b) /. k) /. 1))))
.=
(dom (decomp (((decomp b) /. k) /. 1))) /\ (dom (decomp (((decomp b) /. k) /. 1)))
by FINSEQ_1:def 3
.=
dom (decomp (((decomp b) /. k) /. 1))
;
set vdblk =
v * (dbl . k);
k in dom dbl
by A22, A1, A30, FINSEQ_3:25;
then
dbl . k in rng dbl
by FUNCT_1:def 3;
then
dbl . k is
Element of
(3 -tuples_on (Bags n)) *
;
then reconsider dblk =
dbl . k as
FinSequence of 3
-tuples_on (Bags n) ;
rng dblk c= 3
-tuples_on (Bags n)
;
then A42:
dom (v * (dbl . k)) = dom dblk
by A27, RELAT_1:27;
then A43:
dom (v * (dbl . k)) = Seg (len (decomp (((decomp b) /. k) /. 1)))
by A41, FINSEQ_1:def 3;
reconsider b29 =
b2 as
Element of
Bags n by PRE_POLY:def 12;
consider pqs being
FinSequence of the
carrier of
L such that A44:
(p *' q) . b1 = Sum pqs
and A45:
len pqs = len (decomp b1)
and A46:
for
i being
Element of
NAT st
i in dom pqs holds
ex
b11,
b12 being
bag of
n st
(
(decomp b1) /. i = <*b11,b12*> &
pqs /. i = (p . b11) * (q . b12) )
by Def10;
A47:
dom pqs = dom (pqs * (r . b2))
by Def2;
2
in dom <*b1,b2*>
by A37, FINSEQ_3:25;
then A48:
((decomp b) /. k) /. 2 =
<*b1,b2*> . 2
by A35, PARTFUN1:def 6
.=
b2
;
reconsider vdblk =
v * (dbl . k) as
FinSequence by A43, FINSEQ_1:def 2;
A49:
Sum (pqs * (r . b2)) = (Sum pqs) * (r . b2)
by Th13;
A50:
dom (decomp (((decomp b) /. k) /. 1)) = Seg (len (decomp (((decomp b) /. k) /. 1)))
by FINSEQ_1:def 3;
now ( len vdblk = len (pqs * (r . b2)) & ( for i being Nat st 1 <= i & i <= len (pqs * (r . b2)) holds
(v * (dbl . k)) . i = (pqs * (r . b2)) . i ) )A51:
dom pqs = dom (pqs * (r . b2))
by Def2;
thus len vdblk =
len pqs
by A45, A38, A41, A42, FINSEQ_3:29
.=
len (pqs * (r . b2))
by A47, FINSEQ_3:29
;
for i being Nat st 1 <= i & i <= len (pqs * (r . b2)) holds
(v * (dbl . k)) . i = (pqs * (r . b2)) . ithen A52:
dom vdblk = dom (pqs * (r . b2))
by FINSEQ_3:29;
let i be
Nat;
( 1 <= i & i <= len (pqs * (r . b2)) implies (v * (dbl . k)) . i = (pqs * (r . b2)) . i )reconsider i9 =
i as
Element of
NAT by ORDINAL1:def 12;
assume A53:
( 1
<= i &
i <= len (pqs * (r . b2)) )
;
(v * (dbl . k)) . i = (pqs * (r . b2)) . ithen A54:
i in dom (pqs * (r . b2))
by FINSEQ_3:25;
then consider b11,
b12 being
bag of
n such that A55:
(decomp b1) /. i = <*b11,b12*>
and A56:
pqs /. i = (p . b11) * (q . b12)
by A46, A47;
(
((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>) . i9 = <*(((decomp b) /. k) /. 2)*> &
(decomp b1) /. i = (decomp b1) . i )
by A38, A41, A50, A42, A52, A54, FUNCOP_1:7, PARTFUN1:def 6;
then A57:
dblk . i =
<*b11,b12*> ^ <*b2*>
by A48, A38, A40, A42, A52, A54, A55, PRE_POLY:def 4
.=
<*b11,b12,b2*>
by FINSEQ_1:43
;
reconsider b119 =
b11,
b129 =
b12 as
Element of
Bags n by PRE_POLY:def 12;
reconsider B =
<*b119,b129,b29*> as
Element of 3
-tuples_on (Bags n) by FINSEQ_2:104;
A58:
i in dom pqs
by A47, A53, FINSEQ_3:25;
thus (v * (dbl . k)) . i =
v . (dblk . i)
by A52, A54, FUNCT_1:12
.=
((p . (B /. 1)) * (q . (B /. 2))) * (r . (B /. 3))
by A11, A57
.=
((p . b119) * (q . (B /. 2))) * (r . (B /. 3))
by FINSEQ_4:18
.=
((p . b11) * (q . b12)) * (r . (B /. 3))
by FINSEQ_4:18
.=
(pqs /. i) * (r . b2)
by A56, FINSEQ_4:18
.=
(pqs * (r . b2)) /. i
by A58, Def2
.=
(pqs * (r . b2)) . i
by A58, A51, PARTFUN1:def 6
;
verum end; then A59:
vdblk = pqs * (r . b2)
by FINSEQ_1:14;
vdbl /. k =
vdbl . k
by A39, PARTFUN1:def 6
.=
(((dom dbl) --> v) . k) * (dbl . k)
by A25, A39, PBOOLE:def 19
.=
pqs * (r . b2)
by A28, A39, A59, FUNCOP_1:7
;
hence
(Sum vdbl) . k = ls . k
by A31, A36, A44, A49, A34, A32, MATRLIN:def 6;
verum end; then A60:
Sum vdbl = ls
by FINSEQ_1:14;
consider vdbr being
FinSequence of the
carrier of
L * such that A61:
vdbr = ((dom dbr) --> v) ** dbr
and A62:
vfdbr = FlattenSeq vdbr
by PRE_POLY:32;
A63:
Sum vfdbr = Sum (Sum vdbr)
by A62, Th14;
consider rs being
FinSequence of the
carrier of
L such that A64:
pqrb . b = Sum rs
and A65:
len rs = len (decomp b)
and A66:
for
k being
Element of
NAT st
k in dom rs holds
ex
b1,
b2 being
bag of
n st
(
(decomp b) /. k = <*b1,b2*> &
rs /. k = (p . b1) * ((q *' r) . b2) )
by Def10;
now ( len (Sum vdbr) = len rs & ( for k being Nat st 1 <= k & k <= len rs holds
(Sum vdbr) . k = rs . k ) )set f =
Sum vdbr;
A67:
dom vdbr =
(dom ((dom dbr) --> v)) /\ (dom dbr)
by A61, PBOOLE:def 19
.=
(dom dbr) /\ (dom dbr)
.=
dom dbr
;
A68:
dom (Sum vdbr) = dom vdbr
by Th2;
hence
len (Sum vdbr) = len rs
by A65, A12, A67, FINSEQ_3:29;
for k being Nat st 1 <= k & k <= len rs holds
(Sum vdbr) . k = rs . klet k be
Nat;
( 1 <= k & k <= len rs implies (Sum vdbr) . k = rs . k )assume A69:
( 1
<= k &
k <= len rs )
;
(Sum vdbr) . k = rs . kA70:
k in dom (Sum vdbr)
by A65, A12, A68, A67, A69, FINSEQ_3:25;
then A71:
(Sum vdbr) /. k = (Sum vdbr) . k
by PARTFUN1:def 6;
set dbrk =
dbr . k;
set dbk2 =
((decomp b) /. k) /. 1;
set ddbk1 =
decomp (((decomp b) /. k) /. 2);
A72:
k in dom vdbr
by A65, A12, A67, A69, FINSEQ_3:25;
then A73:
dbr . k = ((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) ^^ (decomp (((decomp b) /. k) /. 2))
by A13, A67;
then A74:
dom (dbr . k) =
(dom (decomp (((decomp b) /. k) /. 2))) /\ (dom ((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>))
by PRE_POLY:def 4
.=
(dom (decomp (((decomp b) /. k) /. 2))) /\ (Seg (len (decomp (((decomp b) /. k) /. 2))))
.=
(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 A65, A12, A69, FINSEQ_3:25;
then
dbr . k in rng dbr
by FUNCT_1:def 3;
then A75:
dbr . k is
Element of
(3 -tuples_on (Bags n)) *
;
set vdbrk =
v * (dbr . k);
A76:
dom (decomp (((decomp b) /. k) /. 2)) = Seg (len (decomp (((decomp b) /. k) /. 2)))
by FINSEQ_1:def 3;
reconsider dbrk =
dbr . k as
FinSequence of 3
-tuples_on (Bags n) by A75;
rng dbrk c= 3
-tuples_on (Bags n)
;
then A77:
dom (v * (dbr . k)) = dom dbrk
by A27, RELAT_1:27;
then A78:
dom (v * (dbr . k)) = Seg (len (decomp (((decomp b) /. k) /. 2)))
by A74, FINSEQ_1:def 3;
A79:
dom rs = dom (Sum vdbr)
by A65, A12, A68, A67, FINSEQ_3:29;
then A80:
rs /. k = rs . k
by A70, PARTFUN1:def 6;
consider b1,
b2 being
bag of
n such that A81:
(decomp b) /. k = <*b1,b2*>
and A82:
rs /. k = (p . b1) * ((q *' r) . b2)
by A66, A79, A70;
reconsider b19 =
b1 as
Element of
Bags n by PRE_POLY:def 12;
consider qrs being
FinSequence of the
carrier of
L such that A83:
(q *' r) . b2 = Sum qrs
and A84:
len qrs = len (decomp b2)
and A85:
for
i being
Element of
NAT st
i in dom qrs holds
ex
b11,
b12 being
bag of
n st
(
(decomp b2) /. i = <*b11,b12*> &
qrs /. i = (q . b11) * (r . b12) )
by Def10;
A86:
dom qrs = dom ((p . b1) * qrs)
by Def1;
then A87:
len qrs = len ((p . b1) * qrs)
by FINSEQ_3:29;
A88:
len <*b1,b2*> = 2
by FINSEQ_1:44;
then
1
in dom <*b1,b2*>
by FINSEQ_3:25;
then A89:
((decomp b) /. k) /. 1 =
<*b1,b2*> . 1
by A81, PARTFUN1:def 6
.=
b1
;
reconsider vdbrk =
v * (dbr . k) as
FinSequence by A78, FINSEQ_1:def 2;
A90:
Sum ((p . b1) * qrs) = (p . b1) * (Sum qrs)
by Th12;
2
in dom <*b1,b2*>
by A88, FINSEQ_3:25;
then A91:
((decomp b) /. k) /. 2 =
<*b1,b2*> . 2
by A81, PARTFUN1:def 6
.=
b2
;
then A92:
dom vdbrk = dom ((p . b1) * qrs)
by A84, A74, A77, A86, FINSEQ_3:29;
A93:
now for i being Nat st 1 <= i & i <= len ((p . b1) * qrs) holds
(v * (dbr . k)) . i = ((p . b1) * qrs) . ilet i be
Nat;
( 1 <= i & i <= len ((p . b1) * qrs) implies (v * (dbr . k)) . i = ((p . b1) * qrs) . i )reconsider i9 =
i as
Element of
NAT by ORDINAL1:def 12;
assume A94:
( 1
<= i &
i <= len ((p . b1) * qrs) )
;
(v * (dbr . k)) . i = ((p . b1) * qrs) . ithen A95:
i in dom qrs
by A86, FINSEQ_3:25;
A96:
i in dom dbrk
by A84, A91, A74, A87, A94, FINSEQ_3:25;
then consider b11,
b12 being
bag of
n such that A97:
(decomp b2) /. i = <*b11,b12*>
and A98:
qrs /. i = (q . b11) * (r . b12)
by A85, A77, A86, A92;
(
((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) . i9 = <*(((decomp b) /. k) /. 1)*> &
(decomp b2) /. i = (decomp b2) . i )
by A91, A74, A76, A96, FUNCOP_1:7, PARTFUN1:def 6;
then A99:
dbrk . i =
<*b1*> ^ <*b11,b12*>
by A89, A91, A73, A96, A97, PRE_POLY:def 4
.=
<*b1,b11,b12*>
by FINSEQ_1:43
;
reconsider b119 =
b11,
b129 =
b12 as
Element of
Bags n by PRE_POLY:def 12;
reconsider B =
<*b19,b119,b129*> as
Element of 3
-tuples_on (Bags n) by FINSEQ_2:104;
thus (v * (dbr . k)) . i =
v . (dbrk . i)
by A77, A96, FUNCT_1:12
.=
((p . (B /. 1)) * (q . (B /. 2))) * (r . (B /. 3))
by A11, A99
.=
((p . b1) * (q . (B /. 2))) * (r . (B /. 3))
by FINSEQ_4:18
.=
((p . b1) * (q . b11)) * (r . (B /. 3))
by FINSEQ_4:18
.=
((p . b1) * (q . b11)) * (r . b12)
by FINSEQ_4:18
.=
(p . b1) * (qrs /. i)
by A98, GROUP_1:def 3
.=
((p . b1) * qrs) /. i
by A95, Def1
.=
((p . b1) * qrs) . i
by A86, A95, PARTFUN1:def 6
;
verum end;
len vdbrk = len ((p . b1) * qrs)
by A84, A91, A74, A77, A87, FINSEQ_3:29;
then A100:
vdbrk = (p . b1) * qrs
by A93, FINSEQ_1:14;
vdbr /. k =
vdbr . k
by A72, PARTFUN1:def 6
.=
(((dom dbr) --> v) . k) * (dbr . k)
by A61, A72, PBOOLE:def 19
.=
(p . b1) * qrs
by A67, A72, A100, FUNCOP_1:7
;
hence
(Sum vdbr) . k = rs . k
by A70, A82, A83, A90, A80, A71, MATRLIN:def 6;
verum end; then A101:
Sum vdbr = rs
by FINSEQ_1:14;
dom dbl = dom (decomp b)
by A1, FINSEQ_3:29;
then consider P being
Permutation of
(dom (FlattenSeq dbl)) such that A102:
FlattenSeq dbr = (FlattenSeq dbl) * P
by A2, A13, A24, PRE_POLY:74;
rng (FlattenSeq dbl) c= 3
-tuples_on (Bags n)
;
then
dom vfdbl = dom (FlattenSeq dbl)
by A27, RELAT_1:27;
then reconsider P =
P as
Permutation of
(dom vfdbl) ;
A103:
vfdbr = vfdbl * P
by A102, RELAT_1:36;
Sum vfdbl = Sum (Sum vdbl)
by A26, Th14;
hence
pqra . b = pqrb . b
by A21, A64, A60, A63, A101, A103, RLVECT_2:7;
verum end;
hence
(p *' q) *' r = p *' (q *' r)
; verum