:: Semigroup operations on finite subsets
:: by Czes{\l}aw Byli\'nski
::
:: Received May 4, 1990
:: Copyright (c) 1990-2026 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;
definitions XBOOLE_0;
equalities RELAT_1;
expansions BINOP_1, XBOOLE_0;
theorems TARSKI, ENUMSET1, ZFMISC_1, NAT_1, FUNCT_1, FUNCT_2, FUNCOP_1,
FINSEQ_1, FINSUB_1, BINOP_1, SETWISEO, FINSEQ_2, WELLORD2, CARD_1,
FINSEQOP, RELAT_1, FUNCT_4, FINSOP_1, XBOOLE_0, XBOOLE_1, XREAL_1,
ORDINAL1;
schemes NAT_1, SETWISEO, FINSEQ_2;
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;
Lm1: for i be Nat holds Seg i is Element of Fin NAT by FINSUB_1:def 5;
Lm2: for i holds not i+1 in Seg i by FINSEQ_1:1,XREAL_1:29;
theorem Th1:
F is commutative associative & c1 <> c2 implies F $$ ({.c1,c2.},f
) = F.(f.c1, f.c2)
proof
assume that
A1: F is commutative associative and
A2: c1 <> c2;
consider g being Function of Fin C, D such that
A3: F $$ ({.c1,c2.},f) = g.{c1,c2} and
for e st e is_a_unity_wrt F holds g.{} = e and
A4: for c holds g.{c} = f.c and
A5: for B st B c= { c1,c2 } & B <> {} for c st c in { c1,c2 } \ B holds
g.(B \/ {c}) = F.(g.B,f.c) by A1,SETWISEO:def 3;
c1 in {c1} & not c2 in {c1} by A2,TARSKI:def 1;
then {c1,c2} \ {c1} = {c2} by ZFMISC_1:62;
then
A6: c2 in {c1,c2} \ {c1} by TARSKI:def 1;
thus F $$ ({.c1,c2.},f) = g.({.c1.} \/ {.c2.}) by A3,ENUMSET1:1
.= F.(g.{c1}, f.c2) by A5,A6,ZFMISC_1:7
.= F.(f.c1, f.c2) by A4;
end;
theorem Th2:
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)
proof
assume that
A1: F is commutative associative and
A2: B <> {} or F is having_a_unity and
A3: not c in B;
per cases;
suppose
A4: B = {};
then B = {}.C;
then F $$(B,f) = the_unity_wrt F by A1,A2,SETWISEO:31;
hence F.(F $$(B,f),f.c) = f.c by A2,A4,SETWISEO:15
.= F $$(B \/ {.c.}, f) by A1,A4,SETWISEO:17;
end;
suppose
A5: B <> {};
consider g9 being Function of Fin C, D such that
A6: F $$ (B,f) = g9.B and
for e st e is_a_unity_wrt F holds g9.{} = e and
A7: for c9 holds g9.{c9} = f.c9 and
A8: for B9 st B9 c= B & B9 <> {} for c9 st c9 in B \ B9 holds g9.(B9
\/ {c9}) = F.(g9.B9,f.c9) by A1,A2,SETWISEO:def 3;
consider g being Function of Fin C, D such that
A9: F $$ (B \/ {.c.},f) = g.(B \/ {c}) and
for e st e is_a_unity_wrt F holds g.{} = e and
A10: for c9 holds g.{c9} = f.c9 and
A11: for B9 st B9 c= B \/ {c} & B9 <> {} for c9 st c9 in (B \/ {c}) \
B9 holds g.(B9 \/ {c9}) = F.(g.B9,f.c9) by A1,SETWISEO:def 3;
defpred X[set] means $1 <> {} & $1 c= B implies g.($1) = g9.($1);
A12: for B9 being Element of Fin C, b being Element of C holds X[B9] & not
b in B9 implies X[B9 \/ {b}]
proof
A13: B c= B \/ {c} by XBOOLE_1:7;
let B9, c9 such that
A14: B9 <> {} & B9 c= B implies g.B9 = g9.B9 and
A15: not c9 in B9 and
B9 \/ {c9} <> {} and
A16: B9 \/ {c9} c= B;
A17: c9 in B by A16,ZFMISC_1:137;
then
A18: c9 in B \ B9 by A15,XBOOLE_0:def 5;
c9 in (B \/ {c}) by A17,XBOOLE_0:def 3;
then
A19: c9 in (B \/ {c}) \ B9 by A15,XBOOLE_0:def 5;
B9 c= B by A16,XBOOLE_1:11;
then
A20: B9 c= B \/ {c} by A13,XBOOLE_1:1;
per cases;
suppose
A21: B9 = {};
then g.(B9 \/ {c9}) = f.c9 by A10;
hence thesis by A7,A21;
end;
suppose
A22: B9 <> {};
hence g.(B9 \/ {c9}) = F.(g9.B9, f.c9) by A11,A14,A16,A20,A19,
XBOOLE_1:11
.= g9.(B9 \/ {c9}) by A8,A16,A18,A22,XBOOLE_1:11;
end;
end;
A23: X[{}.C];
A24: for B9 holds X[B9] from SETWISEO:sch 2(A23,A12);
c in B \/ {c} by ZFMISC_1:136;
then c in (B \/ {c}) \ B by A3,XBOOLE_0:def 5;
hence F $$(B \/ {.c.}, f) = F.(g.B, f.c) by A5,A9,A11,XBOOLE_1:7
.= F.(F $$(B,f),f.c) by A5,A6,A24;
end;
end;
theorem
F is commutative associative & c1 <> c2 & c1 <> c3 & c2 <> c3 implies
F $$ ({.c1,c2,c3.},f) = F.(F.(f.c1, f.c2),f.c3)
proof
assume that
A1: F is commutative associative and
A2: c1 <> c2;
assume c1 <> c3 & c2 <> c3;
then
A3: not c3 in {c1,c2} by TARSKI:def 2;
thus F $$ ({.c1,c2,c3.},f) = F $$ ({.c1,c2.} \/ {.c3.},f) by ENUMSET1:3
.= F.(F $$ ({.c1,c2.},f),f.c3) by A1,A3,Th2
.= F.(F.(f.c1, f.c2),f.c3) by A1,A2,Th1;
end;
theorem
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))
proof
assume that
A1: F is commutative associative and
A2: B1 <> {} & B2 <> {} or F is having_a_unity and
A3: B1 /\ B2 = {};
now
per cases;
suppose
A4: B1 = {} or B2 = {};
now
per cases by A4;
suppose
A5: B1 = {};
hence F $$(B1 \/ B2, f) = F.(the_unity_wrt F,F $$(B2,f)) by A2,
SETWISEO:15
.= F.(F $$({}.C,f),F $$(B2,f)) by A1,A2,A4,SETWISEO:31
.= F.(F $$(B1,f),F $$(B2,f)) by A5;
end;
suppose
A6: B2 = {};
hence F $$(B1 \/ B2, f) = F.(F $$(B1,f),the_unity_wrt F) by A2,
SETWISEO:15
.= F.(F $$(B1,f),F $$({}.C,f)) by A1,A2,A4,SETWISEO:31
.= F.(F $$(B1,f),F $$(B2,f)) by A6;
end;
end;
hence thesis;
end;
suppose
A7: B1 <> {} & B2 <> {};
defpred X[Element of Fin C] means $1 <> {} & B1 /\ $1 = {} implies F $$(
B1 \/ $1,f) = F.(F $$(B1,f),F $$($1,f));
A8: for B9 being Element of Fin C, b being Element of C holds X[B9] &
not b in B9 implies X[B9 \/ {.b.}]
proof
let B,c such that
A9: B <> {} & B1 /\ B = {} implies F $$(B1 \/ B,f) = F.(F $$ (B1,
f),F $$(B,f)) and
A10: not c in B and
B \/ {c} <> {};
assume
A11: B1 /\ (B \/ {c}) = {};
then
A12: B1 misses (B \/ {c});
c in B \/ {c} by ZFMISC_1:136;
then
A13: not c in B1 by A11,XBOOLE_0:def 4;
A14: B <> {} & B1 misses B implies F $$(B1 \/ B,f) = F.(F $$ (B1,f),F
$$(B,f)) by A9;
now
per cases;
suppose
A15: B = {};
hence
F $$ (B1 \/ (B \/ {.c.}),f) = F.(F $$ (B1,f), f.c) by A1,A7,A13,Th2
.= F.(F $$ (B1,f),F $$(B \/ {.c.},f)) by A1,A15,SETWISEO:17;
end;
suppose
A16: B <> {};
A17: not c in B1 \/ B by A10,A13,XBOOLE_0:def 3;
thus F $$ (B1 \/ (B \/ {.c.}),f) = F $$ (B1 \/ B \/ {.c.},f) by
XBOOLE_1:4
.= F.(F.(F $$ (B1,f),F $$(B,f)), f.c) by A1,A14,A12,A16,A17,Th2,
XBOOLE_1:7,63
.= F.(F $$ (B1,f),F.(F $$(B,f), f.c)) by A1
.= F.(F $$(B1,f),F $$(B \/ {.c.},f)) by A1,A10,A16,Th2;
end;
end;
hence thesis;
end;
A18: X[{}.C];
for B2 holds X[B2] from SETWISEO:sch 2(A18,A8);
hence thesis by A3,A7;
end;
end;
hence thesis;
end;
theorem Th5:
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)
proof
defpred X[Element of Fin C9] means $1 <> {} or F is having_a_unity implies
for B st ex s st dom s = $1 & rng s = B & s is one-to-one & g|$1 = f*s holds F
$$($1,g) = F $$(B,f);
assume
A1: F is commutative associative;
A2: for B9 being Element of Fin C9, b being Element of C9 holds X[B9] & not
b in B9 implies X[B9 \/ {.b.}]
proof
let A9 be Element of Fin C9,a be Element of C9 such that
A3: A9 <> {} or F is having_a_unity implies for B st ex s st dom s =
A9 & rng s = B & s is one-to-one & g|A9 = f*s holds F $$(A9,g) = F $$(B,f)
and
A4: not a in A9;
assume A9 \/ {a} <> {} or F is having_a_unity;
let B;
set A = A9 \/ {.a.};
given s such that
A5: dom s = A and
A6: rng s = B and
A7: s is one-to-one and
A8: g|A = f*s;
A9: a in A by ZFMISC_1:136;
then
A10: s.a in B by A5,A6,FUNCT_1:def 3;
B c= C by FINSUB_1:def 5;
then reconsider c = s.a as Element of C by A10;
set B9 = B \ {.c.};
set s9 = s|A9;
A11: s9 is one-to-one by A7,FUNCT_1:52;
now
let y be object;
thus y in rng s9 implies y in B9
proof
assume y in rng s9;
then consider x being object such that
A12: x in dom s9 and
A13: y = s9.x by FUNCT_1:def 3;
A14: s9.x = s.x by A12,FUNCT_1:47;
A15: x in dom s /\ A9 by A12,RELAT_1:61;
then x in dom s & x <> a by A4,XBOOLE_0:def 4;
then s.x <> c by A5,A7,A9,FUNCT_1:def 4;
then
A16: not y in {c} by A13,A14,TARSKI:def 1;
x in dom s by A15,XBOOLE_0:def 4;
then y in B by A6,A13,A14,FUNCT_1:def 3;
hence thesis by A16,XBOOLE_0:def 5;
end;
assume
A17: y in B9;
then y in B by XBOOLE_0:def 5;
then consider x being object such that
A18: x in dom s and
A19: y = s.x by A6,FUNCT_1:def 3;
A20: x in A9 or x in {a} by A5,A18,XBOOLE_0:def 3;
not y in {c} by A17,XBOOLE_0:def 5;
then x <> a by A19,TARSKI:def 1;
then x in dom s /\ A9 by A18,A20,TARSKI:def 1,XBOOLE_0:def 4;
then x in dom s9 & s9.x = s.x by FUNCT_1:48,RELAT_1:61;
hence y in rng s9 by A19,FUNCT_1:def 3;
end;
then
A21: rng s9 = B9 by TARSKI:2;
now
let x be object;
thus x in dom(g|A9) implies x in dom(f*s9)
proof
assume x in dom(g|A9);
then
A22: x in dom g /\ A9 by RELAT_1:61;
then
A23: x in A9 by XBOOLE_0:def 4;
A24: x in dom g by A22,XBOOLE_0:def 4;
x in A by A23,ZFMISC_1:136;
then x in dom g /\ A by A24,XBOOLE_0:def 4;
then
A25: x in dom(f*s) by A8,RELAT_1:61;
then
A26: s.x in dom f by FUNCT_1:11;
x in dom s by A25,FUNCT_1:11;
then x in dom s /\ A9 by A23,XBOOLE_0:def 4;
then
A27: x in dom s9 by RELAT_1:61;
then s9.x = s.x by FUNCT_1:47;
hence thesis by A26,A27,FUNCT_1:11;
end;
assume
A28: x in dom(f*s9);
then
A29: x in dom s9 by FUNCT_1:11;
then
A30: x in dom s /\ A9 by RELAT_1:61;
then
A31: x in dom s by XBOOLE_0:def 4;
s9.x in dom f by A28,FUNCT_1:11;
then s.x in dom f by A29,FUNCT_1:47;
then x in dom(g|A) by A8,A31,FUNCT_1:11;
then x in dom g /\ A by RELAT_1:61;
then
A32: x in dom g by XBOOLE_0:def 4;
x in A9 by A30,XBOOLE_0:def 4;
then x in dom g /\ A9 by A32,XBOOLE_0:def 4;
hence x in dom(g|A9) by RELAT_1:61;
end;
then
A33: dom(g|A9) = dom(f*s9) by TARSKI:2;
a in C9;
then a in dom g by FUNCT_2:def 1;
then a in dom g /\ A by A9,XBOOLE_0:def 4;
then a in dom(f*s) & g.a = (f*s).a by A8,FUNCT_1:48,RELAT_1:61;
then
A34: g.a = f.c by FUNCT_1:12;
B9 \/ {c} = B \/ {c} by XBOOLE_1:39;
then
A35: B = B9 \/ {c} by A10,ZFMISC_1:40;
A36: dom s9 = A9 by A5,RELAT_1:62,XBOOLE_1:7;
A37: for x being object st x in dom(g|A9) holds (g|A9).x = (f*s9).x
proof
let x be object;
assume x in dom(g|A9);
then
A38: x in dom g /\ A9 by RELAT_1:61;
then
A39: x in A9 by XBOOLE_0:def 4;
then
A40: x in A by ZFMISC_1:136;
x in dom g by A38,XBOOLE_0:def 4;
then x in dom g /\ A by A40,XBOOLE_0:def 4;
then x in dom(f*s) by A8,RELAT_1:61;
then
A41: x in dom s by FUNCT_1:11;
then x in dom s /\ A9 by A39,XBOOLE_0:def 4;
then
A42: x in dom s9 by RELAT_1:61;
then
A43: s9.x = s.x by FUNCT_1:47;
thus (g|A9).x = g.x by A39,FUNCT_1:49
.= (f*s).x by A8,A40,FUNCT_1:49
.= f.(s.x) by A41,FUNCT_1:13
.= (f*s9).x by A42,A43,FUNCT_1:13;
end;
then
A44: g|A9 = f*s9 by A33,FUNCT_1:2;
now
let y be object;
thus y in g.:A9 implies y in f.:B9
proof
assume y in g.:A9;
then consider x being object such that
A45: x in dom g and
A46: x in A9 and
A47: y = g.x by FUNCT_1:def 6;
x in dom g /\ A9 by A45,A46,XBOOLE_0:def 4;
then
A48: x in dom(g|A9) by RELAT_1:61;
then x in dom s9 by A33,FUNCT_1:11;
then
A49: s9.x in B9 by A21,FUNCT_1:def 3;
y = (f*s9).x by A44,A46,A47,FUNCT_1:49;
then
A50: y = f.(s9.x) by A33,A48,FUNCT_1:12;
s9.x in dom f by A33,A48,FUNCT_1:11;
hence thesis by A50,A49,FUNCT_1:def 6;
end;
assume y in f.:B9;
then consider x being object such that
x in dom f and
A51: x in B9 and
A52: y = f.x by FUNCT_1:def 6;
set x9 = s9".x;
A53: x9 in A9 by A11,A36,A21,A51,FUNCT_1:32;
A9 c= C9 by FINSUB_1:def 5;
then x9 in C9 by A53;
then
A54: x9 in dom g by FUNCT_2:def 1;
s9.x9 = x by A11,A21,A51,FUNCT_1:35;
then y = (f*s9).x9 by A36,A52,A53,FUNCT_1:13
.= g.x9 by A44,A53,FUNCT_1:49;
hence y in g.:A9 by A53,A54,FUNCT_1:def 6;
end;
then
A55: f.:B9 = g.:A9 by TARSKI:2;
A56: not c in B9 by ZFMISC_1:56;
now
per cases;
suppose
A57: A9 = {};
B9 c= C by FINSUB_1:def 5;
then B9 c= dom f by FUNCT_2:def 1;
then
A58: B9 = {} by A55,A57;
thus F $$(A,g) = f.c by A1,A34,A57,SETWISEO:17
.= F $$(B,f) by A1,A35,A58,SETWISEO:17;
end;
suppose
A59: A9 <> {};
A9 c= C9 by FINSUB_1:def 5;
then A9 c= dom g by FUNCT_2:def 1;
then
A60: B9 <> {} by A55,A59;
thus F $$(A,g) = F.(F $$(A9,g),g.a) by A1,A4,A59,Th2
.= F.(F $$(B9,f),f.c) by A3,A34,A11,A36,A21,A33,A37,A59,FUNCT_1:2
.= F $$(B,f) by A1,A35,A56,A60,Th2;
end;
end;
hence thesis;
end;
A61: X[{}.C9]
proof
assume
A62: {}.C9 <> {} or F is having_a_unity;
let B;
given s such that
A63: dom s = {}.C9 & rng s = B & s is one-to-one and
g|({}.C9) = f*s;
B,{} are_equipotent by A63,WELLORD2:def 4;
then
A64: B = {}.C by CARD_1:26;
F $$({}.C9,g) = the_unity_wrt F by A1,A62,SETWISEO:31;
hence thesis by A1,A62,A64,SETWISEO:31;
end;
for A holds X[A] from SETWISEO:sch 2(A61,A2);
hence thesis;
end;
theorem
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)
proof
assume that
A1: H is commutative associative &( B <> {} or H is having_a_unity) and
A2: f is one-to-one;
set s = f|B;
A3: rng s = f.:B & (h*f)|B = h*s by RELAT_1:83,115;
B c= C by FINSUB_1:def 5;
then B c= dom f by FUNCT_2:def 1;
then
A4: dom s = B by RELAT_1:62;
s is one-to-one by A2,FUNCT_1:52;
hence thesis by A1,A4,A3,Th5;
end;
theorem
F is commutative associative & (B <> {} or F is having_a_unity) & f|B
= f9|B implies F $$(B,f) = F $$(B,f9)
proof
assume
A1: F is commutative associative &( B <> {} or F is having_a_unity);
set s = id B;
A2: dom s = B & rng s = B;
assume f|B = f9|B;
then f|B = f9*s by RELAT_1:65;
hence thesis by A1,A2,Th5;
end;
theorem
F is commutative associative & F is having_a_unity & e = the_unity_wrt
F & f.:B = {e} implies F$$(B,f) = e
proof
assume that
A1: F is commutative associative and
A2: F is having_a_unity and
A3: e = the_unity_wrt F;
defpred X[Element of Fin C] means f.:($1) = {e} implies F$$($1,f) = e;
A4: for B9 being Element of Fin C, b being Element of C holds X[B9] & not b
in B9 implies X[B9 \/ {.b.}]
proof
let B9,c such that
A5: f.:(B9) = {e} implies F$$(B9,f) = e and
A6: not c in B9 and
A7: f.:(B9 \/ {c}) = {e};
A8: now
per cases;
suppose
B9 = {};
then
A9: B9 = {}.C;
thus F$$(B9 \/ {.c.},f) = F.(F $$(B9,f),f.c) by A1,A2,A6,Th2
.= F.(e,f.c) by A1,A2,A3,A9,SETWISEO:31;
end;
suppose
A10: B9 <> {};
B9 c= C by FINSUB_1:def 5;
then
A11: B9 c= dom f by FUNCT_2:def 1;
f.:B9 c= {e} by A7,RELAT_1:123,XBOOLE_1:7;
hence F$$(B9 \/ {.c.},f) = F.(e,f.c) by A1,A5,A6,A10,A11,Th2,
ZFMISC_1:33;
end;
end;
{.c.} c= C by FINSUB_1:def 5;
then
A12: {c} c= dom f by FUNCT_2:def 1;
then
A13: c in dom f by ZFMISC_1:31;
Im(f,c) c= {e} by A7,RELAT_1:123,XBOOLE_1:7;
then Im(f,c) = {e} by A12,ZFMISC_1:33;
then {e} = {f.c} by A13,FUNCT_1:59;
then f.c = e by ZFMISC_1:3;
hence thesis by A2,A3,A8,SETWISEO:15;
end;
A14: X[{}.C];
for B holds X[B] from SETWISEO:sch 2(A14,A4);
hence thesis;
end;
theorem Th9:
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))
proof
assume that
A1: F is commutative associative & F is having_a_unity and
A2: e = the_unity_wrt F and
A3: G.(e,e) = e and
A4: for d1,d2,d3,d4 holds F.(G.(d1,d2),G.(d3,d4))= G.(F.(d1,d3),F.(d2,d4 ));
defpred X[Element of Fin C] means G.(F$$($1,f),F$$($1,f9)) = F $$($1,G.:(f,
f9));
A5: for B9 being Element of Fin C, b being Element of C holds X[B9] & not b
in B9 implies X[B9 \/ {.b.}]
proof
let B,c such that
A6: G.(F$$(B,f),F$$(B,f9)) = F $$(B,G.:(f,f9)) and
A7: not c in B;
set s9 = F$$(B,f9);
set s = F$$(B,f);
F$$(B \/ {.c.},f) = F.(s,f.c) & F$$(B \/ {.c.},f9) = F.(s9,f9.c) by A1,A7
,Th2;
hence G.(F$$(B \/ {.c.},f),F$$(B \/ {.c.},f9)) = F.(G.(s,s9),G.(f.c,f9.c))
by A4
.= F.(G.(s,s9),G.:(f,f9).c) by FUNCOP_1:37
.= F $$(B \/ {.c.},G.:(f,f9)) by A1,A6,A7,Th2;
end;
F$$({}.C,f) = e & F$$({}.C,f9) = e by A1,A2,SETWISEO:31;
then
A8: X[{}.C] by A1,A2,A3,SETWISEO:31;
for B holds X[B] from SETWISEO:sch 2(A8,A5);
hence thesis;
end;
Lm3: F is commutative associative implies for d1,d2,d3,d4 holds F.(F.(d1,d2),F
.(d3,d4))= F.(F.(d1,d3),F.(d2,d4))
proof
assume that
A1: F is commutative and
A2: F is associative;
let d1,d2,d3,d4;
thus F.(F.(d1,d2),F.(d3,d4)) = F.(d1,F.(d2,F.(d3,d4))) by A2
.= F.(d1,F.(F.(d2,d3),d4)) by A2
.= F.(d1,F.(F.(d3,d2),d4)) by A1
.= F.(d1,F.(d3,F.(d2,d4))) by A2
.= F.(F.(d1,d3),F.(d2,d4)) by A2;
end;
theorem
F is commutative associative & F is having_a_unity implies F.(F$$(B,f)
,F$$(B,f9)) = F $$(B,F.:(f,f9))
proof
set e = the_unity_wrt F;
assume
A1: F is commutative & F is associative & F is having_a_unity;
then
F.(e,e) = e & for d1,d2,d3,d4 holds F.(F.(d1,d2),F.(d3,d4))= F.(F.(d1,d3
),F. (d2,d4)) by Lm3,SETWISEO:15;
hence thesis by A1,Th9;
end;
theorem
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))
proof
assume that
A1: F is commutative associative & F is having_a_unity and
A2: F is having_an_inverseOp & G = F*(id D,the_inverseOp_wrt F);
set 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)) by A1,A2,FINSEQOP:86,89;
hence thesis by A1,Th9;
end;
theorem Th12:
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))
proof
assume that
A1: F is commutative associative & F is having_a_unity and
A2: e = the_unity_wrt F and
A3: G is_distributive_wrt F;
defpred X[Element of Fin C] means G.(d,F$$($1,f)) = F $$($1,G[;](d,f));
A4: for B9 being Element of Fin C, b being Element of C holds X[B9] & not b
in B9 implies X[B9 \/ {.b.}]
proof
let B9,c such that
A5: G.(d,F$$(B9,f)) = F $$(B9,G[;](d,f)) and
A6: not c in B9;
thus G.(d,F$$(B9 \/ {.c.},f)) = G.(d,F.(F$$(B9,f),f.c)) by A1,A6,Th2
.= F.(G.(d,F$$(B9,f)),G.(d,f.c)) by A3,BINOP_1:11
.= F.(F $$(B9,G[;](d,f)),(G[;](d,f)).c) by A5,FUNCOP_1:53
.= F $$(B9 \/ {.c.},G[;](d,f)) by A1,A6,Th2;
end;
assume G.(d,e) = e;
then G.(d,F$$({}.C,f)) = e by A1,A2,SETWISEO:31
.= F $$({}.C,G[;](d,f)) by A1,A2,SETWISEO:31;
then
A7: X[{}.C];
for B holds X[B] from SETWISEO:sch 2(A7,A4);
hence thesis;
end;
theorem Th13:
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))
proof
assume that
A1: F is commutative associative & F is having_a_unity and
A2: e = the_unity_wrt F and
A3: G is_distributive_wrt F;
defpred X[Element of Fin C] means G.(F$$($1,f),d) = F $$($1,G[:](f,d));
A4: for B9 being (Element of Fin C), b being Element of C holds X[B9] & not
b in B9 implies X[B9 \/ {.b.}]
proof
let B9,c such that
A5: G.(F$$(B9,f),d) = F $$(B9,G[:](f,d)) and
A6: not c in B9;
thus G.(F$$(B9 \/ {.c.},f),d) = G.(F.(F$$(B9,f),f.c),d) by A1,A6,Th2
.= F.(G.(F$$(B9,f),d),G.(f.c,d)) by A3,BINOP_1:11
.= F.(F $$(B9,G[:](f,d)),(G[:](f,d)).c) by A5,FUNCOP_1:48
.= F $$(B9 \/ {.c.},G[:](f,d)) by A1,A6,Th2;
end;
assume G.(e,d) = e;
then G.(F$$({}.C,f),d) = e by A1,A2,SETWISEO:31
.= F $$({}.C,G[:](f,d)) by A1,A2,SETWISEO:31;
then
A7: X[{}.C];
for B holds X[B] from SETWISEO:sch 2(A7,A4);
hence thesis;
end;
theorem
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))
proof
assume that
A1: F is commutative associative & F is having_a_unity and
A2: F is having_an_inverseOp and
A3: G is_distributive_wrt F;
set e = the_unity_wrt F;
G.(d,e) = e by A1,A2,A3,FINSEQOP:66;
hence thesis by A1,A3,Th12;
end;
theorem
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))
proof
assume that
A1: F is commutative associative & F is having_a_unity and
A2: F is having_an_inverseOp and
A3: G is_distributive_wrt F;
set e = the_unity_wrt F;
G.(e,d) = e by A1,A2,A3,FINSEQOP:66;
hence thesis by A1,A3,Th13;
end;
theorem Th16:
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)
proof
assume that
A1: F is commutative associative & F is having_a_unity and
A2: H is commutative associative & H is having_a_unity and
A3: h.the_unity_wrt F = the_unity_wrt H and
A4: for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2);
defpred X[Element of Fin C] means h.(F$$($1,f)) = H $$($1,h*f);
A5: for B9 being (Element of Fin C), b being Element of C holds X[B9] & not
b in B9 implies X[B9 \/ {.b.}]
proof
let B,c such that
A6: h.(F$$(B,f)) = H $$(B,h*f) and
A7: not c in B;
thus h.(F$$(B \/ {.c.},f)) = h.(F.(F$$(B,f),f.c)) by A1,A7,Th2
.= H.(H $$(B,h*f),h.(f.c)) by A4,A6
.= H.(H $$(B,h*f),(h*f).c) by FUNCT_2:15
.= H $$(B \/ {.c.},h*f) by A2,A7,Th2;
end;
h.(F$$({}.C,f)) = the_unity_wrt H by A1,A3,SETWISEO:31
.= H $$({}.C,h*f) by A2,SETWISEO:31;
then
A8: X[{}.C];
for B holds X[B] from SETWISEO:sch 2(A8,A5);
hence thesis;
end;
theorem
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)
by Th16;
theorem
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)
proof
assume that
A1: F is commutative associative & F is having_a_unity and
A2: F is having_an_inverseOp and
A3: G is_distributive_wrt F;
set e = the_unity_wrt F;
set u = G[;](d,id D);
u is_distributive_wrt F by A3,FINSEQOP:54;
then
A4: for d1,d2 holds u.(F.(d1,d2)) = F.(u.d1,u.d2);
G[;](d,id D).e = e by A1,A2,A3,FINSEQOP:69;
hence thesis by A1,A4,Th16;
end;
theorem
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)
proof
assume that
A1: F is commutative associative & F is having_a_unity and
A2: F is having_an_inverseOp;
set e = the_unity_wrt F, u = the_inverseOp_wrt F;
u is_distributive_wrt F by A1,A2,FINSEQOP:63;
then
A3: for d1,d2 holds u.(F.(d1,d2)) = F.(u.d1,u.d2);
u.e = e by A1,A2,FINSEQOP:61;
hence thesis by A1,A3,Th16;
end;
definition
let D,p,d;
func [#](p,d) -> sequence of D equals
(NAT --> d) +* p;
coherence;
end;
theorem Th20:
(i in dom p implies [#](p,d).i = p.i) & (not i in dom p implies
[#](p,d).i = d)
proof
thus i in dom p implies [#](p,d).i = p.i by FUNCT_4:13;
A1: i in NAT by ORDINAL1:def 12;
assume not i in dom p;
hence [#](p,d).i = (NAT --> d).i by FUNCT_4:11
.= d by A1,FUNCOP_1:7;
end;
theorem
[#](p,d)|(dom p) = p
proof
set k = len p, f = [#](p,d);
Seg k c= NAT;
then Seg k c= dom f by FUNCT_2:def 1;
then
A1: dom (f|Seg k) = Seg k by RELAT_1:62;
A2: dom p = Seg k by FINSEQ_1:def 3;
now
let x be object;
assume
A3: x in Seg k;
then (f|Seg k).x = f.x by A1,FUNCT_1:47;
hence (f|Seg k).x = p.x by A2,A3,Th20;
end;
hence thesis by A1,A2,FUNCT_1:2;
end;
theorem
[#](p^q,d)|(dom p) = p
proof
set k = len p, f = [#](p^q,d);
Seg k c= NAT;
then Seg k c= dom f by FUNCT_2:def 1;
then
A1: dom (f|Seg k) = Seg k by RELAT_1:62;
A2: dom p = Seg k by FINSEQ_1:def 3;
now
let x be object;
k <= k + len q by NAT_1:12;
then k <= len (p^q) by FINSEQ_1:22;
then
A3: Seg(len(p^q)) = dom (p^q) & Seg k c= Seg len(p^q) by FINSEQ_1:5,def 3;
assume
A4: x in Seg k;
then (f|Seg k).x = f.x by A1,FUNCT_1:47;
hence (f|Seg k).x = (p^q).x by A4,A3,Th20
.= p.x by A2,A4,FINSEQ_1:def 7;
end;
hence thesis by A1,A2,FUNCT_1:2;
end;
theorem
rng [#](p,d) = rng p \/ {d}
proof
now
let y be object;
thus y in rng [#](p,d) implies y in rng p \/ {d}
proof
assume y in rng [#](p,d);
then consider x being object such that
A1: x in dom [#](p,d) and
A2: y = [#](p,d).x by FUNCT_1:def 3;
reconsider i = x as Element of NAT by A1;
now
per cases;
case
A3: i in dom p;
then y = p.i by A2,Th20;
hence y in rng p by A3,FUNCT_1:def 3;
end;
case
not i in dom p;
then y = d by A2,Th20;
hence y in {d} by TARSKI:def 1;
end;
end;
hence thesis by XBOOLE_0:def 3;
end;
assume
A4: y in rng p \/ {d};
now
per cases by A4,XBOOLE_0:def 3;
suppose
y in rng p;
then consider i being Nat such that
A5: i in dom p and
A6: y = p.i by FINSEQ_2:10;
y = [#](p,d).i by A5,A6,Th20;
hence y in rng [#](p,d) by A5,FUNCT_2:4;
end;
suppose
A7: y in {d};
dom p = Seg len p by FINSEQ_1:def 3;
then
A8: not len p + 1 in dom p by Lm2;
y = d by A7,TARSKI:def 1;
then y = [#](p,d).(len p + 1) by A8,Th20;
hence y in rng [#](p,d) by FUNCT_2:4;
end;
end;
hence y in rng [#](p,d);
end;
hence thesis by TARSKI:2;
end;
theorem
h*[#](p,d) = [#](h*p,h.d)
proof
now
let i be Element of NAT;
A1: dom(h*p)=Seg len(h*p) by FINSEQ_1:def 3;
A2: len(h*p) = len p & Seg len p = dom p by FINSEQ_1:def 3,FINSEQ_2:33;
now
per cases;
suppose
A3: i in dom p;
hence h.([#](p,d).i) = h.(p.i) by Th20
.= (h*p).i by A3,FUNCT_1:13
.= [#](h*p,h.d).i by A2,A1,A3,Th20;
end;
suppose
A4: not i in dom p;
hence h.([#](p,d).i) = h.d by Th20
.= [#](h*p,h.d).i by A2,A1,A4,Th20;
end;
end;
hence (h*[#](p,d)).i = [#](h*p,h.d).i by FUNCT_2:15;
end;
hence thesis by FUNCT_2:63;
end;
Lm4: len p = len q & F.(e,e) = e implies F.:([#](p,e),[#](q,e)) = [#](F.:(p,q)
,e)
proof
assume that
A1: len p = len q and
A2: F.(e,e) = e;
set r = F.:(p,q);
A3: len r = len p by A1,FINSEQ_2:72;
A4: dom r = Seg len r by FINSEQ_1:def 3;
A5: dom p = Seg len p by FINSEQ_1:def 3;
A6: dom q = Seg len q by FINSEQ_1:def 3;
now
let i be Element of NAT;
now
per cases;
suppose
A7: i in dom p;
hence F.([#](p,e).i,[#](q,e).i) = F.(p.i,[#](q,e).i) by Th20
.= F.(p.i,q.i) by A1,A5,A6,A7,Th20
.= r.i by A3,A5,A4,A7,FUNCOP_1:22
.= [#](r,e).i by A3,A5,A4,A7,Th20;
end;
suppose
A8: not i in dom p;
hence F.([#](p,e).i,[#](q,e).i) = F.(e,[#](q,e).i) by Th20
.= e by A1,A2,A5,A6,A8,Th20
.= [#](r,e).i by A3,A5,A4,A8,Th20;
end;
end;
hence F.:([#](p,e),[#](q,e)).i = [#](r,e).i by FUNCOP_1:37;
end;
hence thesis by FUNCT_2:63;
end;
Lm5: F.(e,d) = e implies F[:]([#](p,e),d) = [#](F[:](p,d),e)
proof
assume
A1: F.(e,d) = e;
now
let i be Element of NAT;
A2: dom p = Seg len p by FINSEQ_1:def 3;
A3: len(F[:](p,d)) = len p & dom(F[:](p,d)) = Seg len(F[:](p,d)) by
FINSEQ_1:def 3,FINSEQ_2:84;
now
per cases;
suppose
A4: i in dom p;
hence F.([#](p,e).i,d) = F.(p.i,d) by Th20
.= (F[:](p,d)).i by A3,A2,A4,FUNCOP_1:27
.= ([#](F[:](p,d),e)).i by A3,A2,A4,Th20;
end;
suppose
A5: not i in dom p;
hence F.([#](p,e).i,d) = F.(e,d) by Th20
.= ([#](F[:](p,d),e)).i by A1,A3,A2,A5,Th20;
end;
end;
hence (F[:]([#](p,e),d)).i = ([#](F[:](p,d),e)).i by FUNCOP_1:48;
end;
hence thesis by FUNCT_2:63;
end;
Lm6: F.(d,e) = e implies F[;](d,[#](p,e)) = [#](F[;](d,p),e)
proof
assume
A1: F.(d,e) = e;
now
let i be Element of NAT;
A2: dom p = Seg len p by FINSEQ_1:def 3;
A3: len(F[;](d,p)) = len p & dom(F[;](d,p)) = Seg len(F[;](d,p)) by
FINSEQ_1:def 3,FINSEQ_2:78;
now
per cases;
suppose
A4: i in dom p;
hence F.(d,[#](p,e).i) = F.(d,p.i) by Th20
.= (F[;](d,p)).i by A3,A2,A4,FUNCOP_1:32
.= ([#](F[;](d,p),e)).i by A3,A2,A4,Th20;
end;
suppose
A5: not i in dom p;
hence F.(d,[#](p,e).i) = F.(d,e) by Th20
.= ([#](F[;](d,p),e)).i by A1,A3,A2,A5,Th20;
end;
end;
hence (F[;](d,[#](p,e))).i = ([#](F[;](d,p),e)).i by FUNCOP_1:53;
end;
hence thesis by FUNCT_2:63;
end;
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; :: redefines finSeg (SETWOP_2, synonym) → Seg (FINSEQ_1, definition)
coherence by Lm1;
end;
notation
let D,p,F;
synonym F $$ p for F "**" p;
end;
definition
let D,p,F;
assume
A1: ( F is having_a_unity or len p >= 1)& F is associative commutative;
redefine func F $$ p equals :: redefines $$ (SETWOP_2, synonym) → "**" (FINSOP_1, definition)
:Def2:
F $$(findom p,[#](p,the_unity_wrt F));
compatibility by A1,FINSOP_1:3;
end;
theorem Th25:
F is having_a_unity implies F"**"(i|->the_unity_wrt F) = the_unity_wrt F
proof
set e = the_unity_wrt F;
defpred X[Nat] means F"**"($1|->e) = e;
assume
A1: F is having_a_unity;
A2: for i st X[i] holds X[i+1]
proof
let i;
assume
A3: F"**"(i|->e) = e;
thus F"**"((i+1)|->e) = F"**"((i|->e)^<*e*>) by FINSEQ_2:60
.= F.(F"**"(i|->e),e) by A1,FINSOP_1:4
.= e by A1,A3,SETWISEO:15;
end;
F"**"(0|->e) = F"**" <*>D .= e by A1,FINSOP_1:10;
then
A4: X[0];
for i holds X[i] from NAT_1:sch 2(A4,A2);
hence thesis;
end;
theorem Th26:
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))
proof
assume
A1: F is associative;
set p1 = (i|->d),p2 = (j|->d);
assume i>=1 & j>=1 or F is having_a_unity;
then len p1 >= 1 & len p2 >= 1 or F is having_a_unity by CARD_1:def 7;
then F "**"(p1^p2) = F.(F"**"p1,F"**"p2) by A1,FINSOP_1:5;
hence thesis by FINSEQ_2:123;
end;
theorem
F is commutative associative & (i>=1 & j>=1 or F is having_a_unity)
implies F"**"((i*j)|->d) = F"**"(j|->(F"**"(i|->d)))
proof
assume that
A1: F is commutative associative and
A2: i>=1 & j>=1 or F is having_a_unity;
per cases;
suppose
A3: i = 0 or j = 0;
set e = the_unity_wrt F;
A4: now
per cases by A3;
suppose
i = 0;
then i|->d = <*>D;
then F"**"(i|->d) = e by A2,A3,FINSOP_1:10;
hence F"**"(j|->(F"**"(i|->d))) = e by A2,A3,Th25;
end;
suppose
j = 0;
then j|->(F"**"(i|->d)) = <*>D;
hence F"**"(j|->(F"**"(i|->d))) = e by A2,A3,FINSOP_1:10;
end;
end;
(i*j)|->d = <*>D by A3;
hence thesis by A2,A3,A4,FINSOP_1:10;
end;
suppose
A5: i > 0 & j > 0;
defpred X[Nat] means $1 <> 0 implies F"**"((i*$1)|->d) = F"**"($1|->(F"**"
(i|->d)));
A6: for j st X[j] holds X[j+1]
proof
let j such that
A7: j <> 0 implies F"**"((i*j)|->d) = F"**"(j|->(F"**"(i|->d)));
now
per cases by NAT_1:14;
suppose
A8: j = 0;
1|->(F"**"(i|->d)) = <*F"**"(i|->d)*> by FINSEQ_2:59;
hence thesis by A8,FINSOP_1:11;
end;
suppose
A9: j >= 1+0;
then j > 0;
then i*j > i*0 by A5,XREAL_1:68;
then
A10: i*j >= 1+0 by NAT_1:13;
F"**"((i*(j+1))|->d) = F"**"((i*j+i*1)|->d)
.= F.(F"**"((i*j)|->d),F"**"(i|->d)) by A1,A2,A10,Th26
.= F.(F"**"((i*j)|->d),F"**"(1|->(F"**"(i|->d)))) by FINSOP_1:16
.= F"**"((j+1)|->(F"**"(i|->d))) by A1,A7,A9,Th26;
hence thesis;
end;
end;
hence thesis;
end;
A11: X[0];
for j holds X[j] from NAT_1:sch 2(A11,A6);
hence thesis by A5;
end;
end;
theorem Th28:
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)
proof
assume that
A1: F is having_a_unity and
A2: H is having_a_unity and
A3: h.the_unity_wrt F = the_unity_wrt H and
A4: for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2);
defpred X[FinSequence of D] means h.(F"**"$1) = H "**"(h*$1);
A5: for q,d st X[q] holds X[q^<*d*>]
proof
let q,d such that
A6: h.(F"**"q) = H "**"(h*q);
thus h.(F"**"(q^<*d*>)) = h.(F.(F"**"q,d)) by A1,FINSOP_1:4
.= H.(H "**"(h*q),h.d) by A4,A6
.= H "**" ((h*q)^<*h.d*>) by A2,FINSOP_1:4
.= H "**"(h*(q^<*d*>)) by FINSEQOP:8;
end;
h.(F"**"<*>D) = h.(the_unity_wrt F) by A1,FINSOP_1:10
.= H "**"(<*>E) by A2,A3,FINSOP_1:10
.= H "**"(h*<*>D);
then
A7: X[<*>D];
X[q] from FINSEQ_2:sch 2(A7,A5);
hence thesis;
end;
theorem
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)
by Th28;
theorem
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)
proof
assume that
A1: F is associative and
A2: F is having_a_unity and
A3: F is having_an_inverseOp and
A4: G is_distributive_wrt F;
set e = the_unity_wrt F;
set u = G[;](d,id D);
u is_distributive_wrt F by A4,FINSEQOP:54;
then
A5: for d1,d2 holds u.(F.(d1,d2)) = F.(u.d1,u.d2);
G[;](d,id D).e = e by A1,A2,A3,A4,FINSEQOP:69;
hence thesis by A2,A5,Th28;
end;
theorem
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)
proof
assume that
A1: F is commutative associative and
A2: F is having_a_unity and
A3: F is having_an_inverseOp;
set e = the_unity_wrt F, u = the_inverseOp_wrt F;
u is_distributive_wrt F by A1,A2,A3,FINSEQOP:63;
then
A4: for d1,d2 holds u.(F.(d1,d2)) = F.(u.d1,u.d2);
u.e = e by A1,A2,A3,FINSEQOP:61;
hence thesis by A2,A4,Th28;
end;
theorem Th32:
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))
proof
assume that
A1: F is commutative & F is associative & F is having_a_unity & e =
the_unity_wrt F and
A2: G.(e,e) = e and
A3: F.(G.(d1,d2),G.(d3,d4))= G.(F.(d1,d3),F.(d2,d4)) and
A4: len p = len q;
A5: len p = len(G.:(p,q)) by A4,FINSEQ_2:72;
A6: dom(G.:(p,q)) = Seg len(G.:(p,q)) by FINSEQ_1:def 3;
A7: dom q = Seg len q by FINSEQ_1:def 3;
A8: dom p = Seg len p by FINSEQ_1:def 3;
thus G.(F "**"p,F "**"q) = G.(F $$(findom p,[#](p,e)),F "**"q) by A1,Def2
.= G.(F $$(findom p,[#](p,e)),F $$(findom q,[#](q,e))) by A1,Def2
.= F $$(findom p,G.:([#](p,e),[#](q,e))) by A1,A2,A3,A4,A8,A7,Th9
.= F $$(findom(G.:(p,q)),[#](G.:(p,q),e)) by A2,A4,A5,A8,A6,Lm4
.= F "**"(G.:(p,q)) by A1,Def2;
end;
theorem Th33:
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))
proof
len T1 = i & len T2 = i by CARD_1:def 7;
hence thesis by Th32;
end;
theorem Th34:
F is commutative associative & F is having_a_unity & len p = len
q implies F.(F"**"p,F"**"q) = F "**"(F.:(p,q))
proof
set e = the_unity_wrt F;
assume
A1: F is commutative & F is associative & F is having_a_unity;
then
F.(e,e) = e & for d1,d2,d3,d4 holds F.(F.(d1,d2),F.(d3,d4))= F.(F.(d1,d3
),F. (d2,d4)) by Lm3,SETWISEO:15;
hence thesis by A1,Th32;
end;
theorem Th35:
F is commutative associative & F is having_a_unity implies
F.(F"**"T1,F"**"T2) = F "**"(F.:(T1,T2))
proof
len T1 = i & len T2 = i by CARD_1:def 7;
hence thesis by Th34;
end;
theorem
F is commutative associative & F is having_a_unity implies
F"**"(i|->(F.(d1,d2))) = F.(F"**"(i|->d1),F"**"(i|->d2))
proof
reconsider T1 = i|->d1, T2 = i|->d2 as Element of i-tuples_on D;
i|->(F.(d1,d2)) = F.:(T1,T2) by FINSEQOP:17;
hence thesis by Th35;
end;
theorem
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))
proof
assume that
A1: F is commutative associative & F is having_a_unity and
A2: F is having_an_inverseOp & G = F*(id D,the_inverseOp_wrt F);
set 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)) by A1,A2,FINSEQOP:86,89;
hence thesis by A1,Th33;
end;
theorem Th38:
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))
proof
assume that
A1: F is commutative & F is associative & F is having_a_unity & e =
the_unity_wrt F and
A2: G is_distributive_wrt F and
A3: G.(d,e) = e;
A4: len p = len(G[;](d,p)) & Seg len p = dom p by FINSEQ_1:def 3,FINSEQ_2:78;
A5: Seg len(G[;](d,p)) = dom(G[;](d,p)) by FINSEQ_1:def 3;
thus G.(d,F"**"p) = G.(d,F$$(findom p,[#](p,e))) by A1,Def2
.= F $$(findom p,G[;](d,[#](p,e))) by A1,A2,A3,Th12
.= F $$(findom p,[#](G[;](d,p),e)) by A3,Lm6
.= F "**"(G[;](d,p)) by A1,A4,A5,Def2;
end;
theorem Th39:
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))
proof
assume that
A1: F is commutative associative & F is having_a_unity & e =
the_unity_wrt F and
A2: G is_distributive_wrt F and
A3: G.(e,d) = e;
A4: len p = len(G[:](p,d)) & Seg len p = dom p by FINSEQ_1:def 3,FINSEQ_2:84;
A5: Seg len(G[:](p,d)) = dom(G[:](p,d)) by FINSEQ_1:def 3;
thus G.(F"**"p,d) = G.(F$$(findom p,[#](p,e)),d) by A1,Def2
.= F $$(findom p,G[:]([#](p,e),d)) by A1,A2,A3,Th13
.= F $$(findom p,[#](G[:](p,d),e)) by A3,Lm5
.= F "**"(G[:](p,d)) by A1,A4,A5,Def2;
end;
theorem
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))
proof
assume that
A1: F is commutative associative & F is having_a_unity and
A2: F is having_an_inverseOp and
A3: G is_distributive_wrt F;
set e = the_unity_wrt F;
G.(d,e) = e by A1,A2,A3,FINSEQOP:66;
hence thesis by A1,A3,Th38;
end;
theorem
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))
proof
assume that
A1: F is commutative associative & F is having_a_unity and
A2: F is having_an_inverseOp and
A3: G is_distributive_wrt F;
set e = the_unity_wrt F;
G.(e,d) = e by A1,A2,A3,FINSEQOP:66;
hence thesis by A1,A3,Th39;
end;