let M be finite-degree Matroid; :: thesis: for A, B being Subset of M holds (Rnk (A \/ B)) + (Rnk (A /\ B)) <= (Rnk A) + (Rnk B)

let A, B be Subset of M; :: thesis: (Rnk (A \/ B)) + (Rnk (A /\ B)) <= (Rnk A) + (Rnk B)

consider C being 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 being 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

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

then consider Cb being 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 (Rnk (A \/ B)) + (Rnk (A /\ B)) <= (Rnk A) + (Rnk B) by A22, XREAL_1:6; :: thesis: verum

let A, B be Subset of M; :: thesis: (Rnk (A \/ B)) + (Rnk (A /\ B)) <= (Rnk A) + (Rnk B)

consider C being 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 being 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

A /\ B c= B
by XBOOLE_1:17;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Ca /\ B or x in C )

assume A7: x in Ca /\ B ; :: thesis: x in C

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 x in C by ZFMISC_1:31; :: thesis: verum

end;assume A7: x in Ca /\ B ; :: thesis: x in C

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 x in C by ZFMISC_1:31; :: thesis: verum

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

C9 /\ B c= B
by XBOOLE_1:17;
thus
C9 c= Ca \/ (C9 /\ B)
:: according to XBOOLE_0:def 10 :: thesis: not Ca \/ (C9 /\ B) c/= C9

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

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

hence x in C9 by A12, XBOOLE_0:def 4; :: thesis: verum

end;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Ca \/ (C9 /\ B) or x in C9 )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in C9 or x in Ca \/ (C9 /\ B) )

assume A17: x in C9 ; :: thesis: x in Ca \/ (C9 /\ B)

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;

hence x in Ca \/ (C9 /\ B) by A15, A17, A18, XBOOLE_0:def 3; :: thesis: verum

end;assume A17: x in C9 ; :: thesis: x in Ca \/ (C9 /\ B)

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 :: thesis: ( x in A implies x in Ca )

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

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

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

hence x in Ca \/ (C9 /\ B) by A15, A17, A18, XBOOLE_0:def 3; :: thesis: verum

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

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

hence x in C9 by A12, XBOOLE_0:def 4; :: thesis: verum

then consider Cb being 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 (Rnk (A \/ B)) + (Rnk (A /\ B)) <= (Rnk A) + (Rnk B) by A22, XREAL_1:6; :: thesis: verum