let L be LATTICE; :: thesis: for a, b being Element of L st L is modular holds
subrelstr [#b,(a "\/" b)#], subrelstr [#(a "/\" b),a#] are_isomorphic
let a, b be Element of L; :: thesis: ( L is modular implies subrelstr [#b,(a "\/" b)#], subrelstr [#(a "/\" b),a#] are_isomorphic )
assume A1:
L is modular
; :: thesis: subrelstr [#b,(a "\/" b)#], subrelstr [#(a "/\" b),a#] are_isomorphic
defpred S1[ set , set ] means ( $2 is Element of L & ( for X, Y being Element of L st $1 = X & $2 = Y holds
Y = X "/\" a ) );
A2:
for x being set st x in the carrier of (subrelstr [#b,(a "\/" b)#]) holds
ex y being set st
( y in the carrier of (subrelstr [#(a "/\" b),a#]) & S1[x,y] )
proof
let x be
set ;
:: thesis: ( x in the carrier of (subrelstr [#b,(a "\/" b)#]) implies ex y being set st
( y in the carrier of (subrelstr [#(a "/\" b),a#]) & S1[x,y] ) )
assume
x in the
carrier of
(subrelstr [#b,(a "\/" b)#])
;
:: thesis: ex y being set st
( y in the carrier of (subrelstr [#(a "/\" b),a#]) & S1[x,y] )
then A3:
x in [#b,(a "\/" b)#]
by YELLOW_0:def 15;
then reconsider x1 =
x as
Element of
L ;
take y =
a "/\" x1;
:: thesis: ( y in the carrier of (subrelstr [#(a "/\" b),a#]) & S1[x,y] )
(
b <= x1 &
x1 <= a "\/" b )
by A3, Def4;
then
(
a "/\" b <= y &
y <= a "/\" (a "\/" b) )
by YELLOW_5:6;
then
(
a "/\" b <= y &
y <= a )
by LATTICE3:18;
then
y in [#(a "/\" b),a#]
by Def4;
hence
y in the
carrier of
(subrelstr [#(a "/\" b),a#])
by YELLOW_0:def 15;
:: thesis: S1[x,y]
thus
S1[
x,
y]
;
:: thesis: verum
end;
consider f being Function of the carrier of (subrelstr [#b,(a "\/" b)#]),the carrier of (subrelstr [#(a "/\" b),a#]) such that
A4:
for x being set st x in the carrier of (subrelstr [#b,(a "\/" b)#]) holds
S1[x,f . x]
from FUNCT_2:sch 1(A2);
reconsider f = f as Function of (subrelstr [#b,(a "\/" b)#]),(subrelstr [#(a "/\" b),a#]) ;
take
f
; :: according to WAYBEL_1:def 8 :: thesis: f is isomorphic
thus
f is isomorphic
:: thesis: verumproof
not
subrelstr [#b,(b "\/" a)#] is
empty
then reconsider s1 =
subrelstr [#b,(b "\/" a)#] as non
empty full Sublattice of
L ;
not
subrelstr [#(a "/\" b),a#] is
empty
then reconsider s2 =
subrelstr [#(a "/\" b),a#] as non
empty full Sublattice of
L ;
reconsider f1 =
f as
Function of
s1,
s2 ;
dom f1 = the
carrier of
(subrelstr [#b,(a "\/" b)#])
by FUNCT_2:def 1;
then A5:
dom f1 = [#b,(a "\/" b)#]
by YELLOW_0:def 15;
A6:
f1 is
one-to-one
proof
let x1,
x2 be
set ;
:: according to FUNCT_1:def 8 :: thesis: ( not x1 in K32(f1) or not x2 in K32(f1) or not f1 . x1 = f1 . x2 or x1 = x2 )
assume A7:
(
x1 in dom f1 &
x2 in dom f1 &
f1 . x1 = f1 . x2 )
;
:: thesis: x1 = x2
then reconsider X1 =
x1 as
Element of
L by A5;
reconsider X2 =
x2 as
Element of
L by A5, A7;
reconsider f1X1 =
f1 . X1 as
Element of
L by A4, A7;
reconsider f1X2 =
f1 . X2 as
Element of
L by A4, A7;
A8:
(
b <= X1 &
X1 <= a "\/" b &
b <= X2 &
X2 <= a "\/" b )
by A5, A7, Def4;
A9:
(
f1X1 = X1 "/\" a &
f1X2 = X2 "/\" a )
by A4, A7;
X1 =
(b "\/" a) "/\" X1
by A8, YELLOW_5:10
.=
b "\/" (a "/\" X2)
by A1, A7, A8, A9, Def3
.=
(b "\/" a) "/\" X2
by A1, A8, Def3
.=
X2
by A8, YELLOW_5:10
;
hence
x1 = x2
;
:: thesis: verum
end;
A10:
rng f1 = the
carrier of
(subrelstr [#(a "/\" b),a#])
proof
thus
rng f1 c= the
carrier of
(subrelstr [#(a "/\" b),a#])
;
:: according to XBOOLE_0:def 10 :: thesis: the carrier of (subrelstr [#(a "/\" b),a#]) c= rng f1
thus
the
carrier of
(subrelstr [#(a "/\" b),a#]) c= rng f1
:: thesis: verumproof
let y be
set ;
:: according to TARSKI:def 3 :: thesis: ( not y in the carrier of (subrelstr [#(a "/\" b),a#]) or y in rng f1 )
assume
y in the
carrier of
(subrelstr [#(a "/\" b),a#])
;
:: thesis: y in rng f1
then A11:
y in [#(a "/\" b),a#]
by YELLOW_0:def 15;
then reconsider Y =
y as
Element of
L ;
A12:
(
a "/\" b <= Y &
Y <= a )
by A11, Def4;
then
(
(a "/\" b) "\/" b <= Y "\/" b &
Y "\/" b <= a "\/" b )
by WAYBEL_1:3;
then
(
b <= Y "\/" b &
Y "\/" b <= a "\/" b )
by LATTICE3:17;
then A13:
Y "\/" b in [#b,(a "\/" b)#]
by Def4;
then A14:
Y "\/" b in the
carrier of
(subrelstr [#b,(a "\/" b)#])
by YELLOW_0:def 15;
then reconsider f1yb =
f1 . (Y "\/" b) as
Element of
L by A4;
f1yb =
(Y "\/" b) "/\" a
by A4, A14
.=
Y "\/" (b "/\" a)
by A1, A12, Def3
.=
Y
by A12, YELLOW_5:8
;
hence
y in rng f1
by A5, A13, FUNCT_1:def 5;
:: thesis: verum
end;
end;
for
x,
y being
Element of
s1 holds
(
x <= y iff
f1 . x <= f1 . y )
proof
let x,
y be
Element of
s1;
:: thesis: ( x <= y iff f1 . x <= f1 . y )
A15:
the
carrier of
s1 = [#b,(a "\/" b)#]
by YELLOW_0:def 15;
then A16:
(
x in [#b,(a "\/" b)#] &
y in [#b,(a "\/" b)#] )
;
then reconsider X =
x as
Element of
L ;
reconsider Y =
y as
Element of
L by A16;
reconsider f1X =
f1 . X as
Element of
L by A4;
reconsider f1Y =
f1 . Y as
Element of
L by A4;
thus
(
x <= y implies
f1 . x <= f1 . y )
:: thesis: ( f1 . x <= f1 . y implies x <= y )
thus
(
f1 . x <= f1 . y implies
x <= y )
:: thesis: verumproof
assume
f1 . x <= f1 . y
;
:: thesis: x <= y
then A19:
[(f1 . x),(f1 . y)] in the
InternalRel of
s2
by ORDERS_2:def 9;
the
InternalRel of
s2 c= the
InternalRel of
L
by YELLOW_0:def 13;
then A20:
f1X <= f1Y
by A19, ORDERS_2:def 9;
(
f1X = X "/\" a &
f1Y = Y "/\" a )
by A4;
then A21:
b "\/" (a "/\" X) <= b "\/" (a "/\" Y)
by A20, WAYBEL_1:3;
A22:
(
b <= X &
X <= b "\/" a &
b <= Y &
Y <= b "\/" a )
by A15, Def4;
then
(b "\/" a) "/\" X <= b "\/" (a "/\" Y)
by A1, A21, Def3;
then
(b "\/" a) "/\" X <= (b "\/" a) "/\" Y
by A1, A22, Def3;
then
X <= (b "\/" a) "/\" Y
by A22, YELLOW_5:10;
then
X <= Y
by A22, YELLOW_5:10;
hence
x <= y
by YELLOW_0:61;
:: thesis: verum
end;
end;
hence
f is
isomorphic
by A6, A10, WAYBEL_0:66;
:: thesis: verum
end;