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

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 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 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 (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 b₁ -element real-valued FinSequence holds f is Point of (TOP-REAL n)

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 (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 b₁ being Function of (TOP-REAL n),(TOP-REAL m) st
for f being n -element real-valued FinSequence holds b₁ . f = Line (((LineVec2Mx (@ f)) * M),1) ) & ( not n <> 0 implies ex b₁ being Function of (TOP-REAL n),(TOP-REAL m) st
for f being n -element real-valued FinSequence holds b₁ . f = 0. (TOP-REAL m) ) )

proof end;

uniqueness
for b₁, b₂ being Function of (TOP-REAL n),(TOP-REAL m) holds
( ( n <> 0 & ( for f being n -element real-valued FinSequence holds b₁ . f = Line (((LineVec2Mx (@ f)) * M),1) ) & ( for f being n -element real-valued FinSequence holds b₂ . f = Line (((LineVec2Mx (@ f)) * M),1) ) implies b₁ = b₂ ) & ( not n <> 0 & ( for f being n -element real-valued FinSequence holds b₁ . f = 0. (TOP-REAL m) ) & ( for f being n -element real-valued FinSequence holds b₂ . f = 0. (TOP-REAL m) ) implies b₁ = b₂ ) )

proof end;

correctness
consistency
for b₁ 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 b₄ being Function of (TOP-REAL n),(TOP-REAL m) holds
( ( n <> 0 implies ( b₄ = Mx2Tran M iff for f being b₁ -element real-valued FinSequence holds b₄ . f = Line (((LineVec2Mx (@ f)) * M),1) ) ) & ( not n <> 0 implies ( b₄ = Mx2Tran M iff for f being b₁ -element real-valued FinSequence holds b₄ . 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 object 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 object holds (Mx2Tran b₅) . b₆ is real-valued FinSequence
let M be Matrix of n,m,F_Real; :: thesis: for x being object holds (Mx2Tran b₄) . b₅ is real-valued FinSequence
let x be object ; :: thesis: (Mx2Tran b₃) . b₄ 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 b₃) . b₄ 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 b₃) . b₄ 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 object ;

cluster (Mx2Tran M) . x -> Relation-like Function-like ;

coherence
( (Mx2Tran M) . x is Function-like & (Mx2Tran M) . 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 ;

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 n, m, i being Nat
for f being b₁ -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 n, m being Nat
for f being b₁ -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 b₁ -element FinSequence of REAL )

proof end;

theorem Th22: :: MATRTOP1:22

for n, m being Nat
for f1, f2 being b₁ -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;

reconsider zz = 0 as Real ;

theorem Th23: :: MATRTOP1:23

for n, m being Nat
for r being Real
for f being b₁ -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 b₁ -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 b₁ -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 b₁ -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 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 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 b₁ -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 b₁ -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 b₃ -element real-valued FinSequence holds (Mx2Tran (A ^ B)) . (f ^ g) = ((Mx2Tran A) . f) + ((Mx2Tran B) . g)

proof end;

theorem :: MATRTOP1:37

for n, m, k being Nat
for f being b₁ -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 n, m being Nat
for f being b₁ -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;

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 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 b₁ -element real-valued FinSequence ex L being b₂ -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 n, m being Nat
for M being Matrix of n,m,F_Real ex L being b₂ -element FinSequence of REAL st
( ( for i being Nat st i in dom L holds
L . i = |.(@ (Col (M,i))).| ) & ( for f being b₁ -element real-valued FinSequence holds |.((Mx2Tran M) . 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 b₁ -element real-valued FinSequence holds |.((Mx2Tran M) . 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 b₁ -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 V145( the carrier of K,n,n) invertible for FinSequence of the carrier of K * ;

existence
ex b₁ being Matrix of n,K st b₁ 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;