:: Binary Operations Applied to Finite Sequences
:: by Czes{\l}aw Byli\'nski
::
:: Received May 4, 1990
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, SUBSET_1, FUNCT_1, PARTFUN1, RELAT_1, ZFMISC_1,
FUNCOP_1, TARSKI, NAT_1, FINSEQ_1, FINSEQ_2, ORDINAL4, ARYTM_3, CARD_1,
BINOP_1, SETWISEO, FINSEQOP, ORDINAL1, PBOOLE;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
NAT_1, RELAT_1, EQREL_1, FUNCT_1, FINSEQ_1, RELSET_1, PARTFUN1,
PBOOLE, FUNCT_2, BINOP_1, FUNCT_3, FUNCOP_1, FINSEQ_2, SETWISEO;
constructors PARTFUN1, BINOP_1, FUNCT_3, FUNCOP_1, SETWISEO, NAT_1, FINSEQ_2,
RELSET_1, EQREL_1, NUMBERS, PBOOLE;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, NAT_1,
FINSEQ_2, ORDINAL1, FINSEQ_1, CARD_1, RELSET_1;
requirements NUMERALS, BOOLE, SUBSET;
definitions BINOP_1;
equalities BINOP_1, FUNCOP_1, FINSEQ_2;
expansions BINOP_1;
theorems ZFMISC_1, FUNCT_1, FUNCT_2, FUNCOP_1, FINSEQ_1, BINOP_1, SETWISEO,
FINSEQ_2, FUNCT_3, RELAT_1, XBOOLE_0, CARD_1, TARSKI, PARTFUN1;
schemes NAT_1, FINSEQ_2;
begin
reserve x,y for set;
reserve C,C9,D,D9,E for non empty set;
reserve c for Element of C;
reserve c9 for Element of C9;
reserve d,d1,d2,d3,d4,e for Element of D;
reserve d9 for Element of D9;
:: Auxiliary theorems
theorem Th1:
for f being Function holds <:{},f:> = {} & <:f,{}:> = {}
proof
let f be Function;
dom <:{},f:> = dom {} /\ dom f & dom <:f,{}:> = dom f /\ dom {} by
FUNCT_3:def 7;
hence thesis;
end;
theorem
for f being Function holds [:{},f:] = {} & [:f,{}:] = {}
proof
let f be Function;
dom [:{},f:] = [:dom {},dom f:] & dom [:f,{}:] = [:dom f,dom {}:] by
FUNCT_3:def 8;
hence thesis by ZFMISC_1:90;
end;
theorem Th3:
for F,f being Function holds F.:({},f) = {} & F.:(f,{}) = {}
proof
let F,f be Function;
F.:({},f) = F*{} by Th1;
hence thesis by Th1;
end;
theorem
for F being Function holds F[:]({},x) = {}
proof
let F be Function;
F[:]({},x) = F.:({}, dom {} --> x);
hence thesis by Th3;
end;
theorem
for F being Function holds F[;](x,{}) = {}
proof
let F be Function;
F[;](x,{}) = F.:(dom {} --> x, {});
hence thesis by Th3;
end;
theorem Th6:
for X being set, x1,x2 being set holds <:X-->x1,X-->x2:> = X -->[x1,x2]
proof
let X be set, x1,x2 be set;
set f = X-->x1, g = X-->x2;
set fg = <:f,g:>;
now
per cases;
suppose
A1: X = {};
thus thesis by A1;
end;
suppose
A2: X <> {};
rng fg c= [:{x1},{x2}:];
then
A3: rng fg c= {[x1,x2]} by ZFMISC_1:29;
set x = the Element of X;
A4: dom f = X & dom g = X;
then
A5: dom fg = X by FUNCT_3:50;
f.x = x1 & g.x = x2 by A2,FUNCOP_1:7;
then fg.x = [x1,x2] by A2,A4,FUNCT_3:49;
then [x1,x2] in rng fg by A2,A5,FUNCT_1:def 3;
then {[x1,x2]} c= rng fg by ZFMISC_1:31;
then rng fg = {[x1,x2]} by A3,XBOOLE_0:def 10;
hence thesis by A5,FUNCOP_1:9;
end;
end;
hence thesis;
end;
theorem Th7:
for F being Function, X being set, x1,x2 being set st
[x1,x2] in dom F holds F.:(X-->x1,X-->x2) = X --> F.(x1,x2)
proof
let F be Function, X be set, x1,x2 be set such that
A1: [x1,x2] in dom F;
set f = X-->x1, g = X-->x2;
thus F.:(f,g) = F*(X-->[x1,x2]) by Th6
.= X --> F.(x1,x2) by A1,FUNCOP_1:17;
end;
reserve i,j for natural Number;
reserve F for Function of [:D,D9:],E;
reserve p,q for FinSequence of D,
p9,q9 for FinSequence of D9;
definition
let D,D9,E,F,p,p9;
redefine func F.:(p,p9) -> FinSequence of E; :: redefines .: (FUNCOP_1, definition)
coherence by FINSEQ_2:70;
end;
definition
let D,D9,E,F,p,d9;
redefine func F[:](p,d9) -> FinSequence of E; :: redefines [:] (FUNCOP_1, definition)
coherence by FINSEQ_2:83;
end;
definition
let D,D9,E,F,d,p9;
redefine func F[;](d,p9) -> FinSequence of E; :: redefines [;] (FUNCOP_1, definition)
coherence by FINSEQ_2:77;
end;
reserve f,f9 for Function of C,D,
h for Function of D,E;
definition
let D,E be set, p be FinSequence of D, h be Function of D,E;
redefine func h*p -> FinSequence of E; :: redefines * (FUNCT_1, synonym) → * (RELAT_1, synonym) → (#) (RELAT_1, definition)
coherence by FINSEQ_2:32;
end;
theorem Th8:
h*(p^<*d*>) = (h*p)^<*h.d*>
proof
set q = h*(p^<*d*>);
set r = (h*p)^<*h.d*>;
set i = len p + 1;
A1: len q = len(p^<*d*>) by FINSEQ_2:33;
A2: len(h*p) = len p by FINSEQ_2:33;
len(p^<*d*>) = i by FINSEQ_2:16;
then
A3: dom q = Seg i by A1,FINSEQ_1:def 3;
A4: now
let j be Nat;
A5: Seg len p = dom p by FINSEQ_1:def 3;
A6: Seg len(h*p) = dom(h*p) by FINSEQ_1:def 3;
assume
A7: j in dom q;
now
per cases by A3,A7,A5,FINSEQ_2:7;
suppose
A8: j in dom p;
hence h.((p^<*d*>).j) = h.(p.j) by FINSEQ_1:def 7
.= (h*p).j by A2,A5,A6,A8,FUNCT_1:12
.= r.j by A2,A5,A6,A8,FINSEQ_1:def 7;
end;
suppose
A9: j = i;
hence h.((p^<*d*>).j) = h.d by FINSEQ_1:42
.= r.j by A2,A9,FINSEQ_1:42;
end;
end;
hence q.j = r.j by A7,FUNCT_1:12;
end;
len r = len(h*p)+1 by FINSEQ_2:16;
hence thesis by A1,A2,A4,FINSEQ_2:9,16;
end;
theorem
h*(p^q) = (h*p)^(h*q)
proof
defpred P[FinSequence of D] means h*(p^$1) = (h*p)^(h*$1);
A1: for q,d st P[q] holds P[q^<*d*>]
proof
let q,d such that
A2: h*(p^q) = (h*p)^(h*q);
thus h*(p^(q^<*d*>)) = h*((p^q)^<*d*>) by FINSEQ_1:32
.= (h*(p^q))^<*h.d*> by Th8
.= (h*p)^((h*q)^<*h.d*>) by A2,FINSEQ_1:32
.= (h*p)^(h*(q^<*d*>)) by Th8;
end;
h*(p^<*>D) = h*p by FINSEQ_1:34
.= (h*p)^(h*(<*>D)) by FINSEQ_1:34;
then
A3: P[<*>D];
for q holds P[q] from FINSEQ_2:sch 2(A3,A1);
hence thesis;
end;
reserve T,T1,T2,T3 for Tuple of i,D;
reserve T9 for Tuple of i, D9;
reserve S for Tuple of j, D;
reserve S9 for Tuple of j, D9;
Lm1: for T being Tuple of 0, D holds F.:(T,T9) = <*>E
proof
let T be Tuple of 0, D;
T = <*>D;
hence thesis by FINSEQ_2:73;
end;
Lm2: for T9 being Tuple of 0, D9 holds F[;](d,T9) = <*>E
proof
let T9 be Tuple of 0, D9;
T9 = <*>D9;
hence thesis by FINSEQ_2:79;
end;
Lm3: for T being Tuple of 0, D holds F[:](T,d9) = <*>E
proof
let T be Tuple of 0, D;
T = <*>D;
hence thesis by FINSEQ_2:85;
end;
theorem Th10:
F.:(T^<*d*>,T9^<*d9*>) = (F.:(T,T9))^<*F.(d,d9)*>
proof
set p = T^<*d*>, q = T9^<*d9*>, pq = F.:(T,T9);
set r = F.:(p,q), s = pq^<*F.(d,d9)*>;
A1: len T9 = i by CARD_1:def 7;
then
A2: len q = i+1 by FINSEQ_2:16;
A3: len T = i by CARD_1:def 7;
then
A4: len pq = i by A1,FINSEQ_2:72;
len p = i+1 by A3,FINSEQ_2:16;
then
A5: len r = i+1 by A2,FINSEQ_2:72;
then
A6: dom r = Seg(i+1) by FINSEQ_1:def 3;
A7: now
let j be Nat;
assume
A8: j in dom r;
now
per cases by A6,A8,FINSEQ_2:7;
suppose
A9: j in Seg i;
Seg len T = dom T by FINSEQ_1:def 3;
then
A10: p.j = T.j by A3,A9,FINSEQ_1:def 7;
A11: Seg len pq = dom pq by FINSEQ_1:def 3;
Seg len T9 = dom T9 by FINSEQ_1:def 3;
then
A12: q.j = T9.j by A1,A9,FINSEQ_1:def 7;
j in dom pq by A4,A9,FINSEQ_1:def 3;
hence F.(p.j,q.j) = pq.j by A10,A12,FUNCOP_1:22
.= s.j by A4,A9,A11,FINSEQ_1:def 7;
end;
suppose
A13: j = i+1;
then p.j = d & q.j = d9 by A3,A1,FINSEQ_1:42;
hence F.(p.j,q.j) = s.j by A4,A13,FINSEQ_1:42;
end;
end;
hence r.j = s.j by A8,FUNCOP_1:22;
end;
len s = len pq + 1 by FINSEQ_2:16;
hence thesis by A5,A4,A7,FINSEQ_2:9;
end;
theorem
F.:(T^S,T9^S9) = (F.:(T,T9))^(F.:(S,S9))
proof
A0: i is Nat & j is Nat by TARSKI:1;
defpred P[Nat] means for S being Tuple of $1, D, S9 being Tuple
of $1, D9 holds F.:(T^S,T9^S9) = (F.:(T,T9))^(F.:(S,S9));
now
let j such that
A1: for S,S9 holds F.:(T^S,T9^S9) = (F.:(T,T9))^(F.:(S,S9));
let S be Tuple of j+1, D;
let S9 be Tuple of j+1, D9;
consider S1 being Element of j-tuples_on D, d such that
A2: S = S1^<*d*> by FINSEQ_2:117;
A3: T^S = T^S1^<*d*> by A2,FINSEQ_1:32;
reconsider S1 as Tuple of j, D;
consider S19 being Element of j-tuples_on D9, d9 such that
A4: S9 = S19^<*d9*> by FINSEQ_2:117;
A5: T9^S9 = T9^S19^<*d9*> by A4,FINSEQ_1:32;
reconsider S19 as Tuple of j, D9;
thus F.:(T^S,T9^S9) = (F.:(T^S1,T9^S19))^<*F.(d,d9)*> by A3,A5,Th10
.= (F.:(T,T9))^(F.:(S1,S19))^<*F.(d,d9)*> by A1
.= (F.:(T,T9))^((F.:(S1,S19))^<*F.(d,d9)*>) by FINSEQ_1:32
.= (F.:(T,T9))^(F.:(S,S9)) by A2,A4,Th10;
end;
then
A6: for j be Nat st P[j] holds P[j+1];
now
let S be Tuple of 0, D;
let S9 be Tuple of 0, D9;
S = <*>D;
then
A7: F.:(S,S9) = <*>E by FINSEQ_2:73;
T^S = T & T9^S9 = T9 by FINSEQ_2:95;
hence F.:(T^S,T9^S9) = (F.:(T,T9))^(F.:(S,S9)) by A7,FINSEQ_1:34;
end;
then
A8: P[0];
for j be Nat holds P[j] from NAT_1:sch 2(A8,A6);
hence thesis by A0;
end;
theorem Th12:
F[;](d,p9^<*d9*>) = (F[;](d,p9))^<*F.(d,d9)*>
proof
set pd = p9^<*d9*>, q = F[;](d,p9);
set r = F[;](d,pd), s = q^<*F.(d,d9)*>;
set i = len p9;
A1: len q = i by FINSEQ_2:78;
len pd = i + 1 by FINSEQ_2:16;
then
A2: len r = i + 1 by FINSEQ_2:78;
then
A3: dom r = Seg(i+1) by FINSEQ_1:def 3;
A4: now
let j be Nat;
assume
A5: j in dom r;
now
per cases by A3,A5,FINSEQ_2:7;
suppose
A6: j in Seg i;
then
A7: j in dom q by A1,FINSEQ_1:def 3;
A8: Seg len q = dom q by FINSEQ_1:def 3;
Seg len p9 = dom p9 by FINSEQ_1:def 3;
hence F.(d,pd.j) = F.(d,p9.j) by A6,FINSEQ_1:def 7
.= q.j by A7,FUNCOP_1:32
.= s.j by A1,A6,A8,FINSEQ_1:def 7;
end;
suppose
A9: j = i+1;
hence F.(d,pd.j) = F.(d,d9) by FINSEQ_1:42
.= s.j by A1,A9,FINSEQ_1:42;
end;
end;
hence r.j = s.j by A5,FUNCOP_1:32;
end;
len s = len q + 1 by FINSEQ_2:16;
hence thesis by A1,A2,A4,FINSEQ_2:9;
end;
theorem
F[;](d,p9^q9) = (F[;](d,p9))^(F[;](d,q9))
proof
defpred P[FinSequence of D9] means F[;](d,p9^($1)) = (F[;](d,p9))^(F[;](d,$1
));
A1: for q9,d9 st P[q9] holds P[q9^<*d9*>]
proof
let q9,d9 such that
A2: F[;](d,p9^q9) = (F[;](d,p9))^(F[;](d,q9));
thus F[;](d,p9^(q9^<*d9*>)) = F[;](d,(p9^q9)^<*d9*>) by FINSEQ_1:32
.= (F[;](d,p9^q9))^<*F.(d,d9)*> by Th12
.= (F[;](d,p9))^((F[;](d,q9))^<*F.(d,d9)*>) by A2,FINSEQ_1:32
.= (F[;](d,p9))^(F[;](d,q9^<*d9*>)) by Th12;
end;
F[;](d,p9^(<*>D9)) = F[;](d,p9) by FINSEQ_1:34
.= (F[;](d,p9))^(<*>E) by FINSEQ_1:34
.= (F[;](d,p9))^(F[;](d,<*>D9)) by FINSEQ_2:79;
then
A3: P[<*>D9];
for q9 holds P[q9] from FINSEQ_2:sch 2(A3,A1);
hence thesis;
end;
theorem Th14:
F[:](p^<*d*>,d9) = (F[:](p,d9))^<*F.(d,d9)*>
proof
set pd = p^<*d*>, q = F[:](p,d9);
set r = F[:](pd,d9), s = q^<*F.(d,d9)*>;
set i = len p;
A1: len q = i by FINSEQ_2:84;
len pd = i + 1 by FINSEQ_2:16;
then
A2: len r = i + 1 by FINSEQ_2:84;
then
A3: dom r = Seg(i+1) by FINSEQ_1:def 3;
A4: now
let j be Nat;
assume
A5: j in dom r;
now
per cases by A3,A5,FINSEQ_2:7;
suppose
A6: j in Seg i;
then
A7: j in dom q by A1,FINSEQ_1:def 3;
Seg len p = dom p by FINSEQ_1:def 3;
hence F.(pd.j,d9) = F.(p.j,d9) by A6,FINSEQ_1:def 7
.= q.j by A7,FUNCOP_1:27
.= s.j by A7,FINSEQ_1:def 7;
end;
suppose
A8: j = i+1;
hence F.(pd.j,d9) = F.(d,d9) by FINSEQ_1:42
.= s.j by A1,A8,FINSEQ_1:42;
end;
end;
hence r.j = s.j by A5,FUNCOP_1:27;
end;
len s = len q + 1 by FINSEQ_2:16;
hence thesis by A1,A2,A4,FINSEQ_2:9;
end;
theorem
F[:](p^q,d9) = (F[:](p,d9))^(F[:](q,d9))
proof
defpred P[FinSequence of D] means F[:](p^($1),d9) = (F[:](p,d9))^(F[:]($1,d9
));
A1: for q,d st P[q] holds P[q^<*d*>]
proof
let q,d such that
A2: F[:](p^q,d9) = (F[:](p,d9))^(F[:](q,d9));
thus F[:](p^(q^<*d*>),d9) = F[:]((p^q)^<*d*>,d9) by FINSEQ_1:32
.= (F[:](p^q,d9))^<*F.(d,d9)*> by Th14
.= (F[:](p,d9))^((F[:](q,d9))^<*F.(d,d9)*>) by A2,FINSEQ_1:32
.= (F[:](p,d9))^(F[:](q^<*d*>,d9)) by Th14;
end;
F[:](p^(<*>D),d9) = F[:](p,d9) by FINSEQ_1:34
.= (F[:](p,d9))^(<*>E) by FINSEQ_1:34
.= (F[:](p,d9))^(F[:](<*>D,d9)) by FINSEQ_2:85;
then
A3: P[<*>D];
for q holds P[q] from FINSEQ_2:sch 2(A3,A1);
hence thesis;
end;
theorem
for h being Function of D,E holds h*(i|->d) = i|->(h.d)
proof
let h be Function of D,E;
d in D;
then d in dom h by FUNCT_2:def 1;
hence thesis by FUNCOP_1:17;
end;
theorem Th17:
F.:(i|->d,i|->d9) = i |-> (F.(d,d9))
proof
[d,d9] in [:D,D9:] by ZFMISC_1:def 2;
then [d,d9] in dom F by FUNCT_2:def 1;
hence thesis by Th7;
end;
theorem
F[;](d,i|->d9) = i |-> (F.(d,d9))
proof
thus F[;](d,i|->d9) = F.:(i |->d,i|->d9)
.= i |-> (F.(d,d9)) by Th17;
end;
theorem
F[:](i|->d,d9) = i |-> (F.(d,d9))
proof
thus F[:](i|->d,d9) = F.:(i |->d,i|->d9)
.= i |-> (F.(d,d9)) by Th17;
end;
theorem
F.:(i|->d,T9) = F[;](d,T9)
proof
dom T9 = Seg len T9 by FINSEQ_1:def 3
.= Seg i by CARD_1:def 7;
hence thesis;
end;
theorem
F.:(T,i|->d) = F[:](T,d)
proof
dom T = Seg len T by FINSEQ_1:def 3
.= Seg i by CARD_1:def 7;
hence thesis;
end;
theorem
F[;](d,T9) = F[;](d,id D9)*T9
proof
rng T9 c= D9;
hence F[;](d,T9) = F[;](d,(id D9)*T9) by RELAT_1:53
.= F[;](d,(id D9))*T9 by FUNCOP_1:34;
end;
theorem
F[:](T,d) = F[:](id D,d)*T
proof
rng T c= D;
hence F[:](T,d) = F[:]((id D)*T,d) by RELAT_1:53
.= F[:]((id D),d)*T by FUNCOP_1:29;
end;
:: Binary Operations
reserve F,G for BinOp of D;
reserve u for UnOp of D;
reserve H for BinOp of E;
Lm4: T is Function of Seg i,D
proof
len T = i by CARD_1:def 7;
then Seg i = dom T by FINSEQ_1:def 3;
hence thesis by FINSEQ_2:26;
end;
theorem Th24:
F is associative implies F[;](d,id D)*(F.:(f,f9)) = F.:(F[;](d, id D)*f,f9)
proof
assume
A1: F is associative;
now
let c;
thus (F[;](d,id D)*(F.:(f,f9))).c = (F[;](d,id D)).((F.:(f,f9)).c) by
FUNCT_2:15
.= (F[;](d,id D)).(F.(f.c,f9.c)) by FUNCOP_1:37
.= F.(d,(id D).(F.(f.c,f9.c))) by FUNCOP_1:53
.= F.(d,F.(f.c,f9.c))
.= F.(F.(d,f.c),f9.c) by A1
.= F.((F[;](d,f)).c,f9.c) by FUNCOP_1:53
.= F.(((F[;](d,id D))*f).c,f9.c) by FUNCOP_1:55
.= (F.:(F[;](d,id D)*f,f9)).c by FUNCOP_1:37;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th25:
F is associative implies F[:](id D,d)*(F.:(f,f9)) = F.:(f,F[:](id D,d)*f9)
proof
assume
A1: F is associative;
now
let c;
thus (F[:](id D,d)*(F.:(f,f9))).c = (F[:](id D,d)).((F.:(f,f9)).c) by
FUNCT_2:15
.= (F[:](id D,d)).(F.(f.c,f9.c)) by FUNCOP_1:37
.= F.((id D).(F.(f.c,f9.c)),d) by FUNCOP_1:48
.= F.(F.(f.c,f9.c),d)
.= F.(f.c,F.(f9.c,d)) by A1
.= F.(f.c,(F[:](f9,d)).c) by FUNCOP_1:48
.= F.(f.c,((F[:](id D,d))*f9).c) by FUNCOP_1:50
.= (F.:(f,F[:](id D,d)*f9)).c by FUNCOP_1:37;
end;
hence thesis by FUNCT_2:63;
end;
theorem
F is associative implies
F[;](d,id D)*(F.:(T1,T2)) = F.:(F[;](d,id D)*T1,T2 )
proof
assume
A1: F is associative;
per cases;
suppose
A2: i = 0;
then F.:(T1,T2) = <*>D by Lm1;
then
A3: F[;](d,id D)*(F.:(T1,T2)) = <*>D;
T2 = <*>D by A2;
hence thesis by A3,FINSEQ_2:73;
end;
suppose
i <> 0;
then reconsider C = Seg i as non empty set;
T1 is Function of C,D & T2 is Function of C,D by Lm4;
hence thesis by A1,Th24;
end;
end;
theorem
F is associative implies
F[:](id D,d)*(F.:(T1,T2)) = F.:(T1,F[:](id D,d)*T2 )
proof
assume
A1: F is associative;
per cases;
suppose
A2: i = 0;
then F.:(T1,T2) = <*>D by Lm1;
then
A3: F[:](id D,d)*(F.:(T1,T2)) = <*>D;
T1 = <*>D by A2;
hence thesis by A3,FINSEQ_2:73;
end;
suppose
i <> 0;
then reconsider C = Seg i as non empty set;
T1 is Function of C,D & T2 is Function of C,D by Lm4;
hence thesis by A1,Th25;
end;
end;
theorem
F is associative implies F.:(F.:(T1,T2),T3) = F.:(T1,F.:(T2,T3))
proof
assume
A1: F is associative;
per cases;
suppose
A2: i = 0;
then F.:(T1,T2) = <*>D by Lm1;
then
A3: F.:(F.:(T1,T2),T3) = <*>D by FINSEQ_2:73;
F.:(T2,T3) = <*>D by A2,Lm1;
hence thesis by A3,FINSEQ_2:73;
end;
suppose
i <> 0;
then reconsider C = Seg i as non empty set;
A4: T3 is Function of C,D by Lm4;
T1 is Function of C,D & T2 is Function of C,D by Lm4;
hence thesis by A1,A4,FUNCOP_1:61;
end;
end;
theorem
F is associative implies F[:](F[;](d1,T),d2) = F[;](d1,F[:](T,d2))
proof
assume
A1: F is associative;
per cases;
suppose
A2: i = 0;
then F[;](d1,T) = <*>D by Lm2;
then
A3: F[:](F[;](d1,T),d2) = <*>D by FINSEQ_2:85;
F[:](T,d2) = <*>D by A2,Lm3;
hence thesis by A3,FINSEQ_2:79;
end;
suppose
i <> 0;
then reconsider C = Seg i as non empty set;
T is Function of C,D by Lm4;
hence thesis by A1,FUNCOP_1:59;
end;
end;
theorem
F is associative implies F.:(F[:](T1,d),T2) = F.:(T1,F[;](d,T2))
proof
assume
A1: F is associative;
per cases;
suppose
A2: i = 0;
then F[:](T1,d) = <*>D by Lm3;
then
A3: F.:(F[:](T1,d),T2) = <*>D by FINSEQ_2:73;
F[;](d,T2) = <*>D by A2,Lm2;
hence thesis by A3,FINSEQ_2:73;
end;
suppose
i <> 0;
then reconsider C = Seg i as non empty set;
T1 is Function of C,D & T2 is Function of C,D by Lm4;
hence thesis by A1,FUNCOP_1:60;
end;
end;
theorem
F is associative implies F[;](F.(d1,d2),T) = F[;](d1,F[;](d2,T))
proof
assume
A1: F is associative;
per cases;
suppose
i = 0;
then T = <*>D & F[;](d2,T) = <*>D by Lm2;
hence thesis;
end;
suppose
i <> 0;
then reconsider C = Seg i as non empty set;
T is Function of C,D by Lm4;
hence thesis by A1,FUNCOP_1:62;
end;
end;
theorem
F is associative implies F[:](T,F.(d1,d2)) = F[:](F[:](T,d1),d2)
proof
assume
A1: F is associative;
per cases;
suppose
i = 0;
then T = <*>D & F[:](T,d1) = <*>D by Lm3;
hence thesis;
end;
suppose
i <> 0;
then reconsider C = Seg i as non empty set;
T is Function of C,D by Lm4;
hence thesis by A1,FUNCOP_1:63;
end;
end;
theorem
F is commutative implies F.:(T1,T2) = F.:(T2,T1)
proof
assume
A1: F is commutative;
per cases;
suppose
A2: i = 0;
then F.:(T1,T2) = <*>D by Lm1;
hence thesis by A2,Lm1;
end;
suppose
i <> 0;
then reconsider C = Seg i as non empty set;
T1 is Function of C,D & T2 is Function of C,D by Lm4;
hence thesis by A1,FUNCOP_1:65;
end;
end;
theorem
F is commutative implies F[;](d,T) = F[:](T,d)
proof
assume
A1: F is commutative;
per cases;
suppose
A2: i = 0;
then F[;](d,T) = <*>D by Lm2;
hence thesis by A2,Lm3;
end;
suppose
i <> 0;
then reconsider C = Seg i as non empty set;
T is Function of C,D by Lm4;
hence thesis by A1,FUNCOP_1:64;
end;
end;
theorem Th35:
F is_distributive_wrt G implies
F[;](G.(d1,d2),f) = G.:(F[;](d1,f),F[;] (d2,f))
proof
assume
A1: F is_distributive_wrt G;
now
let c;
thus (F[;](G.(d1,d2),f)).c = F.(G.(d1,d2),f.c) by FUNCOP_1:53
.= G.(F.(d1,f.c),F.(d2,f.c)) by A1,BINOP_1:11
.= G.(F[;](d1,f).c,F.(d2,f.c)) by FUNCOP_1:53
.= G.((F[;](d1,f)).c,(F[;](d2,f)).c) by FUNCOP_1:53
.= (G.:(F[;](d1,f),F[;](d2,f))).c by FUNCOP_1:37;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th36:
F is_distributive_wrt G implies
F[:](f,G.(d1,d2)) = G.:(F[:](f,d1),F[:] (f,d2))
proof
assume
A1: F is_distributive_wrt G;
now
let c;
thus (F[:](f,G.(d1,d2))).c = F.(f.c,G.(d1,d2)) by FUNCOP_1:48
.= G.(F.(f.c,d1),F.(f.c,d2)) by A1,BINOP_1:11
.= G.(F[:](f,d1).c,F.(f.c,d2)) by FUNCOP_1:48
.= G.((F[:](f,d1)).c,(F[:](f,d2)).c) by FUNCOP_1:48
.= (G.:(F[:](f,d1),F[:](f,d2))).c by FUNCOP_1:37;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th37:
(for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2)) implies
h*(F.:(f,f9)) = H.:(h*f,h*f9)
proof
assume
A1: for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2);
now
let c;
thus (h*(F.:(f,f9))).c = h.((F.:(f,f9)).c) by FUNCT_2:15
.= h.(F.(f.c,f9.c)) by FUNCOP_1:37
.= H.(h.(f.c),h.(f9.c)) by A1
.= H.((h*f).c,h.(f9.c)) by FUNCT_2:15
.= H.((h*f).c,(h*f9).c) by FUNCT_2:15
.= (H.:(h*f,h*f9)).c by FUNCOP_1:37;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th38:
(for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2)) implies
h*(F[;](d,f)) = H[;](h.d,h*f)
proof
assume
A1: for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2);
reconsider g = C --> d as Function of C,D;
A2: dom h = D & dom(h*f) = C by FUNCT_2:def 1;
thus h*(F[;](d,f)) = h*(F.:(g,f)) by FUNCT_2:def 1
.= H.:(h*g,h*f) by A1,Th37
.= H[;](h.d,h*f) by A2,FUNCOP_1:17;
end;
theorem Th39:
(for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2)) implies
h*(F[:](f,d)) = H[:](h*f,h.d)
proof
assume
A1: for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2);
reconsider g = C --> d as Function of C,D;
A2: dom h = D & dom(h*f) = C by FUNCT_2:def 1;
thus h*(F[:](f,d)) = h*(F.:(f,g)) by FUNCT_2:def 1
.= H.:(h*f,h*g) by A1,Th37
.= H[:](h*f,h.d) by A2,FUNCOP_1:17;
end;
theorem
u is_distributive_wrt F implies u*(F.:(f,f9)) = F.:(u*f,u*f9) by Th37;
theorem
u is_distributive_wrt F implies u*(F[;](d,f)) = F[;](u.d,u*f) by Th38;
theorem
u is_distributive_wrt F implies u*(F[:](f,d)) = F[:](u*f,u.d) by Th39;
theorem Th43:
F is having_a_unity implies F.:(C-->the_unity_wrt F,f) = f &
F.:(f,C-->the_unity_wrt F) = f
proof
set e = the_unity_wrt F;
reconsider g = C-->e as Function of C,D;
assume
A1: F is having_a_unity;
now
let c;
thus (F.:(g,f)).c = F.(g.c,f.c) by FUNCOP_1:37
.= F.(e,f.c)
.= f.c by A1,SETWISEO:15;
end;
hence F.:(C-->e,f) = f by FUNCT_2:63;
now
let c;
thus (F.:(f,g)).c = F.(f.c,g.c) by FUNCOP_1:37
.= F.(f.c,e)
.= f.c by A1,SETWISEO:15;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th44:
F is having_a_unity implies F[;](the_unity_wrt F,f) = f
proof
set e = the_unity_wrt F;
assume
A1: F is having_a_unity;
now
let c;
thus (F[;](e,f)).c = F.(e,f.c) by FUNCOP_1:53
.= f.c by A1,SETWISEO:15;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th45:
F is having_a_unity implies F[:](f,the_unity_wrt F) = f
proof
set e = the_unity_wrt F;
assume
A1: F is having_a_unity;
now
let c;
thus (F[:](f,e)).c = F.(f.c,e) by FUNCOP_1:48
.= f.c by A1,SETWISEO:15;
end;
hence thesis by FUNCT_2:63;
end;
theorem
F is_distributive_wrt G implies
F[;](G.(d1,d2),T) = G.:(F[;](d1,T),F[;](d2,T))
proof
assume
A1: F is_distributive_wrt G;
per cases;
suppose
i = 0;
then F[;](d1,T) = <*>D & F[;](G.(d1,d2),T) = <*>D by Lm2;
hence thesis by FINSEQ_2:73;
end;
suppose
i <> 0;
then reconsider C = Seg i as non empty set;
T is Function of C,D by Lm4;
hence thesis by A1,Th35;
end;
end;
theorem
F is_distributive_wrt G implies
F[:](T,G.(d1,d2)) = G.:(F[:](T,d1),F [:] (T,d2))
proof
assume
A1: F is_distributive_wrt G;
per cases;
suppose
i = 0;
then F[:](T,d1) = <*>D & F[:](T,G.(d1,d2)) = <*>D by Lm3;
hence thesis by FINSEQ_2:73;
end;
suppose
i <> 0;
then reconsider C = Seg i as non empty set;
T is Function of C,D by Lm4;
hence thesis by A1,Th36;
end;
end;
theorem Th48:
(for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2)) implies
h*(F.:(T1,T2)) = H.:(h*T1,h*T2)
proof
assume
A1: for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2);
per cases;
suppose
A2: i = 0;
then F.:(T1,T2) = <*>D by Lm1;
then
A3: h*(F.:(T1,T2)) = <*>E;
h*T1 = <*>E by A2;
hence thesis by A3,FINSEQ_2:73;
end;
suppose
i <> 0;
then reconsider C = Seg i as non empty set;
T1 is Function of C,D & T2 is Function of C,D by Lm4;
hence thesis by A1,Th37;
end;
end;
theorem Th49:
(for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2)) implies
h*(F[;](d,T)) = H[;](h.d,h*T)
proof
assume
A1: for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2);
per cases;
suppose
A2: i = 0;
then F[;](d,T) = <*>D by Lm2;
then
A3: h*(F[;](d,T)) = <*>E;
h*T = <*>E by A2;
hence thesis by A3,FINSEQ_2:79;
end;
suppose
i <> 0;
then reconsider C = Seg i as non empty set;
T is Function of C,D by Lm4;
hence thesis by A1,Th38;
end;
end;
theorem Th50:
(for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2)) implies
h*(F[:](T,d)) = H[:](h*T,h.d)
proof
assume
A1: for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2);
per cases;
suppose
A2: i = 0;
then F[:](T,d) = <*>D by Lm3;
then
A3: h*(F[:](T,d)) = <*>E;
h*T = <*>E by A2;
hence thesis by A3,FINSEQ_2:85;
end;
suppose
i <> 0;
then reconsider C = Seg i as non empty set;
T is Function of C,D by Lm4;
hence thesis by A1,Th39;
end;
end;
theorem
u is_distributive_wrt F implies u*(F.:(T1,T2)) = F.:(u*T1,u*T2) by Th48;
theorem
u is_distributive_wrt F implies u*(F[;](d,T)) = F[;](u.d,u*T) by Th49;
theorem
u is_distributive_wrt F implies u*(F[:](T,d)) = F[:](u*T,u.d) by Th50;
theorem
G is_distributive_wrt F & u = G[;](d,id D) implies u is_distributive_wrt F
proof
assume that
A1: G is_distributive_wrt F and
A2: u = G[;](d,id D);
let d1,d2;
thus u.(F.(d1,d2)) = G.(d,(id D).(F.(d1,d2))) by A2,FUNCOP_1:53
.= G.(d,F.(d1,d2))
.= F.(G.(d,d1),G.(d,d2)) by A1,BINOP_1:11
.= F.(G.(d,(id D).d1),G.(d,d2))
.= F.(G.(d,(id D).d1),G.(d,(id D).d2))
.= F.(u.d1,G.(d,(id D).d2)) by A2,FUNCOP_1:53
.= F.(u.d1,u.d2) by A2,FUNCOP_1:53;
end;
theorem
G is_distributive_wrt F & u = G[:](id D,d) implies u is_distributive_wrt F
proof
assume that
A1: G is_distributive_wrt F and
A2: u = G[:](id D,d);
let d1,d2;
thus u.(F.(d1,d2)) = G.((id D).(F.(d1,d2)),d) by A2,FUNCOP_1:48
.= G.(F.(d1,d2),d)
.= F.(G.(d1,d),G.(d2,d)) by A1,BINOP_1:11
.= F.(G.((id D).d1,d),G.(d2,d))
.= F.(G.((id D).d1,d),G.((id D).d2,d))
.= F.(u.d1,G.((id D).d2,d)) by A2,FUNCOP_1:48
.= F.(u.d1,u.d2) by A2,FUNCOP_1:48;
end;
theorem
F is having_a_unity implies
F.:(i|->the_unity_wrt F,T) = T & F.:(T,i|->the_unity_wrt F) = T
proof
assume
A1: F is having_a_unity;
per cases;
suppose
A2: i = 0;
then T = <*>D;
hence thesis by A2,Lm1;
end;
suppose
i <> 0;
then reconsider C = Seg i as non empty set;
T is Function of C,D by Lm4;
hence thesis by A1,Th43;
end;
end;
theorem
F is having_a_unity implies F[;](the_unity_wrt F,T) = T
proof
assume
A1: F is having_a_unity;
per cases;
suppose
i = 0;
then T = <*>D;
hence thesis by Lm2;
end;
suppose
i <> 0;
then reconsider C = Seg i as non empty set;
T is Function of C,D by Lm4;
hence thesis by A1,Th44;
end;
end;
theorem
F is having_a_unity implies F[:](T,the_unity_wrt F) = T
proof
assume
A1: F is having_a_unity;
per cases;
suppose
i = 0;
then T = <*>D;
hence thesis by Lm3;
end;
suppose
i <> 0;
then reconsider C = Seg i as non empty set;
T is Function of C,D by Lm4;
hence thesis by A1,Th45;
end;
end;
definition
let D,u,F;
pred u is_an_inverseOp_wrt F means
for d holds F.(d,u.d) = the_unity_wrt F & F.(u.d,d) = the_unity_wrt F;
end;
definition
let D,F;
attr F is having_an_inverseOp means
ex u st u is_an_inverseOp_wrt F;
end;
definition
let D,F;
assume that
A1: F is having_a_unity and
A2: F is associative and
A3: F is having_an_inverseOp;
func the_inverseOp_wrt F -> UnOp of D means :Def3:
it is_an_inverseOp_wrt F;
existence by A3;
uniqueness
proof
set e = the_unity_wrt F;
let u1,u2 be UnOp of D such that
A4: for d holds F.(d,u1.d) = e & F.(u1.d,d) = e and
A5: for d holds F.(d,u2.d) = e & F.(u2.d,d) = e;
now
let d;
set d1 = u1.d, d2 = u2.d;
thus u1.d = F.(d1,e) by A1,SETWISEO:15
.= F.(d1,F.(d,d2)) by A5
.= F.(F.(d1,d),d2) by A2
.= F.(e,d2) by A4
.= u2.d by A1,SETWISEO:15;
end;
hence thesis by FUNCT_2:63;
end;
end;
theorem Th59:
F is having_a_unity & F is associative & F is having_an_inverseOp implies
F.((the_inverseOp_wrt F).d,d) = the_unity_wrt F &
F.(d,(the_inverseOp_wrt F).d) = the_unity_wrt F
proof
assume F is having_a_unity & F is associative & F is having_an_inverseOp;
then the_inverseOp_wrt F is_an_inverseOp_wrt F by Def3;
hence thesis;
end;
theorem Th60:
F is having_a_unity & F is associative & F is having_an_inverseOp &
F.(d1,d2) = the_unity_wrt F implies
d1 = (the_inverseOp_wrt F).d2 & (the_inverseOp_wrt F).d1 = d2
proof
assume that
A1: F is having_a_unity and
A2: F is associative and
A3: F is having_an_inverseOp and
A4: F.(d1,d2) = the_unity_wrt F;
set e = the_unity_wrt F, d3 = (the_inverseOp_wrt F).d2;
F.(F.(d1,d2),d3) = d3 by A1,A4,SETWISEO:15;
then F.(d1,F.(d2,d3)) = d3 by A2;
then F.(d1,e) = d3 by A1,A2,A3,Th59;
hence d1 = d3 by A1,SETWISEO:15;
set d3 = (the_inverseOp_wrt F).d1;
F.(d3,F.(d1,d2)) = d3 by A1,A4,SETWISEO:15;
then F.(F.(d3,d1),d2) = d3 by A2;
then F.(e,d2) = d3 by A1,A2,A3,Th59;
hence thesis by A1,SETWISEO:15;
end;
theorem Th61:
F is having_a_unity & F is associative & F is having_an_inverseOp implies
(the_inverseOp_wrt F).(the_unity_wrt F) = the_unity_wrt F
proof
assume that
A1: F is having_a_unity and
A2: F is associative & F is having_an_inverseOp;
set e = the_unity_wrt F;
F.(e,e) = e by A1,SETWISEO:15;
hence thesis by A1,A2,Th60;
end;
theorem Th62:
F is having_a_unity & F is associative & F is having_an_inverseOp implies
(the_inverseOp_wrt F).((the_inverseOp_wrt F).d) = d
proof
assume
A1: F is having_a_unity & F is associative & F is having_an_inverseOp;
then F.(d,(the_inverseOp_wrt F).d) = the_unity_wrt F by Th59;
hence thesis by A1,Th60;
end;
theorem Th63:
F is having_a_unity & F is associative & F is commutative &
F is having_an_inverseOp implies
(the_inverseOp_wrt F) is_distributive_wrt F
proof
assume that
A1: F is having_a_unity and
A2: F is associative and
A3: F is commutative and
A4: F is having_an_inverseOp;
let d1,d2;
set e = the_unity_wrt F, u = the_inverseOp_wrt F;
F.(F.(u.d1,u.d2),F.(d1,d2)) = F.(u.d1,F.(u.d2,F.(d1,d2))) by A2
.= F.(u.d1,F.(F.(u.d2,d1),d2)) by A2
.= F.(u.d1,F.(F.(d1,u.d2),d2)) by A3
.= F.(u.d1,F.(d1,F.(u.d2,d2))) by A2
.= F.(u.d1,F.(d1,e)) by A1,A2,A4,Th59
.= F.(F.(u.d1,d1),e) by A2
.= F.(e,e) by A1,A2,A4,Th59
.= e by A1,SETWISEO:15;
hence u.(F.(d1,d2)) = F.(u.d1,u.d2) by A1,A2,A4,Th60;
end;
theorem Th64:
F is having_a_unity & F is associative & F is having_an_inverseOp &
(F.(d,d1) = F.(d,d2) or F.(d1,d) = F.(d2,d)) implies d1 = d2
proof
assume that
A1: F is having_a_unity and
A2: F is associative and
A3: F is having_an_inverseOp and
A4: F.(d,d1) = F.(d,d2) or F.(d1,d) = F.(d2,d);
set e = the_unity_wrt F, u = the_inverseOp_wrt F;
per cases by A4;
suppose
A5: F.(d,d1) = F.(d,d2);
thus d1 = F.(e,d1) by A1,SETWISEO:15
.= F.(F.(u.d,d),d1) by A1,A2,A3,Th59
.= F.(u.d,F.(d,d2)) by A2,A5
.= F.(F.(u.d,d),d2) by A2
.= F.(e,d2) by A1,A2,A3,Th59
.= d2 by A1,SETWISEO:15;
end;
suppose
A6: F.(d1,d) = F.(d2,d);
thus d1 = F.(d1,e) by A1,SETWISEO:15
.= F.(d1,F.(d,u.d)) by A1,A2,A3,Th59
.= F.(F.(d2,d),u.d) by A2,A6
.= F.(d2,F.(d,u.d)) by A2
.= F.(d2,e) by A1,A2,A3,Th59
.= d2 by A1,SETWISEO:15;
end;
end;
theorem Th65:
F is having_a_unity & F is associative & F is having_an_inverseOp &
(F.(d1,d2) = d2 or F.(d2,d1) = d2) implies d1 = the_unity_wrt F
proof
assume that
A1: F is having_a_unity and
A2: F is associative & F is having_an_inverseOp;
set e = the_unity_wrt F;
assume F.(d1,d2) = d2 or F.(d2,d1) = d2;
then F.(d1,d2) = F.(e,d2) or F.(d2,d1) = F.(d2,e) by A1,SETWISEO:15;
hence thesis by A1,A2,Th64;
end;
theorem Th66:
F is associative & F is having_a_unity & F is having_an_inverseOp &
G is_distributive_wrt F & e = the_unity_wrt F implies
for d holds G.(e,d) = e & G.(d,e) = e
proof
assume that
A1: F is associative and
A2: F is having_a_unity and
A3: F is having_an_inverseOp and
A4: G is_distributive_wrt F and
A5: e = the_unity_wrt F;
let d;
set ed = G.(e,d);
F.(ed,ed) = G.(F.(e,e),d) by A4,BINOP_1:11
.= ed by A2,A5,SETWISEO:15;
hence ed = e by A1,A2,A3,A5,Th65;
set de = G.(d,e);
F.(de,de) = G.(d,F.(e,e)) by A4,BINOP_1:11
.= de by A2,A5,SETWISEO:15;
hence thesis by A1,A2,A3,A5,Th65;
end;
theorem Th67:
F is having_a_unity & F is associative & F is having_an_inverseOp &
u = the_inverseOp_wrt F & G is_distributive_wrt F implies
u.(G.(d1,d2)) = G.(u.d1,d2) & u.(G.(d1,d2)) = G.(d1,u.d2)
proof
assume that
A1: F is having_a_unity & F is associative & F is having_an_inverseOp and
A2: u = the_inverseOp_wrt F and
A3: G is_distributive_wrt F;
set e = the_unity_wrt F;
F.(G.(d1,d2),G.(u.d1,d2)) = G.(F.(d1,u.d1),d2) by A3,BINOP_1:11
.= G.(e,d2) by A1,A2,Th59
.= e by A1,A3,Th66;
hence u.(G.(d1,d2)) = G.(u.d1,d2) by A1,A2,Th60;
F.(G.(d1,d2),G.(d1,u.d2)) = G.(d1,F.(d2,u.d2)) by A3,BINOP_1:11
.= G.(d1,e) by A1,A2,Th59
.= e by A1,A3,Th66;
hence thesis by A1,A2,Th60;
end;
theorem
F is having_a_unity & F is associative & F is having_an_inverseOp &
u = the_inverseOp_wrt F & G is_distributive_wrt F & G is having_a_unity
implies G [;](u.(the_unity_wrt G),id D) = u
proof
assume that
A1: F is having_a_unity & F is associative & F is having_an_inverseOp &
u = the_inverseOp_wrt F & G is_distributive_wrt F and
A2: G is having_a_unity;
set o = the_unity_wrt G;
for d holds (G[;](u.o,id D)).d = u.d
proof
let d;
thus (G[;](u.o,id D)).d = G.(u.o,(id D).d) by FUNCOP_1:53
.= G.(u.o,d)
.= u.(G.(o,d)) by A1,Th67
.= u.d by A2,SETWISEO:15;
end;
hence thesis by FUNCT_2:63;
end;
theorem
F is associative & F is having_a_unity & F is having_an_inverseOp &
G is_distributive_wrt F implies
G[;](d,id D).the_unity_wrt F = the_unity_wrt F
proof
assume that
A1: F is associative and
A2: F is having_a_unity and
A3: F is having_an_inverseOp and
A4: G is_distributive_wrt F;
set e = the_unity_wrt F, i = the_inverseOp_wrt F;
G.(d,e) = G.(d,F.(e,e)) by A2,SETWISEO:15
.= F.(G.(d,e),G.(d,e)) by A4,BINOP_1:11;
then e = F.(F.(G.(d,e),G.(d,e)),i.(G.(d,e))) by A1,A2,A3,Th59;
then e = F.(G.(d,e),F.(G.(d,e),i.(G.(d,e)))) by A1;
then e = F.(G.(d,e),e) by A1,A2,A3,Th59;
then e = G.(d,e) by A2,SETWISEO:15;
then G.(d,(id D).e) = e;
hence thesis by FUNCOP_1:53;
end;
theorem
F is associative & F is having_a_unity & F is having_an_inverseOp &
G is_distributive_wrt F implies
G[:](id D,d).the_unity_wrt F = the_unity_wrt F
proof
assume that
A1: F is associative and
A2: F is having_a_unity and
A3: F is having_an_inverseOp and
A4: G is_distributive_wrt F;
set e = the_unity_wrt F, i = the_inverseOp_wrt F;
G.(e,d) = G.(F.(e,e),d) by A2,SETWISEO:15
.= F.(G.(e,d),G.(e,d)) by A4,BINOP_1:11;
then e = F.(F.(G.(e,d),G.(e,d)),i.(G.(e,d))) by A1,A2,A3,Th59;
then e = F.(G.(e,d),F.(G.(e,d),i.(G.(e,d)))) by A1;
then e = F.(G.(e,d),e) by A1,A2,A3,Th59;
then e = G.(e,d) by A2,SETWISEO:15;
then G.((id D).e,d) = e;
hence thesis by FUNCOP_1:48;
end;
theorem Th71:
F is having_a_unity & F is associative & F is having_an_inverseOp
implies F.:(f,(the_inverseOp_wrt F)*f) = C-->the_unity_wrt F &
F.:((the_inverseOp_wrt F)*f,f) = C-->the_unity_wrt F
proof
set u = the_inverseOp_wrt F;
reconsider g = C-->the_unity_wrt F as Function of C,D;
assume
A1: F is having_a_unity & F is associative & F is having_an_inverseOp;
now
let c;
thus (F.:(f,u*f)).c = F.(f.c,(u*f).c) by FUNCOP_1:37
.= F.(f.c,u.(f.c)) by FUNCT_2:15
.= the_unity_wrt F by A1,Th59
.= g.c;
end;
hence F.:(f,(the_inverseOp_wrt F)*f) = C-->the_unity_wrt F by FUNCT_2:63;
now
let c;
thus (F.:(u*f,f)).c = F.((u*f).c,f.c) by FUNCOP_1:37
.= F.(u.(f.c),f.c) by FUNCT_2:15
.= the_unity_wrt F by A1,Th59
.= g.c;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th72:
F is associative & F is having_an_inverseOp & F is having_a_unity &
F.:(f,f9) = C-->the_unity_wrt F implies
f = (the_inverseOp_wrt F)*f9 & (the_inverseOp_wrt F)*f = f9
proof
assume that
A1: F is associative & F is having_an_inverseOp & F is having_a_unity and
A2: F.:(f,f9) = C-->the_unity_wrt F;
set u = the_inverseOp_wrt F;
set e = the_unity_wrt F;
reconsider g = C-->e as Function of C,D;
now
let c;
F.(f.c,f9.c) = g.c by A2,FUNCOP_1:37
.= e;
hence f.c = u.(f9.c) by A1,Th60
.= (u*f9).c by FUNCT_2:15;
end;
hence f = (the_inverseOp_wrt F)*f9 by FUNCT_2:63;
now
let c;
F.(f.c,f9.c) = g.c by A2,FUNCOP_1:37
.= e;
then f9.c = u.(f.c) by A1,Th60;
hence (u*f).c = f9.c by FUNCT_2:15;
end;
hence thesis by FUNCT_2:63;
end;
theorem
F is having_a_unity & F is associative & F is having_an_inverseOp
implies F.:(T,(the_inverseOp_wrt F)*T) = i|->the_unity_wrt F &
F.:((the_inverseOp_wrt F)*T,T) = i|->the_unity_wrt F
proof
assume
A1: F is having_a_unity & F is associative & F is having_an_inverseOp;
reconsider uT = the_inverseOp_wrt F*T as Element of i-tuples_on D by
FINSEQ_2:113;
per cases;
suppose
A2: i = 0;
then F.:(T,uT) = <*>D & F.:(uT,T) = <*>D by Lm1;
hence thesis by A2;
end;
suppose
i <> 0;
then reconsider C = Seg i as non empty set;
T is Function of C,D by Lm4;
hence thesis by A1,Th71;
end;
end;
theorem
F is associative & F is having_an_inverseOp & F is having_a_unity &
F.:(T1,T2) = i|->the_unity_wrt F implies
T1 = (the_inverseOp_wrt F)*T2 & (the_inverseOp_wrt F)*T1 = T2
proof
assume
A1: F is associative & F is having_an_inverseOp & F is having_a_unity &
F .:(T1,T2) = i|->the_unity_wrt F;
per cases;
suppose
i = 0;
then T1 = <*>D & T2 = <*>D;
hence thesis;
end;
suppose
i <> 0;
then reconsider C = Seg i as non empty set;
T1 is Function of C,D & T2 is Function of C,D by Lm4;
hence thesis by A1,Th72;
end;
end;
theorem Th75:
F is associative & F is having_a_unity & e = the_unity_wrt F &
F is having_an_inverseOp & G is_distributive_wrt F implies
G[;](e,f) = C-->e
proof
reconsider g = C-->e as Function of C,D;
assume
A1: F is associative & F is having_a_unity & e = the_unity_wrt F & F is
having_an_inverseOp & G is_distributive_wrt F;
now
let c;
thus (G[;](e,f)).c = G.(e,f.c) by FUNCOP_1:53
.= e by A1,Th66
.= g.c;
end;
hence thesis by FUNCT_2:63;
end;
theorem
F is associative & F is having_a_unity & e = the_unity_wrt F &
F is having_an_inverseOp & G is_distributive_wrt F implies
G[;](e,T) = i|->e
proof
assume
A1: F is associative & F is having_a_unity & e = the_unity_wrt F & F is
having_an_inverseOp & G is_distributive_wrt F;
per cases;
suppose
A2: i = 0;
then G[;](e,T) = <*>D by Lm2;
hence thesis by A2;
end;
suppose
i <> 0;
then reconsider C = Seg i as non empty set;
T is Function of C,D by Lm4;
hence thesis by A1,Th75;
end;
end;
definition
let F,f,g be Function;
func F*(f,g) -> Function equals
F*[:f,g:];
correctness;
end;
theorem Th77:
for F,f,g being Function st [x,y] in dom(F*(f,g)) holds
(F*(f,g)).(x,y) = F.(f.x,g.y)
proof
let F,f,g be Function such that
A1: [x,y] in dom(F*(f,g));
[x,y] in dom [:f,g:] by A1,FUNCT_1:11;
then [x,y] in [:dom f,dom g:] by FUNCT_3:def 8;
then [:f,g:].(x,y) = [f.x,g.y] by FUNCT_3:65;
hence thesis by A1,FUNCT_1:12;
end;
::$CT
theorem Th78:
for F being Function of [:D,D9:],E, f being Function of C,D,
g being Function of C9,D9 holds F*(f,g) is Function of [:C,C9:],E
proof
let F be Function of [:D,D9:],E, f be Function of C,D, g be Function of C9,
D9;
F*(f,g) = F*[:f,g:];
hence thesis;
end;
theorem
for u,u9 being Function of D,D holds F*(u,u9) is BinOp of D by Th78;
definition
let D,F;
let f,f9 be Function of D,D;
redefine func F*(f,f9) -> BinOp of D; :: redefines * (FINSEQOP, definition)
coherence by Th78;
end;
theorem Th80:
for F being Function of [:D,D9:],E, f being Function of C,D,
g being Function of C9,D9 holds (F*(f,g)).(c,c9) = F.(f.c,g.c9)
proof
let F be Function of [:D,D9:],E, f be Function of C,D, g be Function of C9,
D9;
set H = F*(f,g);
H is Function of [:C,C9:],E by Th78;
then dom H = [:C,C9:] by FUNCT_2:def 1;
then [c,c9] in dom H by ZFMISC_1:def 2;
hence thesis by Th77;
end;
theorem Th81:
for u being Function of D,D holds
(F*(id D,u)).(d1,d2) = F.(d1,u.d2) & (F*(u,id D)).(d1,d2) = F.(u.d1,d2)
proof
let u be Function of D,D;
(id D).d1 = d1 & (id D).d2 = d2;
hence thesis by Th80;
end;
theorem Th82:
(F*(id D,u)).:(f,f9) = F.:(f,u*f9)
proof
now
let c;
thus ((F*(id D,u)).:(f,f9)).c = (F*(id D,u)).(f.c,f9.c) by FUNCOP_1:37
.= F.(f.c,u.(f9.c)) by Th81
.= F.(f.c,(u*f9).c) by FUNCT_2:15
.= (F.:(f,u*f9)).c by FUNCOP_1:37;
end;
hence thesis by FUNCT_2:63;
end;
theorem
(F*(id D,u)).:(T1,T2) = F.:(T1,u*T2)
proof
now
per cases;
suppose
i = 0;
then (F*(id D,u)).:(T1,T2) = <*>D & u*T2 = <*>D by Lm1;
hence thesis by FINSEQ_2:73;
end;
suppose
i <> 0;
then reconsider C = Seg i as non empty set;
T1 is Function of C,D & T2 is Function of C,D by Lm4;
hence thesis by Th82;
end;
end;
hence thesis;
end;
theorem
F is associative & F is having_a_unity & F is commutative &
F is having_an_inverseOp & u = the_inverseOp_wrt F implies
u.(F*(id D,u).(d1,d2)) =
F*(u,id D).(d1,d2) & F*(id D,u).(d1,d2) = u.(F*(u,id D).(d1,d2))
proof
assume that
A1: F is associative & F is having_a_unity and
A2: F is commutative and
A3: F is having_an_inverseOp & u = the_inverseOp_wrt F;
A4: u is_distributive_wrt F by A1,A2,A3,Th63;
thus u.(F*(id D,u).(d1,d2)) = u.(F.(d1,u.d2)) by Th81
.= F.(u.d1,u.(u.d2)) by A4
.= F.(u.d1,d2) by A1,A3,Th62
.= F*(u,id D).(d1,d2) by Th81;
hence thesis by A1,A3,Th62;
end;
theorem
F is associative & F is having_a_unity & F is having_an_inverseOp
implies (F*(id D,the_inverseOp_wrt F)).(d,d) = the_unity_wrt F
proof
assume
A1: F is associative & F is having_a_unity & F is having_an_inverseOp;
set u = the_inverseOp_wrt F;
thus F*(id D,u).(d,d) = F.(d,u.d) by Th81
.= the_unity_wrt F by A1,Th59;
end;
theorem
F is associative & F is having_a_unity & F is having_an_inverseOp
implies (F*(id D,the_inverseOp_wrt F)).(d,the_unity_wrt F) = d
proof
assume that
A1: F is associative and
A2: F is having_a_unity and
A3: F is having_an_inverseOp;
set u = the_inverseOp_wrt F, e = the_unity_wrt F;
thus (F*(id D,u)).(d,e) = F.(d,u.e) by Th81
.= F.(d,e) by A1,A2,A3,Th61
.= d by A2,SETWISEO:15;
end;
theorem
F is having_a_unity implies (F*(id D,u)).(the_unity_wrt F,d) = u.d
proof
assume
A1: F is having_a_unity;
set e = the_unity_wrt F;
thus (F*(id D,u)).(e,d) = F.(e,u.d) by Th81
.= u.d by A1,SETWISEO:15;
end;
theorem
F is commutative associative & F is having_a_unity &
F is having_an_inverseOp & G = F*(id D,the_inverseOp_wrt F) implies
for d1,d2,d3,d4 holds F.(G.(d1,d2),G.(d3,d4))= G.(F.(d1,d3),F.(d2,d4))
proof
assume that
A1: F is commutative and
A2: F is associative and
A3: F is having_a_unity & F is having_an_inverseOp and
A4: G = F*(id D,the_inverseOp_wrt F);
set u = the_inverseOp_wrt F;
A5: u is_distributive_wrt F by A1,A2,A3,Th63;
let d1,d2,d3,d4;
thus F.(G.(d1,d2),G.(d3,d4)) = F.(F.(d1,u.d2),G.(d3,d4)) by A4,Th81
.= F.(F.(d1,u.d2),F.(d3,u.d4)) by A4,Th81
.= F.(d1,F.(u.d2,F.(d3,u.d4))) by A2
.= F.(d1,F.(F.(u.d2,d3),u.d4)) by A2
.= F.(d1,F.(F.(d3,u.d2),u.d4)) by A1
.= F.(d1,F.(d3,F.(u.d2,u.d4))) by A2
.= F.(F.(d1,d3),F.(u.d2,u.d4)) by A2
.= F.(F.(d1,d3),u.(F.(d2,d4))) by A5
.= G.(F.(d1,d3),F.(d2,d4)) by A4,Th81;
end;
:: SK, 15.11.2024
registration
let D being non empty set;
let p being FinSequence of D;
let h being ManySortedSet of D;
cluster h*p -> FinSequence-like;
coherence
proof
rng p c= D & dom h = D by PARTFUN1:def 2;
then dom(h*p) = dom p by RELAT_1:27;
then ex k being Nat st dom(h*p) = Seg k by FINSEQ_1:def 2;
hence thesis by FINSEQ_1:def 2;
end;
end;