set M = ProdMatroid P;
A1:
the_family_of (ProdMatroid P) = { A where A is Subset of (union P) : for D being set st D in P holds
ex d being set st A /\ D c= {d} }
by Def7;
let A, B be finite Subset of (ProdMatroid P); MATROID0:def 4 ( A in the_family_of (ProdMatroid P) & B in the_family_of (ProdMatroid P) & card B = (card A) + 1 implies ex e being Element of (ProdMatroid P) st
( e in B \ A & A \/ {e} in the_family_of (ProdMatroid P) ) )
assume that
A2:
A in the_family_of (ProdMatroid P)
and
A3:
B in the_family_of (ProdMatroid P)
; ( not card B = (card A) + 1 or ex e being Element of (ProdMatroid P) st
( e in B \ A & A \/ {e} in the_family_of (ProdMatroid P) ) )
consider f being Function of A,P such that
A4:
for a being object st a in A holds
a in f . a
by Th9;
assume
card B = (card A) + 1
; ex e being Element of (ProdMatroid P) st
( e in B \ A & A \/ {e} in the_family_of (ProdMatroid P) )
then A5:
card B > card A
by NAT_1:13;
consider g being Function of B,P such that
A6:
for a being object st a in B holds
a in g . a
by Th9;
A7:
the carrier of (ProdMatroid P) = union P
by Def7;
then
( P = {} implies A = {} )
by ZFMISC_1:2;
then A8:
dom f = A
by FUNCT_2:def 1;
reconsider A9 = rng f, B9 = rng g as finite set ;
A9:
A is independent
by A2;
then
f is one-to-one
by A4, Th10;
then
A,A9 are_equipotent
by A8, WELLORD2:def 4;
then A10:
card A = card A9
by CARD_1:5;
( P = {} implies B = {} )
by A7, ZFMISC_1:2;
then A11:
dom g = B
by FUNCT_2:def 1;
B is independent
by A3;
then
g is one-to-one
by A6, Th10;
then
B,B9 are_equipotent
by A11, WELLORD2:def 4;
then
card B = card B9
by CARD_1:5;
then consider a being set such that
A12:
a in B9 \ A9
by A10, A5, Th5;
consider x9 being object such that
A13:
x9 in B
and
A14:
a = g . x9
by A11, A12, FUNCT_1:def 3;
reconsider x = x9 as Element of (ProdMatroid P) by A13;
take
x
; ( x in B \ A & A \/ {x} in the_family_of (ProdMatroid P) )
A15:
a nin A9
by A12, XBOOLE_0:def 5;
now not x in AA16:
x in g . x
by A6, A13;
assume A17:
x in A
;
contradictionthen
x in f . x
by A4;
then A18:
f . x meets g . x
by A16, XBOOLE_0:3;
A19:
g . x in rng g
by A11, A13, FUNCT_1:def 3;
f . x in rng f
by A8, A17, FUNCT_1:def 3;
hence
contradiction
by A15, A14, A19, A18, TAXONOM2:def 5;
verum end;
hence
x in B \ A
by A13, XBOOLE_0:def 5; A \/ {x} in the_family_of (ProdMatroid P)
reconsider xx = {x} as Subset of (ProdMatroid P) by A13, ZFMISC_1:31;
reconsider Ax = A \/ xx as Subset of (union P) by Def7;
A20:
a in B9
by A12;
now for D being set st D in P holds
ex x9 being set st Ax /\ D c= {x9}let D be
set ;
( D in P implies ex x9 being set st Ax /\ x9 c= {b2} )A21:
Ax /\ D = (A /\ D) \/ (xx /\ D)
by XBOOLE_1:23;
assume A22:
D in P
;
ex x9 being set st Ax /\ x9 c= {b2}then consider d being
Element of
D such that A23:
A /\ D c= {d}
by A9, Th8;
per cases
( D = a or D <> a )
;
suppose A29:
D <> a
;
ex d being set st Ax /\ d c= {b2}
a in rng g
by A11, A13, A14, FUNCT_1:def 3;
then A30:
a misses D
by A22, A29, TAXONOM2:def 5;
x in a
by A6, A13, A14;
then
x nin D
by A30, XBOOLE_0:3;
then
xx c/= D
by ZFMISC_1:31;
then A31:
xx /\ D <> xx
by XBOOLE_1:17;
reconsider d =
d as
set ;
take d =
d;
Ax /\ D c= {d}
xx /\ D c= xx
by XBOOLE_1:17;
then
xx /\ D = {}
by A31, ZFMISC_1:33;
hence
Ax /\ D c= {d}
by A23, A21;
verum end; end; end;
hence
A \/ {x} in the_family_of (ProdMatroid P)
by A1; verum