:: Linear Transformations of Euclidean Topological Spaces. Part {II}
:: by Karol P\kak
::
:: Received October 26, 2010
:: Copyright (c) 2010-2011 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)

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 b₁ -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;

begin

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)

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 m, n being Nat
for f being b₂ -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 m, n being Nat
for f being b₂ -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 b₁ -element real-valued FinSequence
for M being Matrix of n,m,F_Real st M is one-to-one 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 b₁ -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 b₁ -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;

begin

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

proof end;

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

proof end;

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 b₂ -element real-valued FinSequence holds (v |-- A) . f = (((Mx2Tran M) . v) |-- ((Mx2Tran M) .: A)) . ((Mx2Tran M) . f) ) )

proof end;

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

proof end;

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

proof end;