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