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

A7: a in A and

A8: a nin A /\ B ;

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;

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;

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

.= card (A9 \/ B9) by A13, A21, CARD_2:41 ;

hence contradiction by A20, A11, NAT_1:13; :: thesis: verum

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

A7: a in A and

A8: a nin A /\ B ;

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;

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;

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

then (Rnk (A \/ B)) + 1 =
(card C) + 1
by Th19
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;

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

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

.= card (A9 \/ B9) by A13, A21, CARD_2:41 ;

hence contradiction by A20, A11, NAT_1:13; :: thesis: verum