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

Lm1: for n being Nat holds the carrier of () = the carrier of ()
proof end;

Lm2: for n being Nat holds 0. () = 0. ()
proof end;

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

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 ()
for fr being Function of (),REAL
for Fv being FinSequence of ()
for fv being Function of (),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 ()
for Fv being FinSequence of () 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 ()
for Ar being Subset of () st Af = Ar holds
[#] (Lin Ar) = [#] (Lin Af)
proof end;

theorem Th7: :: MATRTOP2:7
for n being Nat
for Af being Subset of ()
for Ar being Subset of () 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 ();
coherence ;
end;

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

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 ()
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 () = 1 holds
ex L being Linear_Combination of lines M st
( Sum L = () . 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 = () . 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 = () . 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 () st B = M holds
for Mf being Element of (Lin ()) st Mf = () . 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 () = [#] (Lin ())
proof end;

theorem Th19: :: MATRTOP2:19
for n being Nat
for F being one-to-one FinSequence of () 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 () 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
() .: ([#] (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 () st card A = card B holds
ex M being Matrix of n,F_Real st
( M is invertible & () .: ([#] (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 () st the_rank_of M = n holds
() .: 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 () st the_rank_of M = n holds
() .: 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 () st the_rank_of M = n holds
for v being Element of () st v in Affin A holds
( () . v in Affin (() .: A) & ( for f being b1 -element real-valued FinSequence holds (v |-- A) . f = ((() . v) |-- (() .: A)) . (() . 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 () st the_rank_of M = n holds
() " 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 () st the_rank_of M = n holds
() " A is affinely-independent
proof end;