Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### Semigroup Operations on Finite Subsets

by
Czeslaw Bylinski

MML identifier: SETWOP_2
[ Mizar article, MML identifier index ]

```environ

vocabulary FINSUB_1, BINOP_1, FUNCT_1, FINSEQ_1, FINSEQ_2, SETWISEO, BOOLE,
RELAT_1, TARSKI, FINSEQOP, FUNCOP_1, SUBSET_1, FUNCT_4, FINSOP_1;
notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XREAL_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;
constructors NAT_1, BINOP_1, WELLORD2, SETWISEO, FINSEQOP, FINSOP_1, XREAL_0,
MEMBERED, PARTFUN1, XBOOLE_0;
clusters SUBSET_1, FUNCT_1, RELSET_1, FINSEQ_2, FINSUB_1, FINSEQ_1, ARYTM_3,
MEMBERED, ZFMISC_1, FUNCT_2, XBOOLE_0, ORDINAL2;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;

begin

reserve x,y for set;
reserve C,C',D,E for non empty set;
reserve c,c',c1,c2,c3 for Element of C;
reserve B,B',B1,B2 for Element of Fin C;
reserve A for Element of Fin C';
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,f' for Function of C,D;
reserve g for Function of C',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;
canceled 2;

theorem :: SETWOP_2:3
F is commutative associative & c1 <> c2
implies F \$\$ ({c1,c2},f) = F.(f.c1, f.c2);

theorem :: SETWOP_2:4
F is commutative associative & (B <> {} or F has_a_unity) & not c in B
implies F \$\$(B \/ {c}, f) = F.(F \$\$(B,f),f.c);

theorem :: SETWOP_2:5
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:6
F is commutative associative &
(B1 <> {} & B2 <> {} or F has_a_unity) & B1 misses B2
implies F \$\$(B1 \/ B2, f) = F.(F \$\$(B1,f),F \$\$(B2,f));

theorem :: SETWOP_2:7
F is commutative associative & (A <> {} or F has_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:8
H is commutative associative & (B <> {} or H has_a_unity) &
f is one-to-one implies H \$\$(f.:B,h) = H \$\$(B,h*f);

theorem :: SETWOP_2:9
F is commutative associative & (B <> {} or F has_a_unity) &
f|B = f'|B implies F \$\$(B,f) = F \$\$(B,f');

theorem :: SETWOP_2:10
F is commutative associative & F has_a_unity &
e = the_unity_wrt F & f.:B = {e} implies F\$\$(B,f) = e;

theorem :: SETWOP_2:11
F is commutative associative &
F has_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,f')) = F \$\$(B,G.:(f,f'));

theorem :: SETWOP_2:12
F is commutative associative & F has_a_unity
implies F.(F\$\$(B,f),F\$\$(B,f')) = F \$\$(B,F.:(f,f'));

theorem :: SETWOP_2:13
F is commutative associative & F has_a_unity &
F has_an_inverseOp & G = F*(id D,the_inverseOp_wrt F)
implies G.(F\$\$(B,f),F\$\$(B,f')) = F \$\$(B,G.:(f,f'));

theorem :: SETWOP_2:14
F is commutative associative & F has_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:15
F is commutative associative & F has_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:16
F is commutative associative & F has_a_unity & F has_an_inverseOp &
G is_distributive_wrt F
implies G.(d,F\$\$(B,f)) = F \$\$(B,G[;](d,f));

theorem :: SETWOP_2:17
F is commutative associative & F has_a_unity & F has_an_inverseOp &
G is_distributive_wrt F
implies G.(F\$\$(B,f),d) = F \$\$(B,G[:](f,d));

theorem :: SETWOP_2:18
F is commutative associative & F has_a_unity &
H is commutative associative & H has_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:19
F is commutative associative & F has_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:20
F is commutative associative & F has_a_unity & F has_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:21
F is commutative associative & F has_a_unity & F has_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) -> Function of NAT,D equals
:: SETWOP_2:def 1
(NAT --> d) +* p;
end;

theorem :: SETWOP_2:22
(i in dom p implies [#](p,d).i = p.i) &
(not i in dom p implies [#](p,d).i = d);

theorem :: SETWOP_2:23
[#](p,d)|(dom p) = p;

theorem :: SETWOP_2:24
[#](p^q,d)|(dom p) = p;

theorem :: SETWOP_2:25
rng [#](p,d) = rng p \/ {d};

theorem :: SETWOP_2:26
h*[#](p,d) = [#](h*p,h.d);

definition let i;
redefine func Seg i -> Element of Fin NAT;
end;

definition let f be FinSequence;
redefine func dom f -> Element of Fin NAT;
end;

definition let D,p,F;
assume
(F has_a_unity or len p >= 1) & F is associative commutative;
redefine func F "**" p equals
:: SETWOP_2:def 2
F \$\$(dom p,[#](p,the_unity_wrt F));
synonym F \$\$ p;
end;

canceled 8;

theorem :: SETWOP_2:35
F has_a_unity implies F"**"(i|->the_unity_wrt F) = the_unity_wrt F;

canceled;

theorem :: SETWOP_2:37
F is associative & (i>=1 & j>=1 or F has_a_unity)
implies F"**"((i+j)|->d) = F.(F"**"(i|->d),F"**"(j|->d));

theorem :: SETWOP_2:38
F is commutative associative & (i>=1 & j>=1 or F has_a_unity)
implies F"**"((i*j)|->d) = F"**"(j|->(F"**"(i|->d)));

theorem :: SETWOP_2:39
F has_a_unity & H has_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:40
F has_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:41
F is associative & F has_a_unity & F has_an_inverseOp &
G is_distributive_wrt F
implies G[;](d,id D).(F"**"p) = F "**"(G[;](d,id D)*p);

theorem :: SETWOP_2:42
F is commutative associative & F has_a_unity & F has_an_inverseOp
implies (the_inverseOp_wrt F).(F"**"p) = F "**"((the_inverseOp_wrt F)*p);

theorem :: SETWOP_2:43
F is commutative associative &
F has_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:44
F is commutative associative &
F has_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:45
F is commutative associative & F has_a_unity &
len p = len q implies F.(F"**"p,F"**"q) = F "**"(F.:(p,q));

theorem :: SETWOP_2:46
F is commutative associative & F has_a_unity
implies F.(F"**"T1,F"**"T2) = F "**"(F.:(T1,T2));

theorem :: SETWOP_2:47
F is commutative associative & F has_a_unity
implies F"**"(i|->(F.(d1,d2))) = F.(F"**"(i|->d1),F"**"(i|->d2));

theorem :: SETWOP_2:48
F is commutative associative & F has_a_unity &
F has_an_inverseOp & G = F*(id D,the_inverseOp_wrt F)
implies G.(F"**"T1,F"**"T2) = F "**"(G.:(T1,T2));

theorem :: SETWOP_2:49
F is commutative associative & F has_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:50
F is commutative associative & F has_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:51
F is commutative associative & F has_a_unity & F has_an_inverseOp &
G is_distributive_wrt F
implies G.(d,F"**"p) = F "**"(G[;](d,p));

theorem :: SETWOP_2:52
F is commutative associative & F has_a_unity & F has_an_inverseOp &
G is_distributive_wrt F
implies G.(F"**"p,d) = F "**"(G[:](p,d));
```