Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### Binary Operations Applied to Finite Sequences

by
Czeslaw Bylinski

MML identifier: FINSEQOP
[ Mizar article, MML identifier index ]

```environ

vocabulary FUNCT_1, PARTFUN1, BOOLE, RELAT_1, FUNCOP_1, FINSEQ_1, FINSEQ_2,
BINOP_1, SETWISEO, FINSEQOP;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NAT_1, RELAT_1, FUNCT_1,
FINSEQ_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCT_3, FUNCOP_1, FINSEQ_2,
SETWISEO;
constructors NAT_1, BINOP_1, FUNCT_3, FUNCOP_1, FINSEQ_2, SETWISEO, RELAT_2,
PARTFUN1, XBOOLE_0;
clusters SUBSET_1, RELAT_1, FUNCT_1, FINSEQ_2, RELSET_1, FUNCOP_1, ARYTM_3,
ZFMISC_1, FUNCT_2, PARTFUN1, XBOOLE_0;
requirements NUMERALS, BOOLE, SUBSET;

begin

reserve x,y for set;
reserve C,C',D,D',E for non empty set;
reserve c for Element of C;
reserve c' for Element of C';
reserve d,d1,d2,d3,d4,e for Element of D;
reserve d' for Element of D';

:: Auxiliary theorems

theorem :: FINSEQOP:1
for f being Function holds <:{},f:> = {} & <:f,{}:> = {};

theorem :: FINSEQOP:2
for f being Function holds [:{},f:] = {} & [:f,{}:] = {};

canceled;

theorem :: FINSEQOP:4
for F,f being Function holds F.:({},f) = {} & F.:(f,{}) = {};

theorem :: FINSEQOP:5
for F being Function holds F[:]({},x) = {};

theorem :: FINSEQOP:6
for F being Function holds F[;](x,{}) = {};

theorem :: FINSEQOP:7
for X being set, x1,x2 being set holds <:X-->x1,X-->x2:> = X -->[x1,x2];

theorem :: FINSEQOP:8
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]);

reserve i,j for Nat;

reserve F for Function of [:D,D':],E;
reserve p,q for FinSequence of D, p',q' for FinSequence of D';

definition let D,D',E,F,p,p';
redefine func F.:(p,p') -> FinSequence of E;
end;

definition let D,D',E,F,p,d';
redefine func F[:](p,d') -> FinSequence of E;
end;

definition let D,D',E,F,d,p';
redefine func F[;](d,p') -> FinSequence of E;
end;

definition let D,i,d;
redefine func i|-> d -> Element of i-tuples_on D;
end;

reserve f,f' 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;
end;

theorem :: FINSEQOP:9
h*(p^<*d*>) = (h*p)^<*h.d*>;

theorem :: FINSEQOP:10
h*(p^q) = (h*p)^(h*q);

reserve T,T1,T2,T3 for Element of i-tuples_on D;
reserve T' for Element of i-tuples_on D';
reserve S,S1 for Element of j-tuples_on D;
reserve S',S1' for Element of j-tuples_on D';

theorem :: FINSEQOP:11
F.:(T^<*d*>,T'^<*d'*>) = (F.:(T,T'))^<*F.(d,d')*>;

theorem :: FINSEQOP:12
F.:(T^S,T'^S') = (F.:(T,T'))^(F.:(S,S'));

theorem :: FINSEQOP:13
F[;](d,p'^<*d'*>) = (F[;](d,p'))^<*F.(d,d')*>;

theorem :: FINSEQOP:14
F[;](d,p'^q') = (F[;](d,p'))^(F[;](d,q'));

theorem :: FINSEQOP:15
F[:](p^<*d*>,d') = (F[:](p,d'))^<*F.(d,d')*>;

theorem :: FINSEQOP:16
F[:](p^q,d') = (F[:](p,d'))^(F[:](q,d'));

theorem :: FINSEQOP:17
for h being Function of D,E holds h*(i|->d) = i|->(h.d);

theorem :: FINSEQOP:18
F.:(i|->d,i|->d') = i |-> (F.(d,d'));

theorem :: FINSEQOP:19
F[;](d,i|->d') = i |-> (F.(d,d'));

theorem :: FINSEQOP:20
F[:](i|->d,d') = i |-> (F.(d,d'));

theorem :: FINSEQOP:21
F.:(i|->d,T') = F[;](d,T');

theorem :: FINSEQOP:22
F.:(T,i|->d) = F[:](T,d);

theorem :: FINSEQOP:23
F[;](d,T') = F[;](d,id D')*T';

theorem :: FINSEQOP:24
F[:](T,d) = F[:](id D,d)*T;

:: Binary Operations

reserve F,G for BinOp of D;
reserve u for UnOp of D;
reserve H for BinOp of E;

theorem :: FINSEQOP:25
F is associative implies F[;](d,id D)*(F.:(f,f')) = F.:(F[;](d,id D)*f,f');

theorem :: FINSEQOP:26
F is associative implies F[:](id D,d)*(F.:(f,f')) = F.:(f,F[:](id D,d)*f');

theorem :: FINSEQOP:27
F is associative implies F[;](d,id D)*(F.:(T1,T2)) = F.:(F[;](d,id D)*T1,T2);

theorem :: FINSEQOP:28
F is associative implies F[:](id D,d)*(F.:(T1,T2)) = F.:(T1,F[:](id D,d)*T2);

theorem :: FINSEQOP:29
F is associative implies F.:(F.:(T1,T2),T3) = F.:(T1,F.:(T2,T3));

theorem :: FINSEQOP:30
F is associative implies F[:](F[;](d1,T),d2) = F[;](d1,F[:](T,d2));

theorem :: FINSEQOP:31
F is associative implies F.:(F[:](T1,d),T2) = F.:(T1,F[;](d,T2));

theorem :: FINSEQOP:32
F is associative implies F[;](F.(d1,d2),T) = F[;](d1,F[;](d2,T));

theorem :: FINSEQOP:33
F is associative implies F[:](T,F.(d1,d2)) = F[:](F[:](T,d1),d2);

theorem :: FINSEQOP:34
F is commutative implies F.:(T1,T2) = F.:(T2,T1);

theorem :: FINSEQOP:35
F is commutative implies F[;](d,T) = F[:](T,d);

theorem :: FINSEQOP:36
F is_distributive_wrt G implies F[;](G.(d1,d2),f) = G.:(F[;](d1,f),F[;]
(d2,f));

theorem :: FINSEQOP:37
F is_distributive_wrt G implies F[:](f,G.(d1,d2)) = G.:(F[:](f,d1),F[:]
(f,d2));

theorem :: FINSEQOP:38
(for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2))
implies h*(F.:(f,f')) = H.:(h*f,h*f');

theorem :: FINSEQOP:39
(for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2))
implies h*(F[;](d,f)) = H[;](h.d,h*f);

theorem :: FINSEQOP:40
(for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2))
implies h*(F[:](f,d)) = H[:](h*f,h.d);

theorem :: FINSEQOP:41
u is_distributive_wrt F implies u*(F.:(f,f')) = F.:(u*f,u*f');

theorem :: FINSEQOP:42
u is_distributive_wrt F implies u*(F[;](d,f)) = F[;](u.d,u*f);

theorem :: FINSEQOP:43
u is_distributive_wrt F implies u*(F[:](f,d)) = F[:](u*f,u.d);

theorem :: FINSEQOP:44
F has_a_unity implies
F.:(C-->the_unity_wrt F,f) = f & F.:(f,C-->the_unity_wrt F) = f;

theorem :: FINSEQOP:45
F has_a_unity implies F[;](the_unity_wrt F,f) = f;

theorem :: FINSEQOP:46
F has_a_unity implies F[:](f,the_unity_wrt F) = f;

theorem :: FINSEQOP:47
F is_distributive_wrt G implies F[;](G.(d1,d2),T) = G.:(F[;](d1,T),F[;]
(d2,T));

theorem :: FINSEQOP:48
F is_distributive_wrt G implies F[:](T,G.(d1,d2)) = G.:(F[:](T,d1),F[:]
(T,d2));

theorem :: FINSEQOP:49
(for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2))
implies h*(F.:(T1,T2)) = H.:(h*T1,h*T2);

theorem :: FINSEQOP:50
(for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2))
implies h*(F[;](d,T)) = H[;](h.d,h*T);

theorem :: FINSEQOP:51
(for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2))
implies h*(F[:](T,d)) = H[:](h*T,h.d);

theorem :: FINSEQOP:52
u is_distributive_wrt F implies u*(F.:(T1,T2)) = F.:(u*T1,u*T2);

theorem :: FINSEQOP:53
u is_distributive_wrt F implies u*(F[;](d,T)) = F[;](u.d,u*T);

theorem :: FINSEQOP:54
u is_distributive_wrt F implies u*(F[:](T,d)) = F[:](u*T,u.d);

theorem :: FINSEQOP:55
G is_distributive_wrt F & u = G[;](d,id D) implies u is_distributive_wrt F
;

theorem :: FINSEQOP:56
G is_distributive_wrt F & u = G[:](id D,d) implies u is_distributive_wrt F
;

theorem :: FINSEQOP:57
F has_a_unity implies
F.:(i|->the_unity_wrt F,T) = T & F.:(T,i|->the_unity_wrt F) = T;

theorem :: FINSEQOP:58
F has_a_unity implies F[;](the_unity_wrt F,T) = T;

theorem :: FINSEQOP:59
F has_a_unity implies F[:](T,the_unity_wrt F) = T;

definition let D,u,F;
pred u is_an_inverseOp_wrt F means
:: FINSEQOP:def 1

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
:: FINSEQOP:def 2
ex u st u is_an_inverseOp_wrt F;
synonym F has_an_inverseOp;
end;

definition let D,F;
assume that
F has_a_unity and
F is associative and
F has_an_inverseOp;
func the_inverseOp_wrt F -> UnOp of D means
:: FINSEQOP:def 3
it is_an_inverseOp_wrt F;
end;

canceled 3;

theorem :: FINSEQOP:63
F has_a_unity & F is associative & F has_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;

theorem :: FINSEQOP:64
F has_a_unity & F is associative &
F has_an_inverseOp & F.(d1,d2) = the_unity_wrt F
implies d1 = (the_inverseOp_wrt F).d2 & (the_inverseOp_wrt F).d1 = d2;

theorem :: FINSEQOP:65
F has_a_unity & F is associative & F has_an_inverseOp
implies (the_inverseOp_wrt F).(the_unity_wrt F) = the_unity_wrt F;

theorem :: FINSEQOP:66
F has_a_unity & F is associative & F has_an_inverseOp
implies (the_inverseOp_wrt F).((the_inverseOp_wrt F).d) = d;

theorem :: FINSEQOP:67
F has_a_unity & F is associative & F is commutative & F has_an_inverseOp
implies (the_inverseOp_wrt F) is_distributive_wrt F;

theorem :: FINSEQOP:68
F has_a_unity & F is associative & F has_an_inverseOp &
(F.(d,d1) = F.(d,d2) or F.(d1,d) = F.(d2,d)) implies d1 = d2;

theorem :: FINSEQOP:69
F has_a_unity & F is associative & F has_an_inverseOp &
(F.(d1,d2) = d2 or F.(d2,d1) = d2) implies d1 = the_unity_wrt F;

theorem :: FINSEQOP:70
F is associative & F has_a_unity & F has_an_inverseOp &
G is_distributive_wrt F & e = the_unity_wrt F
implies for d holds G.(e,d) = e & G.(d,e) = e;

theorem :: FINSEQOP:71
F has_a_unity & F is associative & F has_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);

theorem :: FINSEQOP:72
F has_a_unity & F is associative & F has_an_inverseOp &
u = the_inverseOp_wrt F & G is_distributive_wrt F & G has_a_unity
implies G[;](u.(the_unity_wrt G),id D) = u;

theorem :: FINSEQOP:73
F is associative & F has_a_unity & F has_an_inverseOp &
G is_distributive_wrt F
implies G[;](d,id D).the_unity_wrt F = the_unity_wrt F;

theorem :: FINSEQOP:74
F is associative & F has_a_unity & F has_an_inverseOp &
G is_distributive_wrt F
implies G[:](id D,d).the_unity_wrt F = the_unity_wrt F;

theorem :: FINSEQOP:75
F has_a_unity & F is associative & F has_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;

theorem :: FINSEQOP:76
F is associative & F has_an_inverseOp &
F has_a_unity & F.:(f,f') = C-->the_unity_wrt F implies
f = (the_inverseOp_wrt F)*f' & (the_inverseOp_wrt F)*f = f';

theorem :: FINSEQOP:77
F has_a_unity & F is associative & F has_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;

theorem :: FINSEQOP:78
F is associative & F has_an_inverseOp &
F has_a_unity & F.:(T1,T2) = i|->the_unity_wrt F implies
T1 = (the_inverseOp_wrt F)*T2 & (the_inverseOp_wrt F)*T1 = T2;

theorem :: FINSEQOP:79
F is associative & F has_a_unity & e = the_unity_wrt F &
F has_an_inverseOp & G is_distributive_wrt F
implies G[;](e,f) = C-->e;

theorem :: FINSEQOP:80
F is associative & F has_a_unity & e = the_unity_wrt F &
F has_an_inverseOp & G is_distributive_wrt F
implies G[;](e,T) = i|->e;

definition
let F,f,g be Function;
func F*(f,g) -> Function equals
:: FINSEQOP:def 4
F*[:f,g:];
end;

canceled;

theorem :: FINSEQOP:82
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];

theorem :: FINSEQOP:83
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);

theorem :: FINSEQOP:84
for F being Function of [:D,D':],E,
f being Function of C,D, g being Function of C',D'
holds F*(f,g) is Function of [:C,C':],E;

theorem :: FINSEQOP:85
for u,u' being Function of D,D holds F*(u,u') is BinOp of D;

definition let D,F; let f,f' be Function of D,D;
redefine func F*(f,f') -> BinOp of D;
end;

theorem :: FINSEQOP:86
for F being Function of [:D,D':],E,
f being Function of C,D, g being Function of C',D'
holds (F*(f,g)).(c,c') = F.(f.c,g.c');

theorem :: FINSEQOP:87
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);

theorem :: FINSEQOP:88
(F*(id D,u)).:(f,f') = F.:(f,u*f');

theorem :: FINSEQOP:89
(F*(id D,u)).:(T1,T2) = F.:(T1,u*T2);

theorem :: FINSEQOP:90
F is associative & F has_a_unity & F is commutative &
F has_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));

theorem :: FINSEQOP:91
F is associative & F has_a_unity & F has_an_inverseOp implies
(F*(id D,the_inverseOp_wrt F)).(d,d) = the_unity_wrt F;

theorem :: FINSEQOP:92
F is associative & F has_a_unity & F has_an_inverseOp
implies (F*(id D,the_inverseOp_wrt F)).(d,the_unity_wrt F) = d;

theorem :: FINSEQOP:93
F is associative & F has_a_unity &
F has_an_inverseOp & u = the_inverseOp_wrt F
implies (F*(id D,u)).(the_unity_wrt F,d) = u.d;

theorem :: FINSEQOP:94
F is commutative & F is associative & F has_a_unity &
F has_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));
```