:: Semigroup operations on finite subsets :: by Czes{\l}aw Byli\'nski :: :: Received May 4, 1990 :: Copyright (c) 1990-2021 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 NUMBERS, XBOOLE_0, SUBSET_1, FINSUB_1, BINOP_1, FUNCT_1, NAT_1, FINSEQ_1, FINSEQ_2, ARYTM_3, XXREAL_0, SETWISEO, TARSKI, RELAT_1, FINSEQOP, FUNCOP_1, FUNCT_4, ORDINAL4, FINSOP_1, CARD_1, SETWOP_2; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, RELAT_1, RELSET_1, FUNCT_1, FINSEQ_1, FINSUB_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1, SETWISEO, FINSEQ_2, FINSEQOP, FINSOP_1, XXREAL_0; constructors PARTFUN1, WELLORD2, BINOP_1, SETWISEO, XXREAL_0, XREAL_0, NAT_1, FINSEQOP, FINSOP_1, RELSET_1, FINSEQ_2, NUMBERS; registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, FINSUB_1, XREAL_0, FINSEQ_1, FINSEQ_2, NAT_1, CARD_1, RELAT_1; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin reserve x,y for set; reserve C,C9,D,E for non empty set; reserve c,c9,c1,c2,c3 for Element of C; reserve B,B9,B1,B2 for Element of Fin C; reserve A for Element of Fin C9; reserve d,d1,d2,d3,d4,e for Element of D; reserve F,G for BinOp of D; reserve u for UnOp of D; reserve f,f9 for Function of C,D; reserve g for Function of C9,D; reserve H for BinOp of E; reserve h for Function of D,E; reserve i,j for Nat; reserve s for Function; reserve p,q for FinSequence of D; reserve T1,T2 for Element of i-tuples_on D; theorem :: SETWOP_2:1 F is commutative associative & c1 <> c2 implies F $$ ({.c1,c2.},f ) = F.(f.c1, f.c2); theorem :: SETWOP_2:2 F is commutative associative & (B <> {} or F is having_a_unity) & not c in B implies F $$(B \/ {.c.}, f) = F.(F $$(B,f),f.c); theorem :: SETWOP_2:3 F is commutative associative & c1 <> c2 & c1 <> c3 & c2 <> c3 implies F $$ ({.c1,c2,c3.},f) = F.(F.(f.c1, f.c2),f.c3); theorem :: SETWOP_2:4 F is commutative associative & (B1 <> {} & B2 <> {} or F is having_a_unity) & B1 misses B2 implies F $$(B1 \/ B2, f) = F.(F $$(B1,f),F $$( B2,f)); theorem :: SETWOP_2:5 F is commutative associative & (A <> {} or F is having_a_unity) & (ex s st dom s = A & rng s = B & s is one-to-one & g|A = f*s) implies F $$(A,g) = F $$(B,f); theorem :: SETWOP_2:6 H is commutative associative & (B <> {} or H is having_a_unity) & f is one-to-one implies H $$(f.:B,h) = H $$(B,h*f); theorem :: SETWOP_2:7 F is commutative associative & (B <> {} or F is having_a_unity) & f|B = f9|B implies F $$(B,f) = F $$(B,f9); theorem :: SETWOP_2:8 F is commutative associative & F is having_a_unity & e = the_unity_wrt F & f.:B = {e} implies F$$(B,f) = e; theorem :: SETWOP_2:9 F is commutative associative & F is having_a_unity & e = the_unity_wrt F & G.(e,e) = e & (for d1,d2,d3,d4 holds F.(G.(d1,d2),G.(d3,d4))= G.(F.(d1,d3),F.(d2,d4))) implies G.(F$$(B,f),F$$(B,f9)) = F $$(B,G.:(f,f9)); theorem :: SETWOP_2:10 F is commutative associative & F is having_a_unity implies F.(F$$(B,f) ,F$$(B,f9)) = F $$(B,F.:(f,f9)); theorem :: SETWOP_2:11 F is commutative associative & F is having_a_unity & F is having_an_inverseOp & G = F*(id D,the_inverseOp_wrt F) implies G.(F$$(B,f),F$$( B,f9)) = F $$(B,G.:(f,f9)); theorem :: SETWOP_2:12 F is commutative associative & F is having_a_unity & e = the_unity_wrt F & G is_distributive_wrt F & G.(d,e) = e implies G.(d,F$$(B,f)) = F $$(B,G[;](d,f)); theorem :: SETWOP_2:13 F is commutative associative & F is having_a_unity & e = the_unity_wrt F & G is_distributive_wrt F & G.(e,d) = e implies G.(F$$(B,f),d) = F $$(B,G[:](f,d)); theorem :: SETWOP_2:14 F is commutative associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F implies G.(d,F$$(B,f)) = F $$(B,G [;](d,f)); theorem :: SETWOP_2:15 F is commutative associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F implies G.(F$$(B,f),d) = F $$(B,G [:](f,d)); theorem :: SETWOP_2:16 F is commutative associative & F is having_a_unity & H is commutative associative & H is having_a_unity & h.the_unity_wrt F = the_unity_wrt H & (for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2)) implies h.(F $$(B,f)) = H $$(B,h*f); theorem :: SETWOP_2:17 F is commutative associative & F is having_a_unity & u.the_unity_wrt F = the_unity_wrt F & u is_distributive_wrt F implies u.(F$$(B,f)) = F $$(B,u*f); theorem :: SETWOP_2:18 F is commutative associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F implies G[;](d,id D).(F$$(B,f)) = F $$(B,G[;](d,id D)*f); theorem :: SETWOP_2:19 F is commutative associative & F is having_a_unity & F is having_an_inverseOp implies (the_inverseOp_wrt F).(F$$(B,f)) = F $$(B,( the_inverseOp_wrt F)*f); definition let D,p,d; func [#](p,d) -> sequence of D equals :: SETWOP_2:def 1 (NAT --> d) +* p; end; theorem :: SETWOP_2:20 (i in dom p implies [#](p,d).i = p.i) & (not i in dom p implies [#](p,d).i = d); theorem :: SETWOP_2:21 [#](p,d)|(dom p) = p; theorem :: SETWOP_2:22 [#](p^q,d)|(dom p) = p; theorem :: SETWOP_2:23 rng [#](p,d) = rng p \/ {d}; theorem :: SETWOP_2:24 h*[#](p,d) = [#](h*p,h.d); notation let i be Nat; synonym finSeg i for Seg i; end; definition let i be Nat; redefine func finSeg i -> Element of Fin NAT; end; notation let D,p,F; synonym F $$ p for F "**" p; end; definition let D,p,F; assume ( F is having_a_unity or len p >= 1)& F is associative commutative; redefine func F $$ p equals :: SETWOP_2:def 2 F $$(findom p,[#](p,the_unity_wrt F)); end; theorem :: SETWOP_2:25 F is having_a_unity implies F"**"(i|->the_unity_wrt F) = the_unity_wrt F; theorem :: SETWOP_2:26 F is associative & (i>=1 & j>=1 or F is having_a_unity) implies F"**"((i+j)|->d) = F.(F"**"(i|->d),F"**"(j|->d)); theorem :: SETWOP_2:27 F is commutative associative & (i>=1 & j>=1 or F is having_a_unity) implies F"**"((i*j)|->d) = F"**"(j|->(F"**"(i|->d))); theorem :: SETWOP_2:28 F is having_a_unity & H is having_a_unity & h.the_unity_wrt F = the_unity_wrt H & (for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2)) implies h.(F "**"p) = H "**"(h*p); theorem :: SETWOP_2:29 F is having_a_unity & u.the_unity_wrt F = the_unity_wrt F & u is_distributive_wrt F implies u.(F"**"p) = F "**"(u*p); theorem :: SETWOP_2:30 F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F implies G[;](d,id D).(F"**"p) = F "**"(G[;](d,id D)*p); theorem :: SETWOP_2:31 F is commutative associative & F is having_a_unity & F is having_an_inverseOp implies (the_inverseOp_wrt F).(F"**"p) = F "**"(( the_inverseOp_wrt F)*p); theorem :: SETWOP_2:32 F is commutative associative & F is having_a_unity & e = the_unity_wrt F & G.(e,e) = e & (for d1,d2,d3,d4 holds F.(G.(d1,d2),G.(d3,d4))= G.(F.(d1,d3),F.(d2,d4))) & len p = len q implies G.(F"**"p,F"**"q) = F "**"(G.: (p,q)); theorem :: SETWOP_2:33 F is commutative associative & F is having_a_unity & e = the_unity_wrt F & G.(e,e) = e & (for d1,d2,d3,d4 holds F.(G.(d1,d2),G.(d3,d4))= G.(F.(d1,d3),F.(d2,d4))) implies G.(F"**"T1,F"**"T2) = F "**"(G.:(T1,T2)); theorem :: SETWOP_2:34 F is commutative associative & F is having_a_unity & len p = len q implies F.(F"**"p,F"**"q) = F "**"(F.:(p,q)); theorem :: SETWOP_2:35 F is commutative associative & F is having_a_unity implies F.(F"**"T1,F"**"T2) = F "**"(F.:(T1,T2)); theorem :: SETWOP_2:36 F is commutative associative & F is having_a_unity implies F"**"(i|->(F.(d1,d2))) = F.(F"**"(i|->d1),F"**"(i|->d2)); theorem :: SETWOP_2:37 F is commutative associative & F is having_a_unity & F is having_an_inverseOp & G = F*(id D,the_inverseOp_wrt F) implies G.(F"**"T1,F"**" T2) = F "**"(G.:(T1,T2)); theorem :: SETWOP_2:38 F is commutative associative & F is having_a_unity & e = the_unity_wrt F & G is_distributive_wrt F & G.(d,e) = e implies G.(d,F"**"p) = F "**"(G[;](d,p)); theorem :: SETWOP_2:39 F is commutative associative & F is having_a_unity & e = the_unity_wrt F & G is_distributive_wrt F & G.(e,d) = e implies G.(F"**"p,d) = F "**"(G[:](p,d)); theorem :: SETWOP_2:40 F is commutative associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F implies G.(d,F"**"p) = F "**"(G [;](d,p)); theorem :: SETWOP_2:41 F is commutative associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F implies G.(F"**"p,d) = F "**"(G [:](p,d));