:: Extensions of Mappings on Generator Set
:: by Artur Korni{\l}owicz
::
:: Received March 23, 1995
:: Copyright (c) 1995-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 STRUCT_0, XBOOLE_0, MSUALG_1, RELAT_1, PBOOLE, MEMBER_1, TARSKI,
REALSET1, FUNCT_1, PZFMISC1, MSUALG_3, FUNCT_6, MSAFREE, LANG1, MCART_1,
TREES_4, SUBSET_1, FUNCOP_1, PRELAMB, MSUALG_2, UNIALG_2, MARGREL1,
CARD_3, NAT_1, PARTFUN1;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, RELSET_1, FUNCT_1, XTUPLE_0,
MCART_1, PARTFUN1, FUNCOP_1, FUNCT_6, PZFMISC1, FINSEQ_2, STRUCT_0,
LANG1, FUNCT_2, CARD_3, ORDINAL1, TREES_4, DTCONSTR, PBOOLE, MSUALG_1,
MSUALG_2, MSUALG_3, MSAFREE;
constructors PZFMISC1, MSUALG_3, MSAFREE, RELSET_1, XTUPLE_0;
registrations FUNCT_1, RELSET_1, FUNCOP_1, PBOOLE, STRUCT_0, MSUALG_1,
MSUALG_3, MSAFREE, MSSUBFAM, FINSEQ_1, XTUPLE_0;
requirements SUBSET, BOOLE;
definitions MSUALG_2, MSUALG_3, PBOOLE, FUNCOP_1, TARSKI, XBOOLE_0;
equalities XBOOLE_0;
expansions MSUALG_3, PBOOLE;
theorems FUNCOP_1, FUNCT_1, FUNCT_2, FUNCT_6, MSAFREE, MSAFREE2, MSUALG_1,
MSUALG_2, MSUALG_3, MSUHOM_1, PBOOLE, RELAT_1, CARD_3, RELSET_1,
PZFMISC1, ORDINAL1, PARTFUN1, FINSEQ_2;
schemes MSAFREE1, PBOOLE;
begin :: Preliminaries
reserve S for non void non empty ManySortedSign,
U1, U2, U3 for non-empty MSAlgebra over S,
I for set,
A for ManySortedSet of I,
B, C for non-empty ManySortedSet of I;
Lm1: for I be set for A, B, C be ManySortedSet of I for F be
ManySortedFunction of A, B for G be ManySortedFunction of B, C holds G ** F is
ManySortedSet of I
proof
let I be set;
let A, B, C be ManySortedSet of I;
let F be ManySortedFunction of A, B;
let G be ManySortedFunction of B, C;
dom (G ** F) = (dom F) /\ (dom G) by PBOOLE:def 19
.= I /\ (dom G) by PARTFUN1:def 2
.= I /\ I by PARTFUN1:def 2
.= I;
hence thesis by PARTFUN1:def 2,RELAT_1:def 18;
end;
begin :: Facts about Many Sorted Functions
theorem
for F be ManySortedFunction of A, B for X be ManySortedSubset of A st
A c= X holds F || X = F
proof
let F be ManySortedFunction of A, B, X be ManySortedSubset of A such that
A1: A c= X;
now
let i be object;
assume
A2: i in I;
then reconsider f = F.i as Function of A.i, B.i by PBOOLE:def 15;
A3: A.i c= X.i by A1,A2;
thus (F || X).i = (f | (X.i)) by A2,MSAFREE:def 1
.= F.i by A3,RELSET_1:19;
end;
hence thesis;
end;
theorem
for A, B be ManySortedSet of I for M be ManySortedSubset of A for F be
ManySortedFunction of A, B holds F.:.:M c= F.:.:A
proof
let A, B be ManySortedSet of I, M be ManySortedSubset of A, F be
ManySortedFunction of A, B;
let i be object such that
A1: i in I;
reconsider f = F.i as Function of A.i, B.i by A1,PBOOLE:def 15;
A2: (F.:.:M).i = f.:(M.i) by A1,PBOOLE:def 20;
M c= A by PBOOLE:def 18;
then M.i c= A.i by A1;
then
A3: f.:(M.i) c= f.:(A.i) by RELAT_1:123;
let x be object;
assume x in (F.:.:M).i;
then x in f.:(A.i) by A2,A3;
hence thesis by A1,PBOOLE:def 20;
end;
theorem
for F be ManySortedFunction of A, B for M1, M2 be ManySortedSubset of
A st M1 c= M2 holds (F||M2).:.:M1 = F.:.:M1
proof
let F be ManySortedFunction of A, B, M1, M2 be ManySortedSubset of A such
that
A1: M1 c= M2;
now
let i be object;
assume
A2: i in I;
then reconsider f = F.i as Function of A.i, B.i by PBOOLE:def 15;
reconsider fm = (F||M2).i as Function of M2.i, B.i by A2,PBOOLE:def 15;
A3: M1.i c= M2.i by A1,A2;
fm = f|(M2.i) by A2,MSAFREE:def 1;
hence ((F||M2).:.:M1).i = (f|(M2.i)).:(M1.i) by A2,PBOOLE:def 20
.= f.:(M1.i) by A3,RELAT_1:129
.= (F.:.:M1).i by A2,PBOOLE:def 20;
end;
hence thesis;
end;
theorem Th4:
for F be ManySortedFunction of A, B for G be ManySortedFunction
of B, C for X be ManySortedSubset of A holds (G ** F) || X = G ** (F || X)
proof
let F be ManySortedFunction of A, B, G be ManySortedFunction of B, C, X be
ManySortedSubset of A;
now
let i be object;
assume
A1: i in I;
then reconsider gf = (G ** F).i as Function of A.i, C.i by PBOOLE:def 15;
reconsider fx = (F || X).i as Function of X.i, B.i by A1,PBOOLE:def 15;
reconsider g = G.i as Function of B.i, C.i by A1,PBOOLE:def 15;
reconsider f = F.i as Function of A.i, B.i by A1,PBOOLE:def 15;
thus ((G ** F) || X).i = gf | (X.i) by A1,MSAFREE:def 1
.= (g*f) | (X.i) by A1,MSUALG_3:2
.= g * (f | (X.i)) by RELAT_1:83
.= g * fx by A1,MSAFREE:def 1
.= (G ** (F || X)).i by A1,MSUALG_3:2;
end;
hence thesis;
end;
theorem
for A, B be ManySortedSet of I st A is_transformable_to B for F be
ManySortedFunction of A, B for C be ManySortedSet of I st B is ManySortedSubset
of C holds F is ManySortedFunction of A, C
proof
let A, B be ManySortedSet of I such that
A1: A is_transformable_to B;
let F be ManySortedFunction of A, B, C be ManySortedSet of I;
assume B is ManySortedSubset of C;
then
A2: B c= C by PBOOLE:def 18;
let i be object such that
A3: i in I;
A4: B.i = {} implies A.i = {} by A1,A3,PZFMISC1:def 3;
A5: F.i is Function of A.i, B.i by A3,PBOOLE:def 15;
(B.i) c= (C.i) by A3,A2;
hence thesis by A4,A5,FUNCT_2:7;
end;
theorem
for F be ManySortedFunction of A, B for X be ManySortedSubset of A
holds F is "1-1" implies F || X is "1-1"
proof
let F be ManySortedFunction of A, B, X be ManySortedSubset of A;
assume
A1: F is "1-1";
now
let i be set;
assume
A2: i in I;
then reconsider f = F.i as Function of A.i, B.i by PBOOLE:def 15;
f is one-to-one by A1,A2,MSUALG_3:1;
then f | (X.i) is one-to-one by FUNCT_1:52;
hence (F||X).i is one-to-one by A2,MSAFREE:def 1;
end;
hence thesis by MSUALG_3:1;
end;
begin :: doms & rngs of Many Sorted Function
theorem
for F be ManySortedFunction of A, B for X be ManySortedSubset of A
holds doms (F || X) c= doms F
proof
let F be ManySortedFunction of A, B, X be ManySortedSubset of A;
let i be object;
A1: dom (F||X) = I by PARTFUN1:def 2;
assume
A2: i in I;
then reconsider f = F.i as Function of A.i, B.i by PBOOLE:def 15;
dom F = I by PARTFUN1:def 2;
then
A3: (doms F).i = dom f by A2,FUNCT_6:22;
(F||X).i = f|(X.i) by A2,MSAFREE:def 1;
then (doms (F||X)).i = dom (f|(X.i)) by A2,A1,FUNCT_6:22;
hence thesis by A3,RELAT_1:60;
end;
theorem
for F be ManySortedFunction of A, B for X be ManySortedSubset of A
holds rngs (F || X) c= rngs F
proof
let F be ManySortedFunction of A, B, X be ManySortedSubset of A;
let i be object;
A1: dom (F||X) = I by PARTFUN1:def 2;
assume
A2: i in I;
then reconsider f = F.i as Function of A.i, B.i by PBOOLE:def 15;
dom F = I by PARTFUN1:def 2;
then
A3: (rngs F).i = rng f by A2,FUNCT_6:22;
(F||X).i = f|(X.i) by A2,MSAFREE:def 1;
then (rngs (F||X)).i = rng (f|(X.i)) by A2,A1,FUNCT_6:22;
hence thesis by A3,RELAT_1:70;
end;
theorem
for A, B be ManySortedSet of I for F be ManySortedFunction of A, B
holds F is "onto" iff rngs F = B
proof
let A, B be ManySortedSet of I, F be ManySortedFunction of A, B;
A1: dom F = I by PARTFUN1:def 2;
thus F is "onto" implies rngs F = B
proof
assume
A2: F is "onto";
now
let i be object;
assume
A3: i in I;
then reconsider f = F.i as Function of A.i, B.i by PBOOLE:def 15;
rng f = B.i by A2,A3;
hence (rngs F).i = B.i by A1,A3,FUNCT_6:22;
end;
hence thesis;
end;
assume
A4: rngs F = B;
let i be set;
assume i in I;
hence thesis by A1,A4,FUNCT_6:22;
end;
theorem
for X be non-empty ManySortedSet of the carrier of S holds rngs Reverse X = X
proof
let X be non-empty ManySortedSet of the carrier of S;
set I = the carrier of S, R = Reverse X;
now
let i be object such that
A1: i in I;
reconsider r = R.i as Function of (FreeGen X).i, X.i by A1,PBOOLE:def 15;
A2: dom R = I by PARTFUN1:def 2;
thus (rngs R).i = X.i
proof
reconsider s0 = i as SortSymbol of S by A1;
set D = DTConMSA X;
thus (rngs R).i c= X.i
proof
let x be object;
assume x in (rngs R).i;
then
A3: x in rng r by A1,A2,FUNCT_6:22;
rng r c= X.i by RELAT_1:def 19;
hence thesis by A3;
end;
let x be object;
assume x in X.i;
then
A4: [x,s0] in Terminals D by MSAFREE:7;
then reconsider t = [x,s0] as Symbol of D;
t`2 = s0;
then root-tree t in {root-tree tt where tt is Symbol of D : tt in
Terminals D & tt`2 = s0} by A4;
then
A5: root-tree t in FreeGen(s0, X) by MSAFREE:13;
A6: R.s0 = Reverse(s0, X) by MSAFREE:def 18;
then
A7: (R.s0).(root-tree t) = t`1 by A5,MSAFREE:def 17
.= x;
dom (R.s0) = FreeGen(s0, X) by A6,FUNCT_2:def 1;
then (R.s0).(root-tree t) in rng (R.s0) by A5,FUNCT_1:def 3;
hence thesis by A2,A7,FUNCT_6:22;
end;
end;
hence thesis;
end;
theorem
for F be ManySortedFunction of A, B for G be ManySortedFunction of B,
C for X be non-empty ManySortedSubset of B st rngs F c= X holds (G || X) ** F =
G ** F
proof
let F be ManySortedFunction of A, B, G be ManySortedFunction of B, C, X be
non-empty ManySortedSubset of B such that
A1: rngs F c= X;
A2: dom F = I by PARTFUN1:def 2;
A3: F is ManySortedFunction of A, X
proof
let i be object;
assume
A4: i in I;
then reconsider f = F.i as Function of A.i, B.i by PBOOLE:def 15;
A5: (rngs F).i c= X.i by A1,A4;
dom f = A.i & (rngs F).i = rng f by A2,A4,FUNCT_2:def 1,FUNCT_6:22;
hence thesis by A4,A5,FUNCT_2:def 1,RELSET_1:4;
end;
A6: now
let i be object;
assume
A7: i in I;
then reconsider f = F.i as Function of A.i, B.i by PBOOLE:def 15;
(rngs F).i = rng f by A2,A7,FUNCT_6:22;
then
A8: rng f c= X.i by A1,A7;
dom f = A.i by A7,FUNCT_2:def 1;
then reconsider f9 = f as Function of A.i, X.i by A7,A8,FUNCT_2:def 1
,RELSET_1:4;
reconsider g = G.i as Function of B.i, C.i by A7,PBOOLE:def 15;
A9: rng f9 c= X.i by RELAT_1:def 19;
reconsider gx = (G || X).i as Function of X.i, C.i by A7,PBOOLE:def 15;
thus ((G || X) ** F).i = gx * f9 by A3,A7,MSUALG_3:2
.= (g | (X.i)) * f by A7,MSAFREE:def 1
.= g * f9 by A9,MSUHOM_1:1
.= (G ** F).i by A7,MSUALG_3:2;
end;
(G || X) ** F is ManySortedSet of I by A3,Lm1;
hence thesis by A6,PBOOLE:3;
end;
begin :: Other properties of "onto" & "1-1"
theorem Th12:
for F be ManySortedFunction of A, B holds F is "onto" iff for C
for G, H be ManySortedFunction of B, C st G**F = H**F holds G = H
proof
let F be ManySortedFunction of A, B;
thus F is "onto" implies for C for G, H be ManySortedFunction of B, C st G**
F = H**F holds G = H
proof
assume
A1: F is "onto";
let C;
let G, H be ManySortedFunction of B, C such that
A2: G**F = H**F;
now
let i be object;
assume
A3: i in I;
then reconsider f = F.i as Function of A.i, B.i by PBOOLE:def 15;
reconsider h = H.i as Function of B.i, C.i by A3,PBOOLE:def 15;
reconsider g = G.i as Function of B.i, C.i by A3,PBOOLE:def 15;
A4: rng f = B.i by A1,A3;
g*f = (H**F).i by A2,A3,MSUALG_3:2
.= h*f by A3,MSUALG_3:2;
hence G.i = H.i by A3,A4,FUNCT_2:16;
end;
hence thesis;
end;
assume that
A5: for C for G, H be ManySortedFunction of B, C st G**F = H**F holds G = H and
A6: not F is "onto";
consider j be set such that
A7: j in I and
A8: rng (F.j) <> B.j by A6;
reconsider I as non empty set by A7;
reconsider j as Element of I by A7;
reconsider A,B as ManySortedSet of I;
reconsider F as ManySortedFunction of A,B;
reconsider f =F.j as Function of A.j,B.j;
consider Z be set such that
A9: Z <> {} and
A10: ex g, h be Function of B.j, Z st g*f = h*f & g <> h by A8,FUNCT_2:16;
consider g, h be Function of B.j, Z such that
A11: g*(F.j) = h*(F.j) and
A12: g <> h by A10;
ex C be ManySortedSet of I st C is non-empty & ex G, H be
ManySortedFunction of B, C st G**F = H**F & G <> H
proof
deffunc F(object) = IFEQ($1, j, Z, B.$1);
consider C be ManySortedSet of I such that
A13: for i be object st i in I holds C.i = F(i) from PBOOLE:sch 4;
take C;
thus C is non-empty
proof
let i be object such that
A14: i in I;
now
per cases;
case
i = j;
then IFEQ(i, j, Z, B.i) = Z by FUNCOP_1:def 8;
hence thesis by A9,A13,A14;
end;
case
i <> j;
then IFEQ(i, j, Z, B.i) = B.i by FUNCOP_1:def 8;
hence thesis by A13,A14;
end;
end;
hence thesis;
end;
deffunc F(object) = IFEQ($1, j, g, (id B).$1);
consider G be ManySortedSet of I such that
A15: for i be object st i in I holds G.i = F(i) from PBOOLE:sch 4;
deffunc F(object) = IFEQ($1, j, h, (id B).$1);
consider H be ManySortedSet of I such that
A16: for i be object st i in I holds H.i = F(i) from PBOOLE:sch 4;
now
let G be ManySortedSet of I;
let g, h be Function of B.j, Z such that
g*(F.j) = h*(F.j) and
g <> h and
A17: for i be object st i in I holds G.i = IFEQ(i, j, g, (id B).i);
thus G is Function-yielding
proof
let i be object;
assume i in dom G;
then
A18: i in I;
now
per cases;
case
i = j;
then IFEQ(i, j, g, (id B).i) = g by FUNCOP_1:def 8;
hence thesis by A17,A18;
end;
case
i <> j;
then IFEQ(i, j, g, (id B).i) = (id B).i by FUNCOP_1:def 8;
hence thesis by A17,A18;
end;
end;
hence thesis;
end;
end;
then reconsider G, H as ManySortedFunction of I by A11,A12,A15,A16;
now
let G be ManySortedFunction of I;
let g, h be Function of B.j, Z such that
g*(F.j) = h*(F.j) and
g <> h and
A19: for i be object st i in I holds G.i = IFEQ(i, j, g, (id B).i);
thus G is ManySortedFunction of B, C
proof
let i be object such that
A20: i in I;
now
per cases;
case
A21: i = j;
then
A22: IFEQ(i, j, Z, B.i) = Z by FUNCOP_1:def 8;
IFEQ(i, j, g, (id B).i) = g & C.i = IFEQ(i, j, Z, B.i) by A13,A21,
FUNCOP_1:def 8;
hence thesis by A19,A21,A22;
end;
case
A23: i <> j;
then IFEQ(i, j, Z, B.i) = B.i by FUNCOP_1:def 8;
then
A24: B.i = C.i by A13,A20;
IFEQ(i, j, g, (id B).i) = (id B).i by A23,FUNCOP_1:def 8;
then G.i = (id B).i by A19,A20;
hence thesis by A20,A24,PBOOLE:def 15;
end;
end;
hence thesis;
end;
end;
then reconsider G, H as ManySortedFunction of B, C by A11,A12,A15,A16;
A25: now
let i be object such that
A26: i in I;
now
per cases;
case
A27: i = j;
then IFEQ(i, j, h, (id B).i) = h by FUNCOP_1:def 8;
then
A28: h = H.i by A16,A26;
IFEQ(i, j, g, (id B).i) = g by A27,FUNCOP_1:def 8;
then g = G.i by A15,A26;
hence (G**F).i = h*(F.j) by A11,A27,MSUALG_3:2
.= (H**F).i by A27,A28,MSUALG_3:2;
end;
case
A29: i <> j;
reconsider g9 = G.i as Function of B.i, C.i by A26,PBOOLE:def 15;
reconsider f9 = F.i as Function of A.i, B.i by A26,PBOOLE:def 15;
reconsider h9 = H.i as Function of B.i, C.i by A26,PBOOLE:def 15;
A30: IFEQ(i, j, h, (id B).i) = (id B).i by A29,FUNCOP_1:def 8;
IFEQ(i, j, g, (id B).i) = (id B).i by A29,FUNCOP_1:def 8;
then g9 = (id B).i by A15,A26
.= h9 by A16,A26,A30;
hence (G**F).i = h9*f9 by A26,MSUALG_3:2
.= (H**F).i by A26,MSUALG_3:2;
end;
end;
hence (G**F).i = (H**F).i;
end;
take G, H;
G**F is ManySortedSet of I & H**F is ManySortedSet of I by Lm1;
hence G**F = H**F by A25,PBOOLE:3;
ex i be set st i in I & G.i <> H.i
proof
take i = j;
thus i in I;
A31: h = IFEQ(i, j, h, (id B).i) by FUNCOP_1:def 8
.= H.i by A16;
g = IFEQ(i, j, g, (id B).i) by FUNCOP_1:def 8
.= G.i by A15;
hence thesis by A12,A31;
end;
hence thesis;
end;
hence contradiction by A5;
end;
theorem Th13:
for F be ManySortedFunction of A, B st A is non-empty holds F is
"1-1" iff for C be ManySortedSet of I for G, H be ManySortedFunction of C, A st
F**G = F**H holds G = H
proof
let F be ManySortedFunction of A, B such that
A1: A is non-empty;
thus F is "1-1" implies for C be ManySortedSet of I for G, H be
ManySortedFunction of C, A st F**G = F**H holds G = H
proof
assume
A2: F is "1-1";
let C be ManySortedSet of I;
let G, H be ManySortedFunction of C, A such that
A3: F**G = F**H;
now
let i be object;
assume
A4: i in I;
then reconsider f = F.i as Function of A.i, B.i by PBOOLE:def 15;
reconsider h = H.i as Function of C.i, A.i by A4,PBOOLE:def 15;
reconsider g = G.i as Function of C.i, A.i by A4,PBOOLE:def 15;
A5: f is one-to-one by A2,A4,MSUALG_3:1;
f*g = (F**H).i by A3,A4,MSUALG_3:2
.= f*h by A4,MSUALG_3:2;
hence G.i = H.i by A1,A4,A5,FUNCT_2:21;
end;
hence thesis;
end;
assume that
A6: for C be ManySortedSet of I for G, H be ManySortedFunction of C, A
st F**G = F**H holds G = H and
A7: not F is "1-1";
consider j be set such that
A8: j in I and
A9: not (F.j) is one-to-one by A7,MSUALG_3:1;
F.j is Function of A.j, B.j by A8,PBOOLE:def 15;
then consider Z be set such that
A10: ex g, h be Function of Z, A.j st (F.j)*g = (F.j)*h & g <> h by A1,A8,A9,
FUNCT_2:21;
consider g, h be Function of Z, A.j such that
A11: (F.j)*g = (F.j)*h and
A12: g <> h by A10;
ex C be ManySortedSet of I st ex G, H be ManySortedFunction of C, A st
F**G = F**H & G <> H
proof
deffunc F(object) = IFEQ($1, j, Z, A.$1);
consider C be ManySortedSet of I such that
A13: for i be object st i in I holds C.i = F(i) from PBOOLE:sch 4;
take C;
deffunc F(object) = IFEQ($1, j, g, (id C).$1);
consider G be ManySortedSet of I such that
A14: for i be object st i in I holds G.i = F(i) from PBOOLE:sch 4;
deffunc F(object) = IFEQ($1, j, h, (id C).$1);
consider H be ManySortedSet of I such that
A15: for i be object st i in I holds H.i = F(i) from PBOOLE:sch 4;
now
let G be ManySortedSet of I;
let g, h be Function of Z, A.j such that
(F.j)*g = (F.j)*h and
g <> h and
A16: for i be object st i in I holds G.i = IFEQ(i, j, g, (id C).i);
thus G is Function-yielding
proof
let i be object;
assume i in dom G;
then
A17: i in I;
now
per cases;
case
i = j;
then IFEQ(i, j, g, (id C).i) = g by FUNCOP_1:def 8;
hence thesis by A16,A17;
end;
case
i <> j;
then IFEQ(i, j, g, (id C).i) = (id C).i by FUNCOP_1:def 8;
hence thesis by A16,A17;
end;
end;
hence thesis;
end;
end;
then reconsider G, H as ManySortedFunction of I by A11,A12,A14,A15;
now
let G be ManySortedFunction of I;
let g, h be Function of Z, A.j such that
(F.j)*g = (F.j)*h and
g <> h and
A18: for i be object st i in I holds G.i = IFEQ(i, j, g, (id C).i);
thus G is ManySortedFunction of C, A
proof
let i be object such that
A19: i in I;
now
per cases;
case
A20: i = j;
then
A21: IFEQ(i, j, g, (id C).i) = g & IFEQ(i, j, Z, A.i) = Z by
FUNCOP_1:def 8;
C.i = IFEQ(i, j, Z, A.i) by A13,A19;
hence thesis by A18,A19,A20,A21;
end;
case
A22: i <> j;
then IFEQ(i, j, Z, A.i) = A.i by FUNCOP_1:def 8;
then
A23: C.i = A.i by A13,A19;
IFEQ(i, j, g, (id C).i) = (id C).i by A22,FUNCOP_1:def 8;
then G.i = (id C).i by A18,A19;
hence thesis by A19,A23,PBOOLE:def 15;
end;
end;
hence thesis;
end;
end;
then reconsider G, H as ManySortedFunction of C, A by A11,A12,A14,A15;
A24: now
let i be object such that
A25: i in I;
now
per cases;
case
A26: i = j;
then IFEQ(i, j, h, (id C).i) = h by FUNCOP_1:def 8;
then
A27: h = H.i by A15,A25;
IFEQ(i, j, g, (id C).i) = g by A26,FUNCOP_1:def 8;
then g = G.i by A14,A25;
hence (F**G).i = (F.j)*h by A8,A11,A26,MSUALG_3:2
.= (F**H).i by A8,A26,A27,MSUALG_3:2;
end;
case
A28: i <> j;
reconsider g9 = G.i as Function of C.i, A.i by A25,PBOOLE:def 15;
reconsider f9 = F.i as Function of A.i, B.i by A25,PBOOLE:def 15;
reconsider h9 = H.i as Function of C.i, A.i by A25,PBOOLE:def 15;
A29: IFEQ(i, j, h, (id C).i) = (id C).i by A28,FUNCOP_1:def 8;
IFEQ(i, j, g, (id C).i) = (id C).i by A28,FUNCOP_1:def 8;
then g9 = (id C).i by A14,A25
.= h9 by A15,A25,A29;
hence (F**G).i = f9*h9 by A25,MSUALG_3:2
.= (F**H).i by A25,MSUALG_3:2;
end;
end;
hence (F**G).i = (F**H).i;
end;
take G, H;
F**G is ManySortedSet of I & F**H is ManySortedSet of I by Lm1;
hence F**G = F**H by A24,PBOOLE:3;
ex i be set st i in I & G.i <> H.i
proof
take i = j;
thus i in I by A8;
A30: h = IFEQ(i, j, h, (id C).i) by FUNCOP_1:def 8
.= H.i by A8,A15;
g = IFEQ(i, j, g, (id C).i) by FUNCOP_1:def 8
.= G.i by A8,A14;
hence thesis by A12,A30;
end;
hence thesis;
end;
hence contradiction by A6;
end;
begin :: Extensions of Mappings on Generator Set
theorem Th14:
for X be non-empty ManySortedSet of the carrier of S for h1, h2
be ManySortedFunction of FreeMSA X, U1 st h1 is_homomorphism FreeMSA X, U1 & h2
is_homomorphism FreeMSA X, U1 & h1 || FreeGen (X) = h2 || FreeGen (X) holds h1
= h2
proof
let X be non-empty ManySortedSet of the carrier of S, h1, h2 be
ManySortedFunction of FreeMSA X, U1;
assume that
A1: h1 is_homomorphism FreeMSA X, U1 and
A2: h2 is_homomorphism FreeMSA X, U1 and
A3: h1 || FreeGen (X) = h2 || FreeGen (X);
A4: h2 is_homomorphism FreeMSA X, U1 by A2;
defpred P[SortSymbol of S,set,set] means h1.$1.$3 = $2;
A5: for s be SortSymbol of S, x, y be set st y in FreeGen(s,X) holds h2.s.y
= x iff P[s,x,y]
proof
set FG = FreeGen X;
let s be SortSymbol of S, x, y be set;
assume y in FreeGen(s, X);
then
A6: y in FG.s by MSAFREE:def 16;
A7: (h1 || FG).s = (h1.s) | (FG.s) & (h2 || FG).s = (h2.s) | (FG.s) by
MSAFREE:def 1;
((h1.s) | (FG.s)).y = h1.s.y by A6,FUNCT_1:49;
hence thesis by A3,A7,A6,FUNCT_1:49;
end;
A8: for s be SortSymbol of S, x, y be set st y in FreeGen(s,X) holds h1.s.y
= x iff P[s,x,y];
A9: h1 is_homomorphism FreeMSA X, U1 by A1;
thus h1 = h2 from MSAFREE1:sch 3 (A9, A8, A4, A5);
end;
theorem
for F be ManySortedFunction of U1, U2 st F is_epimorphism U1, U2 for
U3 be non-empty MSAlgebra over S for h1, h2 be ManySortedFunction of U2, U3 st
h1**F = h2**F holds h1 = h2 by Th12;
theorem
for F be ManySortedFunction of U2, U3 st F is_homomorphism U2, U3
holds F is_monomorphism U2, U3 iff for U1 be non-empty MSAlgebra over S for h1,
h2 be ManySortedFunction of U1, U2 st h1 is_homomorphism U1, U2 & h2
is_homomorphism U1, U2 holds (F**h1 = F**h2 implies h1 = h2)
proof
let F be ManySortedFunction of U2, U3 such that
A1: F is_homomorphism U2, U3;
set C = the Sorts of U3;
set B = the Sorts of U2;
thus F is_monomorphism U2, U3 implies for U1 be non-empty MSAlgebra over S
for h1, h2 be ManySortedFunction of U1, U2 st h1 is_homomorphism U1, U2 & h2
is_homomorphism U1, U2 holds (F**h1 = F**h2 implies h1 = h2)
by Th13;
set I = the carrier of S;
assume that
A2: for U1 be non-empty MSAlgebra over S for h1, h2 be
ManySortedFunction of U1, U2 st h1 is_homomorphism U1, U2 & h2 is_homomorphism
U1, U2 holds F**h1 = F**h2 implies h1 = h2 and
A3: not F is_monomorphism U2, U3;
not F is "1-1" by A1,A3;
then consider j be set such that
A4: j in I and
A5: not F.j is one-to-one by MSUALG_3:1;
set f = F.j;
F.j is Function of B.j, C.j by A4,PBOOLE:def 15;
then consider x1, x2 be object such that
A6: x1 in B.j and
A7: x2 in B.j and
A8: f.x1 = f.x2 and
A9: x1 <> x2 by A4,A5,FUNCT_2:19;
ex U1 be non-empty MSAlgebra over S st ex h1, h2 be ManySortedFunction
of the Sorts of U1, the Sorts of U2 st h1 is_homomorphism U1, U2 & h2
is_homomorphism U1, U2 & F**h1 = F**h2 & h1 <> h2
proof
take U1 = FreeMSA the Sorts of U2;
reconsider FG = FreeGen(B) as GeneratorSet of U1;
FG is non-empty by MSAFREE:14;
then reconsider FGj = FG.j, Bj = B.j as non empty set by A4;
reconsider h = FGj --> x2 as Function of FGj, Bj by A7,FUNCOP_1:45;
reconsider g = FGj --> x1 as Function of FGj, Bj by A6,FUNCOP_1:45;
set r = Reverse(B);
deffunc F(object) = IFEQ($1, j, g, r.$1);
consider G be ManySortedSet of I such that
A10: for i be object st i in I holds G.i = F(i) from PBOOLE:sch 4;
deffunc F(object) = IFEQ($1, j, h, r.$1);
consider H be ManySortedSet of I such that
A11: for i be object st i in I holds H.i = F(i) from PBOOLE:sch 4;
now
let G be ManySortedSet of I;
let g, h be Function of FGj, Bj such that
A12: for i be object st i in I holds G.i = IFEQ(i, j, g, r.i);
thus G is Function-yielding
proof
let i be object;
assume i in dom G;
then
A13: i in I;
now
per cases;
case
i = j;
then IFEQ(i, j, g, r.i) = g by FUNCOP_1:def 8;
hence thesis by A12,A13;
end;
case
i <> j;
then IFEQ(i, j, g, r.i) = r.i by FUNCOP_1:def 8;
hence thesis by A12,A13;
end;
end;
hence thesis;
end;
end;
then reconsider G, H as ManySortedFunction of I by A10,A11;
now
let G be ManySortedFunction of I;
let g, h be Function of FGj, Bj such that
A14: for i be object st i in I holds G.i = IFEQ(i, j, g, r.i);
thus G is ManySortedFunction of FG, B
proof
let i be object such that
A15: i in I;
now
per cases;
case
A16: i = j;
then IFEQ(i, j, g, r.i) = g by FUNCOP_1:def 8;
hence thesis by A14,A15,A16;
end;
case
i <> j;
then IFEQ(i, j, g, r.i) = r.i by FUNCOP_1:def 8;
then G.i = r.i by A14,A15;
hence thesis by A15,PBOOLE:def 15;
end;
end;
hence thesis;
end;
end;
then reconsider G, H as ManySortedFunction of FG, B by A10,A11;
A17: FG is free by MSAFREE:16;
then consider h1 be ManySortedFunction of U1, U2 such that
A18: h1 is_homomorphism U1, U2 and
A19: h1 || FG = G by MSAFREE:def 5;
consider h2 be ManySortedFunction of U1, U2 such that
A20: h2 is_homomorphism U1, U2 and
A21: h2 || FG = H by A17,MSAFREE:def 5;
take h1, h2;
thus h1 is_homomorphism U1, U2 & h2 is_homomorphism U1, U2 by A18,A20;
reconsider Fh1 = F**h1, Fh2 = F**h2 as ManySortedFunction of U1, U3;
A22: Fh1 is_homomorphism U1, U3 by A1,A18,MSUALG_3:10;
now
let i be object;
assume
A23: i in I;
now
per cases;
case
A24: i = j;
then
A25: f is Function of B.i, C.i by A4,PBOOLE:def 15;
then reconsider fg = f*g as Function of FGj, C.i by A24,FUNCT_2:13;
reconsider fh = f*h as Function of FGj, C.i by A24,A25,FUNCT_2:13;
now
let x be object;
assume
A26: x in FGj;
hence fg.x = f.(g.x) by FUNCT_2:15
.= f.x2 by A8,A26,FUNCOP_1:7
.= f.(h.x) by A26,FUNCOP_1:7
.= fh.x by A26,FUNCT_2:15;
end;
then
A27: f*g = f*h by FUNCT_2:12;
IFEQ(i, j, g, r.i) = g by A24,FUNCOP_1:def 8;
then g = (h1 || FG).i by A10,A19,A23;
then
A28: (F**(h1 || FG)).i = f*g by A4,A24,MSUALG_3:2;
IFEQ(i, j, h, r.i) = h by A24,FUNCOP_1:def 8;
then h = (h2 || FG).i by A11,A21,A23;
hence (F**(h1 || FG)).i = (F**(h2 || FG)).i by A4,A24,A27,A28,
MSUALG_3:2;
end;
case
A29: i <> j;
reconsider f9 = F.i as Function of B.i, C.i by A23,PBOOLE:def 15;
reconsider h29 = (h2 || FG).i as Function of FG.i, B.i by A23,
PBOOLE:def 15;
A30: IFEQ(i, j, h, r.i) = r.i by A29,FUNCOP_1:def 8;
IFEQ(i, j, g, r.i) = r.i by A29,FUNCOP_1:def 8;
then (h1 || FG).i = r.i by A10,A19,A23
.= (h2 || FG).i by A11,A21,A23,A30;
hence (F**(h1 || FG)).i = f9*h29 by A23,MSUALG_3:2
.= (F**(h2 || FG)).i by A23,MSUALG_3:2;
end;
end;
hence (F**(h1 || FG)).i = (F**(h2 || FG)).i;
end;
then
A31: F**(h1 || FG) = F**(h2 || FG);
A32: Fh2 is_homomorphism U1, U3 by A1,A20,MSUALG_3:10;
(F**h1) || FG = F**(h1 || FG) by Th4
.= (F**h2) || FG by A31,Th4;
hence F**h1 = F**h2 by A22,A32,Th14;
now
take i = j;
thus i in I by A4;
A33: now
let x be Element of FGj;
assume g = h;
then g.x = x2 by FUNCOP_1:7;
hence contradiction by A9;
end;
A34: h = IFEQ(i, j, h, r.i) by FUNCOP_1:def 8
.= H.i by A4,A11;
g = IFEQ(i, j, g, r.i) by FUNCOP_1:def 8
.= G.i by A4,A10;
hence G <> H by A34,A33;
end;
hence thesis by A19,A21;
end;
hence contradiction by A2;
end;
registration
let S, U1;
cluster non-empty for GeneratorSet of U1;
existence
proof
the Sorts of U1 is GeneratorSet of U1 by MSAFREE2:6;
then consider G be GeneratorSet of U1 such that
A1: G = the Sorts of U1;
take G;
thus thesis by A1;
end;
end;
theorem
for U1 being MSAlgebra over S for A, B being MSSubset of U1 st A is
ManySortedSubset of B holds GenMSAlg A is MSSubAlgebra of GenMSAlg B
proof
let U1 be MSAlgebra over S, A, B be MSSubset of U1;
B is MSSubset of GenMSAlg B by MSUALG_2:def 17;
then
A1: B c= the Sorts of GenMSAlg B by PBOOLE:def 18;
assume A is ManySortedSubset of B;
then A c= B by PBOOLE:def 18;
then A c= the Sorts of GenMSAlg B by A1,PBOOLE:13;
then A is MSSubset of GenMSAlg B by PBOOLE:def 18;
hence thesis by MSUALG_2:def 17;
end;
theorem
for U1 being MSAlgebra over S, U2 being MSSubAlgebra of U1 for B1
being MSSubset of U1, B2 being MSSubset of U2 st B1 = B2 holds GenMSAlg B1 =
GenMSAlg B2
proof
let U1 be MSAlgebra over S, U2 be MSSubAlgebra of U1, B1 be MSSubset of U1,
B2 be MSSubset of U2 such that
A1: B1 = B2;
reconsider H = GenMSAlg B1 as MSSubAlgebra of U2 by A1,MSUALG_2:def 17;
reconsider G = GenMSAlg B2 as MSSubAlgebra of U1 by MSUALG_2:6;
B1 is MSSubset of G by A1,MSUALG_2:def 17;
then
A2: GenMSAlg B1 is MSSubAlgebra of G by MSUALG_2:def 17;
B1 is MSSubset of H by MSUALG_2:def 17;
then GenMSAlg B2 is MSSubAlgebra of GenMSAlg B1 by A1,MSUALG_2:def 17;
hence thesis by A2,MSUALG_2:7;
end;
theorem
for U1 being non-empty MSAlgebra over S for U2 being non-empty
MSAlgebra over S for Gen being GeneratorSet of U1 for h1, h2 being
ManySortedFunction of U1, U2 st h1 is_homomorphism U1, U2 & h2 is_homomorphism
U1, U2 & h1 || Gen = h2 || Gen holds h1 = h2
proof
let U1 be non-empty MSAlgebra over S, U2 be non-empty MSAlgebra over
S, Gen be GeneratorSet of U1, h1, h2 be ManySortedFunction of U1, U2 such that
A1: h1 is_homomorphism U1, U2 and
A2: h2 is_homomorphism U1, U2 and
A3: h1 || Gen = h2 || Gen;
defpred P[object,object] means
ex s being SortSymbol of S st $1 = s & h1.s.$2 = h2.s.$2;
set I = the carrier of S;
consider A being ManySortedSet of I such that
A4: for i being object st i in I
for e being object holds e in A.i iff e in (
the Sorts of U1).i & P[i,e] from PBOOLE:sch 2;
A is ManySortedSubset of the Sorts of U1
proof
let i be object such that
A5: i in I;
let e be object;
assume e in A.i;
hence thesis by A4,A5;
end;
then reconsider A as MSSubset of U1;
A is opers_closed
proof
let o be OperSymbol of S;
let y be object;
set r = the_result_sort_of o;
set ar = the_arity_of o;
assume y in rng ((Den(o,U1))|((A# * the Arity of S).o));
then consider x being object such that
A6: x in dom ((Den(o,U1))|((A# * the Arity of S).o)) and
A7: ((Den(o,U1))|((A# * the Arity of S).o)).x = y by FUNCT_1:def 3;
A8: x in (A# * the Arity of S).o by A6,RELAT_1:57;
then x in A#.((the Arity of S).o) by FUNCT_2:15;
then x in A#.ar by MSUALG_1:def 1;
then
A9: x in product(A*ar) by FINSEQ_2:def 5;
reconsider x as Element of Args(o,U1) by A6;
A10: y = Den(o,U1).x by A7,A8,FUNCT_1:49;
A11: dom (h1#x) = dom ar by MSUALG_3:6;
A12: for n being object st n in dom (h1#x) holds (h1#x).n = (h2#x).n
proof
let n be object;
A13: dom x = dom ar by MSUALG_3:6;
assume
A14: n in dom (h1#x);
then reconsider n9 = n as Nat by A11,ORDINAL1:def 12;
dom x = dom (A*ar) by A9,CARD_3:9;
then x.n in (A*ar).n by A9,A11,A14,A13,CARD_3:9;
then x.n in A.(ar.n) by A11,A14,FUNCT_1:13;
then x.n in A.(ar/.n) by A11,A14,PARTFUN1:def 6;
then ex s being SortSymbol of S st s = ar/.n & h1.s.(x.n) = h2.s.(x.n)
by A4;
hence (h1#x).n = h2.(ar/.n).(x.n9) by A11,A14,A13,MSUALG_3:def 6
.= (h2#x).n by A11,A14,A13,MSUALG_3:def 6;
end;
Den(o,U1).x is Element of ((the Sorts of U1)*the ResultSort of S).o
by MSUALG_1:def 5;
then
Den(o,U1).x is Element of (the Sorts of U1).((the ResultSort of S). o
) by FUNCT_2:15;
then
A15: Den(o,U1).x is Element of (the Sorts of U1).r by MSUALG_1:def 2;
A16: dom (h2#x) = dom ar by MSUALG_3:6;
h1.r.y = h1.r.(Den(o,U1).x) by A7,A8,FUNCT_1:49
.= Den(o,U2).(h1#x) by A1
.= Den(o,U2).(h2#x) by A16,A12,FUNCT_1:2,MSUALG_3:6
.= h2.r.(Den(o,U1).x) by A2
.= h2.r.y by A7,A8,FUNCT_1:49;
then y in A.r by A4,A10,A15;
then y in A.((the ResultSort of S).o) by MSUALG_1:def 2;
hence thesis by FUNCT_2:15;
end;
then
A17: U1|A = MSAlgebra (#A, Opers(U1,A)#) by MSUALG_2:def 15;
Gen is ManySortedSubset of the Sorts of U1|A
proof
let i be object such that
A18: i in I;
reconsider s = i as SortSymbol of S by A18;
Gen c= the Sorts of U1 by PBOOLE:def 18;
then
A19: Gen.i c= (the Sorts of U1).i by A18;
let x be object such that
A20: x in Gen.i;
h1.s.x = ((h1.s) | (Gen.s)).x by A20,FUNCT_1:49
.= (h1 || Gen).s.x by MSAFREE:def 1
.= ((h2.s) | (Gen.s)).x by A3,MSAFREE:def 1
.= h2.s.x by A20,FUNCT_1:49;
hence thesis by A4,A17,A20,A19;
end;
then
A21: GenMSAlg Gen is MSSubAlgebra of U1|A by MSUALG_2:def 17;
the Sorts of GenMSAlg Gen = the Sorts of U1 by MSAFREE:def 4;
then the Sorts of U1 is ManySortedSubset of A by A17,A21,MSUALG_2:def 9;
then
A22: the Sorts of U1 c= A by PBOOLE:def 18;
now
let i be object;
assume
A23: i in I;
then reconsider s = i as SortSymbol of S;
A24: dom (h1.s) = (the Sorts of U1).i by FUNCT_2:def 1;
A25: now
A26: (the Sorts of U1).i c= A.i by A22,A23;
let x be object;
assume x in dom (h1.s);
then
ex t being SortSymbol of S st t = s & h1.t.x = h2.t.x by A4,A24,A26;
hence h1.s.x = h2.s.x;
end;
dom (h2.s) = (the Sorts of U1).i by FUNCT_2:def 1;
hence h1.i = h2.i by A24,A25,FUNCT_1:2;
end;
hence thesis;
end;