:: Linear Transformations of Euclidean Topological Spaces
:: by Karol P\kak
::
:: Copyright (c) 2010-2021 Association of Mizar Users

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

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

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

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

registration
let rf be real-valued FinSequence;
coherence
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 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;
coherence ;
end;

registration
let rf be real-valued FinSubsequence;
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 f1, f2, g1, g2 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 () 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 ()

proof end;

:: 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 (),() 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. ();
existence
( ( n <> 0 implies ex b1 being Function of (),() 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 (),() st
for f being n -element real-valued FinSequence holds b1 . f = 0. () ) )
proof end;
uniqueness
for b1, b2 being Function of (),() 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. () ) & ( for f being n -element real-valued FinSequence holds b2 . f = 0. () ) implies b1 = b2 ) )
proof end;
correctness
consistency
for b1 being Function of (),() 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 (),() 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. () ) ) );

Lm3: now :: thesis: for n, m being Nat
for M being Matrix of n,m,F_Real
for x being object holds () . x is real-valued FinSequence
let n, m be Nat; :: thesis: for M being Matrix of n,m,F_Real
for x being object holds (Mx2Tran b5) . b6 is real-valued FinSequence

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

registration
let n, m be Nat;
let M be Matrix of n,m,F_Real;
let x be object ;
coherence
( () . x is Function-like & () . x is Relation-like )
by Lm3;
end;

registration
let n, m be Nat;
let M be Matrix of n,m,F_Real;
let x be object ;
coherence
( () . x is real-valued & () . 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 () . f -> m -element ;
coherence
() . f is m -element
proof end;
end;

theorem Th18: :: MATRTOP1:18
for n, m, i being Nat
for f being b1 -element real-valued FinSequence
for M being Matrix of n,m,F_Real st 1 <= i & i <= m & n <> 0 holds
(() . 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 n, m being Nat
for f being b1 -element real-valued FinSequence
for M being Matrix of n,m,F_Real
for P being Permutation of (Seg n) holds
( () . f = (Mx2Tran (M * P)) . (f * P) & f * P is b1 -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 () . (f1 + f2) = (() . f1) + (() . f2)
proof end;

reconsider zz = 0 as Real ;

theorem Th23: :: MATRTOP1:23
for n, m being Nat
for r being Real
for f being b1 -element real-valued FinSequence
for M being Matrix of n,m,F_Real holds () . (r * f) = r * (() . 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 () . (f1 - f2) = (() . f1) - (() . 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
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 * (() . f) = (Mx2Tran (R * M)) . f
proof end;

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

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

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

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

theorem :: MATRTOP1:31
for n, m being Nat
for p being Point of ()
for M being Matrix of n,m,F_Real
for A being Subset of () holds () " ((() . p) + A) = p + (() " 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 (A * B)
proof end;

theorem Th33: :: MATRTOP1:33
for n being Nat holds Mx2Tran (1. (F_Real,n)) = id ()
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)) = () . f & (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = () . 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) = (() . f) + (() . g)
proof end;

theorem :: MATRTOP1:37
for n, m, k 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 = (() . f) ^ (() . f)
proof end;

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

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

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

reconsider jj = 1 as Real ;

theorem :: MATRTOP1:46
for n, m 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 b1 -element real-valued FinSequence holds |.f.| <= L * |.(() . 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;
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;
coherence
proof end;
end;