let L be LATTICE; 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; ( L is modular implies subrelstr [#b,(a "\/" b)#], subrelstr [#(a "/\" b),a#] are_isomorphic )
assume A1:
L is modular
; subrelstr [#b,(a "\/" b)#], subrelstr [#(a "/\" b),a#] are_isomorphic
defpred S1[ object , object ] 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 object st x in the carrier of (subrelstr [#b,(a "\/" b)#]) holds
ex y being object st
( y in the carrier of (subrelstr [#(a "/\" b),a#]) & S1[x,y] )
proof
let x be
object ;
( x in the carrier of (subrelstr [#b,(a "\/" b)#]) implies ex y being object st
( y in the carrier of (subrelstr [#(a "/\" b),a#]) & S1[x,y] ) )
assume
x in the
carrier of
(subrelstr [#b,(a "\/" b)#])
;
ex y being object 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;
( y in the carrier of (subrelstr [#(a "/\" b),a#]) & S1[x,y] )
x1 <= a "\/" b
by A3, Def4;
then
y <= a "/\" (a "\/" b)
by YELLOW_5:6;
then A4:
y <= a
by LATTICE3:18;
b <= x1
by A3, Def4;
then
a "/\" b <= y
by YELLOW_5:6;
then
y in [#(a "/\" b),a#]
by A4, Def4;
hence
y in the
carrier of
(subrelstr [#(a "/\" b),a#])
by YELLOW_0:def 15;
S1[x,y]
thus
S1[
x,
y]
;
verum
end;
consider f being Function of the carrier of (subrelstr [#b,(a "\/" b)#]), the carrier of (subrelstr [#(a "/\" b),a#]) such that
A5:
for x being object 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
; WAYBEL_1:def 8 f is isomorphic
thus
f is isomorphic
verumproof
A6:
b <= a "\/" b
by YELLOW_0:22;
b <= b
;
then
b in [#b,(a "\/" b)#]
by A6, Def4;
then reconsider s1 =
subrelstr [#b,(b "\/" a)#] as non
empty full Sublattice of
L by YELLOW_0:def 15;
A7:
a "/\" b <= a
by YELLOW_0:23;
a "/\" b <= a "/\" b
;
then
a "/\" b in [#(a "/\" b),a#]
by A7, Def4;
then reconsider s2 =
subrelstr [#(a "/\" b),a#] as non
empty full Sublattice of
L by YELLOW_0:def 15;
reconsider f1 =
f as
Function of
s1,
s2 ;
dom f1 = the
carrier of
(subrelstr [#b,(a "\/" b)#])
by FUNCT_2:def 1;
then A8:
dom f1 = [#b,(a "\/" b)#]
by YELLOW_0:def 15;
the
carrier of
(subrelstr [#(a "/\" b),a#]) c= rng f1
proof
let y be
object ;
TARSKI:def 3 ( 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#])
;
y in rng f1
then A9:
y in [#(a "/\" b),a#]
by YELLOW_0:def 15;
then reconsider Y =
y as
Element of
L ;
A10:
a "/\" b <= Y
by A9, Def4;
then
(a "/\" b) "\/" b <= Y "\/" b
by WAYBEL_1:2;
then A11:
b <= Y "\/" b
by LATTICE3:17;
A12:
Y <= a
by A9, Def4;
then
Y "\/" b <= a "\/" b
by WAYBEL_1:2;
then A13:
Y "\/" b in [#b,(a "\/" b)#]
by A11, 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 A5;
f1yb =
(Y "\/" b) "/\" a
by A5, A14
.=
Y "\/" (b "/\" a)
by A1, A12
.=
Y
by A10, YELLOW_5:8
;
hence
y in rng f1
by A8, A13, FUNCT_1:def 3;
verum
end;
then A15:
rng f1 = the
carrier of
(subrelstr [#(a "/\" b),a#])
;
A16:
for
x,
y being
Element of
s1 holds
(
x <= y iff
f1 . x <= f1 . y )
proof
let x,
y be
Element of
s1;
( x <= y iff f1 . x <= f1 . y )
A17:
the
carrier of
s1 = [#b,(a "\/" b)#]
by YELLOW_0:def 15;
then
x in [#b,(a "\/" b)#]
;
then reconsider X =
x as
Element of
L ;
y in [#b,(a "\/" b)#]
by A17;
then reconsider Y =
y as
Element of
L ;
reconsider f1Y =
f1 . Y as
Element of
L by A5;
reconsider f1X =
f1 . X as
Element of
L by A5;
thus
(
x <= y implies
f1 . x <= f1 . y )
( f1 . x <= f1 . y implies x <= y )
thus
(
f1 . x <= f1 . y implies
x <= y )
verumproof
assume
f1 . x <= f1 . y
;
x <= y
then A21:
[(f1 . x),(f1 . y)] in the
InternalRel of
s2
by ORDERS_2:def 5;
the
InternalRel of
s2 c= the
InternalRel of
L
by YELLOW_0:def 13;
then A22:
f1X <= f1Y
by A21, ORDERS_2:def 5;
A23:
f1Y = Y "/\" a
by A5;
A24:
b <= X
by A17, Def4;
f1X = X "/\" a
by A5;
then
b "\/" (a "/\" X) <= b "\/" (a "/\" Y)
by A22, A23, WAYBEL_1:2;
then A25:
(b "\/" a) "/\" X <= b "\/" (a "/\" Y)
by A1, A24;
A26:
X <= b "\/" a
by A17, Def4;
b <= Y
by A17, Def4;
then
(b "\/" a) "/\" X <= (b "\/" a) "/\" Y
by A1, A25;
then A27:
X <= (b "\/" a) "/\" Y
by A26, YELLOW_5:10;
Y <= b "\/" a
by A17, Def4;
then
X <= Y
by A27, YELLOW_5:10;
hence
x <= y
by YELLOW_0:60;
verum
end;
end;
f1 is
one-to-one
proof
let x1,
x2 be
object ;
FUNCT_1:def 4 ( not x1 in K21(f1) or not x2 in K21(f1) or not f1 . x1 = f1 . x2 or x1 = x2 )
assume that A28:
x1 in dom f1
and A29:
x2 in dom f1
and A30:
f1 . x1 = f1 . x2
;
x1 = x2
reconsider X2 =
x2 as
Element of
L by A8, A29;
A31:
b <= X2
by A8, A29, Def4;
reconsider X1 =
x1 as
Element of
L by A8, A28;
A32:
b <= X1
by A8, A28, Def4;
reconsider f1X1 =
f1 . X1 as
Element of
L by A5, A28;
A33:
f1X1 = X1 "/\" a
by A5, A28;
reconsider f1X2 =
f1 . X2 as
Element of
L by A5, A29;
A34:
f1X2 = X2 "/\" a
by A5, A29;
A35:
X2 <= a "\/" b
by A8, A29, Def4;
X1 <= a "\/" b
by A8, A28, Def4;
then X1 =
(b "\/" a) "/\" X1
by YELLOW_5:10
.=
b "\/" (a "/\" X2)
by A1, A30, A32, A33, A34
.=
(b "\/" a) "/\" X2
by A1, A31
.=
X2
by A35, YELLOW_5:10
;
hence
x1 = x2
;
verum
end;
hence
f is
isomorphic
by A15, A16, WAYBEL_0:66;
verum
end;