let L1, L2 be LATTICE; :: thesis: ( L1,L2 are_isomorphic & L1 is lower-bounded & L1 is arithmetic implies L2 is arithmetic )
assume that
A1:
L1,L2 are_isomorphic
and
A2:
( L1 is lower-bounded & L1 is arithmetic )
; :: thesis: L2 is arithmetic
consider f being Function of L1,L2 such that
A3:
f is isomorphic
by A1, WAYBEL_1:def 8;
reconsider g = f " as Function of L2,L1 by A3, WAYBEL_0:67;
A4:
g is isomorphic
by A3, WAYBEL_0:68;
A5:
L2 is algebraic
by A1, A2, WAYBEL13:32;
A7:
L2 is up-complete LATTICE
by A1, A2, WAYBEL13:30;
now let x2,
y2 be
Element of
L2;
:: thesis: ( x2 in the carrier of (CompactSublatt L2) & y2 in the carrier of (CompactSublatt L2) & ex_inf_of {x2,y2},L2 implies inf {x2,y2} in the carrier of (CompactSublatt L2) )assume that A8:
x2 in the
carrier of
(CompactSublatt L2)
and A9:
y2 in the
carrier of
(CompactSublatt L2)
and A10:
ex_inf_of {x2,y2},
L2
;
:: thesis: inf {x2,y2} in the carrier of (CompactSublatt L2)
(
x2 is
compact &
y2 is
compact )
by A8, A9, WAYBEL_8:def 1;
then
(
g . x2 is
compact &
g . y2 is
compact )
by A4, A2, A7, WAYBEL13:28;
then A11:
(
g . x2 in the
carrier of
(CompactSublatt L1) &
g . y2 in the
carrier of
(CompactSublatt L1) )
by WAYBEL_8:def 1;
(
x2 in the
carrier of
L2 &
y2 in the
carrier of
L2 & not the
carrier of
L1 is
empty )
;
then A12:
(
x2 in dom g &
y2 in dom g )
by FUNCT_2:def 1;
g is
infs-preserving
by A4, WAYBEL13:20;
then A13:
g preserves_inf_of {x2,y2}
by WAYBEL_0:def 32;
then A14:
g . (inf {x2,y2}) =
inf (g .: {x2,y2})
by A10, WAYBEL_0:def 30
.=
inf {(g . x2),(g . y2)}
by A12, FUNCT_1:118
;
ex_inf_of g .: {x2,y2},
L1
by A10, A13, WAYBEL_0:def 30;
then A15:
ex_inf_of {(g . x2),(g . y2)},
L1
by A12, FUNCT_1:118;
CompactSublatt L1 is
meet-inheriting
by A2, WAYBEL_8:def 5;
then
inf {(g . x2),(g . y2)} in the
carrier of
(CompactSublatt L1)
by A11, A15, YELLOW_0:def 16;
then
inf {(g . x2),(g . y2)} is
compact
by WAYBEL_8:def 1;
then
inf {x2,y2} is
compact
by A4, A2, A7, A14, WAYBEL13:28;
hence
inf {x2,y2} in the
carrier of
(CompactSublatt L2)
by WAYBEL_8:def 1;
:: thesis: verum end;
then
CompactSublatt L2 is meet-inheriting
by YELLOW_0:def 16;
hence
L2 is arithmetic
by A5, WAYBEL_8:def 5; :: thesis: verum