:: On the Characterization of Modular and Distributive Lattices
::
:: Copyright (c) 1998-2019 Association of Mizar Users

:: Preliminaries
theorem :: YELLOW11:1
3 = {0,1,2} by CARD_1:51;

theorem Th2: :: YELLOW11:2
2 \ 1 = {1}
proof end;

theorem Th3: :: YELLOW11:3
3 \ 1 = {1,2}
proof end;

theorem Th4: :: YELLOW11:4
3 \ 2 = {2}
proof end;

Lm1: 3 \ 2 c= 3 \ 1
proof end;

theorem Th5: :: YELLOW11:5
for L being reflexive antisymmetric with_suprema with_infima RelStr
for a, b being Element of L holds
( a "/\" b = b iff a "\/" b = a )
proof end;

theorem Th6: :: YELLOW11:6
for L being LATTICE
for a, b, c being Element of L holds (a "/\" b) "\/" (a "/\" c) <= a "/\" (b "\/" c)
proof end;

theorem Th7: :: YELLOW11:7
for L being LATTICE
for a, b, c being Element of L holds a "\/" (b "/\" c) <= (a "\/" b) "/\" (a "\/" c)
proof end;

theorem Th8: :: YELLOW11:8
for L being LATTICE
for a, b, c being Element of L st a <= c holds
a "\/" (b "/\" c) <= (a "\/" b) "/\" c
proof end;

definition
func N_5 -> RelStr equals :: YELLOW11:def 1
InclPoset {0,(3 \ 1),2,(3 \ 2),3};
correctness
coherence
InclPoset {0,(3 \ 1),2,(3 \ 2),3} is RelStr
;
;
end;

:: deftheorem defines N_5 YELLOW11:def 1 :
N_5 = InclPoset {0,(3 \ 1),2,(3 \ 2),3};

registration
correctness
coherence
( N_5 is strict & N_5 is reflexive & N_5 is transitive & N_5 is antisymmetric )
;
;
correctness
coherence ;
proof end;
end;

definition
func M_3 -> RelStr equals :: YELLOW11:def 2
InclPoset {0,1,(2 \ 1),(3 \ 2),3};
correctness
coherence
InclPoset {0,1,(2 \ 1),(3 \ 2),3} is RelStr
;
;
end;

:: deftheorem defines M_3 YELLOW11:def 2 :
M_3 = InclPoset {0,1,(2 \ 1),(3 \ 2),3};

registration
correctness
coherence
( M_3 is strict & M_3 is reflexive & M_3 is transitive & M_3 is antisymmetric )
;
;
correctness
coherence ;
proof end;
end;

theorem Th9: :: YELLOW11:9
for L being LATTICE holds
( ex K being full Sublattice of L st N_5 ,K are_isomorphic iff 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 ) )
proof end;

theorem Th10: :: YELLOW11:10
for L being LATTICE holds
( ex K being full Sublattice of L st M_3 ,K are_isomorphic iff 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 & a "/\" d = a & b "/\" e = b & c "/\" e = c & d "/\" e = d & b "/\" c = a & b "/\" d = a & c "/\" d = a & b "\/" c = e & b "\/" d = e & c "\/" d = e ) )
proof end;

definition
let L be non empty RelStr ;
attr L is modular means :: YELLOW11:def 3
for a, b, c being Element of L st a <= c holds
a "\/" (b "/\" c) = (a "\/" b) "/\" c;
end;

:: deftheorem defines modular YELLOW11:def 3 :
for L being non empty RelStr holds
( L is modular iff for a, b, c being Element of L st a <= c holds
a "\/" (b "/\" c) = (a "\/" b) "/\" c );

registration
coherence
for b1 being non empty reflexive antisymmetric with_infima RelStr st b1 is distributive holds
b1 is modular
proof end;
end;

Lm2: for L being LATTICE holds
( 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 ) )

proof end;

theorem :: YELLOW11:11
for L being LATTICE holds
( L is modular iff for K being full Sublattice of L holds not N_5 ,K are_isomorphic )
proof end;

Lm3: for L being LATTICE st L is modular holds
( L is distributive 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 a "/\" d = a or not b "/\" e = b or not c "/\" e = c or not d "/\" e = d or not b "/\" c = a or not b "/\" d = a or not c "/\" d = a or not b "\/" c = e or not b "\/" d = e or not c "\/" d = e ) )

proof end;

theorem :: YELLOW11:12
for L being LATTICE st L is modular holds
( L is distributive iff for K being full Sublattice of L holds not M_3 ,K are_isomorphic )
proof end;

definition
let L be non empty RelStr ;
let a, b be Element of L;
func [#a,b#] -> Subset of L means :Def4: :: YELLOW11:def 4
for c being Element of L holds
( c in it iff ( a <= c & c <= b ) );
existence
ex b1 being Subset of L st
for c being Element of L holds
( c in b1 iff ( a <= c & c <= b ) )
proof end;
uniqueness
for b1, b2 being Subset of L st ( for c being Element of L holds
( c in b1 iff ( a <= c & c <= b ) ) ) & ( for c being Element of L holds
( c in b2 iff ( a <= c & c <= b ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines [# YELLOW11:def 4 :
for L being non empty RelStr
for a, b being Element of L
for b4 being Subset of L holds
( b4 = [#a,b#] iff for c being Element of L holds
( c in b4 iff ( a <= c & c <= b ) ) );

definition
let L be non empty RelStr ;
let IT be Subset of L;
attr IT is interval means :: YELLOW11:def 5
ex a, b being Element of L st IT = [#a,b#];
end;

:: deftheorem defines interval YELLOW11:def 5 :
for L being non empty RelStr
for IT being Subset of L holds
( IT is interval iff ex a, b being Element of L st IT = [#a,b#] );

registration
let L be non empty reflexive transitive RelStr ;
cluster non empty interval -> directed for Element of bool the carrier of L;
coherence
for b1 being Subset of L st not b1 is empty & b1 is interval holds
b1 is directed
proof end;
cluster non empty interval -> filtered for Element of bool the carrier of L;
coherence
for b1 being Subset of L st not b1 is empty & b1 is interval holds
b1 is filtered
proof end;
end;

registration
let L be non empty RelStr ;
let a, b be Element of L;
cluster [#a,b#] -> interval ;
coherence
[#a,b#] is interval
;
end;

theorem :: YELLOW11:13
for L being non empty reflexive transitive RelStr
for a, b being Element of L holds [#a,b#] = () /\ ()
proof end;

registration
let L be with_infima Poset;
let a, b be Element of L;
coherence
proof end;
end;

registration
let L be with_suprema Poset;
let a, b be Element of L;
coherence
proof end;
end;

theorem :: YELLOW11:14
for L being LATTICE
for a, b being Element of L st L is modular holds
subrelstr [#b,(a "\/" b)#], subrelstr [#(a "/\" b),a#] are_isomorphic
proof end;

registration
existence
ex b1 being LATTICE st
( b1 is finite & not b1 is empty )
proof end;
end;

registration
coherence
for b1 being Semilattice st b1 is finite holds
b1 is lower-bounded
proof end;
end;

registration
coherence
for b1 being LATTICE st b1 is finite holds
b1 is complete
proof end;
end;