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