:: On the Two Short Axiomatizations of Ortholattices
:: by Wioletta Truszkowska and Adam Grabowski
::
:: Received June 28, 2003
:: Copyright (c) 2003-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, ROBBINS1, SUBSET_1, ARYTM_3, LATTICES, ROBBINS2;
notations STRUCT_0, LATTICES, ROBBINS1;
constructors ROBBINS1;
registrations LATTICES, ROBBINS1, STRUCT_0;
theorems ROBBINS1, LATTICES, STRUCT_0;
begin :: One Axiom for Boolean Algebra
definition
let L be non empty ComplLLattStr;
attr L is satisfying_DN_1 means
:Def1:
for x, y, z, u being Element of L
holds (((x + y)` + z)` + (x + (z` + (z + u)`)`)`)` = z;
end;
registration
cluster TrivComplLat -> satisfying_DN_1;
coherence
by STRUCT_0:def 10;
cluster TrivOrtLat -> satisfying_DN_1;
coherence
by STRUCT_0:def 10;
end;
registration
cluster join-commutative join-associative satisfying_DN_1 for non empty
ComplLLattStr;
existence
proof
take TrivComplLat;
thus thesis;
end;
end;
reserve L for satisfying_DN_1 non empty ComplLLattStr;
reserve x, y, z for Element of L;
theorem Th1:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z, u,
v being Element of L holds ((x + y)` + (((z + u)` + x)` + (y` + (y + v)`)`)`)`
= y
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y, z, u, v be Element of L;
set X = ((z + u)` + x)`, Y = (z + (x` + (x + u)`)`)`;
set Z = y, U = v;
(((X + Y)` + Z)` + (X + (Z` + (Z + U)`)`)`)` = Z by Def1;
hence thesis by Def1;
end;
theorem Th2:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z, u
being Element of L holds ((x + y)` + ((z + x)` + (y` + (y + u)`)`)`)` = y
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y, z, u be Element of L;
set v = the Element of L;
((x + z)` + (((y + u)` + x)` + (z` + (z + v)`)`)`)` = z by Th1;
hence thesis by Th1;
end;
theorem Th3:
for L being satisfying_DN_1 non empty ComplLLattStr, x being
Element of L holds ((x + x`)` + x)` = x`
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x be Element of L;
set y = the Element of L;
set V = (x + y)`;
((x + x`)` + (((x`` + y)` + x)` + (x`` + (x` + V)`)`)`)` = x` by Th1;
hence thesis by Def1;
end;
theorem Th4:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z, u
being Element of L holds ((x + y)` + ((z + x)` + (((y + y`)` + y)` + (y + u)`)`
)`)` = y
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y, z, u be Element of L;
((y + y`)` + y)` = y` by Th3;
hence thesis by Th2;
end;
theorem Th5:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds ((x + y)` + ((z + x)` + y)`)` = y
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y, z be Element of L;
set u = the Element of L;
set U = (y` + (y + u)`)`;
((x + y)` + ((z + x)` + (((y + y`)` + y)` + (y + U)`)`)`)` = y by Th4;
hence thesis by Def1;
end;
theorem Th6:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds ((x + y)` + (x` + y)`)` = y
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y be Element of L;
set Z = (x + x`)`;
((x + y)` + ((Z + x)` + y)`)` = y by Th5;
hence thesis by Th3;
end;
theorem Th7:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds (((x + y)` + x)` + (x + y)`)` = x
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y be Element of L;
set X = (x + y)`;
((X + x)` + ((x + X)` + (((x + x`)` + x)` + (x + y)`)`)`)` = x by Th4;
hence thesis by Th5;
end;
theorem Th8:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds (x + ((x + y)` + x)`)` = (x + y)`
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y be Element of L;
set X = (x + y)`, Y = x;
(((X + Y)` + X)` + (X + Y)`)` = X by Th7;
hence thesis by Th7;
end;
theorem Th9:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds (((x + y)` + z)` + (x + z)`)` = z
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y, z be Element of L;
set X = (x + y)`, Y = z, Z = ((x + y)` + x)`;
((X + Y)` + ((Z + X)` + Y)`)` = Y by Th5;
hence thesis by Th7;
end;
theorem Th10:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds (x + ((y + z)` + (y + x)`)`)` = (y + x)`
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y, z be Element of L;
set Z = (y + x)`, X = (y + z)`, Y = x;
(((X + Y)` + Z)` + (X + Z)`)` = Z by Th9;
hence thesis by Th9;
end;
theorem Th11:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds ((((x + y)` + z)` + (x` + y)`)` + y)` = (x` + y)`
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y, z be Element of L;
set X = (x + y)`, Z = (x` + y)`, Y = z;
(((X + Y)` + Z)` + (X + Z)`)` = Z by Th9;
hence thesis by Th6;
end;
theorem Th12:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds (x + ((y + z)` + (z + x)`)`)` = (z + x)`
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y, z be Element of L;
set Y = z, Z = ((y + x)` + (y + z)`)`;
(x + ((Y + Z)` + (Y + x)`)`)` = (Y + x)` by Th10;
hence thesis by Th10;
end;
theorem Th13:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z, u
being Element of L holds ((x + y)` + ((z + x)` + (y` + (u + y)`)`)`)` = y
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y, z, u be Element of L;
set U = ((u + z)` + (u + y)`)`;
((x + y)` + ((z + x)` + (y` + (y + U)`)`)`)` = y by Th2;
hence thesis by Th10;
end;
theorem Th14:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds (x + y)` = (y + x)`
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y be Element of L;
set Z = y, X = x, Y = (y + x)`;
((Y + Z)` + (Z + X)`)` = y by Th7;
hence thesis by Th12;
end;
theorem Th15:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds (((x + y)` + (y + z)`)` + z)` = (y + z)`
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y, z be Element of L;
set Y = ((x + y)` + (y + z)`)`;
(z + Y)` = (Y + z)` by Th14;
hence thesis by Th12;
end;
theorem Th16:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds ((x + ((x + y)` + z)`)` + z)` = ((x + y)` + z)`
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y, z be Element of L;
set X = ((x + y)` + x)`, Y = (x + y)`;
(X + Y)` = x by Th7;
hence thesis by Th15;
end;
theorem Th17:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds (((x + y)` + x)` + y)` = (y + y)`
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y be Element of L;
set X = (x + y)`;
(X + ((X + x)` + y)`)` = y by Th5;
hence thesis by Th16;
end;
theorem Th18:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds (x` + (y + x)`)` = x
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y be Element of L;
set X = (y + x)`;
(X + ((x` + y)` + (x` + X)`)`)` = x by Th13;
hence thesis by Th10;
end;
theorem Th19:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds ((x + y)` + y`)` = y
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y be Element of L;
(y` + (x + y)`)` = y by Th18;
hence thesis by Th14;
end;
theorem Th20:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds (x + (y + x`)`)` = x`
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y be Element of L;
set Z = x`, X = y, Y = x;
(((X + Y)` + Z)` + (X + Z)`)` = Z by Th9;
hence thesis by Th19;
end;
theorem Th21:
for L being satisfying_DN_1 non empty ComplLLattStr, x being
Element of L holds (x + x)` = x`
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x be Element of L;
set y = the Element of L;
set Y = (y + x)`;
(x + (Y + x`)`)` = x` by Th20;
hence thesis by Th19;
end;
theorem Th22:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds (((x + y)` + x)` + y)` = y`
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y be Element of L;
y` = (y + y)` by Th21
.= (((x + y)` + x)` + y)` by Th17;
hence thesis;
end;
theorem Th23:
for L being satisfying_DN_1 non empty ComplLLattStr, x being
Element of L holds x`` = x
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x be Element of L;
x`` = (((x + x`)` + x)` + x`)` by Th22
.= x by Th19;
hence thesis;
end;
theorem Th24:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds ((x + y)` + x)`+ y = y``
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y be Element of L;
(((x + y)` + x)` + y)`` = y`` by Th22;
hence thesis by Th23;
end;
theorem Th25:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds (x + y)`` = y + x
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y be Element of L;
(x + y)`` = (y + x)`` by Th14
.= y + x by Th23;
hence thesis;
end;
theorem Th26:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds x + ((y + z)` + (y + x)`)` = (y + x )``
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y, z be Element of L;
(x + ((y + z)` + (y + x)`)`)`` = (y + x)`` by Th10;
hence thesis by Th23;
end;
theorem Th27:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds x + y = y + x
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y be Element of L;
x + y = (x + y)`` by Th23
.= y + x by Th25;
hence thesis;
end;
Lm1: for L being satisfying_DN_1 non empty ComplLLattStr holds L is
join-commutative
proof
let L;
for x, y holds x + y = y + x by Th27;
hence thesis by LATTICES:def 4;
end;
registration
cluster satisfying_DN_1 -> join-commutative for non empty ComplLLattStr;
coherence by Lm1;
end;
theorem Th28:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds ((x + y)` + x)` + y = y
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y be Element of L;
((x + y)` + x)` + y = y`` by Th24;
hence thesis by Th23;
end;
theorem
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds ((x + y)` + y)`+ x = x by Th28;
theorem
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds x + ((y + x)` + y)` = x by Th28;
theorem Th31:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds (x + y`)` + (y` + y)` = (x + y`)`
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y be Element of L;
set X = (x + y`)`;
X + ((y + X)` + y)` = X by Th28;
hence thesis by Th20;
end;
theorem Th32:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds (x + y)` + (y + y`)` = (x + y)`
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y be Element of L;
set X = (x + y)`, Y = y`;
X + ((Y + X)` + Y)` = X by Th28;
hence thesis by Th18;
end;
theorem
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds (x + y)` + (y` + y)` = (x + y)` by Th32;
theorem Th34:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds ((x + y`)`` + y)` = (y` + y)`
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y be Element of L;
set Y = y`, Z = y;
(((x + Y)` + (Y + Z)`)` + Z)` = (Y + Z)` by Th15;
hence thesis by Th31;
end;
theorem Th35:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds ((x + y`) + y)` = (y` + y)`
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y be Element of L;
((x + y`)`` + y)` = (y` + y)` by Th34;
hence thesis by Th23;
end;
theorem Th36:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds ((((x + y`) + z)` + y)` + (y` + y)`)` = y
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y, z be Element of L;
((x + y`) + y)` = (y` + y)` by Th35;
hence thesis by Th9;
end;
theorem Th37:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds x + ((y + z)` + (y + x)`)` = y + x
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y, z be Element of L;
x + ((y + z)` + (y + x)`)` = (y + x )`` by Th26;
hence thesis by Th23;
end;
theorem Th38:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds x + (y + ((z + y)` + x)`)` = (z + y)` + x
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y, z be Element of L;
set Y = (z + y)`, Z = y`;
x + ((Y + Z)` + (Y + x)`)` = Y + x by Th37;
hence thesis by Th19;
end;
theorem
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being
Element of L holds x + ((y + x)` + (y + z)`)` = y + x by Th37;
theorem Th40:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds ((x + y)` + ((x + y)` + (x + z)`)`)` + y = y
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y, z be Element of L;
set Y = ((x + y)` + (x + z)`)`;
((y + Y)` + Y)`+ y = y by Th28;
hence thesis by Th37;
end;
theorem Th41:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds (((x + y`) + z)` + y)`` = y
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y, z be Element of L;
(((x + y`) + z)` + y)` + (y` + y)` = (((x + y`) + z)` + y)` by Th32;
hence thesis by Th36;
end;
theorem Th42:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds x + ((y + x`) + z)` = x
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y, z be Element of L;
(((y + x`) + z)` + x)`` = x by Th41;
hence thesis by Th25;
end;
theorem Th43:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds x` + ((y + x) + z)` = x`
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y, z be Element of L;
set X = x`;
X + ((y + X`) + z)` = X by Th42;
hence thesis by Th23;
end;
theorem Th44:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds (x + y)` + x = x + y`
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y be Element of L;
set Z = x;
x + (y + ((Z + y)` + x)`)` = (Z + y)` + x by Th38;
hence thesis by Th28;
end;
theorem Th45:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y being
Element of L holds (x + (x + y`)`)` = (x + y)`
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y be Element of L;
(x + ((x + y)` + x)`)` = (x + y)` by Th8;
hence thesis by Th44;
end;
theorem Th46:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds ((x + y)` + (x + z))` + y = y
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y, z be Element of L;
((x + y)` + ((x + y)` + (x + z)`)`)` = ((x + y)` + (x + z))` by Th45;
hence thesis by Th40;
end;
theorem Th47:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds (((x + y)` + z)` + (x` + y)`)` + y = (x` + y)``
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y, z be Element of L;
((((x + y)` + z)` + (x` + y)`)` + y)`` = (x` + y)`` by Th11;
hence thesis by Th23;
end;
theorem Th48:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds (((x + y)` + z)` + (x` + y)`)` + y = x` + y
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y, z be Element of L;
(((x + y)` + z)` + (x` + y)`)` + y = (x` + y)`` by Th47;
hence thesis by Th23;
end;
theorem Th49:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds (x` + ((y + x)`` + (y + z))`)` + (y + z) = (y + x)``+
(y + z)
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y, z be Element of L;
set X = (y + x)`, Y = (y + z), Z = x;
(((X + Y)` + Z)` + (X` + Y)`)` + Y = X` + Y by Th48;
hence thesis by Th46;
end;
theorem Th50:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds (x` + ((y + x) + (y + z))`)` + (y + z) = (y + x)`` + (
y + z)
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y, z be Element of L;
(x` + ((y + x)`` + (y + z))`)` + (y + z) = (y + x)`` + (y + z) by Th49;
hence thesis by Th23;
end;
theorem Th51:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds (x` + ((y + x) + (y + z))`)` + (y + z) = (y + x) + (y
+ z)
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y, z be Element of L;
(x` + ((y + x) + (y + z))`)` + (y + z) = (y + x)`` + (y + z) by Th50;
hence thesis by Th23;
end;
theorem Th52:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds x`` + (y + z) = (y + x) + (y + z)
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y, z be Element of L;
x` + ((y + x) + (y + z))` = x` by Th43;
hence thesis by Th51;
end;
theorem Th53:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds (x + y) + (x + z) = y + (x + z)
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y, z be Element of L;
set Y = x, X = y;
X`` + (Y + z) = (Y + X) + (Y + z) by Th52;
hence thesis by Th23;
end;
theorem
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being
Element of L holds (x + y) + (x + z) = z + (x + y) by Th53;
theorem Th55:
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z
being Element of L holds x + (y + z) = z + (y + x)
proof
let L be satisfying_DN_1 non empty ComplLLattStr;
let x, y, z be Element of L;
(y + x) + (y + z) = z + (y + x) by Th53;
hence thesis by Th53;
end;
theorem
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being
Element of L holds x + (y + z) = y + (z + x) by Th55;
theorem
for L being satisfying_DN_1 non empty ComplLLattStr, x, y, z being
Element of L holds (x + y) + z = x + (y + z) by Th55;
Lm2: for L being satisfying_DN_1 non empty ComplLLattStr holds L is
join-associative
proof
let L;
for x, y, z holds (x + y) + z = x + (y + z) by Th55;
hence thesis by LATTICES:def 5;
end;
Lm3: L is Robbins
proof
for x, y holds ((x + y)` + (x + y`)`)` = x by Th6;
hence thesis by ROBBINS1:def 5;
end;
registration
cluster satisfying_DN_1 -> join-associative for non empty ComplLLattStr;
coherence by Lm2;
cluster satisfying_DN_1 -> Robbins for non empty ComplLLattStr;
coherence by Lm3;
end;
theorem Th58:
for L being non empty ComplLLattStr, x, z being Element of L st L
is join-commutative join-associative Huntington holds (z + x) *' (z + x`) = z
proof
let L be non empty ComplLLattStr;
let x, z be Element of L;
assume L is join-commutative join-associative Huntington;
then reconsider
L9 = L as join-commutative join-associative Huntington non empty
ComplLLattStr;
reconsider z9 = z, x9 = x as Element of L9;
(z9 + x9) *' (z9 + x9`) = z9 + (x9 *' x9`) by ROBBINS1:31
.= z9 + Bot L9 by ROBBINS1:15
.= z9 by ROBBINS1:13;
hence thesis;
end;
theorem Th59:
for L being join-commutative join-associative non empty ComplLLattStr
st L is Robbins holds L is satisfying_DN_1
proof
let L be join-commutative join-associative non empty ComplLLattStr;
assume L is Robbins;
then reconsider
L9 = L as join-commutative join-associative Robbins non empty
ComplLLattStr;
let x, y, z, u be Element of L;
A1: L9 is Huntington;
then
A2: (z + x) *' (z + x`) = z by Th58;
A3: ((x + y)` + z) *' z = (z + (x + y)`) *' z
.= z *' (z + (x + y)`)
.= z by A1,ROBBINS1:21;
A4: (((x + y)` + z) *' x) + z = z + (((x + y)` + z) *' x)
.= (z + ((x + y)` + z)) *' (z + x) by A1,ROBBINS1:31
.= (((x + y)` + z) + z) *' (z + x)
.= ((x + y)` + (z + z)) *' (z + x) by LATTICES:def 5
.= ((x + y)` + z) *' (z + x) by A1,ROBBINS1:12
.= ((x` *' y`)`` + z) *' (z + x) by A1,ROBBINS1:17
.= ((x` *' y`) + z) *' (z + x) by A1,ROBBINS1:3
.= (z + (x` *' y`)) *' (z + x)
.= ((z + x`) *' (z + y`)) *' (z + x) by A1,ROBBINS1:31
.= (z + x) *' ((z + x`) *' (z + y`))
.= (z + x) *' ((x` + z) *' (z + y`))
.= (z + x) *' ((x` + z) *' (y` + z))
.= (z + x) *' (x` + z) *' (y` + z) by A1,ROBBINS1:16
.= (z + x) *' (z + x`) *' (y` + z)
.= z *' (z + y`) by A2
.= z by A1,ROBBINS1:21;
(((x + y)` + z)` + (x + (z` + (z + u)`)`)`)` = (((x + y)` + z)`` *' (x +
(z` + (z + u)`)`)``)`` by A1,ROBBINS1:17
.= ((x + y)` + z)`` *' (x + (z` + (z + u)`)`)`` by A1,ROBBINS1:3
.= ((x + y)` + z)`` *' (x + (z` + (z + u)`)`) by A1,ROBBINS1:3
.= ((x + y)` + z) *' (x + (z` + (z + u)`)`) by A1,ROBBINS1:3
.= ((x + y)`` *' z`)` *' (x + (z` + (z + u)`)`) by A1,ROBBINS1:17
.= ((x + y) *' z`)` *' (x + (z` + (z + u)`)`) by A1,ROBBINS1:3
.= ((x + y) *' z`)` *' (x + (z`` *' (z + u)``)``) by A1,ROBBINS1:17
.= ((x + y) *' z`)` *' (x + (z *' (z + u)``)``) by A1,ROBBINS1:3
.= ((x + y) *' z`)` *' (x + (z *' (z + u)``)) by A1,ROBBINS1:3
.= ((x + y) *' z`)` *' (x + (z *' (z + u))) by A1,ROBBINS1:3
.= ((x + y) *' z`)` *' (x + z) by A1,ROBBINS1:21
.= (((x + y) *' z`)` *' x) + (((x + y) *' z`)` *' z) by A1,ROBBINS1:30
.= (((x + y)`` *' z`)` *' x) + (((x + y) *' z`)` *' z) by A1,ROBBINS1:3
.= (((x + y)` + z) *' x) + (((x + y) *' z`)` *' z) by A1,ROBBINS1:17
.= (((x + y)` + z) *' x) + (((x + y)`` *' z`)` *' z) by A1,ROBBINS1:3
.= z by A1,A3,A4,ROBBINS1:17;
hence thesis;
end;
registration
cluster join-commutative join-associative Robbins -> satisfying_DN_1 for non
empty ComplLLattStr;
coherence by Th59;
end;
registration
cluster satisfying_DN_1 de_Morgan for preOrthoLattice;
existence
proof
take TrivOrtLat;
thus thesis;
end;
end;
registration
cluster satisfying_DN_1 de_Morgan -> Boolean for preOrthoLattice;
coherence;
cluster Boolean -> satisfying_DN_1 for well-complemented preOrthoLattice;
coherence;
end;
begin :: Meredith Two Axioms for Boolean Algebras
definition
let L be non empty ComplLLattStr;
attr L is satisfying_MD_1 means
for x, y being Element of L holds (x` + y)` + x = x;
attr L is satisfying_MD_2 means
for x, y, z being Element of L holds (x` + y)` + (z + y) = y + (z + x);
end;
Lm4: now
let L be non empty ComplLLattStr;
assume
A1: L is satisfying_MD_1 satisfying_MD_2;
A2: for x, y being Element of L holds x` + (x` + y) = x` + y
proof
let x, y be Element of L;
set X = x` + y;
X` + x = x by A1;
hence thesis by A1;
end;
A3: for x, y being Element of L holds (x` + y)` + y = y + x
proof
let x, y be Element of L;
set X = x` + y;
A4: X` + (X` + y) = y + (X` + x) by A1;
(x` + y)` + y = X` + (X` + y) by A2
.= y + x by A1,A4;
hence thesis;
end;
A5: for x being Element of L holds x + x = x
proof
let x be Element of L;
x + x = (x` + x)` + x by A3
.= x by A1;
hence thesis;
end;
A6: for x, y being Element of L holds x + (x + y) = x + y
proof
let x, y be Element of L;
x + (x + y) = (y` + x)` + (x + x) by A1
.= (y` + x)` + x by A5
.= x + y by A3;
hence thesis;
end;
A7: for x, y being Element of L holds (x + y) + y = x + y
proof
let x, y be Element of L;
set Y = x + y;
(x + y) + y = (y` + (x + y))` + (x + y) by A3
.= (y` + (x + y))` + (x + (x + y)) by A6
.= Y + (x + y) by A1
.= x + y by A5;
hence thesis;
end;
A8: for x, y being Element of L holds (x + y) + x = x + y
proof
let x, y be Element of L;
(x + y) + x = ((y` + x)` + x) + x by A3
.= (y` + x)` + x by A7
.= x + y by A3;
hence thesis;
end;
A9: for x, y being Element of L holds x + (y + (y + x)) = y + x
proof
let x, y be Element of L;
set Z = y + x;
x + (y + (y + x)) = (Z` + x)` + (y + x) by A1
.= y + x by A1;
hence thesis;
end;
A10: for x, y being Element of L holds x + (y + x) = y + x
proof
let x, y be Element of L;
x + (y + x) = x + (y + (y + x)) by A6
.= y + x by A9;
hence thesis;
end;
A11: for x, y being Element of L holds (x + y`)` + y = y
proof
let x, y be Element of L;
(x + y`)` + y = (y` + (x + y`))` + y by A10
.= y by A1;
hence thesis;
end;
A12: for x being Element of L holds x`` + x = x
proof
let x be Element of L;
(x` + x`)` + x = x by A1;
hence thesis by A5;
end;
A13: for x being Element of L holds x + x`` = x
proof
let x be Element of L;
x + x`` = (x`` + x) + x`` by A12
.= x`` + x by A8
.= x by A12;
hence thesis;
end;
A14: for x, y being Element of L holds x + (x`` + y) = x + y
proof
let x, y be Element of L;
x + (x`` + y) = (y` + x)` + (x`` + x) by A1
.= (y` + x)` + x by A12
.= x + y by A3;
hence thesis;
end;
A15: for x being Element of L holds x + x```` = x
proof
let x be Element of L;
x + x```` = x + (x`` + x````) by A14
.= x + x`` by A13
.= x by A13;
hence thesis;
end;
A16: for x being Element of L holds x``` = x`
proof
let x be Element of L;
x``` = (x + x````)` + x``` by A11
.= x` + x``` by A15
.= x` by A13;
hence thesis;
end;
A17: for x, y, z being Element of L holds (x` + y)` + ((x` + z)` + y) = y + x
proof
let x, y, z be Element of L;
(x` + y)` + ((x` + z)` + y) = y + ((x` + z)` + x) by A1
.= y + x by A1;
hence thesis;
end;
A18: for x, y being Element of L holds x + y`` = x + y
proof
let x, y be Element of L;
x + y = (y` + x)` + ((y` + x)` + x) by A17
.= (y` + x)` + ((y``` + x)` + x) by A16
.= (y``` + x)` + ((y``` + x)` + x) by A16
.= x + y`` by A17;
hence thesis;
end;
A19: for x being Element of L holds x`` = x
proof
let x be Element of L;
x`` = (x``` + x``)` + x`` by A1
.= (x` + x``)` + x`` by A16
.= (x` + x``)` + x by A18
.= x by A1;
hence thesis;
end;
A20: for x, y, z being Element of L holds (x` + ((y + x)` + z)`)` + (y + ((y
+ x)` + z)`) = y + x
proof
let x, y, z be Element of L;
set P = ((y + x)` + z)`;
(x` + P)` + (y + P) = P + (y + x) by A1
.= y + x by A1;
hence thesis;
end;
A21: for x, y being Element of L holds (x` + (x + y)`)` + (y` + (x + y)`) =
y` + x
proof
let x, y be Element of L;
(x` + (x + y)`)` + (y` + (x + y)`) = (x` + (x + y)`)` + (y` + ((y` +
x)` + x)`) by A3
.= (x` + ((y` + x)` + x)`)` + (y` + ((y` + x)` + x)`) by A3
.= y` + x by A20;
hence thesis;
end;
A22: for x, y being Element of L holds x + (x` + y)` = x
proof
let x, y be Element of L;
x + (x` + y)` = ((x` + y)` + x) + (x` + y)` by A1
.= (x` + y)` + x by A8
.= x by A1;
hence thesis;
end;
A23: for x, y being Element of L holds x` + (x + y)` = x`
proof
let x, y be Element of L;
x` = x` + (x`` + y)` by A22
.= x` + (x + y)` by A19;
hence thesis;
end;
A24: for x, y being Element of L holds x + (y + x`)` = x
proof
let x, y be Element of L;
x + (y + x`)` = ((y + x`)` + x) + (y + x`)` by A11
.= (y + x`)` + x by A8
.= x by A11;
hence thesis;
end;
A25: for x, y being Element of L holds x` + (y + x)` = x`
proof
let x, y be Element of L;
x` = x` + (y + x``)` by A24
.= x` + (y + x)` by A19;
hence thesis;
end;
A26: for x, y being Element of L holds x + y` = y` + x
proof
let x, y be Element of L;
y` + x = (x` + (x + y)`)` + (y` + (x + y)`) by A21
.= x`` + (y` + (x + y)`) by A23
.= x`` + y` by A25
.= x + y` by A19;
hence thesis;
end;
A27: for x, y being Element of L holds x + y = y + x
proof
let x, y be Element of L;
y`` = y by A19;
hence thesis by A26;
end;
hence L is join-commutative by LATTICES:def 4;
A28: for x, y, z being Element of L holds ((x` + y)` + z)` + (x` + z) = z + (
x` + y)
proof
let x, y, z be Element of L;
((x` + y)` + z)` + (x` + z) = z + (x` + (x` + y)) by A1
.= z + (x` + y) by A2;
hence thesis;
end;
A29: for x, y being Element of L holds x + (y` + x) = y` + x
proof
let x, y be Element of L;
x + (y` + x) = ((y` + x)` + x)` + (y` + x) by A28
.= y` + x by A1;
hence thesis;
end;
A30: for x, y being Element of L holds (x + y)` + x = y` + x
proof
let x, y be Element of L;
set Y = y` + x;
y` + x = x + (y` + x) by A29
.= (Y` + x)` + x by A3
.= (x + y)` + x by A3;
hence thesis;
end;
A31: for x, y being Element of L holds (x + y)` + (y` + x)` = x` + (y` + x)`
proof
let x, y be Element of L;
(x + y)` + (y` + x)` = ((y` + x)` + x)` + (y` + x)` by A3
.= x` + (y` + x)` by A30;
hence thesis;
end;
for x, y being Element of L holds (x` + y`)` + (x` + y)` = x
proof
let x, y be Element of L;
(x` + y`)` + (x` + y)` = (y` + x`)` + (x` + y)` by A27
.= (x` + y)` + (y` + x`)` by A27
.= x`` + (y` + x`)` by A31
.= x + (y` + x`)` by A19
.= x by A24;
hence thesis;
end;
hence L is Huntington by ROBBINS1:def 6;
A32: for x, y, z being Element of L holds (x + y) + (y + z) = (x + y) + z
proof
let x, y, z be Element of L;
set Y = x + y;
(x + y) + z = (z` + Y)` + Y by A3
.= (z` + Y)` + (y + Y) by A10
.= Y + (y + z) by A1;
hence thesis;
end;
for x, y, z being Element of L holds (x + y) + z = x + (y + z)
proof
let x, y, z be Element of L;
for x, y, z being Element of L holds (x + y) + (z + x) = y + (x + z)
proof
let x, y, z be Element of L;
(x + y) + (z + x) = (z + x) + (x + y) by A27
.= (z + x) + y by A32
.= (x + z) + y by A27
.= y + (x + z) by A27;
hence thesis;
end;
then (y + x) + (z + y) = x + (y + z);
then
A33: (x + y) + (z + y) = x + (y + z) by A27;
(x + y) + z = (x + y) + (y + z) by A32
.= x + (y + z) by A27,A33;
hence thesis;
end;
hence L is join-associative by LATTICES:def 5;
end;
registration
cluster satisfying_MD_1 satisfying_MD_2 -> join-commutative join-associative
Huntington for non empty ComplLLattStr;
coherence by Lm4;
cluster join-commutative join-associative Huntington -> satisfying_MD_1
satisfying_MD_2 for non empty ComplLLattStr;
coherence
proof
let L be non empty ComplLLattStr;
assume L is join-commutative join-associative Huntington;
then reconsider
L9 = L as join-commutative join-associative Huntington non
empty ComplLLattStr;
A1: L9 is satisfying_MD_2
proof
let x, y, z be Element of L9;
set Z = z + y;
A2: Z + y` = z + (y + y`) by LATTICES:def 5
.= z + Top L9 by ROBBINS1:def 8
.= Top L9 by ROBBINS1:19;
(x` + y)` + (z + y) = (x` + y``)` + (z + y) by ROBBINS1:3
.= (x *' y`) + (z + y) by ROBBINS1:def 4
.= (Z + x) *' (Z + y`) by ROBBINS1:31
.= Z + x by A2,ROBBINS1:14
.= y + (z + x) by LATTICES:def 5;
hence thesis;
end;
L9 is satisfying_MD_1
proof
let x, y be Element of L9;
(x` + y)` + x = (x` + y``)` + x by ROBBINS1:3
.= (x *' y`) + x by ROBBINS1:def 4
.= x by ROBBINS1:20;
hence thesis;
end;
hence thesis by A1;
end;
end;
registration
cluster satisfying_MD_1 satisfying_MD_2 satisfying_DN_1 de_Morgan
for preOrthoLattice;
existence
proof
take TrivOrtLat;
thus thesis;
end;
end;
registration
cluster satisfying_MD_1 satisfying_MD_2 de_Morgan -> Boolean for
preOrthoLattice;
coherence;
cluster Boolean -> satisfying_MD_1 satisfying_MD_2 for well-complemented
preOrthoLattice;
coherence;
end;