let L be lower-bounded algebraic LATTICE; :: thesis: ( L is arithmetic iff L -waybelow is multiplicative )
thus
( L is arithmetic implies L -waybelow is multiplicative )
:: thesis: ( L -waybelow is multiplicative implies L is arithmetic )proof
assume A1:
L is
arithmetic
;
:: thesis: L -waybelow is multiplicative
now let a,
x,
y be
Element of
L;
:: thesis: ( [a,x] in L -waybelow & [a,y] in L -waybelow implies [a,(x "/\" y)] in L -waybelow )assume
(
[a,x] in L -waybelow &
[a,y] in L -waybelow )
;
:: thesis: [a,(x "/\" y)] in L -waybelow then A2:
(
a << x &
a << y )
by WAYBEL_4:def 2;
then consider c being
Element of
L such that A3:
(
c in the
carrier of
(CompactSublatt L) &
a <= c &
c <= x )
by Th7;
consider k being
Element of
L such that A4:
(
k in the
carrier of
(CompactSublatt L) &
a <= k &
k <= y )
by A2, Th7;
a "/\" a = a
by YELLOW_5:2;
then A5:
a <= c "/\" k
by A3, A4, YELLOW_3:2;
reconsider C =
CompactSublatt L as non
empty full meet-inheriting SubRelStr of
L by A1, Def5;
reconsider c' =
c,
k' =
k as
Element of
C by A3, A4;
A6:
c "/\" k <= x "/\" y
by A3, A4, YELLOW_3:2;
c' "/\" k' in the
carrier of
(CompactSublatt L)
;
then
c "/\" k in the
carrier of
(CompactSublatt L)
by YELLOW_0:70;
then
c "/\" k is
compact
by Def1;
then
c "/\" k << c "/\" k
by WAYBEL_3:def 2;
then
a << x "/\" y
by A5, A6, WAYBEL_3:2;
hence
[a,(x "/\" y)] in L -waybelow
by WAYBEL_4:def 2;
:: thesis: verum end;
hence
L -waybelow is
multiplicative
by WAYBEL_7:def 7;
:: thesis: verum
end;
assume A7:
L -waybelow is multiplicative
; :: thesis: L is arithmetic
now let x,
y be
Element of
L;
:: thesis: ( x in the carrier of (CompactSublatt L) & y in the carrier of (CompactSublatt L) & ex_inf_of {x,y},L implies inf {x,y} in the carrier of (CompactSublatt L) )assume that A8:
x in the
carrier of
(CompactSublatt L)
and A9:
y in the
carrier of
(CompactSublatt L)
and
ex_inf_of {x,y},
L
;
:: thesis: inf {x,y} in the carrier of (CompactSublatt L)
(
x is
compact &
y is
compact )
by A8, A9, Def1;
then
(
x << x &
y << y )
by WAYBEL_3:def 2;
then
(
[x,x] in L -waybelow &
[y,y] in L -waybelow )
by WAYBEL_4:def 2;
then
[(x "/\" y),(x "/\" y)] in L -waybelow
by A7, WAYBEL_7:45;
then
x "/\" y << x "/\" y
by WAYBEL_4:def 2;
then
x "/\" y is
compact
by WAYBEL_3:def 2;
then
x "/\" y in the
carrier of
(CompactSublatt L)
by Def1;
hence
inf {x,y} in the
carrier of
(CompactSublatt L)
by YELLOW_0:40;
:: thesis: verum end;
then
CompactSublatt L is meet-inheriting
by YELLOW_0:def 16;
hence
L is arithmetic
by Def5; :: thesis: verum