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;

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;

hence Rnk (Span A) = Rnk A by A2, A4, Th19; :: thesis: verum

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;

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

then
C = Ca
by A3;assume
C c/= Ca
; :: thesis: contradiction

then consider x being 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 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

.= 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; :: thesis: verum

end;then consider x being 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 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

.= 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; :: thesis: verum

hence Rnk (Span A) = Rnk A by A2, A4, Th19; :: thesis: verum