:: NAT_LAT semantic presentation begin definition func hcflat -> BinOp of NAT means :Def1: :: NAT_LAT:def 1 for m, n being Nat holds it . (m,n) = m gcd n; existence ex b1 being BinOp of NAT st for m, n being Nat holds b1 . (m,n) = m gcd n proof deffunc H1( Nat, Nat) -> Element of NAT = $1 gcd $2; consider o being BinOp of NAT such that A1: for a, b being Element of NAT holds o . (a,b) = H1(a,b) from BINOP_1:sch_4(); take o ; ::_thesis: for m, n being Nat holds o . (m,n) = m gcd n let m, n be Nat; ::_thesis: o . (m,n) = m gcd n ( m in NAT & n in NAT ) by ORDINAL1:def_12; hence o . (m,n) = m gcd n by A1; ::_thesis: verum end; uniqueness for b1, b2 being BinOp of NAT st ( for m, n being Nat holds b1 . (m,n) = m gcd n ) & ( for m, n being Nat holds b2 . (m,n) = m gcd n ) holds b1 = b2 proof let f1, f2 be BinOp of NAT; ::_thesis: ( ( for m, n being Nat holds f1 . (m,n) = m gcd n ) & ( for m, n being Nat holds f2 . (m,n) = m gcd n ) implies f1 = f2 ) assume that A2: for m, n being Nat holds f1 . (m,n) = m gcd n and A3: for m, n being Nat holds f2 . (m,n) = m gcd n ; ::_thesis: f1 = f2 now__::_thesis:_for_m,_n_being_Element_of_NAT_holds_f1_._(m,n)_=_f2_._(m,n) let m, n be Element of NAT ; ::_thesis: f1 . (m,n) = f2 . (m,n) thus f1 . (m,n) = m gcd n by A2 .= f2 . (m,n) by A3 ; ::_thesis: verum end; hence f1 = f2 by BINOP_1:2; ::_thesis: verum 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 ex b1 being BinOp of NAT st for m, n being Nat holds b1 . (m,n) = m lcm n proof deffunc H1( Nat, Nat) -> Element of NAT = $1 lcm $2; consider o being BinOp of NAT such that A4: for a, b being Element of NAT holds o . (a,b) = H1(a,b) from BINOP_1:sch_4(); take o ; ::_thesis: for m, n being Nat holds o . (m,n) = m lcm n let m, n be Nat; ::_thesis: o . (m,n) = m lcm n ( m in NAT & n in NAT ) by ORDINAL1:def_12; hence o . (m,n) = m lcm n by A4; ::_thesis: verum end; uniqueness for b1, b2 being BinOp of NAT st ( for m, n being Nat holds b1 . (m,n) = m lcm n ) & ( for m, n being Nat holds b2 . (m,n) = m lcm n ) holds b1 = b2 proof let f1, f2 be BinOp of NAT; ::_thesis: ( ( for m, n being Nat holds f1 . (m,n) = m lcm n ) & ( for m, n being Nat holds f2 . (m,n) = m lcm n ) implies f1 = f2 ) assume that A5: for m, n being Nat holds f1 . (m,n) = m lcm n and A6: for m, n being Nat holds f2 . (m,n) = m lcm n ; ::_thesis: f1 = f2 now__::_thesis:_for_m,_n_being_Element_of_NAT_holds_f1_._(m,n)_=_f2_._(m,n) let m, n be Element of NAT ; ::_thesis: f1 . (m,n) = f2 . (m,n) thus f1 . (m,n) = m lcm n by A5 .= f2 . (m,n) by A6 ; ::_thesis: verum end; hence f1 = f2 by BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def1 defines hcflat NAT_LAT:def_1_:_ for b1 being BinOp of NAT holds ( b1 = hcflat iff for m, n being Nat holds b1 . (m,n) = m gcd n ); :: deftheorem Def2 defines lcmlat NAT_LAT:def_2_:_ for b1 being BinOp of NAT holds ( b1 = lcmlat iff for m, n being Nat holds b1 . (m,n) = m lcm n ); definition func Nat_Lattice -> non empty strict LattStr equals :: NAT_LAT:def 3 LattStr(# NAT,lcmlat,hcflat #); coherence LattStr(# NAT,lcmlat,hcflat #) is non empty strict LattStr ; end; :: deftheorem defines Nat_Lattice NAT_LAT:def_3_:_ Nat_Lattice = LattStr(# NAT,lcmlat,hcflat #); registration cluster the carrier of Nat_Lattice -> natural-membered ; coherence the carrier of Nat_Lattice is natural-membered ; end; registration let p, q be Element of Nat_Lattice; identifyp "\/" q with p lcm q; compatibility p "\/" q = p lcm q by Def2; identifyp "/\" q with p gcd q; compatibility p "/\" q = p gcd q by Def1; end; theorem :: NAT_LAT:1 for p, q being Element of Nat_Lattice holds p "\/" q = p lcm q ; theorem :: NAT_LAT:2 for p, q being Element of Nat_Lattice holds p "/\" q = p gcd q ; theorem :: NAT_LAT:3 for a, b being Element of Nat_Lattice st a [= b holds a divides b proof let a, b be Element of Nat_Lattice; ::_thesis: ( a [= b implies a divides b ) assume a [= b ; ::_thesis: a divides b then a "\/" b = b by LATTICES:def_3; hence a divides b by NEWTON:44; ::_thesis: verum end; definition func 0_NN -> Element of Nat_Lattice equals :: NAT_LAT:def 4 1; coherence 1 is Element of Nat_Lattice ; func 1_NN -> Element of Nat_Lattice equals :: NAT_LAT:def 5 0 ; coherence 0 is Element of Nat_Lattice ; end; :: deftheorem defines 0_NN NAT_LAT:def_4_:_ 0_NN = 1; :: deftheorem defines 1_NN NAT_LAT:def_5_:_ 1_NN = 0 ; theorem :: NAT_LAT:4 0_NN = 1 ; Lm1: for a being Element of Nat_Lattice holds ( 0_NN "/\" a = 0_NN & a "/\" 0_NN = 0_NN ) by NEWTON:51; registration cluster Nat_Lattice -> non empty strict Lattice-like ; coherence Nat_Lattice is Lattice-like proof thus ( ( for p, q being Element of Nat_Lattice holds p "\/" q = q "\/" p ) & ( for p, q, r being Element of Nat_Lattice holds p "\/" (q "\/" r) = (p "\/" q) "\/" r ) & ( for p, q being Element of Nat_Lattice holds (p "/\" q) "\/" q = q ) & ( for p, q being Element of Nat_Lattice holds p "/\" q = q "/\" p ) & ( for p, q, r being Element of Nat_Lattice holds p "/\" (q "/\" r) = (p "/\" q) "/\" r ) & ( for p, q being Element of Nat_Lattice holds p "/\" (p "\/" q) = p ) ) by NEWTON:43, NEWTON:48, NEWTON:53, NEWTON:54; :: according to LATTICES:def_4,LATTICES:def_5,LATTICES:def_6,LATTICES:def_7,LATTICES:def_8,LATTICES:def_9,LATTICES:def_10 ::_thesis: verum end; end; registration cluster Nat_Lattice -> non empty strict ; coherence Nat_Lattice is strict ; end; registration cluster Nat_Lattice -> non empty strict lower-bounded ; coherence Nat_Lattice is lower-bounded by Lm1, LATTICES:def_13; end; theorem Th5: :: NAT_LAT:5 for p, q being Element of Nat_Lattice holds lcmlat . (p,q) = lcmlat . (q,p) proof let p, q be Element of Nat_Lattice; ::_thesis: lcmlat . (p,q) = lcmlat . (q,p) thus lcmlat . (p,q) = q "\/" p by LATTICES:def_1 .= lcmlat . (q,p) ; ::_thesis: verum end; theorem Th6: :: NAT_LAT:6 for q, p being Element of Nat_Lattice holds hcflat . (q,p) = hcflat . (p,q) proof let q, p be Element of Nat_Lattice; ::_thesis: hcflat . (q,p) = hcflat . (p,q) thus hcflat . (q,p) = p "/\" q by LATTICES:def_2 .= hcflat . (p,q) ; ::_thesis: verum end; 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 let p, q, r be Element of Nat_Lattice; ::_thesis: lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (p,q)),r) set s = q "\/" r; thus lcmlat . (p,(lcmlat . (q,r))) = p "\/" (q "\/" r) .= (p "\/" q) "\/" r by NEWTON:43 .= lcmlat . ((lcmlat . (p,q)),r) ; ::_thesis: verum 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) ) proof let p, q, r be Element of Nat_Lattice; ::_thesis: ( 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) ) set s = r "\/" q; thus lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (p,q)),r) by Th7 .= lcmlat . ((lcmlat . (q,p)),r) by Th5 ; ::_thesis: ( 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) ) thus A1: lcmlat . (p,(lcmlat . (q,r))) = lcmlat . (p,(lcmlat . (r,q))) by Th5 .= lcmlat . ((lcmlat . (p,r)),q) by Th7 ; ::_thesis: ( lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (r,q)),p) & lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (r,p)),q) ) thus lcmlat . (p,(lcmlat . (q,r))) = lcmlat . (p,(r "\/" q)) by LATTICES:def_1 .= lcmlat . ((lcmlat . (r,q)),p) by Th5 ; ::_thesis: lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (r,p)),q) thus lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (r,p)),q) by A1, Th5; ::_thesis: verum 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 let p, q, r be Element of Nat_Lattice; ::_thesis: hcflat . (p,(hcflat . (q,r))) = hcflat . ((hcflat . (p,q)),r) set s = q "/\" r; thus hcflat . (p,(hcflat . (q,r))) = p "/\" (q "/\" r) .= (p "/\" q) "/\" r by NEWTON:48 .= hcflat . ((hcflat . (p,q)),r) ; ::_thesis: verum 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) ) proof let p, q, r be Element of Nat_Lattice; ::_thesis: ( 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) ) set s = r "/\" q; thus hcflat . (p,(hcflat . (q,r))) = hcflat . ((hcflat . (p,q)),r) by Th9 .= hcflat . ((hcflat . (q,p)),r) by Th6 ; ::_thesis: ( 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) ) thus A1: hcflat . (p,(hcflat . (q,r))) = hcflat . (p,(hcflat . (r,q))) by Th6 .= hcflat . ((hcflat . (p,r)),q) by Th9 ; ::_thesis: ( hcflat . (p,(hcflat . (q,r))) = hcflat . ((hcflat . (r,q)),p) & hcflat . (p,(hcflat . (q,r))) = hcflat . ((hcflat . (r,p)),q) ) thus hcflat . (p,(hcflat . (q,r))) = hcflat . (p,(r "/\" q)) by LATTICES:def_2 .= hcflat . ((hcflat . (r,q)),p) by Th6 ; ::_thesis: hcflat . (p,(hcflat . (q,r))) = hcflat . ((hcflat . (r,p)),q) thus hcflat . (p,(hcflat . (q,r))) = hcflat . ((hcflat . (r,p)),q) by A1, Th6; ::_thesis: verum 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 ) proof let q, p be Element of Nat_Lattice; ::_thesis: ( hcflat . (q,(lcmlat . (q,p))) = q & hcflat . ((lcmlat . (p,q)),q) = q & hcflat . (q,(lcmlat . (p,q))) = q & hcflat . ((lcmlat . (q,p)),q) = q ) set s = q "\/" p; thus A1: hcflat . (q,(lcmlat . (q,p))) = q "/\" (q "\/" p) .= q by NEWTON:54 ; ::_thesis: ( hcflat . ((lcmlat . (p,q)),q) = q & hcflat . (q,(lcmlat . (p,q))) = q & hcflat . ((lcmlat . (q,p)),q) = q ) thus A2: hcflat . ((lcmlat . (p,q)),q) = hcflat . ((p "\/" q),q) .= q "/\" (q "\/" p) by LATTICES:def_2 .= q by NEWTON:54 ; ::_thesis: ( hcflat . (q,(lcmlat . (p,q))) = q & hcflat . ((lcmlat . (q,p)),q) = q ) thus hcflat . (q,(lcmlat . (p,q))) = q by A1, Th5; ::_thesis: hcflat . ((lcmlat . (q,p)),q) = q thus hcflat . ((lcmlat . (q,p)),q) = q by A2, Th5; ::_thesis: verum 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 ) proof let q, p be Element of Nat_Lattice; ::_thesis: ( lcmlat . (q,(hcflat . (q,p))) = q & lcmlat . ((hcflat . (p,q)),q) = q & lcmlat . (q,(hcflat . (p,q))) = q & lcmlat . ((hcflat . (q,p)),q) = q ) set r = p "/\" q; thus A1: lcmlat . (q,(hcflat . (q,p))) = lcmlat . (q,(q "/\" p)) .= (p "/\" q) "\/" q by LATTICES:def_1 .= q by NEWTON:53 ; ::_thesis: ( lcmlat . ((hcflat . (p,q)),q) = q & lcmlat . (q,(hcflat . (p,q))) = q & lcmlat . ((hcflat . (q,p)),q) = q ) thus A2: lcmlat . ((hcflat . (p,q)),q) = (p "/\" q) "\/" q .= q by NEWTON:53 ; ::_thesis: ( lcmlat . (q,(hcflat . (p,q))) = q & lcmlat . ((hcflat . (q,p)),q) = q ) thus lcmlat . (q,(hcflat . (p,q))) = q by A1, Th6; ::_thesis: lcmlat . ((hcflat . (q,p)),q) = q thus lcmlat . ((hcflat . (q,p)),q) = q by A2, Th6; ::_thesis: verum end; definition func NATPLUS -> Subset of NAT means :Def6: :: NAT_LAT:def 6 for n being Nat holds ( n in it iff 0 < n ); existence ex b1 being Subset of NAT st for n being Nat holds ( n in b1 iff 0 < n ) proof defpred S1[ Nat] means 0 < $1; consider X being Subset of NAT such that A1: for n being Element of NAT holds ( n in X iff S1[n] ) from SUBSET_1:sch_3(); take X ; ::_thesis: for n being Nat holds ( n in X iff 0 < n ) let n be Nat; ::_thesis: ( n in X iff 0 < n ) thus ( n in X implies 0 < n ) by A1; ::_thesis: ( 0 < n implies n in X ) n in NAT by ORDINAL1:def_12; hence ( 0 < n implies n in X ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Subset of NAT st ( for n being Nat holds ( n in b1 iff 0 < n ) ) & ( for n being Nat holds ( n in b2 iff 0 < n ) ) holds b1 = b2 proof let X, Y be Subset of NAT; ::_thesis: ( ( for n being Nat holds ( n in X iff 0 < n ) ) & ( for n being Nat holds ( n in Y iff 0 < n ) ) implies X = Y ) assume that A2: for n being Nat holds ( n in X iff 0 < n ) and A3: for n being Nat holds ( n in Y iff 0 < n ) ; ::_thesis: X = Y thus X c= Y :: according to XBOOLE_0:def_10 ::_thesis: Y c= X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Y ) assume A4: x in X ; ::_thesis: x in Y then reconsider x = x as Nat ; 0 < x by A2, A4; hence x in Y by A3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y or x in X ) assume A5: x in Y ; ::_thesis: x in X then reconsider x = x as Nat ; 0 < x by A3, A5; hence x in X by A2; ::_thesis: verum end; end; :: deftheorem Def6 defines NATPLUS NAT_LAT:def_6_:_ for b1 being Subset of NAT holds ( b1 = NATPLUS iff for n being Nat holds ( n in b1 iff 0 < n ) ); registration cluster NATPLUS -> non empty ; coherence not NATPLUS is empty proof 0 < 1 ; hence not NATPLUS is empty by Def6; ::_thesis: verum end; end; 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 b1 being Element of N holds b1 is Element of S proof let x be Element of N; ::_thesis: x is Element of S thus x is Element of S ; ::_thesis: verum end; end; registration let D be Subset of REAL; cluster -> real for Element of D; coherence for b1 being Element of D holds b1 is real ; end; registration let D be Subset of NAT; cluster -> real for Element of D; coherence for b1 being Element of D holds b1 is real ; end; definition mode NatPlus is Element of NATPLUS ; end; definition let k be Nat; assume A1: k > 0 ; func @ k -> NatPlus equals :Def7: :: NAT_LAT:def 7 k; coherence k is NatPlus by A1, Def6; end; :: deftheorem Def7 defines @ NAT_LAT:def_7_:_ for k being Nat st k > 0 holds @ k = k; registration cluster -> non zero natural for Element of NATPLUS ; coherence for b1 being NatPlus holds ( b1 is natural & not b1 is zero ) by Def6; end; definition func hcflatplus -> BinOp of NATPLUS means :Def8: :: NAT_LAT:def 8 for m, n being NatPlus holds it . (m,n) = m gcd n; existence ex b1 being BinOp of NATPLUS st for m, n being NatPlus holds b1 . (m,n) = m gcd n proof deffunc H1( NatPlus, NatPlus) -> NatPlus = @ ($1 gcd $2); consider f being BinOp of NATPLUS such that A1: for m, n being NatPlus holds f . (m,n) = H1(m,n) from BINOP_1:sch_4(); take f ; ::_thesis: for m, n being NatPlus holds f . (m,n) = m gcd n let m, n be NatPlus; ::_thesis: f . (m,n) = m gcd n A2: f . (m,n) = @ (m gcd n) by A1; n > 0 by Def6; hence f . (m,n) = m gcd n by A2, Def7, NEWTON:58; ::_thesis: verum end; uniqueness for b1, b2 being BinOp of NATPLUS st ( for m, n being NatPlus holds b1 . (m,n) = m gcd n ) & ( for m, n being NatPlus holds b2 . (m,n) = m gcd n ) holds b1 = b2 proof deffunc H1( NatPlus, NatPlus) -> Element of NAT = $1 gcd $2; thus for o1, o2 being BinOp of NATPLUS st ( for a, b being NatPlus holds o1 . (a,b) = H1(a,b) ) & ( for a, b being NatPlus holds o2 . (a,b) = H1(a,b) ) holds o1 = o2 from BINOP_2:sch_2(); ::_thesis: verum 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 ex b1 being BinOp of NATPLUS st for m, n being NatPlus holds b1 . (m,n) = m lcm n proof deffunc H1( NatPlus, NatPlus) -> NatPlus = @ ($1 lcm $2); consider f being BinOp of NATPLUS such that A3: for m, n being NatPlus holds f . (m,n) = H1(m,n) from BINOP_1:sch_4(); take f ; ::_thesis: for m, n being NatPlus holds f . (m,n) = m lcm n let m, n be NatPlus; ::_thesis: f . (m,n) = m lcm n A4: ( m > 0 & n > 0 ) by Def6; thus f . (m,n) = H1(m,n) by A3 .= m lcm n by A4, Def7, NEWTON:59 ; ::_thesis: verum end; uniqueness for b1, b2 being BinOp of NATPLUS st ( for m, n being NatPlus holds b1 . (m,n) = m lcm n ) & ( for m, n being NatPlus holds b2 . (m,n) = m lcm n ) holds b1 = b2 proof deffunc H1( NatPlus, NatPlus) -> Element of NAT = $1 lcm $2; thus for o1, o2 being BinOp of NATPLUS st ( for a, b being NatPlus holds o1 . (a,b) = H1(a,b) ) & ( for a, b being NatPlus holds o2 . (a,b) = H1(a,b) ) holds o1 = o2 from BINOP_2:sch_2(); ::_thesis: verum end; end; :: deftheorem Def8 defines hcflatplus NAT_LAT:def_8_:_ for b1 being BinOp of NATPLUS holds ( b1 = hcflatplus iff for m, n being NatPlus holds b1 . (m,n) = m gcd n ); :: deftheorem Def9 defines lcmlatplus NAT_LAT:def_9_:_ for b1 being BinOp of NATPLUS holds ( b1 = lcmlatplus iff for m, n being NatPlus holds b1 . (m,n) = m lcm n ); definition func NatPlus_Lattice -> strict LattStr equals :: NAT_LAT:def 10 LattStr(# NATPLUS,lcmlatplus,hcflatplus #); coherence LattStr(# NATPLUS,lcmlatplus,hcflatplus #) is strict LattStr ; end; :: deftheorem defines NatPlus_Lattice NAT_LAT:def_10_:_ NatPlus_Lattice = LattStr(# NATPLUS,lcmlatplus,hcflatplus #); registration cluster NatPlus_Lattice -> non empty strict ; coherence not NatPlus_Lattice is empty ; end; definition let m be Element of NatPlus_Lattice; func @ m -> NatPlus equals :: NAT_LAT:def 11 m; coherence m is NatPlus ; end; :: deftheorem defines @ NAT_LAT:def_11_:_ for m being Element of NatPlus_Lattice holds @ m = m; registration cluster -> non zero natural for Element of the carrier of NatPlus_Lattice; coherence for b1 being Element of NatPlus_Lattice holds ( b1 is natural & not b1 is zero ) ; end; registration let p, q be Element of NatPlus_Lattice; identifyp "\/" q with p lcm q; compatibility p "\/" q = p lcm q by Def9; identifyp "/\" q with p gcd q; compatibility p "/\" q = p gcd q by Def8; end; theorem :: NAT_LAT:13 for p, q being Element of NatPlus_Lattice holds p "\/" q = (@ p) lcm (@ q) ; theorem :: NAT_LAT:14 for p, q being Element of NatPlus_Lattice holds p "/\" q = (@ p) gcd (@ q) ; 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 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; end; 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_) 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; definition let L be Lattice; 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 ex b1 being Lattice st ( the carrier of b1 c= the carrier of L & the L_join of b1 = the L_join of L || the carrier of b1 & the L_meet of b1 = the L_meet of L || the carrier of b1 ) proof take L ; ::_thesis: ( the carrier of L c= 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 ) thus ( the carrier of L c= 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 ) by Lm5; ::_thesis: verum end; end; :: deftheorem Def12 defines SubLattice NAT_LAT:def_12_:_ for L, b2 being Lattice holds ( b2 is SubLattice of L iff ( the carrier of b2 c= the carrier of L & the L_join of b2 = the L_join of L || the carrier of b2 & the L_meet of b2 = the L_meet of L || the carrier of b2 ) ); registration let L be Lattice; cluster non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like for SubLattice of L; existence ex b1 being SubLattice of L st b1 is strict proof set S = LattStr(# the carrier of L, the L_join of L, the L_meet of L #); A1: now__::_thesis:_for_a,_b,_c_being_Element_of_LattStr(#_the_carrier_of_L,_the_L_join_of_L,_the_L_meet_of_L_#)_holds_a_"\/"_(b_"\/"_c)_=_(a_"\/"_b)_"\/"_c let a, b, c be Element of LattStr(# the carrier of L, the L_join of L, the L_meet of L #); ::_thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c reconsider a9 = a, b9 = b, c9 = c as Element of L ; thus a "\/" (b "\/" c) = a9 "\/" (b9 "\/" c9) .= (a9 "\/" b9) "\/" c9 by LATTICES:def_5 .= (a "\/" b) "\/" c ; ::_thesis: verum end; A2: now__::_thesis:_for_a,_b_being_Element_of_LattStr(#_the_carrier_of_L,_the_L_join_of_L,_the_L_meet_of_L_#)_holds_(a_"/\"_b)_"\/"_b_=_b let a, b be Element of LattStr(# the carrier of L, the L_join of L, the L_meet of L #); ::_thesis: (a "/\" b) "\/" b = b reconsider a9 = a, b9 = b as Element of L ; thus (a "/\" b) "\/" b = (a9 "/\" b9) "\/" b9 .= b by LATTICES:def_8 ; ::_thesis: verum end; A3: now__::_thesis:_for_a,_b_being_Element_of_LattStr(#_the_carrier_of_L,_the_L_join_of_L,_the_L_meet_of_L_#)_holds_a_"/\"_(a_"\/"_b)_=_a let a, b be Element of LattStr(# the carrier of L, the L_join of L, the L_meet of L #); ::_thesis: a "/\" (a "\/" b) = a reconsider a9 = a, b9 = b as Element of L ; thus a "/\" (a "\/" b) = a9 "/\" (a9 "\/" b9) .= a by LATTICES:def_9 ; ::_thesis: verum end; A4: now__::_thesis:_for_a,_b,_c_being_Element_of_LattStr(#_the_carrier_of_L,_the_L_join_of_L,_the_L_meet_of_L_#)_holds_a_"/\"_(b_"/\"_c)_=_(a_"/\"_b)_"/\"_c let a, b, c be Element of LattStr(# the carrier of L, the L_join of L, the L_meet of L #); ::_thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c reconsider a9 = a, b9 = b, c9 = c as Element of L ; thus a "/\" (b "/\" c) = a9 "/\" (b9 "/\" c9) .= (a9 "/\" b9) "/\" c9 by LATTICES:def_7 .= (a "/\" b) "/\" c ; ::_thesis: verum end; A5: for a, b being Element of LattStr(# the carrier of L, the L_join of L, the L_meet of L #) for a9, b9 being Element of L st a = a9 & b = b9 holds ( a "\/" b = a9 "\/" b9 & a "/\" b = a9 "/\" b9 ) ; A6: now__::_thesis:_for_a,_b_being_Element_of_LattStr(#_the_carrier_of_L,_the_L_join_of_L,_the_L_meet_of_L_#)_holds_a_"/\"_b_=_b_"/\"_a let a, b be Element of LattStr(# the carrier of L, the L_join of L, the L_meet of L #); ::_thesis: a "/\" b = b "/\" a reconsider a9 = a, b9 = b as Element of L ; thus a "/\" b = b9 "/\" a9 by A5 .= b "/\" a ; ::_thesis: verum end; now__::_thesis:_for_a,_b_being_Element_of_LattStr(#_the_carrier_of_L,_the_L_join_of_L,_the_L_meet_of_L_#)_holds_a_"\/"_b_=_b_"\/"_a let a, b be Element of LattStr(# the carrier of L, the L_join of L, the L_meet of L #); ::_thesis: a "\/" b = b "\/" a reconsider a9 = a, b9 = b as Element of L ; thus a "\/" b = b9 "\/" a9 by A5 .= b "\/" a ; ::_thesis: verum end; then ( LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is join-commutative & LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is join-associative & LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is meet-absorbing & LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is meet-commutative & LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is meet-associative & LattStr(# the carrier of L, the L_join of L, the L_meet of L #) is join-absorbing ) by A1, A2, A6, A4, A3, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9; then reconsider S = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) as Lattice ; ( the L_join of S = the L_join of L || the carrier of S & the L_meet of S = the L_meet of L || the carrier of S ) by RELSET_1:19; then S is SubLattice of L by Def12; hence ex b1 being SubLattice of L st b1 is strict ; ::_thesis: verum end; end; theorem :: NAT_LAT:15 for L being Lattice holds L is SubLattice of L proof let L be Lattice; ::_thesis: L is SubLattice of L thus the carrier of L c= the carrier of L ; :: according to NAT_LAT:def_12 ::_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 ) thus ( 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 ) by Lm5; ::_thesis: verum end; theorem :: NAT_LAT:16 NatPlus_Lattice is SubLattice of Nat_Lattice proof A1: for x being set st x in dom hcflatplus holds hcflatplus . x = hcflat . x proof let x be set ; ::_thesis: ( x in dom hcflatplus implies hcflatplus . x = hcflat . x ) assume A2: x in dom hcflatplus ; ::_thesis: hcflatplus . x = hcflat . x then A3: x in [:NATPLUS,NATPLUS:] by FUNCT_2:def_1; consider y1, y2 being set such that A4: [y1,y2] = x by A2, RELAT_1:def_1; ( y1 in NATPLUS & y2 in NATPLUS ) by A3, A4, ZFMISC_1:87; then reconsider n = y1, k = y2 as Nat ; A5: hcflat . (n,k) = n gcd k by Def1; reconsider n = y1, k = y2 as NatPlus by A3, A4, ZFMISC_1:87; hcflatplus . (n,k) = hcflat . (n,k) by A5, Def8; hence hcflatplus . x = hcflat . x by A4; ::_thesis: verum end; ( dom hcflatplus = [:NATPLUS,NATPLUS:] & dom hcflat = [:NAT,NAT:] ) by FUNCT_2:def_1; then dom hcflatplus = (dom hcflat) /\ [:NATPLUS,NATPLUS:] by XBOOLE_1:28, ZFMISC_1:96; then A6: hcflatplus = hcflat || NATPLUS by A1, FUNCT_1:46; A7: for x being set st x in dom lcmlatplus holds lcmlatplus . x = lcmlat . x proof let x be set ; ::_thesis: ( x in dom lcmlatplus implies lcmlatplus . x = lcmlat . x ) assume A8: x in dom lcmlatplus ; ::_thesis: lcmlatplus . x = lcmlat . x then A9: x in [:NATPLUS,NATPLUS:] by FUNCT_2:def_1; consider y1, y2 being set such that A10: [y1,y2] = x by A8, RELAT_1:def_1; ( y1 in NATPLUS & y2 in NATPLUS ) by A9, A10, ZFMISC_1:87; then reconsider n = y1, k = y2 as Nat ; A11: lcmlat . (n,k) = n lcm k by Def2; reconsider n = y1, k = y2 as NatPlus by A9, A10, ZFMISC_1:87; lcmlatplus . (n,k) = lcmlat . (n,k) by A11, Def9; hence lcmlatplus . x = lcmlat . x by A10; ::_thesis: verum end; ( dom lcmlatplus = [:NATPLUS,NATPLUS:] & dom lcmlat = [:NAT,NAT:] ) by FUNCT_2:def_1; then dom lcmlatplus = (dom lcmlat) /\ [:NATPLUS,NATPLUS:] by XBOOLE_1:28, ZFMISC_1:96; then lcmlatplus = lcmlat || NATPLUS by A7, FUNCT_1:46; hence NatPlus_Lattice is SubLattice of Nat_Lattice by A6, Def12; ::_thesis: verum end;