let M be 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
let A, B be 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 e be Element of M; ( 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
; MATROID0:def 14 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;
B c= B \/ {e}
by XBOOLE_1:7;
then
Ca c= B \/ {e}
by A5;
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 not Rnk (B \/ {e}) = (Rnk B) + 1
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
;
contradictionthen
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;
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; MATROID0:def 14 verum