:: Semilattice Operations on Finite Subsets
:: by Andrzej Trybulec
::
:: Received September 18, 1989
:: 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 TARSKI, XBOOLE_0, FUNCT_1, RELAT_1, ZFMISC_1, SUBSET_1, FINSUB_1,
BINOP_1, FINSET_1, FUNCOP_1, SETWISEO;
notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ZFMISC_1, RELAT_1, FUNCT_1,
FINSUB_1, RELSET_1, FINSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1;
constructors ENUMSET1, PARTFUN1, BINOP_1, FUNCOP_1, FINSET_1, FINSUB_1,
RELSET_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, FINSET_1, FINSUB_1,
RELAT_1, FUNCT_3, ZFMISC_1;
requirements BOOLE, SUBSET;
definitions BINOP_1, TARSKI;
equalities RELAT_1;
expansions BINOP_1, TARSKI;
theorems FINSUB_1, ZFMISC_1, SUBSET_1, BINOP_1, TARSKI, FUNCT_1, FUNCT_2,
FUNCOP_1, ENUMSET1, RELAT_1, XBOOLE_0, XBOOLE_1;
schemes FINSET_1, FUNCT_2, BINOP_1, SUBSET_1;
begin :: Auxiliary Theorems
reserve x,y,z,X,Y for set;
theorem Th1:
{x} c= {x,y,z}
proof
{x,y,z} = {x} \/ {y,z} by ENUMSET1:2;
hence thesis by XBOOLE_1:7;
end;
theorem Th2:
{x,y} c= {x,y,z}
proof
{x,y,z} = {x,y} \/ {z} by ENUMSET1:3;
hence thesis by XBOOLE_1:7;
end;
::$CT 3
theorem Th3:
for X,Y for f being Function holds f.:(Y \ f"X) = f.:Y \ X
proof
let X,Y;
let f be Function;
now
let x be object;
thus x in f.:(Y \ f"X) implies x in f.:Y \ X
proof
assume x in f.:(Y \ f"X);
then consider z being object such that
A1: z in dom f and
A2: z in Y \ f"X and
A3: f.z = x by FUNCT_1:def 6;
not z in f"X by A2,XBOOLE_0:def 5;
then
A4: not x in X by A1,A3,FUNCT_1:def 7;
f.z in f.:Y by A1,A2,FUNCT_1:def 6;
hence thesis by A3,A4,XBOOLE_0:def 5;
end;
assume
A5: x in f.:Y \ X;
then consider z being object such that
A6: z in dom f and
A7: z in Y and
A8: f.z = x by FUNCT_1:def 6;
not x in X by A5,XBOOLE_0:def 5;
then not z in f"X by A8,FUNCT_1:def 7;
then z in Y \ f"X by A7,XBOOLE_0:def 5;
hence x in f.:(Y \ f"X) by A6,A8,FUNCT_1:def 6;
end;
hence thesis by TARSKI:2;
end;
reserve X,Y for non empty set,
f for Function of X,Y;
theorem Th4:
for x being Element of X holds x in f"{f.x}
proof
let x be Element of X;
f.x in {f.x} by TARSKI:def 1;
hence thesis by FUNCT_2:38;
end;
theorem Th5:
for x being Element of X holds Im(f,x) = {f.x}
proof
let x be Element of X;
for y be object holds y in f.:{x} iff y = f.x
proof
let y be object;
thus y in f.:{x} implies y = f.x
proof
assume y in f.:{x};
then ex z being object st z in dom f & z in {x} & f.z = y
by FUNCT_1:def 6;
hence thesis by TARSKI:def 1;
end;
x in {x} by TARSKI:def 1;
hence thesis by FUNCT_2:35;
end;
hence thesis by TARSKI:def 1;
end;
:: Theorems related to Fin ...
theorem Th6:
for B being Element of Fin X for x st x in B holds x is Element of X
proof
let B be Element of Fin X;
A1: B c= X by FINSUB_1:def 5;
let x;
assume x in B;
hence thesis by A1;
end;
theorem
for A being (Element of Fin X), B being set for f being Function of X,
Y st for x being Element of X holds x in A implies f.x in B holds f.:A c= B
proof
let A be (Element of Fin X), B be set;
let f be Function of X,Y such that
A1: for x being Element of X holds x in A implies f.x in B;
let x be object;
assume x in f.:A;
then consider y being object such that
y in dom f and
A2: y in A and
A3: x = f.y by FUNCT_1:def 6;
reconsider y as Element of X by A2,Th6;
x = f.y by A3;
hence thesis by A1,A2;
end;
theorem Th8:
for X being set for B being Element of Fin X for A being set st
A c= B holds A is Element of Fin X
proof
let X be set, B be Element of Fin X;
let A be set such that
A1: A c= B;
B c= X by FINSUB_1:def 5;
then A c= X by A1;
hence thesis by A1,FINSUB_1:def 5;
end;
Lm1: for A being Element of Fin X holds f.: A is Element of Fin Y by
FINSUB_1:def 5;
theorem Th9:
for B being Element of Fin X st B <> {} ex x being Element of X st x in B
proof
let B be Element of Fin X;
set x = the Element of B;
assume
A1: B <> {};
then reconsider x as Element of X by Th6;
take x;
thus thesis by A1;
end;
theorem Th10:
for A being Element of Fin X holds f.:A = {} implies A = {}
proof
let A be Element of Fin X;
assume
A1: f.:A = {};
assume A <> {};
then consider x being Element of X such that
A2: x in A by Th9;
f.x in f.:A by A2,FUNCT_2:35;
hence contradiction by A1;
end;
registration
let X be set;
cluster empty for Element of Fin X;
existence
proof
{} is Element of Fin X by FINSUB_1:7;
hence thesis;
end;
end;
definition
let X be set;
func {}.X -> empty Element of Fin X equals
{};
coherence by FINSUB_1:7;
end;
scheme
FinSubFuncEx{ A()->non empty set, B()->(Element of Fin A()), P[set,set] } :
ex f being Function of A(), Fin A() st for b,a being Element of A() holds a in
f.b iff a in B() & P[a,b] proof
defpred X[set,Element of Fin A()] means for a being Element of A() holds a
in $2 iff a in B() & P[a,$1];
A1: now
reconsider B = B() as Subset of A() by FINSUB_1:def 5;
let x be Element of A();
defpred X[set] means $1 in B() & P[$1,x];
consider y being Subset of A() such that
A2: for a being Element of A() holds a in y iff X[a] from SUBSET_1:sch
3;
for x being Element of A() holds x in y implies x in B by A2;
then y c= B();
then reconsider y as Element of Fin A() by FINSUB_1:def 5;
take y9 = y;
thus X[x,y9] by A2;
end;
thus ex f being Function of A(), Fin A() st for x being Element of A() holds
X[x,f.x] from FUNCT_2:sch 3(A1);
end;
:: theorems related to BinOp of ...
definition
let X be non empty set, F be BinOp of X;
attr F is having_a_unity means
ex x being Element of X st x is_a_unity_wrt F;
end;
theorem Th11:
for X being non empty set, F being BinOp of X holds F is
having_a_unity iff the_unity_wrt F is_a_unity_wrt F
by BINOP_1:def 8;
theorem Th12:
for X being non empty set, F being BinOp of X st F is
having_a_unity for x being Element of X holds F.(the_unity_wrt F, x) = x & F.(x
, the_unity_wrt F) = x
proof
let X be non empty set, F be BinOp of X;
assume F is having_a_unity;
then
A1: the_unity_wrt F is_a_unity_wrt F by Th11;
let x be Element of X;
thus thesis by A1,BINOP_1:3;
end;
:: Main part
registration
let X be non empty set;
cluster non empty for Element of Fin X;
existence
proof
set x = the Element of X;
{x} is Subset of X by SUBSET_1:41;
then {x} is Element of Fin X by FINSUB_1:def 5;
hence thesis;
end;
end;
notation
let X be non empty set, x be Element of X;
synonym {.x.} for {x};
let y be Element of X;
synonym {.x,y.} for {x,y};
let z be Element of X;
synonym {.x,y,z.} for {x,y,z};
end;
definition
let X be non empty set, x be Element of X;
redefine func {.x.} -> Element of Fin X; :: redefines {. (SETWISEO, synonym) → { (TARSKI, definition)
coherence
proof
{x} is Subset of X by SUBSET_1:41;
hence thesis by FINSUB_1:def 5;
end;
let y be Element of X;
redefine func {.x,y.} -> Element of Fin X; :: redefines {. (SETWISEO, synonym) → { (TARSKI, definition)
coherence
proof
{x,y} is Subset of X by SUBSET_1:34;
hence thesis by FINSUB_1:def 5;
end;
let z be Element of X;
redefine func {.x,y,z.} -> Element of Fin X; :: redefines {. (SETWISEO, synonym) → { (ENUMSET1, definition)
coherence
proof
{x,y,z} is Subset of X by SUBSET_1:35;
hence thesis by FINSUB_1:def 5;
end;
end;
definition
let X be set;
let A,B be Element of Fin X;
redefine func A \/ B -> Element of Fin X; :: redefines \/ (XBOOLE_0, definition)
coherence by FINSUB_1:1;
end;
definition
let X be set;
let A,B be Element of Fin X;
redefine func A \ B -> Element of Fin X; :: redefines \ (XBOOLE_0, definition)
coherence by FINSUB_1:1;
end;
scheme
FinSubInd1{ X() -> non empty set, P[set] } : for B being Element of Fin X()
holds P[B]
provided
A1: P[{}.X()] and
A2: for B9 being (Element of Fin X()), b being Element of X() holds P[B9
] & not b in B9 implies P[B9 \/ {b}]
proof
defpred X[set] means ex B9 being Element of Fin X() st B9 = $1 & P[B9];
let B be Element of Fin X();
A3: for x,A being set st x in B & A c= B & X[A] holds X[A \/ {x}]
proof
let x,A be set such that
A4: x in B and
A5: A c= B and
A6: ex B9 being Element of Fin X() st B9 = A & P[B9];
reconsider x9 = x as Element of X() by A4,Th6;
reconsider A9 = A as Element of Fin X() by A5,Th8;
take Ax = A9 \/ {.x9.};
thus Ax = A \/ {x};
thus P[Ax] by A2,A6,ZFMISC_1:40;
end;
A7: B is finite;
A8: X[{}] by A1;
X[B] from FINSET_1:sch 2(A7,A8,A3);
hence thesis;
end;
scheme
FinSubInd2{ X() -> non empty set, P[Element of Fin X()] } : for B being non
empty Element of Fin X() holds P[B]
provided
A1: for x being Element of X() holds P[{.x.}] and
A2: for B1,B2 being non empty Element of Fin X() st P[B1] & P[B2] holds
P[B1 \/ B2]
proof
defpred X[set] means $1 <> {} implies ex B9 being Element of Fin X() st B9 =
$1 & P[B9];
let B be non empty Element of Fin X();
A3: for x,A being set st x in B & A c= B & X[A] holds X[A \/ {x}]
proof
let x,A be set such that
A4: x in B and
A5: A c= B and
A6: A <> {} implies ex B9 being Element of Fin X() st B9 = A & P[B9] and
A \/ {x} <> {};
reconsider x9 = x as Element of X() by A4,Th6;
reconsider A9 = A as Element of Fin X() by A5,Th8;
take A9 \/ {.x9.};
thus A9 \/ {.x9.} =A \/ {x};
A7: P[{.x9.}] by A1;
per cases;
suppose
A = {};
hence thesis by A1;
end;
suppose
A <> {};
hence thesis by A2,A6,A7;
end;
end;
A8: X[{}];
A9: B is finite;
X[B] from FINSET_1:sch 2(A9,A8,A3);
hence thesis;
end;
scheme
FinSubInd3{ X() -> non empty set, P[set] } : for B being Element of Fin X()
holds P[B]
provided
A1: P[{}.X()] and
A2: for B9 being (Element of Fin X()), b being Element of X() holds P[B9
] implies P[B9 \/ {b}]
proof
A3: for B9 being (Element of Fin X()), b being Element of X() holds P[B9] &
not b in B9 implies P[B9 \/ {b}] by A2;
A4: P[{}.X()] by A1;
thus for B being Element of Fin X() holds P[B] from FinSubInd1(A4, A3);
end;
definition
let X, Y be non empty set;
let F be BinOp of Y;
let B be Element of Fin X;
let f be Function of X,Y;
assume that
A1: B <> {} or F is having_a_unity and
A2: F is commutative and
A3: F is associative;
func F $$ (B,f) -> Element of Y means
:Def3:
ex G being Function of Fin X, Y
st it = G.B & (for e being Element of Y st e is_a_unity_wrt F holds G.{} = e) &
(for x being Element of X holds G.{x} = f.x) & for B9 being Element of Fin X st
B9 c= B & B9 <> {} for x being Element of X st x in B \ B9 holds G.(B9 \/ {x})
= F.(G.B9,f.x);
existence
proof
defpred X[set] means ex G being Function of Fin X, Y st (for e being
Element of Y st e is_a_unity_wrt F holds G.{} = e) & (for x being Element of X
holds G.{x} = f.x) & for B9 being Element of Fin X st B9 c= $1 & B9 <> {} for x
being Element of X st x in $1 \ B9 holds G.(B9 \/ {x}) = F.(G.B9, f.x);
A4: for B9 being Element of Fin X, b being Element of X holds X[B9] & not
b in B9 implies X[B9 \/ {b}]
proof
let B be (Element of Fin X), x be Element of X;
given G being Function of Fin X, Y such that
A5: for e being Element of Y st e is_a_unity_wrt F holds G.{} = e and
A6: for x being Element of X holds G.{x} = f.x and
A7: for B9 being Element of Fin X st B9 c= B & B9 <> {} for x being
Element of X st x in B \ B9 holds G.(B9 \/ {x}) = F.(G.B9, f.x);
assume
A8: not x in B;
thus ex G being Function of Fin X, Y st (for e being Element of Y st e
is_a_unity_wrt F holds G.{} = e) & (for x being Element of X holds G.{x} = f.x)
& for B9 being Element of Fin X st B9 c= B \/ {x} & B9 <> {} for x9 being
Element of X st x9 in (B \/ {x}) \ B9 holds G.(B9 \/ {x9}) = F.(G.B9, f.x9)
proof
defpred X[set,set] means (for C being Element of Fin X st C <> {} & C
c= B & $1 = C \/ {.x.} holds $2 = F.(G.C, f.x)) & ((not ex C being Element of
Fin X st C <> {} & C c= B & $1 = C \/ {.x.}) implies $2 = G.$1);
A9: now
let B9 be Element of Fin X;
thus ex y being Element of Y st X[B9,y]
proof
A10: now
given C being Element of Fin X such that
A11: C <> {} and
A12: C c= B and
A13: B9 = C \/ {x};
take y = F.(G.C, f.x);
for C being Element of Fin X st C <> {} & C c= B & B9 = C
\/ {x} holds y = F.(G.C, f.x)
proof
not x in C by A8,A12;
then
A14: C c= B9 \ {x} by A13,XBOOLE_1:7,ZFMISC_1:34;
B9 \ {x} = C \ {x} by A13,XBOOLE_1:40;
then
A15: B9 \ {x} = C by A14,XBOOLE_0:def 10;
let C1 be Element of Fin X such that
C1 <> {} and
A16: C1 c= B and
A17: B9 = C1 \/ {x};
not x in C1 by A8,A16;
then
A18: C1 c= B9 \ {x} by A17,XBOOLE_1:7,ZFMISC_1:34;
B9 \{x} = C1 \ {x} by A17,XBOOLE_1:40;
hence thesis by A18,A15,XBOOLE_0:def 10;
end;
hence thesis by A11,A12,A13;
end;
now
assume
A19: not ex C being Element of Fin X st C <> {} & C c= B &
B9 = C \/ {x};
take y = G.B9;
thus for C being Element of Fin X st C <> {} & C c= B & B9 = C
\/ {x} holds y = F.(G.C, f.x) by A19;
thus (not ex C being Element of Fin X st C <> {} & C c= B & B9 =
C \/ {x}) implies y = G.B9;
end;
hence thesis by A10;
end;
end;
consider H being Function of Fin X, Y such that
A20: for B9 being Element of Fin X holds X[B9,H.B9] from FUNCT_2:
sch 3 (A9);
take J = H;
now
given C being Element of Fin X such that
A21: C <> {} and
A22: C c= B and
A23: {x} = C \/ {x};
C = {x} by A21,A23,XBOOLE_1:7,ZFMISC_1:33;
then x in C by TARSKI:def 1;
hence contradiction by A8,A22;
end;
then
A24: J.{x} = G.{.x.} by A20;
thus for e being Element of Y st e is_a_unity_wrt F holds J.{} = e
proof
reconsider E = {} as Element of Fin X by FINSUB_1:7;
not ex C being Element of Fin X st C <> {} & C c= B & E = C \/ { x};
then J.E = G.E by A20;
hence thesis by A5;
end;
thus for x being Element of X holds J.{x} = f.x
proof
let x9 be Element of X;
now
given C being Element of Fin X such that
A25: C <> {} and
A26: C c= B and
A27: {x9} = C \/ {x};
A28: C = {x9} by A25,A27,XBOOLE_1:7,ZFMISC_1:33;
x = x9 by A27,XBOOLE_1:7,ZFMISC_1:18;
then x in C by A28,TARSKI:def 1;
hence contradiction by A8,A26;
end;
hence J.{x9} = G.{.x9.} by A20
.= f.x9 by A6;
end;
let B9 be Element of Fin X such that
A29: B9 c= B \/ {x} and
A30: B9 <> {};
let x9 be Element of X;
assume
A31: x9 in (B \/ {x}) \ B9;
then
A32: not x9 in B9 by XBOOLE_0:def 5;
per cases;
suppose
A33: x in B9;
then
A34: x9 in B by A31,A32,ZFMISC_1:136;
per cases;
suppose
A35: B9 = {x};
hence J.(B9 \/ {.x9.}) = F.(G.{.x9.}, f.x)
by A20,A34,ZFMISC_1:31
.= F.(f.x9, f.x) by A6
.= F.(f.x, f.x9) by A2
.= F.(J.B9, f.x9) by A6,A24,A35;
end;
suppose
B9 <> {x};
then not B9 c= {x} by A30,ZFMISC_1:33;
then
A36: B9 \ {x} <> {} by XBOOLE_1:37;
set C = (B9 \ {.x.}) \/ {.x9.};
not x9 in B9 \ {x} by A31,XBOOLE_0:def 5;
then
A37: x9 in B \(B9 \ {x}) by A34,XBOOLE_0:def 5;
B9 \ {x} c= B by A29,XBOOLE_1:43;
then
A38: C c= B by A33,A31,A32,ZFMISC_1:136,137;
B9 \/ {.x9.} = B9 \/ {x} \/ {x9} by A33,ZFMISC_1:40
.= (B9 \ {x}) \/ {x} \/ {x9} by XBOOLE_1:39
.= C \/ {.x.} by XBOOLE_1:4;
hence J.(B9 \/ {.x9.}) = F.(G.C, f.x) by A20,A38
.= F.(F.(G.(B9\{.x.}), f.x9), f.x) by A7,A29,A36,A37,XBOOLE_1:43
.= F.(G.(B9\{.x.}),F.(f.x9, f.x)) by A3
.= F.(G.(B9\{x}),F.(f.x, f.x9)) by A2
.= F.(F.(G.(B9\{.x.}), f.x), f.x9) by A3
.= F.(J.((B9\{.x.})\/{.x.}), f.x9) by A20,A29,A36,XBOOLE_1:43
.= F.(J.(B9 \/ {x}), f.x9) by XBOOLE_1:39
.= F.(J.B9, f.x9) by A33,ZFMISC_1:40;
end;
end;
suppose
A39: not x in B9;
then
A40: B9 c= B by A29,ZFMISC_1:135;
A41: not ex C being Element of Fin X st C <> {} & C c= B & B9 = C
\/ {x} by A39,ZFMISC_1:136;
per cases;
suppose
A42: x <> x9;
then x9 in B by A31,ZFMISC_1:136;
then
A43: x9 in B \ B9 by A32,XBOOLE_0:def 5;
not x in B9 \/ {x9} by A39,A42,ZFMISC_1:136;
then not ex C being Element of Fin X st C <> {} & C c= B & B9 \/
{x9} = C \/ {x} by ZFMISC_1:136;
hence J.(B9 \/ {.x9.}) = G.(B9 \/ {.x9.}) by A20
.= F.(G.B9, f.x9) by A7,A30,A40,A43
.= F.(J.B9, f.x9) by A20,A41;
end;
suppose
x = x9;
hence J.(B9 \/ {.x9.}) = F.(G.B9, f.x9)
by A20,A29,A30,A39,ZFMISC_1:135
.= F.(J.B9, f.x9) by A20,A41;
end;
end;
end;
end;
A44: X[{}.X]
proof
consider e being Element of Y such that
A45: (ex e being Element of Y st e is_a_unity_wrt F) implies e =
the_unity_wrt F;
defpred X[set,set] means (for x9 being Element of X st $1 = {x9} holds
$2 = f.x9) & (not (ex x9 being Element of X st $1 = {x9}) implies $2 = e);
A46: now
let x be Element of Fin X;
A47: now
given x9 being Element of X such that
A48: x = {x9};
take y = f.x9;
thus for x9 being Element of X st x = {x9} holds y = f.x9 by A48,
ZFMISC_1:3;
thus not (ex x9 being Element of X st x = {x9}) implies y = e by A48;
end;
now
assume
A49: not ex x9 being Element of X st x = {x9};
take y = e;
thus (for x9 being Element of X st x = {x9} holds y = f.x9) & (not (
ex x9 being Element of X st x = {x9}) implies y = e) by A49;
end;
hence ex y being Element of Y st X[x,y] by A47;
end;
consider G9 being Function of Fin X, Y such that
A50: for B9 being Element of Fin X holds X[B9,G9.B9] from FUNCT_2:
sch 3(A46 );
take G = G9;
thus for e being Element of Y st e is_a_unity_wrt F holds G.{} = e
proof
reconsider E = {} as Element of Fin X by FINSUB_1:7;
let e9 be Element of Y such that
A51: e9 is_a_unity_wrt F;
not ex x9 being Element of X st E = {x9};
hence G.{} = e by A50
.= e9 by A45,A51,BINOP_1:def 8;
end;
thus for x being Element of X holds G.{.x.} = f.x by A50;
thus for B9 being Element of Fin X st B9 c= {}.X & B9 <> {} for x being
Element of X st x in {}.X \ B9 holds G.(B9 \/ {x}) = F.(G.B9, f.x);
end;
for B being Element of Fin X holds X[B] from FinSubInd1(A44,A4);
then consider G being Function of Fin X, Y such that
A52: ( ( for e being Element of Y st e is_a_unity_wrt F holds G.{} =
e)& for x being Element of X holds G.{x} = f.x )& for B9 being Element of Fin X
st B9 c= B & B9 <> {} for x being Element of X st x in B \ B9 holds G.(B9 \/ {x
}) = F.(G .B9, f.x);
take G.B, G;
thus thesis by A52;
end;
uniqueness
proof
let x,y be Element of Y;
given G1 being Function of Fin X, Y such that
A53: x = G1.B and
A54: for e being Element of Y st e is_a_unity_wrt F holds G1.{} = e and
A55: for x being Element of X holds G1.{x} = f.x and
A56: for B9 being Element of Fin X st B9 c= B & B9 <> {} for x being
Element of X st x in B \ B9 holds G1.(B9 \/ {x}) = F.(G1.B9,f.x);
given G2 being Function of Fin X, Y such that
A57: y = G2.B and
A58: for e being Element of Y st e is_a_unity_wrt F holds G2.{} = e and
A59: for x being Element of X holds G2.{x} = f.x and
A60: for B9 being Element of Fin X st B9 c= B & B9 <> {} for x being
Element of X st x in B \ B9 holds G2.(B9 \/ {x}) = F.(G2.B9,f.x);
per cases;
suppose
A61: B = {};
thus x = the_unity_wrt F by A53,A54,A61,A1,Th11
.= y by A57,A58,A61,A1,Th11;
end;
suppose
A62: B <> {};
defpred X[set] means $1 c= B & $1 <> {} implies G1.$1 = G2.$1;
A63: for B9 being Element of Fin X, b being Element of X holds X[B9] &
not b in B9 implies X[B9 \/ {b}]
proof
let B9 be (Element of Fin X), x be Element of X;
assume
A64: B9 c= B & B9 <> {} implies G1.B9 = G2.B9;
assume
A65: not x in B9;
assume
A66: B9 \/ {x} c= B;
then
A67: B9 c= B by ZFMISC_1:137;
assume B9 \/ {x} <> {};
x in B by A66,ZFMISC_1:137;
then
A68: x in B \ B9 by A65,XBOOLE_0:def 5;
per cases;
suppose
A69: B9 = {};
hence G1.(B9 \/ {x}) = f.x by A55
.= G2.(B9 \/ {x}) by A59,A69;
end;
suppose
A70: B9 <> {};
hence G1.(B9 \/ {x}) = F.(G1.B9, f.x) by A56,A67,A68
.= G2.(B9 \/ {x}) by A60,A64,A67,A68,A70;
end;
end;
A71: X[{}.X];
for B9 being Element of Fin X holds X[B9] from FinSubInd1(A71,
A63 );
hence thesis by A53,A57,A62;
end;
end;
end;
theorem Th13:
for X, Y being non empty set for F being BinOp of Y for B being
Element of Fin X for f being Function of X,Y st (B <> {} or F is having_a_unity
) & F is idempotent & F is commutative & F is associative for IT being Element
of Y holds IT = F $$ (B,f) iff ex G being Function of Fin X, Y st IT = G.B & (
for e being Element of Y st e is_a_unity_wrt F holds G.{} = e) & (for x being
Element of X holds G.{x} = f.x) & for B9 being Element of Fin X st B9 c= B & B9
<> {} for x being Element of X st x in B holds G.(B9 \/ {x}) = F.(G.B9,f.x)
proof
let X, Y be non empty set;
let F be BinOp of Y;
let B be Element of Fin X;
let f be Function of X,Y;
assume that
A1: B <> {} or F is having_a_unity and
A2: F is idempotent and
A3: F is commutative and
A4: F is associative;
let IT be Element of Y;
thus IT = F $$ (B,f) implies ex G being Function of Fin X, Y st IT = G.B & (
for e being Element of Y st e is_a_unity_wrt F holds G.{} = e) & (for x being
Element of X holds G.{x} = f.x) & for B9 being Element of Fin X st B9 c= B & B9
<> {} for x being Element of X st x in B holds G.(B9 \/ {x}) = F.(G.B9,f.x)
proof
assume IT = F $$ (B,f);
then consider G being Function of Fin X, Y such that
A5: IT = G.B & for e being Element of Y st e is_a_unity_wrt F holds G.
{} = e and
A6: for x being Element of X holds G.{x} = f.x and
A7: for B9 being Element of Fin X st B9 c= B & B9 <> {} for x being
Element of X st x in B \ B9 holds G.(B9 \/ {x}) = F.(G.B9,f.x) by A1,A3,A4
,Def3;
for B9 being Element of Fin X st B9 c= B & B9 <> {} for x being
Element of X st x in B holds G.(B9 \/ {x}) = F.(G.B9,f.x)
proof
let B9 be Element of Fin X such that
A8: B9 c= B and
A9: B9 <> {};
let x be Element of X such that
A10: x in B;
per cases;
suppose
x in B9;
then
A11: B9 \/ {x} = B9 by ZFMISC_1:40;
then
A12: {x} c= B9 by XBOOLE_1:7;
not x in B9 \ {x} by ZFMISC_1:56;
then
A13: x in B \ (B9 \ {x}) by A10,XBOOLE_0:def 5;
per cases;
suppose
A14: B9 = {x};
hence G.(B9 \/ {x}) = F.(f.x, f.x) by A2,A6
.= F.(G.B9,f.x) by A6,A14;
end;
suppose
B9 <> {x};
then not B9 c= {x} by A12,XBOOLE_0:def 10;
then B9 \ {x} <> {} by XBOOLE_1:37;
then
A15: G.(B9 \ {.x.} \/ {.x.}) = F.(G.(B9 \ {.x.}), f.x) by A7,A8,A13,
XBOOLE_1:1;
thus G.(B9 \/ {x})
= F.(G.(B9 \ {x}), F.(f.x,f.x)) by A2,A15,XBOOLE_1:39
.= F.(F.(G.(B9 \ {.x.}),f.x), f.x) by A4
.= F.(G.B9,f.x) by A11,A15,XBOOLE_1:39;
end;
end;
suppose
not x in B9;
then x in B \ B9 by A10,XBOOLE_0:def 5;
hence thesis by A7,A8,A9;
end;
end;
hence thesis by A5,A6;
end;
given G being Function of Fin X, Y such that
A16: ( IT = G.B & for e being Element of Y st e is_a_unity_wrt F holds G
.{} = e ) & for x being Element of X holds G.{x} = f.x and
A17: for B9 being Element of Fin X st B9 c= B & B9 <> {} for x being
Element of X st x in B holds G.(B9 \/ {x}) = F.(G.B9,f.x);
for B9 being Element of Fin X st B9 c= B & B9 <> {} for x being Element
of X st x in B \ B9 holds G.(B9 \/ {x}) = F.(G.B9,f.x)
proof
let B9 be Element of Fin X such that
A18: B9 c= B & B9 <> {};
let x be Element of X;
assume x in B \ B9;
then x in B by XBOOLE_0:def 5;
hence thesis by A17,A18;
end;
hence thesis by A1,A3,A4,A16,Def3;
end;
reserve X, Y for non empty set,
F for (BinOp of Y),
B for (Element of Fin X),
f for Function of X,Y;
theorem Th14:
F is commutative & F is associative implies for b being Element
of X holds F $$ ({.b.},f) = f.b
proof
assume
A1: F is commutative & F is associative;
let b be Element of X;
ex G being Function of Fin X, Y st F $$ ({.b.},f) = G.{b} & (for e being
Element of Y st e is_a_unity_wrt F holds G.{} = e) & ( for x being Element of X
holds G.{x} = f.x) & for B9 being Element of Fin X st B9 c= {b} & B9 <> {} for
x being Element of X st x in {b} \ B9 holds G.(B9 \/ {x}) = F.(G.B9,f.x) by A1
,Def3;
hence thesis;
end;
theorem Th15:
F is idempotent & F is commutative & F is associative implies
for a,b being Element of X holds F $$ ({.a,b.},f) = F.(f.a, f.b)
proof
assume
A1: F is idempotent & F is commutative & F is associative;
let a,b be Element of X;
consider G being Function of Fin X, Y such that
A2: F $$ ({.a,b.},f) = G.{a,b} and
for e being Element of Y st e is_a_unity_wrt F holds G.{} = e and
A3: for x being Element of X holds G.{x} = f.x and
A4: for B9 being Element of Fin X st B9 c= {a,b} & B9 <> {} for x being
Element of X st x in {a,b} holds G.(B9 \/ {x}) = F.(G.B9,f.x) by A1,Th13;
A5: b in {a,b} by TARSKI:def 2;
thus F $$ ({.a,b.},f) = G.({.a.} \/ {.b.}) by A2,ENUMSET1:1
.= F.(G.{.a.}, f.b) by A4,A5,ZFMISC_1:7
.= F.(f.a, f.b) by A3;
end;
theorem Th16:
F is idempotent & F is commutative & F is associative implies
for a,b,c being Element of X holds F $$ ({.a,b,c.},f) = F.(F.(f.a, f.b), f.c)
proof
assume
A1: F is idempotent & F is commutative & F is associative;
let a,b,c be Element of X;
consider G being Function of Fin X, Y such that
A2: F $$ ({.a,b,c.},f) = G.{a,b,c} and
for e being Element of Y st e is_a_unity_wrt F holds G.{} = e and
A3: for x being Element of X holds G.{x} = f.x and
A4: for B9 being Element of Fin X st B9 c= {a,b,c} & B9 <> {} for x
being Element of X st x in {a,b,c} holds G.(B9 \/ {x}) = F.(G.B9,f.x) by A1
,Th13;
A5: b in {a,b,c} by ENUMSET1:def 1;
A6: G.{a,b} = G.({a} \/ {b}) by ENUMSET1:1
.= F.(G.{.a.}, f.b) by A4,A5,Th1
.= F.(f.a, f.b) by A3;
A7: c in {a,b,c} by ENUMSET1:def 1;
thus F $$ ({.a,b,c.},f) = G.({.a,b.} \/ {.c.}) by A2,ENUMSET1:3
.= F.(F.(f.a, f.b), f.c) by A4,A6,A7,Th2;
end;
:: If B is non empty
theorem Th17:
F is idempotent & F is commutative & F is associative & B <> {}
implies for x being Element of X holds F $$(B \/ {.x.}, f) = F.(F $$(B,f),f.x)
proof
assume
A1: F is idempotent & F is commutative & F is associative;
assume
A2: B <> {};
then consider G9 being Function of Fin X, Y such that
A3: F $$ (B,f) = G9.B and
for e being Element of Y st e is_a_unity_wrt F holds G9.{} = e and
A4: for x being Element of X holds G9.{x} = f.x and
A5: for B9 being Element of Fin X st B9 c= B & B9 <> {} for x being
Element of X st x in B holds G9.(B9 \/ {x}) = F.(G9.B9,f.x) by A1,Th13;
let x be Element of X;
consider G being Function of Fin X, Y such that
A6: F $$ (B \/ {.x.},f) = G.(B \/ {.x.}) and
for e being Element of Y st e is_a_unity_wrt F holds G.{} = e and
A7: for x being Element of X holds G.{x} = f.x and
A8: for B9 being Element of Fin X st B9 c= B \/ {x} & B9 <> {} for x9
being Element of X st x9 in B \/ {x} holds G.(B9 \/ {x9}) = F.(G.B9,f.x9) by A1
,Th13;
defpred X[set] means $1 <> {} & $1 c= B implies G.$1 = G9.$1;
A9: for B9 being Element of Fin X, b being Element of X holds X[B9] implies
X[B9 \/ {b}]
proof
A10: B c= B \/ {x} by XBOOLE_1:7;
let C be (Element of Fin X), y be Element of X such that
A11: C <> {} & C c= B implies G.C = G9.C;
assume that
C \/ {y} <> {} and
A12: C \/ {y} c= B;
A13: C c= B & y in B by A12,ZFMISC_1:137;
per cases;
suppose
A14: C = {};
hence G.(C \/ {y}) = f.y by A7
.= G9.(C \/ {y}) by A4,A14;
end;
suppose
A15: C <> {};
hence G.(C \/ {y}) = F.(G9.C, f.y) by A8,A11,A13,A10,XBOOLE_1:1
.= G9.(C \/ {y}) by A5,A13,A15;
end;
end;
A16: X[{}.X];
A17: for C being Element of Fin X holds X[C] from FinSubInd3(A16,A9);
x in B \/ {x} by ZFMISC_1:136;
hence F $$(B \/ {.x.}, f) = F.(G.B, f.x) by A2,A6,A8,XBOOLE_1:7
.= F.(F $$(B,f),f.x) by A2,A3,A17;
end;
theorem Th18:
F is idempotent & F is commutative & F is associative implies
for B1,B2 being Element of Fin X st B1 <> {} & B2 <> {} holds F $$ (B1 \/ B2,f)
= F.(F $$ (B1,f),F $$ (B2,f))
proof
assume that
A1: F is idempotent and
A2: F is commutative and
A3: F is associative;
let B1,B2 be Element of Fin X;
defpred X[Element of Fin X] means $1 <> {} implies F $$ (B1 \/ $1,f) = F.(F
$$ (B1,f),F $$ ($1,f));
assume
A4: B1 <> {};
A5: for B9 being Element of Fin X, b being Element of X holds X[B9] implies
X[B9 \/ {.b.}]
proof
let B be (Element of Fin X), x be Element of X such that
A6: B <> {} implies F $$ (B1 \/ B,f) = F.(F $$ (B1,f),F $$ (B,f)) and
B \/ {x} <> {};
per cases;
suppose
A7: B = {};
hence
F $$ (B1 \/ (B \/ {.x.}),f) = F.(F $$ (B1,f), f.x) by A1,A2,A3,A4,Th17
.= F.(F $$ (B1,f),F $$ (B \/ {.x.},f)) by A2,A3,A7,Th14;
end;
suppose
A8: B <> {};
thus F $$ (B1 \/ (B \/ {.x.}),f) = F $$ (B1 \/ B \/ {.x.},f) by
XBOOLE_1:4
.= F.(F.(F $$ (B1,f),F $$ (B,f)), f.x) by A1,A2,A3,A6,A8,Th17
.= F.(F $$ (B1,f),F.(F $$ (B,f), f.x)) by A3
.= F.(F $$ (B1,f),F $$ (B \/ {.x.},f)) by A1,A2,A3,A8,Th17;
end;
end;
A9: X[{}.X];
for B2 being Element of Fin X holds X[B2] from FinSubInd3(A9,A5);
hence thesis;
end;
theorem
F is commutative & F is associative & F is idempotent implies for x
being Element of X st x in B holds F.(f.x,F$$(B,f)) = F$$(B,f)
proof
assume that
A1: F is commutative & F is associative and
A2: F is idempotent;
let x be Element of X;
assume
A3: x in B;
thus F.(f.x,F$$(B,f)) = F.(F$$({.x.},f), F$$(B,f)) by A1,Th14
.= F$$({.x.} \/ B, f) by A1,A2,A3,Th18
.= F$$(B,f) by A3,ZFMISC_1:40;
end;
theorem
F is commutative & F is associative & F is idempotent implies for B,C
being Element of Fin X st B <> {} & B c= C holds F.(F$$(B,f),F$$(C,f)) = F$$(C,
f)
proof
assume
A1: F is commutative & F is associative & F is idempotent;
let B,C be Element of Fin X such that
A2: B <> {} and
A3: B c= C;
C <> {} by A2,A3;
hence F.(F$$(B,f),F$$(C,f)) = F$$(B \/ C,f) by A1,A2,Th18
.= F$$(C,f) by A3,XBOOLE_1:12;
end;
theorem Th21:
B <> {} & F is commutative & F is associative & F is idempotent
implies for a being Element of Y st for b being Element of X st b in B holds f.
b = a holds F$$(B,f) = a
proof
assume that
A1: B <> {} and
A2: F is commutative & F is associative and
A3: F is idempotent;
let a be Element of Y;
defpred X[Element of Fin X] means (for b being Element of X st b in $1 holds
f.b = a) implies F$$($1,f) = a;
A4: for B1,B2 being non empty Element of Fin X holds X[B1] & X[B2] implies X
[B1 \/ B2]
proof
let B1,B2 be non empty Element of Fin X;
assume that
A5: ( (for b being Element of X st b in B1 holds f.b = a) implies F$$
(B1,f) = a)&( (for b being Element of X st b in B2 holds f.b = a) implies F$$(
B2,f) = a) and
A6: for b being Element of X st b in B1 \/ B2 holds f.b = a;
A7: now
let b be Element of X;
assume b in B2;
then b in B1 \/ B2 by XBOOLE_0:def 3;
hence f.b = a by A6;
end;
now
let b be Element of X;
assume b in B1;
then b in B1 \/ B2 by XBOOLE_0:def 3;
hence f.b = a by A6;
end;
hence F$$(B1 \/ B2,f) = F.(a,a) by A2,A3,A5,A7,Th18
.= a by A3;
end;
A8: for x being Element of X holds X[{.x.}]
proof
let x be Element of X such that
A9: for b being Element of X st b in {x} holds f.b = a;
A10: x in { x } by TARSKI:def 1;
thus F$$({.x.},f) = f.x by A2,Th14
.= a by A9,A10;
end;
for B being non empty Element of Fin X holds X[B] from FinSubInd2(A8,
A4);
hence thesis by A1;
end;
theorem Th22:
F is commutative & F is associative & F is idempotent implies
for a being Element of Y st f.:B = {a} holds F$$(B,f) = a
proof
assume
A1: F is commutative & F is associative & F is idempotent;
let a be Element of Y;
assume
A2: f.:B = {a};
A3: for b being Element of X st b in B holds f.b = a
proof
let b be Element of X;
assume b in B;
then f.b in {a} by A2,FUNCT_2:35;
hence thesis by TARSKI:def 1;
end;
B <> {} by A2;
hence thesis by A1,A3,Th21;
end;
theorem Th23:
F is commutative & F is associative & F is idempotent implies
for f,g being Function of X,Y for A,B being Element of Fin X st A <> {} & f.:A
= g.:B holds F$$(A,f) = F$$(B,g)
proof
assume that
A1: F is commutative and
A2: F is associative and
A3: F is idempotent;
let f,g be Function of X,Y;
defpred X[Element of Fin X] means $1 <> {} implies for B being Element of
Fin X st f.:$1 = g.:B holds F$$($1,f) = F$$(B,g);
A4: for B9 being Element of Fin X, b being Element of X holds X[B9] implies
X[B9 \/ {.b.}]
proof
let A be (Element of Fin X), x be Element of X such that
A5: A <> {} implies for B being Element of Fin X st f.:A = g.:B holds
F$$(A,f) = F$$(B,g);
assume A \/ {x} <> {};
let B be Element of Fin X such that
A6: f.:(A \/ {x}) = g.:B;
per cases;
suppose
f.x in f.:A;
then consider x9 being Element of X such that
A7: x9 in A and
A8: f.x9 = f.x by FUNCT_2:65;
A9: g.:B = f.:A \/ Im(f,x) by A6,RELAT_1:120
.= f.:A \/ {f.x} by Th5
.= f.:A by A7,A8,FUNCT_2:35,ZFMISC_1:40;
thus F$$(A \/ {.x.},f) = F.(F$$(A,f), f.x) by A1,A2,A3,A7,Th17
.= F.(F$$(A \/ {.x9.},f), f.x) by A7,ZFMISC_1:40
.= F.(F.(F$$(A,f), f.x9), f.x) by A1,A2,A3,A7,Th17
.= F.(F$$(A,f), F.(f.x9, f.x9)) by A2,A8
.= F$$(A \/ {.x9.},f) by A1,A2,A3,A7,Th17
.= F$$(A,f) by A7,ZFMISC_1:40
.= F$$(B,g) by A5,A7,A9;
end;
suppose
A10: not f.x in f.:A;
per cases;
suppose
A11: A = {};
then
A12: g.:B = Im(f,x) by A6
.= {f.x} by Th5;
thus F$$(A \/ {.x.},f) = f.x by A1,A2,A11,Th14
.= F$$(B,g) by A1,A2,A3,A12,Th22;
end;
suppose
A13: A <> {};
reconsider B1 = B \ g"{f.x} as Element of Fin X by Th8;
A14: now
assume B1 = {};
then
A15: g.:B c= g.:g"{f.x} by RELAT_1:123,XBOOLE_1:37;
g.:g"{f.x} c= {f.x} by FUNCT_1:75;
then f.:(A \/ {x}) c= {f.x} by A6,A15;
then f.:A \/ f.:{x} c= {f.x} by RELAT_1:120;
then f.:A = f.:A /\ {f.x} by XBOOLE_1:11,28
.= {} by A10,XBOOLE_0:def 7,ZFMISC_1:50;
hence contradiction by A13,Th10;
end;
reconsider B2 = B /\ g"{f.x} as Element of Fin X by Th8,XBOOLE_1:17;
A16: B = B1 \/ B2 by XBOOLE_1:51;
A17: for b being Element of X st b in B2 holds g.b = f.x
proof
let b be Element of X;
assume b in B2;
then b in g"{f.x} by XBOOLE_0:def 4;
then g.b in {f.x} by FUNCT_1:def 7;
hence thesis by TARSKI:def 1;
end;
A18: f.:A = f.:A \ {f.x} by A10,ZFMISC_1:57
.= f.:A \ Im(f,x) by Th5
.= (f.:A \/ f.:{x}) \ f.:{x} by XBOOLE_1:40
.= f.:(A \/ {x}) \ Im(f,x) by RELAT_1:120
.= g.:B \ {f.x} by A6,Th5
.= g.:B1 by Th3;
x in A \/ {x} by ZFMISC_1:136;
then consider x9 being Element of X such that
A19: x9 in B and
A20: g.x9 = f.x by A6,FUNCT_2:35,65;
x9 in g"{f.x} by A20,Th4;
then
A21: B2 <> {} by A19,XBOOLE_0:def 4;
thus F$$(A \/ {.x.},f) = F.(F$$(A,f), f.x) by A1,A2,A3,A13,Th17
.= F.(F$$(B1,g), f.x) by A5,A13,A18
.= F.(F$$(B1,g), F$$(B2,g)) by A1,A2,A3,A21,A17,Th21
.= F$$(B,g) by A1,A2,A3,A16,A14,A21,Th18;
end;
end;
end;
A22: X[{}.X];
A23: for A being Element of Fin X holds X[A] from FinSubInd3(A22,A4);
let A,B be Element of Fin X;
assume A <> {} & f.:A = g.:B;
hence thesis by A23;
end;
theorem
for F,G being BinOp of Y st F is idempotent & F is commutative & F is
associative & G is_distributive_wrt F for B being Element of Fin X st B <> {}
for f being Function of X,Y for a being Element of Y holds G.(a,F$$(B,f)) = F$$
(B,G[;](a,f))
proof
let F,G be BinOp of Y such that
A1: F is idempotent and
A2: F is commutative & F is associative and
A3: G is_distributive_wrt F;
let B be Element of Fin X such that
A4: B<> {};
let f be Function of X,Y;
let a be Element of Y;
defpred X[Element of Fin X] means G.(a,F$$($1,f)) = F$$($1,G[;](a,f));
A5: for B1,B2 being non empty Element of Fin X holds X[B1] & X[B2] implies X
[B1 \/ B2]
proof
let B1,B2 be non empty Element of Fin X;
assume
A6: G.(a,F$$(B1,f)) = F$$(B1,G[;](a,f)) & G.(a,F$$(B2,f)) = F$$(B2,G [;](a,f));
thus G.(a,F$$(B1 \/ B2,f)) = G.(a,F.(F$$(B1,f),F$$(B2,f))) by A1,A2,Th18
.= F.(F$$(B1,G[;](a,f)), F$$(B2,G[;] (a,f))) by A3,A6,BINOP_1:11
.= F$$(B1 \/ B2,G[;](a,f)) by A1,A2,Th18;
end;
A7: for x being Element of X holds X[{.x.}]
proof
let x be Element of X;
thus G.(a,F$$({.x.},f)) = G.(a,f.x) by A2,Th14
.= (G[;](a,f)).x by FUNCOP_1:53
.= F$$({.x.},G[;](a,f)) by A2,Th14;
end;
for B being non empty Element of Fin X holds X[B] from FinSubInd2(A7,
A5);
hence thesis by A4;
end;
theorem
for F,G being BinOp of Y st F is idempotent & F is commutative & F is
associative & G is_distributive_wrt F for B being Element of Fin X st B <> {}
for f being Function of X,Y for a being Element of Y holds G.(F$$(B,f),a) = F$$
(B,G[:](f,a))
proof
let F,G be BinOp of Y such that
A1: F is idempotent and
A2: F is commutative & F is associative and
A3: G is_distributive_wrt F;
let B be Element of Fin X such that
A4: B<> {};
let f be Function of X,Y;
let a be Element of Y;
defpred X[Element of Fin X] means G.(F$$($1,f),a) = F$$($1,G[:](f,a));
A5: for B1,B2 being non empty Element of Fin X holds X[B1] & X[B2] implies X
[B1 \/ B2]
proof
let B1,B2 be non empty Element of Fin X;
assume
A6: G.(F$$(B1,f),a) = F$$(B1,G[:](f,a)) & G.(F$$(B2,f),a) = F$$(B2,G [:](f,a));
thus G.(F$$(B1 \/ B2,f),a) = G.(F.(F$$(B1,f),F$$(B2,f)),a) by A1,A2,Th18
.= F.(F$$(B1,G[:](f,a)), F$$(B2,G[:] (f,a))) by A3,A6,BINOP_1:11
.= F$$(B1 \/ B2,G[:](f,a)) by A1,A2,Th18;
end;
A7: for x being Element of X holds X[{.x.}]
proof
let x be Element of X;
thus G.(F$$({.x.},f),a) = G.(f.x,a) by A2,Th14
.= (G[:](f,a)).x by FUNCOP_1:48
.= F$$({.x.},G[:](f,a)) by A2,Th14;
end;
for B being non empty Element of Fin X holds X[B] from FinSubInd2(A7,
A5);
hence thesis by A4;
end;
definition
let X, Y be non empty set;
let f be Function of X,Y;
let A be Element of Fin X;
redefine func f.:A -> Element of Fin Y; :: redefines .: (FUNCT_1, redefinition) → .: (RELAT_1, definition)
coherence by Lm1;
end;
theorem Th26:
for A, X, Y being non empty set for F being BinOp of A st F is
idempotent & F is commutative & F is associative for B being Element of Fin X
st B <> {} for f being Function of X,Y holds for g being Function of Y,A holds
F$$(f.:B,g) = F$$(B,g*f)
proof
let A, X, Y be non empty set, F be BinOp of A such that
A1: F is idempotent and
A2: F is commutative & F is associative;
let B be Element of Fin X such that
A3: B <> {};
let f be Function of X,Y;
let g be Function of Y,A;
defpred X[Element of Fin X] means F$$(f.:$1,g) = F$$($1,g*f);
A4: dom f = X by FUNCT_2:def 1;
A5: for B1,B2 being non empty Element of Fin X holds X[B1] & X[B2] implies X
[B1 \/ B2]
proof
let B1,B2 be non empty Element of Fin X;
assume
A6: F$$(f.:B1,g) = F$$(B1,g*f) & F$$(f.:B2,g) = F$$(B2,g*f);
A7: B1 c= X by FINSUB_1:def 5;
A8: B2 c= X by FINSUB_1:def 5;
thus F$$(f.:(B1 \/ B2),g) = F$$(f.:B1 \/ f.:B2, g) by RELAT_1:120
.= F.(F$$(f.:B1,g), F$$(f.:B2,g)) by A1,A2,A7,A8,Th18,A4
.= F$$(B1 \/ B2,g*f) by A1,A2,A6,Th18;
end;
A9: for x being Element of X holds X[{.x.}]
proof
let x be Element of X;
f.:{.x.} = Im(f,x);
hence F$$(f.:{.x.},g) = F$$({.f.x.},g) by A4,FUNCT_1:59
.= g.(f.x) by A2,Th14
.= (g*f).x by FUNCT_2:15
.= F$$({.x.},g*f) by A2,Th14;
end;
for B being non empty Element of Fin X holds X[B] from FinSubInd2(A9,
A5);
hence thesis by A3;
end;
theorem Th27:
F is commutative & F is associative & F is idempotent implies
for Z being non empty set for G being BinOp of Z st G is commutative & G is
associative & G is idempotent for f being Function of X, Y for g being Function
of Y,Z st for x,y being Element of Y holds g.(F.(x,y)) = G.(g.x,g.y) for B
being Element of Fin X st B <> {} holds g.(F$$(B,f)) = G$$(B,g*f)
proof
assume that
A1: F is commutative & F is associative and
A2: F is idempotent;
let Z be non empty set, G be BinOp of Z such that
A3: G is commutative & G is associative and
A4: G is idempotent;
let f be Function of X,Y;
let g be Function of Y,Z such that
A5: for x,y being Element of Y holds g.(F.(x, y)) = G.(g.x, g.y);
defpred X[Element of Fin X] means $1 <> {} implies g.(F$$($1,f)) = G$$($1,g*
f);
A6: for B9 being Element of Fin X, b being Element of X holds X[B9] implies
X[B9 \/ {.b.}]
proof
let B be (Element of Fin X), x be Element of X;
assume that
A7: B <> {} implies g.(F$$(B,f)) = G$$(B,g*f) and
B \/ {x} <> {};
per cases;
suppose
A8: B = {};
hence g.(F$$(B \/ {.x.},f)) = g.(f.x) by A1,Th14
.= (g*f).x by FUNCT_2:15
.= G$$(B \/ {.x.},g*f) by A3,A8,Th14;
end;
suppose
A9: B <> {};
hence g.(F$$(B \/ {.x.},f)) = g.(F.(F$$(B,f), f.x)) by A1,A2,Th17
.= G.(g.(F$$(B,f)), g.(f.x)) by A5
.= G.(G$$(B,g*f), (g*f).x) by A7,A9,FUNCT_2:15
.= G$$(B \/ {.x.},g*f) by A3,A4,A9,Th17;
end;
end;
A10: X[{}.X];
thus for B being Element of Fin X holds X[B] from FinSubInd3(A10,A6 );
end;
:: If F has a unity
theorem Th28:
F is commutative & F is associative & F is having_a_unity
implies for f holds F$$({}.X,f) = the_unity_wrt F
proof
assume
A1: F is commutative & F is associative & F is having_a_unity;
let f;
the_unity_wrt F is_a_unity_wrt F & ex G being Function of Fin X, Y st F
$$ ( {}.X,f) = G.{}.X & (for e being Element of Y st e is_a_unity_wrt F holds G
.{} = e) & (for x being Element of X holds G.{x} = f.x) & for B9 being Element
of Fin X st B9 c= {}.X & B9 <> {} for x being Element of X st x in {}.X \ B9
holds G.( B9 \/ {x}) = F.(G.B9,f.x) by A1,Def3,Th11;
hence thesis;
end;
theorem Th29:
F is idempotent & F is commutative & F is associative & F is
having_a_unity implies for x being Element of X holds F $$(B \/ {.x.}, f) = F.(
F $$(B,f),f.x)
proof
assume that
A1: F is idempotent and
A2: F is commutative & F is associative;
assume
A3: F is having_a_unity;
let x be Element of X;
A4: {} = {}.X;
now
assume
A5: B = {};
hence F $$(B \/ {.x.}, f) = f.x by A2,Th14
.= F.(the_unity_wrt F, f.x) by A3,Th12
.= F.(F $$(B,f),f.x) by A2,A3,A4,A5,Th28;
end;
hence thesis by A1,A2,Th17;
end;
theorem
F is idempotent & F is commutative & F is associative & F is
having_a_unity implies for B1,B2 being Element of Fin X holds F $$ (B1 \/ B2,f)
= F.(F $$ (B1,f),F $$ (B2,f))
proof
assume that
A1: F is idempotent and
A2: F is commutative & F is associative and
A3: F is having_a_unity;
let B1,B2 be Element of Fin X;
now
A4: {} = {}.X;
assume
A5: B1 = {} or B2 = {};
per cases by A5;
suppose
A6: B2 = {};
hence F $$ (B1 \/ B2,f) = F.(F$$(B1,f),the_unity_wrt F) by A3,Th12
.= F.(F $$ (B1,f),F $$ (B2,f)) by A2,A3,A4,A6,Th28;
end;
suppose
A7: B1 = {};
hence F $$ (B1 \/ B2,f) = F.(the_unity_wrt F, F$$(B2,f)) by A3,Th12
.= F.(F $$ (B1,f),F $$ (B2,f)) by A2,A3,A4,A7,Th28;
end;
end;
hence thesis by A1,A2,Th18;
end;
theorem
F is commutative & F is associative & F is idempotent & F is
having_a_unity implies for f,g being Function of X,Y for A,B being Element of
Fin X st f.:A = g.:B holds F$$(A,f) = F$$(B,g)
proof
assume that
A1: F is commutative & F is associative and
A2: F is idempotent and
A3: F is having_a_unity;
let f,g be Function of X,Y;
let A,B be Element of Fin X such that
A4: f.:A = g.:B;
now
assume
A5: A = {};
then A = {}.X;
then
A6: F$$(A,f) = the_unity_wrt F by A1,A3,Th28;
f.:A = {} by A5;
then B = {}.X by A4,Th10;
hence thesis by A1,A3,A6,Th28;
end;
hence thesis by A1,A2,A4,Th23;
end;
theorem Th32:
for A, X, Y being non empty set for F being BinOp of A st F is
idempotent & F is commutative & F is associative & F is having_a_unity for B
being Element of Fin X for f being Function of X,Y holds for g being Function
of Y,A holds F$$(f.:B,g) = F$$(B,g*f)
proof
let A, X, Y be non empty set, F be BinOp of A such that
A1: F is idempotent and
A2: F is commutative & F is associative and
A3: F is having_a_unity;
let B be Element of Fin X;
let f be Function of X,Y;
let g be Function of Y,A;
now
assume
A4: B = {};
then f.:B = {}.Y;
then
A5: F$$(f.:B,g) = the_unity_wrt F by A2,A3,Th28;
B = {}.X by A4;
hence thesis by A2,A3,A5,Th28;
end;
hence thesis by A1,A2,Th26;
end;
theorem
F is commutative & F is associative & F is idempotent & F is
having_a_unity implies for Z being non empty set for G being BinOp of Z st G is
commutative & G is associative & G is idempotent & G is having_a_unity for f
being Function of X, Y for g being Function of Y,Z st g.the_unity_wrt F =
the_unity_wrt G & for x,y being Element of Y holds g.(F.(x,y)) = G.(g.x,g.y)
for B being Element of Fin X holds g.(F$$(B,f)) = G$$(B,g*f)
proof
assume that
A1: F is commutative & F is associative and
A2: F is idempotent and
A3: F is having_a_unity;
let Z be non empty set;
let G be BinOp of Z such that
A4: G is commutative & G is associative and
A5: G is idempotent and
A6: G is having_a_unity;
let f be Function of X, Y;
let g be Function of Y,Z such that
A7: g.the_unity_wrt F = the_unity_wrt G and
A8: for x,y being Element of Y holds g.(F.(x,y)) = G.(g.x,g.y);
let B be Element of Fin X;
per cases;
suppose
B = {};
then
A9: B = {}.X;
hence g.(F$$(B,f)) = g.the_unity_wrt F by A1,A3,Th28
.= G$$(B,g*f) by A4,A6,A7,A9,Th28;
end;
suppose
B <> {};
hence thesis by A1,A2,A4,A5,A8,Th27;
end;
end;
definition
let A be set;
func FinUnion A -> BinOp of Fin A means
:Def4:
for x,y being Element of Fin A holds it.(x,y) = (x \/ y);
existence
proof
deffunc U(Element of Fin A,Element of Fin A) = $1 \/ $2;
ex IT being BinOp of Fin A st for x,y being Element of Fin A holds IT.
(x,y) = U(x,y) from BINOP_1:sch 4;
hence thesis;
end;
uniqueness
proof
let IT, IT9 be BinOp of Fin A such that
A1: for x,y being Element of Fin A holds IT.(x,y) = (x \/ y) and
A2: for x,y being Element of Fin A holds IT9.(x,y) = (x \/ y);
now
let x,y be Element of Fin A;
thus IT.(x,y) = (x \/ y) by A1
.= IT9.(x,y) by A2;
end;
hence IT = IT9;
end;
end;
reserve A for set,
x,y,z for Element of Fin A;
theorem Th34:
FinUnion A is idempotent
proof
let x;
thus FinUnion A.(x,x) = x \/ x by Def4
.= x;
end;
theorem Th35:
FinUnion A is commutative
proof
let x,y;
thus FinUnion A.(x,y) = y \/ x by Def4
.= FinUnion A.(y,x) by Def4;
end;
theorem Th36:
FinUnion A is associative
proof
let x,y,z;
thus FinUnion A.(FinUnion A.(x,y), z) = FinUnion A.(x \/ y, z) by Def4
.= x \/ y \/ z by Def4
.= x \/ (y \/ z) by XBOOLE_1:4
.= FinUnion A.(x, y \/ z) by Def4
.= FinUnion A.(x, FinUnion A.(y,z)) by Def4;
end;
theorem Th37:
{}.A is_a_unity_wrt FinUnion A
proof
thus for x holds FinUnion A.({}.A, x) =x
proof
let x;
thus FinUnion A.({}.A, x) = {} \/ x by Def4
.= x;
end;
let x;
thus FinUnion A.(x, {}.A) = x \/ {} by Def4
.= x;
end;
theorem Th38:
FinUnion A is having_a_unity
proof
{}.A is_a_unity_wrt FinUnion A by Th37;
hence thesis;
end;
theorem
the_unity_wrt FinUnion A is_a_unity_wrt FinUnion A
by Th11,Th38;
theorem Th40:
the_unity_wrt FinUnion A = {}
proof
{}.A is_a_unity_wrt FinUnion A by Th37;
hence thesis by BINOP_1:def 8;
end;
reserve X,Y for non empty set,
A for set,
f for (Function of X, Fin A),
i,j,k for (Element of X);
definition
let X be non empty set, A be set;
let B be Element of Fin X;
let f be Function of X, Fin A;
func FinUnion(B,f) -> Element of Fin A equals
FinUnion A $$(B,f);
coherence;
end;
theorem
FinUnion({.i.},f) = f.i
proof
FinUnion A is commutative by Th35;
hence thesis by Th14,Th36;
end;
theorem
FinUnion({.i,j.},f) = f.i \/ f.j
proof
FinUnion A is idempotent & FinUnion A is commutative by Th34,Th35;
hence FinUnion({.i,j.},f) = FinUnion A.(f.i, f.j) by Th15,Th36
.= f.i \/ f.j by Def4;
end;
theorem
FinUnion({.i,j,k.},f) = f.i \/ f.j \/ f.k
proof
FinUnion A is idempotent & FinUnion A is commutative by Th34,Th35;
hence FinUnion({.i,j,k.},f) = FinUnion A.(FinUnion A.(f.i, f.j), f.k) by Th16
,Th36
.= FinUnion A.(f.i \/ f.j, f.k) by Def4
.= f.i \/ f.j \/ f.k by Def4;
end;
theorem Th44:
FinUnion({}.X,f) = {}
proof
FinUnion A is commutative & FinUnion A is associative by Th35,Th36;
hence FinUnion({}.X,f) = the_unity_wrt FinUnion A by Th28,Th38
.= {} by Th40;
end;
theorem Th45:
for B being Element of Fin X holds FinUnion(B \/ {.i.}, f) =
FinUnion(B,f) \/ f.i
proof
let B be Element of Fin X;
A1: FinUnion A is associative by Th36;
FinUnion A is idempotent & FinUnion A is commutative by Th34,Th35;
hence FinUnion(B \/ {.i.}, f) = FinUnion A.(FinUnion(B,f), f.i) by A1,Th29
,Th38
.= FinUnion(B,f) \/ f.i by Def4;
end;
theorem Th46:
for B being Element of Fin X holds FinUnion(B,f) = union (f.:B)
proof
defpred X[Element of Fin X] means FinUnion($1,f) = union (f.:$1);
A1: for B being (Element of Fin X), i st X[B] holds X[B \/ {.i.}]
proof
let B be (Element of Fin X), i;
assume FinUnion(B,f) = union (f.:B);
hence FinUnion(B \/ {.i.}, f) = union (f.:B) \/ union {f.i} by Th45
.= union (f.:B \/ {f.i}) by ZFMISC_1:78
.= union (f.:B \/ Im(f,i)) by Th5
.= union (f.:(B \/ {i})) by RELAT_1:120;
end;
FinUnion({}.X,f) = union (f.:{}.X) by Th44,ZFMISC_1:2;
then
A2: X[{}.X];
thus for B being Element of Fin X holds X[B] from FinSubInd3(A2,A1 );
end;
theorem
for B1,B2 being Element of Fin X holds FinUnion(B1 \/ B2, f) =
FinUnion(B1,f) \/ FinUnion(B2,f)
proof
let B1,B2 be Element of Fin X;
thus FinUnion(B1 \/ B2, f) = union(f.:(B1 \/ B2)) by Th46
.= union(f.:B1 \/ f .:B2) by RELAT_1:120
.= union(f.:B1) \/ union(f.:B2) by ZFMISC_1:78
.= FinUnion(B1,f) \/ union(f.:B2) by Th46
.= FinUnion(B1,f) \/ FinUnion(B2,f) by Th46;
end;
theorem
for B being Element of Fin X for f being Function of X,Y holds for g
being Function of Y,Fin A holds FinUnion(f.:B,g) = FinUnion(B,g*f)
proof
let B be Element of Fin X;
let f be Function of X,Y;
let g be Function of Y,Fin A;
thus FinUnion(f.:B,g) = union (g.:(f.:B)) by Th46
.= union ((g*f).:B) by RELAT_1:126
.= FinUnion(B,g*f) by Th46;
end;
theorem Th49:
for A,X being non empty set, Y being set for G being BinOp of A
st G is commutative & G is associative & G is idempotent for B being Element of
Fin X st B <> {} for f being (Function of X,Fin Y), g being Function of Fin Y,A
st for x,y being Element of Fin Y holds g.(x \/ y) = G.(g.x,g.y) holds g.(
FinUnion(B,f)) = G$$(B,g*f)
proof
let A,X be non empty set, Y be set, G be BinOp of A such that
A1: G is commutative & G is associative & G is idempotent;
let B be Element of Fin X such that
A2: B <> {};
let f be (Function of X,Fin Y), g be Function of Fin Y,A such that
A3: for x,y being Element of Fin Y holds g.(x \/ y) = G.(g.x,g.y);
A4: now
let x,y be Element of Fin Y;
thus g.(FinUnion Y.(x,y)) = g.(x \/ y) by Def4
.= G.(g.x,g.y) by A3;
end;
A5: FinUnion Y is idempotent by Th34;
FinUnion Y is commutative & FinUnion Y is associative by Th35,Th36;
hence thesis by A1,A5,A2,A4,Th27;
end;
theorem Th50:
for Z being non empty set, Y being set for G being BinOp of Z st
G is commutative & G is associative & G is idempotent & G is having_a_unity for
f being Function of X, Fin Y for g being Function of Fin Y,Z st g.{}.Y =
the_unity_wrt G & for x,y being Element of Fin Y holds g.(x \/ y) = G.(g.x,g.y)
for B being Element of Fin X holds g.(FinUnion(B,f)) = G$$(B,g*f)
proof
let Z be non empty set, Y be set;
let G be BinOp of Z such that
A1: G is commutative & G is associative and
A2: G is idempotent and
A3: G is having_a_unity;
let f be Function of X, Fin Y;
let g be Function of Fin Y,Z such that
A4: g.{}.Y = the_unity_wrt G and
A5: for x,y being Element of Fin Y holds g.(x \/ y) = G.(g.x,g.y);
let B be Element of Fin X;
A6: {} = {}.X;
A7: {} = {}.Fin Y;
per cases;
suppose
A8: B = {};
then
A9: f.:B = {};
thus g.(FinUnion(B,f)) = g.{}.Y by A6,A8,Th44
.= G$$(f.:B,g) by A1,A3,A4,A7,A9,Th28
.= G$$(B,g*f) by A1,A2,A3,Th32;
end;
suppose
B <> {};
hence thesis by A1,A2,A5,Th49;
end;
end;
definition
let A be set;
func singleton A -> Function of A, Fin A means
:Def6:
for x being object st x in A holds it.x = {x};
existence
proof
deffunc U(object) = {$1};
A1: now
let x be object;
assume
A2: x in A;
then reconsider A9 = A as non empty set;
reconsider x9 = x as Element of A9 by A2;
{.x9.} in Fin A9;
hence U(x) in Fin A;
end;
thus ex f being Function of A, Fin A st
for x being object st x in A holds f.
x = U(x) from FUNCT_2:sch 2(A1);
end;
uniqueness
proof
let IT,IT9 be Function of A, Fin A such that
A3: for x being object st x in A holds IT.x = {x} and
A4: for x being object st x in A holds IT9.x = {x};
now
let x be object;
assume
A5: x in A;
then IT.x = {x} by A3;
hence IT.x = IT9.x by A4,A5;
end;
hence thesis by FUNCT_2:12;
end;
end;
theorem Th51:
for A being non empty set for f being Function of A, Fin A holds
f = singleton A iff for x being Element of A holds f.x = {x}
proof
let A be non empty set;
let f be Function of A, Fin A;
thus f = singleton A implies for x being Element of A holds f.x = {x} by Def6
;
assume for x being Element of A holds f.x = {x};
then for x be object holds x in A implies f.x = {x};
hence thesis by Def6;
end;
theorem Th52:
for x being set, y being Element of X holds x in singleton X.y iff x = y
proof
let x be set, y be Element of X;
singleton X.y = {y} by Th51;
hence thesis by TARSKI:def 1;
end;
theorem
for x,y,z being Element of X st x in singleton X.z & y in singleton X.
z holds x = y
proof
let x,y,z be Element of X;
assume that
A1: x in singleton X.z and
A2: y in singleton X.z;
x = z by A1,Th52;
hence thesis by A2,Th52;
end;
Lm2: for D being non empty set, X, P being set for f being Function of X,D
holds f.:P c= D;
theorem Th54:
for B being Element of Fin X, x being set holds x in FinUnion(B,
f) iff ex i being Element of X st i in B & x in f.i
proof
let B be Element of Fin X, x be set;
A1: now
assume x in union (f.:B);
then consider Z being set such that
A2: x in Z and
A3: Z in f .:B by TARSKI:def 4;
f.:B is Subset of Fin A by Lm2;
then reconsider Z as Element of Fin A by A3;
consider i being Element of X such that
A4: i in B & Z = f.i by A3,FUNCT_2:65;
take i9 = i;
thus i9 in B & x in f.i9 by A2,A4;
end;
now
given i being Element of X such that
A5: i in B and
A6: x in f.i;
f.i in f.:B by A5,FUNCT_2:35;
hence x in union (f.:B) by A6,TARSKI:def 4;
end;
hence thesis by A1,Th46;
end;
theorem
for B being Element of Fin X holds FinUnion(B, singleton X) = B
proof
let B be Element of Fin X;
now
let x be object;
thus x in FinUnion(B, singleton X) implies x in B
proof
assume x in FinUnion(B, singleton X);
then ex i being Element of X st i in B & x in singleton X.i by Th54;
hence thesis by Th52;
end;
assume
A1: x in B;
then reconsider x9 = x as Element of X by Th6;
x in singleton X.x9 by Th52;
hence x in FinUnion(B, singleton X) by A1,Th54;
end;
hence thesis by TARSKI:2;
end;
theorem
for Y,Z being set for f being Function of X, Fin Y for g being
Function of Fin Y, Fin Z st g.{}.Y = {}.Z & for x,y being Element of Fin Y
holds g.(x \/ y) = g.x \/ g.y for B being Element of Fin X holds g.(FinUnion(B,
f)) = FinUnion(B,g*f)
proof
let Y,Z be set;
let f be Function of X, Fin Y;
let g be Function of Fin Y, Fin Z;
assume that
A1: g.{}.Y = {}.Z and
A2: for x,y being Element of Fin Y holds g.(x \/ y) = g.x \/ g.y;
A3: g.{}.Y = the_unity_wrt FinUnion Z by A1,Th40;
A4: now
let x,y be Element of Fin Y;
thus g.(x \/ y) = g.x \/ g.y by A2
.= FinUnion Z.(g.x,g.y) by Def4;
end;
let B be Element of Fin X;
A5: FinUnion Z is idempotent by Th34;
FinUnion Z is associative & FinUnion Z is commutative by Th35,Th36;
hence thesis by A5,A3,A4,Th38,Th50;
end;