:: Extensions of Mappings on Generator Set
:: by Artur Korni{\l}owicz
::
:: Received March 23, 1995
:: Copyright (c) 1995-2016 Association of Mizar Users

environ

vocabularies HIDDEN, 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 HIDDEN, 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;
definitions MSUALG_2, MSUALG_3, PBOOLE, FUNCOP_1, TARSKI, XBOOLE_0;
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;
registrations FUNCT_1, RELSET_1, FUNCOP_1, PBOOLE, STRUCT_0, MSUALG_1, MSUALG_3, MSAFREE, MSSUBFAM, FINSEQ_1, XTUPLE_0;
constructors HIDDEN, PZFMISC1, MSUALG_3, MSAFREE, RELSET_1, XTUPLE_0;
requirements HIDDEN, SUBSET, BOOLE;
equalities XBOOLE_0;
expansions MSUALG_3, PBOOLE;


Lm1: for I being set
for A, B, C being ManySortedSet of I
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C holds G ** F is ManySortedSet of I
proof end;

theorem :: EXTENS_1:1
for I being set
for A being ManySortedSet of I
for B being V2() ManySortedSet of I
for F being ManySortedFunction of A,B
for X being ManySortedSubset of A st A c= X holds
F || X = F
proof end;

theorem :: EXTENS_1:2
for I being set
for A, B being ManySortedSet of I
for M being ManySortedSubset of A
for F being ManySortedFunction of A,B holds F .:.: M c= F .:.: A
proof end;

theorem :: EXTENS_1:3
for I being set
for A being ManySortedSet of I
for B being V2() ManySortedSet of I
for F being ManySortedFunction of A,B
for M1, M2 being ManySortedSubset of A st M1 c= M2 holds
(F || M2) .:.: M1 = F .:.: M1
proof end;

theorem Th4: :: EXTENS_1:4
for I being set
for A being ManySortedSet of I
for B, C being V2() ManySortedSet of I
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C
for X being ManySortedSubset of A holds (G ** F) || X = G ** (F || X)
proof end;

theorem :: EXTENS_1:5
for I being set
for A, B being ManySortedSet of I st A is_transformable_to B holds
for F being ManySortedFunction of A,B
for C being ManySortedSet of I st B is ManySortedSubset of C holds
F is ManySortedFunction of A,C
proof end;

theorem :: EXTENS_1:6
for I being set
for A being ManySortedSet of I
for B being V2() ManySortedSet of I
for F being ManySortedFunction of A,B
for X being ManySortedSubset of A st F is "1-1" holds
F || X is "1-1"
proof end;

theorem :: EXTENS_1:7
for I being set
for A being ManySortedSet of I
for B being V2() ManySortedSet of I
for F being ManySortedFunction of A,B
for X being ManySortedSubset of A holds doms (F || X) c= doms F
proof end;

theorem :: EXTENS_1:8
for I being set
for A being ManySortedSet of I
for B being V2() ManySortedSet of I
for F being ManySortedFunction of A,B
for X being ManySortedSubset of A holds rngs (F || X) c= rngs F
proof end;

theorem :: EXTENS_1:9
for I being set
for A, B being ManySortedSet of I
for F being ManySortedFunction of A,B holds
( F is "onto" iff rngs F = B )
proof end;

theorem :: EXTENS_1:10
for S being non empty non void ManySortedSign
for X being V2() ManySortedSet of the carrier of S holds rngs (Reverse X) = X
proof end;

theorem :: EXTENS_1:11
for I being set
for A being ManySortedSet of I
for B, C being V2() ManySortedSet of I
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C
for X being V2() ManySortedSubset of B st rngs F c= X holds
(G || X) ** F = G ** F
proof end;

theorem Th12: :: EXTENS_1:12
for I being set
for A being ManySortedSet of I
for B being V2() ManySortedSet of I
for F being ManySortedFunction of A,B holds
( F is "onto" iff for C being V2() ManySortedSet of I
for G, H being ManySortedFunction of B,C st G ** F = H ** F holds
G = H )
proof end;

theorem Th13: :: EXTENS_1:13
for I being set
for A being ManySortedSet of I
for B being V2() ManySortedSet of I
for F being ManySortedFunction of A,B st A is V2() holds
( F is "1-1" iff for C being ManySortedSet of I
for G, H being ManySortedFunction of C,A st F ** G = F ** H holds
G = H )
proof end;

theorem Th14: :: EXTENS_1:14
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for X being V2() ManySortedSet of the carrier of S
for h1, h2 being 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 end;

theorem :: EXTENS_1:15
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 holds
for U3 being non-empty MSAlgebra over S
for h1, h2 being ManySortedFunction of U2,U3 st h1 ** F = h2 ** F holds
h1 = h2 by Th12;

theorem :: EXTENS_1:16
for S being non empty non void ManySortedSign
for U2, U3 being non-empty MSAlgebra over S
for F being ManySortedFunction of U2,U3 st F is_homomorphism U2,U3 holds
( F is_monomorphism U2,U3 iff for U1 being non-empty MSAlgebra over S
for h1, h2 being ManySortedFunction of U1,U2 st h1 is_homomorphism U1,U2 & h2 is_homomorphism U1,U2 & F ** h1 = F ** h2 holds
h1 = h2 )
proof end;

registration
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra over S;
cluster Relation-like V2() the carrier of S -defined Function-like non empty total for GeneratorSet of U1;
existence
not for b1 being GeneratorSet of U1 holds b1 is V2()
proof end;
end;

theorem :: EXTENS_1:17
for S being non empty non void ManySortedSign
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 end;

theorem :: EXTENS_1:18
for S being non empty non void ManySortedSign
for U1 being MSAlgebra over S
for U2 being MSSubAlgebra of U1
for B1 being MSSubset of U1
for B2 being MSSubset of U2 st B1 = B2 holds
GenMSAlg B1 = GenMSAlg B2
proof end;

theorem :: EXTENS_1:19
for S being non empty non void ManySortedSign
for U1, 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 end;