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


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

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

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

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 )
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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)
proof end;

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 )
proof end;

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
proof end;

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
proof end;

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
proof end;

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 )
proof end;

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 )
proof end;

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))
proof end;

:: a Vector in Basis
theorem :: MATRTOP2:13
for n, m 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)
proof end;

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)
proof end;

Lm5: for n, m being Nat
for f being b1 -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 ) ) )
proof end;

theorem Th15: :: MATRTOP2:15
for n, m being Nat
for f being b1 -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))}))) ) )
proof end;

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 ) )
proof end;

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
proof end;

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))
proof end;

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 )
proof end;

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) )
proof end;

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))
proof end;

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) )
proof end;

:: Mx2Tran Operator
theorem Th23: :: MATRTOP2:23
for n, m 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
proof end;

theorem Th24: :: MATRTOP2:24
for n, m 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
proof end;

theorem :: MATRTOP2:25
for n, m 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 b1 -element real-valued FinSequence holds (v |-- A) . f = (((Mx2Tran M) . v) |-- ((Mx2Tran M) .: A)) . ((Mx2Tran M) . f) ) )
proof end;

theorem Th26: :: MATRTOP2:26
for n, m 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
proof end;

theorem :: MATRTOP2:27
for n, m 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
proof end;