:: Algebra of Normal Forms
:: by Andrzej Trybulec
::
:: Received October 5, 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 XBOOLE_0, FINSUB_1, SUBSET_1, ZFMISC_1, TARSKI, MCART_1, BINOP_1,
FUNCT_1, SETWISEO, RELAT_1, FINSET_1, ORDINAL4, STRUCT_0, LATTICES,
EQREL_1, NORMFORM;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XTUPLE_0, MCART_1, RELAT_1,
FUNCT_2, FINSET_1, BINOP_1, DOMAIN_1, FINSUB_1, SETWISEO, STRUCT_0,
LATTICES;
constructors PARTFUN1, BINOP_1, DOMAIN_1, FINSET_1, SETWISEO, LATTICES,
RELSET_1, XTUPLE_0;
registrations SUBSET_1, FINSUB_1, LATTICES, RELAT_1, XTUPLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI, BINOP_1, LATTICES, XBOOLE_0;
equalities LATTICES, XBOOLE_0;
expansions TARSKI, BINOP_1, XBOOLE_0;
theorems BINOP_1, FINSUB_1, DOMAIN_1, MCART_1, ZFMISC_1, SETWISEO, LATTICE2,
TARSKI, FINSET_1, LATTICES, XBOOLE_0, XBOOLE_1, RELAT_1;
schemes BINOP_1, SETWISEO, FRAENKEL;
begin
:: A u x i l i a r y t h e o r e m s
:: Part 1. BOOLEan operations on pairs & relations between pairs
reserve A, B for non empty preBoolean set,
x, y for Element of [:A,B:];
definition
let A,B,x,y;
pred x c= y means
x`1 c= y`1 & x`2 c= y`2;
reflexivity;
func x \/ y -> Element of [:A, B:] equals
[x`1 \/ y`1, x`2 \/ y`2];
correctness;
commutativity;
idempotence by MCART_1:21;
func x /\ y -> Element of [:A, B:] equals
[x`1 /\ y`1, x`2 /\ y`2];
correctness;
commutativity;
idempotence by MCART_1:21;
func x \ y -> Element of [:A, B:] equals
[x`1 \ y`1, x`2 \ y`2];
correctness;
func x \+\ y -> Element of [:A, B:] equals
[x`1 \+\ y`1, x`2 \+\ y`2];
correctness;
commutativity;
end;
reserve X for set,
a,b,c for Element of [:A,B:];
theorem Th1:
a c= b & b c= a implies a = b
proof
assume a`1 c= b`1 & a`2 c= b`2 & b`1 c= a`1 & b`2 c= a`2;
then a`1 = b`1 & a`2 = b`2;
hence thesis by DOMAIN_1:2;
end;
theorem Th2:
a c= b & b c= c implies a c= c
proof
assume a`1 c= b`1 & a`2 c= b`2 & b`1 c= c`1 & b`2 c= c`2;
hence a`1 c= c`1 & a`2 c= c`2;
end;
theorem Th3:
(a \/ b) \/ c = a \/ (b \/ c)
proof
A1: ((a \/ b) \/ c)`2 = (a \/ b)`2 \/ c`2
.= a`2 \/ b`2 \/ c`2
.= a`2 \/ (b`2 \/ c`2) by XBOOLE_1:4
.= a`2 \/ (b \/ c)`2
.= (a \/ (b \/ c))`2;
((a \/ b) \/ c)`1 = (a \/ b)`1 \/ c`1
.= a`1 \/ b`1 \/ c`1
.= a`1 \/ (b`1 \/ c`1) by XBOOLE_1:4
.= a`1 \/ (b \/ c)`1
.= (a \/ (b \/ c))`1;
hence thesis by A1,DOMAIN_1:2;
end;
theorem
(a /\ b) /\ c = a /\ (b /\ c)
proof
A1: ((a /\ b) /\ c)`2 = (a /\ b)`2 /\ c`2
.= a`2 /\ b`2 /\ c`2
.= a`2 /\ (b`2 /\ c`2) by XBOOLE_1:16
.= a`2 /\ (b /\ c)`2
.= (a /\ (b /\ c))`2;
((a /\ b) /\ c)`1 = (a /\ b)`1 /\ c`1
.= a`1 /\ b`1 /\ c`1
.= a`1 /\ (b`1 /\ c`1) by XBOOLE_1:16
.= a`1 /\ (b /\ c)`1
.= (a /\ (b /\ c))`1;
hence thesis by A1,DOMAIN_1:2;
end;
theorem Th5:
a /\ (b \/ c) = a /\ b \/ a /\ c
proof
A1: (a /\ (b \/ c))`2 = a`2 /\ (b \/ c)`2
.= a`2 /\ (b`2 \/ c`2)
.= a`2 /\ b`2 \/ a`2 /\ c`2 by XBOOLE_1:23
.= a`2 /\ b`2 \/ (a /\ c)`2
.= (a /\ b)`2 \/ (a /\ c)`2
.= (a /\ b \/ a /\ c)`2;
(a /\ (b \/ c))`1 = a`1 /\ (b \/ c)`1
.= a`1 /\ (b`1 \/ c`1)
.= a`1 /\ b`1 \/ a`1 /\ c`1 by XBOOLE_1:23
.= a`1 /\ b`1 \/ (a /\ c)`1
.= (a /\ b)`1 \/ (a /\ c)`1
.= (a /\ b \/ a /\ c)`1;
hence thesis by A1,DOMAIN_1:2;
end;
theorem Th6:
a \/ (b /\ a) = a
proof
A1: (a \/ (b /\ a))`2 = a`2 \/ (b /\ a)`2
.= a`2 \/ b`2 /\ a`2
.= a`2 by XBOOLE_1:22;
(a \/ (b /\ a))`1 = a`1 \/ (b /\ a)`1
.= a`1 \/ b`1 /\ a`1
.= a`1 by XBOOLE_1:22;
hence thesis by A1,DOMAIN_1:2;
end;
theorem Th7:
a /\ (b \/ a) = a
proof
thus a /\ (b \/ a) = a /\ b \/ a /\ a by Th5
.= a by Th6;
end;
theorem
a \/ (b /\ c) = (a \/ b) /\ (a \/ c)
proof
thus a \/ (b /\ c) = a \/ c /\ a \/ c /\ b by Th6
.= a \/ (c /\ a \/ c /\ b) by Th3
.= a \/ c /\ (a \/ b) by Th5
.= (a \/ b) /\ a \/ (a \/ b) /\ c by Th7
.= (a \/ b) /\ (a \/ c) by Th5;
end;
theorem Th9:
a c= c & b c= c implies a \/ b c= c
by XBOOLE_1:8;
theorem Th10:
a c= a \/ b & b c= a \/ b
by XBOOLE_1:7;
theorem
a = a \/ b implies b c= a by Th10;
theorem Th12:
a c= b implies c \/ a c= c \/ b & a \/ c c= b \/ c
by XBOOLE_1:9;
theorem
a\b \/ b = a \/ b
proof
a`1 \ b`1 \/ b`1 = a`1 \/ b`1 & a`2 \ b`2 \/ b`2 = a`2 \/ b`2 by XBOOLE_1:39;
hence thesis;
end;
theorem
a \ b c= c implies a c= b \/ c
by XBOOLE_1:44;
theorem
a c= b \/ c implies a \ c c= b
by XBOOLE_1:43;
reserve a for Element of [:Fin X, Fin X:];
definition
let A be set;
func FinPairUnion A -> BinOp of [:Fin A, Fin A:] means
:Def6:
for x,y being Element of [:Fin A, Fin A:] holds it.(x,y) = x \/ y;
existence
proof
deffunc O(Element of [:Fin A, Fin A:],Element of [:Fin A, Fin A:]) = $1 \/
$2;
ex IT being BinOp of [:Fin A, Fin A:] st for x,y being Element of [:
Fin A, Fin A:] holds IT.(x,y) = O(x,y) from BINOP_1:sch 4;
hence thesis;
end;
uniqueness
proof
let IT, IT9 be BinOp of [:Fin A, Fin A:] such that
A1: for x,y being Element of [:Fin A, Fin A:] holds IT.(x,y) = x \/ y and
A2: for x,y being Element of [:Fin A, Fin A:] holds IT9.(x,y) = x \/ y;
now
let x,y be Element of [:Fin A, 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;
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, Fin A:];
func FinPairUnion(B,f) -> Element of [:Fin A, Fin A:] equals
FinPairUnion A $$(B,f);
correctness;
end;
Lm1: FinPairUnion A is idempotent
proof
let a be Element of [:Fin A, Fin A:];
thus FinPairUnion A.(a, a) = a \/ a by Def6
.= a;
end;
Lm2: FinPairUnion A is commutative
proof
let a,b be Element of [:Fin A, Fin A:];
thus FinPairUnion A.(a,b) = b \/ a by Def6
.= FinPairUnion A.(b,a) by Def6;
end;
Lm3: FinPairUnion A is associative
proof
let a,b,c be Element of [:Fin A, Fin A:];
thus FinPairUnion A.(a, FinPairUnion A.(b,c)) = a \/ FinPairUnion A.(b,c) by
Def6
.= a \/ (b \/ c) by Def6
.= a \/ b \/ c by Th3
.= FinPairUnion A.(a,b) \/ c by Def6
.= FinPairUnion A.(FinPairUnion A.(a,b), c) by Def6;
end;
registration
let A be set;
cluster FinPairUnion A -> commutative idempotent associative;
coherence by Lm1,Lm2,Lm3;
end;
theorem
for X being non empty set for f being Function of X, [:Fin A,Fin A:]
for B being Element of Fin X for x being Element of X st x in B holds f.x c=
FinPairUnion(B,f)
proof
let X be non empty set, f be Function of X, [:Fin A,Fin A:];
let B be (Element of Fin X), x be Element of X;
assume
A1: x in B;
then FinPairUnion A $$(B, f) = FinPairUnion A $$(B \/ {.x.}, f) by
ZFMISC_1:40
.= FinPairUnion A.(FinPairUnion A $$(B,f),f.x) by A1,SETWISEO:20
.= FinPairUnion A $$(B,f) \/ f.x by Def6;
hence thesis by Th10;
end;
theorem Th17:
[{}.A, {}.A] is_a_unity_wrt FinPairUnion A
proof
now
let x be Element of [:Fin A, Fin A:];
thus FinPairUnion A.([{}.A, {}.A], x) = [{}.A, {}.A] \/ x by Def6
.= x by MCART_1:21;
end;
hence thesis by BINOP_1:4;
end;
theorem Th18:
FinPairUnion A is having_a_unity
proof
[{}.A, {}.A] is_a_unity_wrt FinPairUnion A by Th17;
hence thesis by SETWISEO:def 2;
end;
theorem Th19:
the_unity_wrt FinPairUnion A = [{}.A, {}.A]
proof
[{}.A, {}.A] is_a_unity_wrt FinPairUnion A by Th17;
hence thesis by BINOP_1:def 8;
end;
theorem Th20:
for x being Element of [:Fin A, Fin A:] holds the_unity_wrt
FinPairUnion A c= x
proof
let x be Element of [:Fin A, Fin A:];
[{}.A, {}.A] is_a_unity_wrt FinPairUnion A by Th17;
then the_unity_wrt FinPairUnion A = [{}, {}] by BINOP_1:def 8;
then
(the_unity_wrt FinPairUnion A)`1 = {} & (the_unity_wrt FinPairUnion A)`2
= {};
hence
(the_unity_wrt FinPairUnion A)`1 c= x`1 & (the_unity_wrt FinPairUnion A
)`2 c= x`2;
end;
theorem
for X being non empty set for f being (Function of X,[:Fin A,Fin A:]),
B being (Element of Fin X) for c being Element of [:Fin A, Fin A:] st for x
being Element of X st x in B holds f.x c= c holds FinPairUnion(B,f) c= c
proof
let X be non empty set, f be Function of X,[:Fin A,Fin A:];
let B be (Element of Fin X), c be Element of [:Fin A, Fin A:];
defpred P[Element of Fin X] means $1 c= B implies FinPairUnion A $$($1,f) c=
c;
assume
A1: for x being Element of X st x in B holds f.x c= c;
A2: now
let C be (Element of Fin X), b be Element of X;
assume
A3: P[C];
now
assume
A4: C \/ {b} c= B;
then {b} c= B by XBOOLE_1:11;
then b in B by ZFMISC_1:31;
then
A5: f.b c= c by A1;
FinPairUnion A $$(C \/ {.b.},f) = FinPairUnion A.(FinPairUnion A $$
(C,f),f.b) by Th18,SETWISEO:32
.= FinPairUnion A $$(C,f) \/ f.b by Def6;
hence FinPairUnion A $$(C \/ {.b.},f) c= c by A3,A4,A5,Th9,XBOOLE_1:11;
end;
hence P[C \/ {.b.}];
end;
A6: P[{}.X]
proof
assume {}.X c= B;
FinPairUnion A $$({}.X,f) = the_unity_wrt FinPairUnion A by Th18,
SETWISEO:31;
hence thesis by Th20;
end;
for C being Element of Fin X holds P[C] from SETWISEO:sch 4(A6,A2);
hence thesis;
end;
theorem
for X being non empty set, B being Element of Fin X for f,g being
Function of X,[:Fin A,Fin A:] st f|B = g|B holds FinPairUnion(B,f) =
FinPairUnion(B,g)
proof
let X be non empty set, B be Element of Fin X;
let f,g be Function of X,[:Fin A,Fin A:];
set J = FinPairUnion A;
A1: [{}.A, {}.A] = the_unity_wrt J by Th19;
assume
A2: f|B = g|B;
now
per cases;
suppose
A3: B = {};
hence FinPairUnion(B,f) = J$$({}.X,f)
.= [{}.A, {}.A] by A1,Th18,SETWISEO:31
.= J$$({}.X,g) by A1,Th18,SETWISEO:31
.= FinPairUnion(B,g) by A3;
end;
suppose
A4: B <> {};
f.:B = g.:B by A2,RELAT_1:166;
hence thesis by A4,SETWISEO:26;
end;
end;
hence thesis;
end;
:: Part 2. Disjoint pairs of finite sets
definition
let X;
func DISJOINT_PAIRS(X) -> Subset of [:Fin X, Fin X:] equals
{ a : a`1 misses
a`2 };
coherence
proof
set D = { a : a`1 misses a`2 };
D c= [:Fin X, Fin X:]
proof
let x be object;
assume x in D;
then ex a st x = a & a`1 misses a`2;
hence thesis;
end;
hence thesis;
end;
end;
registration
let X;
cluster DISJOINT_PAIRS(X) -> non empty;
coherence
proof
{} is Element of Fin X by FINSUB_1:7;
then reconsider b = [{},{}] as Element of [:Fin X, Fin X:] by
ZFMISC_1:def 2;
b`1 misses b`2;
then b in { a : a`1 misses a`2 };
hence thesis;
end;
end;
theorem Th23:
for y being Element of [:Fin X, Fin X:] holds y in
DISJOINT_PAIRS X iff y`1 misses y`2
proof
let y be Element of [:Fin X, Fin X:];
y in DISJOINT_PAIRS X iff ex a st y = a & a`1 misses a`2;
hence thesis;
end;
reserve x,y for Element of [:Fin X, Fin X:],
a,b for Element of DISJOINT_PAIRS X;
theorem
y in DISJOINT_PAIRS X & x in DISJOINT_PAIRS X implies (y \/ x in
DISJOINT_PAIRS X iff y`1 /\ x`2 \/ x`1 /\ y`2 = {})
proof
assume that
A1: y in DISJOINT_PAIRS X and
A2: x in DISJOINT_PAIRS X;
A3: (y`1 \/ x`1) /\ (y`2 \/ x`2) = (y`1 \/ x`1) /\ y`2 \/ (y`1 \/ x`1) /\ x
`2 & (y`1 \/ x`1) /\ y`2 = y`1 /\ y`2 \/ x`1 /\ y`2 by XBOOLE_1:23;
x`1 misses x`2 by A2,Th23;
then
A4: x`1 /\ x`2 = {};
y`1 misses y`2 by A1,Th23;
then
A5: y`1 /\ y`2 = {};
A6: (y`1 \/ x`1) /\ x`2 = y`1 /\ x`2 \/ x`1 /\ x`2 by XBOOLE_1:23;
A7: (y \/ x)`1 = y`1 \/ x`1 & (y \/ x)`2 = y`2 \/ x`2;
thus y \/ x in DISJOINT_PAIRS X implies y`1 /\ x`2 \/ x`1 /\y`2 = {}
by A5,A4,A7,A3,A6,XBOOLE_0:def 7,Th23;
assume y`1 /\ x`2 \/ x`1 /\ y`2 = {};
then (y \/ x)`1 misses (y \/ x)`2 by A5,A4,A3,A6;
hence thesis;
end;
theorem
a`1 misses a`2 by Th23;
theorem Th26:
x c= b implies x is Element of DISJOINT_PAIRS X
proof
assume
A1: x`1 c= b`1 & x`2 c= b`2;
b`1 misses b`2 by Th23;
then x`1 misses x`2 by A1,XBOOLE_1:64;
hence thesis by Th23;
end;
theorem Th27:
not (ex x being set st x in a`1 & x in a`2)
by Th23,XBOOLE_0:3;
theorem
not a \/ b in DISJOINT_PAIRS X implies ex p being Element of X st p in
a`1 & p in b`2 or p in b`1 & p in a`2
proof
set p = the Element of (a \/ b)`1 /\ (a \/ b)`2;
assume not a \/ b in DISJOINT_PAIRS X;
then (a \/ b)`1 meets (a \/ b)`2;
then
A1: (a \/ b)`1 /\ (a \/ b)`2 <> {};
(a \/ b)`1 /\ (a \/ b)`2 is Subset of X by FINSUB_1:16;
then reconsider p as Element of X by A1,TARSKI:def 3;
p in (a \/ b)`2 by A1,XBOOLE_0:def 4;
then p in a`2 \/ b`2;
then
A2: p in b`2 or p in a`2 by XBOOLE_0:def 3;
take p;
p in (a \/ b)`1 by A1,XBOOLE_0:def 4;
then p in a`1 \/ b`1;
then p in a`1 or p in b`1 by XBOOLE_0:def 3;
hence thesis by A2,Th27;
end;
theorem
x`1 misses x`2 implies x is Element of DISJOINT_PAIRS X by Th23;
theorem
for V,W being set st V c= a`1 & W c= a`2 holds [V,W] is Element of
DISJOINT_PAIRS X
proof
let V,W be set;
assume
A1: V c= a`1 & W c= a`2;
then V is Element of Fin X & W is Element of Fin X by SETWISEO:11;
then reconsider x = [V,W] as Element of [:Fin X, Fin X:] by ZFMISC_1:def 2;
a`1 misses a`2 & [V,W]`1 = V by Th23;
then x`1 misses x`2 by A1,XBOOLE_1:64;
hence thesis by Th23;
end;
reserve A for set,
x for Element of [:Fin A, Fin A:],
a,b,c,d,s,t for Element of DISJOINT_PAIRS A,
B,C,D for Element of Fin DISJOINT_PAIRS A;
Lm4: for A holds {} in { B : a in B & b in B & a c= b implies a = b}
proof
let A;
{} is Element of Fin DISJOINT_PAIRS A & for a,b holds a in {} & b in {}
& a c= b implies a = b by FINSUB_1:7;
hence thesis;
end;
definition
let A;
func Normal_forms_on A -> Subset of Fin DISJOINT_PAIRS A equals
{ B : a in B
& b in B & a c= b implies a = b};
coherence
proof
set IT = { B : a in B & b in B & a c= b implies a = b};
IT c= Fin DISJOINT_PAIRS A
proof
let x be object;
assume x in IT;
then
ex B st x = B & for a,b holds a in B & b in B & a c= b implies a = b;
hence thesis;
end;
hence thesis;
end;
end;
registration
let A;
cluster Normal_forms_on A -> non empty;
coherence by Lm4;
end;
reserve K,L,M for Element of Normal_forms_on A;
theorem
{} in Normal_forms_on A by Lm4;
theorem Th32:
B in Normal_forms_on A & a in B & b in B & a c= b implies a = b
proof
assume B in Normal_forms_on A;
then ex C st B = C & for a,b holds a in C & b in C & a c= b implies a = b;
hence thesis;
end;
theorem Th33:
(for a,b st a in B & b in B & a c= b holds a = b) implies B in
Normal_forms_on A;
definition
let A,B;
func mi B -> Element of Normal_forms_on A equals
{ t : s in B & s c= t iff s
= t };
coherence
proof
set M = { t : s in B & s c= t iff s = t };
now
let x be object;
assume x in M;
then ex t st x = t & for s holds s in B & s c= t iff s = t;
hence x in B;
end;
then
A1: M c= B;
then
A2: M is finite by FINSET_1:1;
B c= DISJOINT_PAIRS A by FINSUB_1:def 5;
then M c= DISJOINT_PAIRS A by A1;
then reconsider M9 = M as Element of Fin DISJOINT_PAIRS A by A2,
FINSUB_1:def 5;
now
let c,d be Element of DISJOINT_PAIRS A;
assume c in M;
then ex t st c = t & for s holds s in B & s c= t iff s = t;
then
A3: c in B;
assume d in M;
then ex t st d = t & for s holds s in B & s c= t iff s = t;
hence c c= d implies c = d by A3;
end;
then M9 is Element of Normal_forms_on A by Th33;
hence thesis;
end;
correctness;
let C;
func B^C -> Element of Fin DISJOINT_PAIRS A equals
DISJOINT_PAIRS A /\ { s
\/ t: s in B & t in C };
coherence
proof
deffunc F(Element of DISJOINT_PAIRS A,Element of DISJOINT_PAIRS A) = $1 \/
$2;
set M = DISJOINT_PAIRS A /\ { F(s,t): s in B & t in C };
A4: C is finite;
A5: B is finite;
{ F(s, t) : s in B & t in C } is finite from FRAENKEL:sch 22(A5, A4
);
then M c= DISJOINT_PAIRS A & M is finite by FINSET_1:1,XBOOLE_1:17;
hence thesis by FINSUB_1:def 5;
end;
correctness;
end;
theorem Th34:
x in B^C implies ex b,c st b in B & c in C & x = b \/ c
proof
assume x in B^C;
then x in { s \/ t: s in B & t in C } by XBOOLE_0:def 4;
then ex s,t st x = s \/ t & s in B & t in C;
hence thesis;
end;
theorem Th35:
b in B & c in C & b \/ c in DISJOINT_PAIRS A implies b \/ c in B ^C
proof
assume b in B & c in C;
then
A1: b \/ c in { s \/ t: s in B & t in C };
assume b \/ c in DISJOINT_PAIRS A;
hence thesis by A1,XBOOLE_0:def 4;
end;
theorem Th36:
a in mi B implies a in B & (b in B & b c= a implies b = a)
proof
assume a in mi B;
then ex t st a = t & for s holds s in B & s c= t iff s = t;
hence thesis;
end;
theorem
a in mi B implies a in B by Th36;
theorem
a in mi B & b in B & b c= a implies b = a by Th36;
theorem Th39:
a in B & (for b st b in B & b c= a holds b = a) implies a in mi B
proof
assume a in B & for s st s in B & s c= a holds s = a;
then s in B & s c= a iff s = a;
hence thesis;
end;
Lm5: (for a holds a in B implies a in C) implies B c= C
proof
assume
A1: for a holds a in B implies a in C;
let x be object;
assume
A2: x in B;
then x is Element of DISJOINT_PAIRS A by SETWISEO:9;
hence thesis by A1,A2;
end;
theorem Th40:
mi B c= B
proof
for a holds a in mi B implies a in B by Th36;
hence thesis by Lm5;
end;
theorem Th41:
b in B implies ex c st c c= b & c in mi B
proof
assume
A1: b in B;
defpred P[Element of DISJOINT_PAIRS A,Element of DISJOINT_PAIRS A] means $1
c= $2;
A2: for a holds P[a,a];
A3: for a,b,c st P[a,b] & P[b,c] holds P[a,c] by Th2;
for a st a in B ex b st b in B & P[b,a] & for c st c in B & P[c,b] holds
P[b,c] from FRAENKEL:sch 23(A2,A3);
then consider c such that
A4: c in B and
A5: c c= b and
A6: for a st a in B & a c= c holds c c= a by A1;
take c;
thus c c= b by A5;
now
let b;
assume that
A7: b in B and
A8: b c= c;
c c= b by A6,A7,A8;
hence b = c by A8,Th1;
end;
hence thesis by A4,Th39;
end;
theorem Th42:
mi K = K
proof
thus mi K c= K by Th40;
now
let a;
assume
A1: a in K;
then for b st b in K & b c= a holds b = a by Th32;
hence a in mi K by A1,Th39;
end;
hence thesis by Lm5;
end;
theorem Th43:
mi (B \/ C) c= mi B \/ C
proof
now
let a;
assume
A1: a in mi(B \/ C);
then
A2: a in B \/ C by Th36;
now
per cases by A2,XBOOLE_0:def 3;
suppose
A3: a in B;
now
let b;
assume b in B;
then b in B \/ C by XBOOLE_0:def 3;
hence b c= a implies b = a by A1,Th36;
end;
then a in mi B by A3,Th39;
hence a in mi B \/ C by XBOOLE_0:def 3;
end;
suppose
a in C;
hence a in mi B \/ C by XBOOLE_0:def 3;
end;
end;
hence a in mi B \/ C;
end;
hence thesis by Lm5;
end;
theorem Th44:
mi(mi B \/ C) = mi (B \/ C)
proof
A1: mi B \/ C c= B \/ C by Th40,XBOOLE_1:9;
now
let a;
assume
A2: a in mi(mi B \/ C);
A3: now
let b;
assume that
A4: b in B \/ C and
A5: b c= a;
now
per cases by A4,XBOOLE_0:def 3;
suppose
b in B;
then consider c such that
A6: c c= b and
A7: c in mi B by Th41;
c in mi B \/ C & c c= a by A5,A6,A7,Th2,XBOOLE_0:def 3;
then c = a by A2,Th36;
hence b = a by A5,A6,Th1;
end;
suppose
b in C;
then b in mi B \/ C by XBOOLE_0:def 3;
hence b = a by A2,A5,Th36;
end;
end;
hence b = a;
end;
a in mi B \/ C by A2,Th36;
hence a in mi (B \/ C) by A1,A3,Th39;
end;
hence mi(mi B \/ C) c= mi (B \/ C) by Lm5;
A8: mi(B \/ C) c= mi B \/ C by Th43;
now
let a;
assume
A9: a in mi (B \/ C);
then for b st b in mi B \/ C holds b c= a implies b = a by A1,Th36;
hence a in mi(mi B \/ C) by A8,A9,Th39;
end;
hence thesis by Lm5;
end;
theorem
mi(B \/ mi C) = mi (B \/ C) by Th44;
theorem Th46:
B c= C implies B ^ D c= C ^ D
proof
deffunc F(Element of DISJOINT_PAIRS A, Element of DISJOINT_PAIRS A) = $1 \/
$2;
defpred P[set,set] means $1 in B & $2 in D;
defpred Q[set,set] means $1 in C & $2 in D;
set X1 = { F(s,t): P[s,t] };
set X2 = { F(s,t): Q[s,t] };
assume B c= C;
then
A1: P[s, t] implies Q[s, t];
X1 c= X2 from FRAENKEL:sch 2(A1);
hence thesis by XBOOLE_1:26;
end;
Lm6: a in B ^ C implies ex b st b c= a & b in mi B ^ C
proof
assume a in B ^ C;
then consider b,c such that
A1: b in B and
A2: c in C and
A3: a = b \/ c by Th34;
consider d such that
A4: d c= b and
A5: d in mi B by A1,Th41;
d \/ c c= a by A3,A4,Th12;
then reconsider e = d \/ c as Element of DISJOINT_PAIRS A by Th26;
take e;
thus e c= a by A3,A4,Th12;
thus thesis by A2,A5,Th35;
end;
theorem Th47:
mi(B ^ C) c= mi B ^ C
proof
A1: mi B ^ C c= B ^ C by Th40,Th46;
now
let a;
assume
A2: a in mi(B ^ C);
then a in B ^ C by Th36;
then ex b st b c= a & b in mi B ^ C by Lm6;
hence a in mi B ^ C by A1,A2,Th36;
end;
hence thesis by Lm5;
end;
theorem Th48:
B^C = C^B
proof
deffunc F(Element of DISJOINT_PAIRS A,Element of DISJOINT_PAIRS A) = $1 \/
$2;
defpred P[set,set] means $1 in B & $2 in C;
defpred Q[set,set] means $2 in C & $1 in B;
set X1 = { F(s,t) where s,t is Element of DISJOINT_PAIRS A: P[s,t] };
set X2 = { F(t,s) where s,t is Element of DISJOINT_PAIRS A: Q[s,t] };
A1: F(s,t) = F(t,s);
A2: now
let x be object;
x in X2 iff ex s,t st x = t \/ s & t in C & s in B;
then x in X2 iff ex t,s st x = t \/ s & t in C & s in B;
hence x in X2 iff x in{ t \/ s where t,s: t in C & s in B };
end;
A3: P[s,t] iff Q[s,t];
X1 = X2 from FRAENKEL:sch 8(A3,A1);
hence thesis by A2,TARSKI:2;
end;
theorem Th49:
B c= C implies D ^ B c= D ^ C
proof
D ^ C = C ^ D & D ^ B = B ^ D by Th48;
hence thesis by Th46;
end;
theorem Th50:
mi(mi B ^ C) = mi (B ^ C)
proof
A1: mi B ^ C c= B ^ C by Th40,Th46;
now
let a;
assume
A2: a in mi(mi B ^ C);
A3: now
let b;
assume b in B ^ C;
then consider c such that
A4: c c= b and
A5: c in mi B ^ C by Lm6;
assume
A6: b c= a;
then c c= a by A4,Th2;
then c = a by A2,A5,Th36;
hence b = a by A4,A6,Th1;
end;
a in mi B ^ C by A2,Th36;
hence a in mi(B ^ C) by A1,A3,Th39;
end;
hence mi(mi B ^ C) c= mi(B ^ C) by Lm5;
A7: mi(B ^ C) c= mi B ^ C by Th47;
now
let a;
assume
A8: a in mi(B ^ C);
then for b st b in mi B ^ C holds b c= a implies b = a by A1,Th36;
hence a in mi(mi B ^ C) by A7,A8,Th39;
end;
hence thesis by Lm5;
end;
theorem Th51:
mi(B ^ mi C) = mi (B ^ C)
proof
B ^ mi C = mi C ^ B & B ^ C = C ^ B by Th48;
hence thesis by Th50;
end;
theorem Th52:
K^(L^M) = K^L^M
proof
A1: L^M = M^L & K^L = L^K by Th48;
A2: now
let K,L,M;
now
let a;
assume a in K^(L^M);
then consider b,c such that
A3: b in K and
A4: c in L^M and
A5: a = b \/ c by Th34;
consider b1,c1 being Element of DISJOINT_PAIRS A such that
A6: b1 in L and
A7: c1 in M and
A8: c = b1 \/ c1 by A4,Th34;
reconsider d = b \/ (b1 \/ c1) as Element of DISJOINT_PAIRS A by A5,A8;
A9: b \/(b1 \/ c1) = b \/ b1 \/ c1 by Th3;
then b \/ b1 c= d by Th10;
then reconsider c2 = b \/ b1 as Element of DISJOINT_PAIRS A by Th26;
c2 in K^L by A3,A6,Th35;
hence a in K^L^M by A5,A7,A8,A9,Th35;
end;
hence K^(L^M) c= K^L^M by Lm5;
end;
then
A10: K^(L^M) c= K^L^M;
K^L^M = M^(K^L) & K^(L^M) = L^M^K by Th48;
then K^L^M c= K^(L^M) by A1,A2;
hence thesis by A10;
end;
theorem Th53:
K^(L \/ M) = K^L \/ K^M
proof
now
let a;
assume a in K^(L \/ M);
then consider b,c such that
A1: b in K and
A2: c in L \/ M and
A3: a = b \/ c by Th34;
c in L or c in M by A2,XBOOLE_0:def 3;
then a in K^L or a in K^M by A1,A3,Th35;
hence a in K^L \/ K^M by XBOOLE_0:def 3;
end;
hence K^(L \/ M) c= K^L \/ K^M by Lm5;
K^L c= K^(L \/ M) & K^M c= K^(L \/ M) by Th49,XBOOLE_1:7;
hence thesis by XBOOLE_1:8;
end;
Lm7: a in B ^ C implies ex c st c in C & c c= a
proof
assume a in B ^ C;
then consider b,c such that
b in B and
A1: c in C and
A2: a = b \/ c by Th34;
take c;
thus c in C by A1;
thus thesis by A2,Th10;
end;
Lm8: mi(K ^ L \/ L) = mi L
proof
now
let a;
assume
A1: a in mi(K ^ L \/ L);
A2: now
let b;
assume b in L;
then b in K ^ L \/ L by XBOOLE_0:def 3;
hence b c= a implies b = a by A1,Th36;
end;
A3: now
assume a in K ^ L;
then consider b such that
A4: b in L and
A5: b c= a by Lm7;
b in K ^ L \/ L by A4,XBOOLE_0:def 3;
hence a in L by A1,A4,A5,Th36;
end;
a in K ^ L \/ L by A1,Th36;
then a in K ^ L or a in L by XBOOLE_0:def 3;
hence a in mi L by A3,A2,Th39;
end;
hence mi(K ^ L \/ L) c= mi L by Lm5;
now
let a;
assume
A6: a in mi L;
then
A7: a in L by Th36;
A8: now
let b;
assume b in K ^ L \/ L;
then
A9: b in K ^ L or b in L by XBOOLE_0:def 3;
assume
A10: b c= a;
now
assume b in K ^ L;
then consider c such that
A11: c in L and
A12: c c= b by Lm7;
c c= a by A10,A12,Th2;
then c = a by A6,A11,Th36;
hence b in L by A7,A10,A12,Th1;
end;
hence b = a by A6,A9,A10,Th36;
end;
a in K ^ L \/ L by A7,XBOOLE_0:def 3;
hence a in mi(K ^ L \/ L) by A8,Th39;
end;
hence thesis by Lm5;
end;
theorem Th54:
B c= B ^ B
proof
now
let a;
a = a \/ a;
hence a in B implies a in B ^ B by Th35;
end;
hence thesis by Lm5;
end;
theorem Th55:
mi(K ^ K) = mi K
proof
thus mi (K ^ K) = mi (K ^ K \/ K) by Th54,XBOOLE_1:12
.= mi K by Lm8;
end;
definition
let A;
func NormForm A -> strict LattStr means
:Def12:
the carrier of it =
Normal_forms_on A & for B, C being Element of Normal_forms_on A holds (the
L_join of it).(B, C) = mi (B \/ C) & (the L_meet of it).(B, C) = mi (B^C);
existence
proof
set L = Normal_forms_on A;
deffunc O(Element of L,Element of L) = mi ($1 \/ $2);
consider j being BinOp of L such that
A1: for x,y being Element of L holds j.(x,y) = O(x,y) from BINOP_1:sch
4;
deffunc O1(Element of L,Element of L) = mi ($1 ^ $2);
consider m being BinOp of L such that
A2: for x,y being Element of L holds m.(x,y) = O1(x,y) from BINOP_1:
sch 4;
take LattStr (# L, j, m #);
thus thesis by A1,A2;
end;
uniqueness
proof
set L = Normal_forms_on A;
let A1, A2 be strict LattStr such that
A3: the carrier of A1 = L and
A4: for A, B being Element of L holds (the L_join of A1).(A,B) = mi (A
\/ B) & (the L_meet of A1).(A,B) = mi (A^B) and
A5: the carrier of A2 = L and
A6: for A, B being Element of L holds (the L_join of A2).(A,B) = mi (A
\/ B) & (the L_meet of A2).(A,B) = mi (A^B);
reconsider a3 = the L_meet of A1, a4 = the L_meet of A2, a1 = the L_join
of A1, a2 = the L_join of A2 as BinOp of L by A3,A5;
now
let x,y be Element of L;
thus a1.(x,y) = mi (x \/ y) by A4
.= a2.(x,y) by A6;
end;
then
A7: a1 = a2;
now
let x,y be Element of L;
thus a3.(x,y) = mi (x^y) by A4
.= a4.(x,y) by A6;
end;
hence thesis by A3,A5,A7,BINOP_1:2;
end;
end;
registration
let A;
cluster NormForm A -> non empty;
coherence
proof
the carrier of NormForm A = Normal_forms_on A by Def12;
hence thesis;
end;
end;
Lm9: for a,b being Element of NormForm A holds a"\/"b = b"\/"a
proof
set G = NormForm A;
let a,b be Element of G;
reconsider a9 = a, b9 = b as Element of Normal_forms_on A by Def12;
a"\/"b = mi (b9 \/ a9) by Def12
.= b"\/"a by Def12;
hence thesis;
end;
Lm10: for a,b,c being Element of NormForm A holds a"\/"(b"\/"c) = (a"\/"b)"\/"
c
proof
set G = NormForm A;
let a, b, c be Element of G;
reconsider a9 = a, b9 = b, c9 = c as Element of Normal_forms_on A by Def12;
a"\/"(b"\/"c) = (the L_join of G).(a, mi (b9 \/ c9)) by Def12
.= mi (mi (b9 \/ c9) \/ a9) by Def12
.= mi ( a9 \/ ( b9 \/ c9 ) ) by Th44
.= mi ( a9 \/ b9 \/ c9 ) by XBOOLE_1:4
.= mi ( mi ( a9 \/ b9 ) \/ c9 ) by Th44
.= (the L_join of G).(mi (a9 \/ b9), c9 ) by Def12
.= (a"\/"b)"\/"c by Def12;
hence thesis;
end;
reserve K, L, M for Element of Normal_forms_on A;
Lm11: (the L_join of NormForm A).((the L_meet of NormForm A).(K,L), L) = L
proof
thus (the L_join of NormForm A). ((the L_meet of NormForm A).(K,L), L) = (
the L_join of NormForm A).(mi (K^L), L) by Def12
.= mi(mi(K ^ L) \/ L) by Def12
.= mi(K ^ L \/ L) by Th44
.= mi L by Lm8
.= L by Th42;
end;
Lm12: for a,b being Element of NormForm A holds (a"/\"b)"\/" b = b
proof
let a,b be Element of NormForm A;
reconsider a9 = a, b9 = b as Element of Normal_forms_on A by Def12;
set G = NormForm A;
thus (a"/\"b)"\/"b = (the L_join of G).((the L_meet of G).(a9,b9), b9)
.= b by Lm11;
end;
Lm13: for a,b being Element of NormForm A holds a"/\"b = b"/\"a
proof
set G = NormForm A;
let a, b be Element of G;
reconsider a9 = a, b9 = b as Element of Normal_forms_on A by Def12;
a"/\"b = mi (a9 ^ b9) by Def12
.= mi (b9 ^ a9) by Th48
.= b"/\"a by Def12;
hence thesis;
end;
Lm14: for a,b,c being Element of NormForm A holds a"/\"(b"/\"c) = (a"/\"b)"/\"
c
proof
set G = NormForm A;
let a, b, c be Element of G;
reconsider a9 = a, b9 = b, c9 = c as Element of Normal_forms_on A by Def12;
a"/\"(b"/\"c) = (the L_meet of G).(a, mi (b9 ^ c9)) by Def12
.= mi (a9 ^ mi (b9 ^ c9)) by Def12
.= mi ( a9 ^ ( b9 ^ c9 ) ) by Th51
.= mi ( a9 ^ b9 ^ c9 ) by Th52
.= mi ( mi ( a9 ^ b9 ) ^ c9 ) by Th50
.= (the L_meet of G).(mi (a9 ^ b9), c9 ) by Def12
.= (a"/\"b)"/\"c by Def12;
hence thesis;
end;
Lm15: (the L_meet of NormForm A).(K,(the L_join of NormForm A). (L,M)) = (the
L_join of NormForm A).((the L_meet of NormForm A).(K,L), (the L_meet of
NormForm A).(K,M))
proof
A1: (the L_meet of NormForm A).(K,M) = mi (K ^ M) by Def12;
(the L_join of NormForm A).(L, M) = mi (L \/ M) & (the L_meet of
NormForm A) .(K,L) = mi (K ^ L) by Def12;
then reconsider La = (the L_join of NormForm A).(L, M), Lb = (the L_meet of
NormForm A).(K,L), Lc = (the L_meet of NormForm A).(K,M) as Element of
Normal_forms_on A by A1;
(the L_meet of NormForm A). (K,(the L_join of NormForm A).(L,M)) = mi (K
^La) by Def12
.= mi (K^mi(L \/ M)) by Def12
.= mi (K^(L \/ M)) by Th51
.= mi (K^L \/ K^M) by Th53
.= mi (mi(K^L) \/ K^M) by Th44
.= mi (mi(K^L) \/ mi (K^M)) by Th44
.= mi (Lb \/ mi(K^M)) by Def12
.= mi (Lb \/ Lc) by Def12;
hence thesis by Def12;
end;
Lm16: for a,b being Element of NormForm A holds a"/\"(a"\/"b)=a
proof
set G = NormForm A;
let a,b be Element of G;
reconsider a9 = a, b9 = b as Element of Normal_forms_on A by Def12;
thus a"/\"(a"\/"b) = (the L_join of G).((the L_meet of G).(a9,a9), (the
L_meet of G).(a9,b9)) by Lm15
.= (the L_join of G).(mi (a9 ^ a9), (the L_meet of G).(a9,b9)) by Def12
.= (the L_join of G).(mi a9, (the L_meet of G).(a9,b9)) by Th55
.= a"\/"(a"/\"b) by Th42
.= (a"/\"b)"\/"a by Lm9
.= (b"/\"a)"\/"a by Lm13
.= a by Lm12;
end;
registration
let A;
cluster NormForm A -> Lattice-like;
coherence
proof
set G = NormForm A;
thus for u,v being Element of G holds u"\/"v = v"\/" u by Lm9;
thus for u,v,w being Element of G holds u"\/"(v"\/"w) = (u"\/"v)"\/"w by
Lm10;
thus for u,v being Element of G holds (u"/\"v)"\/" v = v by Lm12;
thus for u,v being Element of G holds u"/\"v = v"/\" u by Lm13;
thus for u,v,w being Element of G holds u"/\"(v"/\"w) = (u"/\"v)"/\"w by
Lm14;
let u,v be Element of G;
thus thesis by Lm16;
end;
end;
registration
let A;
cluster NormForm A -> distributive lower-bounded;
coherence
proof
set G = NormForm A;
thus G is distributive
proof
let u,v,w be Element of G;
reconsider K = u, L = v, M = w as Element of Normal_forms_on A by Def12;
thus u "/\" (v "\/" w) = (the L_meet of G).(K,(the L_join of G). (L,M))
.= (u "/\" v) "\/" (u "/\" w) by Lm15;
end;
thus G is lower-bounded
proof
reconsider E = {} as Element of Normal_forms_on A by Lm4;
reconsider e = E as Element of G by Def12;
take e;
let u be Element of G;
reconsider K = u as Element of Normal_forms_on A by Def12;
A1: e "\/" u = mi (E \/ K) by Def12
.= u by Th42;
then u "/\" e = e by LATTICES:def 9;
hence thesis by A1,LATTICES:def 9;
end;
end;
end;
theorem
{} is Element of NormForm A
proof
the carrier of NormForm A = Normal_forms_on A by Def12;
hence thesis by Lm4;
end;
theorem
Bottom NormForm A = {}
proof
{} in Normal_forms_on A by Lm4;
then reconsider Z = {} as Element of NormForm A by Def12;
now
let u be Element of NormForm A;
reconsider z = Z, u9 = u as Element of Normal_forms_on A by Def12;
thus Z "\/" u = mi (z \/ u9) by Def12
.= u by Th42;
end;
hence thesis by LATTICE2:14;
end;