The Mizar article:

On the Two Short Axiomatizations of Ortholattices

by
Wioletta Truszkowska, and
Adam Grabowski

Received June 28, 2003

Copyright (c) 2003 Association of Mizar Users

MML identifier: ROBBINS2
[ MML identifier index ]


environ

 vocabulary LATTICES, SUBSET_1, ARYTM_3, ROBBINS1, ROBBINS2;
 notation STRUCT_0, LATTICES, ROBBINS1;
 constructors REALSET1, ROBBINS1;
 clusters ROBBINS1;
 theorems ROBBINS1, LATTICES, REALSET1;

begin :: One Axiom for Boolean Algebra

definition let L be non empty ComplLattStr;
  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;

definition
  cluster TrivComplLat -> satisfying_DN_1;
  coherence
  proof
    let x, y, z, u be Element of TrivComplLat;
    thus thesis by REALSET1:def 20;
  end;
  cluster TrivOrtLat -> satisfying_DN_1;
  coherence
  proof
    let x, y, z, u be Element of TrivOrtLat;
    thus thesis by REALSET1:def 20;
  end;
end;

definition
  cluster join-commutative join-associative satisfying_DN_1
    (non empty ComplLattStr);
  existence
  proof
    take TrivComplLat;
    thus thesis;
  end;
end;

 reserve L for satisfying_DN_1 (non empty ComplLattStr);
 reserve x, y, z, u, v for Element of L;

theorem Th1: :: A61
  for L being satisfying_DN_1 (non empty ComplLattStr),
      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 ComplLattStr);
      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: :: A62
  for L being satisfying_DN_1 (non empty ComplLattStr),
      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 ComplLattStr);
      let x, y, z, u be Element of L;
      consider v being Element of L;
      ((x + z)` + (((y + u)` + x)` + (z` + (z + v)`)`)`)` = z by Th1;
      hence thesis by Th1;
    end;

theorem Th3: :: A63
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x being Element of L holds
    ((x + x`)` + x)` = x`
    proof
      let L be satisfying_DN_1 (non empty ComplLattStr);
      let x be Element of L;
      consider y, u being Element of L;
      set V = (x + u)`;
      ((x + x`)` + (((x`` + y)` + x)` + (x`` + (x` + V)`)`)`)` = x` by Th1;
      hence thesis by Def1;
    end;

theorem Th4: :: A64
  for L being satisfying_DN_1 (non empty ComplLattStr),
      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 ComplLattStr);
      let x, y, z, u be Element of L;
      ((y + y`)` + y)` = y` by Th3;
      hence thesis by Th2;
    end;

theorem Th5: :: A65
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    ((x + y)` + ((z + x)` + y)`)` = y
    proof
      let L be satisfying_DN_1 (non empty ComplLattStr);
      let x, y, z be Element of L;
      consider u being 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: :: A66
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    ((x + y)` + (x` + y)`)` = y
    proof
      let L be satisfying_DN_1 (non empty ComplLattStr);
      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: :: A67
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    (((x + y)` + x)` + (x + y)`)` = x
    proof
      let L be satisfying_DN_1 (non empty ComplLattStr);
      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: :: A68
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    (x + ((x + y)` + x)`)` = (x + y)`
    proof
      let L be satisfying_DN_1 (non empty ComplLattStr);
      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: :: A69
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    (((x + y)` + z)` + (x + z)`)` = z
    proof
      let L be satisfying_DN_1 (non empty ComplLattStr);
      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: :: A70
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    (x + ((y + z)` + (y + x)`)`)` = (y + x)`
    proof
      let L be satisfying_DN_1 (non empty ComplLattStr);
      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: :: A71
  for L being satisfying_DN_1 (non empty ComplLattStr),
      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 ComplLattStr);
      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: :: A72
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    (x + ((y + z)` + (z + x)`)`)` = (z + x)`
    proof
      let L be satisfying_DN_1 (non empty ComplLattStr);
      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: :: A73
  for L being satisfying_DN_1 (non empty ComplLattStr),
      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 ComplLattStr);
      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: :: A74
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    (x + y)` = (y + x)`
    proof
      let L be satisfying_DN_1 (non empty ComplLattStr);
      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: :: A75
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    (((x + y)` + (y + z)`)` + z)` = (y + z)`
    proof
      let L be satisfying_DN_1 (non empty ComplLattStr);
      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: :: A76
  for L being satisfying_DN_1 (non empty ComplLattStr),
      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 ComplLattStr);
      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: :: A77
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    (((x + y)` + x)` + y)` = (y + y)`
    proof
      let L be satisfying_DN_1 (non empty ComplLattStr);
      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: :: A78
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    (x` + (y + x)`)` = x
    proof
      let L be satisfying_DN_1 (non empty ComplLattStr);
      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: :: A79
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    ((x + y)` + y`)` = y
    proof
      let L be satisfying_DN_1 (non empty ComplLattStr);
      let x, y be Element of L;
      (y` + (x + y)`)` = y by Th18;
      hence thesis by Th14;
    end;

theorem Th20: :: A80
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    (x + (y + x`)`)` = x`
    proof
      let L be satisfying_DN_1 (non empty ComplLattStr);
      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: :: A81
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x being Element of L holds
    (x + x)` = x`
    proof
      let L be satisfying_DN_1 (non empty ComplLattStr);
      let x be Element of L;
      consider y being Element of L;
      set Y = (y + x)`;
      (x + (Y + x`)`)` = x` by Th20;
      hence thesis by Th19;
    end;

theorem Th22: :: A83
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    (((x + y)` + x)` + y)` = y`
    proof
      let L be satisfying_DN_1 (non empty ComplLattStr);
      let x, y be Element of L;
      y` = (y + y)` by Th21
        .= (((x + y)` + x)` + y)` by Th17;
      hence thesis;
    end;

theorem Th23: :: A85
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x being Element of L holds
    x`` = x
    proof
      let L be satisfying_DN_1 (non empty ComplLattStr);
      let x be Element of L;
      x`` = (((x + x`)` + x)` + x`)` by Th22
         .= x by Th19;
      hence thesis;
    end;

theorem Th24: :: A86
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    ((x + y)` + x)`+ y = y``
    proof
      let L be satisfying_DN_1 (non empty ComplLattStr);
      let x, y be Element of L;
      (((x + y)` + x)` + y)`` = y`` by Th22;
      hence thesis by Th23;
    end;

theorem Th25: :: A87
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    (x + y)`` = y + x
    proof
      let L be satisfying_DN_1 (non empty ComplLattStr);
      let x, y be Element of L;
      (x + y)`` = (y + x)`` by Th14
               .= y + x by Th23;
      hence thesis;
    end;

theorem Th26: :: A88
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    x + ((y + z)` + (y + x)`)` = (y + x )``
    proof
      let L be satisfying_DN_1 (non empty ComplLattStr);
      let x, y, z be Element of L;
      (x + ((y + z)` + (y + x)`)`)`` = (y + x)`` by Th10;
      hence thesis by Th23;
    end;

theorem Th27: :: A89
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    x + y = y + x
    proof
      let L be satisfying_DN_1 (non empty ComplLattStr);
      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 ComplLattStr) 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;

definition
  cluster satisfying_DN_1 -> join-commutative (non empty ComplLattStr);
  coherence by Lm1;
end;

theorem Th28: :: A90
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    ((x + y)` + x)` + y = y
    proof
      let L be satisfying_DN_1 (non empty ComplLattStr);
      let x, y be Element of L;
      ((x + y)` + x)` + y = y`` by Th24;
      hence thesis by Th23;
    end;

theorem :: A91
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    ((x + y)` + y)`+ x = x by Th28;

theorem :: A92
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    x + ((y + x)` + y)` = x by Th28;

theorem Th31: :: A93
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    (x + y`)` + (y` + y)` = (x + y`)`
    proof
      let L be satisfying_DN_1 (non empty ComplLattStr);
      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: :: A94
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    (x + y)` + (y + y`)` = (x + y)`
    proof
      let L be satisfying_DN_1 (non empty ComplLattStr);
      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 :: A95
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    (x + y)` + (y` + y)` = (x + y)` by Th32;

theorem Th34: :: A96
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    ((x + y`)`` + y)` = (y` + y)`
    proof
      let L be satisfying_DN_1 (non empty ComplLattStr);
      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: :: A97
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    ((x + y`) + y)` = (y` + y)`
    proof
      let L be satisfying_DN_1 (non empty ComplLattStr);
      let x, y be Element of L;
      ((x + y`)`` + y)` = (y` + y)` by Th34;
      hence thesis by Th23;
    end;

theorem Th36: :: A98
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    ((((x + y`) + z)` + y)` + (y` + y)`)` = y
    proof
      let L be satisfying_DN_1 (non empty ComplLattStr);
      let x, y, z be Element of L;
      ((x + y`) + y)` = (y` + y)` by Th35;
      hence thesis by Th9;
    end;

theorem Th37: :: A99
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    x + ((y + z)` + (y + x)`)` = y + x
    proof
      let L be satisfying_DN_1 (non empty ComplLattStr);
      let x, y, z be Element of L;
      x + ((y + z)` + (y + x)`)` = (y + x )`` by Th26;
      hence thesis by Th23;
    end;

theorem Th38: :: A100
  for L being satisfying_DN_1 (non empty ComplLattStr),
      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 ComplLattStr);
      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 :: A101
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    x + ((y + x)` + (y + z)`)` = y + x by Th37;

theorem Th40: :: A102
  for L being satisfying_DN_1 (non empty ComplLattStr),
      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 ComplLattStr);
      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: :: A103
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    (((x + y`) + z)` + y)`` = y
    proof
      let L be satisfying_DN_1 (non empty ComplLattStr);
      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: :: A104
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    x + ((y + x`) + z)` = x
    proof
      let L be satisfying_DN_1 (non empty ComplLattStr);
      let x, y, z be Element of L;
      (((y + x`) + z)` + x)`` = x by Th41;
      hence thesis by Th25;
    end;

theorem Th43: :: A105
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    x` + ((y + x) + z)` = x`
    proof
      let L be satisfying_DN_1 (non empty ComplLattStr);
      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: :: A107
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    (x + y)` + x = x + y`
    proof
      let L be satisfying_DN_1 (non empty ComplLattStr);
      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: :: A108
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y being Element of L holds
    (x + (x + y`)`)` = (x + y)`
    proof
      let L be satisfying_DN_1 (non empty ComplLattStr);
      let x, y be Element of L;
      (x + ((x + y)` + x)`)` = (x + y)` by Th8;
      hence thesis by Th44;
    end;

theorem Th46: :: A109
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    ((x + y)` + (x + z))` + y = y
    proof
      let L be satisfying_DN_1 (non empty ComplLattStr);
      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: :: A110
  for L being satisfying_DN_1 (non empty ComplLattStr),
      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 ComplLattStr);
      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: :: A111
  for L being satisfying_DN_1 (non empty ComplLattStr),
      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 ComplLattStr);
      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: :: A112
  for L being satisfying_DN_1 (non empty ComplLattStr),
      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 ComplLattStr);
      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: :: A113
  for L being satisfying_DN_1 (non empty ComplLattStr),
      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 ComplLattStr);
      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: :: A114
  for L being satisfying_DN_1 (non empty ComplLattStr),
      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 ComplLattStr);
      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: :: A115
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    x`` + (y + z) = (y + x) + (y + z)
    proof
      let L be satisfying_DN_1 (non empty ComplLattStr);
      let x, y, z be Element of L;
      x` + ((y + x) + (y + z))` = x` by Th43;
      hence thesis by Th51;
    end;

theorem Th53: :: A117
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    (x + y) + (x + z) = y + (x + z)
    proof
      let L be satisfying_DN_1 (non empty ComplLattStr);
      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 :: A118
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    (x + y) + (x + z) = z + (x + y) by Th53;

theorem Th55: :: A119
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    x + (y + z) = z + (y + x)
    proof
      let L be satisfying_DN_1 (non empty ComplLattStr);
      let x, y, z be Element of L;
      (y + x) + (y + z) = z + (y + x) by Th53;
      hence thesis by Th53;
    end;

theorem :: A120
  for L being satisfying_DN_1 (non empty ComplLattStr),
      x, y, z being Element of L holds
    x + (y + z) = y + (z + x) by Th55;

theorem :: A121
  for L being satisfying_DN_1 (non empty ComplLattStr),
      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 ComplLattStr) 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 L is Robbins by ROBBINS1:def 5;
    end;

definition
  cluster satisfying_DN_1 -> join-associative (non empty ComplLattStr);
  coherence by Lm2;
  cluster satisfying_DN_1 -> Robbins (non empty ComplLattStr);
  coherence by Lm3;
end;

theorem Th58:
  for L being non empty ComplLattStr,
      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 ComplLattStr;
     let x, z be Element of L;
     assume L is join-commutative join-associative Huntington;
     then reconsider L' = L as join-commutative join-associative Huntington
       (non empty ComplLattStr);
     reconsider z' = z, x' = x as Element of L';
     (z' + x') *' (z' + x'`) = z' + (x' *' x'`) by ROBBINS1:32
        .= z' + Bot L' by ROBBINS1:16
        .= z' by ROBBINS1:14;
     hence thesis;
   end;

theorem Th59:
  for L being non empty ComplLattStr st
    L is join-commutative join-associative Robbins holds
      L is satisfying_DN_1
  proof
    let L be non empty ComplLattStr;
    assume
A1: L is join-commutative join-associative Robbins; then
    reconsider L' = L as join-commutative join-associative Robbins
      (non empty ComplLattStr);
A2: L' is Huntington;
    let x, y, z, u be Element of L;
A3: ((x + y)` + z) *' z = (z + (x + y)`) *' z by A1,LATTICES:def 4
       .= z *' (z + (x + y)`) by A1,ROBBINS1:8
       .= z by A2,ROBBINS1:22;
A4: (z + x) *' (z + x`) = z by A2,Th58;
A5: (((x + y)` + z) *' x) + z = z + (((x + y)` + z) *' x)
       by A1,LATTICES:def 4
       .= (z + ((x + y)` + z)) *' (z + x) by A2,ROBBINS1:32
       .= (((x + y)` + z) + z) *' (z + x) by A2,LATTICES:def 4
       .= ((x + y)` + (z + z)) *' (z + x) by A2,LATTICES:def 5
       .= ((x + y)` + z) *' (z + x) by A2,ROBBINS1:13
       .= ((x` *' y`)`` + z) *' (z + x) by A2,ROBBINS1:18
       .= ((x` *' y`) + z) *' (z + x) by A2,ROBBINS1:3
       .= (z + (x` *' y`)) *' (z + x) by A2,LATTICES:def 4
       .= ((z + x`) *' (z + y`)) *' (z + x) by A2,ROBBINS1:32
       .= (z + x) *' ((z + x`) *' (z + y`)) by A2,ROBBINS1:8
       .= (z + x) *' ((x` + z) *' (z + y`)) by A2,LATTICES:def 4
       .= (z + x) *' ((x` + z) *' (y` + z)) by A2,LATTICES:def 4
       .= (z + x) *' (x` + z) *' (y` + z) by A2,ROBBINS1:17
       .= (z + x) *' (z + x`) *' (y` + z) by A2,LATTICES:def 4
       .= z *' (z + y`) by A2,A4,LATTICES:def 4
       .= z by A2,ROBBINS1:22;
    (((x + y)` + z)` + (x + (z` + (z + u)`)`)`)` =
      (((x + y)` + z)`` *' (x + (z` + (z + u)`)`)``)``
        by A2,ROBBINS1:18
      .= ((x + y)` + z)`` *' (x + (z` + (z + u)`)`)`` by A2,ROBBINS1:3
      .= ((x + y)` + z)`` *' (x + (z` + (z + u)`)`) by A2,ROBBINS1:3
      .= ((x + y)` + z) *' (x + (z` + (z + u)`)`) by A2,ROBBINS1:3
      .= ((x + y)`` *' z`)` *' (x + (z` + (z + u)`)`) by A2,ROBBINS1:18
      .= ((x + y) *' z`)` *' (x + (z` + (z + u)`)`) by A2,ROBBINS1:3
      .= ((x + y) *' z`)` *' (x + (z`` *' (z + u)``)``)
           by A2,ROBBINS1:18
      .= ((x + y) *' z`)` *' (x + (z *' (z + u)``)``)
           by A2,ROBBINS1:3
      .= ((x + y) *' z`)` *' (x + (z *' (z + u)``)) by A2,ROBBINS1:3
      .= ((x + y) *' z`)` *' (x + (z *' (z + u))) by A2,ROBBINS1:3
      .= ((x + y) *' z`)` *' (x + z) by A2,ROBBINS1:22
      .= (((x + y) *' z`)` *' x) + (((x + y) *' z`)` *' z)
           by A2,ROBBINS1:31
      .= (((x + y)`` *' z`)` *' x) + (((x + y) *' z`)` *' z)
           by A2,ROBBINS1:3
      .= (((x + y)` + z) *' x) + (((x + y) *' z`)` *' z)
           by A2,ROBBINS1:18
      .= (((x + y)` + z) *' x) + (((x + y)`` *' z`)` *' z)
           by A2,ROBBINS1:3
      .= z by A2,A3,A5,ROBBINS1:18;
    hence thesis;
  end;

definition
  cluster join-commutative join-associative Robbins -> satisfying_DN_1
      (non empty ComplLattStr);
  coherence by Th59;
end;

definition
  cluster satisfying_DN_1 de_Morgan preOrthoLattice;
  existence
  proof
    take TrivOrtLat;
    thus thesis;
  end;
end;

definition
  cluster satisfying_DN_1 de_Morgan -> Boolean preOrthoLattice;
  coherence
  proof
    let L be preOrthoLattice;
    assume L is satisfying_DN_1 de_Morgan; then
    reconsider L' = L as satisfying_DN_1 de_Morgan preOrthoLattice;
    L' is Boolean;
    hence thesis;
  end;
  cluster Boolean -> satisfying_DN_1 (well-complemented preOrthoLattice);
  coherence
  proof
    let L be well-complemented preOrthoLattice;
    assume
A1: L is Boolean;
    reconsider L' = L as Boolean well-complemented preOrthoLattice by A1;
    L' is satisfying_DN_1;
    hence thesis;
  end;
end;

begin :: Meredith Two Axioms for Boolean Algebras

definition let L be non empty ComplLattStr;
  attr L is satisfying_MD_1 means :Def2:
    for x, y being Element of L holds
      (x` + y)` + x = x;
  attr L is satisfying_MD_2 means :Def3:
    for x, y, z being Element of L holds
      (x` + y)` + (z + y) = y + (z + x);
end;

Lm4: now
  let L be non empty ComplLattStr;
  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,Def2;
       hence thesis by A1,Def2;
     end;

A3:  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,Def3
         .= z + (x` + y) by A2;
       hence thesis;
     end;

A4: 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,Def3
              .= y + x by A1,Def2;
       hence thesis;
     end;

A5: 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,Def3
                          .= y + x by A1,Def2;
       hence thesis;
     end;

A6: 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;
A7:    X` + (X` + y) = y + (X` + x) by A1,Def3;
       (x` + y)` + y = X` + (X` + y) by A2
                    .= y + x by A1,A7,Def2;
       hence thesis;
     end;

A8: 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,Def3
           .= y + x by A1,Def2;
       hence thesis;
     end;

A9: 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 A3
            .= y` + x by A1,Def2;
       hence thesis;
     end;

A10: for x being Element of L holds
       x + x = x
     proof
       let x be Element of L;
       x + x = (x` + x)` + x by A6
            .= x by A1,Def2;
       hence thesis;
     end;

A11: 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,Def3
            .= (y` + x)` + x by A10
            .= x + y by A6;
        hence thesis;
      end;

A12: 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 A6
                   .= (y` + (x + y))` + (x + (x + y)) by A11
                   .= Y + (x + y) by A1,Def3
                   .= x + y by A10;
        hence thesis;
      end;

A13:
   for x being Element of L holds
     x`` + x = x
   proof
     let x be Element of L;
     (x` + x`)` + x = x by A1,Def2;
     hence thesis by A10;
   end;

A14:
   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 A11
                .= y + x by A8;
     hence thesis;
   end;

A15:
   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,Def3
                  .= (y` + x)` + x by A13
                  .= x + y by A6;
     hence thesis;
   end;

A16:
   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 A6
                .= (y` + x)` + x by A12
                .= x + y by A6;
     hence thesis;
   end;

A17:
   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 A6
                .= (z` + Y)` + (y + Y) by A14
                .= Y + (y + z) by A1,Def3;
     hence thesis;
   end;

A18:
   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 A14
                  .= y by A1,Def2;
     hence thesis;
   end;

A19:
   for x being Element of L holds
     x + x`` = x
   proof
     let x be Element of L;
     x + x`` = (x`` + x) + x`` by A13
            .= x`` + x by A16
            .= x by A13;
     hence thesis;
   end;

A20:
   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,Def2
                  .= (x` + y)` + x by A16
                  .= x by A1,Def2;
     hence thesis;
   end;

A21:
   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 A18
                  .= (y + x`)` + x by A16
                  .= x by A18;
     hence thesis;
   end;

A22:
   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 A6
       .= (x` + ((y` + x)` + x)`)` + (y` + ((y` + x)` + x)`) by A6
       .= y` + x by A5;
     hence thesis;
   end;

A23: 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 A9
             .= (Y` + x)` + x by A6
             .= (x + y)` + x by A6;
       hence thesis;
     end;

A24:
    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 A6
          .= x` + (y` + x)` by A23;
       hence thesis;
    end;

A25:
    for x being Element of L holds
      x + x```` = x
    proof
       let x be Element of L;
       x + x```` = x + (x`` + x````) by A15
                .= x + x`` by A19
                .= x by A19;
       hence thesis;
    end;

A26:
    for x being Element of L holds
      x``` = x`
    proof
      let x be Element of L;
      x``` = (x + x````)` + x``` by A18
          .= x` + x``` by A25
          .= x` by A19;
      hence thesis;
    end;

A27:
    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 A4
        .= (y` + x)` + ((y``` + x)` + x) by A26
        .= (y``` + x)` + ((y``` + x)` + x) by A26
        .= x + y`` by A4;
      hence thesis;
    end;

A28:
    for x being Element of L holds
      x`` = x
    proof
      let x be Element of L;
      x`` = (x``` + x``)` + x`` by A1,Def2
         .= (x` + x``)` + x`` by A26
         .= (x` + x``)` + x by A27
         .= x by A1,Def2;
      hence thesis;
    end;

A29:
    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 A21
        .= x` + (y + x)` by A28;
      hence thesis;
    end;

A30:
    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 A20
        .= x` + (x + y)` by A28;
      hence thesis;
    end;

A31:
    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 A22
            .= x`` + (y` + (x + y)`) by A30
            .= x`` + y` by A29
            .= x + y` by A28;
      hence thesis;
    end;

A32:
    for x, y being Element of L holds
      x + y = y + x
    proof
      let x, y be Element of L;
      y`` = y by A28;
      hence thesis by A31;
    end;
    hence L is join-commutative by LATTICES:def 4;

    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 A32
           .= (x` + y)` + (y` + x`)` by A32
           .= x`` + (y` + x`)` by A24
           .= x + (y` + x`)` by A28
           .= x by A21;
      hence thesis;
    end;
    hence L is Huntington by ROBBINS1:def 6;

    for x, y, z being Element of L holds
      (x + y) + z = x + (y + z)
    proof
      let x, y, z be Element of L;
A33: 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 A32
                         .= (z + x) + y by A17
                         .= (x + z) + y by A32
                         .= y + (x + z) by A32;
        hence thesis;
      end;
      (y + x) + (z + y) = x + (y + z) by A33; then
A34:    (x + y) + (z + y) = x + (y + z) by A32;
      (x + y) + z = (x + y) + (y + z) by A17
                 .= x + (y + z) by A32,A34;
      hence thesis;
    end;
    hence L is join-associative by LATTICES:def 5;
  end;

definition
  cluster satisfying_MD_1 satisfying_MD_2 ->
     join-commutative join-associative Huntington (non empty ComplLattStr);
  coherence by Lm4;
  cluster join-commutative join-associative Huntington ->
     satisfying_MD_1 satisfying_MD_2 (non empty ComplLattStr);
  coherence
  proof
    let L be non empty ComplLattStr;
    assume L is join-commutative join-associative Huntington; then
    reconsider L' = L as join-commutative join-associative Huntington
      (non empty ComplLattStr);
A1: L' is satisfying_MD_1
    proof
      let x, y be Element of L';
      (x` + y)` + x = (x` + y``)` + x by ROBBINS1:3
                   .= (x *' y`) + x by ROBBINS1:def 4
                   .= x by ROBBINS1:21;
      hence thesis;
    end;
    L' is satisfying_MD_2
    proof
      let x, y, z be Element of L';
      set Z = z + y;
      consider k being Element of L' such that
A2:   k + k` = Top L' by ROBBINS1:def 8;
A3:   Z + y` = z + (y + y`) by LATTICES:def 5
            .= z + Top L' by A2,ROBBINS1:4
            .= Top L' by ROBBINS1:20;
      (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:32
                         .= Z + x by A3,ROBBINS1:15
                         .= y + (z + x) by LATTICES:def 5;
      hence thesis;
    end;
    hence thesis by A1;
  end;
end;

definition
  cluster satisfying_MD_1 satisfying_MD_2 satisfying_DN_1 de_Morgan
    preOrthoLattice;
  existence
  proof
    take TrivOrtLat;
    thus thesis;
  end;
end;

definition
  cluster satisfying_MD_1 satisfying_MD_2 de_Morgan ->
    Boolean preOrthoLattice;
  coherence
  proof
    let L be preOrthoLattice;
    assume L is satisfying_MD_1 satisfying_MD_2 de_Morgan; then
    reconsider L' = L as satisfying_MD_1 satisfying_MD_2 de_Morgan
      preOrthoLattice;
    L' is Boolean;
    hence thesis;
  end;
  cluster Boolean -> satisfying_MD_1 satisfying_MD_2 (well-complemented
    preOrthoLattice);
  coherence
  proof
    let L be well-complemented preOrthoLattice;
    assume
A1: L is Boolean;
    reconsider L' = L as Boolean well-complemented preOrthoLattice by A1;
    L' is satisfying_MD_1 satisfying_MD_2;
    hence thesis;
  end;
end;

Back to top