The Mizar abstract of SETWOP

Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users
The abstract of the Mizar article:: Semigroup Operations on Finite Subsets
by
Czeslaw Bylinski
Received May 4, 1990
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));
The abstract of the Mizar article:

Semigroup Operations on Finite Subsets
