:: J\'onsson Theorem about Representation of Modular Lattices :: by Mariusz {\L}api\'nski :: :: Received June 29, 2000 :: Copyright (c) 2000-2012 Association of Mizar Users begin definition let L be RelStr ; attrL is finitely_typed means :Def1: :: LATTICE8:def 1 ex A being non empty set st ( ( for e being set 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 for x, y being set 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; :: deftheorem Def1 defines finitely_typed LATTICE8:def_1_:_ for L being RelStr holds ( L is finitely_typed iff ex A being non empty set st ( ( for e being set 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 for x, y being set 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 ) ) ); definition let L be lower-bounded LATTICE; let n be Element of NAT ; predL has_a_representation_of_type<= n means :Def2: :: LATTICE8:def 2 ex A being non trivial set ex f being Homomorphism of L,(EqRelLATT A) st ( f is V14() & 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; :: deftheorem Def2 defines has_a_representation_of_type<= LATTICE8:def_2_:_ for L being lower-bounded LATTICE for n being Element of NAT holds ( L has_a_representation_of_type<= n iff ex A being non trivial set ex f being Homomorphism of L,(EqRelLATT A) st ( f is V14() & 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 ) ); registration cluster non empty finite reflexive transitive antisymmetric lower-bounded distributive with_suprema with_infima for RelStr ; existence ex b1 being LATTICE st ( b1 is lower-bounded & b1 is distributive & b1 is finite ) proofend; end; Lm1: 1 is odd proofend; Lm2: 2 is even proofend; registration let A be non trivial set ; cluster non empty non trivial full meet-inheriting join-inheriting finitely_typed for SubRelStr of EqRelLATT A; existence ex b1 being non empty Sublattice of EqRelLATT A st ( not b1 is trivial & b1 is finitely_typed & b1 is full ) proofend; end; theorem Th1: :: LATTICE8:1 for A being non empty set for L being lower-bounded LATTICE for d being distance_function of A,L holds succ {} c= DistEsti d proofend; theorem :: LATTICE8:2 for L being trivial Semilattice holds L is modular proofend; 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 ) ) proofend; theorem Th4: :: LATTICE8:4 for L1, L2 being lower-bounded LATTICE for f being Function of L1,L2 st f is infs-preserving & f is sups-preserving holds ( f is meet-preserving & f is join-preserving ) proofend; theorem Th5: :: LATTICE8:5 for L1, L2 being lower-bounded LATTICE st L1,L2 are_isomorphic & L1 is modular holds L2 is modular proofend; theorem Th6: :: LATTICE8:6 for S being non empty lower-bounded Poset for T being non empty Poset for f being monotone Function of S,T holds Image f is lower-bounded proofend; theorem Th7: :: LATTICE8:7 for L being lower-bounded LATTICE for x, y being Element of L for A being non empty set for f being Homomorphism of L,(EqRelLATT A) st f is V14() & (corestr f) . x <= (corestr f) . y holds x <= y proofend; begin :: => :: L has_a_representation_of_type<= 2 implies L is modular theorem Th8: :: LATTICE8:8 for A being non trivial set for L being non empty full finitely_typed Sublattice of EqRelLATT A for e being Equivalence_Relation of A st e in the carrier of L & e <> id A & type_of L <= 2 holds L is modular proofend; theorem Th9: :: LATTICE8:9 for L being lower-bounded LATTICE st L has_a_representation_of_type<= 2 holds L is modular proofend; :: <= :: 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}}}; correctness coherence A \/ {{A},{{A}}} is set ; ; end; :: deftheorem defines new_set2 LATTICE8:def_3_:_ for A being set holds new_set2 A = A \/ {{A},{{A}}}; registration let A be set ; cluster new_set2 A -> non empty ; coherence not new_set2 A is 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 :Def4: :: 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) ) ) ); existence ex b1 being BiFunction of (new_set2 A),L st ( ( for u, v being Element of A holds b1 . (u,v) = d . (u,v) ) & b1 . ({A},{A}) = Bottom L & b1 . ({{A}},{{A}}) = Bottom L & b1 . ({A},{{A}}) = ((d . ((q `1_4),(q `2_4))) "\/" (q `3_4)) "/\" (q `4_4) & b1 . ({{A}},{A}) = ((d . ((q `1_4),(q `2_4))) "\/" (q `3_4)) "/\" (q `4_4) & ( for u being Element of A holds ( b1 . (u,{A}) = (d . (u,(q `1_4))) "\/" (q `3_4) & b1 . ({A},u) = (d . (u,(q `1_4))) "\/" (q `3_4) & b1 . (u,{{A}}) = (d . (u,(q `2_4))) "\/" (q `3_4) & b1 . ({{A}},u) = (d . (u,(q `2_4))) "\/" (q `3_4) ) ) ) proofend; uniqueness for b1, b2 being BiFunction of (new_set2 A),L st ( for u, v being Element of A holds b1 . (u,v) = d . (u,v) ) & b1 . ({A},{A}) = Bottom L & b1 . ({{A}},{{A}}) = Bottom L & b1 . ({A},{{A}}) = ((d . ((q `1_4),(q `2_4))) "\/" (q `3_4)) "/\" (q `4_4) & b1 . ({{A}},{A}) = ((d . ((q `1_4),(q `2_4))) "\/" (q `3_4)) "/\" (q `4_4) & ( for u being Element of A holds ( b1 . (u,{A}) = (d . (u,(q `1_4))) "\/" (q `3_4) & b1 . ({A},u) = (d . (u,(q `1_4))) "\/" (q `3_4) & b1 . (u,{{A}}) = (d . (u,(q `2_4))) "\/" (q `3_4) & b1 . ({{A}},u) = (d . (u,(q `2_4))) "\/" (q `3_4) ) ) & ( for u, v being Element of A holds b2 . (u,v) = d . (u,v) ) & b2 . ({A},{A}) = Bottom L & b2 . ({{A}},{{A}}) = Bottom L & b2 . ({A},{{A}}) = ((d . ((q `1_4),(q `2_4))) "\/" (q `3_4)) "/\" (q `4_4) & b2 . ({{A}},{A}) = ((d . ((q `1_4),(q `2_4))) "\/" (q `3_4)) "/\" (q `4_4) & ( for u being Element of A holds ( b2 . (u,{A}) = (d . (u,(q `1_4))) "\/" (q `3_4) & b2 . ({A},u) = (d . (u,(q `1_4))) "\/" (q `3_4) & b2 . (u,{{A}}) = (d . (u,(q `2_4))) "\/" (q `3_4) & b2 . ({{A}},u) = (d . (u,(q `2_4))) "\/" (q `3_4) ) ) holds b1 = b2 proofend; end; :: deftheorem Def4 defines new_bi_fun2 LATTICE8:def_4_:_ for A being non empty set for L being lower-bounded LATTICE for d being BiFunction of A,L for q being Element of [:A,A, the carrier of L, the carrier of L:] for b5 being BiFunction of (new_set2 A),L holds ( b5 = new_bi_fun2 (d,q) iff ( ( for u, v being Element of A holds b5 . (u,v) = d . (u,v) ) & b5 . ({A},{A}) = Bottom L & b5 . ({{A}},{{A}}) = Bottom L & b5 . ({A},{{A}}) = ((d . ((q `1_4),(q `2_4))) "\/" (q `3_4)) "/\" (q `4_4) & b5 . ({{A}},{A}) = ((d . ((q `1_4),(q `2_4))) "\/" (q `3_4)) "/\" (q `4_4) & ( for u being Element of A holds ( b5 . (u,{A}) = (d . (u,(q `1_4))) "\/" (q `3_4) & b5 . ({A},u) = (d . (u,(q `1_4))) "\/" (q `3_4) & b5 . (u,{{A}}) = (d . (u,(q `2_4))) "\/" (q `3_4) & b5 . ({{A}},u) = (d . (u,(q `2_4))) "\/" (q `3_4) ) ) ) ); theorem Th10: :: 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 holds for q being Element of [:A,A, the carrier of L, the carrier of L:] holds new_bi_fun2 (d,q) is zeroed proofend; theorem Th11: :: 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 holds for q being Element of [:A,A, the carrier of L, the carrier of L:] holds new_bi_fun2 (d,q) is symmetric proofend; theorem Th12: :: LATTICE8:12 for A being non empty set for L being lower-bounded LATTICE st L is modular holds for d being BiFunction of A,L st d is symmetric & d is u.t.i. holds 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. proofend; theorem Th13: :: LATTICE8:13 for A being non empty set for L being lower-bounded LATTICE for d being BiFunction of A,L for q being Element of [:A,A, the carrier of L, the carrier of L:] holds d c= new_bi_fun2 (d,q) proofend; definition let A be non empty set ; let O be Ordinal; func ConsecutiveSet2 (A,O) -> set means :Def5: :: LATTICE8:def 5 ex L0 being T-Sequence st ( it = last L0 & dom L0 = succ O & L0 . {} = 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 <> {} & C is limit_ordinal holds L0 . C = union (rng (L0 | C)) ) ); correctness existence ex b1 being set ex L0 being T-Sequence st ( b1 = last L0 & dom L0 = succ O & L0 . {} = 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 <> {} & C is limit_ordinal holds L0 . C = union (rng (L0 | C)) ) ); uniqueness for b1, b2 being set st ex L0 being T-Sequence st ( b1 = last L0 & dom L0 = succ O & L0 . {} = 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 <> {} & C is limit_ordinal holds L0 . C = union (rng (L0 | C)) ) ) & ex L0 being T-Sequence st ( b2 = last L0 & dom L0 = succ O & L0 . {} = 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 <> {} & C is limit_ordinal holds L0 . C = union (rng (L0 | C)) ) ) holds b1 = b2; proofend; end; :: deftheorem Def5 defines ConsecutiveSet2 LATTICE8:def_5_:_ for A being non empty set for O being Ordinal for b3 being set holds ( b3 = ConsecutiveSet2 (A,O) iff ex L0 being T-Sequence st ( b3 = last L0 & dom L0 = succ O & L0 . {} = 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 <> {} & C is limit_ordinal holds L0 . C = union (rng (L0 | C)) ) ) ); theorem Th14: :: LATTICE8:14 for A being non empty set holds ConsecutiveSet2 (A,{}) = A proofend; theorem Th15: :: LATTICE8:15 for A being non empty set for O being Ordinal holds ConsecutiveSet2 (A,(succ O)) = new_set2 (ConsecutiveSet2 (A,O)) proofend; theorem Th16: :: LATTICE8:16 for A being non empty set for O being Ordinal for T being T-Sequence st O <> {} & O is limit_ordinal & dom T = O & ( for O1 being Ordinal st O1 in O holds T . O1 = ConsecutiveSet2 (A,O1) ) holds ConsecutiveSet2 (A,O) = union (rng T) proofend; registration let A be non empty set ; let O be Ordinal; cluster ConsecutiveSet2 (A,O) -> non empty ; coherence not ConsecutiveSet2 (A,O) is empty proofend; end; theorem Th17: :: LATTICE8:17 for A being non empty set for O being Ordinal holds A c= ConsecutiveSet2 (A,O) proofend; 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 A1: 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 :Def6: :: LATTICE8:def 6 q . O; correctness coherence q . O is Element of [:(ConsecutiveSet2 (A,O)),(ConsecutiveSet2 (A,O)), the carrier of L, the carrier of L:]; proofend; end; :: deftheorem Def6 defines Quadr2 LATTICE8:def_6_:_ for A being non empty set for L being lower-bounded LATTICE for d being BiFunction of A,L for q being QuadrSeq of d for O being Ordinal st O in dom q holds Quadr2 (q,O) = q . 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; func ConsecutiveDelta2 (q,O) -> set means :Def7: :: LATTICE8:def 7 ex L0 being T-Sequence st ( it = last L0 & dom L0 = succ O & L0 . {} = 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 <> {} & C is limit_ordinal holds L0 . C = union (rng (L0 | C)) ) ); correctness existence ex b1 being set ex L0 being T-Sequence st ( b1 = last L0 & dom L0 = succ O & L0 . {} = 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 <> {} & C is limit_ordinal holds L0 . C = union (rng (L0 | C)) ) ); uniqueness for b1, b2 being set st ex L0 being T-Sequence st ( b1 = last L0 & dom L0 = succ O & L0 . {} = 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 <> {} & C is limit_ordinal holds L0 . C = union (rng (L0 | C)) ) ) & ex L0 being T-Sequence st ( b2 = last L0 & dom L0 = succ O & L0 . {} = 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 <> {} & C is limit_ordinal holds L0 . C = union (rng (L0 | C)) ) ) holds b1 = b2; proofend; end; :: deftheorem Def7 defines ConsecutiveDelta2 LATTICE8:def_7_:_ for A being non empty set for L being lower-bounded LATTICE for d being BiFunction of A,L for q being QuadrSeq of d for O being Ordinal for b6 being set holds ( b6 = ConsecutiveDelta2 (q,O) iff ex L0 being T-Sequence st ( b6 = last L0 & dom L0 = succ O & L0 . {} = 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 <> {} & C is limit_ordinal holds L0 . C = union (rng (L0 | C)) ) ) ); theorem Th18: :: LATTICE8:18 for A being non empty set for L being lower-bounded LATTICE for d being BiFunction of A,L for q being QuadrSeq of d holds ConsecutiveDelta2 (q,{}) = d proofend; theorem Th19: :: LATTICE8:19 for A being non empty set for L being lower-bounded LATTICE for d being 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))) proofend; theorem Th20: :: LATTICE8:20 for A being non empty set for L being lower-bounded LATTICE for d being BiFunction of A,L for q being QuadrSeq of d for T being T-Sequence for O being Ordinal st O <> {} & O is limit_ordinal & dom T = O & ( for O1 being Ordinal st O1 in O holds T . O1 = ConsecutiveDelta2 (q,O1) ) holds ConsecutiveDelta2 (q,O) = union (rng T) proofend; theorem Th21: :: LATTICE8:21 for A being non empty set for O, O1, O2 being Ordinal st O1 c= O2 holds ConsecutiveSet2 (A,O1) c= ConsecutiveSet2 (A,O2) proofend; theorem Th22: :: LATTICE8:22 for A being non empty set for L being lower-bounded LATTICE for d being 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 proofend; 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; :: original:ConsecutiveDelta2 redefine func ConsecutiveDelta2 (q,O) -> BiFunction of (ConsecutiveSet2 (A,O)),L; coherence ConsecutiveDelta2 (q,O) is BiFunction of (ConsecutiveSet2 (A,O)),L by Th22; end; theorem Th23: :: LATTICE8:23 for A being non empty set for L being lower-bounded LATTICE for d being BiFunction of A,L for q being QuadrSeq of d for O being Ordinal holds d c= ConsecutiveDelta2 (q,O) proofend; theorem Th24: :: LATTICE8:24 for A being non empty set for L being 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) proofend; theorem Th25: :: LATTICE8:25 for A being non empty set for L being lower-bounded LATTICE for d being BiFunction of A,L st d is zeroed holds for q being QuadrSeq of d for O being Ordinal holds ConsecutiveDelta2 (q,O) is zeroed proofend; theorem Th26: :: LATTICE8:26 for A being non empty set for L being lower-bounded LATTICE for d being BiFunction of A,L st d is symmetric holds for q being QuadrSeq of d for O being Ordinal holds ConsecutiveDelta2 (q,O) is symmetric proofend; theorem Th27: :: LATTICE8:27 for A being non empty set for L being lower-bounded LATTICE st L is modular holds for d being BiFunction of A,L st d is symmetric & d is u.t.i. holds for O being Ordinal for q being QuadrSeq of d st O c= DistEsti d holds ConsecutiveDelta2 (q,O) is u.t.i. proofend; 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 by Th25, Th26, Th27; 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)); correctness coherence ConsecutiveSet2 (A,(DistEsti d)) is set ; ; end; :: deftheorem defines NextSet2 LATTICE8:def_8_:_ for A being non empty set for L being lower-bounded LATTICE for d being BiFunction of A,L holds NextSet2 d = ConsecutiveSet2 (A,(DistEsti d)); 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 ; coherence not NextSet2 d is 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)); correctness coherence ConsecutiveDelta2 (q,(DistEsti d)) is set ; ; end; :: deftheorem defines NextDelta2 LATTICE8:def_9_:_ for A being non empty set for L being lower-bounded LATTICE for d being BiFunction of A,L for q being QuadrSeq of d holds NextDelta2 q = ConsecutiveDelta2 (q,(DistEsti d)); 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; :: original:NextDelta2 redefine func NextDelta2 q -> distance_function of (NextSet2 d),L; coherence NextDelta2 q is distance_function of (NextSet2 d),L by Th25, Th26, Th27; 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; predAq,dq is_extension2_of A,d means :Def10: :: LATTICE8:def 10 ex q being QuadrSeq of d st ( Aq = NextSet2 d & dq = NextDelta2 q ); end; :: deftheorem Def10 defines is_extension2_of LATTICE8:def_10_:_ for A being non empty set for L being lower-bounded LATTICE for d being distance_function of A,L for Aq being non empty set for dq being distance_function of Aq,L holds ( Aq,dq is_extension2_of A,d iff ex q being QuadrSeq of d st ( Aq = NextSet2 d & dq = NextDelta2 q ) ); theorem Th29: :: LATTICE8:29 for A being non empty set for L being lower-bounded LATTICE for d being distance_function of A,L for Aq being non empty set for dq being distance_function of Aq,L st Aq,dq is_extension2_of A,d holds for x, y being Element of A for a, b being Element of L st d . (x,y) <= a "\/" b holds ex z1, z2 being Element of Aq st ( dq . (x,z1) = a & dq . (z1,z2) = ((d . (x,y)) "\/" a) "/\" b & dq . (z2,y) = a ) proofend; 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 :Def11: :: LATTICE8:def 11 ( dom it = NAT & it . 0 = [A,d] & ( for n being Element of NAT ex A9 being non empty set ex d9 being distance_function of A9,L ex Aq being non empty set ex dq being distance_function of Aq,L st ( Aq,dq is_extension2_of A9,d9 & it . n = [A9,d9] & it . (n + 1) = [Aq,dq] ) ) ); existence ex b1 being Function st ( dom b1 = NAT & b1 . 0 = [A,d] & ( for n being Element of NAT ex A9 being non empty set ex d9 being distance_function of A9,L ex Aq being non empty set ex dq being distance_function of Aq,L st ( Aq,dq is_extension2_of A9,d9 & b1 . n = [A9,d9] & b1 . (n + 1) = [Aq,dq] ) ) ) proofend; end; :: deftheorem Def11 defines ExtensionSeq2 LATTICE8:def_11_:_ for A being non empty set for L being lower-bounded modular LATTICE for d being distance_function of A,L for b4 being Function holds ( b4 is ExtensionSeq2 of A,d iff ( dom b4 = NAT & b4 . 0 = [A,d] & ( for n being Element of NAT ex A9 being non empty set ex d9 being distance_function of A9,L ex Aq being non empty set ex dq being distance_function of Aq,L st ( Aq,dq is_extension2_of A9,d9 & b4 . n = [A9,d9] & b4 . (n + 1) = [Aq,dq] ) ) ) ); theorem Th30: :: LATTICE8:30 for A being non empty set for L being lower-bounded modular LATTICE for d being distance_function of A,L for S being ExtensionSeq2 of A,d for k, l being Element of NAT st k <= l holds (S . k) `1 c= (S . l) `1 proofend; theorem Th31: :: LATTICE8:31 for A being non empty set for L being lower-bounded modular LATTICE for d being distance_function of A,L for S being ExtensionSeq2 of A,d for k, l being Element of NAT st k <= l holds (S . k) `2 c= (S . l) `2 proofend; theorem Th32: :: LATTICE8:32 for L being lower-bounded modular LATTICE for S being ExtensionSeq2 of the carrier of L, BasicDF L for FS being non empty set st FS = union { ((S . i) `1) where i is Element of NAT : verum } holds union { ((S . i) `2) where i is Element of NAT : verum } is distance_function of FS,L proofend; theorem Th33: :: LATTICE8:33 for L being 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 { ((S . i) `1) where i is Element of NAT : verum } & FD = union { ((S . i) `2) where i is Element of NAT : verum } & FD . (x,y) <= a "\/" b holds ex z1, z2 being Element of FS st ( FD . (x,z1) = a & FD . (z1,z2) = ((FD . (x,y)) "\/" a) "/\" b & FD . (z2,y) = a ) proofend; Lm3: for m being Element of NAT holds ( not m in Seg 4 or m = 1 or m = 2 or m = 3 or m = 4 ) proofend; Lm4: for j being Element of NAT st 1 <= j & j < 4 & not j = 1 & not j = 2 holds j = 3 proofend; theorem Th34: :: LATTICE8:34 for L being 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 set st f = alpha FD & FS = union { ((S . i) `1) where i is Element of NAT : verum } & FD = union { ((S . i) `2) where i is Element of NAT : verum } & e1 in the carrier of (Image f) & e2 in the carrier of (Image f) & [x,y] in e1 "\/" e2 holds ex F being non empty FinSequence of FS st ( len F = 2 + 2 & x,y are_joint_by F,e1,e2 ) proofend; theorem Th35: :: LATTICE8:35 for L being lower-bounded modular LATTICE holds L has_a_representation_of_type<= 2 proofend; :: <=> :: L has_a_representation_of_type<= 2 iff L is modular :: [WP: ] Jonsson_Theorem_for_modular_lattices theorem :: LATTICE8:36 for L being lower-bounded LATTICE holds ( L has_a_representation_of_type<= 2 iff L is modular ) by Th9, Th35;