Volume 8, 1996

University of Bialystok

Copyright (c) 1996 Association of Mizar Users

### The abstract of the Mizar article:

### More on Products of Many Sorted Algebras

**by****Mariusz Giero**- Received April 29, 1996
- MML identifier: PRALG_3

- [ Mizar article, MML identifier index ]

environ vocabulary PBOOLE, AMI_1, MSUALG_1, PRALG_2, EQREL_1, FUNCT_1, CARD_3, ZF_REFLE, RELAT_1, BOOLE, RLVECT_2, FUNCT_2, PRALG_1, FRAENKEL, TARSKI, QC_LANG1, UNIALG_2, FUNCT_5, CQC_LANG, FUNCT_6, TDGROUP, FINSEQ_4, FINSEQ_1, BORSUK_1, ALG_1, MSUALG_3, ARYTM_3, WELLORD1, GROUP_6, PRALG_3; notation TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, STRUCT_0, FUNCT_2, FRAENKEL, CQC_LANG, EQREL_1, FINSEQ_1, FUNCT_5, FUNCT_6, CARD_3, PBOOLE, MSUALG_1, MSUALG_3, PRALG_2, AMI_1, FINSEQ_4, PRALG_1, MSUALG_2; constructors EQREL_1, AMI_1, PRALG_2, FINSEQ_4, MSUALG_3, TOLER_1; clusters SUBSET_1, STRUCT_0, MSUALG_1, FUNCT_1, PBOOLE, AMI_1, PUA2MSS1, RELAT_1, MSUALG_3, PRALG_1, RELSET_1, MSAFREE, PRALG_2, FILTER_1, EQREL_1, TOLER_1, PARTFUN1; requirements NUMERALS, BOOLE, SUBSET; begin ::Preliminaries ::------------------------------------------------------------------- :: Acknowledgements: :: ================ :: :: I would like to thank Professor A.Trybulec for his help in the preparation :: of the article. ::------------------------------------------------------------------- reserve I for non empty set, J for ManySortedSet of I, S for non void non empty ManySortedSign, i for Element of I, c for set, A for MSAlgebra-Family of I,S, EqR for Equivalence_Relation of I, U0,U1,U2 for MSAlgebra over S, s for SortSymbol of S, o for OperSymbol of S, f for Function; definition let I be set, S; let AF be MSAlgebra-Family of I,S; cluster product AF -> non-empty; end; definition let I be set; redefine func id I -> ManySortedSet of I; end; definition let I, EqR; cluster Class EqR -> with_non-empty_elements; end; definition let X be with_non-empty_elements set; redefine func id X -> non-empty ManySortedSet of X; end; theorem :: PRALG_3:1 for f,F being Function, A being set st f in product F holds f|A in product(F|A); theorem :: PRALG_3:2 for A be MSAlgebra-Family of I,S, s be SortSymbol of S, a be non empty Subset of I, Aa be MSAlgebra-Family of a,S st A|a = Aa holds Carrier(Aa,s) = (Carrier(A,s))|a; theorem :: PRALG_3:3 for i be set, I be non empty set, EqR be Equivalence_Relation of I, c1,c2 be Element of Class EqR st i in c1 & i in c2 holds c1 = c2; theorem :: PRALG_3:4 for X,Y being set for f being Function st f in Funcs(X,Y) holds dom f = X & rng f c= Y; theorem :: PRALG_3:5 for D being non empty set for F being ManySortedFunction of D for C being with_common_domain functional non empty set st C = rng F for d being Element of D,e being set st d in dom F & e in DOM C holds F.d.e = (commute F).e.d; begin :: Constants of Many Sorted Algebras definition let S,U0; let o be OperSymbol of S; func const(o,U0) equals :: PRALG_3:def 1 Den(o,U0).{}; end; theorem :: PRALG_3:6 the_arity_of o = {} & Result(o,U0) <> {} implies const(o,U0) in Result(o,U0); theorem :: PRALG_3:7 (the Sorts of U0).s <> {} implies Constants(U0,s) = { const(o,U0) where o is Element of the OperSymbols of S : the_result_sort_of o = s & the_arity_of o = {} }; theorem :: PRALG_3:8 the_arity_of o = {} implies (commute (OPER A)).o in Funcs(I,Funcs({{}}, union { Result(o,A.i') where i' is Element of I: not contradiction })); theorem :: PRALG_3:9 the_arity_of o = {} implies const(o,product A) in Funcs(I, union { Result(o,A.i') where i' is Element of I: not contradiction }); definition let S,I,o,A; cluster const (o,product A) -> Relation-like Function-like; end; theorem :: PRALG_3:10 for o be OperSymbol of S st the_arity_of o = {} holds (const (o,product A)).i = const (o,A.i); theorem :: PRALG_3:11 the_arity_of o = {} & dom f = I & (for i be Element of I holds f.i = const(o,A.i)) implies f = const(o,product A); theorem :: PRALG_3:12 for e be Element of Args(o,U1) st e = {} & the_arity_of o = {} & Args(o,U1) <> {} & Args(o,U2) <> {} for F be ManySortedFunction of U1,U2 holds F#e = {}; begin :: Properties of Arguments of operations in Many Sorted Algebras theorem :: PRALG_3:13 for U1,U2 be non-empty MSAlgebra over S for F be ManySortedFunction of U1,U2 for x be Element of Args(o,U1) holds x in product doms (F*the_arity_of o); theorem :: PRALG_3:14 for U1,U2 be non-empty MSAlgebra over S for F be ManySortedFunction of U1,U2 for x be Element of Args(o,U1) for n be set st n in dom (the_arity_of o) holds (F#x).n = F.((the_arity_of o)/.n).(x.n); theorem :: PRALG_3:15 for x be Element of Args(o,product A) holds x in Funcs (dom (the_arity_of o),Funcs (I,union { (the Sorts of A.i').s' where i' is Element of I,s' is Element of (the carrier of S) : not contradiction })); theorem :: PRALG_3:16 for x be Element of Args(o,product A) for n be set st n in dom (the_arity_of o) holds x.n in product Carrier(A,(the_arity_of o)/.n); theorem :: PRALG_3:17 for i be Element of I for n be set st n in dom(the_arity_of o) for s be SortSymbol of S st s = (the_arity_of o).n for y be Element of Args(o,product A) for g be Function st g = y.n holds g.i in (the Sorts of A.i).s; theorem :: PRALG_3:18 for y be Element of Args(o,product A) st (the_arity_of o) <> {} holds (commute y) in product doms (A?.o); theorem :: PRALG_3:19 for y be Element of Args(o,product A) st the_arity_of o <> {} holds y in dom (Commute Frege(A?.o)); theorem :: PRALG_3:20 for I be set, S be non void non empty ManySortedSign, A be MSAlgebra-Family of I,S, o be OperSymbol of S for x be Element of Args(o,product A) holds Den(o,product A).x in product Carrier(A,the_result_sort_of o); theorem :: PRALG_3:21 for I,S,A,i for o be OperSymbol of S st (the_arity_of o) <> {} for U1 be non-empty MSAlgebra over S for x be Element of Args(o,product A) holds (commute x).i is Element of Args(o,A.i); theorem :: PRALG_3:22 for I,S,A,i,o for x be Element of Args(o,product A) for n be set st n in dom(the_arity_of o) for f be Function st f = x.n holds ((commute x).i).n = f.i; theorem :: PRALG_3:23 for o be OperSymbol of S st (the_arity_of o) <> {} for y be Element of Args(o,product A), i' be Element of I for g be Function st g = Den(o,product A).y holds g.i' = Den(o,A.i').((commute y).i'); begin :: The Projection of Family of Many Sorted Algebras definition let f be Function, x be set; func proj(f,x) -> Function means :: PRALG_3:def 2 dom it = product f & for y being Function st y in dom it holds it.y = y.x; end; definition let I,S; let A be MSAlgebra-Family of I,S, i be Element of I; func proj(A,i) -> ManySortedFunction of product A,A.i means :: PRALG_3:def 3 for s be Element of S holds it.s = proj (Carrier(A,s), i); end; theorem :: PRALG_3:24 for x be Element of Args(o,product A) st Args(o,product A) <> {} & the_arity_of o <> {} for i be Element of I holds proj(A,i)#x = (commute x).i; theorem :: PRALG_3:25 for i be Element of I for A be MSAlgebra-Family of I,S holds proj(A,i) is_homomorphism product A,A.i; theorem :: PRALG_3:26 for U1 be non-empty MSAlgebra over S for F being ManySortedFunction of I st (for i be Element of I holds ex F1 being ManySortedFunction of U1,A.i st F1 = F.i & F1 is_homomorphism U1,A.i) holds F in Funcs(I,Funcs(the carrier of S, {F.i'.s1 where s1 is SortSymbol of S,i' is Element of I :not contradiction})) & (commute F).s.i = F.i.s; theorem :: PRALG_3:27 for U1 be non-empty MSAlgebra over S for F being ManySortedFunction of I st (for i be Element of I holds ex F1 being ManySortedFunction of U1,A.i st F1 = F.i & F1 is_homomorphism U1,A.i) holds (commute F).s in Funcs(I,Funcs((the Sorts of U1).s, union {(the Sorts of A.i').s1 where i' is Element of I,s1 is SortSymbol of S : not contradiction})); theorem :: PRALG_3:28 for U1 be non-empty MSAlgebra over S for F being ManySortedFunction of I st (for i be Element of I holds ex F1 being ManySortedFunction of U1,A.i st F1 = F.i & F1 is_homomorphism U1,A.i) for F' be ManySortedFunction of U1,A.i st F' = F.i for x be set st x in (the Sorts of U1).s for f be Function st f = (commute((commute F).s)).x holds f.i = F'.s.x; theorem :: PRALG_3:29 for U1 be non-empty MSAlgebra over S for F being ManySortedFunction of I st (for i be Element of I holds ex F1 being ManySortedFunction of U1,A.i st F1 = F.i & F1 is_homomorphism U1,A.i) for x be set st x in (the Sorts of U1).s holds (commute ((commute F).s)).x in product (Carrier(A,s)); theorem :: PRALG_3:30 for U1 be non-empty MSAlgebra over S for F being ManySortedFunction of I st (for i be Element of I holds ex F1 being ManySortedFunction of U1,A.i st F1 = F.i & F1 is_homomorphism U1,A.i) holds ex H being ManySortedFunction of U1,(product A) st H is_homomorphism U1,(product A) & (for i be Element of I holds proj(A,i) ** H = F.i); begin :: The Class of Family of Many Sorted Algebras definition let I,J,S; mode MSAlgebra-Class of S,J -> ManySortedSet of I means :: PRALG_3:def 4 for i be set st i in I holds it.i is MSAlgebra-Family of J.i,S; end; definition let I,S,A,EqR; func A / EqR -> MSAlgebra-Class of S,id (Class EqR) means :: PRALG_3:def 5 for c st c in Class EqR holds it.c = A|c; end; definition let I,S; let J be non-empty ManySortedSet of I; let C be MSAlgebra-Class of S,J; func product C -> MSAlgebra-Family of I,S means :: PRALG_3:def 6 for i st i in I ex Ji be non empty set, Cs be MSAlgebra-Family of Ji,S st Ji = J.i & Cs = C.i & it.i = product Cs; end; theorem :: PRALG_3:31 for A be MSAlgebra-Family of I,S, EqR be Equivalence_Relation of I holds product A, product (product (A/EqR)) are_isomorphic;

Back to top