:: J\'onsson Theorem about Representation of Modular Lattices :: by Mariusz {\L}api\'nski :: :: Received June 29, 2000 :: Copyright (c) 2000-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, ORDERS_2, XBOOLE_0, STRUCT_0, EQREL_1, SUBSET_1, FINSEQ_1, LATTICE5, LATTICES, WAYBEL_0, ZFMISC_1, GROUP_6, FUNCT_1, RELAT_1, XXREAL_0, FINSET_1, ABIAN, CARD_1, ARYTM_3, CAT_1, YELLOW_0, ORDINAL2, ORDINAL1, TARSKI, WELLORD1, SEQM_3, LATTICE3, WAYBEL_1, MCART_1, VALUED_0, RELAT_2, PARTFUN1, FUNCOP_1, FUNCT_6, NAT_1, FUNCT_2, LATTICE8, RECDEF_2; notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, FUNCT_6, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, ORDINAL2, MCART_1, DOMAIN_1, PARTFUN1, FUNCOP_1, STRUCT_0, ORDERS_2, EQREL_1, FINSEQ_1, LATTICE3, BINOP_1, YELLOW_0, YELLOW_2, LATTICE5, YELLOW11, WAYBEL_1, WAYBEL_0, ABIAN, XXREAL_0; constructors ORDINAL2, FUNCT_6, RFUNCT_3, ABIAN, REALSET2, ORDERS_3, WAYBEL_1, LATTICE5, YELLOW11, RELSET_1, XTUPLE_0, NUMBERS, XFAMILY; registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCOP_1, XREAL_0, INT_1, CARD_1, FINSEQ_1, EQREL_1, ABIAN, STRUCT_0, LATTICE3, YELLOW_0, YELLOW_2, WAYBEL_1, WAYBEL10, LATTICE5, YELLOW11, WAYBEL21, LATTICE7, ZFMISC_1, FUNCT_1, XTUPLE_0; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin :: Preliminaries definition let L be RelStr; attr L is finitely_typed means :: LATTICE8:def 1 ex A being non empty set st (for e being object st e in the carrier of L holds e is Equivalence_Relation of A) & ex o being Element of NAT st for e1,e2 being Equivalence_Relation of A, x,y being object st e1 in the carrier of L & e2 in the carrier of L & [x,y] in e1 "\/" e2 holds ex F being non empty FinSequence of A st len F = o & x,y are_joint_by F, e1,e2; end; definition let L be lower-bounded LATTICE; let n be Element of NAT; pred L has_a_representation_of_type<= n means :: LATTICE8:def 2 ex A being non trivial set, f be Homomorphism of L,EqRelLATT A st f is one-to-one & Image f is finitely_typed & (ex e being Equivalence_Relation of A st e in the carrier of Image f & e <> id A) & type_of Image f <= n; end; registration cluster lower-bounded distributive finite for LATTICE; end; registration let A be non trivial set; cluster non trivial finitely_typed full for non empty Sublattice of EqRelLATT A; end; theorem :: LATTICE8:1 for A be non empty set for L be lower-bounded LATTICE for d be distance_function of A,L holds succ {} c= DistEsti(d); theorem :: LATTICE8:2 for L being trivial Semilattice holds L is modular; theorem :: LATTICE8:3 for A being non empty set for L being non empty Sublattice of EqRelLATT A holds L is trivial or ex e being Equivalence_Relation of A st e in the carrier of L & e <> id A; theorem :: LATTICE8:4 for L1,L2 be lower-bounded LATTICE for f being Function of L1,L2 st f is infs-preserving sups-preserving holds f is meet-preserving join-preserving; theorem :: LATTICE8:5 for L1,L2 be lower-bounded LATTICE st L1,L2 are_isomorphic & L1 is modular holds L2 is modular; theorem :: LATTICE8:6 for S being lower-bounded non empty Poset for T being non empty Poset for f being monotone Function of S,T holds Image f is lower-bounded; theorem :: LATTICE8:7 for L being lower-bounded LATTICE for x,y being Element of L for A being non empty set for f be Homomorphism of L,EqRelLATT A st f is one-to-one holds (corestr f).x <= (corestr f).y implies x <= y; begin theorem :: LATTICE8:8 for A being non trivial set for L being finitely_typed full non empty Sublattice of EqRelLATT A for e being Equivalence_Relation of A st e in the carrier of L & e <> id A holds type_of L <= 2 implies L is modular; theorem :: LATTICE8:9 for L be lower-bounded LATTICE holds L has_a_representation_of_type<= 2 implies L is modular; :: <= :: L is modular implies L has_a_representation_of_type<= 2 definition let A be set; func new_set2 A -> set equals :: LATTICE8:def 3 A \/ {{A}, {{A}}}; end; registration let A be set; cluster new_set2 A -> non empty; end; definition let A be non empty set; let L be lower-bounded LATTICE; let d be BiFunction of A,L; let q be Element of [:A,A,the carrier of L,the carrier of L:]; func new_bi_fun2(d,q) -> BiFunction of new_set2 A,L means :: LATTICE8:def 4 (for u,v being Element of A holds it.(u,v) = d.(u,v)) & it.({A},{A}) = Bottom L & it.({{A}},{{A}}) = Bottom L & it.({A},{{A}}) = (d.(q`1_4,q`2_4)"\/"(q`3_4))"/\"(q`4_4) & it.({{A} },{A}) = (d.(q`1_4,q`2_4)"\/"(q`3_4))"/\"(q`4_4) & for u being Element of A holds it.(u,{A}) = d.(u,q`1_4)"\/"(q`3_4) & it.({A},u) = d.(u,q`1_4)"\/"(q`3_4) & it.(u,{{A}}) = d.(u,q`2_4) "\/"(q`3_4) & it.({{A}},u) = d.(u,q`2_4)"\/"(q`3_4); end; theorem :: LATTICE8:10 for A being non empty set for L being lower-bounded LATTICE for d being BiFunction of A,L st d is zeroed for q being Element of [:A,A,the carrier of L,the carrier of L:] holds new_bi_fun2(d,q) is zeroed; theorem :: LATTICE8:11 for A being non empty set for L being lower-bounded LATTICE for d being BiFunction of A,L st d is symmetric for q being Element of [:A,A,the carrier of L,the carrier of L:] holds new_bi_fun2(d,q) is symmetric; theorem :: LATTICE8:12 for A being non empty set for L being lower-bounded LATTICE st L is modular for d being BiFunction of A,L st d is symmetric & d is u.t.i. for q being Element of [:A,A,the carrier of L,the carrier of L:] st d.(q`1_4,q`2_4) <= (q`3_4)"\/"(q`4_4) holds new_bi_fun2(d,q) is u.t.i.; theorem :: LATTICE8:13 for A being non empty set for L being lower-bounded LATTICE for d be BiFunction of A,L for q be Element of [:A,A,the carrier of L,the carrier of L:] holds d c= new_bi_fun2(d,q); reserve x for set, C for Ordinal, L0 for Sequence; definition let A be non empty set; let O be Ordinal; func ConsecutiveSet2(A,O) -> set means :: LATTICE8:def 5 ex L0 being Sequence st it = last L0 & dom L0 = succ O & L0.0 = A & (for C being Ordinal st succ C in succ O holds L0.succ C = new_set2(L0.C)) & for C being Ordinal st C in succ O & C <> 0 & C is limit_ordinal holds L0.C = union rng (L0|C); end; theorem :: LATTICE8:14 for A being non empty set holds ConsecutiveSet2(A,0) = A; theorem :: LATTICE8:15 for A being non empty set for O being Ordinal holds ConsecutiveSet2(A,succ O) = new_set2 ConsecutiveSet2(A,O); theorem :: LATTICE8:16 for A being non empty set for O being Ordinal for T being Sequence holds O <> 0 & O is limit_ordinal & dom T = O & (for O1 being Ordinal st O1 in O holds T.O1 = ConsecutiveSet2(A,O1)) implies ConsecutiveSet2( A,O) = union rng T; reserve O1,O2 for Ordinal; registration let A be non empty set; let O be Ordinal; cluster ConsecutiveSet2(A,O) -> non empty; end; theorem :: LATTICE8:17 for A being non empty set for O being Ordinal holds A c= ConsecutiveSet2(A,O) ; definition let A be non empty set; let L be lower-bounded LATTICE; let d be BiFunction of A,L; let q be QuadrSeq of d; let O be Ordinal; assume O in dom q; func Quadr2(q,O) -> Element of [:ConsecutiveSet2(A,O),ConsecutiveSet2(A,O), the carrier of L,the carrier of L:] equals :: LATTICE8:def 6 q.O; end; definition let A be non empty set; let L be lower-bounded LATTICE; let d be BiFunction of A,L; let q be QuadrSeq of d; let O be Ordinal; func ConsecutiveDelta2(q,O) -> set means :: LATTICE8:def 7 ex L0 being Sequence st it = last L0 & dom L0 = succ O & L0.0 = d & (for C being Ordinal st succ C in succ O holds L0.succ C = new_bi_fun2(BiFun(L0.C,ConsecutiveSet2(A,C),L),Quadr2(q,C))) & for C being Ordinal st C in succ O & C <> 0 & C is limit_ordinal holds L0.C = union rng(L0|C); end; theorem :: LATTICE8:18 for A being non empty set for L be lower-bounded LATTICE for d being BiFunction of A,L for q being QuadrSeq of d holds ConsecutiveDelta2(q,0) = d; theorem :: LATTICE8:19 for A being non empty set for L be lower-bounded LATTICE for d be BiFunction of A,L for q being QuadrSeq of d for O being Ordinal holds ConsecutiveDelta2(q,succ O) = new_bi_fun2(BiFun(ConsecutiveDelta2(q,O), ConsecutiveSet2(A,O),L),Quadr2(q,O)); theorem :: LATTICE8:20 for A being non empty set for L be lower-bounded LATTICE for d be BiFunction of A,L for q being QuadrSeq of d for T being Sequence for O being Ordinal holds O <> 0 & O is limit_ordinal & dom T = O & (for O1 being Ordinal st O1 in O holds T.O1 = ConsecutiveDelta2(q,O1)) implies ConsecutiveDelta2(q,O) = union rng T; theorem :: LATTICE8:21 for A being non empty set for O,O1,O2 being Ordinal holds O1 c= O2 implies ConsecutiveSet2(A,O1) c= ConsecutiveSet2(A,O2); theorem :: LATTICE8:22 for A being non empty set for L be lower-bounded LATTICE for d be BiFunction of A,L for q being QuadrSeq of d for O being Ordinal holds ConsecutiveDelta2(q,O) is BiFunction of ConsecutiveSet2(A,O),L; definition let A be non empty set; let L be lower-bounded LATTICE; let d be BiFunction of A,L; let q be QuadrSeq of d; let O be Ordinal; redefine func ConsecutiveDelta2(q,O) -> BiFunction of ConsecutiveSet2(A,O),L; end; theorem :: LATTICE8:23 for A being non empty set for L be lower-bounded LATTICE for d be BiFunction of A,L for q being QuadrSeq of d for O being Ordinal holds d c= ConsecutiveDelta2(q,O); theorem :: LATTICE8:24 for A being non empty set for L be lower-bounded LATTICE for d being BiFunction of A,L for O1,O2 being Ordinal for q being QuadrSeq of d st O1 c= O2 holds ConsecutiveDelta2(q,O1) c= ConsecutiveDelta2(q,O2); theorem :: LATTICE8:25 for A being non empty set for L be lower-bounded LATTICE for d be BiFunction of A,L st d is zeroed for q being QuadrSeq of d for O being Ordinal holds ConsecutiveDelta2(q,O) is zeroed; theorem :: LATTICE8:26 for A being non empty set for L be lower-bounded LATTICE for d be BiFunction of A,L st d is symmetric for q being QuadrSeq of d for O being Ordinal holds ConsecutiveDelta2(q,O) is symmetric; theorem :: LATTICE8:27 for A being non empty set for L being lower-bounded LATTICE st L is modular for d be BiFunction of A,L st d is symmetric u.t.i. for O being Ordinal for q being QuadrSeq of d st O c= DistEsti(d) holds ConsecutiveDelta2(q ,O) is u.t.i.; theorem :: LATTICE8:28 for A being non empty set for L being lower-bounded modular LATTICE for d being distance_function of A,L for O being Ordinal for q being QuadrSeq of d st O c= DistEsti(d) holds ConsecutiveDelta2(q,O) is distance_function of ConsecutiveSet2(A,O),L; definition let A be non empty set; let L be lower-bounded LATTICE; let d be BiFunction of A,L; func NextSet2(d) -> set equals :: LATTICE8:def 8 ConsecutiveSet2(A,DistEsti(d)); end; registration let A be non empty set; let L be lower-bounded LATTICE; let d be BiFunction of A,L; cluster NextSet2(d) -> non empty; end; definition let A be non empty set; let L be lower-bounded LATTICE; let d be BiFunction of A,L; let q be QuadrSeq of d; func NextDelta2(q) -> set equals :: LATTICE8:def 9 ConsecutiveDelta2(q,DistEsti(d)); end; definition let A be non empty set; let L be lower-bounded modular LATTICE; let d be distance_function of A,L; let q be QuadrSeq of d; redefine func NextDelta2(q) -> distance_function of NextSet2(d),L; end; definition let A be non empty set; let L be lower-bounded LATTICE; let d be distance_function of A,L; let Aq be non empty set; let dq be distance_function of Aq,L; pred Aq, dq is_extension2_of A,d means :: LATTICE8:def 10 ex q being QuadrSeq of d st Aq = NextSet2(d) & dq = NextDelta2(q); end; theorem :: LATTICE8:29 for A being non empty set for L be lower-bounded LATTICE for d be distance_function of A,L for Aq be non empty set for dq be distance_function of Aq,L st Aq, dq is_extension2_of A,d for x,y being Element of A, a,b being Element of L st d.(x,y) <= a "\/" b ex z1,z2 being Element of Aq st dq.(x,z1) = a & dq.(z1,z2) = (d.(x,y) "\/" a) "/\" b & dq.(z2,y) = a; definition let A be non empty set; let L be lower-bounded modular LATTICE; let d be distance_function of A,L; mode ExtensionSeq2 of A,d -> Function means :: LATTICE8:def 11 dom it = NAT & it.0 = [A ,d] & for n being Nat holds ex A9 being non empty set, d9 being distance_function of A9,L, Aq being non empty set, dq being distance_function of Aq,L st Aq, dq is_extension2_of A9,d9 & it.n = [A9,d9] & it.(n+1) = [Aq,dq]; end; theorem :: LATTICE8:30 for A being non empty set for L be lower-bounded modular LATTICE for d be distance_function of A,L for S being ExtensionSeq2 of A,d for k,l being Nat st k <= l holds (S.k)`1 c= (S.l)`1; theorem :: LATTICE8:31 for A being non empty set for L be lower-bounded modular LATTICE for d be distance_function of A,L for S being ExtensionSeq2 of A,d for k,l being Nat st k <= l holds (S.k)`2 c= (S.l)`2; theorem :: LATTICE8:32 for L be lower-bounded modular LATTICE for S being ExtensionSeq2 of the carrier of L, BasicDF(L) for FS being non empty set st FS = union the set of all (S.i )`1 where i is Element of NAT holds union the set of all (S.i)`2 where i is Element of NAT is distance_function of FS,L; theorem :: LATTICE8:33 for L be lower-bounded modular LATTICE for S being ExtensionSeq2 of the carrier of L, BasicDF(L) for FS being non empty set for FD being distance_function of FS,L for x,y being Element of FS for a,b being Element of L st FS = union the set of all (S.i)`1 where i is Element of NAT & FD = union the set of all (S.i)`2 where i is Element of NAT & FD.(x,y) <= a "\/"b ex z1,z2 being Element of FS st FD.(x,z1) = a & FD.(z1,z2) = (FD.(x,y) "\/"a)"/\"b & FD.(z2,y) = a; theorem :: LATTICE8:34 for L be lower-bounded modular LATTICE for S being ExtensionSeq2 of the carrier of L, BasicDF(L) for FS being non empty set for FD being distance_function of FS,L for f being Homomorphism of L,EqRelLATT FS for e1,e2 being Equivalence_Relation of FS for x,y being object st f = alpha FD & FS = union the set of all (S.i)`1 where i is Element of NAT & FD = union the set of all (S.i)`2 where i is Element of NAT & e1 in the carrier of Image f & e2 in the carrier of Image f & [x,y] in e1 "\/" e2 ex F being non empty FinSequence of FS st len F = 2+2 & x,y are_joint_by F,e1,e2; theorem :: LATTICE8:35 for L be lower-bounded modular LATTICE holds L has_a_representation_of_type<= 2; :: <=> :: L has_a_representation_of_type<= 2 iff L is modular ::$N Jonsson Theorem for modular lattices theorem :: LATTICE8:36 for L be lower-bounded LATTICE holds L has_a_representation_of_type<= 2 iff L is modular;