let L be LATTICE; ( L is modular iff for a, b, c, d, e being Element of L holds
( not a,b,c,d,e are_mutually_distinct or not a "/\" b = a or not a "/\" c = a or not c "/\" e = c or not d "/\" e = d or not b "/\" c = a or not b "/\" d = b or not c "/\" d = a or not b "\/" c = e or not c "\/" d = e ) )
now ( ex a, b, c, d, e being Element of L st
( b <> d & a "/\" b = a & d "/\" e = d & b "/\" d = b & c "/\" d = a & b "\/" c = e ) implies not L is modular )given a,
b,
c,
d,
e being
Element of
L such that A1:
b <> d
and A2:
a "/\" b = a
and A3:
d "/\" e = d
and A4:
b "/\" d = b
and A5:
c "/\" d = a
and A6:
b "\/" c = e
;
not L is modular A7:
b <= d
by A4, YELLOW_0:23;
b "\/" (c "/\" d) = b
by A2, A5, Th5;
hence
not
L is
modular
by A1, A3, A6, A7;
verum end;
hence
( L is modular implies for a, b, c, d, e being Element of L holds
( not a,b,c,d,e are_mutually_distinct or not a "/\" b = a or not a "/\" c = a or not c "/\" e = c or not d "/\" e = d or not b "/\" c = a or not b "/\" d = b or not c "/\" d = a or not b "\/" c = e or not c "\/" d = e ) )
; ( ( for a, b, c, d, e being Element of L holds
( not a,b,c,d,e are_mutually_distinct or not a "/\" b = a or not a "/\" c = a or not c "/\" e = c or not d "/\" e = d or not b "/\" c = a or not b "/\" d = b or not c "/\" d = a or not b "\/" c = e or not c "\/" d = e ) ) implies L is modular )
now ( not L is modular implies ex a, b, c, d, e being Element of L st
( a,b,c,d,e are_mutually_distinct & a "/\" b = a & a "/\" c = a & c "/\" e = c & d "/\" e = d & b "/\" c = a & b "/\" d = b & c "/\" d = a & b "\/" c = e & c "\/" d = e ) )assume
not
L is
modular
;
ex a, b, c, d, e being Element of L st
( a,b,c,d,e are_mutually_distinct & a "/\" b = a & a "/\" c = a & c "/\" e = c & d "/\" e = d & b "/\" c = a & b "/\" d = b & c "/\" d = a & b "\/" c = e & c "\/" d = e )then consider x,
y,
z being
Element of
L such that A8:
x <= z
and A9:
x "\/" (y "/\" z) <> (x "\/" y) "/\" z
;
x "\/" (y "/\" z) <= z "\/" (y "/\" z)
by A8, YELLOW_5:7;
then A10:
x "\/" (y "/\" z) <= z
by LATTICE3:17;
set z1 =
(x "\/" y) "/\" z;
set y1 =
y;
x "\/" y <= x "\/" y
;
then
(x "\/" y) "/\" x <= (x "\/" y) "/\" z
by A8, YELLOW_3:2;
then
x <= (x "\/" y) "/\" z
by LATTICE3:18;
then A11:
x "\/" y <= ((x "\/" y) "/\" z) "\/" y
by YELLOW_5:7;
set x1 =
x "\/" (y "/\" z);
A12:
y "/\" z <= y
by YELLOW_0:23;
y <= y
;
then A13:
(x "\/" (y "/\" z)) "/\" y <= y "/\" z
by A10, YELLOW_3:2;
set t =
x "\/" y;
set b =
y "/\" z;
y "/\" z <= x "\/" (y "/\" z)
by YELLOW_0:22;
then
(y "/\" z) "/\" (y "/\" z) <= (x "\/" (y "/\" z)) "/\" y
by A12, YELLOW_3:2;
then A16:
y "/\" z <= (x "\/" (y "/\" z)) "/\" y
by YELLOW_5:2;
A17:
(x "\/" y) "/\" z <= x "\/" y
by YELLOW_0:23;
thus
ex
a,
b,
c,
d,
e being
Element of
L st
(
a,
b,
c,
d,
e are_mutually_distinct &
a "/\" b = a &
a "/\" c = a &
c "/\" e = c &
d "/\" e = d &
b "/\" c = a &
b "/\" d = b &
c "/\" d = a &
b "\/" c = e &
c "\/" d = e )
verumproof
take
y "/\" z
;
ex b, c, d, e being Element of L st
( y "/\" z,b,c,d,e are_mutually_distinct & (y "/\" z) "/\" b = y "/\" z & (y "/\" z) "/\" c = y "/\" z & c "/\" e = c & d "/\" e = d & b "/\" c = y "/\" z & b "/\" d = b & c "/\" d = y "/\" z & b "\/" c = e & c "\/" d = e )
take
x "\/" (y "/\" z)
;
ex c, d, e being Element of L st
( y "/\" z,x "\/" (y "/\" z),c,d,e are_mutually_distinct & (y "/\" z) "/\" (x "\/" (y "/\" z)) = y "/\" z & (y "/\" z) "/\" c = y "/\" z & c "/\" e = c & d "/\" e = d & (x "\/" (y "/\" z)) "/\" c = y "/\" z & (x "\/" (y "/\" z)) "/\" d = x "\/" (y "/\" z) & c "/\" d = y "/\" z & (x "\/" (y "/\" z)) "\/" c = e & c "\/" d = e )
take
y
;
ex d, e being Element of L st
( y "/\" z,x "\/" (y "/\" z),y,d,e are_mutually_distinct & (y "/\" z) "/\" (x "\/" (y "/\" z)) = y "/\" z & (y "/\" z) "/\" y = y "/\" z & y "/\" e = y & d "/\" e = d & (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" d = x "\/" (y "/\" z) & y "/\" d = y "/\" z & (x "\/" (y "/\" z)) "\/" y = e & y "\/" d = e )
take
(x "\/" y) "/\" z
;
ex e being Element of L st
( y "/\" z,x "\/" (y "/\" z),y,(x "\/" y) "/\" z,e are_mutually_distinct & (y "/\" z) "/\" (x "\/" (y "/\" z)) = y "/\" z & (y "/\" z) "/\" y = y "/\" z & y "/\" e = y & ((x "\/" y) "/\" z) "/\" e = (x "\/" y) "/\" z & (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = e & y "\/" ((x "\/" y) "/\" z) = e )
take
x "\/" y
;
( y "/\" z,x "\/" (y "/\" z),y,(x "\/" y) "/\" z,x "\/" y are_mutually_distinct & (y "/\" z) "/\" (x "\/" (y "/\" z)) = y "/\" z & (y "/\" z) "/\" y = y "/\" z & y "/\" (x "\/" y) = y & ((x "\/" y) "/\" z) "/\" (x "\/" y) = (x "\/" y) "/\" z & (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )
A18:
y <= x "\/" y
by YELLOW_0:22;
hence
y "/\" z <> x "\/" (y "/\" z)
;
ZFMISC_1:def 7 ( not y "/\" z = y & not y "/\" z = (x "\/" y) "/\" z & not y "/\" z = x "\/" y & not x "\/" (y "/\" z) = y & not x "\/" (y "/\" z) = (x "\/" y) "/\" z & not x "\/" (y "/\" z) = x "\/" y & not y = (x "\/" y) "/\" z & not y = x "\/" y & not (x "\/" y) "/\" z = x "\/" y & (y "/\" z) "/\" (x "\/" (y "/\" z)) = y "/\" z & (y "/\" z) "/\" y = y "/\" z & y "/\" (x "\/" y) = y & ((x "\/" y) "/\" z) "/\" (x "\/" y) = (x "\/" y) "/\" z & (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )
hence
y "/\" z <> y
;
( not y "/\" z = (x "\/" y) "/\" z & not y "/\" z = x "\/" y & not x "\/" (y "/\" z) = y & not x "\/" (y "/\" z) = (x "\/" y) "/\" z & not x "\/" (y "/\" z) = x "\/" y & not y = (x "\/" y) "/\" z & not y = x "\/" y & not (x "\/" y) "/\" z = x "\/" y & (y "/\" z) "/\" (x "\/" (y "/\" z)) = y "/\" z & (y "/\" z) "/\" y = y "/\" z & y "/\" (x "\/" y) = y & ((x "\/" y) "/\" z) "/\" (x "\/" y) = (x "\/" y) "/\" z & (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )
hence
y "/\" z <> (x "\/" y) "/\" z
;
( not y "/\" z = x "\/" y & not x "\/" (y "/\" z) = y & not x "\/" (y "/\" z) = (x "\/" y) "/\" z & not x "\/" (y "/\" z) = x "\/" y & not y = (x "\/" y) "/\" z & not y = x "\/" y & not (x "\/" y) "/\" z = x "\/" y & (y "/\" z) "/\" (x "\/" (y "/\" z)) = y "/\" z & (y "/\" z) "/\" y = y "/\" z & y "/\" (x "\/" y) = y & ((x "\/" y) "/\" z) "/\" (x "\/" y) = (x "\/" y) "/\" z & (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )
thus
y "/\" z <> x "\/" y
by A14;
( not x "\/" (y "/\" z) = y & not x "\/" (y "/\" z) = (x "\/" y) "/\" z & not x "\/" (y "/\" z) = x "\/" y & not y = (x "\/" y) "/\" z & not y = x "\/" y & not (x "\/" y) "/\" z = x "\/" y & (y "/\" z) "/\" (x "\/" (y "/\" z)) = y "/\" z & (y "/\" z) "/\" y = y "/\" z & y "/\" (x "\/" y) = y & ((x "\/" y) "/\" z) "/\" (x "\/" y) = (x "\/" y) "/\" z & (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )
hence
x "\/" (y "/\" z) <> y
;
( not x "\/" (y "/\" z) = (x "\/" y) "/\" z & not x "\/" (y "/\" z) = x "\/" y & not y = (x "\/" y) "/\" z & not y = x "\/" y & not (x "\/" y) "/\" z = x "\/" y & (y "/\" z) "/\" (x "\/" (y "/\" z)) = y "/\" z & (y "/\" z) "/\" y = y "/\" z & y "/\" (x "\/" y) = y & ((x "\/" y) "/\" z) "/\" (x "\/" y) = (x "\/" y) "/\" z & (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )
thus
x "\/" (y "/\" z) <> (x "\/" y) "/\" z
by A9;
( not x "\/" (y "/\" z) = x "\/" y & not y = (x "\/" y) "/\" z & not y = x "\/" y & not (x "\/" y) "/\" z = x "\/" y & (y "/\" z) "/\" (x "\/" (y "/\" z)) = y "/\" z & (y "/\" z) "/\" y = y "/\" z & y "/\" (x "\/" y) = y & ((x "\/" y) "/\" z) "/\" (x "\/" y) = (x "\/" y) "/\" z & (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )
hence
x "\/" (y "/\" z) <> x "\/" y
;
( not y = (x "\/" y) "/\" z & not y = x "\/" y & not (x "\/" y) "/\" z = x "\/" y & (y "/\" z) "/\" (x "\/" (y "/\" z)) = y "/\" z & (y "/\" z) "/\" y = y "/\" z & y "/\" (x "\/" y) = y & ((x "\/" y) "/\" z) "/\" (x "\/" y) = (x "\/" y) "/\" z & (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )
hence
y <> (x "\/" y) "/\" z
;
( not y = x "\/" y & not (x "\/" y) "/\" z = x "\/" y & (y "/\" z) "/\" (x "\/" (y "/\" z)) = y "/\" z & (y "/\" z) "/\" y = y "/\" z & y "/\" (x "\/" y) = y & ((x "\/" y) "/\" z) "/\" (x "\/" y) = (x "\/" y) "/\" z & (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )
hence
y <> x "\/" y
;
( not (x "\/" y) "/\" z = x "\/" y & (y "/\" z) "/\" (x "\/" (y "/\" z)) = y "/\" z & (y "/\" z) "/\" y = y "/\" z & y "/\" (x "\/" y) = y & ((x "\/" y) "/\" z) "/\" (x "\/" y) = (x "\/" y) "/\" z & (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )
hence
(x "\/" y) "/\" z <> x "\/" y
;
( (y "/\" z) "/\" (x "\/" (y "/\" z)) = y "/\" z & (y "/\" z) "/\" y = y "/\" z & y "/\" (x "\/" y) = y & ((x "\/" y) "/\" z) "/\" (x "\/" y) = (x "\/" y) "/\" z & (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )
y "/\" z <= x "\/" (y "/\" z)
by YELLOW_0:22;
hence
(y "/\" z) "/\" (x "\/" (y "/\" z)) = y "/\" z
by YELLOW_5:10;
( (y "/\" z) "/\" y = y "/\" z & y "/\" (x "\/" y) = y & ((x "\/" y) "/\" z) "/\" (x "\/" y) = (x "\/" y) "/\" z & (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )
y "/\" z <= y
by YELLOW_0:23;
hence
(y "/\" z) "/\" y = y "/\" z
by YELLOW_5:10;
( y "/\" (x "\/" y) = y & ((x "\/" y) "/\" z) "/\" (x "\/" y) = (x "\/" y) "/\" z & (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )
y <= x "\/" y
by YELLOW_0:22;
hence
y "/\" (x "\/" y) = y
by YELLOW_5:10;
( ((x "\/" y) "/\" z) "/\" (x "\/" y) = (x "\/" y) "/\" z & (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )
(x "\/" y) "/\" z <= x "\/" y
by YELLOW_0:23;
hence
((x "\/" y) "/\" z) "/\" (x "\/" y) = (x "\/" y) "/\" z
by YELLOW_5:10;
( (x "\/" (y "/\" z)) "/\" y = y "/\" z & (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )
thus
(x "\/" (y "/\" z)) "/\" y = y "/\" z
by A16, A13, YELLOW_0:def 3;
( (x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) & y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )
thus
(x "\/" (y "/\" z)) "/\" ((x "\/" y) "/\" z) = x "\/" (y "/\" z)
by A8, Th8, YELLOW_5:10;
( y "/\" ((x "\/" y) "/\" z) = y "/\" z & (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )
thus y "/\" ((x "\/" y) "/\" z) =
(y "/\" (x "\/" y)) "/\" z
by LATTICE3:16
.=
y "/\" z
by LATTICE3:18
;
( (x "\/" (y "/\" z)) "\/" y = x "\/" y & y "\/" ((x "\/" y) "/\" z) = x "\/" y )
thus (x "\/" (y "/\" z)) "\/" y =
x "\/" ((y "/\" z) "\/" y)
by LATTICE3:14
.=
x "\/" y
by LATTICE3:17
;
y "\/" ((x "\/" y) "/\" z) = x "\/" y
x "\/" y <= x "\/" y
;
then
(x "\/" y) "/\" x <= (x "\/" y) "/\" z
by A8, YELLOW_3:2;
then
x <= (x "\/" y) "/\" z
by LATTICE3:18;
then A33:
x "\/" y <= ((x "\/" y) "/\" z) "\/" y
by YELLOW_5:7;
(x "\/" y) "/\" z <= x "\/" y
by YELLOW_0:23;
then
y "\/" ((x "\/" y) "/\" z) <= x "\/" y
by A18, YELLOW_5:9;
hence
y "\/" ((x "\/" y) "/\" z) = x "\/" y
by A33, YELLOW_0:def 3;
verum
end; end;
hence
( ( for a, b, c, d, e being Element of L holds
( not a,b,c,d,e are_mutually_distinct or not a "/\" b = a or not a "/\" c = a or not c "/\" e = c or not d "/\" e = d or not b "/\" c = a or not b "/\" d = b or not c "/\" d = a or not b "\/" c = e or not c "\/" d = e ) ) implies L is modular )
; verum