:: by Marek Chmur

::

:: Received April 26, 1991

:: Copyright (c) 1991-2012 Association of Mizar Users

begin

definition

ex b_{1} being BinOp of NAT st

for m, n being Nat holds b_{1} . (m,n) = m gcd n

for b_{1}, b_{2} being BinOp of NAT st ( for m, n being Nat holds b_{1} . (m,n) = m gcd n ) & ( for m, n being Nat holds b_{2} . (m,n) = m gcd n ) holds

b_{1} = b_{2}

ex b_{1} being BinOp of NAT st

for m, n being Nat holds b_{1} . (m,n) = m lcm n

for b_{1}, b_{2} being BinOp of NAT st ( for m, n being Nat holds b_{1} . (m,n) = m lcm n ) & ( for m, n being Nat holds b_{2} . (m,n) = m lcm n ) holds

b_{1} = b_{2}
end;

func hcflat -> BinOp of NAT means :Def1: :: NAT_LAT:def 1

for m, n being Nat holds it . (m,n) = m gcd n;

existence for m, n being Nat holds it . (m,n) = m gcd n;

ex b

for m, n being Nat holds b

proof end;

uniqueness for b

b

proof end;

func lcmlat -> BinOp of NAT means :Def2: :: NAT_LAT:def 2

for m, n being Nat holds it . (m,n) = m lcm n;

existence for m, n being Nat holds it . (m,n) = m lcm n;

ex b

for m, n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines hcflat NAT_LAT:def 1 :

for b_{1} being BinOp of NAT holds

( b_{1} = hcflat iff for m, n being Nat holds b_{1} . (m,n) = m gcd n );

for b

( b

:: deftheorem Def2 defines lcmlat NAT_LAT:def 2 :

for b_{1} being BinOp of NAT holds

( b_{1} = lcmlat iff for m, n being Nat holds b_{1} . (m,n) = m lcm n );

for b

( b

definition

LattStr(# NAT,lcmlat,hcflat #) is non empty strict LattStr ;

end;

func Nat_Lattice -> non empty strict LattStr equals :: NAT_LAT:def 3

LattStr(# NAT,lcmlat,hcflat #);

coherence LattStr(# NAT,lcmlat,hcflat #);

LattStr(# NAT,lcmlat,hcflat #) is non empty strict LattStr ;

registration

let p, q be Element of Nat_Lattice;

compatibility

p "\/" q = p lcm q by Def2;

compatibility

p "/\" q = p gcd q by Def1;

end;
compatibility

p "\/" q = p lcm q by Def2;

compatibility

p "/\" q = p gcd q by Def1;

Lm1: for a being Element of Nat_Lattice holds

( 0_NN "/\" a = 0_NN & a "/\" 0_NN = 0_NN )

by NEWTON:51;

theorem Th7: :: NAT_LAT:7

for p, q, r being Element of Nat_Lattice holds lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (p,q)),r)

proof end;

theorem :: NAT_LAT:8

for p, q, r being Element of Nat_Lattice holds

( lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (q,p)),r) & lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (p,r)),q) & lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (r,q)),p) & lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (r,p)),q) )

( lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (q,p)),r) & lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (p,r)),q) & lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (r,q)),p) & lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (r,p)),q) )

proof end;

theorem Th9: :: NAT_LAT:9

for p, q, r being Element of Nat_Lattice holds hcflat . (p,(hcflat . (q,r))) = hcflat . ((hcflat . (p,q)),r)

proof end;

theorem :: NAT_LAT:10

for p, q, r being Element of Nat_Lattice holds

( hcflat . (p,(hcflat . (q,r))) = hcflat . ((hcflat . (q,p)),r) & hcflat . (p,(hcflat . (q,r))) = hcflat . ((hcflat . (p,r)),q) & hcflat . (p,(hcflat . (q,r))) = hcflat . ((hcflat . (r,q)),p) & hcflat . (p,(hcflat . (q,r))) = hcflat . ((hcflat . (r,p)),q) )

( hcflat . (p,(hcflat . (q,r))) = hcflat . ((hcflat . (q,p)),r) & hcflat . (p,(hcflat . (q,r))) = hcflat . ((hcflat . (p,r)),q) & hcflat . (p,(hcflat . (q,r))) = hcflat . ((hcflat . (r,q)),p) & hcflat . (p,(hcflat . (q,r))) = hcflat . ((hcflat . (r,p)),q) )

proof end;

theorem :: NAT_LAT:11

for q, p being Element of Nat_Lattice holds

( hcflat . (q,(lcmlat . (q,p))) = q & hcflat . ((lcmlat . (p,q)),q) = q & hcflat . (q,(lcmlat . (p,q))) = q & hcflat . ((lcmlat . (q,p)),q) = q )

( hcflat . (q,(lcmlat . (q,p))) = q & hcflat . ((lcmlat . (p,q)),q) = q & hcflat . (q,(lcmlat . (p,q))) = q & hcflat . ((lcmlat . (q,p)),q) = q )

proof end;

theorem :: NAT_LAT:12

for q, p being Element of Nat_Lattice holds

( lcmlat . (q,(hcflat . (q,p))) = q & lcmlat . ((hcflat . (p,q)),q) = q & lcmlat . (q,(hcflat . (p,q))) = q & lcmlat . ((hcflat . (q,p)),q) = q )

( lcmlat . (q,(hcflat . (q,p))) = q & lcmlat . ((hcflat . (p,q)),q) = q & lcmlat . (q,(hcflat . (p,q))) = q & lcmlat . ((hcflat . (q,p)),q) = q )

proof end;

:: NATPLUS

definition

ex b_{1} being Subset of NAT st

for n being Nat holds

( n in b_{1} iff 0 < n )

for b_{1}, b_{2} being Subset of NAT st ( for n being Nat holds

( n in b_{1} iff 0 < n ) ) & ( for n being Nat holds

( n in b_{2} iff 0 < n ) ) holds

b_{1} = b_{2}
end;

func NATPLUS -> Subset of NAT means :Def6: :: NAT_LAT:def 6

for n being Nat holds

( n in it iff 0 < n );

existence for n being Nat holds

( n in it iff 0 < n );

ex b

for n being Nat holds

( n in b

proof end;

uniqueness for b

( n in b

( n in b

b

proof end;

:: deftheorem Def6 defines NATPLUS NAT_LAT:def 6 :

for b_{1} being Subset of NAT holds

( b_{1} = NATPLUS iff for n being Nat holds

( n in b_{1} iff 0 < n ) );

for b

( b

( n in b

definition

let D be non empty set ;

let S be non empty Subset of D;

let N be non empty Subset of S;

:: original: Element

redefine mode Element of N -> Element of S;

coherence

for b_{1} being Element of N holds b_{1} is Element of S

end;
let S be non empty Subset of D;

let N be non empty Subset of S;

:: original: Element

redefine mode Element of N -> Element of S;

coherence

for b

proof end;

registration
end;

registration
end;

:: LATTICE of NATURAL NUMBERS > 0

registration
end;

definition

ex b_{1} being BinOp of NATPLUS st

for m, n being NatPlus holds b_{1} . (m,n) = m gcd n

for b_{1}, b_{2} being BinOp of NATPLUS st ( for m, n being NatPlus holds b_{1} . (m,n) = m gcd n ) & ( for m, n being NatPlus holds b_{2} . (m,n) = m gcd n ) holds

b_{1} = b_{2}

ex b_{1} being BinOp of NATPLUS st

for m, n being NatPlus holds b_{1} . (m,n) = m lcm n

for b_{1}, b_{2} being BinOp of NATPLUS st ( for m, n being NatPlus holds b_{1} . (m,n) = m lcm n ) & ( for m, n being NatPlus holds b_{2} . (m,n) = m lcm n ) holds

b_{1} = b_{2}
end;

func hcflatplus -> BinOp of NATPLUS means :Def8: :: NAT_LAT:def 8

for m, n being NatPlus holds it . (m,n) = m gcd n;

existence for m, n being NatPlus holds it . (m,n) = m gcd n;

ex b

for m, n being NatPlus holds b

proof end;

uniqueness for b

b

proof end;

func lcmlatplus -> BinOp of NATPLUS means :Def9: :: NAT_LAT:def 9

for m, n being NatPlus holds it . (m,n) = m lcm n;

existence for m, n being NatPlus holds it . (m,n) = m lcm n;

ex b

for m, n being NatPlus holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def8 defines hcflatplus NAT_LAT:def 8 :

for b_{1} being BinOp of NATPLUS holds

( b_{1} = hcflatplus iff for m, n being NatPlus holds b_{1} . (m,n) = m gcd n );

for b

( b

:: deftheorem Def9 defines lcmlatplus NAT_LAT:def 9 :

for b_{1} being BinOp of NATPLUS holds

( b_{1} = lcmlatplus iff for m, n being NatPlus holds b_{1} . (m,n) = m lcm n );

for b

( b

definition

LattStr(# NATPLUS,lcmlatplus,hcflatplus #) is strict LattStr ;

end;

func NatPlus_Lattice -> strict LattStr equals :: NAT_LAT:def 10

LattStr(# NATPLUS,lcmlatplus,hcflatplus #);

coherence LattStr(# NATPLUS,lcmlatplus,hcflatplus #);

LattStr(# NATPLUS,lcmlatplus,hcflatplus #) is strict LattStr ;

:: deftheorem defines NatPlus_Lattice NAT_LAT:def 10 :

NatPlus_Lattice = LattStr(# NATPLUS,lcmlatplus,hcflatplus #);

NatPlus_Lattice = LattStr(# NATPLUS,lcmlatplus,hcflatplus #);

registration
end;

registration

coherence

for b_{1} being Element of NatPlus_Lattice holds

( b_{1} is natural & not b_{1} is zero )
;

end;
for b

( b

registration

let p, q be Element of NatPlus_Lattice;

compatibility

p "\/" q = p lcm q by Def9;

compatibility

p "/\" q = p gcd q by Def8;

end;
compatibility

p "\/" q = p lcm q by Def9;

compatibility

p "/\" q = p gcd q by Def8;

Lm2: ( ( for a, b being Element of NatPlus_Lattice holds a "\/" b = b "\/" a ) & ( for a, b, c being Element of NatPlus_Lattice holds a "\/" (b "\/" c) = (a "\/" b) "\/" c ) )

by NEWTON:43;

Lm3: ( ( for a, b being Element of NatPlus_Lattice holds (a "/\" b) "\/" b = b ) & ( for a, b being Element of NatPlus_Lattice holds a "/\" b = b "/\" a ) )

by NEWTON:53;

Lm4: ( ( for a, b, c being Element of NatPlus_Lattice holds a "/\" (b "/\" c) = (a "/\" b) "/\" c ) & ( for a, b being Element of NatPlus_Lattice holds a "/\" (a "\/" b) = a ) )

by NEWTON:48, NEWTON:54;

registration

( NatPlus_Lattice is join-commutative & NatPlus_Lattice is join-associative & NatPlus_Lattice is meet-commutative & NatPlus_Lattice is meet-associative & NatPlus_Lattice is join-absorbing & NatPlus_Lattice is meet-absorbing ) by Lm2, Lm3, Lm4, LATTICES:def 4, LATTICES:def 5, LATTICES:def 6, LATTICES:def 7, LATTICES:def 8, LATTICES:def 9;

end;

cluster NatPlus_Lattice -> strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing ;

coherence ( NatPlus_Lattice is join-commutative & NatPlus_Lattice is join-associative & NatPlus_Lattice is meet-commutative & NatPlus_Lattice is meet-associative & NatPlus_Lattice is join-absorbing & NatPlus_Lattice is meet-absorbing ) by Lm2, Lm3, Lm4, LATTICES:def 4, LATTICES:def 5, LATTICES:def 6, LATTICES:def 7, LATTICES:def 8, LATTICES:def 9;

Lm5: now :: thesis: for L being Lattice holds

( the L_join of L = the L_join of L || the carrier of L & the L_meet of L = the L_meet of L || the carrier of L )

( the L_join of L = the L_join of L || the carrier of L & the L_meet of L = the L_meet of L || the carrier of L )

let L be Lattice; :: thesis: ( the L_join of L = the L_join of L || the carrier of L & the L_meet of L = the L_meet of L || the carrier of L )

[: the carrier of L, the carrier of L:] = dom the L_join of L by FUNCT_2:def 1;

hence the L_join of L = the L_join of L || the carrier of L by RELAT_1:68; :: thesis: the L_meet of L = the L_meet of L || the carrier of L

[: the carrier of L, the carrier of L:] = dom the L_meet of L by FUNCT_2:def 1;

hence the L_meet of L = the L_meet of L || the carrier of L by RELAT_1:68; :: thesis: verum

end;
[: the carrier of L, the carrier of L:] = dom the L_join of L by FUNCT_2:def 1;

hence the L_join of L = the L_join of L || the carrier of L by RELAT_1:68; :: thesis: the L_meet of L = the L_meet of L || the carrier of L

[: the carrier of L, the carrier of L:] = dom the L_meet of L by FUNCT_2:def 1;

hence the L_meet of L = the L_meet of L || the carrier of L by RELAT_1:68; :: thesis: verum

definition

let L be Lattice;

ex b_{1} being Lattice st

( the carrier of b_{1} c= the carrier of L & the L_join of b_{1} = the L_join of L || the carrier of b_{1} & the L_meet of b_{1} = the L_meet of L || the carrier of b_{1} )

end;
mode SubLattice of L -> Lattice means :Def12: :: NAT_LAT:def 12

( the carrier of it c= the carrier of L & the L_join of it = the L_join of L || the carrier of it & the L_meet of it = the L_meet of L || the carrier of it );

existence ( the carrier of it c= the carrier of L & the L_join of it = the L_join of L || the carrier of it & the L_meet of it = the L_meet of L || the carrier of it );

ex b

( the carrier of b

proof end;

:: deftheorem Def12 defines SubLattice NAT_LAT:def 12 :

for L, b_{2} being Lattice holds

( b_{2} is SubLattice of L iff ( the carrier of b_{2} c= the carrier of L & the L_join of b_{2} = the L_join of L || the carrier of b_{2} & the L_meet of b_{2} = the L_meet of L || the carrier of b_{2} ) );

for L, b

( b

registration

let L be Lattice;

ex b_{1} being SubLattice of L st b_{1} is strict

end;
cluster non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like for SubLattice of L;

existence ex b

proof end;