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


begin

registration
let X, Y be set ;
let F be positive-yielding PartFunc of X,REAL;
cluster F | Y -> positive-yielding ;
coherence
F | Y is positive-yielding
proof end;
end;

registration
let X, Y be set ;
let F be negative-yielding PartFunc of X,REAL;
cluster F | Y -> negative-yielding ;
coherence
F | Y is negative-yielding
proof end;
end;

registration
let X, Y be set ;
let F be nonpositive-yielding PartFunc of X,REAL;
cluster F | Y -> nonpositive-yielding ;
coherence
F | Y is nonpositive-yielding
proof end;
end;

registration
let X, Y be set ;
let F be nonnegative-yielding PartFunc of X,REAL;
cluster F | Y -> nonnegative-yielding ;
coherence
F | Y is nonnegative-yielding
proof end;
end;

registration
let rf be real-valued FinSequence;
cluster sqrt rf -> FinSequence-like ;
coherence
sqrt rf is FinSequence-like
proof end;
end;

definition
let rf be real-valued FinSequence;
func @ rf -> FinSequence of F_Real equals :: MATRTOP1:def 1
rf;
coherence
rf is FinSequence of F_Real
proof end;
end;

:: deftheorem defines @ MATRTOP1:def 1 :
for rf being real-valued FinSequence holds @ rf = rf;

definition
let p be FinSequence of F_Real;
func @ p -> FinSequence of REAL equals :: MATRTOP1:def 2
p;
coherence
p is FinSequence of REAL ;
end;

:: deftheorem defines @ MATRTOP1:def 2 :
for p being FinSequence of F_Real holds @ p = p;

theorem :: MATRTOP1:1
for rf1, rf2 being real-valued FinSequence holds (@ rf1) + (@ rf2) = rf1 + rf2 by RVSUM_1:def 4;

theorem Th2: :: MATRTOP1:2
for rf1, rf2 being real-valued FinSequence holds sqrt (rf1 ^ rf2) = (sqrt rf1) ^ (sqrt rf2)
proof end;

theorem Th3: :: MATRTOP1:3
for r being real number holds sqrt <*r*> = <*(sqrt r)*>
proof end;

theorem Th4: :: MATRTOP1:4
for rf being real-valued FinSequence holds sqrt (rf ^2) = abs rf
proof end;

theorem Th5: :: MATRTOP1:5
for rf being real-valued FinSequence st rf is nonnegative-yielding holds
sqrt (Sum rf) <= Sum (sqrt rf)
proof end;

theorem :: MATRTOP1:6
for F being Function ex X being set st
( X c= dom F & rng F = rng (F | X) & F | X is one-to-one )
proof end;

registration
let cf be complex-valued FinSequence;
let X be set ;
cluster cf - X -> complex-valued ;
coherence
cf - X is complex-valued
proof end;
end;

registration
let rf be real-valued FinSequence;
let X be set ;
cluster rf - X -> real-valued ;
coherence
rf - X is real-valued
proof end;
end;

registration
let cf be complex-valued FinSubsequence;
cluster Seq cf -> complex-valued ;
coherence
Seq cf is complex-valued ;
end;

registration
let rf be real-valued FinSubsequence;
cluster Seq rf -> real-valued ;
coherence
Seq rf is real-valued ;
end;

theorem Th7: :: MATRTOP1:7
for X being set
for f, f1 being FinSequence
for P being Permutation of (dom f) st f1 = f * P holds
ex Q being Permutation of (dom (f - X)) st f1 - X = (f - X) * Q
proof end;

theorem :: MATRTOP1:8
for X being set
for cf, cf1 being complex-valued FinSequence
for P being Permutation of (dom cf) st cf1 = cf * P holds
Sum (cf1 - X) = Sum (cf - X)
proof end;

theorem Th9: :: MATRTOP1:9
for X being set
for f, f1 being FinSubsequence
for P being Permutation of (dom f) st f1 = f * P holds
ex Q being Permutation of (dom (Seq (f1 | (P " X)))) st Seq (f | X) = (Seq (f1 | (P " X))) * Q
proof end;

theorem :: MATRTOP1:10
for X being set
for cf, cf1 being complex-valued FinSubsequence
for P being Permutation of (dom cf) st cf1 = cf * P holds
Sum (Seq (cf | X)) = Sum (Seq (cf1 | (P " X)))
proof end;

theorem Th11: :: MATRTOP1:11
for X, Y being set
for f being FinSubsequence
for n being Element of NAT st ( for i being Nat holds
( i + n in X iff i in Y ) ) holds
(n Shift f) | X = n Shift (f | Y)
proof end;

theorem Th12: :: MATRTOP1:12
for X being set
for f1, f2 being FinSequence ex Y being Subset of NAT st
( Seq ((f1 ^ f2) | X) = (Seq (f1 | X)) ^ (Seq (f2 | Y)) & ( for n being Nat st n > 0 holds
( n in Y iff n + (len f1) in X /\ (dom (f1 ^ f2)) ) ) )
proof end;

theorem :: MATRTOP1:13
for X being set
for g1, f1, g2, f2 being FinSequence st len g1 = len f1 & len g2 <= len f2 holds
Seq ((f1 ^ f2) | ((g1 ^ g2) " X)) = (Seq (f1 | (g1 " X))) ^ (Seq (f2 | (g2 " X)))
proof end;

theorem :: MATRTOP1:14
for X being set
for n, m being Nat
for D being non empty set
for M being Matrix of n,m,D holds M - X is Matrix of n -' (card (M " X)),m,D
proof end;

theorem Th15: :: MATRTOP1:15
for n, m being Nat
for F being Function of (Seg n),(Seg n)
for D being non empty set
for M being Matrix of n,m,D
for i being Nat st i in Seg (width M) holds
Col ((M * F),i) = (Col (M,i)) * F
proof end;

Lm1: for n, m being Nat
for K being Field
for A being Matrix of n,m,K st ( n = 0 implies m = 0 ) & the_rank_of A = n holds
ex B being Matrix of m -' n,m,K st the_rank_of (A ^ B) = m
proof end;

theorem Th16: :: MATRTOP1:16
for n, m being Nat
for K being Field
for A being Matrix of n,m,K st the_rank_of A = n holds
ex B being Matrix of m -' n,m,K st the_rank_of (A ^ B) = m
proof end;

theorem :: MATRTOP1:17
for n, m being Nat
for K being Field
for A being Matrix of n,m,K st the_rank_of A = m holds
ex B being Matrix of n,n -' m,K st the_rank_of (A ^^ B) = n
proof end;

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

begin

:: given by a Transformation Matrix
definition
let n, m be Nat;
let M be Matrix of n,m,F_Real;
func Mx2Tran M -> Function of (TOP-REAL n),(TOP-REAL m) means :Def3: :: MATRTOP1:def 3
 for f being n -element real-valued FinSequence holds it . f = Line (((LineVec2Mx (@ f)) * M),1) if n <> 0
otherwise for f being n -element real-valued FinSequence holds it . f = 0. (TOP-REAL m);
existence
( ( n <> 0 implies ex b1 being Function of (TOP-REAL n),(TOP-REAL m) st
for f being n -element real-valued FinSequence holds b1 . f = Line (((LineVec2Mx (@ f)) * M),1) ) & ( not n <> 0 implies ex b1 being Function of (TOP-REAL n),(TOP-REAL m) st
for f being n -element real-valued FinSequence holds b1 . f = 0. (TOP-REAL m) ) )
proof end;
uniqueness
for b1, b2 being Function of (TOP-REAL n),(TOP-REAL m) holds
( ( n <> 0 & ( for f being n -element real-valued FinSequence holds b1 . f = Line (((LineVec2Mx (@ f)) * M),1) ) & ( for f being n -element real-valued FinSequence holds b2 . f = Line (((LineVec2Mx (@ f)) * M),1) ) implies b1 = b2 ) & ( not n <> 0 & ( for f being n -element real-valued FinSequence holds b1 . f = 0. (TOP-REAL m) ) & ( for f being n -element real-valued FinSequence holds b2 . f = 0. (TOP-REAL m) ) implies b1 = b2 ) )
proof end;
correctness
consistency
for b1 being Function of (TOP-REAL n),(TOP-REAL m) holds verum;
;
end;

:: deftheorem Def3 defines Mx2Tran MATRTOP1:def 3 :
for n, m being Nat
for M being Matrix of n,m,F_Real
for b4 being Function of (TOP-REAL n),(TOP-REAL m) holds
( ( n <> 0 implies ( b4 = Mx2Tran M iff for f being b1 -element real-valued FinSequence holds b4 . f = Line (((LineVec2Mx (@ f)) * M),1) ) ) & ( not n <> 0 implies ( b4 = Mx2Tran M iff for f being b1 -element real-valued FinSequence holds b4 . f = 0. (TOP-REAL m) ) ) );

Lm3: now :: thesis: for n, m being Nat
for M being Matrix of n,m,F_Real
for x being set holds (Mx2Tran M) . x is real-valued FinSequence
let n, m be Nat; :: thesis: for M being Matrix of n,m,F_Real
for x being set holds (Mx2Tran b5) . b6 is real-valued FinSequence
let M be Matrix of n,m,F_Real; :: thesis: for x being set holds (Mx2Tran b4) . b5 is real-valued FinSequence
let x be set ; :: thesis: (Mx2Tran b3) . b4 is real-valued FinSequence
set T = Mx2Tran M;
per cases ( x in dom (Mx2Tran M) or not x in dom (Mx2Tran M) ) ;
suppose A1: x in dom (Mx2Tran M) ; :: thesis: (Mx2Tran b3) . b4 is real-valued FinSequence
A2: rng (Mx2Tran M) c= the carrier of (TOP-REAL m) by RELAT_1:def 19;
(Mx2Tran M) . x in rng (Mx2Tran M) by A1, FUNCT_1:def 3;
hence (Mx2Tran M) . x is real-valued FinSequence by A2; :: thesis: verum
end;
suppose not x in dom (Mx2Tran M) ; :: thesis: (Mx2Tran b3) . b4 is real-valued FinSequence
hence (Mx2Tran M) . x is real-valued FinSequence by FUNCT_1:def 2; :: thesis: verum
end;
end;
end;

registration
let n, m be Nat;
let M be Matrix of n,m,F_Real;
let x be set ;
cluster (Mx2Tran M) . x -> Relation-like Function-like ;
coherence
( (Mx2Tran M) . x is Function-like & (Mx2Tran M) . x is Relation-like ) by Lm3;
cluster (Mx2Tran M) . x -> FinSequence-like real-valued ;
coherence
( (Mx2Tran M) . x is real-valued & (Mx2Tran M) . x is FinSequence-like ) by Lm3;
end;

registration
let n, m be Nat;
let M be Matrix of n,m,F_Real;
let f be n -element real-valued FinSequence;
cluster (Mx2Tran M) . f -> m -element ;
coherence
(Mx2Tran M) . f is m -element
proof end;
end;

theorem Th18: :: MATRTOP1:18
for i, m, n being Nat
for f being b3 -element real-valued FinSequence
for M being Matrix of n,m,F_Real st 1 <= i & i <= m & n <> 0 holds
((Mx2Tran M) . f) . i = (@ f) "*" (Col (M,i))
proof end;

theorem Th19: :: MATRTOP1:19
for n being Nat
for K being Field holds len (MX2FinS (1. (K,n))) = n
proof end;

theorem Th20: :: MATRTOP1:20
for n, m being Nat
for M being Matrix of n,m,F_Real
for Bn being OrdBasis of n -VectSp_over F_Real
for Bm being OrdBasis of m -VectSp_over F_Real st Bn = MX2FinS (1. (F_Real,n)) & Bm = MX2FinS (1. (F_Real,m)) holds
for M1 being Matrix of len Bn, len Bm,F_Real st M1 = M holds
Mx2Tran M = Mx2Tran (M1,Bn,Bm)
proof end;

theorem :: MATRTOP1:21
for m, n being Nat
for f being b2 -element real-valued FinSequence
for M being Matrix of n,m,F_Real
for P being Permutation of (Seg n) holds
( (Mx2Tran M) . f = (Mx2Tran (M * P)) . (f * P) & f * P is b2 -element FinSequence of REAL )
proof end;

theorem Th22: :: MATRTOP1:22
for n, m being Nat
for f1, f2 being b1 -element real-valued FinSequence
for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (f1 + f2) = ((Mx2Tran M) . f1) + ((Mx2Tran M) . f2)
proof end;

theorem Th23: :: MATRTOP1:23
for n, m being Nat
for r being real number
for f being b1 -element real-valued FinSequence
for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (r * f) = r * ((Mx2Tran M) . f)
proof end;

theorem Th24: :: MATRTOP1:24
for n, m being Nat
for f1, f2 being b1 -element real-valued FinSequence
for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (f1 - f2) = ((Mx2Tran M) . f1) - ((Mx2Tran M) . f2)
proof end;

theorem :: MATRTOP1:25
for n, m being Nat
for f being b1 -element real-valued FinSequence
for M1, M2 being Matrix of n,m,F_Real holds (Mx2Tran (M1 + M2)) . f = ((Mx2Tran M1) . f) + ((Mx2Tran M2) . f)
proof end;

theorem :: MATRTOP1:26
for n, m being Nat
for r being real number
for R being Element of F_Real
for f being b1 -element real-valued FinSequence
for M being Matrix of n,m,F_Real st r = R holds
r * ((Mx2Tran M) . f) = (Mx2Tran (R * M)) . f
proof end;

theorem Th27: :: MATRTOP1:27
for n, m being Nat
for p1, p2 being Point of (TOP-REAL n)
for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (p1 + p2) = ((Mx2Tran M) . p1) + ((Mx2Tran M) . p2) by Th22;

theorem Th28: :: MATRTOP1:28
for n, m being Nat
for p1, p2 being Point of (TOP-REAL n)
for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (p1 - p2) = ((Mx2Tran M) . p1) - ((Mx2Tran M) . p2) by Th24;

theorem Th29: :: MATRTOP1:29
for n, m being Nat
for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (0. (TOP-REAL n)) = 0. (TOP-REAL m)
proof end;

theorem :: MATRTOP1:30
for m, n being Nat
for p being Point of (TOP-REAL n)
for M being Matrix of n,m,F_Real
for A being Subset of (TOP-REAL n) holds (Mx2Tran M) .: (p + A) = ((Mx2Tran M) . p) + ((Mx2Tran M) .: A)
proof end;

theorem :: MATRTOP1:31
for n, m being Nat
for p being Point of (TOP-REAL n)
for M being Matrix of n,m,F_Real
for A being Subset of (TOP-REAL m) holds (Mx2Tran M) " (((Mx2Tran M) . p) + A) = p + ((Mx2Tran M) " A)
proof end;

theorem Th32: :: MATRTOP1:32
for n, m, k being Nat
for A being Matrix of n,m,F_Real
for B being Matrix of width A,k,F_Real st ( n = 0 implies m = 0 ) & ( m = 0 implies k = 0 ) holds
(Mx2Tran B) * (Mx2Tran A) = Mx2Tran (A * B)
proof end;

theorem Th33: :: MATRTOP1:33
for n being Nat holds Mx2Tran (1. (F_Real,n)) = id (TOP-REAL n)
proof end;

theorem Th34: :: MATRTOP1:34
for n, m being Nat
for M1, M2 being Matrix of n,m,F_Real st Mx2Tran M1 = Mx2Tran M2 holds
M1 = M2
proof end;

theorem Th35: :: MATRTOP1:35
for n, m, k being Nat
for f being b1 -element real-valued FinSequence
for A being Matrix of n,m,F_Real
for B being Matrix of k,m,F_Real holds
( (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = (Mx2Tran A) . f & (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = (Mx2Tran A) . f )
proof end;

theorem :: MATRTOP1:36
for n, m, k being Nat
for f being b1 -element real-valued FinSequence
for A being Matrix of n,m,F_Real
for B being Matrix of k,m,F_Real
for g being b3 -element real-valued FinSequence holds (Mx2Tran (A ^ B)) . (f ^ g) = ((Mx2Tran A) . f) + ((Mx2Tran B) . g)
proof end;

theorem :: MATRTOP1:37
for n, k, m being Nat
for f being b1 -element real-valued FinSequence
for A being Matrix of n,k,F_Real
for B being Matrix of n,m,F_Real st ( n = 0 implies k + m = 0 ) holds
(Mx2Tran (A ^^ B)) . f = ((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)
proof end;

theorem :: MATRTOP1:38
for m, n being Nat
for f being b2 -element real-valued FinSequence
for M being Matrix of n,m,F_Real st M = (1. (F_Real,m)) | n holds
((Mx2Tran M) . f) | n = f
proof end;

begin

theorem Th39: :: MATRTOP1:39
for m, n being Nat
for M being Matrix of n,m,F_Real holds
( Mx2Tran M is one-to-one iff the_rank_of M = n )
proof end;

theorem Th40: :: MATRTOP1:40
for n being Nat
for A being Matrix of n,F_Real holds
( Mx2Tran A is one-to-one iff Det A <> 0. F_Real )
proof end;

theorem Th41: :: MATRTOP1:41
for n, m being Nat
for M being Matrix of n,m,F_Real holds
( Mx2Tran M is onto iff the_rank_of M = m )
proof end;

theorem Th42: :: MATRTOP1:42
for n being Nat
for A being Matrix of n,F_Real holds
( Mx2Tran A is onto iff Det A <> 0. F_Real )
proof end;

theorem Th43: :: MATRTOP1:43
for n being Nat
for A, B being Matrix of n,F_Real st Det A <> 0. F_Real holds
( (Mx2Tran A) " = Mx2Tran B iff A ~ = B )
proof end;

Lm4: for n, m being Nat
for M being Matrix of n,m,F_Real
for f being b1 -element real-valued FinSequence ex L being b2 -element FinSequence of REAL st
( |.((Mx2Tran M) . f).| <= (Sum L) * |.f.| & ( for i being Nat st i in dom L holds
L . i = |.(@ (Col (M,i))).| ) )
proof end;

theorem Th44: :: MATRTOP1:44
for m, n being Nat
for M being Matrix of n,m,F_Real ex L being b1 -element FinSequence of REAL st
( ( for i being Nat st i in dom L holds
L . i = |.(@ (Col (M,i))).| ) & ( for f being b2 -element real-valued FinSequence holds |.((Mx2Tran M) . f).| <= (Sum L) * |.f.| ) )
proof end;

theorem Th45: :: MATRTOP1:45
for m, n being Nat
for M being Matrix of n,m,F_Real ex L being Real st
( L > 0 & ( for f being b2 -element real-valued FinSequence holds |.((Mx2Tran M) . f).| <= L * |.f.| ) )
proof end;

theorem :: MATRTOP1:46
for m, n being Nat
for M being Matrix of n,m,F_Real st the_rank_of M = n holds
ex L being Real st
( L > 0 & ( for f being b2 -element real-valued FinSequence holds |.f.| <= L * |.((Mx2Tran M) . f).| ) )
proof end;

theorem Th47: :: MATRTOP1:47
for n, m being Nat
for M being Matrix of n,m,F_Real holds Mx2Tran M is continuous
proof end;

registration
let n be Nat;
let K be Field;
cluster Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like tabular invertible for Matrix of n,n, the carrier of K;
existence
ex b1 being Matrix of n,K st b1 is invertible
proof end;
end;

registration
let n be Nat;
let A be invertible Matrix of n,F_Real;
cluster Mx2Tran A -> being_homeomorphism ;
coherence
Mx2Tran A is being_homeomorphism
proof end;
end;