:: MATROID0 semantic presentation begin notation let x, y be set ; antonym x c/= y for x c= y; end; definition mode SubsetFamilyStr is TopStruct ; end; notation let M be SubsetFamilyStr; let A be Subset of M; synonym independent A for open ; antonym dependent A for open ; end; definition let M be SubsetFamilyStr; func the_family_of M -> Subset-Family of M equals :: MATROID0:def 1 the topology of M; coherence the topology of M is Subset-Family of M ; end; :: deftheorem defines the_family_of MATROID0:def_1_:_ for M being SubsetFamilyStr holds the_family_of M = the topology of M; definition let M be SubsetFamilyStr; let A be Subset of M; redefine attr A is open means :Def2: :: MATROID0:def 2 A in the_family_of M; compatibility ( A is independent iff A in the_family_of M ) by PRE_TOPC:def_2; end; :: deftheorem Def2 defines independent MATROID0:def_2_:_ for M being SubsetFamilyStr for A being Subset of M holds ( A is independent iff A in the_family_of M ); definition let M be SubsetFamilyStr; attrM is subset-closed means :Def3: :: MATROID0:def 3 the_family_of M is subset-closed ; attrM is with_exchange_property means :: MATROID0:def 4 for A, B being finite Subset of M st A in the_family_of M & B in the_family_of M & card B = (card A) + 1 holds ex e being Element of M st ( e in B \ A & A \/ {e} in the_family_of M ); end; :: deftheorem Def3 defines subset-closed MATROID0:def_3_:_ for M being SubsetFamilyStr holds ( M is subset-closed iff the_family_of M is subset-closed ); :: deftheorem defines with_exchange_property MATROID0:def_4_:_ for M being SubsetFamilyStr holds ( M is with_exchange_property iff for A, B being finite Subset of M st A in the_family_of M & B in the_family_of M & card B = (card A) + 1 holds ex e being Element of M st ( e in B \ A & A \/ {e} in the_family_of M ) ); registration cluster non empty finite strict non void subset-closed with_exchange_property for TopStruct ; existence ex b1 being SubsetFamilyStr st ( b1 is strict & not b1 is empty & not b1 is void & b1 is finite & b1 is subset-closed & b1 is with_exchange_property ) proof reconsider S = bool {0} as Subset-Family of {0} ; take M = TopStruct(# {0},S #); ::_thesis: ( M is strict & not M is empty & not M is void & M is finite & M is subset-closed & M is with_exchange_property ) thus M is strict ; ::_thesis: ( not M is empty & not M is void & M is finite & M is subset-closed & M is with_exchange_property ) thus not the carrier of M is empty ; :: according to STRUCT_0:def_1 ::_thesis: ( not M is void & M is finite & M is subset-closed & M is with_exchange_property ) thus not the topology of M is empty ; :: according to PENCIL_1:def_4 ::_thesis: ( M is finite & M is subset-closed & M is with_exchange_property ) thus the carrier of M is finite ; :: according to STRUCT_0:def_11 ::_thesis: ( M is subset-closed & M is with_exchange_property ) thus the_family_of M is subset-closed by COH_SP:2; :: according to MATROID0:def_3 ::_thesis: M is with_exchange_property let A, B be finite Subset of M; :: according to MATROID0:def_4 ::_thesis: ( A in the_family_of M & B in the_family_of M & card B = (card A) + 1 implies ex e being Element of M st ( e in B \ A & A \/ {e} in the_family_of M ) ) assume A in the_family_of M ; ::_thesis: ( not B in the_family_of M or not card B = (card A) + 1 or ex e being Element of M st ( e in B \ A & A \/ {e} in the_family_of M ) ) assume B in the_family_of M ; ::_thesis: ( not card B = (card A) + 1 or ex e being Element of M st ( e in B \ A & A \/ {e} in the_family_of M ) ) assume A1: card B = (card A) + 1 ; ::_thesis: ex e being Element of M st ( e in B \ A & A \/ {e} in the_family_of M ) reconsider e = 0 as Element of M by TARSKI:def_1; take e ; ::_thesis: ( e in B \ A & A \/ {e} in the_family_of M ) A2: bool {0} = {{},{0}} by ZFMISC_1:24; then A3: ( B = {} or B = {0} ) by TARSKI:def_2; then A4: ( card B = 0 or card B = 1 ) by CARD_1:30; A5: ( A = {} or A = {0} ) by A2, TARSKI:def_2; then ( card A = 0 or card A = 1 ) by CARD_1:30; hence ( e in B \ A & A \/ {e} in the_family_of M ) by A1, A5, A3, A4; ::_thesis: verum end; end; registration let M be non void SubsetFamilyStr; cluster independent for Element of K19( the carrier of M); existence ex b1 being Subset of M st b1 is independent proof set a = the Element of the topology of M; reconsider a = the Element of the topology of M as Subset of M ; take a ; ::_thesis: a is independent thus a in the_family_of M ; :: according to MATROID0:def_2 ::_thesis: verum end; end; registration let M be subset-closed SubsetFamilyStr; cluster the_family_of M -> subset-closed ; coherence the_family_of M is subset-closed by Def3; end; theorem Th1: :: MATROID0:1 for M being non void subset-closed SubsetFamilyStr for A being independent Subset of M for B being set st B c= A holds B is independent Subset of M proof let M be non void subset-closed SubsetFamilyStr; ::_thesis: for A being independent Subset of M for B being set st B c= A holds B is independent Subset of M let A be independent Subset of M; ::_thesis: for B being set st B c= A holds B is independent Subset of M let B be set ; ::_thesis: ( B c= A implies B is independent Subset of M ) assume A1: B c= A ; ::_thesis: B is independent Subset of M A in the_family_of M by Def2; then B in the_family_of M by A1, CLASSES1:def_1; hence B is independent Subset of M by Def2; ::_thesis: verum end; registration let M be non void subset-closed SubsetFamilyStr; cluster finite independent for Element of K19( the carrier of M); existence ex b1 being Subset of M st ( b1 is finite & b1 is independent ) proof set a = the Element of the topology of M; reconsider a = the Element of the topology of M as independent Subset of M by PRE_TOPC:def_2; {} c= a by XBOOLE_1:2; then reconsider b = {} as independent Subset of M by Th1; take b ; ::_thesis: ( b is finite & b is independent ) thus ( b is finite & b is independent ) ; ::_thesis: verum end; end; definition mode Matroid is non empty non void subset-closed with_exchange_property SubsetFamilyStr; end; theorem Th2: :: MATROID0:2 for M being subset-closed SubsetFamilyStr holds ( not M is void iff {} in the_family_of M ) proof let M be subset-closed SubsetFamilyStr; ::_thesis: ( not M is void iff {} in the_family_of M ) hereby ::_thesis: ( {} in the_family_of M implies not M is void ) assume not M is void ; ::_thesis: {} in the_family_of M then reconsider M9 = M as non void subset-closed SubsetFamilyStr ; set a = the independent Subset of M9; {} c= the independent Subset of M9 by XBOOLE_1:2; then {} is independent Subset of M9 by Th1; hence {} in the_family_of M by Def2; ::_thesis: verum end; assume {} in the_family_of M ; ::_thesis: not M is void hence not the topology of M is empty ; :: according to PENCIL_1:def_4 ::_thesis: verum end; registration let M be non void subset-closed SubsetFamilyStr; cluster empty -> independent for Element of K19( the carrier of M); coherence for b1 being Subset of M st b1 is empty holds b1 is independent proof let S be Subset of M; ::_thesis: ( S is empty implies S is independent ) assume S is empty ; ::_thesis: S is independent hence S in the_family_of M by Th2; :: according to MATROID0:def_2 ::_thesis: verum end; end; theorem Th3: :: MATROID0:3 for M being non void SubsetFamilyStr holds ( M is subset-closed iff for A, B being Subset of M st A is independent & B c= A holds B is independent ) proof let M be non void SubsetFamilyStr; ::_thesis: ( M is subset-closed iff for A, B being Subset of M st A is independent & B c= A holds B is independent ) thus ( M is subset-closed implies for A, B being Subset of M st A is independent & B c= A holds B is independent ) by Th1; ::_thesis: ( ( for A, B being Subset of M st A is independent & B c= A holds B is independent ) implies M is subset-closed ) assume A1: for A, B being Subset of M st A is independent & B c= A holds B is independent ; ::_thesis: M is subset-closed let x, y be set ; :: according to CLASSES1:def_1,MATROID0:def_3 ::_thesis: ( not x in the_family_of M or y c/= x or y in the_family_of M ) assume x in the_family_of M ; ::_thesis: ( y c/= x or y in the_family_of M ) then A2: x is independent Subset of M by Def2; assume y c= x ; ::_thesis: y in the_family_of M then y is independent Subset of M by A1, A2, XBOOLE_1:1; hence y in the_family_of M by Def2; ::_thesis: verum end; registration let M be non void subset-closed SubsetFamilyStr; let A be independent Subset of M; let B be set ; clusterA /\ B -> independent for Subset of M; coherence for b1 being Subset of M st b1 = A /\ B holds b1 is independent proof A /\ B c= A by XBOOLE_1:17; hence for b1 being Subset of M st b1 = A /\ B holds b1 is independent by Th3; ::_thesis: verum end; clusterB /\ A -> independent for Subset of M; coherence for b1 being Subset of M st b1 = B /\ A holds b1 is independent ; clusterA \ B -> independent for Subset of M; coherence for b1 being Subset of M st b1 = A \ B holds b1 is independent proof A \ B c= A by XBOOLE_1:36; hence for b1 being Subset of M st b1 = A \ B holds b1 is independent by Th3; ::_thesis: verum end; end; theorem Th4: :: MATROID0:4 for M being non empty non void SubsetFamilyStr holds ( M is with_exchange_property iff for A, B being finite Subset of M st A is independent & B is independent & card B = (card A) + 1 holds ex e being Element of M st ( e in B \ A & A \/ {e} is independent ) ) proof let M be non empty non void SubsetFamilyStr; ::_thesis: ( M is with_exchange_property iff for A, B being finite Subset of M st A is independent & B is independent & card B = (card A) + 1 holds ex e being Element of M st ( e in B \ A & A \/ {e} is independent ) ) thus ( M is with_exchange_property implies for A, B being finite Subset of M st A is independent & B is independent & card B = (card A) + 1 holds ex e being Element of M st ( e in B \ A & A \/ {e} is independent ) ) ::_thesis: ( ( for A, B being finite Subset of M st A is independent & B is independent & card B = (card A) + 1 holds ex e being Element of M st ( e in B \ A & A \/ {e} is independent ) ) implies M is with_exchange_property ) proof assume A1: for A, B being finite Subset of M st A in the_family_of M & B in the_family_of M & card B = (card A) + 1 holds ex e being Element of M st ( e in B \ A & A \/ {e} in the_family_of M ) ; :: according to MATROID0:def_4 ::_thesis: for A, B being finite Subset of M st A is independent & B is independent & card B = (card A) + 1 holds ex e being Element of M st ( e in B \ A & A \/ {e} is independent ) let A, B be finite Subset of M; ::_thesis: ( A is independent & B is independent & card B = (card A) + 1 implies ex e being Element of M st ( e in B \ A & A \/ {e} is independent ) ) assume that A2: A in the_family_of M and A3: B in the_family_of M and A4: card B = (card A) + 1 ; :: according to MATROID0:def_2 ::_thesis: ex e being Element of M st ( e in B \ A & A \/ {e} is independent ) consider e being Element of M such that A5: e in B \ A and A6: A \/ {e} in the_family_of M by A1, A2, A3, A4; take e ; ::_thesis: ( e in B \ A & A \/ {e} is independent ) thus ( e in B \ A & A \/ {e} in the_family_of M ) by A5, A6; :: according to MATROID0:def_2 ::_thesis: verum end; assume A7: for A, B being finite Subset of M st A is independent & B is independent & card B = (card A) + 1 holds ex e being Element of M st ( e in B \ A & A \/ {e} is independent ) ; ::_thesis: M is with_exchange_property let A, B be finite Subset of M; :: according to MATROID0:def_4 ::_thesis: ( A in the_family_of M & B in the_family_of M & card B = (card A) + 1 implies ex e being Element of M st ( e in B \ A & A \/ {e} in the_family_of M ) ) assume that A8: A in the_family_of M and A9: B in the_family_of M ; ::_thesis: ( not card B = (card A) + 1 or ex e being Element of M st ( e in B \ A & A \/ {e} in the_family_of M ) ) A10: B is independent by A9, Def2; assume A11: card B = (card A) + 1 ; ::_thesis: ex e being Element of M st ( e in B \ A & A \/ {e} in the_family_of M ) A is independent by A8, Def2; then consider e being Element of M such that A12: e in B \ A and A13: A \/ {e} is independent by A7, A10, A11; take e ; ::_thesis: ( e in B \ A & A \/ {e} in the_family_of M ) thus ( e in B \ A & A \/ {e} in the_family_of M ) by A12, A13, Def2; ::_thesis: verum end; definition canceled; let M be SubsetFamilyStr; attrM is finite-membered means :Def6: :: MATROID0:def 6 the_family_of M is finite-membered ; end; :: deftheorem MATROID0:def_5_:_ canceled; :: deftheorem Def6 defines finite-membered MATROID0:def_6_:_ for M being SubsetFamilyStr holds ( M is finite-membered iff the_family_of M is finite-membered ); definition let M be SubsetFamilyStr; attrM is finite-degree means :Def7: :: MATROID0:def 7 ( M is finite-membered & ex n being Nat st for A being finite Subset of M st A is independent holds card A <= n ); end; :: deftheorem Def7 defines finite-degree MATROID0:def_7_:_ for M being SubsetFamilyStr holds ( M is finite-degree iff ( M is finite-membered & ex n being Nat st for A being finite Subset of M st A is independent holds card A <= n ) ); registration cluster finite-degree -> finite-membered for TopStruct ; coherence for b1 being SubsetFamilyStr st b1 is finite-degree holds b1 is finite-membered proof let M be SubsetFamilyStr; ::_thesis: ( M is finite-degree implies M is finite-membered ) assume M is finite-membered ; :: according to MATROID0:def_7 ::_thesis: ( for n being Nat ex A being finite Subset of M st ( A is independent & not card A <= n ) or M is finite-membered ) hence ( for n being Nat ex A being finite Subset of M st ( A is independent & not card A <= n ) or M is finite-membered ) ; ::_thesis: verum end; cluster finite -> finite-degree for TopStruct ; coherence for b1 being SubsetFamilyStr st b1 is finite holds b1 is finite-degree proof let M be SubsetFamilyStr; ::_thesis: ( M is finite implies M is finite-degree ) assume the carrier of M is finite ; :: according to STRUCT_0:def_11 ::_thesis: M is finite-degree then reconsider X = the carrier of M as finite set ; thus M is finite-membered :: according to MATROID0:def_7 ::_thesis: ex n being Nat st for A being finite Subset of M st A is independent holds card A <= n proof let x be set ; :: according to FINSET_1:def_6,MATROID0:def_6 ::_thesis: ( not x in the_family_of M or x is finite ) assume x in the_family_of M ; ::_thesis: x is finite then x c= X ; hence x is finite ; ::_thesis: verum end; take card X ; ::_thesis: for A being finite Subset of M st A is independent holds card A <= card X let A be finite Subset of M; ::_thesis: ( A is independent implies card A <= card X ) thus ( A is independent implies card A <= card X ) by NAT_1:43; ::_thesis: verum end; end; begin registration cluster non empty mutually-disjoint with_non-empty_elements for set ; existence ex b1 being set st ( b1 is mutually-disjoint & not b1 is empty & b1 is with_non-empty_elements ) proof take {{0}} ; ::_thesis: ( {{0}} is mutually-disjoint & not {{0}} is empty & {{0}} is with_non-empty_elements ) thus ( {{0}} is mutually-disjoint & not {{0}} is empty & {{0}} is with_non-empty_elements ) by TAXONOM2:10; ::_thesis: verum end; end; theorem Th5: :: MATROID0:5 for A, B being finite set st card A < card B holds ex x being set st x in B \ A proof let A, B be finite set ; ::_thesis: ( card A < card B implies ex x being set st x in B \ A ) assume card A < card B ; ::_thesis: ex x being set st x in B \ A then not B c= A by NAT_1:43; then consider x being set such that A1: x in B and A2: x nin A by TARSKI:def_3; take x ; ::_thesis: x in B \ A thus x in B \ A by A1, A2, XBOOLE_0:def_5; ::_thesis: verum end; theorem :: MATROID0:6 for P being non empty mutually-disjoint with_non-empty_elements set for f being Choice_Function of P holds f is one-to-one proof let P be non empty mutually-disjoint with_non-empty_elements set ; ::_thesis: for f being Choice_Function of P holds f is one-to-one let f be Choice_Function of P; ::_thesis: f is one-to-one let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in K48(f) or not x2 in K48(f) or not f . x1 = f . x2 or x1 = x2 ) assume that A1: x1 in dom f and A2: x2 in dom f and A3: f . x1 = f . x2 ; ::_thesis: x1 = x2 A4: not {} in P ; then A5: f . x1 in x1 by A1, ORDERS_1:def_1; f . x1 in x2 by A2, A3, A4, ORDERS_1:def_1; then x1 meets x2 by A5, XBOOLE_0:3; hence x1 = x2 by A1, A2, TAXONOM2:def_5; ::_thesis: verum end; registration cluster discrete -> discrete non void subset-closed with_exchange_property for TopStruct ; coherence for b1 being discrete SubsetFamilyStr holds ( not b1 is void & b1 is subset-closed & b1 is with_exchange_property ) proof let T be discrete SubsetFamilyStr; ::_thesis: ( not T is void & T is subset-closed & T is with_exchange_property ) not the topology of T is empty by TDLAT_3:def_1; hence A1: not T is void by PENCIL_1:def_4; ::_thesis: ( T is subset-closed & T is with_exchange_property ) for A, B being Subset of T st A is independent & B c= A holds B is independent by TDLAT_3:15; hence T is subset-closed by A1, Th3; ::_thesis: T is with_exchange_property let A, B be finite Subset of T; :: according to MATROID0:def_4 ::_thesis: ( A in the_family_of T & B in the_family_of T & card B = (card A) + 1 implies ex e being Element of T st ( e in B \ A & A \/ {e} in the_family_of T ) ) assume that A in the_family_of T and B in the_family_of T and A2: card B = (card A) + 1 ; ::_thesis: ex e being Element of T st ( e in B \ A & A \/ {e} in the_family_of T ) now__::_thesis:_not_B_c=_A assume B c= A ; ::_thesis: contradiction then card B c= card A by CARD_1:11; then card B <= card A by NAT_1:39; then (card B) + 0 < (card A) + 1 by XREAL_1:8; hence contradiction by A2; ::_thesis: verum end; then consider x being set such that A3: x in B and A4: not x in A by TARSKI:def_3; reconsider x = x as Element of T by A3; {x} c= the carrier of T by A3, ZFMISC_1:31; then reconsider C = A \/ {x} as Subset of T by XBOOLE_1:8; take x ; ::_thesis: ( x in B \ A & A \/ {x} in the_family_of T ) thus x in B \ A by A3, A4, XBOOLE_0:def_5; ::_thesis: A \/ {x} in the_family_of T C is independent by TDLAT_3:15; hence A \/ {x} in the_family_of T by Def2; ::_thesis: verum end; end; theorem :: MATROID0:7 for T being non empty discrete TopStruct holds T is Matroid ; definition let P be set ; func ProdMatroid P -> strict SubsetFamilyStr means :Def8: :: MATROID0:def 8 ( the carrier of it = union P & the_family_of it = { A where A is Subset of (union P) : for D being set st D in P holds ex d being set st A /\ D c= {d} } ); existence ex b1 being strict SubsetFamilyStr st ( the carrier of b1 = union P & the_family_of b1 = { A where A is Subset of (union P) : for D being set st D in P holds ex d being set st A /\ D c= {d} } ) proof set F = { A where A is Subset of (union P) : for D being set st D in P holds ex d being set st A /\ D c= {d} } ; set X = union P; { A where A is Subset of (union P) : for D being set st D in P holds ex d being set st A /\ D c= {d} } c= bool (union P) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { A where A is Subset of (union P) : for D being set st D in P holds ex d being set st A /\ D c= {d} } or x in bool (union P) ) assume x in { A where A is Subset of (union P) : for D being set st D in P holds ex d being set st A /\ D c= {d} } ; ::_thesis: x in bool (union P) then ex A being Subset of (union P) st ( x = A & ( for D being set st D in P holds ex d being set st A /\ D c= {d} ) ) ; hence x in bool (union P) ; ::_thesis: verum end; then reconsider F = { A where A is Subset of (union P) : for D being set st D in P holds ex d being set st A /\ D c= {d} } as Subset-Family of (union P) ; take TopStruct(# (union P),F #) ; ::_thesis: ( the carrier of TopStruct(# (union P),F #) = union P & the_family_of TopStruct(# (union P),F #) = { A where A is Subset of (union P) : for D being set st D in P holds ex d being set st A /\ D c= {d} } ) thus ( the carrier of TopStruct(# (union P),F #) = union P & the_family_of TopStruct(# (union P),F #) = { A where A is Subset of (union P) : for D being set st D in P holds ex d being set st A /\ D c= {d} } ) ; ::_thesis: verum end; uniqueness for b1, b2 being strict SubsetFamilyStr st the carrier of b1 = union P & the_family_of b1 = { A where A is Subset of (union P) : for D being set st D in P holds ex d being set st A /\ D c= {d} } & the carrier of b2 = union P & the_family_of b2 = { A where A is Subset of (union P) : for D being set st D in P holds ex d being set st A /\ D c= {d} } holds b1 = b2 ; end; :: deftheorem Def8 defines ProdMatroid MATROID0:def_8_:_ for P being set for b2 being strict SubsetFamilyStr holds ( b2 = ProdMatroid P iff ( the carrier of b2 = union P & the_family_of b2 = { A where A is Subset of (union P) : for D being set st D in P holds ex d being set st A /\ D c= {d} } ) ); registration let P be non empty with_non-empty_elements set ; cluster ProdMatroid P -> non empty strict ; coherence not ProdMatroid P is empty proof set M = ProdMatroid P; the carrier of (ProdMatroid P) = union P by Def8; hence not the carrier of (ProdMatroid P) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum end; end; theorem Th8: :: MATROID0:8 for P being set for A being Subset of (ProdMatroid P) holds ( A is independent iff for D being Element of P ex d being Element of D st A /\ D c= {d} ) proof let P be set ; ::_thesis: for A being Subset of (ProdMatroid P) holds ( A is independent iff for D being Element of P ex d being Element of D st A /\ D c= {d} ) set M = ProdMatroid P; A1: the_family_of (ProdMatroid P) = { A where A is Subset of (union P) : for D being set st D in P holds ex d being set st A /\ D c= {d} } by Def8; let A be Subset of (ProdMatroid P); ::_thesis: ( A is independent iff for D being Element of P ex d being Element of D st A /\ D c= {d} ) A2: the carrier of (ProdMatroid P) = union P by Def8; thus ( A is independent implies for D being Element of P ex d being Element of D st A /\ D c= {d} ) ::_thesis: ( ( for D being Element of P ex d being Element of D st A /\ D c= {d} ) implies A is independent ) proof assume A in the_family_of (ProdMatroid P) ; :: according to MATROID0:def_2 ::_thesis: for D being Element of P ex d being Element of D st A /\ D c= {d} then A3: ex B being Subset of (union P) st ( A = B & ( for D being set st D in P holds ex d being set st B /\ D c= {d} ) ) by A1; let D be Element of P; ::_thesis: ex d being Element of D st A /\ D c= {d} ( P = {} implies ( A = {} & {} /\ D = {} ) ) by A2, ZFMISC_1:2; then ( P = {} implies A /\ D c= {1} ) by XBOOLE_1:2; then consider d being set such that A4: A /\ D c= {d} by A3; set d0 = the Element of D; now__::_thesis:_(_d_nin_D_implies_A_/\_D_c=_{_the_Element_of_D}_) assume d nin D ; ::_thesis: A /\ D c= { the Element of D} then d nin A /\ D by XBOOLE_0:def_4; then A /\ D <> {d} by TARSKI:def_1; then A /\ D = {} by A4, ZFMISC_1:33; hence A /\ D c= { the Element of D} by XBOOLE_1:2; ::_thesis: verum end; hence ex d being Element of D st A /\ D c= {d} by A4; ::_thesis: verum end; assume A5: for D being Element of P ex d being Element of D st A /\ D c= {d} ; ::_thesis: A is independent A6: now__::_thesis:_for_D_being_set_st_D_in_P_holds_ ex_d_being_set_st_A_/\_D_c=_{d} let D be set ; ::_thesis: ( D in P implies ex d being set st A /\ D c= {d} ) assume D in P ; ::_thesis: ex d being set st A /\ D c= {d} then ex d being Element of D st A /\ D c= {d} by A5; hence ex d being set st A /\ D c= {d} ; ::_thesis: verum end; the carrier of (ProdMatroid P) = union P by Def8; hence A in the_family_of (ProdMatroid P) by A1, A6; :: according to MATROID0:def_2 ::_thesis: verum end; registration let P be set ; cluster ProdMatroid P -> strict non void subset-closed ; coherence ( not ProdMatroid P is void & ProdMatroid P is subset-closed ) proof set M = ProdMatroid P; A1: the_family_of (ProdMatroid P) = { A where A is Subset of (union P) : for D being set st D in P holds ex d being set st A /\ D c= {d} } by Def8; set A = {} (union P); now__::_thesis:_for_D_being_set_st_D_in_P_holds_ ex_d_being_set_st_({}_(union_P))_/\_D_c=_{d} let D be set ; ::_thesis: ( D in P implies ex d being set st ({} (union P)) /\ D c= {d} ) assume D in P ; ::_thesis: ex d being set st ({} (union P)) /\ D c= {d} take d = {} ; ::_thesis: ({} (union P)) /\ D c= {d} thus ({} (union P)) /\ D c= {d} by XBOOLE_1:2; ::_thesis: verum end; then {} (union P) in the_family_of (ProdMatroid P) by A1; hence not the topology of (ProdMatroid P) is empty ; :: according to PENCIL_1:def_4 ::_thesis: ProdMatroid P is subset-closed thus the_family_of (ProdMatroid P) is subset-closed :: according to MATROID0:def_3 ::_thesis: verum proof let a, b be set ; :: according to CLASSES1:def_1 ::_thesis: ( not a in the_family_of (ProdMatroid P) or b c/= a or b in the_family_of (ProdMatroid P) ) assume that A2: a in the_family_of (ProdMatroid P) and A3: b c= a ; ::_thesis: b in the_family_of (ProdMatroid P) A4: ex B being Subset of (union P) st ( a = B & ( for D being set st D in P holds ex d being set st B /\ D c= {d} ) ) by A1, A2; A5: now__::_thesis:_for_D_being_set_st_D_in_P_holds_ ex_d_being_set_st_b_/\_D_c=_{d} let D be set ; ::_thesis: ( D in P implies ex d being set st b /\ D c= {d} ) assume D in P ; ::_thesis: ex d being set st b /\ D c= {d} then consider d being set such that A6: a /\ D c= {d} by A4; take d = d; ::_thesis: b /\ D c= {d} b /\ D c= a /\ D by A3, XBOOLE_1:26; hence b /\ D c= {d} by A6, XBOOLE_1:1; ::_thesis: verum end; b is Subset of (union P) by A3, A4, XBOOLE_1:1; hence b in the_family_of (ProdMatroid P) by A1, A5; ::_thesis: verum end; end; end; theorem Th9: :: MATROID0:9 for P being mutually-disjoint set for x being Subset of (ProdMatroid P) ex f being Function of x,P st for a being set st a in x holds a in f . a proof defpred S1[ set , set ] means $1 in $2; let P be mutually-disjoint set ; ::_thesis: for x being Subset of (ProdMatroid P) ex f being Function of x,P st for a being set st a in x holds a in f . a let x be Subset of (ProdMatroid P); ::_thesis: ex f being Function of x,P st for a being set st a in x holds a in f . a A1: now__::_thesis:_for_a_being_set_st_a_in_x_holds_ ex_y_being_set_st_ (_y_in_P_&_S1[a,y]_) let a be set ; ::_thesis: ( a in x implies ex y being set st ( y in P & S1[a,y] ) ) assume a in x ; ::_thesis: ex y being set st ( y in P & S1[a,y] ) then a in the carrier of (ProdMatroid P) ; then a in union P by Def8; then ex y being set st ( a in y & y in P ) by TARSKI:def_4; hence ex y being set st ( y in P & S1[a,y] ) ; ::_thesis: verum end; consider f being Function of x,P such that A2: for a being set st a in x holds S1[a,f . a] from FUNCT_2:sch_1(A1); take f ; ::_thesis: for a being set st a in x holds a in f . a thus for a being set st a in x holds a in f . a by A2; ::_thesis: verum end; theorem Th10: :: MATROID0:10 for P being mutually-disjoint set for x being Subset of (ProdMatroid P) for f being Function of x,P st ( for a being set st a in x holds a in f . a ) holds ( x is independent iff f is one-to-one ) proof let P be mutually-disjoint set ; ::_thesis: for x being Subset of (ProdMatroid P) for f being Function of x,P st ( for a being set st a in x holds a in f . a ) holds ( x is independent iff f is one-to-one ) let x be Subset of (ProdMatroid P); ::_thesis: for f being Function of x,P st ( for a being set st a in x holds a in f . a ) holds ( x is independent iff f is one-to-one ) let f be Function of x,P; ::_thesis: ( ( for a being set st a in x holds a in f . a ) implies ( x is independent iff f is one-to-one ) ) assume A1: for a being set st a in x holds a in f . a ; ::_thesis: ( x is independent iff f is one-to-one ) hereby ::_thesis: ( f is one-to-one implies x is independent ) assume A2: x is independent ; ::_thesis: f is one-to-one thus f is one-to-one ::_thesis: verum proof let a, b be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not a in K48(f) or not b in K48(f) or not f . a = f . b or a = b ) assume that A3: a in dom f and A4: b in dom f ; ::_thesis: ( not f . a = f . b or a = b ) A5: f . b in rng f by A4, FUNCT_1:def_3; f . a in rng f by A3, FUNCT_1:def_3; then reconsider D1 = f . a, D2 = f . b as Element of P by A5; a in D1 by A1, A3; then A6: a in x /\ D1 by A3, XBOOLE_0:def_4; consider d2 being Element of D2 such that A7: x /\ D2 c= {d2} by A2, Th8; b in D2 by A1, A4; then b in x /\ D2 by A4, XBOOLE_0:def_4; then b = d2 by A7, TARSKI:def_1; hence ( not f . a = f . b or a = b ) by A7, A6, TARSKI:def_1; ::_thesis: verum end; end; assume A8: f is one-to-one ; ::_thesis: x is independent now__::_thesis:_for_D_being_Element_of_P_holds_ not__for_d_being_Element_of_D_holds_x_/\_D_c/=_{d} let D be Element of P; ::_thesis: not for d being Element of D holds x /\ D c/= {d} set d1 = the Element of D; assume A9: for d being Element of D holds x /\ D c/= {d} ; ::_thesis: contradiction then x /\ D c/= { the Element of D} ; then consider d2 being set such that A10: d2 in x /\ D and d2 nin { the Element of D} by TARSKI:def_3; A11: d2 in D by A10, XBOOLE_0:def_4; A12: d2 in x by A10, XBOOLE_0:def_4; then d2 in f . d2 by A1; then A13: f . d2 meets D by A11, XBOOLE_0:3; the carrier of (ProdMatroid P) = union P by Def8; then ex y being set st ( d2 in y & y in P ) by A10, TARSKI:def_4; then A14: dom f = x by FUNCT_2:def_1; then f . d2 in rng f by A12, FUNCT_1:def_3; then A15: f . d2 = D by A13, TAXONOM2:def_5; x /\ D c= {d2} proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in x /\ D or a in {d2} ) assume A16: a in x /\ D ; ::_thesis: a in {d2} then A17: a in x by XBOOLE_0:def_4; A18: a in D by A16, XBOOLE_0:def_4; a in f . a by A1, A17; then A19: f . a meets D by A18, XBOOLE_0:3; f . a in rng f by A14, A17, FUNCT_1:def_3; then f . a = D by A19, TAXONOM2:def_5; then a = d2 by A8, A12, A14, A15, A17, FUNCT_1:def_4; hence a in {d2} by TARSKI:def_1; ::_thesis: verum end; hence contradiction by A9, A11; ::_thesis: verum end; hence x is independent by Th8; ::_thesis: verum end; registration let P be mutually-disjoint set ; cluster ProdMatroid P -> strict with_exchange_property ; coherence ProdMatroid P is with_exchange_property proof set M = ProdMatroid P; A1: the_family_of (ProdMatroid P) = { A where A is Subset of (union P) : for D being set st D in P holds ex d being set st A /\ D c= {d} } by Def8; let A, B be finite Subset of (ProdMatroid P); :: according to MATROID0:def_4 ::_thesis: ( A in the_family_of (ProdMatroid P) & B in the_family_of (ProdMatroid P) & card B = (card A) + 1 implies ex e being Element of (ProdMatroid P) st ( e in B \ A & A \/ {e} in the_family_of (ProdMatroid P) ) ) assume that A2: A in the_family_of (ProdMatroid P) and A3: B in the_family_of (ProdMatroid P) ; ::_thesis: ( not card B = (card A) + 1 or ex e being Element of (ProdMatroid P) st ( e in B \ A & A \/ {e} in the_family_of (ProdMatroid P) ) ) consider f being Function of A,P such that A4: for a being set st a in A holds a in f . a by Th9; assume card B = (card A) + 1 ; ::_thesis: ex e being Element of (ProdMatroid P) st ( e in B \ A & A \/ {e} in the_family_of (ProdMatroid P) ) then A5: card B > card A by NAT_1:13; consider g being Function of B,P such that A6: for a being set st a in B holds a in g . a by Th9; A7: the carrier of (ProdMatroid P) = union P by Def8; then ( P = {} implies A = {} ) by ZFMISC_1:2; then A8: dom f = A by FUNCT_2:def_1; reconsider A9 = rng f, B9 = rng g as finite set ; A9: A is independent by A2, Def2; then f is one-to-one by A4, Th10; then A,A9 are_equipotent by A8, WELLORD2:def_4; then A10: card A = card A9 by CARD_1:5; ( P = {} implies B = {} ) by A7, ZFMISC_1:2; then A11: dom g = B by FUNCT_2:def_1; B is independent by A3, Def2; then g is one-to-one by A6, Th10; then B,B9 are_equipotent by A11, WELLORD2:def_4; then card B = card B9 by CARD_1:5; then consider a being set such that A12: a in B9 \ A9 by A10, A5, Th5; consider x9 being set such that A13: x9 in B and A14: a = g . x9 by A11, A12, FUNCT_1:def_3; reconsider x = x9 as Element of (ProdMatroid P) by A13; take x ; ::_thesis: ( x in B \ A & A \/ {x} in the_family_of (ProdMatroid P) ) A15: a nin A9 by A12, XBOOLE_0:def_5; now__::_thesis:_not_x_in_A A16: x in g . x by A6, A13; assume A17: x in A ; ::_thesis: contradiction then x in f . x by A4; then A18: f . x meets g . x by A16, XBOOLE_0:3; A19: g . x in rng g by A11, A13, FUNCT_1:def_3; f . x in rng f by A8, A17, FUNCT_1:def_3; hence contradiction by A15, A14, A19, A18, TAXONOM2:def_5; ::_thesis: verum end; hence x in B \ A by A13, XBOOLE_0:def_5; ::_thesis: A \/ {x} in the_family_of (ProdMatroid P) reconsider xx = {x} as Subset of (ProdMatroid P) by A13, ZFMISC_1:31; reconsider Ax = A \/ xx as Subset of (union P) by Def8; A20: a in B9 by A12; now__::_thesis:_for_D_being_set_st_D_in_P_holds_ ex_x9_being_set_st_Ax_/\_D_c=_{x9} let D be set ; ::_thesis: ( D in P implies ex x9 being set st Ax /\ x9 c= {b2} ) A21: Ax /\ D = (A /\ D) \/ (xx /\ D) by XBOOLE_1:23; assume A22: D in P ; ::_thesis: ex x9 being set st Ax /\ x9 c= {b2} then consider d being Element of D such that A23: A /\ D c= {d} by A9, Th8; percases ( D = a or D <> a ) ; supposeA24: D = a ; ::_thesis: ex x9 being set st Ax /\ x9 c= {b2} take x9 = x9; ::_thesis: Ax /\ D c= {x9} A /\ D c= {} proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in A /\ D or z in {} ) assume A25: z in A /\ D ; ::_thesis: z in {} then A26: z in D by XBOOLE_0:def_4; A27: z in A by A25, XBOOLE_0:def_4; then z in f . z by A4; then A28: D meets f . z by A26, XBOOLE_0:3; f . z in rng f by A8, A27, FUNCT_1:def_3; hence z in {} by A20, A15, A24, A28, TAXONOM2:def_5; ::_thesis: verum end; then A /\ D = {} ; hence Ax /\ D c= {x9} by A21, XBOOLE_1:17; ::_thesis: verum end; supposeA29: D <> a ; ::_thesis: ex d being set st Ax /\ d c= {b2} a in rng g by A11, A13, A14, FUNCT_1:def_3; then A30: a misses D by A22, A29, TAXONOM2:def_5; x in a by A6, A13, A14; then x nin D by A30, XBOOLE_0:3; then xx c/= D by ZFMISC_1:31; then A31: xx /\ D <> xx by XBOOLE_1:17; reconsider d = d as set ; take d = d; ::_thesis: Ax /\ D c= {d} xx /\ D c= xx by XBOOLE_1:17; then xx /\ D = {} by A31, ZFMISC_1:33; hence Ax /\ D c= {d} by A23, A21; ::_thesis: verum end; end; end; hence A \/ {x} in the_family_of (ProdMatroid P) by A1; ::_thesis: verum end; end; registration let X be finite set ; let P be Subset of (bool X); cluster ProdMatroid P -> finite strict ; coherence ProdMatroid P is finite proof union P is finite ; hence the carrier of (ProdMatroid P) is finite by Def8; :: according to STRUCT_0:def_11 ::_thesis: verum end; end; registration let X be set ; cluster -> mutually-disjoint for a_partition of X; coherence for b1 being a_partition of X holds b1 is mutually-disjoint proof let P be a_partition of X; ::_thesis: P is mutually-disjoint let x, y be set ; :: according to TAXONOM2:def_5 ::_thesis: ( not x in P or not y in P or x = y or x misses y ) thus ( not x in P or not y in P or x = y or x misses y ) by EQREL_1:def_4; ::_thesis: verum end; end; registration cluster non empty finite strict non void subset-closed with_exchange_property for TopStruct ; existence ex b1 being Matroid st ( b1 is finite & b1 is strict ) proof set X = the non empty finite set ; set P = the a_partition of the non empty finite set ; take ProdMatroid the a_partition of the non empty finite set ; ::_thesis: ( ProdMatroid the a_partition of the non empty finite set is finite & ProdMatroid the a_partition of the non empty finite set is strict ) thus ( ProdMatroid the a_partition of the non empty finite set is finite & ProdMatroid the a_partition of the non empty finite set is strict ) ; ::_thesis: verum end; end; registration let M be non void finite-membered SubsetFamilyStr; cluster independent -> finite independent for Element of K19( the carrier of M); coherence for b1 being independent Subset of M holds b1 is finite proof let A be independent Subset of M; ::_thesis: A is finite A1: the_family_of M is finite-membered by Def6; A in the_family_of M by Def2; hence A is finite by A1; ::_thesis: verum end; end; definition let F be Field; let V be VectSp of F; func LinearlyIndependentSubsets V -> strict SubsetFamilyStr means :Def9: :: MATROID0:def 9 ( the carrier of it = the carrier of V & the_family_of it = { A where A is Subset of V : A is linearly-independent } ); existence ex b1 being strict SubsetFamilyStr st ( the carrier of b1 = the carrier of V & the_family_of b1 = { A where A is Subset of V : A is linearly-independent } ) proof set F = { A where A is Subset of V : A is linearly-independent } ; set X = the carrier of V; { A where A is Subset of V : A is linearly-independent } c= bool the carrier of V proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { A where A is Subset of V : A is linearly-independent } or x in bool the carrier of V ) assume x in { A where A is Subset of V : A is linearly-independent } ; ::_thesis: x in bool the carrier of V then ex A being Subset of the carrier of V st ( x = A & A is linearly-independent ) ; hence x in bool the carrier of V ; ::_thesis: verum end; then reconsider F = { A where A is Subset of V : A is linearly-independent } as Subset-Family of the carrier of V ; take TopStruct(# the carrier of V,F #) ; ::_thesis: ( the carrier of TopStruct(# the carrier of V,F #) = the carrier of V & the_family_of TopStruct(# the carrier of V,F #) = { A where A is Subset of V : A is linearly-independent } ) thus ( the carrier of TopStruct(# the carrier of V,F #) = the carrier of V & the_family_of TopStruct(# the carrier of V,F #) = { A where A is Subset of V : A is linearly-independent } ) ; ::_thesis: verum end; uniqueness for b1, b2 being strict SubsetFamilyStr st the carrier of b1 = the carrier of V & the_family_of b1 = { A where A is Subset of V : A is linearly-independent } & the carrier of b2 = the carrier of V & the_family_of b2 = { A where A is Subset of V : A is linearly-independent } holds b1 = b2 ; end; :: deftheorem Def9 defines LinearlyIndependentSubsets MATROID0:def_9_:_ for F being Field for V being VectSp of F for b3 being strict SubsetFamilyStr holds ( b3 = LinearlyIndependentSubsets V iff ( the carrier of b3 = the carrier of V & the_family_of b3 = { A where A is Subset of V : A is linearly-independent } ) ); registration let F be Field; let V be VectSp of F; cluster LinearlyIndependentSubsets V -> non empty strict non void subset-closed ; coherence ( not LinearlyIndependentSubsets V is empty & not LinearlyIndependentSubsets V is void & LinearlyIndependentSubsets V is subset-closed ) proof set M = LinearlyIndependentSubsets V; A1: the_family_of (LinearlyIndependentSubsets V) = { A where A is Subset of V : A is linearly-independent } by Def9; the carrier of (LinearlyIndependentSubsets V) = the carrier of V by Def9; hence not the carrier of (LinearlyIndependentSubsets V) is empty ; :: according to STRUCT_0:def_1 ::_thesis: ( not LinearlyIndependentSubsets V is void & LinearlyIndependentSubsets V is subset-closed ) {} V is linearly-independent ; then {} in the_family_of (LinearlyIndependentSubsets V) by A1; hence not the topology of (LinearlyIndependentSubsets V) is empty ; :: according to PENCIL_1:def_4 ::_thesis: LinearlyIndependentSubsets V is subset-closed let x, y be set ; :: according to CLASSES1:def_1,MATROID0:def_3 ::_thesis: ( not x in the_family_of (LinearlyIndependentSubsets V) or y c/= x or y in the_family_of (LinearlyIndependentSubsets V) ) assume x in the_family_of (LinearlyIndependentSubsets V) ; ::_thesis: ( y c/= x or y in the_family_of (LinearlyIndependentSubsets V) ) then A2: ex A being Subset of V st ( x = A & A is linearly-independent ) by A1; assume A3: y c= x ; ::_thesis: y in the_family_of (LinearlyIndependentSubsets V) then reconsider B = y as Subset of V by A2, XBOOLE_1:1; B is linearly-independent by A2, A3, VECTSP_7:1; hence y in the_family_of (LinearlyIndependentSubsets V) by A1; ::_thesis: verum end; end; theorem Th11: :: MATROID0:11 for F being Field for V being VectSp of F for A being Subset of (LinearlyIndependentSubsets V) holds ( A is independent iff A is linearly-independent Subset of V ) proof let F be Field; ::_thesis: for V being VectSp of F for A being Subset of (LinearlyIndependentSubsets V) holds ( A is independent iff A is linearly-independent Subset of V ) let V be VectSp of F; ::_thesis: for A being Subset of (LinearlyIndependentSubsets V) holds ( A is independent iff A is linearly-independent Subset of V ) set M = LinearlyIndependentSubsets V; let B be Subset of (LinearlyIndependentSubsets V); ::_thesis: ( B is independent iff B is linearly-independent Subset of V ) the_family_of (LinearlyIndependentSubsets V) = { A where A is Subset of V : A is linearly-independent } by Def9; then ( B in the_family_of (LinearlyIndependentSubsets V) iff ex A being Subset of V st ( B = A & A is linearly-independent ) ) ; hence ( B is independent iff B is linearly-independent Subset of V ) by Def2; ::_thesis: verum end; theorem :: MATROID0:12 for F being Field for V being VectSp of F for A, B being finite Subset of V st B c= A holds for v being Vector of V st v in Lin A & not v in Lin B holds ex w being Vector of V st ( w in A \ B & w in Lin ((A \ {w}) \/ {v}) ) proof let F be Field; ::_thesis: for V being VectSp of F for A, B being finite Subset of V st B c= A holds for v being Vector of V st v in Lin A & not v in Lin B holds ex w being Vector of V st ( w in A \ B & w in Lin ((A \ {w}) \/ {v}) ) let V be VectSp of F; ::_thesis: for A, B being finite Subset of V st B c= A holds for v being Vector of V st v in Lin A & not v in Lin B holds ex w being Vector of V st ( w in A \ B & w in Lin ((A \ {w}) \/ {v}) ) let A, B be finite Subset of V; ::_thesis: ( B c= A implies for v being Vector of V st v in Lin A & not v in Lin B holds ex w being Vector of V st ( w in A \ B & w in Lin ((A \ {w}) \/ {v}) ) ) assume B c= A ; ::_thesis: for v being Vector of V st v in Lin A & not v in Lin B holds ex w being Vector of V st ( w in A \ B & w in Lin ((A \ {w}) \/ {v}) ) then A = B \/ (A \ B) by XBOOLE_1:45; hence for v being Vector of V st v in Lin A & not v in Lin B holds ex w being Vector of V st ( w in A \ B & w in Lin ((A \ {w}) \/ {v}) ) by VECTSP_9:18; ::_thesis: verum end; theorem Th13: :: MATROID0:13 for F being Field for V being VectSp of F for A being Subset of V st A is linearly-independent holds for a being Element of V st a nin the carrier of (Lin A) holds A \/ {a} is linearly-independent proof let F be Field; ::_thesis: for V being VectSp of F for A being Subset of V st A is linearly-independent holds for a being Element of V st a nin the carrier of (Lin A) holds A \/ {a} is linearly-independent let V be VectSp of F; ::_thesis: for A being Subset of V st A is linearly-independent holds for a being Element of V st a nin the carrier of (Lin A) holds A \/ {a} is linearly-independent let A be Subset of V; ::_thesis: ( A is linearly-independent implies for a being Element of V st a nin the carrier of (Lin A) holds A \/ {a} is linearly-independent ) assume A1: A is linearly-independent ; ::_thesis: for a being Element of V st a nin the carrier of (Lin A) holds A \/ {a} is linearly-independent A2: { (Sum s) where s is Linear_Combination of A : verum } = the carrier of (Lin A) by VECTSP_7:def_2; let a be Element of V; ::_thesis: ( a nin the carrier of (Lin A) implies A \/ {a} is linearly-independent ) set B = A \/ {a}; assume that A3: a nin the carrier of (Lin A) and A4: A \/ {a} is linearly-dependent ; ::_thesis: contradiction consider l being Linear_Combination of A \/ {a} such that A5: Sum l = 0. V and A6: Carrier l <> {} by A4, VECTSP_7:def_1; a in {a} by TARSKI:def_1; then A7: (l ! {a}) . a = l . a by RANKNULL:25; A c= the carrier of (Lin A) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in the carrier of (Lin A) ) assume A8: x in A ; ::_thesis: x in the carrier of (Lin A) then reconsider x = x as Element of V ; x in Lin A by A8, VECTSP_7:8; hence x in the carrier of (Lin A) by STRUCT_0:def_5; ::_thesis: verum end; then a nin A by A3; then (A \/ {a}) \ A = {a} by XBOOLE_1:88, ZFMISC_1:50; then l = (l ! A) + (l ! {a}) by RANKNULL:27, XBOOLE_1:7; then 0. V = (Sum (l ! A)) + (Sum (l ! {a})) by A5, VECTSP_6:44 .= (Sum (l ! A)) + ((l . a) * a) by A7, VECTSP_6:17 ; then A9: (l . a) * a = - (Sum (l ! A)) by ALGSTR_0:def_13; A10: (- ((l . a) ")) * (l ! A) is Linear_Combination of A by VECTSP_6:31; now__::_thesis:_not_l_._a_<>_0._F assume l . a <> 0. F ; ::_thesis: contradiction then a = ((l . a) ") * (- (Sum (l ! A))) by A9, VECTSP_1:20 .= - (((l . a) ") * (Sum (l ! A))) by VECTSP_1:22 .= (- ((l . a) ")) * (Sum (l ! A)) by VECTSP_1:21 .= Sum ((- ((l . a) ")) * (l ! A)) by VECTSP_6:45 ; hence contradiction by A3, A2, A10; ::_thesis: verum end; then A11: a nin Carrier l by VECTSP_6:2; A12: Carrier l c= A \/ {a} by VECTSP_6:def_4; Carrier l c= A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier l or x in A ) thus ( not x in Carrier l or x in A ) by A11, A12, ZFMISC_1:136; ::_thesis: verum end; then l is Linear_Combination of A by VECTSP_6:def_4; hence contradiction by A1, A5, A6, VECTSP_7:def_1; ::_thesis: verum end; registration let F be Field; let V be VectSp of F; cluster LinearlyIndependentSubsets V -> strict with_exchange_property ; coherence LinearlyIndependentSubsets V is with_exchange_property proof set M = LinearlyIndependentSubsets V; A1: the_family_of (LinearlyIndependentSubsets V) = { A where A is Subset of V : A is linearly-independent } by Def9; let A, B be finite Subset of (LinearlyIndependentSubsets V); :: according to MATROID0:def_4 ::_thesis: ( A in the_family_of (LinearlyIndependentSubsets V) & B in the_family_of (LinearlyIndependentSubsets V) & card B = (card A) + 1 implies ex e being Element of (LinearlyIndependentSubsets V) st ( e in B \ A & A \/ {e} in the_family_of (LinearlyIndependentSubsets V) ) ) assume that A2: A in the_family_of (LinearlyIndependentSubsets V) and A3: B in the_family_of (LinearlyIndependentSubsets V) and A4: card B = (card A) + 1 ; ::_thesis: ex e being Element of (LinearlyIndependentSubsets V) st ( e in B \ A & A \/ {e} in the_family_of (LinearlyIndependentSubsets V) ) A5: B is independent by A3, Def2; A is independent by A2, Def2; then reconsider A9 = A, B9 = B as finite linearly-independent Subset of V by A5, Th11; set V9 = Lin (A9 \/ B9); A9 c= the carrier of (Lin (A9 \/ B9)) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A9 or a in the carrier of (Lin (A9 \/ B9)) ) assume a in A9 ; ::_thesis: a in the carrier of (Lin (A9 \/ B9)) then a in A9 \/ B9 by XBOOLE_0:def_3; then a in Lin (A9 \/ B9) by VECTSP_7:8; hence a in the carrier of (Lin (A9 \/ B9)) by STRUCT_0:def_5; ::_thesis: verum end; then reconsider A99 = A9 as finite linearly-independent Subset of (Lin (A9 \/ B9)) by VECTSP_9:12; B9 c= the carrier of (Lin (A9 \/ B9)) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in B9 or a in the carrier of (Lin (A9 \/ B9)) ) assume a in B9 ; ::_thesis: a in the carrier of (Lin (A9 \/ B9)) then a in A9 \/ B9 by XBOOLE_0:def_3; then a in Lin (A9 \/ B9) by VECTSP_7:8; hence a in the carrier of (Lin (A9 \/ B9)) by STRUCT_0:def_5; ::_thesis: verum end; then reconsider B99 = B9 as finite linearly-independent Subset of (Lin (A9 \/ B9)) by VECTSP_9:12; A6: Lin (A9 \/ B9) = Lin (A99 \/ B99) by VECTSP_9:17; then consider D being Basis of Lin (A9 \/ B9) such that A7: B9 c= D by VECTSP_7:19; consider C being Basis of Lin (A9 \/ B9) such that A8: C c= A99 \/ B99 by A6, VECTSP_7:20; reconsider c = C as finite set by A8; c is Basis of Lin (A9 \/ B9) ; then Lin (A9 \/ B9) is finite-dimensional by MATRLIN:def_1; then card c = card D by VECTSP_9:22; then card B c= card c by A7, CARD_1:11; then card B <= card c by NAT_1:39; then A9: card A < card c by A4, NAT_1:13; set e = the Element of C \ the carrier of (Lin A9); A10: A9 is Basis of Lin A9 by RANKNULL:20; then A11: Lin A9 is finite-dimensional by MATRLIN:def_1; now__::_thesis:_not_C_c=_the_carrier_of_(Lin_A9) assume C c= the carrier of (Lin A9) ; ::_thesis: contradiction then reconsider C9 = C as Subset of (Lin A9) ; the carrier of (Lin A9) c= the carrier of V by VECTSP_4:def_2; then reconsider C99 = C9 as Subset of V by XBOOLE_1:1; C is linearly-independent by VECTSP_7:def_3; then C99 is linearly-independent by VECTSP_9:11; then consider E being Basis of Lin A9 such that A12: C9 c= E by VECTSP_7:19, VECTSP_9:12; A13: card A = card E by A10, A11, VECTSP_9:22; then E is finite ; hence contradiction by A9, A12, A13, NAT_1:43; ::_thesis: verum end; then consider x being set such that A14: x in C and A15: x nin the carrier of (Lin A9) by TARSKI:def_3; A16: x in C \ the carrier of (Lin A9) by A14, A15, XBOOLE_0:def_5; then A17: the Element of C \ the carrier of (Lin A9) nin the carrier of (Lin A9) by XBOOLE_0:def_5; A18: the Element of C \ the carrier of (Lin A9) in C by A16, XBOOLE_0:def_5; then the Element of C \ the carrier of (Lin A9) in A \/ B by A8; then reconsider e = the Element of C \ the carrier of (Lin A9) as Element of (LinearlyIndependentSubsets V) ; take e ; ::_thesis: ( e in B \ A & A \/ {e} in the_family_of (LinearlyIndependentSubsets V) ) A c= the carrier of (Lin A9) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in the carrier of (Lin A9) ) assume x in A ; ::_thesis: x in the carrier of (Lin A9) then x in Lin A9 by VECTSP_7:8; hence x in the carrier of (Lin A9) by STRUCT_0:def_5; ::_thesis: verum end; then A19: e nin A by A16, XBOOLE_0:def_5; then A20: e in B9 by A8, A18, XBOOLE_0:def_3; hence e in B \ A by A19, XBOOLE_0:def_5; ::_thesis: A \/ {e} in the_family_of (LinearlyIndependentSubsets V) reconsider a = e as Element of V by A20; A9 \/ {a} is linearly-independent by A17, Th13; hence A \/ {e} in the_family_of (LinearlyIndependentSubsets V) by A1; ::_thesis: verum end; end; registration let F be Field; let V be finite-dimensional VectSp of F; cluster LinearlyIndependentSubsets V -> strict finite-membered ; coherence LinearlyIndependentSubsets V is finite-membered proof let A be set ; :: according to FINSET_1:def_6,MATROID0:def_6 ::_thesis: ( not A in the_family_of (LinearlyIndependentSubsets V) or A is finite ) set M = LinearlyIndependentSubsets V; assume A in the_family_of (LinearlyIndependentSubsets V) ; ::_thesis: A is finite then A is independent Subset of (LinearlyIndependentSubsets V) by Def2; then A is linearly-independent Subset of V by Th11; hence A is finite by VECTSP_9:21; ::_thesis: verum end; end; begin definition let M be SubsetFamilyStr; let A, C be Subset of M; predA is_maximal_independent_in C means :Def10: :: MATROID0:def 10 ( A is independent & A c= C & ( for B being Subset of M st B is independent & B c= C & A c= B holds A = B ) ); end; :: deftheorem Def10 defines is_maximal_independent_in MATROID0:def_10_:_ for M being SubsetFamilyStr for A, C being Subset of M holds ( A is_maximal_independent_in C iff ( A is independent & A c= C & ( for B being Subset of M st B is independent & B c= C & A c= B holds A = B ) ) ); theorem Th14: :: MATROID0:14 for M being non void finite-degree SubsetFamilyStr for C, A being Subset of M st A c= C & A is independent holds ex B being independent Subset of M st ( A c= B & B is_maximal_independent_in C ) proof let M be non void finite-degree SubsetFamilyStr; ::_thesis: for C, A being Subset of M st A c= C & A is independent holds ex B being independent Subset of M st ( A c= B & B is_maximal_independent_in C ) let C, A0 be Subset of M; ::_thesis: ( A0 c= C & A0 is independent implies ex B being independent Subset of M st ( A0 c= B & B is_maximal_independent_in C ) ) assume that A1: A0 c= C and A2: A0 is independent ; ::_thesis: ex B being independent Subset of M st ( A0 c= B & B is_maximal_independent_in C ) reconsider AA = A0 as independent Subset of M by A2; defpred S1[ Nat] means for A being finite Subset of M st A0 c= A & A c= C & A is independent holds card A <= $1; consider n being Nat such that A3: for A being finite Subset of M st A is independent holds card A <= n by Def7; reconsider n = n as Element of NAT by ORDINAL1:def_12; S1[n] by A3; then A4: ex n being Nat st S1[n] ; consider n0 being Nat such that A5: ( S1[n0] & ( for m being Nat st S1[m] holds n0 <= m ) ) from NAT_1:sch_5(A4); now__::_thesis:_ex_A_being_independent_Subset_of_M_st_ (_A0_c=_A_&_A_c=_C_&_not_card_A_<_n0_) 0 <= card AA by NAT_1:2; then A6: (card AA) + 1 >= 0 + 1 by XREAL_1:6; assume A7: for A being independent Subset of M st A0 c= A & A c= C holds card A < n0 ; ::_thesis: contradiction then card AA < n0 by A1; then (card AA) + 1 <= n0 by NAT_1:13; then consider n being Nat such that A8: n0 = 1 + n by A6, NAT_1:10, XXREAL_0:2; reconsider n = n as Element of NAT by ORDINAL1:def_12; S1[n] proof let A be finite Subset of M; ::_thesis: ( A0 c= A & A c= C & A is independent implies card A <= n ) assume that A9: A0 c= A and A10: A c= C and A11: A is independent ; ::_thesis: card A <= n card A < n + 1 by A7, A8, A9, A10, A11; hence card A <= n by NAT_1:13; ::_thesis: verum end; then n + 1 <= n by A5, A8; hence contradiction by NAT_1:13; ::_thesis: verum end; then consider A being independent Subset of M such that A12: A0 c= A and A13: A c= C and A14: card A >= n0 ; A15: card A <= n0 by A5, A12, A13; take A ; ::_thesis: ( A0 c= A & A is_maximal_independent_in C ) thus ( A0 c= A & A is independent & A c= C ) by A12, A13; :: according to MATROID0:def_10 ::_thesis: for B being Subset of M st B is independent & B c= C & A c= B holds A = B let B be Subset of M; ::_thesis: ( B is independent & B c= C & A c= B implies A = B ) assume that A16: B is independent and A17: B c= C and A18: A c= B ; ::_thesis: A = B reconsider B9 = B as independent Subset of M by A16; card A <= card B9 by A18, NAT_1:43; then A19: n0 <= card B9 by A14, XXREAL_0:2; A0 c= B by A12, A18, XBOOLE_1:1; then card B9 <= n0 by A5, A17; then card B9 = n0 by A19, XXREAL_0:1; hence A = B by A14, A18, A15, CARD_FIN:1, XXREAL_0:1; ::_thesis: verum end; theorem :: MATROID0:15 for M being non void subset-closed finite-degree SubsetFamilyStr for C being Subset of M ex A being independent Subset of M st A is_maximal_independent_in C proof let M be non void subset-closed finite-degree SubsetFamilyStr; ::_thesis: for C being Subset of M ex A being independent Subset of M st A is_maximal_independent_in C let C be Subset of M; ::_thesis: ex A being independent Subset of M st A is_maximal_independent_in C {} M c= C by XBOOLE_1:2; then ex A being independent Subset of M st ( {} M c= A & A is_maximal_independent_in C ) by Th14; hence ex A being independent Subset of M st A is_maximal_independent_in C ; ::_thesis: verum end; theorem Th16: :: MATROID0:16 for M being non empty non void subset-closed finite-degree SubsetFamilyStr holds ( M is Matroid iff for C being Subset of M for A, B being independent Subset of M st A is_maximal_independent_in C & B is_maximal_independent_in C holds card A = card B ) proof let M be non empty non void subset-closed finite-degree SubsetFamilyStr; ::_thesis: ( M is Matroid iff for C being Subset of M for A, B being independent Subset of M st A is_maximal_independent_in C & B is_maximal_independent_in C holds card A = card B ) hereby ::_thesis: ( ( for C being Subset of M for A, B being independent Subset of M st A is_maximal_independent_in C & B is_maximal_independent_in C holds card A = card B ) implies M is Matroid ) assume A1: M is Matroid ; ::_thesis: for C being Subset of M for A, B being independent Subset of M st A is_maximal_independent_in C & B is_maximal_independent_in C holds card A = card B let C be Subset of M; ::_thesis: for A, B being independent Subset of M st A is_maximal_independent_in C & B is_maximal_independent_in C holds card A = card B A2: now__::_thesis:_for_A,_B_being_independent_Subset_of_M_st_A_is_maximal_independent_in_C_&_B_is_maximal_independent_in_C_holds_ not_card_A_<_card_B let A, B be independent Subset of M; ::_thesis: ( A is_maximal_independent_in C & B is_maximal_independent_in C implies not card A < card B ) assume that A3: A is_maximal_independent_in C and A4: B is_maximal_independent_in C and A5: card A < card B ; ::_thesis: contradiction A6: A c= C by A3, Def10; (card A) + 1 <= card B by A5, NAT_1:13; then (card A) + 1 c= card B by NAT_1:39; then consider D being set such that A7: D c= B and A8: card D = (card A) + 1 by CARD_FIL:36; reconsider D = D as finite Subset of M by A7, XBOOLE_1:1; D is independent by A7, Th3; then consider e being Element of M such that A9: e in D \ A and A10: A \/ {e} is independent by A1, A8, Th4; D \ A c= D by XBOOLE_1:36; then A11: D \ A c= B by A7, XBOOLE_1:1; B c= C by A4, Def10; then D \ A c= C by A11, XBOOLE_1:1; then {e} c= C by A9, ZFMISC_1:31; then A12: A \/ {e} c= C by A6, XBOOLE_1:8; A c= A \/ {e} by XBOOLE_1:7; then A \/ {e} = A by A3, A10, A12, Def10; then {e} c= A by XBOOLE_1:7; then e in A by ZFMISC_1:31; hence contradiction by A9, XBOOLE_0:def_5; ::_thesis: verum end; let A, B be independent Subset of M; ::_thesis: ( A is_maximal_independent_in C & B is_maximal_independent_in C implies card A = card B ) assume that A13: A is_maximal_independent_in C and A14: B is_maximal_independent_in C ; ::_thesis: card A = card B ( card A < card B or card B < card A or card A = card B ) by XXREAL_0:1; hence card A = card B by A2, A13, A14; ::_thesis: verum end; assume A15: for C being Subset of M for A, B being independent Subset of M st A is_maximal_independent_in C & B is_maximal_independent_in C holds card A = card B ; ::_thesis: M is Matroid M is with_exchange_property proof let A, B be finite Subset of M; :: according to MATROID0:def_4 ::_thesis: ( A in the_family_of M & B in the_family_of M & card B = (card A) + 1 implies ex e being Element of M st ( e in B \ A & A \/ {e} in the_family_of M ) ) reconsider C = A \/ B as Subset of M ; assume that A16: A in the_family_of M and A17: B in the_family_of M and A18: card B = (card A) + 1 ; ::_thesis: ex e being Element of M st ( e in B \ A & A \/ {e} in the_family_of M ) B is independent by A17, Def2; then consider B9 being independent Subset of M such that A19: B c= B9 and A20: B9 is_maximal_independent_in C by Th14, XBOOLE_1:7; A21: card B <= card B9 by A19, NAT_1:43; assume A22: for e being Element of M st e in B \ A holds not A \/ {e} in the_family_of M ; ::_thesis: contradiction reconsider A = A as independent Subset of M by A16, Def2; A is_maximal_independent_in C proof thus A in the_family_of M by A16; :: according to MATROID0:def_2,MATROID0:def_10 ::_thesis: ( A c= C & ( for B being Subset of M st B is independent & B c= C & A c= B holds A = B ) ) thus A c= C by XBOOLE_1:7; ::_thesis: for B being Subset of M st B is independent & B c= C & A c= B holds A = B let D be Subset of M; ::_thesis: ( D is independent & D c= C & A c= D implies A = D ) assume that A23: D is independent and A24: D c= C and A25: A c= D ; ::_thesis: A = D assume ( not A c= D or not D c= A ) ; :: according to XBOOLE_0:def_10 ::_thesis: contradiction then consider e being set such that A26: e in D and A27: not e in A by A25, TARSKI:def_3; reconsider e = e as Element of M by A26; e in B by A24, A26, A27, XBOOLE_0:def_3; then e in B \ A by A27, XBOOLE_0:def_5; then not A \/ {e} in the_family_of M by A22; then A28: not A \/ {e} is independent by Def2; {e} c= D by A26, ZFMISC_1:31; then A \/ {e} c= D by A25, XBOOLE_1:8; hence contradiction by A23, A28, Th3; ::_thesis: verum end; then card A = card B9 by A15, A20; hence contradiction by A18, A21, NAT_1:13; ::_thesis: verum end; hence M is Matroid ; ::_thesis: verum end; definition let M be finite-degree Matroid; let C be Subset of M; func Rnk C -> Nat equals :: MATROID0:def 11 union { (card A) where A is independent Subset of M : A c= C } ; coherence union { (card A) where A is independent Subset of M : A c= C } is Nat proof set X = { (card A) where A is independent Subset of M : A c= C } ; defpred S1[ Nat] means ex A being independent Subset of M st ( A c= C & $1 = card A ); defpred S2[ Nat] means for A being independent Subset of M st A c= C holds card A <= $1; consider n being Nat such that A1: for A being finite Subset of M st A is independent holds card A <= n by Def7; A2: ex ne being Nat st S2[ne] proof take n ; ::_thesis: S2[n] thus S2[n] by A1; ::_thesis: verum end; consider n0 being Nat such that A3: ( S2[n0] & ( for m being Nat st S2[m] holds n0 <= m ) ) from NAT_1:sch_5(A2); union { (card A) where A is independent Subset of M : A c= C } = n0 proof now__::_thesis:_for_a_being_set_st_a_in__{__(card_A)_where_A_is_independent_Subset_of_M_:_A_c=_C__}__holds_ a_c=_n0 let a be set ; ::_thesis: ( a in { (card A) where A is independent Subset of M : A c= C } implies a c= n0 ) assume a in { (card A) where A is independent Subset of M : A c= C } ; ::_thesis: a c= n0 then consider A being independent Subset of M such that A4: a = card A and A5: A c= C ; card A <= n0 by A3, A5; hence a c= n0 by A4, NAT_1:39; ::_thesis: verum end; hence union { (card A) where A is independent Subset of M : A c= C } c= n0 by ZFMISC_1:76; :: according to XBOOLE_0:def_10 ::_thesis: not n0 c/= union { (card A) where A is independent Subset of M : A c= C } A6: {} M c= C by XBOOLE_1:2; A7: for k being Nat st S1[k] holds k <= n0 by A3; card {} = card {} ; then A8: ex n being Nat st S1[n] by A6; consider n being Nat such that A9: ( S1[n] & ( for m being Nat st S1[m] holds m <= n ) ) from NAT_1:sch_6(A7, A8); S2[n] by A9; then A10: n0 <= n by A3; n <= n0 by A3, A9; then n = n0 by A10, XXREAL_0:1; then n0 in { (card A) where A is independent Subset of M : A c= C } by A9; hence not n0 c/= union { (card A) where A is independent Subset of M : A c= C } by ZFMISC_1:74; ::_thesis: verum end; hence union { (card A) where A is independent Subset of M : A c= C } is Nat ; ::_thesis: verum end; end; :: deftheorem defines Rnk MATROID0:def_11_:_ for M being finite-degree Matroid for C being Subset of M holds Rnk C = union { (card A) where A is independent Subset of M : A c= C } ; theorem Th17: :: MATROID0:17 for M being finite-degree Matroid for C being Subset of M for A being independent Subset of M st A c= C holds card A <= Rnk C proof let M be finite-degree Matroid; ::_thesis: for C being Subset of M for A being independent Subset of M st A c= C holds card A <= Rnk C let C be Subset of M; ::_thesis: for A being independent Subset of M st A c= C holds card A <= Rnk C let A be independent Subset of M; ::_thesis: ( A c= C implies card A <= Rnk C ) assume A c= C ; ::_thesis: card A <= Rnk C then card A in { (card B) where B is independent Subset of M : B c= C } ; then card A c= Rnk C by ZFMISC_1:74; hence card A <= Rnk C by NAT_1:39; ::_thesis: verum end; theorem Th18: :: MATROID0:18 for M being finite-degree Matroid for C being Subset of M ex A being independent Subset of M st ( A c= C & card A = Rnk C ) proof let M be finite-degree Matroid; ::_thesis: for C being Subset of M ex A being independent Subset of M st ( A c= C & card A = Rnk C ) let C be Subset of M; ::_thesis: ex A being independent Subset of M st ( A c= C & card A = Rnk C ) defpred S1[ Nat] means for A being independent Subset of M st A c= C holds card A <= $1; defpred S2[ Nat] means ex A being independent Subset of M st ( A c= C & $1 = card A ); set X = { (card A) where A is independent Subset of M : A c= C } ; A1: {} M c= C by XBOOLE_1:2; card {} = card {} ; then A2: ex n being Nat st S2[n] by A1; consider n being Nat such that A3: for A being finite Subset of M st A is independent holds card A <= n by Def7; A4: ex ne being Nat st S1[ne] proof take n ; ::_thesis: S1[n] thus S1[n] by A3; ::_thesis: verum end; consider n0 being Nat such that A5: ( S1[n0] & ( for m being Nat st S1[m] holds n0 <= m ) ) from NAT_1:sch_5(A4); now__::_thesis:_for_a_being_set_st_a_in__{__(card_A)_where_A_is_independent_Subset_of_M_:_A_c=_C__}__holds_ a_c=_n0 let a be set ; ::_thesis: ( a in { (card A) where A is independent Subset of M : A c= C } implies a c= n0 ) assume a in { (card A) where A is independent Subset of M : A c= C } ; ::_thesis: a c= n0 then consider A being independent Subset of M such that A6: a = card A and A7: A c= C ; card A <= n0 by A5, A7; hence a c= n0 by A6, NAT_1:39; ::_thesis: verum end; then A8: Rnk C c= n0 by ZFMISC_1:76; A9: for k being Nat st S2[k] holds k <= n0 by A5; consider n being Nat such that A10: ( S2[n] & ( for m being Nat st S2[m] holds m <= n ) ) from NAT_1:sch_6(A9, A2); S1[n] by A10; then A11: n0 <= n by A5; consider A being independent Subset of M such that A12: A c= C and A13: n = card A by A10; take A ; ::_thesis: ( A c= C & card A = Rnk C ) n <= n0 by A5, A10; then A14: n = n0 by A11, XXREAL_0:1; then n0 in { (card A) where A is independent Subset of M : A c= C } by A12, A13; then n0 c= Rnk C by ZFMISC_1:74; hence ( A c= C & card A = Rnk C ) by A8, A12, A13, A14, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th19: :: MATROID0:19 for M being finite-degree Matroid for C being Subset of M for A being independent Subset of M holds ( A is_maximal_independent_in C iff ( A c= C & card A = Rnk C ) ) proof let M be finite-degree Matroid; ::_thesis: for C being Subset of M for A being independent Subset of M holds ( A is_maximal_independent_in C iff ( A c= C & card A = Rnk C ) ) let C be Subset of M; ::_thesis: for A being independent Subset of M holds ( A is_maximal_independent_in C iff ( A c= C & card A = Rnk C ) ) set X = { (card A) where A is independent Subset of M : A c= C } ; let A be independent Subset of M; ::_thesis: ( A is_maximal_independent_in C iff ( A c= C & card A = Rnk C ) ) consider B being independent Subset of M such that A1: B c= C and A2: card B = Rnk C by Th18; A3: now__::_thesis:_for_A_being_independent_Subset_of_M_st_A_c=_C_&_card_A_=_Rnk_C_holds_ A_is_maximal_independent_in_C let A be independent Subset of M; ::_thesis: ( A c= C & card A = Rnk C implies A is_maximal_independent_in C ) assume that A4: A c= C and A5: card A = Rnk C ; ::_thesis: A is_maximal_independent_in C thus A is_maximal_independent_in C ::_thesis: verum proof thus ( A is independent & A c= C ) by A4; :: according to MATROID0:def_10 ::_thesis: for B being Subset of M st B is independent & B c= C & A c= B holds A = B let B be Subset of M; ::_thesis: ( B is independent & B c= C & A c= B implies A = B ) assume B is independent ; ::_thesis: ( not B c= C or not A c= B or A = B ) then reconsider B9 = B as independent Subset of M ; assume B c= C ; ::_thesis: ( not A c= B or A = B ) then card B9 in { (card A) where A is independent Subset of M : A c= C } ; then A6: card B9 c= Rnk C by ZFMISC_1:74; assume A7: A c= B ; ::_thesis: A = B then card A c= card B9 by CARD_1:11; then card A = card B9 by A5, A6, XBOOLE_0:def_10; hence A = B by A7, CARD_FIN:1; ::_thesis: verum end; end; hereby ::_thesis: ( A c= C & card A = Rnk C implies A is_maximal_independent_in C ) assume A8: A is_maximal_independent_in C ; ::_thesis: ( A c= C & card A = Rnk C ) hence A c= C by Def10; ::_thesis: card A = Rnk C B is_maximal_independent_in C by A3, A1, A2; hence card A = Rnk C by A2, A8, Th16; ::_thesis: verum end; thus ( A c= C & card A = Rnk C implies A is_maximal_independent_in C ) by A3; ::_thesis: verum end; theorem Th20: :: MATROID0:20 for M being finite-degree Matroid for C being finite Subset of M holds Rnk C <= card C proof let M be finite-degree Matroid; ::_thesis: for C being finite Subset of M holds Rnk C <= card C let C be finite Subset of M; ::_thesis: Rnk C <= card C ex A being independent Subset of M st ( A c= C & card A = Rnk C ) by Th18; then Rnk C c= card C by CARD_1:11; hence Rnk C <= card C by NAT_1:39; ::_thesis: verum end; theorem Th21: :: MATROID0:21 for M being finite-degree Matroid for C being finite Subset of M holds ( C is independent iff card C = Rnk C ) proof let M be finite-degree Matroid; ::_thesis: for C being finite Subset of M holds ( C is independent iff card C = Rnk C ) let C be finite Subset of M; ::_thesis: ( C is independent iff card C = Rnk C ) set X = { (card A) where A is independent Subset of M : A c= C } ; hereby ::_thesis: ( card C = Rnk C implies C is independent ) assume C is independent ; ::_thesis: card C = Rnk C then card C in { (card A) where A is independent Subset of M : A c= C } ; then card C c= Rnk C by ZFMISC_1:74; then A1: card C <= Rnk C by NAT_1:39; Rnk C <= card C by Th20; hence card C = Rnk C by A1, XXREAL_0:1; ::_thesis: verum end; ex A being independent Subset of M st ( A c= C & card A = Rnk C ) by Th18; hence ( card C = Rnk C implies C is independent ) by CARD_FIN:1; ::_thesis: verum end; definition let M be finite-degree Matroid; func Rnk M -> Nat equals :: MATROID0:def 12 Rnk ([#] M); coherence Rnk ([#] M) is Nat ; end; :: deftheorem defines Rnk MATROID0:def_12_:_ for M being finite-degree Matroid holds Rnk M = Rnk ([#] M); definition let M be non void finite-degree SubsetFamilyStr; mode Basis of M -> independent Subset of M means :Def13: :: MATROID0:def 13 it is_maximal_independent_in [#] M; existence ex b1 being independent Subset of M st b1 is_maximal_independent_in [#] M proof set A = the independent Subset of M; set C = [#] M; consider B being independent Subset of M such that the independent Subset of M c= B and A1: B is_maximal_independent_in [#] M by Th14; take B ; ::_thesis: B is_maximal_independent_in [#] M thus B is_maximal_independent_in [#] M by A1; ::_thesis: verum end; end; :: deftheorem Def13 defines Basis MATROID0:def_13_:_ for M being non void finite-degree SubsetFamilyStr for b2 being independent Subset of M holds ( b2 is Basis of M iff b2 is_maximal_independent_in [#] M ); theorem :: MATROID0:22 for M being finite-degree Matroid for B1, B2 being Basis of M holds card B1 = card B2 proof let M be finite-degree Matroid; ::_thesis: for B1, B2 being Basis of M holds card B1 = card B2 let B1, B2 be Basis of M; ::_thesis: card B1 = card B2 A1: B2 is_maximal_independent_in [#] M by Def13; B1 is_maximal_independent_in [#] M by Def13; hence card B1 = card B2 by A1, Th16; ::_thesis: verum end; theorem :: MATROID0:23 for M being finite-degree Matroid for A being independent Subset of M ex B being Basis of M st A c= B proof let M be finite-degree Matroid; ::_thesis: for A being independent Subset of M ex B being Basis of M st A c= B let A be independent Subset of M; ::_thesis: ex B being Basis of M st A c= B consider B being independent Subset of M such that A1: A c= B and A2: B is_maximal_independent_in [#] M by Th14; reconsider B = B as Basis of M by A2, Def13; take B ; ::_thesis: A c= B thus A c= B by A1; ::_thesis: verum end; theorem Th24: :: MATROID0:24 for M being finite-degree Matroid for A, B being Subset of M st A c= B holds Rnk A <= Rnk B proof let M be finite-degree Matroid; ::_thesis: for A, B being Subset of M st A c= B holds Rnk A <= Rnk B let A, B be Subset of M; ::_thesis: ( A c= B implies Rnk A <= Rnk B ) ex C being independent Subset of M st ( C c= A & card C = Rnk A ) by Th18; hence ( A c= B implies Rnk A <= Rnk B ) by Th17, XBOOLE_1:1; ::_thesis: verum end; theorem Th25: :: MATROID0:25 for M being finite-degree Matroid for A, B being Subset of M holds (Rnk (A \/ B)) + (Rnk (A /\ B)) <= (Rnk A) + (Rnk B) proof let M be finite-degree Matroid; ::_thesis: for A, B being Subset of M holds (Rnk (A \/ B)) + (Rnk (A /\ B)) <= (Rnk A) + (Rnk B) let A, B be Subset of M; ::_thesis: (Rnk (A \/ B)) + (Rnk (A /\ B)) <= (Rnk A) + (Rnk B) consider C being independent Subset of M such that A1: C c= A /\ B and A2: card C = Rnk (A /\ B) by Th18; A /\ B c= A by XBOOLE_1:17; then C c= A by A1, XBOOLE_1:1; then consider Ca being independent Subset of M such that A3: C c= Ca and A4: Ca is_maximal_independent_in A by Th14; A5: Ca c= A by A4, Def10; A6: Ca /\ B c= C proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Ca /\ B or x in C ) assume A7: x in Ca /\ B ; ::_thesis: x in C then A8: x in Ca by XBOOLE_0:def_4; then {x} c= Ca by ZFMISC_1:31; then C \/ {x} c= Ca by A3, XBOOLE_1:8; then reconsider Cx = C \/ {x} as independent Subset of M by Th3, XBOOLE_1:1; x in B by A7, XBOOLE_0:def_4; then x in A /\ B by A5, A8, XBOOLE_0:def_4; then {x} c= A /\ B by ZFMISC_1:31; then A9: Cx c= A /\ B by A1, XBOOLE_1:8; A10: C c= Cx by XBOOLE_1:7; C is_maximal_independent_in A /\ B by A1, A2, Th19; then C = Cx by A9, A10, Def10; then {x} c= C by XBOOLE_1:7; hence x in C by ZFMISC_1:31; ::_thesis: verum end; A /\ B c= B by XBOOLE_1:17; then C c= B by A1, XBOOLE_1:1; then C c= Ca /\ B by A3, XBOOLE_1:19; then A11: Ca /\ B = C by A6, XBOOLE_0:def_10; A c= A \/ B by XBOOLE_1:7; then Ca c= A \/ B by A5, XBOOLE_1:1; then consider C9 being independent Subset of M such that A12: Ca c= C9 and A13: C9 is_maximal_independent_in A \/ B by Th14; A14: Ca /\ (C9 /\ B) = (Ca /\ C9) /\ B by XBOOLE_1:16 .= Ca /\ B by A12, XBOOLE_1:28 ; A15: C9 c= A \/ B by A13, Th19; A16: C9 = Ca \/ (C9 /\ B) proof thus C9 c= Ca \/ (C9 /\ B) :: according to XBOOLE_0:def_10 ::_thesis: not Ca \/ (C9 /\ B) c/= C9 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C9 or x in Ca \/ (C9 /\ B) ) assume A17: x in C9 ; ::_thesis: x in Ca \/ (C9 /\ B) then {x} c= C9 by ZFMISC_1:31; then Ca \/ {x} c= C9 by A12, XBOOLE_1:8; then reconsider Cax = Ca \/ {x} as independent Subset of M by Th3, XBOOLE_1:1; A18: now__::_thesis:_(_x_in_A_implies_x_in_Ca_) assume x in A ; ::_thesis: x in Ca then {x} c= A by ZFMISC_1:31; then A19: Cax c= A by A5, XBOOLE_1:8; Ca c= Cax by XBOOLE_1:7; then Ca = Cax by A4, A19, Def10; then {x} c= Ca by XBOOLE_1:7; hence x in Ca by ZFMISC_1:31; ::_thesis: verum end; ( x in B implies x in C9 /\ B ) by A17, XBOOLE_0:def_4; hence x in Ca \/ (C9 /\ B) by A15, A17, A18, XBOOLE_0:def_3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Ca \/ (C9 /\ B) or x in C9 ) assume x in Ca \/ (C9 /\ B) ; ::_thesis: x in C9 then ( x in Ca or x in C9 /\ B ) by XBOOLE_0:def_3; hence x in C9 by A12, XBOOLE_0:def_4; ::_thesis: verum end; C9 /\ B c= B by XBOOLE_1:17; then consider Cb being independent Subset of M such that A20: C9 /\ B c= Cb and A21: Cb is_maximal_independent_in B by Th14; card Cb = Rnk B by A21, Th19; then A22: card (C9 /\ B) <= Rnk B by A20, NAT_1:43; A23: card C9 = Rnk (A \/ B) by A13, Th19; card Ca = Rnk A by A4, Th19; then Rnk (A \/ B) = ((Rnk A) + (card (C9 /\ B))) - (Rnk (A /\ B)) by A2, A23, A16, A14, A11, CARD_2:45; hence (Rnk (A \/ B)) + (Rnk (A /\ B)) <= (Rnk A) + (Rnk B) by A22, XREAL_1:6; ::_thesis: verum end; theorem Th26: :: MATROID0:26 for M being finite-degree Matroid for A, B being Subset of M for e being Element of M holds ( Rnk A <= Rnk (A \/ B) & Rnk (A \/ {e}) <= (Rnk A) + 1 ) proof let M be finite-degree Matroid; ::_thesis: for A, B being Subset of M for e being Element of M holds ( Rnk A <= Rnk (A \/ B) & Rnk (A \/ {e}) <= (Rnk A) + 1 ) let A, B be Subset of M; ::_thesis: for e being Element of M holds ( Rnk A <= Rnk (A \/ B) & Rnk (A \/ {e}) <= (Rnk A) + 1 ) let e be Element of M; ::_thesis: ( Rnk A <= Rnk (A \/ B) & Rnk (A \/ {e}) <= (Rnk A) + 1 ) A1: card {e} = 1 by CARD_1:30; thus Rnk A <= Rnk (A \/ B) by Th24, XBOOLE_1:7; ::_thesis: Rnk (A \/ {e}) <= (Rnk A) + 1 A2: (Rnk (A \/ {e})) + (Rnk (A /\ {e})) <= (Rnk A) + (Rnk {e}) by Th25; Rnk {e} <= card {e} by Th20; then (Rnk A) + (Rnk {e}) <= (Rnk A) + 1 by A1, XREAL_1:6; then A3: (Rnk (A \/ {e})) + (Rnk (A /\ {e})) <= (Rnk A) + 1 by A2, XXREAL_0:2; Rnk (A \/ {e}) <= (Rnk (A \/ {e})) + (Rnk (A /\ {e})) by NAT_1:11; hence Rnk (A \/ {e}) <= (Rnk A) + 1 by A3, XXREAL_0:2; ::_thesis: verum end; theorem :: MATROID0:27 for M being finite-degree Matroid for A being Subset of M for e, f being Element of M st Rnk (A \/ {e}) = Rnk (A \/ {f}) & Rnk (A \/ {f}) = Rnk A holds Rnk (A \/ {e,f}) = Rnk A proof let M be finite-degree Matroid; ::_thesis: for A being Subset of M for e, f being Element of M st Rnk (A \/ {e}) = Rnk (A \/ {f}) & Rnk (A \/ {f}) = Rnk A holds Rnk (A \/ {e,f}) = Rnk A let A be Subset of M; ::_thesis: for e, f being Element of M st Rnk (A \/ {e}) = Rnk (A \/ {f}) & Rnk (A \/ {f}) = Rnk A holds Rnk (A \/ {e,f}) = Rnk A let e, f be Element of M; ::_thesis: ( Rnk (A \/ {e}) = Rnk (A \/ {f}) & Rnk (A \/ {f}) = Rnk A implies Rnk (A \/ {e,f}) = Rnk A ) assume that A1: Rnk (A \/ {e}) = Rnk (A \/ {f}) and A2: Rnk (A \/ {f}) = Rnk A ; ::_thesis: Rnk (A \/ {e,f}) = Rnk A consider C being independent Subset of M such that A3: C c= A and A4: card C = Rnk A by Th18; A5: C is_maximal_independent_in A by A3, A4, Th19; A c= A \/ {f} by XBOOLE_1:7; then C c= A \/ {f} by A3, XBOOLE_1:1; then A6: C is_maximal_independent_in A \/ {f} by A4, A2, Th19; A c= A \/ {e} by XBOOLE_1:7; then C c= A \/ {e} by A3, XBOOLE_1:1; then A7: C is_maximal_independent_in A \/ {e} by A4, A1, A2, Th19; A c= A \/ {e,f} by XBOOLE_1:7; then C c= A \/ {e,f} by A3, XBOOLE_1:1; then consider C9 being independent Subset of M such that A8: C c= C9 and A9: C9 is_maximal_independent_in A \/ {e,f} by Th14; A10: C9 c= A \/ {e,f} by A9, Th19; now__::_thesis:_not_C9_<>_C assume C9 <> C ; ::_thesis: contradiction then consider x being set such that A11: ( ( x in C9 & not x in C ) or ( x in C & not x in C9 ) ) by TARSKI:1; {x} c= C9 by A8, A11, ZFMISC_1:31; then C \/ {x} c= C9 by A8, XBOOLE_1:8; then reconsider Cx = C \/ {x} as independent Subset of M by Th3, XBOOLE_1:1; now__::_thesis:_not_x_in_A assume x in A ; ::_thesis: contradiction then {x} c= A by ZFMISC_1:31; then A12: Cx c= A by A3, XBOOLE_1:8; C c= Cx by XBOOLE_1:7; then C = Cx by A5, A12, Def10; then {x} c= C by XBOOLE_1:7; hence contradiction by A8, A11, ZFMISC_1:31; ::_thesis: verum end; then x in {e,f} by A8, A10, A11, XBOOLE_0:def_3; then ( x = e or x = f ) by TARSKI:def_2; then ( ( {x} c= A \/ {e} & C c= A \/ {e} ) or ( {x} c= A \/ {f} & C c= A \/ {f} ) ) by A3, XBOOLE_1:10; then A13: ( Cx c= A \/ {e} or Cx c= A \/ {f} ) by XBOOLE_1:8; C c= Cx by XBOOLE_1:7; then C = Cx by A7, A6, A13, Def10; then {x} c= C by XBOOLE_1:7; hence contradiction by A8, A11, ZFMISC_1:31; ::_thesis: verum end; hence Rnk (A \/ {e,f}) = Rnk A by A4, A9, Th19; ::_thesis: verum end; begin definition let M be finite-degree Matroid; let e be Element of M; let A be Subset of M; prede is_dependent_on A means :Def14: :: MATROID0:def 14 Rnk (A \/ {e}) = Rnk A; end; :: deftheorem Def14 defines is_dependent_on MATROID0:def_14_:_ for M being finite-degree Matroid for e being Element of M for A being Subset of M holds ( e is_dependent_on A iff Rnk (A \/ {e}) = Rnk A ); theorem Th28: :: MATROID0:28 for M being finite-degree Matroid for A being Subset of M for e being Element of M st e in A holds e is_dependent_on A proof let M be finite-degree Matroid; ::_thesis: for A being Subset of M for e being Element of M st e in A holds e is_dependent_on A let A be Subset of M; ::_thesis: for e being Element of M st e in A holds e is_dependent_on A let e be Element of M; ::_thesis: ( e in A implies e is_dependent_on A ) assume e in A ; ::_thesis: e is_dependent_on A then {e} c= A by ZFMISC_1:31; hence Rnk (A \/ {e}) = Rnk A by XBOOLE_1:12; :: according to MATROID0:def_14 ::_thesis: verum end; theorem Th29: :: MATROID0:29 for M being finite-degree Matroid for A, B being Subset of M for e being Element of M st A c= B & e is_dependent_on A holds e is_dependent_on B proof let M be finite-degree Matroid; ::_thesis: for A, B being Subset of M for e being Element of M st A c= B & e is_dependent_on A holds e is_dependent_on B let A, B be Subset of M; ::_thesis: for e being Element of M st A c= B & e is_dependent_on A holds e is_dependent_on B let e be Element of M; ::_thesis: ( A c= B & e is_dependent_on A implies e is_dependent_on B ) assume that A1: A c= B and A2: Rnk (A \/ {e}) = Rnk A ; :: according to MATROID0:def_14 ::_thesis: e is_dependent_on B consider Ca being independent Subset of M such that A3: Ca c= A and A4: card Ca = Rnk A by Th18; A5: Ca c= B by A1, A3, XBOOLE_1:1; B c= B \/ {e} by XBOOLE_1:7; then Ca c= B \/ {e} by A5, XBOOLE_1:1; then consider E being independent Subset of M such that A6: Ca c= E and A7: E is_maximal_independent_in B \/ {e} by Th14; A8: now__::_thesis:_not_Rnk_(B_\/_{e})_=_(Rnk_B)_+_1 E c= B \/ {e} by A7, Th19; then A9: E = E /\ (B \/ {e}) by XBOOLE_1:28 .= (E /\ B) \/ (E /\ {e}) by XBOOLE_1:23 ; E /\ {e} c= {e} by XBOOLE_1:17; then A10: ( ( E /\ {e} = {} & card {} = 0 ) or ( E /\ {e} = {e} & card {e} = 1 ) ) by CARD_1:30, ZFMISC_1:33; card (E /\ B) <= Rnk B by Th17, XBOOLE_1:17; then A11: (card (E /\ B)) + 1 <= (Rnk B) + 1 by XREAL_1:6; Ca c= A \/ {e} by A3, XBOOLE_1:10; then A12: Ca is_maximal_independent_in A \/ {e} by A2, A4, Th19; A13: Ca c= Ca \/ {e} by XBOOLE_1:10; assume A14: Rnk (B \/ {e}) = (Rnk B) + 1 ; ::_thesis: contradiction then card E = (Rnk B) + 1 by A7, Th19; then (Rnk B) + 1 <= (card (E /\ B)) + (card (E /\ {e})) by A9, CARD_2:43; then (card (E /\ B)) + 1 <= (card (E /\ B)) + (card (E /\ {e})) by A11, XXREAL_0:2; then e in E /\ {e} by A10, TARSKI:def_1, XREAL_1:6; then e in E by XBOOLE_0:def_4; then {e} c= E by ZFMISC_1:31; then Ca \/ {e} c= E by A6, XBOOLE_1:8; then A15: Ca \/ {e} is independent by Th3; Ca \/ {e} c= A \/ {e} by A3, XBOOLE_1:9; then Ca = Ca \/ {e} by A13, A15, A12, Def10; then {e} c= Ca by XBOOLE_1:7; then B = B \/ {e} by A5, XBOOLE_1:1, XBOOLE_1:12; hence contradiction by A14; ::_thesis: verum end; A16: Rnk (B \/ {e}) <= (Rnk B) + 1 by Th26; Rnk B <= Rnk (B \/ {e}) by Th26; hence Rnk (B \/ {e}) = Rnk B by A16, A8, NAT_1:9; :: according to MATROID0:def_14 ::_thesis: verum end; definition let M be finite-degree Matroid; let A be Subset of M; func Span A -> Subset of M equals :: MATROID0:def 15 { e where e is Element of M : e is_dependent_on A } ; coherence { e where e is Element of M : e is_dependent_on A } is Subset of M proof set X = { e where e is Element of M : e is_dependent_on A } ; { e where e is Element of M : e is_dependent_on A } c= the carrier of M proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { e where e is Element of M : e is_dependent_on A } or x in the carrier of M ) assume x in { e where e is Element of M : e is_dependent_on A } ; ::_thesis: x in the carrier of M then ex e being Element of M st ( x = e & e is_dependent_on A ) ; hence x in the carrier of M ; ::_thesis: verum end; hence { e where e is Element of M : e is_dependent_on A } is Subset of M ; ::_thesis: verum end; end; :: deftheorem defines Span MATROID0:def_15_:_ for M being finite-degree Matroid for A being Subset of M holds Span A = { e where e is Element of M : e is_dependent_on A } ; theorem Th30: :: MATROID0:30 for M being finite-degree Matroid for A being Subset of M for e being Element of M holds ( e in Span A iff Rnk (A \/ {e}) = Rnk A ) proof let M be finite-degree Matroid; ::_thesis: for A being Subset of M for e being Element of M holds ( e in Span A iff Rnk (A \/ {e}) = Rnk A ) let A be Subset of M; ::_thesis: for e being Element of M holds ( e in Span A iff Rnk (A \/ {e}) = Rnk A ) let e be Element of M; ::_thesis: ( e in Span A iff Rnk (A \/ {e}) = Rnk A ) hereby ::_thesis: ( Rnk (A \/ {e}) = Rnk A implies e in Span A ) assume e in Span A ; ::_thesis: Rnk (A \/ {e}) = Rnk A then ex x being Element of M st ( e = x & x is_dependent_on A ) ; hence Rnk (A \/ {e}) = Rnk A by Def14; ::_thesis: verum end; assume Rnk (A \/ {e}) = Rnk A ; ::_thesis: e in Span A then e is_dependent_on A by Def14; hence e in Span A ; ::_thesis: verum end; theorem Th31: :: MATROID0:31 for M being finite-degree Matroid for A being Subset of M holds A c= Span A proof let M be finite-degree Matroid; ::_thesis: for A being Subset of M holds A c= Span A let A be Subset of M; ::_thesis: A c= Span A let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in A or e in Span A ) assume A1: e in A ; ::_thesis: e in Span A then reconsider x = e as Element of M ; x is_dependent_on A by A1, Th28; hence e in Span A ; ::_thesis: verum end; theorem :: MATROID0:32 for M being finite-degree Matroid for A, B being Subset of M st A c= B holds Span A c= Span B proof let M be finite-degree Matroid; ::_thesis: for A, B being Subset of M st A c= B holds Span A c= Span B let A, B be Subset of M; ::_thesis: ( A c= B implies Span A c= Span B ) assume A1: A c= B ; ::_thesis: Span A c= Span B let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Span A or x in Span B ) assume x in Span A ; ::_thesis: x in Span B then ex e being Element of M st ( x = e & e is_dependent_on A ) ; then ex e being Element of M st ( x = e & e is_dependent_on B ) by A1, Th29; hence x in Span B ; ::_thesis: verum end; theorem Th33: :: MATROID0:33 for M being finite-degree Matroid for A being Subset of M holds Rnk (Span A) = Rnk A proof let M be finite-degree Matroid; ::_thesis: for A being Subset of M holds Rnk (Span A) = Rnk A let A be Subset of M; ::_thesis: Rnk (Span A) = Rnk A consider Ca being independent Subset of M such that A1: Ca c= A and A2: card Ca = Rnk A by Th18; A c= Span A by Th31; then Ca c= Span A by A1, XBOOLE_1:1; then consider C being independent Subset of M such that A3: Ca c= C and A4: C is_maximal_independent_in Span A by Th14; now__::_thesis:_not_C_c/=_Ca assume C c/= Ca ; ::_thesis: contradiction then consider x being set such that A5: x in C and A6: x nin Ca by TARSKI:def_3; C c= Span A by A4, Th19; then x in Span A by A5; then consider e being Element of M such that A7: x = e and A8: e is_dependent_on A ; {e} c= C by A5, A7, ZFMISC_1:31; then Ca \/ {e} c= C by A3, XBOOLE_1:8; then reconsider Ce = Ca \/ {e} as independent Subset of M by Th3; Ce c= A \/ {e} by A1, XBOOLE_1:9; then consider D being independent Subset of M such that A9: Ce c= D and A10: D is_maximal_independent_in A \/ {e} by Th14; card Ca = Rnk (A \/ {e}) by A2, A8, Def14 .= card D by A10, Th19 ; then A11: card Ce <= card Ca by A9, NAT_1:43; card Ca <= card Ce by NAT_1:43, XBOOLE_1:7; then card Ca = card Ce by A11, XXREAL_0:1; then Ca = Ce by CARD_FIN:1, XBOOLE_1:7; then e nin {e} by A6, A7, XBOOLE_0:def_3; hence contradiction by TARSKI:def_1; ::_thesis: verum end; then C = Ca by A3, XBOOLE_0:def_10; hence Rnk (Span A) = Rnk A by A2, A4, Th19; ::_thesis: verum end; theorem Th34: :: MATROID0:34 for M being finite-degree Matroid for A being Subset of M for e being Element of M st e is_dependent_on Span A holds e is_dependent_on A proof let M be finite-degree Matroid; ::_thesis: for A being Subset of M for e being Element of M st e is_dependent_on Span A holds e is_dependent_on A let A be Subset of M; ::_thesis: for e being Element of M st e is_dependent_on Span A holds e is_dependent_on A let e be Element of M; ::_thesis: ( e is_dependent_on Span A implies e is_dependent_on A ) assume A1: Rnk ((Span A) \/ {e}) = Rnk (Span A) ; :: according to MATROID0:def_14 ::_thesis: e is_dependent_on A A2: Rnk A = Rnk (Span A) by Th33; consider Ca being independent Subset of M such that A3: Ca c= A and A4: card Ca = Rnk A by Th18; A5: Rnk A = Rnk Ca by A4, Th21; A6: Rnk Ca <= Rnk (A \/ {e}) by A3, Th24, XBOOLE_1:10; A c= Span A by Th31; then Rnk (A \/ {e}) <= Rnk A by A1, A2, Th24, XBOOLE_1:9; hence Rnk (A \/ {e}) = Rnk A by A5, A6, XXREAL_0:1; :: according to MATROID0:def_14 ::_thesis: verum end; theorem :: MATROID0:35 for M being finite-degree Matroid for A being Subset of M holds Span (Span A) = Span A proof let M be finite-degree Matroid; ::_thesis: for A being Subset of M holds Span (Span A) = Span A let A be Subset of M; ::_thesis: Span (Span A) = Span A thus Span (Span A) c= Span A :: according to XBOOLE_0:def_10 ::_thesis: not Span A c/= Span (Span A) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Span (Span A) or x in Span A ) assume x in Span (Span A) ; ::_thesis: x in Span A then consider e being Element of M such that A1: x = e and A2: e is_dependent_on Span A ; e is_dependent_on A by A2, Th34; hence x in Span A by A1; ::_thesis: verum end; thus not Span A c/= Span (Span A) by Th31; ::_thesis: verum end; theorem :: MATROID0:36 for M being finite-degree Matroid for A being Subset of M for f, e being Element of M st f nin Span A & f in Span (A \/ {e}) holds e in Span (A \/ {f}) proof let M be finite-degree Matroid; ::_thesis: for A being Subset of M for f, e being Element of M st f nin Span A & f in Span (A \/ {e}) holds e in Span (A \/ {f}) let A be Subset of M; ::_thesis: for f, e being Element of M st f nin Span A & f in Span (A \/ {e}) holds e in Span (A \/ {f}) let f, e be Element of M; ::_thesis: ( f nin Span A & f in Span (A \/ {e}) implies e in Span (A \/ {f}) ) assume that A1: f nin Span A and A2: f in Span (A \/ {e}) ; ::_thesis: e in Span (A \/ {f}) A3: Rnk A <= Rnk (A \/ {f}) by Th26; A4: Rnk (A \/ {f}) <= (Rnk A) + 1 by Th26; Rnk A <> Rnk (A \/ {f}) by A1, Th30; then A5: Rnk (A \/ {f}) = (Rnk A) + 1 by A3, A4, NAT_1:9; A6: (A \/ {f}) \/ {e} = A \/ ({f} \/ {e}) by XBOOLE_1:4; A7: Rnk (A \/ {e}) <= (Rnk A) + 1 by Th26; A8: (A \/ {e}) \/ {f} = A \/ ({e} \/ {f}) by XBOOLE_1:4; A9: Rnk ((A \/ {e}) \/ {f}) = Rnk (A \/ {e}) by A2, Th30; then Rnk (A \/ {f}) <= Rnk (A \/ {e}) by A6, A8, Th26; then Rnk (A \/ {f}) = Rnk ((A \/ {f}) \/ {e}) by A9, A5, A6, A8, A7, XXREAL_0:1; hence e in Span (A \/ {f}) by Th30; ::_thesis: verum end; definition let M be SubsetFamilyStr; let A be Subset of M; attrA is cycle means :Def16: :: MATROID0:def 16 ( A is dependent & ( for e being Element of M st e in A holds A \ {e} is independent ) ); end; :: deftheorem Def16 defines cycle MATROID0:def_16_:_ for M being SubsetFamilyStr for A being Subset of M holds ( A is cycle iff ( A is dependent & ( for e being Element of M st e in A holds A \ {e} is independent ) ) ); theorem Th37: :: MATROID0:37 for M being finite-degree Matroid for A being Subset of M st A is cycle holds ( not A is empty & A is finite ) proof let M be finite-degree Matroid; ::_thesis: for A being Subset of M st A is cycle holds ( not A is empty & A is finite ) let A be Subset of M; ::_thesis: ( A is cycle implies ( not A is empty & A is finite ) ) assume that A1: A is dependent and A2: for e being Element of M st e in A holds A \ {e} is independent ; :: according to MATROID0:def_16 ::_thesis: ( not A is empty & A is finite ) thus not A is empty by A1; ::_thesis: A is finite set e = the Element of A; now__::_thesis:_(_A_is_non_empty_set_implies_A_is_finite_) assume A3: A is non empty set ; ::_thesis: A is finite then the Element of A in A ; then reconsider e = the Element of A as Element of M ; reconsider Ae = A \ {e} as independent Subset of M by A2, A3; A = Ae \/ {e} by A3, ZFMISC_1:116; hence A is finite ; ::_thesis: verum end; hence A is finite ; ::_thesis: verum end; registration let M be finite-degree Matroid; cluster cycle -> non empty finite for Element of K19( the carrier of M); coherence for b1 being Subset of M st b1 is cycle holds ( not b1 is empty & b1 is finite ) by Th37; end; theorem Th38: :: MATROID0:38 for M being finite-degree Matroid for A being Subset of M holds ( A is cycle iff ( not A is empty & ( for e being Element of M st e in A holds A \ {e} is_maximal_independent_in A ) ) ) proof let M be finite-degree Matroid; ::_thesis: for A being Subset of M holds ( A is cycle iff ( not A is empty & ( for e being Element of M st e in A holds A \ {e} is_maximal_independent_in A ) ) ) let A be Subset of M; ::_thesis: ( A is cycle iff ( not A is empty & ( for e being Element of M st e in A holds A \ {e} is_maximal_independent_in A ) ) ) thus ( A is cycle implies ( not A is empty & ( for e being Element of M st e in A holds A \ {e} is_maximal_independent_in A ) ) ) ::_thesis: ( not A is empty & ( for e being Element of M st e in A holds A \ {e} is_maximal_independent_in A ) implies A is cycle ) proof assume that A1: A is dependent and A2: for e being Element of M st e in A holds A \ {e} is independent ; :: according to MATROID0:def_16 ::_thesis: ( not A is empty & ( for e being Element of M st e in A holds A \ {e} is_maximal_independent_in A ) ) thus not A is empty by A1; ::_thesis: for e being Element of M st e in A holds A \ {e} is_maximal_independent_in A let e be Element of M; ::_thesis: ( e in A implies A \ {e} is_maximal_independent_in A ) set Ae = A \ {e}; assume A3: e in A ; ::_thesis: A \ {e} is_maximal_independent_in A hence ( A \ {e} is independent & A \ {e} c= A ) by A2, XBOOLE_1:36; :: according to MATROID0:def_10 ::_thesis: for B being Subset of M st B is independent & B c= A & A \ {e} c= B holds A \ {e} = B let B be Subset of M; ::_thesis: ( B is independent & B c= A & A \ {e} c= B implies A \ {e} = B ) assume that A4: B is independent and A5: B c= A and A6: A \ {e} c= B ; ::_thesis: A \ {e} = B A = (A \ {e}) \/ {e} by A3, ZFMISC_1:116; hence A \ {e} = B by A1, A4, A5, A6, ZFMISC_1:138; ::_thesis: verum end; set a = the Element of A; assume that A7: not A is empty and A8: for e being Element of M st e in A holds A \ {e} is_maximal_independent_in A ; ::_thesis: A is cycle the Element of A in A by A7; then reconsider a = the Element of A as Element of M ; set Ae = A \ {a}; A9: A \ {a} c= A by XBOOLE_1:36; A10: A \ {a} is_maximal_independent_in A by A7, A8; hereby :: according to MATROID0:def_16 ::_thesis: for e being Element of M st e in A holds A \ {e} is independent assume A is independent ; ::_thesis: contradiction then A = A \ {a} by A10, A9, Def10; then a nin {a} by A7, XBOOLE_0:def_5; hence contradiction by TARSKI:def_1; ::_thesis: verum end; let e be Element of M; ::_thesis: ( e in A implies A \ {e} is independent ) assume e in A ; ::_thesis: A \ {e} is independent then A \ {e} is_maximal_independent_in A by A8; hence A \ {e} is independent by Def10; ::_thesis: verum end; theorem Th39: :: MATROID0:39 for M being finite-degree Matroid for A being Subset of M st A is cycle holds (Rnk A) + 1 = card A proof let M be finite-degree Matroid; ::_thesis: for A being Subset of M st A is cycle holds (Rnk A) + 1 = card A let A be Subset of M; ::_thesis: ( A is cycle implies (Rnk A) + 1 = card A ) assume A1: A is cycle ; ::_thesis: (Rnk A) + 1 = card A then reconsider A = A as non empty finite Subset of M ; set a = the Element of A; A2: A \ { the Element of A} is_maximal_independent_in A by A1, Th38; then A \ { the Element of A} is independent by Def10; then A3: Rnk A = card (A \ { the Element of A}) by A2, Th19; the Element of A in { the Element of A} by TARSKI:def_1; then A4: the Element of A nin A \ { the Element of A} by XBOOLE_0:def_5; A = (A \ { the Element of A}) \/ { the Element of A} by ZFMISC_1:116; hence (Rnk A) + 1 = card A by A3, A4, CARD_2:41; ::_thesis: verum end; theorem :: MATROID0:40 for M being finite-degree Matroid for A being Subset of M for e being Element of M st A is cycle & e in A holds e is_dependent_on A \ {e} proof let M be finite-degree Matroid; ::_thesis: for A being Subset of M for e being Element of M st A is cycle & e in A holds e is_dependent_on A \ {e} let A be Subset of M; ::_thesis: for e being Element of M st A is cycle & e in A holds e is_dependent_on A \ {e} let e be Element of M; ::_thesis: ( A is cycle & e in A implies e is_dependent_on A \ {e} ) assume that A1: A is cycle and A2: e in A ; ::_thesis: e is_dependent_on A \ {e} reconsider Ae = A \ {e} as independent Subset of M by A1, A2, Def16; Ae is_maximal_independent_in A by A1, A2, Th38; then Rnk A = card Ae by Th19; hence Rnk ((A \ {e}) \/ {e}) = card Ae by A2, ZFMISC_1:116 .= Rnk (A \ {e}) by Th21 ; :: according to MATROID0:def_14 ::_thesis: verum end; theorem Th41: :: MATROID0:41 for M being finite-degree Matroid for A, B being Subset of M st A is cycle & B is cycle & A c= B holds A = B proof let M be finite-degree Matroid; ::_thesis: for A, B being Subset of M st A is cycle & B is cycle & A c= B holds A = B let A, B be Subset of M; ::_thesis: ( A is cycle & B is cycle & A c= B implies A = B ) assume that A1: A is dependent and for e being Element of M st e in A holds A \ {e} is independent and B is dependent and A2: for e being Element of M st e in B holds B \ {e} is independent ; :: according to MATROID0:def_16 ::_thesis: ( not A c= B or A = B ) assume that A3: A c= B and A4: A <> B ; ::_thesis: contradiction consider x being set such that A5: ( ( x in A & not x in B ) or ( x in B & not x in A ) ) by A4, TARSKI:1; reconsider x = x as Element of M by A5; A6: A c= B \ {x} by A3, A5, ZFMISC_1:34; B \ {x} is independent by A2, A3, A5; hence contradiction by A1, A6, Th3; ::_thesis: verum end; theorem Th42: :: MATROID0:42 for M being finite-degree Matroid for A being Subset of M st ( for B being Subset of M st B c= A holds not B is cycle ) holds A is independent proof let M be finite-degree Matroid; ::_thesis: for A being Subset of M st ( for B being Subset of M st B c= A holds not B is cycle ) holds A is independent let A be Subset of M; ::_thesis: ( ( for B being Subset of M st B c= A holds not B is cycle ) implies A is independent ) assume A1: for B being Subset of M st B c= A holds not B is cycle ; ::_thesis: A is independent consider C being independent Subset of M such that A2: C c= A and A3: card C = Rnk A by Th18; percases ( A c= C or A c/= C ) ; suppose A c= C ; ::_thesis: A is independent hence A is independent by A2, XBOOLE_0:def_10; ::_thesis: verum end; suppose A c/= C ; ::_thesis: A is independent then consider x being set such that A4: x in A and A5: x nin C by TARSKI:def_3; reconsider x = x as Element of M by A4; A6: C c= C \/ {x} by ZFMISC_1:137; defpred S1[ Nat] means ex B being independent Subset of M st ( card B = $1 & B c= C & B \/ {x} is dependent ); A7: C \/ {x} c= A by A2, A4, ZFMISC_1:137; A8: ex n being Nat st S1[n] proof take n = Rnk A; ::_thesis: S1[n] take C ; ::_thesis: ( card C = n & C c= C & C \/ {x} is dependent ) thus ( card C = n & C c= C ) by A3; ::_thesis: C \/ {x} is dependent assume A9: C \/ {x} is independent ; ::_thesis: contradiction C is_maximal_independent_in A by A2, A3, Th19; then C = C \/ {x} by A7, A6, A9, Def10; then {x} c= C by XBOOLE_1:7; hence contradiction by A5, ZFMISC_1:31; ::_thesis: verum end; consider n being Nat such that A10: ( S1[n] & ( for k being Nat st S1[k] holds n <= k ) ) from NAT_1:sch_5(A8); consider B being independent Subset of M such that A11: card B = n and A12: B c= C and A13: B \/ {x} is dependent by A10; A14: x nin B by A5, A12; A15: B \/ {x} is cycle proof thus B \/ {x} is dependent by A13; :: according to MATROID0:def_16 ::_thesis: for e being Element of M st e in B \/ {x} holds (B \/ {x}) \ {e} is independent let e be Element of M; ::_thesis: ( e in B \/ {x} implies (B \/ {x}) \ {e} is independent ) set Be = B \ {e}; A16: B \ {e} c= B by XBOOLE_1:36; assume A17: e in B \/ {x} ; ::_thesis: (B \/ {x}) \ {e} is independent percases ( e in B or e = x ) by A17, ZFMISC_1:136; supposeA18: e in B ; ::_thesis: (B \/ {x}) \ {e} is independent A19: e nin B \ {e} by ZFMISC_1:56; B = (B \ {e}) \/ {e} by A18, ZFMISC_1:116; then A20: n = (card (B \ {e})) + 1 by A11, A19, CARD_2:41; assume A21: (B \/ {x}) \ {e} is dependent ; ::_thesis: contradiction (B \/ {x}) \ {e} = (B \ {e}) \/ {x} by A14, A18, XBOOLE_1:87, ZFMISC_1:11; then n <= card (B \ {e}) by A10, A12, A16, A21, XBOOLE_1:1; hence contradiction by A20, NAT_1:13; ::_thesis: verum end; suppose e = x ; ::_thesis: (B \/ {x}) \ {e} is independent hence (B \/ {x}) \ {e} is independent by A14, ZFMISC_1:117; ::_thesis: verum end; end; end; B c= A by A2, A12, XBOOLE_1:1; then B \/ {x} c= A by A4, ZFMISC_1:137; hence A is independent by A1, A15; ::_thesis: verum end; end; end; theorem Th43: :: MATROID0:43 for M being finite-degree Matroid for A, B being Subset of M for e being Element of M st A is cycle & B is cycle & A <> B & e in A /\ B holds ex C being Subset of M st ( C is cycle & C c= (A \/ B) \ {e} ) proof let M be finite-degree Matroid; ::_thesis: for A, B being Subset of M for e being Element of M st A is cycle & B is cycle & A <> B & e in A /\ B holds ex C being Subset of M st ( C is cycle & C c= (A \/ B) \ {e} ) let A, B be Subset of M; ::_thesis: for e being Element of M st A is cycle & B is cycle & A <> B & e in A /\ B holds ex C being Subset of M st ( C is cycle & C c= (A \/ B) \ {e} ) let e be Element of M; ::_thesis: ( A is cycle & B is cycle & A <> B & e in A /\ B implies ex C being Subset of M st ( C is cycle & C c= (A \/ B) \ {e} ) ) assume that A1: A is cycle and A2: B is cycle and A3: A <> B and A4: e in A /\ B and A5: for C being Subset of M st C is cycle holds C c/= (A \/ B) \ {e} ; ::_thesis: contradiction A6: e in A by A4, XBOOLE_0:def_4; A /\ B c= B by XBOOLE_1:17; then A c/= A /\ B by A1, A2, A3, Th41, XBOOLE_1:1; then consider a being set such that A7: a in A and A8: a nin A /\ B by TARSKI:def_3; reconsider a = a as Element of M by A7; {a} misses A /\ B by A8, ZFMISC_1:50; then A9: A /\ B c= A \ {a} by XBOOLE_1:17, XBOOLE_1:86; reconsider A9 = A, B9 = B as finite Subset of M by A1, A2; (Rnk (A \/ B)) + (Rnk (A /\ B)) <= (Rnk A) + (Rnk B) by Th25; then A10: ((Rnk (A \/ B)) + (Rnk (A /\ B))) + 1 <= ((Rnk A) + (Rnk B)) + 1 by XREAL_1:6; A \ {a} is independent by A1, A7, Def16; then A /\ B is independent by A9, Th3; then A11: card (A9 /\ B9) = Rnk (A /\ B) by Th21; for C being Subset of M st C c= (A \/ B) \ {e} holds not C is cycle by A5; then reconsider C = (A \/ B) \ {e} as independent Subset of M by Th42; A12: e in {e} by TARSKI:def_1; then A13: e nin C by XBOOLE_0:def_5; A14: e in B by A4, XBOOLE_0:def_4; then reconsider Ae = A \ {e}, Be = B \ {e} as independent Subset of M by A1, A2, A6, Def16; A15: e nin Be by A12, XBOOLE_0:def_5; B = Be \/ {e} by A14, ZFMISC_1:116; then A16: card B9 = (card Be) + 1 by A15, CARD_2:41; then A17: (Rnk B) + 1 = (card Be) + 1 by A2, Th39; A18: e nin Ae by A12, XBOOLE_0:def_5; A = Ae \/ {e} by A6, ZFMISC_1:116; then A19: card A9 = (card Ae) + 1 by A18, CARD_2:41; then (Rnk A) + 1 = (card Ae) + 1 by A1, Th39; then (card (A9 \/ B9)) + (card (A9 /\ B9)) = ((Rnk A) + 1) + ((Rnk B) + 1) by A19, A16, A17, HALLMAR1:1 .= (((Rnk A) + (Rnk B)) + 1) + 1 ; then A20: (((Rnk (A \/ B)) + (Rnk (A /\ B))) + 1) + 1 <= (card (A9 \/ B9)) + (card (A9 /\ B9)) by A10, XREAL_1:6; e in A \/ B by A6, XBOOLE_0:def_3; then A21: C \/ {e} = A9 \/ B9 by ZFMISC_1:116; C is_maximal_independent_in A \/ B proof thus ( C is independent & C c= A \/ B ) by XBOOLE_1:36; :: according to MATROID0:def_10 ::_thesis: for B being Subset of M st B is independent & B c= A \/ B & C c= B holds C = B let D be Subset of M; ::_thesis: ( D is independent & D c= A \/ B & C c= D implies C = D ) A22: A c= A \/ B by XBOOLE_1:7; A is dependent by A1, Def16; then A \/ B is dependent by A22, Th3; hence ( D is independent & D c= A \/ B & C c= D implies C = D ) by A21, ZFMISC_1:138; ::_thesis: verum end; then (Rnk (A \/ B)) + 1 = (card C) + 1 by Th19 .= card (A9 \/ B9) by A13, A21, CARD_2:41 ; hence contradiction by A20, A11, NAT_1:13; ::_thesis: verum end; theorem :: MATROID0:44 for M being finite-degree Matroid for A, B, C being Subset of M for e being Element of M st A is independent & B is cycle & C is cycle & B c= A \/ {e} & C c= A \/ {e} holds B = C proof let M be finite-degree Matroid; ::_thesis: for A, B, C being Subset of M for e being Element of M st A is independent & B is cycle & C is cycle & B c= A \/ {e} & C c= A \/ {e} holds B = C let A, B, C be Subset of M; ::_thesis: for e being Element of M st A is independent & B is cycle & C is cycle & B c= A \/ {e} & C c= A \/ {e} holds B = C let e be Element of M; ::_thesis: ( A is independent & B is cycle & C is cycle & B c= A \/ {e} & C c= A \/ {e} implies B = C ) assume that A1: A is independent and A2: B is cycle and A3: C is cycle and A4: B c= A \/ {e} and A5: C c= A \/ {e} ; ::_thesis: B = C now__::_thesis:_not_C_c=_A assume C c= A ; ::_thesis: contradiction then C is independent by A1, Th3; hence contradiction by A3, Def16; ::_thesis: verum end; then consider c being set such that A6: c in C and A7: c nin A by TARSKI:def_3; c in {e} by A5, A6, A7, XBOOLE_0:def_3; then A8: c = e by TARSKI:def_1; now__::_thesis:_not_B_c=_A assume B c= A ; ::_thesis: contradiction then B is independent by A1, Th3; hence contradiction by A2, Def16; ::_thesis: verum end; then consider b being set such that A9: b in B and A10: b nin A by TARSKI:def_3; assume A11: B <> C ; ::_thesis: contradiction b in {e} by A4, A9, A10, XBOOLE_0:def_3; then b = e by TARSKI:def_1; then e in B /\ C by A9, A6, A8, XBOOLE_0:def_4; then consider D being Subset of M such that A12: D is cycle and A13: D c= (B \/ C) \ {e} by A2, A3, A11, Th43; D c= A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D or x in A ) assume A14: x in D ; ::_thesis: x in A then x in B \/ C by A13, XBOOLE_0:def_5; then A15: ( x in B or x in C ) by XBOOLE_0:def_3; x nin {e} by A13, A14, XBOOLE_0:def_5; hence x in A by A4, A5, A15, XBOOLE_0:def_3; ::_thesis: verum end; then D is independent by A1, Th3; hence contradiction by A12, Def16; ::_thesis: verum end;