let R be Skew-Field; :: thesis: for V being LeftMod of R
for A being Subset of V st Lin A = V holds
ex B being Subset of V st
( B c= A & B is base )
let V be LeftMod of R; :: thesis: for A being Subset of V st Lin A = V holds
ex B being Subset of V st
( B c= A & B is base )
let A be Subset of V; :: thesis: ( Lin A = V implies ex B being Subset of V st
( B c= A & B is base ) )
A1: 0. R <> 1. R ;
defpred S₁[ set ] means ex B being Subset of V st
( B = $1 & B c= A & B is linearly-independent );
assume A2: Lin A = V ; :: thesis: ex B being Subset of V st
( B c= A & B is base )
consider Q being set such that
A3: for Z being set holds
( Z in Q iff ( Z in bool the carrier of V & S₁[Z] ) ) from XBOOLE_0:sch 1();

A4: now

let Z be set ; :: thesis: ( Z <> {} & Z c= Q & Z is c=-linear implies union Z in Q )
assume that
Z <> {} and
A5: Z c= Q and
A6: Z is c=-linear ; :: thesis: union Z in Q
set W = union Z;
union Z c= the carrier of V

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union Z or x in the carrier of V )
assume x in union Z ; :: thesis: x in the carrier of V
then consider X being set such that
A7: x in X and
A8: X in Z by TARSKI:def 4;
X in bool the carrier of V by A3, A5, A8;
hence x in the carrier of V by A7; :: thesis: verum

end;

then reconsider W = union Z as Subset of V ;
A9: W is linearly-independent

proof

deffunc H₁( set ) -> set = { C where C is Subset of V : ( $1 in C & C in Z ) } ;
let l be Linear_Combination of W; :: according to LMOD_5:def 1 :: thesis: ( not Sum l = 0. V or Carrier l = {} )
assume that
A10: Sum l = 0. V and
A11: Carrier l <> {} ; :: thesis: contradiction
consider f being Function such that
A12: dom f = Carrier l and
A13: for x being set st x in Carrier l holds
f . x = H₁(x) from FUNCT_1:sch 3();
reconsider M = rng f as non empty set by A11, A12, RELAT_1:65;
consider F being Choice_Function of M;
set S = rng F;

A14: now

assume {} in M ; :: thesis: contradiction
then consider x being set such that
A15: x in dom f and
A16: f . x = {} by FUNCT_1:def 5;
Carrier l c= W by VECTSP_6:def 7;
then consider X being set such that
A17: x in X and
A18: X in Z by A12, A15, TARSKI:def 4;
reconsider X = X as Subset of V by A3, A5, A18;
X in { C where C is Subset of V : ( x in C & C in Z ) } by A17, A18;
hence contradiction by A12, A13, A15, A16; :: thesis: verum

end;

then A19: dom F = M by RLVECT_3:35;
then dom F is finite by A12, FINSET_1:26;
then A20: rng F is finite by FINSET_1:26;

A21: now

let X be set ; :: thesis: ( X in rng F implies X in Z )
assume X in rng F ; :: thesis: X in Z
then consider x being set such that
A22: x in dom F and
A23: F . x = X by FUNCT_1:def 5;
consider y being set such that
A24: ( y in dom f & f . y = x ) by A19, A22, FUNCT_1:def 5;
A25: x = { C where C is Subset of V : ( y in C & C in Z ) } by A12, A13, A24;
X in x by A14, A19, A22, A23, ORDERS_1:def 1;
then ex C being Subset of V st
( C = X & y in C & C in Z ) by A25;
hence X in Z ; :: thesis: verum

end;

A26: now

let X, Y be set ; :: thesis: ( X in rng F & Y in rng F & not X c= Y implies Y c= X )
assume ( X in rng F & Y in rng F ) ; :: thesis: ( X c= Y or Y c= X )
then ( X in Z & Y in Z ) by A21;
then X,Y are_c=-comparable by A6, ORDINAL1:def 9;
hence ( X c= Y or Y c= X ) by XBOOLE_0:def 9; :: thesis: verum

end;

rng F <> {} by A19, RELAT_1:65;
then union (rng F) in rng F by A26, A20, CARD_2:81;
then union (rng F) in Z by A21;
then consider B being Subset of V such that
A27: B = union (rng F) and
B c= A and
A28: B is linearly-independent by A3, A5;
Carrier l c= union (rng F)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier l or x in union (rng F) )
set X = f . x;
assume A29: x in Carrier l ; :: thesis: x in union (rng F)
then A30: f . x = { C where C is Subset of V : ( x in C & C in Z ) } by A13;
A31: f . x in M by A12, A29, FUNCT_1:def 5;
then F . (f . x) in f . x by A14, ORDERS_1:def 1;
then A32: ex C being Subset of V st
( F . (f . x) = C & x in C & C in Z ) by A30;
F . (f . x) in rng F by A19, A31, FUNCT_1:def 5;
hence x in union (rng F) by A32, TARSKI:def 4; :: thesis: verum

end;

then l is Linear_Combination of B by A27, VECTSP_6:def 7;
hence contradiction by A10, A11, A28, LMOD_5:def 1; :: thesis: verum

end;

W c= A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in W or x in A )
assume x in W ; :: thesis: x in A
then consider X being set such that
A33: x in X and
A34: X in Z by TARSKI:def 4;
ex B being Subset of V st
( B = X & B c= A & B is linearly-independent ) by A3, A5, A34;
hence x in A by A33; :: thesis: verum

end;

hence union Z in Q by A3, A9; :: thesis: verum

end;

( {} the carrier of V c= A & {} the carrier of V is linearly-independent ) by LMOD_5:4, XBOOLE_1:2;
then Q <> {} by A3;
then consider X being set such that
A35: X in Q and
A36: for Z being set st Z in Q & Z <> X holds
not X c= Z by A4, ORDERS_1:177;
consider B being Subset of V such that
A37: B = X and
A38: B c= A and
A39: B is linearly-independent by A3, A35;
take B ; :: thesis: ( B c= A & B is base )
thus ( B c= A & B is linearly-independent ) by A38, A39; :: according to MOD_3:def 2 :: thesis: Lin B = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)
assume A40: Lin B <> VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) ; :: thesis: contradiction

now

assume A41: for v being Vector of V st v in A holds
v in Lin B ; :: thesis: contradiction

now

reconsider F = the carrier of (Lin B) as Subset of V by VECTSP_4:def 2;
let v be Vector of V; :: thesis: ( v in Lin A implies v in Lin B )
assume v in Lin A ; :: thesis: v in Lin B
then consider l being Linear_Combination of A such that
A42: v = Sum l by Th11;
Carrier l c= the carrier of (Lin B)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier l or x in the carrier of (Lin B) )
assume A43: x in Carrier l ; :: thesis: x in the carrier of (Lin B)
then reconsider a = x as Vector of V ;
Carrier l c= A by VECTSP_6:def 7;
then a in Lin B by A41, A43;
hence x in the carrier of (Lin B) by STRUCT_0:def 5; :: thesis: verum

end;

then reconsider l = l as Linear_Combination of F by VECTSP_6:def 7;
Sum l = v by A42;
then v in Lin F by Th11;
hence v in Lin B by A1, Th15; :: thesis: verum

end;

then Lin A is Subspace of Lin B by VECTSP_4:36;
hence contradiction by A2, A40, VECTSP_4:33; :: thesis: verum

end;

then consider v being Vector of V such that
A44: v in A and
A45: not v in Lin B ;
A46: B \/ {v} is linearly-independent

proof

let l be Linear_Combination of B \/ {v}; :: according to LMOD_5:def 1 :: thesis: ( not Sum l = 0. V or Carrier l = {} )
assume A47: Sum l = 0. V ; :: thesis: Carrier l = {}

now

per cases ( v in Carrier l or not v in Carrier l ) ;

suppose v in Carrier l ; :: thesis: Carrier l = {}

then l . v <> 0. R by VECTSP_6:20;
then - (l . v) <> 0. R by Lm1;
then A48: ((- (l . v)) ") * ((- (l . v)) * v) = (1. R) * v by Lm2
.= v by VECTSP_1:def 29 ;
deffunc H₁( Vector of V) -> Element of the carrier of R = l . $1;
consider f being Function of the carrier of V, the carrier of R such that
A49: f . v = 0. R and
A50: for u being Vector of V st u <> v holds
f . u = H₁(u) from FUNCT_2:sch 6();
reconsider f = f as Element of Funcs ( the carrier of V, the carrier of R) by FUNCT_2:11;

now

let u be Vector of V; :: thesis: ( not u in (Carrier l) \ {v} implies f . u = 0. R )
assume not u in (Carrier l) \ {v} ; :: thesis: f . u = 0. R
then ( not u in Carrier l or u in {v} ) by XBOOLE_0:def 5;
then ( ( l . u = 0. R & u <> v ) or u = v ) by TARSKI:def 1;
hence f . u = 0. R by A49, A50; :: thesis: verum

end;

then reconsider f = f as Linear_Combination of V by VECTSP_6:def 4;
Carrier f c= B

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in B )
A51: Carrier l c= B \/ {v} by VECTSP_6:def 7;
assume x in Carrier f ; :: thesis: x in B
then consider u being Vector of V such that
A52: u = x and
A53: f . u <> 0. R ;
f . u = l . u by A49, A50, A53;
then u in Carrier l by A53;
then ( u in B or u in {v} ) by A51, XBOOLE_0:def 3;
hence x in B by A49, A52, A53, TARSKI:def 1; :: thesis: verum

end;

then reconsider f = f as Linear_Combination of B by VECTSP_6:def 7;
deffunc H₂( Vector of V) -> Element of the carrier of R = 0. R;
consider g being Function of the carrier of V, the carrier of R such that
A54: g . v = - (l . v) and
A55: for u being Vector of V st u <> v holds
g . u = H₂(u) from FUNCT_2:sch 6();
reconsider g = g as Element of Funcs ( the carrier of V, the carrier of R) by FUNCT_2:11;

now

let u be Vector of V; :: thesis: ( not u in {v} implies g . u = 0. R )
assume not u in {v} ; :: thesis: g . u = 0. R
then u <> v by TARSKI:def 1;
hence g . u = 0. R by A55; :: thesis: verum

end;

then reconsider g = g as Linear_Combination of V by VECTSP_6:def 4;
Carrier g c= {v}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier g or x in {v} )
assume x in Carrier g ; :: thesis: x in {v}
then ex u being Vector of V st
( x = u & g . u <> 0. R ) ;
then x = v by A55;
hence x in {v} by TARSKI:def 1; :: thesis: verum

end;

then reconsider g = g as Linear_Combination of {v} by VECTSP_6:def 7;
f - g = l

proof

let u be Vector of V; :: according to VECTSP_6:def 10 :: thesis: (f - g) . u = l . u

now

per cases ( v = u or v <> u ) ;

suppose A56: v = u ; :: thesis: (f - g) . u = l . u

thus (f - g) . u = (f . u) - (g . u) by VECTSP_6:73
.= (0. R) + (- (- (l . v))) by A49, A54, A56, RLVECT_1:def 14
.= (l . v) + (0. R) by RLVECT_1:30
.= l . u by A56, RLVECT_1:10 ; :: thesis: verum

end;

suppose A57: v <> u ; :: thesis: (f - g) . u = l . u

thus (f - g) . u = (f . u) - (g . u) by VECTSP_6:73
.= (l . u) - (g . u) by A50, A57
.= (l . u) - (0. R) by A55, A57
.= l . u by RLVECT_1:26 ; :: thesis: verum

end;

end;

end;

hence (f - g) . u = l . u ; :: thesis: verum

end;

then A58: 0. V = (Sum f) - (Sum g) by A47, VECTSP_6:80;
Sum g = (- (l . v)) * v by A54, VECTSP_6:43;
then Sum f = (- (l . v)) * v by A58, VECTSP_1:66;
then (- (l . v)) * v in Lin B by Th11;
hence Carrier l = {} by A45, A48, VECTSP_4:29; :: thesis: verum

end;

suppose A59: not v in Carrier l ; :: thesis: Carrier l = {}

Carrier l c= B

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier l or x in B )
assume A60: x in Carrier l ; :: thesis: x in B
Carrier l c= B \/ {v} by VECTSP_6:def 7;
then ( x in B or x in {v} ) by A60, XBOOLE_0:def 3;
hence x in B by A59, A60, TARSKI:def 1; :: thesis: verum

end;

then l is Linear_Combination of B by VECTSP_6:def 7;
hence Carrier l = {} by A39, A47, LMOD_5:def 1; :: thesis: verum

end;

end;

end;

hence Carrier l = {} ; :: thesis: verum

end;

{v} c= A by A44, ZFMISC_1:37;
then B \/ {v} c= A by A38, XBOOLE_1:8;
then A61: B \/ {v} in Q by A3, A46;
v in {v} by TARSKI:def 1;
then A62: v in B \/ {v} by XBOOLE_0:def 3;
not v in B by A45, Th12;
hence contradiction by A36, A37, A62, A61, XBOOLE_1:7; :: thesis: verum