let A be non trivial set ; for L being non empty full finitely_typed Sublattice of non empty full finitely_typed
for e being Equivalence_Relation of st e in the carrier of L & e <> id A & type_of L <= 2 holds
L is modular
let L be non empty full finitely_typed Sublattice of non empty full finitely_typed ; for e being Equivalence_Relation of st e in the carrier of L & e <> id A & type_of L <= 2 holds
L is modular
let e be Equivalence_Relation of ; ( e in the carrier of L & e <> id A & type_of L <= 2 implies L is modular )
assume that
A1:
e in the carrier of L
and
A2:
e <> id A
; ( not type_of L <= 2 or L is modular )
assume A3:
type_of L <= 2
; L is modular
let a, b, c be Element of ; YELLOW11:def 3 ( not a <= c or a "\/" (b "/\" c) = (a "\/" b) "/\" c )
A4:
the carrier of L c= the carrier of (EqRelLATT A)
by YELLOW_0:def 13;
A5:
b in the carrier of L
;
then reconsider b' = b as Equivalence_Relation of by A4, LATTICE5:4;
reconsider b'' = b' as Element of by A4, A5;
A6:
a in the carrier of L
;
then reconsider a' = a as Equivalence_Relation of by A4, LATTICE5:4;
A7:
c in the carrier of L
;
then reconsider c' = c as Equivalence_Relation of by A4, LATTICE5:4;
reconsider c'' = c' as Element of by A4, A7;
reconsider a'' = a' as Element of by A4, A6;
A8: (a'' "\/" b'') "/\" c'' =
(a'' "\/" b'') /\ c'
by LATTICE5:8
.=
(a' "\/" b') /\ c'
by LATTICE5:10
;
assume A9:
a <= c
; a "\/" (b "/\" c) = (a "\/" b) "/\" c
then
a'' <= c''
by YELLOW_0:60;
then A10:
a' c= c'
by LATTICE5:6;
A11:
a'' "\/" (b'' "/\" c'') <= (a'' "\/" b'') "/\" c''
by A9, YELLOW11:8, YELLOW_0:60;
A12:
b' /\ c' = b'' "/\" c''
by LATTICE5:8;
then
a' "\/" (b' /\ c') = a'' "\/" (b'' "/\" c'')
by LATTICE5:10;
then A13:
a' "\/" (b' /\ c') c= (a' "\/" b') /\ c'
by A11, A8, LATTICE5:6;
consider AA being non empty set such that
A14:
for e being set st e in the carrier of L holds
e is Equivalence_Relation of
and
A15:
ex i being Element of NAT st
for e1, e2 being Equivalence_Relation of
for x, y being set st e1 in the carrier of L & e2 in the carrier of L & [x,y] in e1 "\/" e2 holds
ex F being non empty FinSequence of AA st
( len F = i & x,y are_joint_by F,e1,e2 )
by Def2;
e is Equivalence_Relation of
by A1, A14;
then A16:
( field e = A & field e = AA )
by EQREL_1:16;
A17:
(a' "\/" b') /\ c' c= a' "\/" (b' /\ c')
proof
let x,
y be
Element of
A;
RELSET_1:def 2 ( not [x,y] in (a' "\/" b') /\ c' or [x,y] in a' "\/" (b' /\ c') )
assume A18:
[x,y] in (a' "\/" b') /\ c'
;
[x,y] in a' "\/" (b' /\ c')
then A19:
[x,y] in a' "\/" b'
by XBOOLE_0:def 4;
A20:
[x,y] in c'
by A18, XBOOLE_0:def 4;
per cases
( type_of L = 2 or type_of L = 1 or type_of L = 0 )
by A3, NAT_1:27;
suppose
type_of L = 2
;
[x,y] in a' "\/" (b' /\ c')then consider F being non
empty FinSequence of
A such that A21:
len F = 2
+ 2
and A22:
x,
y are_joint_by F,
a',
b'
by A1, A2, A15, A16, A19, LATTICE5:def 4;
A23:
F . 4
= y
by A21, A22, LATTICE5:def 3;
consider l being
Element of
NAT such that A24:
l = 1
;
(2 * l) + 1
= 3
by A24;
then A25:
[(F . 3),(F . (3 + 1))] in a'
by A21, A22, LATTICE5:def 3;
consider k being
Element of
NAT such that A26:
k = 1
;
2
* k = 2
by A26;
then A27:
[(F . 2),(F . (2 + 1))] in b'
by A21, A22, LATTICE5:def 3;
A28:
F . 1
= x
by A22, LATTICE5:def 3;
reconsider BC =
b' /\ c' as
Element of
by A12;
set z1 =
F . 2;
set z2 =
F . 3;
consider j being
Element of
NAT such that A29:
j = 0
;
(2 * j) + 1
= 1
by A29;
then A30:
[(F . 1),(F . (1 + 1))] in a'
by A21, A22, LATTICE5:def 3;
A31:
a' "\/" (b' /\ c') = a'' "\/" BC
by LATTICE5:10;
BC <= BC "\/" a''
by YELLOW_0:22;
then A32:
b' /\ c' c= a' "\/" (b' /\ c')
by A31, LATTICE5:6;
a'' <= a'' "\/" BC
by YELLOW_0:22;
then A33:
a' c= a' "\/" (b' /\ c')
by A31, LATTICE5:6;
[y,x] in c'
by A20, EQREL_1:12;
then
[(F . 3),x] in c'
by A10, A23, A25, EQREL_1:13;
then
[(F . 3),(F . 2)] in c'
by A10, A28, A30, EQREL_1:13;
then
[(F . 2),(F . 3)] in c'
by EQREL_1:12;
then
[(F . 2),(F . 3)] in b' /\ c'
by A27, XBOOLE_0:def 4;
then
[x,(F . 3)] in a' "\/" (b' /\ c')
by A28, A30, A33, A32, EQREL_1:13;
hence
[x,y] in a' "\/" (b' /\ c')
by A23, A25, A33, EQREL_1:13;
verum end; suppose
type_of L = 1
;
[x,y] in a' "\/" (b' /\ c')then consider F being non
empty FinSequence of
A such that A34:
len F = 1
+ 2
and A35:
x,
y are_joint_by F,
a',
b'
by A1, A2, A15, A16, A19, LATTICE5:def 4;
set z1 =
F . 2;
consider k being
Element of
NAT such that A36:
k = 1
;
reconsider BC =
b' /\ c' as
Element of
by A12;
consider j being
Element of
NAT such that A37:
j = 0
;
(2 * j) + 1
= 1
by A37;
then A38:
[(F . 1),(F . (1 + 1))] in a'
by A34, A35, LATTICE5:def 3;
2
* k = 2
by A36;
then A39:
[(F . 2),(F . (2 + 1))] in b'
by A34, A35, LATTICE5:def 3;
A40:
a' "\/" (b' /\ c') = a'' "\/" BC
by LATTICE5:10;
A41:
[x,y] in c'
by A18, XBOOLE_0:def 4;
A42:
F . 1
= x
by A35, LATTICE5:def 3;
then
[(F . 2),x] in c'
by A10, A38, EQREL_1:12;
then A43:
[(F . 2),y] in c'
by A41, EQREL_1:13;
BC <= BC "\/" a''
by YELLOW_0:22;
then A44:
b' /\ c' c= a' "\/" (b' /\ c')
by A40, LATTICE5:6;
a'' <= a'' "\/" BC
by YELLOW_0:22;
then A45:
a' c= a' "\/" (b' /\ c')
by A40, LATTICE5:6;
F . 3
= y
by A34, A35, LATTICE5:def 3;
then
[(F . 2),y] in b' /\ c'
by A39, A43, XBOOLE_0:def 4;
hence
[x,y] in a' "\/" (b' /\ c')
by A42, A38, A45, A44, EQREL_1:13;
verum end; suppose
type_of L = 0
;
[x,y] in a' "\/" (b' /\ c')then consider F being non
empty FinSequence of
A such that A46:
(
len F = 0 + 2 &
x,
y are_joint_by F,
a',
b' )
by A1, A2, A15, A16, A19, LATTICE5:def 4;
reconsider BC =
b' /\ c' as
Element of
by A12;
consider j being
Element of
NAT such that A47:
j = 0
;
(2 * j) + 1
= 1
by A47;
then A48:
[(F . 1),(F . (1 + 1))] in a'
by A46, LATTICE5:def 3;
(
a'' <= a'' "\/" BC &
a' "\/" (b' /\ c') = a'' "\/" BC )
by LATTICE5:10, YELLOW_0:22;
then A49:
a' c= a' "\/" (b' /\ c')
by LATTICE5:6;
(
F . 1
= x &
F . 2
= y )
by A46, LATTICE5:def 3;
hence
[x,y] in a' "\/" (b' /\ c')
by A48, A49;
verum end;
end;
a'' "\/" b'' = a "\/" b
by YELLOW_0:71;
then A50: (a "\/" b) "/\" c =
(a'' "\/" b'') "/\" c''
by YELLOW_0:70
.=
(a'' "\/" b'') /\ c'
by LATTICE5:8
.=
(a' "\/" b') /\ c'
by LATTICE5:10
;
A51:
b'' "/\" c'' = b "/\" c
by YELLOW_0:70;
a' "\/" (b' /\ c') =
a'' "\/" (b'' "/\" c'')
by A12, LATTICE5:10
.=
a "\/" (b "/\" c)
by A51, YELLOW_0:71
;
hence
a "\/" (b "/\" c) = (a "\/" b) "/\" c
by A13, A17, A50, XBOOLE_0:def 10; verum