matroid0.miz



    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 A is independent for A is open;

      antonym A is dependent for A is open;

    end

    definition

      let M be SubsetFamilyStr;

      :: MATROID0:def1

      func the_family_of M -> Subset-Family of M equals the topology of M;

      coherence ;

    end

    definition

      let M be SubsetFamilyStr;

      let A be Subset of M;

      :: original: independent

      redefine

      :: MATROID0:def2

      attr A is independent means

      : Def2: A in ( the_family_of M);

      compatibility by PRE_TOPC:def 2;

    end

    definition

      let M be SubsetFamilyStr;

      :: MATROID0:def3

      attr M is subset-closed means

      : Def3: ( the_family_of M) is subset-closed;

      :: MATROID0:def4

      attr M is with_exchange_property means for A,B be 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 be Element of M st e in (B \ A) & (A \/ {e}) in ( the_family_of M);

    end

    registration

      cluster strict non empty non void finite subset-closed with_exchange_property for SubsetFamilyStr;

      existence

      proof

        reconsider S = ( bool { 0 }) as Subset-Family of { 0 };

        take M = TopStruct (# { 0 }, S #);

        thus M is strict;

        thus the carrier of M is non empty;

        thus the topology of M is non empty;

        thus the carrier of M is finite;

        thus ( the_family_of M) is subset-closed by COH_SP: 2;

        let A,B be finite Subset of M;

        assume A in ( the_family_of M);

        assume B in ( the_family_of M);

        assume

         A1: ( card B) = (( card A) + 1);

        reconsider e = 0 as Element of M by TARSKI:def 1;

        take e;

        

         A2: ( bool { 0 }) = { {} , { 0 }} by ZFMISC_1: 24;

        then

         A3: B = {} or B = { 0 } by TARSKI:def 2;

        

         A4: A = {} or A = { 0 } by A2, TARSKI:def 2;

        then ( card A) = 0 or ( card A) = 1 by CARD_1: 30;

        hence thesis by A1, A4, A3;

      end;

    end

    registration

      let M be non void SubsetFamilyStr;

      cluster independent for Subset of M;

      existence

      proof

        set a = the Element of the topology of M;

        reconsider a as Subset of M;

        take a;

        thus a in ( the_family_of M);

      end;

    end

    registration

      let M be subset-closed SubsetFamilyStr;

      cluster ( the_family_of M) -> subset-closed;

      coherence by Def3;

    end

    theorem :: MATROID0:1

    

     Th1: for M be non void subset-closed SubsetFamilyStr holds for A be independent Subset of M holds for B be set st B c= A holds B is independent Subset of M

    proof

      let M be non void subset-closed SubsetFamilyStr;

      let A be independent Subset of M;

      let B be set;

      assume

       A1: B c= A;

      A in ( the_family_of M) by Def2;

      then B in ( the_family_of M) by A1, CLASSES1:def 1;

      hence thesis by Def2;

    end;

    registration

      let M be non void subset-closed SubsetFamilyStr;

      cluster finite independent for Subset of M;

      existence

      proof

        set a = the Element of the topology of M;

        reconsider a as independent Subset of M by PRE_TOPC:def 2;

         {} c= a;

        then

        reconsider b = {} as independent Subset of M by Th1;

        take b;

        thus thesis;

      end;

    end

    definition

      mode Matroid is non empty non void subset-closed with_exchange_property SubsetFamilyStr;

    end

    theorem :: MATROID0:2

    

     Th2: for M be subset-closed SubsetFamilyStr holds M is non void iff {} in ( the_family_of M)

    proof

      let M be subset-closed SubsetFamilyStr;

      hereby

        assume M is non void;

        then

        reconsider M9 = M as non void subset-closed SubsetFamilyStr;

        set a = the independent Subset of M9;

         {} c= a;

        then {} is independent Subset of M9 by Th1;

        hence {} in ( the_family_of M) by Def2;

      end;

      assume {} in ( the_family_of M);

      hence the topology of M is non empty;

    end;

    registration

      let M be non void subset-closed SubsetFamilyStr;

      cluster empty -> independent for Subset of M;

      coherence by Th2;

    end

    theorem :: MATROID0:3

    

     Th3: for M be non void SubsetFamilyStr holds M is subset-closed iff for A,B be Subset of M st A is independent & B c= A holds B is independent

    proof

      let M be non void SubsetFamilyStr;

      thus M is subset-closed implies for A,B be Subset of M st A is independent & B c= A holds B is independent by Th1;

      assume

       A1: for A,B be Subset of M st A is independent & B c= A holds B is independent;

      let x,y be set;

      assume x in ( the_family_of M);

      then

       A2: x is independent Subset of M by Def2;

      assume y c= x;

      then y is independent Subset of M by A1, A2, XBOOLE_1: 1;

      hence thesis by Def2;

    end;

    registration

      let M be non void subset-closed SubsetFamilyStr;

      let A be independent Subset of M;

      let B be set;

      cluster (A /\ B) -> independent;

      coherence by Th3, XBOOLE_1: 17;

      cluster (B /\ A) -> independent;

      coherence ;

      cluster (A \ B) -> independent;

      coherence by Th3, XBOOLE_1: 36;

    end

    theorem :: MATROID0:4

    

     Th4: for M be non void non empty SubsetFamilyStr holds M is with_exchange_property iff for A,B be finite Subset of M st A is independent & B is independent & ( card B) = (( card A) + 1) holds ex e be Element of M st e in (B \ A) & (A \/ {e}) is independent

    proof

      let M be non void non empty SubsetFamilyStr;

      thus M is with_exchange_property implies for A,B be finite Subset of M st A is independent & B is independent & ( card B) = (( card A) + 1) holds ex e be Element of M st e in (B \ A) & (A \/ {e}) is independent

      proof

        assume

         A1: for A,B be 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 be Element of M st e in (B \ A) & (A \/ {e}) in ( the_family_of M);

        let A,B be finite Subset of M;

        assume that

         A2: A in ( the_family_of M) and

         A3: B in ( the_family_of M) and

         A4: ( card B) = (( card A) + 1);

        consider e be 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;

        thus e in (B \ A) & (A \/ {e}) in ( the_family_of M) by A5, A6;

      end;

      assume

       A7: for A,B be finite Subset of M st A is independent & B is independent & ( card B) = (( card A) + 1) holds ex e be Element of M st e in (B \ A) & (A \/ {e}) is independent;

      let A,B be finite Subset of M;

      assume that

       A8: A in ( the_family_of M) and

       A9: B in ( the_family_of M);

      

       A10: B is independent by A9;

      assume

       A11: ( card B) = (( card A) + 1);

      A is independent by A8;

      then

      consider e be Element of M such that

       A12: e in (B \ A) and

       A13: (A \/ {e}) is independent by A7, A10, A11;

      take e;

      thus thesis by A12, A13;

    end;

    definition

      ::$Canceled

      let M be SubsetFamilyStr;

      :: MATROID0:def6

      attr M is finite-membered means

      : Def5: ( the_family_of M) is finite-membered;

    end

    definition

      let M be SubsetFamilyStr;

      :: MATROID0:def7

      attr M is finite-degree means

      : Def6: M is finite-membered & ex n be Nat st for A be finite Subset of M st A is independent holds ( card A) <= n;

    end

    registration

      cluster finite-degree -> finite-membered for SubsetFamilyStr;

      coherence ;

      cluster finite -> finite-degree for SubsetFamilyStr;

      coherence

      proof

        let M be SubsetFamilyStr;

        assume the carrier of M is finite;

        then

        reconsider X = the carrier of M as finite set;

        thus M is finite-membered

        proof

          let x be set;

          assume x in ( the_family_of M);

          then x c= X;

          hence thesis;

        end;

        take ( card X);

        let A be finite Subset of M;

        thus thesis by NAT_1: 43;

      end;

    end

    begin

    registration

      cluster mutually-disjoint non empty with_non-empty_elements for set;

      existence

      proof

        take { { 0 }};

        thus thesis by TAXONOM2: 10;

      end;

    end

    theorem :: MATROID0:5

    

     Th5: for A,B be finite set st ( card A) < ( card B) holds ex x be set st x in (B \ A)

    proof

      let A,B be finite set;

      assume ( card A) < ( card B);

      then not B c= A by NAT_1: 43;

      then

      consider x be object such that

       A1: x in B and

       A2: x nin A;

      take x;

      thus thesis by A1, A2, XBOOLE_0:def 5;

    end;

    theorem :: MATROID0:6

    for P be mutually-disjoint with_non-empty_elements non empty set holds for f be Choice_Function of P holds f is one-to-one

    proof

      let P be mutually-disjoint with_non-empty_elements non empty set;

      let f be Choice_Function of P;

      let x1,x2 be object;

      assume that

       A1: x1 in ( dom f) and

       A2: x2 in ( dom f) and

       A3: (f . x1) = (f . x2);

      reconsider x1, x2 as set by TARSKI: 1;

      

       A4: not {} in P;

      then

       A5: (f . x1) in x1 by A1, ORDERS_1: 89;

      (f . x1) in x2 by A2, A3, A4, ORDERS_1: 89;

      then x1 meets x2 by A5, XBOOLE_0: 3;

      hence thesis by A1, A2, TAXONOM2:def 5;

    end;

    registration

      cluster -> non void subset-closed with_exchange_property for discrete SubsetFamilyStr;

      coherence

      proof

        let T be discrete SubsetFamilyStr;

        the topology of T is non empty by TDLAT_3:def 1;

        hence

         A1: T is non void;

        for A,B be 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;

        let A,B be finite Subset of T such that A in ( the_family_of T) and B in ( the_family_of T) and

         A2: ( card B) = (( card A) + 1);

        now

          assume B c= A;

          then ( Segm ( card B)) c= ( Segm ( 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;

        end;

        then

        consider x be object such that

         A3: x in B and

         A4: not x in A;

        reconsider 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;

        thus x in (B \ A) by A3, A4, XBOOLE_0:def 5;

        C is independent by TDLAT_3: 15;

        hence thesis;

      end;

    end

    theorem :: MATROID0:7

    for T be non empty discrete TopStruct holds T is Matroid;

    definition

      let P be set;

      :: MATROID0:def8

      func ProdMatroid P -> strict SubsetFamilyStr means

      : Def7: the carrier of it = ( union P) & ( the_family_of it ) = { A where A be Subset of ( union P) : for D be set st D in P holds ex d be set st (A /\ D) c= {d} };

      existence

      proof

        set F = { A where A be Subset of ( union P) : for D be set st D in P holds ex d be set st (A /\ D) c= {d} };

        set X = ( union P);

        F c= ( bool X)

        proof

          let x be object;

          assume x in F;

          then ex A be Subset of X st x = A & for D be set st D in P holds ex d be set st (A /\ D) c= {d};

          hence thesis;

        end;

        then

        reconsider F as Subset-Family of X;

        take TopStruct (# X, F #);

        thus thesis;

      end;

      uniqueness ;

    end

    registration

      let P be non empty with_non-empty_elements set;

      cluster ( ProdMatroid P) -> non empty;

      coherence

      proof

        set M = ( ProdMatroid P);

        the carrier of M = ( union P) by Def7;

        hence the carrier of M is non empty;

      end;

    end

    theorem :: MATROID0:8

    

     Th8: for P be set holds for A be Subset of ( ProdMatroid P) holds A is independent iff for D be Element of P holds ex d be Element of D st (A /\ D) c= {d}

    proof

      let P be set;

      set M = ( ProdMatroid P);

      

       A1: ( the_family_of M) = { A where A be Subset of ( union P) : for D be set st D in P holds ex d be set st (A /\ D) c= {d} } by Def7;

      let A be Subset of ( ProdMatroid P);

      

       A2: the carrier of M = ( union P) by Def7;

      thus A is independent implies for D be Element of P holds ex d be Element of D st (A /\ D) c= {d}

      proof

        assume A in ( the_family_of M);

        then

         A3: ex B be Subset of ( union P) st A = B & for D be set st D in P holds ex d be set st (B /\ D) c= {d} by A1;

        let D be Element of P;

        P = {} implies A = {} & ( {} /\ D) = {} by A2, ZFMISC_1: 2;

        then P = {} implies (A /\ D) c= {1};

        then

        consider d be set such that

         A4: (A /\ D) c= {d} by A3;

        set d0 = the Element of D;

        now

          assume d nin 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= {d0};

        end;

        hence thesis by A4;

      end;

      assume

       A5: for D be Element of P holds ex d be Element of D st (A /\ D) c= {d};

       A6:

      now

        let D be set;

        assume D in P;

        then ex d be Element of D st (A /\ D) c= {d} by A5;

        hence ex d be set st (A /\ D) c= {d};

      end;

      the carrier of M = ( union P) by Def7;

      hence A in ( the_family_of M) by A1, A6;

    end;

    registration

      let P be set;

      cluster ( ProdMatroid P) -> non void subset-closed;

      coherence

      proof

        set M = ( ProdMatroid P);

        

         A1: ( the_family_of M) = { A where A be Subset of ( union P) : for D be set st D in P holds ex d be set st (A /\ D) c= {d} } by Def7;

        set A = ( {} ( union P));

        now

          let D be set;

          assume D in P;

          take d = {} ;

          thus (A /\ D) c= {d};

        end;

        then A in ( the_family_of M) by A1;

        hence the topology of M is non empty;

        thus ( the_family_of M) is subset-closed

        proof

          let a,b be set;

          assume that

           A2: a in ( the_family_of M) and

           A3: b c= a;

          

           A4: ex B be Subset of ( union P) st a = B & for D be set st D in P holds ex d be set st (B /\ D) c= {d} by A1, A2;

           A5:

          now

            let D be set;

            assume D in P;

            then

            consider d be set such that

             A6: (a /\ D) c= {d} by A4;

            take d;

            (b /\ D) c= (a /\ D) by A3, XBOOLE_1: 26;

            hence (b /\ D) c= {d} by A6;

          end;

          b is Subset of ( union P) by A3, A4, XBOOLE_1: 1;

          hence thesis by A1, A5;

        end;

      end;

    end

    theorem :: MATROID0:9

    

     Th9: for P be mutually-disjoint set holds for x be Subset of ( ProdMatroid P) holds ex f be Function of x, P st for a be object st a in x holds a in (f . a)

    proof

      defpred P[ object, object] means ex D2 be set st D2 = $2 & $1 in D2;

      let P be mutually-disjoint set;

      let x be Subset of ( ProdMatroid P);

       A1:

      now

        let a be object;

        assume a in x;

        then a in the carrier of ( ProdMatroid P);

        then a in ( union P) by Def7;

        then ex y be set st a in y & y in P by TARSKI:def 4;

        hence ex y be object st y in P & P[a, y];

      end;

      consider f be Function of x, P such that

       A2: for a be object st a in x holds P[a, (f . a)] from FUNCT_2:sch 1( A1);

      take f;

      let a be object;

      assume a in x;

      then P[a, (f . a)] by A2;

      hence thesis;

    end;

    theorem :: MATROID0:10

    

     Th10: for P be mutually-disjoint set holds for x be Subset of ( ProdMatroid P) holds for f be Function of x, P st for a be object 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, x be Subset of ( ProdMatroid P);

      let f be Function of x, P;

      assume

       A1: for a be object st a in x holds a in (f . a);

      hereby

        assume

         A2: x is independent;

        thus f is one-to-one

        proof

          let a,b be object;

          assume that

           A3: a in ( dom f) and

           A4: b in ( dom f);

          

           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 be 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 thesis by A7, A6, TARSKI:def 1;

        end;

      end;

      assume

       A8: f is one-to-one;

      now

        let D be Element of P;

        set d1 = the Element of D;

        assume

         A9: for d be Element of D holds (x /\ D) c/= {d};

        then (x /\ D) c/= {d1};

        then

        consider d2 be object such that

         A10: d2 in (x /\ D) and d2 nin {d1};

        

         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 Def7;

        then ex y be 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 object;

          assume

           A16: a in (x /\ D);

          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;

          hence thesis by TARSKI:def 1;

        end;

        hence contradiction by A9, A11;

      end;

      hence thesis by Th8;

    end;

    registration

      let P be mutually-disjoint set;

      cluster ( ProdMatroid P) -> with_exchange_property;

      coherence

      proof

        set M = ( ProdMatroid P);

        

         A1: ( the_family_of M) = { A where A be Subset of ( union P) : for D be set st D in P holds ex d be set st (A /\ D) c= {d} } by Def7;

        let A,B be finite Subset of M;

        assume that

         A2: A in ( the_family_of M) and

         A3: B in ( the_family_of M);

        consider f be Function of A, P such that

         A4: for a be object st a in A holds a in (f . a) by Th9;

        assume ( card B) = (( card A) + 1);

        then

         A5: ( card B) > ( card A) by NAT_1: 13;

        consider g be Function of B, P such that

         A6: for a be object st a in B holds a in (g . a) by Th9;

        

         A7: the carrier of ( ProdMatroid P) = ( union P) by Def7;

        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;

        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;

        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 be set such that

         A12: a in (B9 \ A9) by A10, A5, Th5;

        consider x9 be object such that

         A13: x9 in B and

         A14: a = (g . x9) by A11, A12, FUNCT_1:def 3;

        reconsider x = x9 as Element of M by A13;

        take x;

        

         A15: a nin A9 by A12, XBOOLE_0:def 5;

        now

          

           A16: x in (g . x) by A6, A13;

          assume

           A17: x in A;

          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;

        end;

        hence x in (B \ A) by A13, XBOOLE_0:def 5;

        reconsider xx = {x} as Subset of M by A13, ZFMISC_1: 31;

        reconsider Ax = (A \/ xx) as Subset of ( union P) by Def7;

        

         A20: a in B9 by A12;

        now

          let D be set;

          

           A21: (Ax /\ D) = ((A /\ D) \/ (xx /\ D)) by XBOOLE_1: 23;

          assume

           A22: D in P;

          then

          consider d be Element of D such that

           A23: (A /\ D) c= {d} by A9, Th8;

          per cases ;

            suppose

             A24: D = a;

            reconsider x9 as set by TARSKI: 1;

            take x9;

            (A /\ D) c= {}

            proof

              let z be object;

              assume

               A25: z in (A /\ D);

              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 thesis by A20, A15, A24, A28, TAXONOM2:def 5;

            end;

            then (A /\ D) = {} ;

            hence (Ax /\ D) c= {x9} by A21, XBOOLE_1: 17;

          end;

            suppose

             A29: D <> a;

            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 as set;

            take 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;

          end;

        end;

        hence thesis by A1;

      end;

    end

    registration

      let X be finite set;

      let P be Subset of ( bool X);

      cluster ( ProdMatroid P) -> finite;

      coherence

      proof

        ( union P) is finite;

        hence the carrier of ( ProdMatroid P) is finite by Def7;

      end;

    end

    registration

      let X be set;

      cluster -> mutually-disjoint for a_partition of X;

      coherence

      proof

        let P be a_partition of X;

        let x,y be set;

        thus thesis by EQREL_1:def 4;

      end;

    end

    registration

      cluster finite strict for Matroid;

      existence

      proof

        set X = the finite non empty set, P = the a_partition of X;

        take ( ProdMatroid P);

        thus thesis;

      end;

    end

    registration

      let M be finite-membered non void SubsetFamilyStr;

      cluster -> finite for independent Subset of M;

      coherence

      proof

        let A be independent Subset of M;

        

         A1: ( the_family_of M) is finite-membered by Def5;

        A in ( the_family_of M) by Def2;

        hence thesis by A1;

      end;

    end

    definition

      let F be Field;

      let V be VectSp of F;

      :: MATROID0:def9

      func LinearlyIndependentSubsets V -> strict SubsetFamilyStr means

      : Def8: the carrier of it = the carrier of V & ( the_family_of it ) = { A where A be Subset of V : A is linearly-independent };

      existence

      proof

        set F = { A where A be Subset of V : A is linearly-independent };

        set X = the carrier of V;

        F c= ( bool X)

        proof

          let x be object;

          assume x in F;

          then ex A be Subset of X st x = A & A is linearly-independent;

          hence thesis;

        end;

        then

        reconsider F as Subset-Family of X;

        take TopStruct (# X, F #);

        thus thesis;

      end;

      uniqueness ;

    end

    registration

      let F be Field;

      let V be VectSp of F;

      cluster ( LinearlyIndependentSubsets V) -> non empty non void subset-closed;

      coherence

      proof

        set M = ( LinearlyIndependentSubsets V);

        

         A1: ( the_family_of M) = { A where A be Subset of V : A is linearly-independent } by Def8;

        the carrier of M = the carrier of V by Def8;

        hence the carrier of M is non empty;

        ( {} V) is linearly-independent;

        then {} in ( the_family_of M) by A1;

        hence the topology of M is non empty;

        let x,y be set;

        assume x in ( the_family_of M);

        then

         A2: ex A be Subset of V st x = A & A is linearly-independent by A1;

        assume

         A3: y c= x;

        then

        reconsider B = y as Subset of V by A2, XBOOLE_1: 1;

        B is linearly-independent by A2, A3, VECTSP_7: 1;

        hence thesis by A1;

      end;

    end

    theorem :: MATROID0:11

    

     Th11: for F be Field, V be VectSp of F holds for A be Subset of ( LinearlyIndependentSubsets V) holds A is independent iff A is linearly-independent Subset of V

    proof

      let F be Field;

      let V be VectSp of F;

      set M = ( LinearlyIndependentSubsets V);

      let B be Subset of M;

      ( the_family_of M) = { A where A be Subset of V : A is linearly-independent } by Def8;

      then B in ( the_family_of M) iff ex A be Subset of V st B = A & A is linearly-independent;

      hence thesis;

    end;

    theorem :: MATROID0:12

    for F be Field holds for V be VectSp of F holds for A,B be finite Subset of V st B c= A holds for v be Vector of V st v in ( Lin A) & not v in ( Lin B) holds ex w be Vector of V st w in (A \ B) & w in ( Lin ((A \ {w}) \/ {v}))

    proof

      let F be Field;

      let V be VectSp of F;

      let A,B be finite Subset of V;

      assume B c= A;

      then A = (B \/ (A \ B)) by XBOOLE_1: 45;

      hence thesis by VECTSP_9: 18;

    end;

    theorem :: MATROID0:13

    

     Th13: for F be Field, V be VectSp of F holds for A be Subset of V st A is linearly-independent holds for a be Element of V st a nin the carrier of ( Lin A) holds (A \/ {a}) is linearly-independent

    proof

      let F be Field;

      let V be VectSp of F;

      let A be Subset of V such that

       A1: A is linearly-independent;

      

       A2: the set of all ( Sum s) where s be Linear_Combination of A = the carrier of ( Lin A) by VECTSP_7:def 2;

      let a be Element of V;

      set B = (A \/ {a});

      assume that

       A3: a nin the carrier of ( Lin A) and

       A4: B is linearly-dependent;

      consider l be Linear_Combination of B 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 object;

        assume

         A8: x in A;

        then

        reconsider x as Element of V;

        x in ( Lin A) by A8, VECTSP_7: 8;

        hence thesis;

      end;

      then a nin A by A3;

      then (B \ 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

        assume (l . a) <> ( 0. F);

        

        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;

      end;

      then

       A11: a nin ( Carrier l) by VECTSP_6: 2;

      

       A12: ( Carrier l) c= B by VECTSP_6:def 4;

      ( Carrier l) c= A by A11, A12, ZFMISC_1: 136;

      then l is Linear_Combination of A by VECTSP_6:def 4;

      hence contradiction by A1, A5, A6, VECTSP_7:def 1;

    end;

    registration

      let F be Field;

      let V be VectSp of F;

      cluster ( LinearlyIndependentSubsets V) -> with_exchange_property;

      coherence

      proof

        set M = ( LinearlyIndependentSubsets V);

        

         A1: ( the_family_of M) = { A where A be Subset of V : A is linearly-independent } by Def8;

        let A,B be finite Subset of M such that

         A2: A in ( the_family_of M) and

         A3: B in ( the_family_of M) and

         A4: ( card B) = (( card A) + 1);

        

         A5: B is independent by A3;

        A is independent by A2;

        then

        reconsider A9 = A, B9 = B as linearly-independent finite Subset of V by A5, Th11;

        set V9 = ( Lin (A9 \/ B9));

        A9 c= the carrier of V9

        proof

          let a be object;

          assume a in A9;

          then a in (A9 \/ B9) by XBOOLE_0:def 3;

          then a in V9 by VECTSP_7: 8;

          hence thesis;

        end;

        then

        reconsider A99 = A9 as linearly-independent finite Subset of V9 by VECTSP_9: 12;

        B9 c= the carrier of V9

        proof

          let a be object;

          assume a in B9;

          then a in (A9 \/ B9) by XBOOLE_0:def 3;

          then a in V9 by VECTSP_7: 8;

          hence thesis;

        end;

        then

        reconsider B99 = B9 as linearly-independent finite Subset of V9 by VECTSP_9: 12;

        

         A6: V9 = ( Lin (A99 \/ B99)) by VECTSP_9: 17;

        then

        consider D be Basis of V9 such that

         A7: B9 c= D by VECTSP_7: 19;

        consider C be Basis of V9 such that

         A8: C c= (A99 \/ B99) by A6, VECTSP_7: 20;

        reconsider c = C as finite set by A8;

        c is Basis of V9;

        then V9 is finite-dimensional by MATRLIN:def 1;

        then ( card c) = ( card D) by VECTSP_9: 22;

        then ( Segm ( card B)) c= ( Segm ( 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

          assume C c= the carrier of ( Lin A9);

          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 be 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;

        end;

        then

        consider x be object such that

         A14: x in C and

         A15: x nin the carrier of ( Lin A9);

        

         A16: x in (C \ the carrier of ( Lin A9)) by A14, A15, XBOOLE_0:def 5;

        then

         A17: e nin the carrier of ( Lin A9) by XBOOLE_0:def 5;

        

         A18: e in C by A16, XBOOLE_0:def 5;

        then e in (A \/ B) by A8;

        then

        reconsider e as Element of M;

        take e;

        A c= the carrier of ( Lin A9)

        proof

          let x be object;

          assume x in A;

          then x in ( Lin A9) by VECTSP_7: 8;

          hence thesis;

        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;

        reconsider a = e as Element of V by A20;

        (A9 \/ {a}) is linearly-independent by A17, Th13;

        hence (A \/ {e}) in ( the_family_of M) by A1;

      end;

    end

    registration

      let F be Field;

      let V be finite-dimensional VectSp of F;

      cluster ( LinearlyIndependentSubsets V) -> finite-membered;

      coherence

      proof

        let A be set;

        set M = ( LinearlyIndependentSubsets V);

        assume A in ( the_family_of M);

        then A is independent Subset of M by Def2;

        then A is linearly-independent Subset of V by Th11;

        hence thesis by VECTSP_9: 21;

      end;

    end

    begin

    definition

      let M be SubsetFamilyStr;

      let A,C be Subset of M;

      :: MATROID0:def10

      pred A is_maximal_independent_in C means A is independent & A c= C & for B be Subset of M st B is independent & B c= C & A c= B holds A = B;

    end

    theorem :: MATROID0:14

    

     Th14: for M be non void finite-degree SubsetFamilyStr holds for C,A be Subset of M st A c= C & A is independent holds ex B be independent Subset of M st A c= B & B is_maximal_independent_in C

    proof

      let M be non void finite-degree SubsetFamilyStr;

      let C,A0 be Subset of M;

      assume that

       A1: A0 c= C and

       A2: A0 is independent;

      reconsider AA = A0 as independent Subset of M by A2;

      defpred P[ Nat] means for A be finite Subset of M st A0 c= A & A c= C & A is independent holds ( card A) <= $1;

      consider n be Nat such that

       A3: for A be finite Subset of M st A is independent holds ( card A) <= n by Def6;

      reconsider n as Element of NAT by ORDINAL1:def 12;

       P[n] by A3;

      then

       A4: ex n be Nat st P[n];

      consider n0 be Nat such that

       A5: P[n0] & for m be Nat st P[m] holds n0 <= m from NAT_1:sch 5( A4);

      now

         0 <= ( card AA) by NAT_1: 2;

        then

         A6: (( card AA) + 1) >= ( 0 + 1) by XREAL_1: 6;

        assume

         A7: for A be independent Subset of M st A0 c= A & A c= C holds ( card A) < n0;

        then ( card AA) < n0 by A1;

        then (( card AA) + 1) <= n0 by NAT_1: 13;

        then

        consider n be Nat such that

         A8: n0 = (1 + n) by A6, NAT_1: 10, XXREAL_0: 2;

        reconsider n as Element of NAT by ORDINAL1:def 12;

         P[n]

        proof

          let A be finite Subset of M;

          assume that

           A9: A0 c= A and

           A10: A c= C and

           A11: A is independent;

          ( card A) < (n + 1) by A7, A8, A9, A10, A11;

          hence thesis by NAT_1: 13;

        end;

        then (n + 1) <= n by A5, A8;

        hence contradiction by NAT_1: 13;

      end;

      then

      consider A be 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;

      thus A0 c= A & A is independent & A c= C by A12, A13;

      let B be Subset of M;

      assume that

       A16: B is independent and

       A17: B c= C and

       A18: A c= 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;

      then ( card B9) <= n0 by A5, A17;

      then ( card B9) = n0 by A19, XXREAL_0: 1;

      hence thesis by A14, A18, A15, CARD_2: 102, XXREAL_0: 1;

    end;

    theorem :: MATROID0:15

    for M be non void finite-degree subset-closed SubsetFamilyStr holds for C be Subset of M holds ex A be independent Subset of M st A is_maximal_independent_in C

    proof

      let M be non void finite-degree subset-closed SubsetFamilyStr;

      let C be Subset of M;

      ( {} M) c= C;

      then ex A be independent Subset of M st ( {} M) c= A & A is_maximal_independent_in C by Th14;

      hence thesis;

    end;

    theorem :: MATROID0:16

    

     Th16: for M be non empty non void subset-closed finite-degree SubsetFamilyStr holds M is Matroid iff for C be Subset of M, A,B be 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;

      hereby

        assume

         A1: M is Matroid;

        let C be Subset of M;

         A2:

        now

          let A,B be independent Subset of M such that

           A3: A is_maximal_independent_in C and

           A4: B is_maximal_independent_in C and

           A5: ( card A) < ( card B);

          

           A6: A c= C by A3;

          (( card A) + 1) <= ( card B) by A5, NAT_1: 13;

          then ( Segm (( card A) + 1)) c= ( Segm ( card B)) by NAT_1: 39;

          then

          consider D be set such that

           A7: D c= B and

           A8: ( card D) = (( card A) + 1) by CARD_FIL: 36;

          reconsider D as finite Subset of M by A7, XBOOLE_1: 1;

          D is independent by A7, Th3;

          then

          consider e be 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;

          B c= C by A4;

          then (D \ A) c= C by A11;

          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;

          then {e} c= A by XBOOLE_1: 7;

          then e in A by ZFMISC_1: 31;

          hence contradiction by A9, XBOOLE_0:def 5;

        end;

        let A,B be independent Subset of M such that

         A13: A is_maximal_independent_in C and

         A14: B is_maximal_independent_in C;

        ( 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;

      end;

      assume

       A15: for C be Subset of M, A,B be independent Subset of M st A is_maximal_independent_in C & B is_maximal_independent_in C holds ( card A) = ( card B);

      M is with_exchange_property

      proof

        let A,B be finite Subset 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);

        B is independent by A17;

        then

        consider B9 be 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 be Element of M st e in (B \ A) holds not (A \/ {e}) in ( the_family_of M);

        reconsider 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;

          thus A c= C by XBOOLE_1: 7;

          let D be Subset of M;

          assume that

           A23: D is independent and

           A24: D c= C and

           A25: A c= D;

          assume not (A c= D & D c= A);

          then

          consider e be object such that

           A26: e in D and

           A27: not e in A by A25;

          reconsider 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;

           {e} c= D by A26, ZFMISC_1: 31;

          then (A \/ {e}) c= D by A25, XBOOLE_1: 8;

          hence contradiction by A23, A28, Th3;

        end;

        then ( card A) = ( card B9) by A15, A20;

        hence contradiction by A18, A21, NAT_1: 13;

      end;

      hence thesis;

    end;

    definition

      let M be finite-degree Matroid;

      let C be Subset of M;

      :: MATROID0:def11

      func Rnk C -> Nat equals ( union { ( card A) where A be independent Subset of M : A c= C });

      coherence

      proof

        set X = { ( card A) where A be independent Subset of M : A c= C };

        defpred Q[ Nat] means ex A be independent Subset of M st A c= C & $1 = ( card A);

        defpred P[ Nat] means for A be independent Subset of M st A c= C holds ( card A) <= $1;

        consider n be Nat such that

         A1: for A be finite Subset of M st A is independent holds ( card A) <= n by Def6;

        

         A2: ex ne be Nat st P[ne]

        proof

          take n;

          thus thesis by A1;

        end;

        consider n0 be Nat such that

         A3: P[n0] & for m be Nat st P[m] holds n0 <= m from NAT_1:sch 5( A2);

        ( union X) = n0

        proof

          now

            let a be set;

            assume a in X;

            then

            consider A be independent Subset of M such that

             A4: a = ( card A) and

             A5: A c= C;

            ( card A) <= n0 by A3, A5;

            then ( Segm ( card A)) c= ( Segm n0) by NAT_1: 39;

            hence a c= ( Segm n0) by A4;

          end;

          hence ( union X) c= n0 by ZFMISC_1: 76;

          

           A6: ( {} M) c= C;

          

           A7: for k be Nat st Q[k] holds k <= n0 by A3;

          ( card {} ) = ( card {} );

          then

           A8: ex n be Nat st Q[n] by A6;

          consider n be Nat such that

           A9: Q[n] & for m be Nat st Q[m] holds m <= n from NAT_1:sch 6( A7, A8);

           P[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 X by A9;

          hence thesis by ZFMISC_1: 74;

        end;

        hence thesis;

      end;

    end

    theorem :: MATROID0:17

    

     Th17: for M be finite-degree Matroid holds for C be Subset of M holds for A be independent Subset of M st A c= C holds ( card A) <= ( Rnk C)

    proof

      let M be finite-degree Matroid;

      let C be Subset of M;

      let A be independent Subset of M;

      assume A c= C;

      then ( card A) in { ( card B) where B be independent Subset of M : B c= C };

      then ( Segm ( card A)) c= ( Segm ( Rnk C)) by ZFMISC_1: 74;

      hence thesis by NAT_1: 39;

    end;

    theorem :: MATROID0:18

    

     Th18: for M be finite-degree Matroid holds for C be Subset of M holds ex A be independent Subset of M st A c= C & ( card A) = ( Rnk C)

    proof

      let M be finite-degree Matroid;

      let C be Subset of M;

      defpred P[ Nat] means for A be independent Subset of M st A c= C holds ( card A) <= $1;

      defpred Q[ Nat] means ex A be independent Subset of M st A c= C & $1 = ( card A);

      set X = { ( card A) where A be independent Subset of M : A c= C };

      

       A1: ( {} M) c= C;

      ( card {} ) = ( card {} );

      then

       A2: ex n be Nat st Q[n] by A1;

      consider n be Nat such that

       A3: for A be finite Subset of M st A is independent holds ( card A) <= n by Def6;

      

       A4: ex ne be Nat st P[ne]

      proof

        take n;

        thus thesis by A3;

      end;

      consider n0 be Nat such that

       A5: P[n0] & for m be Nat st P[m] holds n0 <= m from NAT_1:sch 5( A4);

      now

        let a be set;

        assume a in X;

        then

        consider A be independent Subset of M such that

         A6: a = ( card A) and

         A7: A c= C;

        ( card A) <= n0 by A5, A7;

        then ( Segm ( card A)) c= ( Segm n0) by NAT_1: 39;

        hence a c= ( Segm n0) by A6;

      end;

      then

       A8: ( Rnk C) c= n0 by ZFMISC_1: 76;

      

       A9: for k be Nat st Q[k] holds k <= n0 by A5;

      consider n be Nat such that

       A10: Q[n] & for m be Nat st Q[m] holds m <= n from NAT_1:sch 6( A9, A2);

       P[n] by A10;

      then

       A11: n0 <= n by A5;

      consider A be independent Subset of M such that

       A12: A c= C and

       A13: n = ( card A) by A10;

      take A;

      n <= n0 by A5, A10;

      then

       A14: n = n0 by A11, XXREAL_0: 1;

      then n0 in X by A12, A13;

      then n0 c= ( Rnk C) by ZFMISC_1: 74;

      hence thesis by A8, A12, A13, A14;

    end;

    theorem :: MATROID0:19

    

     Th19: for M be finite-degree Matroid holds for C be Subset of M holds for A be 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;

      let C be Subset of M;

      set X = { ( card A) where A be independent Subset of M : A c= C };

      let A be independent Subset of M;

      consider B be independent Subset of M such that

       A1: B c= C and

       A2: ( card B) = ( Rnk C) by Th18;

       A3:

      now

        let A be independent Subset of M;

        assume that

         A4: A c= C and

         A5: ( card A) = ( Rnk C);

        thus A is_maximal_independent_in C

        proof

          thus A is independent & A c= C by A4;

          let B be Subset of M;

          assume B is independent;

          then

          reconsider B9 = B as independent Subset of M;

          assume B c= C;

          then ( card B9) in X;

          then

           A6: ( card B9) c= ( Rnk C) by ZFMISC_1: 74;

          assume

           A7: A c= B;

          then ( card A) c= ( card B9) by CARD_1: 11;

          then ( card A) = ( card B9) by A5, A6;

          hence thesis by A7, CARD_2: 102;

        end;

      end;

      hereby

        assume

         A8: A is_maximal_independent_in C;

        hence A c= C;

        B is_maximal_independent_in C by A3, A1, A2;

        hence ( card A) = ( Rnk C) by A2, A8, Th16;

      end;

      thus thesis by A3;

    end;

    theorem :: MATROID0:20

    

     Th20: for M be finite-degree Matroid holds for C be finite Subset of M holds ( Rnk C) <= ( card C)

    proof

      let M be finite-degree Matroid;

      let C be finite Subset of M;

      ex A be independent Subset of M st A c= C & ( card A) = ( Rnk C) by Th18;

      then ( Segm ( Rnk C)) c= ( Segm ( card C)) by CARD_1: 11;

      hence thesis by NAT_1: 39;

    end;

    theorem :: MATROID0:21

    

     Th21: for M be finite-degree Matroid holds for C be finite Subset of M holds C is independent iff ( card C) = ( Rnk C)

    proof

      let M be finite-degree Matroid;

      let C be finite Subset of M;

      set X = { ( card A) where A be independent Subset of M : A c= C };

      hereby

        assume C is independent;

        then ( card C) in X;

        then ( Segm ( card C)) c= ( Segm ( 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;

      end;

      ex A be independent Subset of M st A c= C & ( card A) = ( Rnk C) by Th18;

      hence thesis by CARD_2: 102;

    end;

    definition

      let M be finite-degree Matroid;

      :: MATROID0:def12

      func Rnk M -> Nat equals ( Rnk ( [#] M));

      coherence ;

    end

    definition

      let M be non void finite-degree SubsetFamilyStr;

      :: MATROID0:def13

      mode Basis of M -> independent Subset of M means

      : Def12: it is_maximal_independent_in ( [#] M);

      existence

      proof

        set A = the independent Subset of M;

        set C = ( [#] M);

        consider B be independent Subset of M such that A c= B and

         A1: B is_maximal_independent_in C by Th14;

        take B;

        thus thesis by A1;

      end;

    end

    theorem :: MATROID0:22

    for M be finite-degree Matroid holds for B1,B2 be Basis of M holds ( card B1) = ( card B2)

    proof

      let M be finite-degree Matroid;

      let B1,B2 be Basis of M;

      

       A1: B2 is_maximal_independent_in ( [#] M) by Def12;

      B1 is_maximal_independent_in ( [#] M) by Def12;

      hence thesis by A1, Th16;

    end;

    theorem :: MATROID0:23

    for M be finite-degree Matroid holds for A be independent Subset of M holds ex B be Basis of M st A c= B

    proof

      let M be finite-degree Matroid;

      let A be independent Subset of M;

      consider B be independent Subset of M such that

       A1: A c= B and

       A2: B is_maximal_independent_in ( [#] M) by Th14;

      reconsider B as Basis of M by A2, Def12;

      take B;

      thus thesis by A1;

    end;

    reserve M for finite-degree Matroid,

A,B,C for Subset of M,

e,f for Element of M;

    theorem :: MATROID0:24

    

     Th24: A c= B implies ( Rnk A) <= ( Rnk B)

    proof

      ex C be independent Subset of M st C c= A & ( card C) = ( Rnk A) by Th18;

      hence thesis by Th17, XBOOLE_1: 1;

    end;

    theorem :: MATROID0:25

    

     Th25: (( Rnk (A \/ B)) + ( Rnk (A /\ B))) <= (( Rnk A) + ( Rnk B))

    proof

      consider C be 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;

      then

      consider Ca be 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;

      

       A6: (Ca /\ B) c= C

      proof

        let x be object;

        assume

         A7: x in (Ca /\ B);

        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;

        then {x} c= C by XBOOLE_1: 7;

        hence thesis by ZFMISC_1: 31;

      end;

      (A /\ B) c= B by XBOOLE_1: 17;

      then C c= B by A1;

      then C c= (Ca /\ B) by A3, XBOOLE_1: 19;

      then

       A11: (Ca /\ B) = C by A6;

      A c= (A \/ B) by XBOOLE_1: 7;

      then Ca c= (A \/ B) by A5;

      then

      consider C9 be 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;

      

       A16: C9 = (Ca \/ (C9 /\ B))

      proof

        thus C9 c= (Ca \/ (C9 /\ B))

        proof

          let x be object;

          assume

           A17: x in C9;

          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

            assume x in A;

            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;

            then {x} c= Ca by XBOOLE_1: 7;

            hence x in Ca by ZFMISC_1: 31;

          end;

          x in B implies x in (C9 /\ B) by A17, XBOOLE_0:def 4;

          hence thesis by A15, A17, A18, XBOOLE_0:def 3;

        end;

        let x be object;

        assume x in (Ca \/ (C9 /\ B));

        then x in Ca or x in (C9 /\ B) by XBOOLE_0:def 3;

        hence thesis by A12, XBOOLE_0:def 4;

      end;

      (C9 /\ B) c= B by XBOOLE_1: 17;

      then

      consider Cb be 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 thesis by A22, XREAL_1: 6;

    end;

    theorem :: MATROID0:26

    

     Th26: ( Rnk A) <= ( Rnk (A \/ B)) & ( Rnk (A \/ {e})) <= (( Rnk A) + 1)

    proof

      

       A1: ( card {e}) = 1 by CARD_1: 30;

      thus ( Rnk A) <= ( Rnk (A \/ B)) by Th24, XBOOLE_1: 7;

      

       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 thesis by A3, XXREAL_0: 2;

    end;

    theorem :: MATROID0:27

    ( Rnk (A \/ {e})) = ( Rnk (A \/ {f})) & ( Rnk (A \/ {f})) = ( Rnk A) implies ( Rnk (A \/ {e, f})) = ( Rnk A)

    proof

      assume that

       A1: ( Rnk (A \/ {e})) = ( Rnk (A \/ {f})) and

       A2: ( Rnk (A \/ {f})) = ( Rnk A);

      consider C be 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;

      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;

      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;

      then

      consider C9 be 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;

      now

        assume C9 <> C;

        then

        consider x be object such that

         A11: not (x in C9 iff x in C) by TARSKI: 2;

         {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

          assume x in A;

          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;

          then {x} c= C by XBOOLE_1: 7;

          hence contradiction by A8, A11, ZFMISC_1: 31;

        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;

        then {x} c= C by XBOOLE_1: 7;

        hence contradiction by A8, A11, ZFMISC_1: 31;

      end;

      hence thesis by A4, A9, Th19;

    end;

    begin

    definition

      let M be finite-degree Matroid;

      let e be Element of M;

      let A be Subset of M;

      :: MATROID0:def14

      pred e is_dependent_on A means ( Rnk (A \/ {e})) = ( Rnk A);

    end

    theorem :: MATROID0:28

    

     Th28: e in A implies e is_dependent_on A by ZFMISC_1: 31, XBOOLE_1: 12;

    theorem :: MATROID0:29

    

     Th29: A c= B & e is_dependent_on A implies e is_dependent_on B

    proof

      assume that

       A1: A c= B and

       A2: ( Rnk (A \/ {e})) = ( Rnk A);

      consider Ca be 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;

      B c= (B \/ {e}) by XBOOLE_1: 7;

      then Ca c= (B \/ {e}) by A5;

      then

      consider E be independent Subset of M such that

       A6: Ca c= E and

       A7: E is_maximal_independent_in (B \/ {e}) by Th14;

       A8:

      now

        E c= (B \/ {e}) by A7;

        

        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);

        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;

        then {e} c= Ca by XBOOLE_1: 7;

        then B = (B \/ {e}) by A5, XBOOLE_1: 1, XBOOLE_1: 12;

        hence contradiction by A14;

      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;

    end;

    definition

      let M be finite-degree Matroid;

      let A be Subset of M;

      :: MATROID0:def15

      func Span A -> Subset of M equals { e where e be Element of M : e is_dependent_on A };

      coherence

      proof

        set X = { e where e be Element of M : e is_dependent_on A };

        X c= the carrier of M

        proof

          let x be object;

          assume x in X;

          then ex e be Element of M st x = e & e is_dependent_on A;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: MATROID0:30

    

     Th30: e in ( Span A) iff ( Rnk (A \/ {e})) = ( Rnk A)

    proof

      hereby

        assume e in ( Span A);

        then ex x be Element of M st e = x & x is_dependent_on A;

        hence ( Rnk (A \/ {e})) = ( Rnk A);

      end;

      assume ( Rnk (A \/ {e})) = ( Rnk A);

      then e is_dependent_on A;

      hence thesis;

    end;

    theorem :: MATROID0:31

    

     Th31: A c= ( Span A)

    proof

      let e be object;

      assume

       A1: e in A;

      then

      reconsider x = e as Element of M;

      x is_dependent_on A by A1, Th28;

      hence thesis;

    end;

    theorem :: MATROID0:32

    A c= B implies ( Span A) c= ( Span B)

    proof

      assume

       A1: A c= B;

      let x be object;

      assume x in ( Span A);

      then ex e st x = e & e is_dependent_on A;

      then ex e st x = e & e is_dependent_on B by A1, Th29;

      hence thesis;

    end;

    theorem :: MATROID0:33

    

     Th33: ( Rnk ( Span A)) = ( Rnk A)

    proof

      consider Ca be 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;

      then

      consider C be independent Subset of M such that

       A3: Ca c= C and

       A4: C is_maximal_independent_in ( Span A) by Th14;

      now

        assume C c/= Ca;

        then

        consider x be object such that

         A5: x in C and

         A6: x nin Ca;

        C c= ( Span A) by A4;

        then x in ( Span A) by A5;

        then

        consider e be 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 be 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

        .= ( 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_2: 102, XBOOLE_1: 7;

        then e nin {e} by A6, A7, XBOOLE_0:def 3;

        hence contradiction by TARSKI:def 1;

      end;

      then C = Ca by A3;

      hence thesis by A2, A4, Th19;

    end;

    theorem :: MATROID0:34

    

     Th34: e is_dependent_on ( Span A) implies e is_dependent_on A

    proof

      assume

       A1: ( Rnk (( Span A) \/ {e})) = ( Rnk ( Span A));

      

       A2: ( Rnk A) = ( Rnk ( Span A)) by Th33;

      consider Ca be 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;

    end;

    theorem :: MATROID0:35

    ( Span ( Span A)) = ( Span A)

    proof

      thus ( Span ( Span A)) c= ( Span A)

      proof

        let x be object;

        assume x in ( Span ( Span A));

        then

        consider e be 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 thesis by A1;

      end;

      thus thesis by Th31;

    end;

    theorem :: MATROID0:36

    f nin ( Span A) & f in ( Span (A \/ {e})) implies e in ( Span (A \/ {f}))

    proof

      assume that

       A1: f nin ( Span A) and

       A2: f in ( Span (A \/ {e}));

      

       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 thesis by Th30;

    end;

    definition

      let M be SubsetFamilyStr;

      let A be Subset of M;

      :: MATROID0:def16

      attr A is cycle means A is dependent & for e be Element of M st e in A holds (A \ {e}) is independent;

    end

    theorem :: MATROID0:37

    

     Th37: A is cycle implies A is non empty finite

    proof

      assume that

       A1: A is dependent and

       A2: for e be Element of M st e in A holds (A \ {e}) is independent;

      thus A is non empty by A1;

      set e = the Element of A;

      now

        assume

         A3: A is non empty set;

        then e in A;

        then

        reconsider e 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 thesis;

      end;

      hence thesis;

    end;

    registration

      let M;

      cluster cycle -> non empty finite for Subset of M;

      coherence by Th37;

    end

    theorem :: MATROID0:38

    

     Th38: A is cycle iff A is non empty & for e st e in A holds (A \ {e}) is_maximal_independent_in A

    proof

      thus A is cycle implies A is non empty & for e st e in A holds (A \ {e}) is_maximal_independent_in A

      proof

        assume that

         A1: A is dependent and

         A2: for e be Element of M st e in A holds (A \ {e}) is independent;

        thus A is non empty by A1;

        let e;

        set Ae = (A \ {e});

        assume

         A3: e in A;

        hence Ae is independent & Ae c= A by A2, XBOOLE_1: 36;

        let B;

        assume that

         A4: B is independent and

         A5: B c= A and

         A6: Ae c= B;

        A = (Ae \/ {e}) by A3, ZFMISC_1: 116;

        hence thesis by A1, A4, A5, A6, ZFMISC_1: 138;

      end;

      set a = the Element of A;

      assume that

       A7: A is non empty and

       A8: for e st e in A holds (A \ {e}) is_maximal_independent_in A;

      a in A by A7;

      then

      reconsider a as Element of M;

      set Ae = (A \ {a});

      

       A9: Ae is_maximal_independent_in A by A7, A8;

      hereby

        assume A is independent;

        then A = Ae by A9;

        then a nin {a} by A7, XBOOLE_0:def 5;

        hence contradiction by TARSKI:def 1;

      end;

      let e;

      assume e in A;

      then (A \ {e}) is_maximal_independent_in A by A8;

      hence thesis;

    end;

    theorem :: MATROID0:39

    

     Th39: A is cycle implies (( Rnk A) + 1) = ( card A)

    proof

      assume

       A1: A is cycle;

      then

      reconsider A as non empty finite Subset of M;

      set a = the Element of A;

      

       A2: (A \ {a}) is_maximal_independent_in A by A1, Th38;

      

       A3: ( Rnk A) = ( card (A \ {a})) by A2, Th19;

      a in {a} by TARSKI:def 1;

      then

       A4: a nin (A \ {a}) by XBOOLE_0:def 5;

      A = ((A \ {a}) \/ {a}) by ZFMISC_1: 116;

      hence thesis by A3, A4, CARD_2: 41;

    end;

    theorem :: MATROID0:40

    A is cycle & e in A implies e is_dependent_on (A \ {e})

    proof

      assume that

       A1: A is cycle and

       A2: e in A;

      reconsider Ae = (A \ {e}) as independent Subset of M by A1, A2;

      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;

    end;

    theorem :: MATROID0:41

    

     Th41: A is cycle & B is cycle & A c= B implies A = B

    proof

      assume that

       A1: A is dependent and for e st e in A holds (A \ {e}) is independent and B is dependent and

       A2: for e st e in B holds (B \ {e}) is independent;

      assume that

       A3: A c= B and

       A4: A <> B;

      consider x be object such that

       A5: not (x in A iff x in B) by A4, TARSKI: 2;

      reconsider 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;

    end;

    theorem :: MATROID0:42

    

     Th42: (for B st B c= A holds not B is cycle) implies A is independent

    proof

      assume

       A1: for B st B c= A holds not B is cycle;

      consider C be independent Subset of M such that

       A2: C c= A and

       A3: ( card C) = ( Rnk A) by Th18;

      per cases ;

        suppose A c= C;

        hence thesis by A2, XBOOLE_0:def 10;

      end;

        suppose A c/= C;

        then

        consider x be object such that

         A4: x in A and

         A5: x nin C;

        reconsider x as Element of M by A4;

        

         A6: C c= (C \/ {x}) by ZFMISC_1: 137;

        defpred P[ Nat] means ex B be 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 be Nat st P[n]

        proof

          take n = ( Rnk A), C;

          thus ( card C) = n & C c= C by A3;

          assume

           A9: (C \/ {x}) is independent;

          C is_maximal_independent_in A by A2, A3, Th19;

          then C = (C \/ {x}) by A7, A6, A9;

          then {x} c= C by XBOOLE_1: 7;

          hence contradiction by A5, ZFMISC_1: 31;

        end;

        consider n be Nat such that

         A10: P[n] & for k be Nat st P[k] holds n <= k from NAT_1:sch 5( A8);

        consider B be 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;

          let e be Element of M;

          set Be = (B \ {e});

          

           A16: Be c= B by XBOOLE_1: 36;

          assume

           A17: e in (B \/ {x});

          per cases by A17, ZFMISC_1: 136;

            suppose

             A18: e in B;

            

             A19: e nin Be by ZFMISC_1: 56;

            B = (Be \/ {e}) by A18, ZFMISC_1: 116;

            then

             A20: n = (( card Be) + 1) by A11, A19, CARD_2: 41;

            assume

             A21: ((B \/ {x}) \ {e}) is dependent;

            ((B \/ {x}) \ {e}) = (Be \/ {x}) by A14, A18, XBOOLE_1: 87, ZFMISC_1: 11;

            then n <= ( card Be) by A10, A12, A16, A21, XBOOLE_1: 1;

            hence contradiction by A20, NAT_1: 13;

          end;

            suppose e = x;

            hence ((B \/ {x}) \ {e}) is independent by A14, ZFMISC_1: 117;

          end;

        end;

        B c= A by A2, A12;

        then (B \/ {x}) c= A by A4, ZFMISC_1: 137;

        hence thesis by A1, A15;

      end;

    end;

    theorem :: MATROID0:43

    

     Th43: A is cycle & B is cycle & A <> B & e in (A /\ B) implies ex C st C is cycle & C c= ((A \/ B) \ {e})

    proof

      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 st C is cycle holds C c/= ((A \/ B) \ {e});

      

       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 be object such that

       A7: a in A and

       A8: a nin (A /\ B);

      reconsider 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;

      then (A /\ B) is independent by A9, Th3;

      then

       A11: ( card (A9 /\ B9)) = ( Rnk (A /\ B)) by Th21;

      for C 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;

      

       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;

        let D be Subset of M;

        

         A22: A c= (A \/ B) by XBOOLE_1: 7;

        A is dependent by A1;

        then (A \/ B) is dependent by A22, Th3;

        hence thesis by A21, ZFMISC_1: 138;

      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;

    end;

    theorem :: MATROID0:44

    A is independent & B is cycle & C is cycle & B c= (A \/ {e}) & C c= (A \/ {e}) implies B = C

    proof

      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});

       not C c= A by A1, Th3, A3;

      then

      consider c be object such that

       A6: c in C and

       A7: c nin A;

      c in {e} by A5, A6, A7, XBOOLE_0:def 3;

      then

       A8: c = e by TARSKI:def 1;

       not B c= A by A1, Th3, A2;

      then

      consider b be object such that

       A9: b in B and

       A10: b nin A;

      assume

       A11: B <> C;

      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 be 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 object;

        assume

         A14: x in D;

        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 thesis by A4, A5, A15, XBOOLE_0:def 3;

      end;

      then D is independent by A1, Th3;

      hence thesis by A12;

    end;