let V be RealLinearSpace; for A, B being finite Subset of V st RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin A & B is linearly-independent holds
( card B <= card A & ex C being finite Subset of V st
( C c= A & card C = (card A) - (card B) & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin (B \/ C) ) )
defpred S1[ Nat] means for n being Element of NAT
for A, B being finite Subset of V st card A = n & card B = $1 & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin A & B is linearly-independent holds
( $1 <= n & ex C being finite Subset of V st
( C c= A & card C = n - $1 & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin (B \/ C) ) );
A1:
for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be
Nat;
( S1[m] implies S1[m + 1] )
assume A2:
S1[
m]
;
S1[m + 1]
let n be
Element of
NAT ;
for A, B being finite Subset of V st card A = n & card B = m + 1 & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin A & B is linearly-independent holds
( m + 1 <= n & ex C being finite Subset of V st
( C c= A & card C = n - (m + 1) & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin (B \/ C) ) )let A,
B be
finite Subset of
V;
( card A = n & card B = m + 1 & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin A & B is linearly-independent implies ( m + 1 <= n & ex C being finite Subset of V st
( C c= A & card C = n - (m + 1) & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin (B \/ C) ) ) )
assume that A3:
card A = n
and A4:
card B = m + 1
and A5:
RLSStruct(# the
carrier of
V, the
ZeroF of
V, the
U5 of
V, the
Mult of
V #)
= Lin A
and A6:
B is
linearly-independent
;
( m + 1 <= n & ex C being finite Subset of V st
( C c= A & card C = n - (m + 1) & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin (B \/ C) ) )
consider v being
object such that A7:
v in B
by A4, CARD_1:27, XBOOLE_0:def 1;
reconsider v =
v as
VECTOR of
V by A7;
set Bv =
B \ {v};
A8:
B \ {v} is
linearly-independent
by A6, RLVECT_3:5, XBOOLE_1:36;
{v} is
Subset of
B
by A7, SUBSET_1:41;
then A9:
card (B \ {v}) =
(card B) - (card {v})
by CARD_2:44
.=
(m + 1) - 1
by A4, CARD_1:30
.=
m
;
then consider C being
finite Subset of
V such that A10:
C c= A
and A11:
card C = n - m
and A12:
RLSStruct(# the
carrier of
V, the
ZeroF of
V, the
U5 of
V, the
Mult of
V #)
= Lin ((B \ {v}) \/ C)
by A2, A3, A5, A8;
A13:
not
v in Lin (B \ {v})
by A6, A7, Th17;
A14:
now not m = nassume
m = n
;
contradictionthen consider C being
finite Subset of
V such that
C c= A
and A15:
card C = m - m
and A16:
RLSStruct(# the
carrier of
V, the
ZeroF of
V, the
U5 of
V, the
Mult of
V #)
= Lin ((B \ {v}) \/ C)
by A2, A3, A5, A9, A8;
C = {}
by A15;
then
B \ {v} is
Basis of
V
by A8, A16, RLVECT_3:def 3;
hence
contradiction
by A13, Th13;
verum end;
v in Lin ((B \ {v}) \/ C)
by A12, STRUCT_0:def 5;
then consider w being
VECTOR of
V such that A17:
w in C
and A18:
w in Lin (((C \/ (B \ {v})) \ {w}) \/ {v})
by A13, Th21;
set Cw =
C \ {w};
((B \ {v}) \ {w}) \/ {v} c= (B \ {v}) \/ {v}
by XBOOLE_1:9, XBOOLE_1:36;
then
(C \ {w}) \/ (((B \ {v}) \ {w}) \/ {v}) c= (C \ {w}) \/ ((B \ {v}) \/ {v})
by XBOOLE_1:9;
then A19:
(C \ {w}) \/ (((B \ {v}) \ {w}) \/ {v}) c= B \/ (C \ {w})
by A7, Lm1;
{w} is
Subset of
C
by A17, SUBSET_1:41;
then A20:
card (C \ {w}) =
(card C) - (card {w})
by CARD_2:44
.=
(n - m) - 1
by A11, CARD_1:30
.=
n - (m + 1)
;
C \ {w} c= C
by XBOOLE_1:36;
then A21:
C \ {w} c= A
by A10;
((C \/ (B \ {v})) \ {w}) \/ {v} =
((C \ {w}) \/ ((B \ {v}) \ {w})) \/ {v}
by XBOOLE_1:42
.=
(C \ {w}) \/ (((B \ {v}) \ {w}) \/ {v})
by XBOOLE_1:4
;
then
Lin (((C \/ (B \ {v})) \ {w}) \/ {v}) is
Subspace of
Lin (B \/ (C \ {w}))
by A19, RLVECT_3:20;
then A22:
w in Lin (B \/ (C \ {w}))
by A18, RLSUB_1:8;
A23:
(
B \ {v} c= B &
C = (C \ {w}) \/ {w} )
by A17, Lm1, XBOOLE_1:36;
then
(B \ {v}) \/ C c= the
carrier of
(Lin (B \/ (C \ {w})))
;
then
Lin ((B \ {v}) \/ C) is
Subspace of
Lin (B \/ (C \ {w}))
by Th19;
then A24:
the
carrier of
(Lin ((B \ {v}) \/ C)) c= the
carrier of
(Lin (B \/ (C \ {w})))
by RLSUB_1:def 2;
the
carrier of
(Lin (B \/ (C \ {w}))) c= the
carrier of
V
by RLSUB_1:def 2;
then
the
carrier of
(Lin (B \/ (C \ {w}))) = the
carrier of
V
by A12, A24, XBOOLE_0:def 10;
then A25:
RLSStruct(# the
carrier of
V, the
ZeroF of
V, the
U5 of
V, the
Mult of
V #)
= Lin (B \/ (C \ {w}))
by A12, RLSUB_1:30;
m <= n
by A2, A3, A5, A9, A8;
then
m < n
by A14, XXREAL_0:1;
hence
(
m + 1
<= n & ex
C being
finite Subset of
V st
(
C c= A &
card C = n - (m + 1) &
RLSStruct(# the
carrier of
V, the
ZeroF of
V, the
U5 of
V, the
Mult of
V #)
= Lin (B \/ C) ) )
by A21, A20, A25, NAT_1:13;
verum
end;
A26:
S1[ 0 ]
proof
let n be
Element of
NAT ;
for A, B being finite Subset of V st card A = n & card B = 0 & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin A & B is linearly-independent holds
( 0 <= n & ex C being finite Subset of V st
( C c= A & card C = n - 0 & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin (B \/ C) ) )let A,
B be
finite Subset of
V;
( card A = n & card B = 0 & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin A & B is linearly-independent implies ( 0 <= n & ex C being finite Subset of V st
( C c= A & card C = n - 0 & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin (B \/ C) ) ) )
assume that A27:
card A = n
and A28:
card B = 0
and A29:
RLSStruct(# the
carrier of
V, the
ZeroF of
V, the
U5 of
V, the
Mult of
V #)
= Lin A
and
B is
linearly-independent
;
( 0 <= n & ex C being finite Subset of V st
( C c= A & card C = n - 0 & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin (B \/ C) ) )
B = {}
by A28;
then
A = B \/ A
;
hence
(
0 <= n & ex
C being
finite Subset of
V st
(
C c= A &
card C = n - 0 &
RLSStruct(# the
carrier of
V, the
ZeroF of
V, the
U5 of
V, the
Mult of
V #)
= Lin (B \/ C) ) )
by A27, A29;
verum
end;
A30:
for m being Nat holds S1[m]
from NAT_1:sch 2(A26, A1);
let A, B be finite Subset of V; ( RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin A & B is linearly-independent implies ( card B <= card A & ex C being finite Subset of V st
( C c= A & card C = (card A) - (card B) & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin (B \/ C) ) ) )
assume
( RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin A & B is linearly-independent )
; ( card B <= card A & ex C being finite Subset of V st
( C c= A & card C = (card A) - (card B) & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin (B \/ C) ) )
hence
( card B <= card A & ex C being finite Subset of V st
( C c= A & card C = (card A) - (card B) & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin (B \/ C) ) )
by A30; verum