let m be Nat; :: thesis: for K being Field
for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1 holds
( rng (b1 | m) is linearly-independent Subset of V1 & ( for A being Subset of V1 st A = rng (b1 | m) holds
b1 | m is OrdBasis of Lin A ) )
let K be Field; :: thesis: for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1 holds
( rng (b1 | m) is linearly-independent Subset of V1 & ( for A being Subset of V1 st A = rng (b1 | m) holds
b1 | m is OrdBasis of Lin A ) )
let V1 be finite-dimensional VectSp of K; :: thesis: for b1 being OrdBasis of V1 holds
( rng (b1 | m) is linearly-independent Subset of V1 & ( for A being Subset of V1 st A = rng (b1 | m) holds
b1 | m is OrdBasis of Lin A ) )
let b1 be OrdBasis of V1; :: thesis: ( rng (b1 | m) is linearly-independent Subset of V1 & ( for A being Subset of V1 st A = rng (b1 | m) holds
b1 | m is OrdBasis of Lin A ) )
reconsider RNG = rng b1 as Basis of V1 by MATRLIN:def 2;
A1: RNG is linearly-independent by VECTSP_7:def 3;
rng (b1 | m) c= RNG by RELAT_1:70;
hence rng (b1 | m) is linearly-independent Subset of V1 by A1, VECTSP_7:1, XBOOLE_1:1; :: thesis: for A being Subset of V1 st A = rng (b1 | m) holds
b1 | m is OrdBasis of Lin A
let A be Subset of V1; :: thesis: ( A = rng (b1 | m) implies b1 | m is OrdBasis of Lin A )
assume A2: A = rng (b1 | m) ; :: thesis: b1 | m is OrdBasis of Lin A
A3: A c= the carrier of (Lin A)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in the carrier of (Lin A) )
assume x in A ; :: thesis: x in the carrier of (Lin A)
then x in Lin A by VECTSP_7:8;
hence x in the carrier of (Lin A) ; :: thesis: verum
end;
A is linearly-independent by A1, A2, RELAT_1:70, VECTSP_7:1;
then reconsider A9 = A as linearly-independent Subset of (Lin A) by A3, VECTSP_9:12;
b1 is one-to-one by MATRLIN:def 2;
then A4: b1 | m is one-to-one by FUNCT_1:52;
Lin A9 = ModuleStr(# the carrier of (Lin A), the addF of (Lin A), the ZeroF of (Lin A), the lmult of (Lin A) #) by VECTSP_9:17;
then ( rng (b1 | m) is Basis of (Lin A) & b1 | m is FinSequence of (Lin A) ) by A2, FINSEQ_1:def 4, VECTSP_7:def 3;
hence b1 | m is OrdBasis of Lin A by A4, MATRLIN:def 2; :: thesis: verum