let K be Field; :: thesis: for V1 being VectSp of K
for U being finite Subset of V1 st U is linearly-independent holds
for u being Vector of V1 st u in U holds
for L being Linear_Combination of U \ {u} holds
( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent )
let V1 be VectSp of K; :: thesis: for U being finite Subset of V1 st U is linearly-independent holds
for u being Vector of V1 st u in U holds
for L being Linear_Combination of U \ {u} holds
( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent )
set V = V1;
let U be finite Subset of V1; :: thesis: ( U is linearly-independent implies for u being Vector of V1 st u in U holds
for L being Linear_Combination of U \ {u} holds
( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent ) )
assume A1:
U is linearly-independent
; :: thesis: for u being Vector of V1 st u in U holds
for L being Linear_Combination of U \ {u} holds
( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent )
let u be Vector of V1; :: thesis: ( u in U implies for L being Linear_Combination of U \ {u} holds
( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent ) )
assume A2:
u in U
; :: thesis: for L being Linear_Combination of U \ {u} holds
( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent )
defpred S1[ Nat] means for L being Linear_Combination of U \ {u} st card (Carrier L) = $1 holds
( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent );
A3:
S1[ 0 ]
A5:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
:: thesis: ( S1[n] implies S1[n + 1] )
assume A6:
S1[
n]
;
:: thesis: S1[n + 1]
set n1 =
n + 1;
let L be
Linear_Combination of
U \ {u};
:: thesis: ( card (Carrier L) = n + 1 implies ( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent ) )
assume A7:
card (Carrier L) = n + 1
;
:: thesis: ( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent )
consider x being
set such that A8:
x in Carrier L
by A7, CARD_1:47, XBOOLE_0:def 1;
A9:
Carrier L c= U \ {u}
by VECTSP_6:def 7;
then
x in U
by A8, XBOOLE_0:def 5;
then A10:
x <> 0. V1
by A1, VECTSP_7:3;
reconsider x =
x as
Vector of
V1 by A8;
x in {x}
by TARSKI:def 1;
then
x in Lin {x}
by VECTSP_7:13;
then consider X being
Linear_Combination of
{x} such that A11:
x = Sum X
by VECTSP_7:12;
(X . x) * x =
x
by A11, VECTSP_6:43
.=
(1_ K) * x
by VECTSP_1:def 26
;
then A12:
X . x = 1_ K
by A10, VECTSP10:5;
set Lx =
L . x;
set LxX =
(L . x) * X;
(
Carrier ((L . x) * X) c= Carrier X &
Carrier X c= {x} )
by VECTSP_6:58, VECTSP_6:def 7;
then A13:
Carrier ((L . x) * X) c= {x}
by XBOOLE_1:1;
then
(
Carrier (L - ((L . x) * X)) c= (Carrier L) \/ (Carrier ((L . x) * X)) &
(Carrier L) \/ (Carrier ((L . x) * X)) c= (Carrier L) \/ {x} )
by VECTSP_6:74, XBOOLE_1:9;
then
Carrier (L - ((L . x) * X)) c= (Carrier L) \/ {x}
by XBOOLE_1:1;
then A14:
Carrier (L - ((L . x) * X)) c= Carrier L
by A8, ZFMISC_1:46;
then
Carrier (L - ((L . x) * X)) c= U \ {u}
by A9, XBOOLE_1:1;
then reconsider LLxX =
L - ((L . x) * X) as
Linear_Combination of
U \ {u} by VECTSP_6:def 7;
(L - ((L . x) * X)) . x =
(L . x) - (((L . x) * X) . x)
by VECTSP_6:73
.=
(L . x) - ((L . x) * (1_ K))
by A12, VECTSP_6:def 12
.=
(L . x) - (L . x)
by VECTSP_1:def 13
.=
0. K
by RLVECT_1:16
;
then
not
x in Carrier (L - ((L . x) * X))
by VECTSP_6:20;
then A15:
Carrier (L - ((L . x) * X)) c= (Carrier L) \ {x}
by A14, ZFMISC_1:40;
(Carrier L) \ {x} c= Carrier (L - ((L . x) * X))
then A18:
Carrier (L - ((L . x) * X)) = (Carrier L) \ {x}
by A15, XBOOLE_0:def 10;
{x} c= Carrier L
by A8, ZFMISC_1:37;
then card (Carrier (L - ((L . x) * X))) =
(n + 1) - (card {x})
by A7, A18, CARD_2:63
.=
(n + 1) - 1
by CARD_1:50
.=
n
;
then A19:
(U \ {u}) \/ {(u + (Sum LLxX))} is
linearly-independent
by A6;
Sum L =
(0. V1) + (Sum L)
by RLVECT_1:def 7
.=
((Sum ((L . x) * X)) + (- (Sum ((L . x) * X)))) + (Sum L)
by RLVECT_1:16
.=
(Sum ((L . x) * X)) + ((Sum L) - (Sum ((L . x) * X)))
by RLVECT_1:def 6
.=
(Sum ((L . x) * X)) + (Sum LLxX)
by VECTSP_6:80
.=
((L . x) * x) + (Sum LLxX)
by A11, VECTSP_6:78
;
then A20:
(u + (Sum LLxX)) + ((L . x) * x) = u + (Sum L)
by RLVECT_1:def 6;
A21:
not
u + (Sum LLxX) in U \ {u}
then A23:
((U \ {u}) \/ {(u + (Sum LLxX))}) \ {(u + (Sum LLxX))} = U \ {u}
by ZFMISC_1:141;
u + (Sum LLxX) in {(u + (Sum LLxX))}
by TARSKI:def 1;
then A24:
(
u + (Sum LLxX) in (U \ {u}) \/ {(u + (Sum LLxX))} &
x in (U \ {u}) \/ {(u + (Sum LLxX))} &
u + (Sum LLxX) <> x )
by A21, A9, A8, XBOOLE_0:def 3;
card U <> 0
by A2;
then reconsider C =
(card U) - 1 as
Element of
NAT by NAT_1:20;
A25:
not
u + (Sum L) in U \ {u}
card U = C + 1
;
then
card (U \ {u}) = C
by A2, STIRL2_1:65;
then
card ((U \ {u}) \/ {(u + (Sum L))}) = C + 1
by A25, CARD_2:54;
hence
(
card U = card ((U \ {u}) \/ {(u + (Sum L))}) &
(U \ {u}) \/ {(u + (Sum L))} is
linearly-independent )
by A23, A24, A19, A20, MATRIX13:115;
:: thesis: verum
end;
A27:
for n being Nat holds S1[n]
from NAT_1:sch 2(A3, A5);
let L be Linear_Combination of U \ {u}; :: thesis: ( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent )
S1[ card (Carrier L)]
by A27;
hence
( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent )
; :: thesis: verum