:: Linear Transformations of Euclidean Topological Spaces. Part {II}
:: by Karol P\kak
::
:: Received October 26, 2010
:: Copyright (c) 2010-2012 Association of Mizar Users


begin

Lm1:  for n being Nat holds the carrier of (n -VectSp_over F_Real) = the carrier of (TOP-REAL n)
proofend;

Lm2:  for n being Nat holds 0. (n -VectSp_over F_Real) = 0. (TOP-REAL n)
proofend;

Lm3:  for n being Nat
for f being b1 -element real-valued FinSequence holds f is Point of (TOP-REAL n)
proofend;

theorem Th1: :: MATRTOP2:1
for X being set
for n being Nat holds
( X is Linear_Combination of n -VectSp_over F_Real iff X is Linear_Combination of TOP-REAL n )
proofend;

theorem Th2: :: MATRTOP2:2
for n being Nat
for Lv being Linear_Combination of n -VectSp_over F_Real
for Lr being Linear_Combination of TOP-REAL n st Lr = Lv holds
Carrier Lr = Carrier Lv
proofend;

theorem Th3: :: MATRTOP2:3
for n being Nat
for F being FinSequence of (TOP-REAL n)
for fr being Function of (TOP-REAL n),REAL
for Fv being FinSequence of (n -VectSp_over F_Real)
for fv being Function of (n -VectSp_over F_Real),F_Real st fr = fv & F = Fv holds
fr (#) F = fv (#) Fv
proofend;

theorem Th4: :: MATRTOP2:4
for n being Nat
for F being FinSequence of (TOP-REAL n)
for Fv being FinSequence of (n -VectSp_over F_Real) st Fv = F holds
Sum F = Sum Fv
proofend;

theorem Th5: :: MATRTOP2:5
for n being Nat
for Lv being Linear_Combination of n -VectSp_over F_Real
for Lr being Linear_Combination of TOP-REAL n st Lr = Lv holds
Sum Lr = Sum Lv
proofend;

theorem Th6: :: MATRTOP2:6
for n being Nat
for Af being Subset of (n -VectSp_over F_Real)
for Ar being Subset of (TOP-REAL n) st Af = Ar holds
[#] (Lin Ar) = [#] (Lin Af)
proofend;

theorem Th7: :: MATRTOP2:7
for n being Nat
for Af being Subset of (n -VectSp_over F_Real)
for Ar being Subset of (TOP-REAL n) st Af = Ar holds
( Af is linearly-independent iff Ar is linearly-independent )
proofend;

theorem Th8: :: MATRTOP2:8
for K being Field
for V being VectSp of K
for W being Subspace of V
for L being Linear_Combination of V holds L | the carrier of W is Linear_Combination of W
proofend;

theorem :: MATRTOP2:9
for K being Field
for V being VectSp of K
for A being linearly-independent Subset of V
for L1, L2 being Linear_Combination of V st Carrier L1 c= A & Carrier L2 c= A & Sum L1 = Sum L2 holds
L1 = L2
proofend;

theorem :: MATRTOP2:10
for V being RealLinearSpace
for W being Subspace of V
for L being Linear_Combination of V holds L | the carrier of W is Linear_Combination of W
proofend;

theorem :: MATRTOP2:11
for X being set
for n being Nat
for U being Subspace of n -VectSp_over F_Real
for W being Subspace of TOP-REAL n st [#] U = [#] W holds
( X is Linear_Combination of U iff X is Linear_Combination of W )
proofend;

theorem :: MATRTOP2:12
for n being Nat
for U being Subspace of n -VectSp_over F_Real
for W being Subspace of TOP-REAL n
for LU being Linear_Combination of U
for LW being Linear_Combination of W st LU = LW holds
( Carrier LU = Carrier LW & Sum LU = Sum LW )
proofend;

registration
let m be Nat;
let K be Field;
let A be Subset of (m -VectSp_over K);
cluster Lin A ->  finite-dimensional ;
coherence
 Lin A is finite-dimensional ;
end;

Lm4:  for n, m being Nat
for M being Matrix of n,m,F_Real holds lines M c= [#] (Lin (lines M))
proofend;

begin

:: a Vector in Basis
theorem :: MATRTOP2:13
for m, n being Nat
for M being Matrix of n,m,F_Real st the_rank_of M = n holds
M is OrdBasis of Lin (lines M)
proofend;

theorem Th14: :: MATRTOP2:14
for K being Field
for V, W being VectSp of K
for T being linear-transformation of V,W
for A being Subset of V
for L being Linear_Combination of A st T | A is one-to-one holds
T . (Sum L) = Sum (T @ L)
proofend;

Lm5:  for m, n being Nat
for f being b2 -element real-valued FinSequence
for M being Matrix of n,m,F_Real st card (lines M) = 1 holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in Seg n holds
( L . (Line (M,k)) = Sum f & M " {(Line (M,k))} = dom f ) ) )
proofend;

theorem Th15: :: MATRTOP2:15
for m, n being Nat
for f being b2 -element real-valued FinSequence
for M being Matrix of n,m,F_Real
for S being Subset of (Seg n) st M | S is one-to-one & rng (M | S) = lines M holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in S holds
L . (Line (M,k)) = Sum (Seq (f | (M " {(Line (M,k))}))) ) )
proofend;

theorem Th16: :: MATRTOP2:16
for n, m being Nat
for f being b1 -element real-valued FinSequence
for M being Matrix of n,m,F_Real st M is without_repeated_line holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in dom f holds
L . (Line (M,k)) = f . k ) )
proofend;

theorem :: MATRTOP2:17
for n, m being Nat
for f being b1 -element real-valued FinSequence
for M being Matrix of n,m,F_Real
for B being OrdBasis of Lin (lines M) st B = M holds
for Mf being Element of (Lin (lines M)) st Mf = (Mx2Tran M) . f holds
Mf |-- B = f
proofend;

theorem Th18: :: MATRTOP2:18
for n, m being Nat
for M being Matrix of n,m,F_Real holds rng (Mx2Tran M) = [#] (Lin (lines M))
proofend;

theorem Th19: :: MATRTOP2:19
for n being Nat
for F being one-to-one FinSequence of (TOP-REAL n) st rng F is linearly-independent holds
ex M being Matrix of n,F_Real st
( M is invertible & M | (len F) = F )
proofend;

theorem Th20: :: MATRTOP2:20
for n, k being Nat
for f being b1 -element real-valued FinSequence
for B being OrdBasis of n -VectSp_over F_Real st B = MX2FinS (1. (F_Real,n)) holds
( f in Lin (rng (B | k)) iff f = (f | k) ^ ((n -' k) |-> 0) )
proofend;

theorem Th21: :: MATRTOP2:21
for n being Nat
for F being one-to-one FinSequence of (TOP-REAL n) st rng F is linearly-independent holds
for B being OrdBasis of n -VectSp_over F_Real st B = MX2FinS (1. (F_Real,n)) holds
for M being Matrix of n,F_Real st M is invertible & M | (len F) = F holds
(Mx2Tran M) .: ([#] (Lin (rng (B | (len F))))) = [#] (Lin (rng F))
proofend;

theorem :: MATRTOP2:22
for n being Nat
for A, B being linearly-independent Subset of (TOP-REAL n) st card A = card B holds
ex M being Matrix of n,F_Real st
( M is invertible & (Mx2Tran M) .: ([#] (Lin A)) = [#] (Lin B) )
proofend;

begin

:: Mx2Tran Operator
theorem Th23: :: MATRTOP2:23
for m, n being Nat
for M being Matrix of n,m,F_Real
for A being linearly-independent Subset of (TOP-REAL n) st the_rank_of M = n holds
(Mx2Tran M) .: A is linearly-independent
proofend;

theorem Th24: :: MATRTOP2:24
for m, n being Nat
for M being Matrix of n,m,F_Real
for A being affinely-independent Subset of (TOP-REAL n) st the_rank_of M = n holds
(Mx2Tran M) .: A is affinely-independent
proofend;

theorem :: MATRTOP2:25
for m, n being Nat
for M being Matrix of n,m,F_Real
for A being affinely-independent Subset of (TOP-REAL n) st the_rank_of M = n holds
for v being Element of (TOP-REAL n) st v in Affin A holds
( (Mx2Tran M) . v in Affin ((Mx2Tran M) .: A) & ( for f being b2 -element real-valued FinSequence holds (v |-- A) . f = (((Mx2Tran M) . v) |-- ((Mx2Tran M) .: A)) . ((Mx2Tran M) . f) ) )
proofend;

theorem Th26: :: MATRTOP2:26
for m, n being Nat
for M being Matrix of n,m,F_Real
for A being linearly-independent Subset of (TOP-REAL m) st the_rank_of M = n holds
(Mx2Tran M) " A is linearly-independent
proofend;

theorem :: MATRTOP2:27
for m, n being Nat
for M being Matrix of n,m,F_Real
for A being affinely-independent Subset of (TOP-REAL m) st the_rank_of M = n holds
(Mx2Tran M) " A is affinely-independent
proofend;