:: Semigroup operations on finite subsets
:: by Czes{\l}aw Byli\'nski
::
:: Received May 4, 1990
:: Copyright (c) 1990-2016 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));