let P be mutually-disjoint set ; for x being Subset of (ProdMatroid P)
for f being Function of x,P st ( for a being object st a in x holds
a in f . a ) holds
( x is independent iff f is one-to-one )
let x be Subset of (ProdMatroid P); for f being Function of x,P st ( for a being object st a in x holds
a in f . a ) holds
( x is independent iff f is one-to-one )
let f be Function of x,P; ( ( for a being object st a in x holds
a in f . a ) implies ( x is independent iff f is one-to-one ) )
assume A1:
for a being object st a in x holds
a in f . a
; ( x is independent iff f is one-to-one )
hereby ( f is one-to-one implies x is independent )
assume A2:
x is
independent
;
f is one-to-one thus
f is
one-to-one
verumproof
let a,
b be
object ;
FUNCT_1:def 4 ( not a in K49(f) or not b in K49(f) or not f . a = f . b or a = b )
assume that A3:
a in dom f
and A4:
b in dom f
;
( not f . a = f . b or a = b )
A5:
f . b in rng f
by A4, FUNCT_1:def 3;
f . a in rng f
by A3, FUNCT_1:def 3;
then reconsider D1 =
f . a,
D2 =
f . b as
Element of
P by A5;
a in D1
by A1, A3;
then A6:
a in x /\ D1
by A3, XBOOLE_0:def 4;
consider d2 being
Element of
D2 such that A7:
x /\ D2 c= {d2}
by A2, Th8;
b in D2
by A1, A4;
then
b in x /\ D2
by A4, XBOOLE_0:def 4;
then
b = d2
by A7, TARSKI:def 1;
hence
( not
f . a = f . b or
a = b )
by A7, A6, TARSKI:def 1;
verum
end;
end;
assume A8:
f is one-to-one
; x is independent
now for D being Element of P holds
not for d being Element of D holds x /\ D c/= {d}let D be
Element of
P;
not for d being Element of D holds x /\ D c/= {d}set d1 = the
Element of
D;
assume A9:
for
d being
Element of
D holds
x /\ D c/= {d}
;
contradictionthen
x /\ D c/= { the Element of D}
;
then consider d2 being
object such that A10:
d2 in x /\ D
and
d2 nin { the Element of D}
;
A11:
d2 in D
by A10, XBOOLE_0:def 4;
A12:
d2 in x
by A10, XBOOLE_0:def 4;
then
d2 in f . d2
by A1;
then A13:
f . d2 meets D
by A11, XBOOLE_0:3;
the
carrier of
(ProdMatroid P) = union P
by Def7;
then
ex
y being
set st
(
d2 in y &
y in P )
by A10, TARSKI:def 4;
then A14:
dom f = x
by FUNCT_2:def 1;
then
f . d2 in rng f
by A12, FUNCT_1:def 3;
then A15:
f . d2 = D
by A13, TAXONOM2:def 5;
x /\ D c= {d2}
proof
let a be
object ;
TARSKI:def 3 ( not a in x /\ D or a in {d2} )
assume A16:
a in x /\ D
;
a in {d2}
then A17:
a in x
by XBOOLE_0:def 4;
A18:
a in D
by A16, XBOOLE_0:def 4;
a in f . a
by A1, A17;
then A19:
f . a meets D
by A18, XBOOLE_0:3;
f . a in rng f
by A14, A17, FUNCT_1:def 3;
then
f . a = D
by A19, TAXONOM2:def 5;
then
a = d2
by A8, A12, A14, A15, A17;
hence
a in {d2}
by TARSKI:def 1;
verum
end; hence
contradiction
by A9, A11;
verum end;
hence
x is independent
by Th8; verum