:: 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;
clusterF | Y ->  positive-yielding ;
coherence
 F | Y is positive-yielding
proofend;
end;

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

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

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

registration
let rf be real-valued FinSequence;
cluster sqrt rf ->  FinSequence-like ;
coherence
 sqrt rf is FinSequence-like
proofend;
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
proofend;
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)
proofend;

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

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

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

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

registration
let cf be complex-valued FinSequence;
let X be set ;
clustercf - X ->  complex-valued ;
coherence
 cf - X is complex-valued
proofend;
end;

registration
let rf be real-valued FinSequence;
let X be set ;
clusterrf - X ->  real-valued ;
coherence
 rf - X is real-valued
proofend;
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
proofend;

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)
proofend;

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
proofend;

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)))
proofend;

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)
proofend;

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)) &amp; ( for n being Nat st n > 0 holds
( n in Y iff n + (len f1) in X /\ (dom (f1 ^ f2)) ) ) )
proofend;

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

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
proofend;

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
proofend;

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

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
proofend;

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
proofend;

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

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) ) &amp; ( 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) ) )
proofend;
uniqueness
 for b1, b2 being Function of (TOP-REAL n),(TOP-REAL m) holds
( ( n <> 0 &amp; ( for f being n -element real-valued FinSequence holds b1 . f = Line (((LineVec2Mx (@ f)) * M),1) ) &amp; ( for f being n -element real-valued FinSequence holds b2 . f = Line (((LineVec2Mx (@ f)) * M),1) ) implies b1 = b2 ) &amp; ( not n <> 0 &amp; ( for f being n -element real-valued FinSequence holds b1 . f = 0. (TOP-REAL m) ) &amp; ( for f being n -element real-valued FinSequence holds b2 . f = 0. (TOP-REAL m) ) implies b1 = b2 ) )
proofend;
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) ) ) &amp; ( 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;
percases ( x in dom (Mx2Tran M) or not x in dom (Mx2Tran M) ) ;
supposeA1: 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 &amp; (Mx2Tran M) . x is Relation-like ) by Lm3;
cluster(Mx2Tran M) . x ->  FinSequence-like real-valued ;
coherence
 ( (Mx2Tran M) . x is real-valued &amp; (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
proofend;
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 &amp; i <= m &amp; n <> 0 holds
((Mx2Tran M) . f) . i = (@ f) "*" (Col (M,i))
proofend;

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

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)) &amp; 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)
proofend;

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) &amp; f * P is b2 -element FinSequence of REAL )
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

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
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

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 ) &amp; ( m = 0 implies k = 0 ) holds
(Mx2Tran B) * (Mx2Tran A) = Mx2Tran (A * B)
proofend;

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

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
proofend;

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 &amp; (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = (Mx2Tran A) . f )
proofend;

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)
proofend;

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)
proofend;

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
proofend;

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 )
proofend;

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 )
proofend;

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 )
proofend;

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 )
proofend;

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 )
proofend;

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.| &amp; ( for i being Nat st i in dom L holds
L . i = |.(@ (Col (M,i))).| ) )
proofend;

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))).| ) &amp; ( for f being b2 -element real-valued FinSequence holds |.((Mx2Tran M) . f).| <= (Sum L) * |.f.| ) )
proofend;

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 &amp; ( for f being b2 -element real-valued FinSequence holds |.((Mx2Tran M) . f).| <= L * |.f.| ) )
proofend;

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 &amp; ( for f being b2 -element real-valued FinSequence holds |.f.| <= L * |.((Mx2Tran M) . f).| ) )
proofend;

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

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