let M be 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} )
let A, B be 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 e be Element of M; ( 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}
; 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
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; verum