let K be Field; 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; 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; ( 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
; 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; ( 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
; 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:
for n being Nat st S1[n] holds
S1[n + 1]
proof
card U <> 0
by A2;
then reconsider C =
(card U) - 1 as
Element of
NAT by NAT_1:20;
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A4:
S1[
n]
;
S1[n + 1]
set n1 =
n + 1;
let L be
Linear_Combination of
U \ {u};
( card (Carrier L) = n + 1 implies ( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent ) )
assume A5:
card (Carrier L) = n + 1
;
( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent )
consider x being
object such that A6:
x in Carrier L
by A5, CARD_1:27, XBOOLE_0:def 1;
A7:
Carrier L c= U \ {u}
by VECTSP_6:def 4;
then
x in U
by A6, XBOOLE_0:def 5;
then A8:
x <> 0. V1
by A1, VECTSP_7:2;
reconsider x =
x as
Vector of
V1 by A6;
x in {x}
by TARSKI:def 1;
then
x in Lin {x}
by VECTSP_7:8;
then consider X being
Linear_Combination of
{x} such that A9:
x = Sum X
by VECTSP_7:7;
set Lx =
L . x;
set LxX =
(L . x) * X;
(
Carrier ((L . x) * X) c= Carrier X &
Carrier X c= {x} )
by VECTSP_6:28, VECTSP_6:def 4;
then A10:
Carrier ((L . x) * X) c= {x}
;
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:41, XBOOLE_1:9;
then
Carrier (L - ((L . x) * X)) c= (Carrier L) \/ {x}
;
then A11:
Carrier (L - ((L . x) * X)) c= Carrier L
by A6, ZFMISC_1:40;
then
Carrier (L - ((L . x) * X)) c= U \ {u}
by A7;
then reconsider LLxX =
L - ((L . x) * X) as
Linear_Combination of
U \ {u} by VECTSP_6:def 4;
A12:
x in (U \ {u}) \/ {(u + (Sum LLxX))}
by A6, A7, XBOOLE_0:def 3;
A13:
(Carrier L) \ {x} c= Carrier (L - ((L . x) * X))
(X . x) * x =
x
by A9, VECTSP_6:17
.=
(1_ K) * x
by VECTSP_1:def 17
;
then A17:
X . x = 1_ K
by A8, VECTSP10:4;
(L - ((L . x) * X)) . x =
(L . x) - (((L . x) * X) . x)
by VECTSP_6:40
.=
(L . x) - ((L . x) * (1_ K))
by A17, VECTSP_6:def 9
.=
(L . x) - (L . x)
.=
0. K
by RLVECT_1:5
;
then
not
x in Carrier (L - ((L . x) * X))
by VECTSP_6:2;
then
Carrier (L - ((L . x) * X)) c= (Carrier L) \ {x}
by A11, ZFMISC_1:34;
then A18:
Carrier (L - ((L . x) * X)) = (Carrier L) \ {x}
by A13;
{x} c= Carrier L
by A6, ZFMISC_1:31;
then card (Carrier (L - ((L . x) * X))) =
(n + 1) - (card {x})
by A5, A18, CARD_2:44
.=
(n + 1) - 1
by CARD_1:30
.=
n
;
then A19:
(U \ {u}) \/ {(u + (Sum LLxX))} is
linearly-independent
by A4;
u + (Sum LLxX) in {(u + (Sum LLxX))}
by TARSKI:def 1;
then A20:
u + (Sum LLxX) in (U \ {u}) \/ {(u + (Sum LLxX))}
by XBOOLE_0:def 3;
A21:
not
u + (Sum L) in U \ {u}
card U = C + 1
;
then
card (U \ {u}) = C
by A2, STIRL2_1:55;
then A24:
card ((U \ {u}) \/ {(u + (Sum L))}) = C + 1
by A21, CARD_2:41;
Sum L =
(0. V1) + (Sum L)
by RLVECT_1:def 4
.=
((Sum ((L . x) * X)) + (- (Sum ((L . x) * X)))) + (Sum L)
by RLVECT_1:5
.=
(Sum ((L . x) * X)) + ((Sum L) - (Sum ((L . x) * X)))
by RLVECT_1:def 3
.=
(Sum ((L . x) * X)) + (Sum LLxX)
by VECTSP_6:47
.=
((L . x) * x) + (Sum LLxX)
by A9, VECTSP_6:45
;
then A25:
(u + (Sum LLxX)) + ((L . x) * x) = u + (Sum L)
by RLVECT_1:def 3;
A26:
not
u + (Sum LLxX) in U \ {u}
then A29:
((U \ {u}) \/ {(u + (Sum LLxX))}) \ {(u + (Sum LLxX))} = U \ {u}
by ZFMISC_1:117;
u + (Sum LLxX) <> x
by A6, A7, A26;
hence
(
card U = card ((U \ {u}) \/ {(u + (Sum L))}) &
(U \ {u}) \/ {(u + (Sum L))} is
linearly-independent )
by A19, A25, A29, A20, A12, A24, MATRIX13:115;
verum
end;
let L be Linear_Combination of U \ {u}; ( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent )
A30:
S1[ 0 ]
for n being Nat holds S1[n]
from NAT_1:sch 2(A30, A3);
then
S1[ card (Carrier L)]
;
hence
( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent )
; verum