let V be RealUnitarySpace; :: thesis: for A, B being finite Subset of V st UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar 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) & UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar of V #) = Lin (B \/ C) ) )
let A, B be finite Subset of V; :: thesis: ( UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar 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) & UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar of V #) = Lin (B \/ C) ) ) )
assume that
A1:
UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar of V #) = Lin A
and
A2:
B is linearly-independent
; :: thesis: ( card B <= card A & ex C being finite Subset of V st
( C c= A & card C = (card A) - (card B) & UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar of V #) = Lin (B \/ C) ) )
defpred S1[ Element of NAT ] means for n being Element of NAT
for A, B being finite Subset of V st card A = n & card B = $1 & UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar 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 & UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar of V #) = Lin (B \/ C) ) );
A3:
S1[ 0 ]
proof
let n be
Element of
NAT ;
:: thesis: for A, B being finite Subset of V st card A = n & card B = 0 & UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar 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 & UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar of V #) = Lin (B \/ C) ) )let A,
B be
finite Subset of
V;
:: thesis: ( card A = n & card B = 0 & UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar 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 & UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar of V #) = Lin (B \/ C) ) ) )
assume A4:
(
card A = n &
card B = 0 &
UNITSTR(# the
carrier of
V,the
U2 of
V,the
addF of
V,the
Mult of
V,the
scalar of
V #)
= Lin A &
B is
linearly-independent )
;
:: thesis: ( 0 <= n & ex C being finite Subset of V st
( C c= A & card C = n - 0 & UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar of V #) = Lin (B \/ C) ) )
B = {}
by A4;
then
A = B \/ A
;
hence
(
0 <= n & ex
C being
finite Subset of
V st
(
C c= A &
card C = n - 0 &
UNITSTR(# the
carrier of
V,the
U2 of
V,the
addF of
V,the
Mult of
V,the
scalar of
V #)
= Lin (B \/ C) ) )
by A4, NAT_1:2;
:: thesis: verum
end;
A5:
for m being Element of NAT st S1[m] holds
S1[m + 1]
proof
let m be
Element of
NAT ;
:: thesis: ( S1[m] implies S1[m + 1] )
assume A6:
S1[
m]
;
:: thesis: S1[m + 1]
let n be
Element of
NAT ;
:: thesis: for A, B being finite Subset of V st card A = n & card B = m + 1 & UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar 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) & UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar of V #) = Lin (B \/ C) ) )let A,
B be
finite Subset of
V;
:: thesis: ( card A = n & card B = m + 1 & UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar 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) & UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar of V #) = Lin (B \/ C) ) ) )
assume that A7:
card A = n
and A8:
card B = m + 1
and A9:
UNITSTR(# the
carrier of
V,the
U2 of
V,the
addF of
V,the
Mult of
V,the
scalar of
V #)
= Lin A
and A10:
B is
linearly-independent
;
:: thesis: ( m + 1 <= n & ex C being finite Subset of V st
( C c= A & card C = n - (m + 1) & UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar of V #) = Lin (B \/ C) ) )
consider v being
set such that A11:
v in B
by A8, CARD_1:47, XBOOLE_0:def 1;
reconsider v =
v as
VECTOR of
V by A11;
{v} is
Subset of
B
by A11, SUBSET_1:63;
then A12:
card (B \ {v}) =
(card B) - (card {v})
by CARD_2:63
.=
(m + 1) - 1
by A8, CARD_1:50
.=
m
;
set Bv =
B \ {v};
A13:
B \ {v} c= B
by XBOOLE_1:36;
A14:
B \ {v} is
linearly-independent
by A10, RLVECT_3:6, XBOOLE_1:36;
A15:
not
v in Lin (B \ {v})
by A10, A11, RUSUB_3:25;
now assume
m = n
;
:: thesis: contradictionthen consider C being
finite Subset of
V such that A16:
(
C c= A &
card C = m - m &
UNITSTR(# the
carrier of
V,the
U2 of
V,the
addF of
V,the
Mult of
V,the
scalar of
V #)
= Lin ((B \ {v}) \/ C) )
by A6, A7, A9, A12, A14;
C = {}
by A16;
then
B \ {v} is
Basis of
V
by A14, A16, RUSUB_3:def 2;
hence
contradiction
by A15, RUSUB_3:21;
:: thesis: verum end;
then
(
m <> n &
m <= n )
by A6, A7, A9, A12, A14;
then A17:
m < n
by XXREAL_0:1;
consider C being
finite Subset of
V such that A18:
C c= A
and A19:
card C = n - m
and A20:
UNITSTR(# the
carrier of
V,the
U2 of
V,the
addF of
V,the
Mult of
V,the
scalar of
V #)
= Lin ((B \ {v}) \/ C)
by A6, A7, A9, A12, A14;
v in Lin ((B \ {v}) \/ C)
by A20, STRUCT_0:def 5;
then consider w being
VECTOR of
V such that A21:
w in C
and A22:
w in Lin (((C \/ (B \ {v})) \ {w}) \/ {v})
by A15, Th1;
set Cw =
C \ {w};
C \ {w} c= C
by XBOOLE_1:36;
then A23:
C \ {w} c= A
by A18, XBOOLE_1:1;
{w} is
Subset of
C
by A21, SUBSET_1:63;
then A24:
card (C \ {w}) =
(card C) - (card {w})
by CARD_2:63
.=
(n - m) - 1
by A19, CARD_1:50
.=
n - (m + 1)
;
A25:
C = (C \ {w}) \/ {w}
by A21, Lm1;
A26:
((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
;
((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
(C \ {w}) \/ (((B \ {v}) \ {w}) \/ {v}) c= B \/ (C \ {w})
by A11, Lm1;
then
Lin (((C \/ (B \ {v})) \ {w}) \/ {v}) is
Subspace of
Lin (B \/ (C \ {w}))
by A26, RUSUB_3:7;
then A27:
w in Lin (B \/ (C \ {w}))
by A22, RUSUB_1:1;
then
(B \ {v}) \/ C c= the
carrier of
(Lin (B \/ (C \ {w})))
by TARSKI:def 3;
then
Lin ((B \ {v}) \/ C) is
Subspace of
Lin (B \/ (C \ {w}))
by RUSUB_3:27;
then
( the
carrier of
(Lin ((B \ {v}) \/ C)) c= the
carrier of
(Lin (B \/ (C \ {w}))) & the
carrier of
(Lin (B \/ (C \ {w}))) c= the
carrier of
V )
by RUSUB_1:def 1;
then
the
carrier of
(Lin (B \/ (C \ {w}))) = the
carrier of
V
by A20, XBOOLE_0:def 10;
then
UNITSTR(# the
carrier of
V,the
U2 of
V,the
addF of
V,the
Mult of
V,the
scalar of
V #)
= Lin (B \/ (C \ {w}))
by A20, RUSUB_1:24;
hence
(
m + 1
<= n & ex
C being
finite Subset of
V st
(
C c= A &
card C = n - (m + 1) &
UNITSTR(# the
carrier of
V,the
U2 of
V,the
addF of
V,the
Mult of
V,the
scalar of
V #)
= Lin (B \/ C) ) )
by A17, A23, A24, NAT_1:13;
:: thesis: verum
end;
for m being Element of NAT holds S1[m]
from NAT_1:sch 1(A3, A5);
hence
( card B <= card A & ex C being finite Subset of V st
( C c= A & card C = (card A) - (card B) & UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar of V #) = Lin (B \/ C) ) )
by A1, A2; :: thesis: verum