:: by Karol P\kak

::

:: Received October 26, 2010

:: Copyright (c) 2010-2021 Association of Mizar Users

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

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 )

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

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

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

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

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)

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 )

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

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

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

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 )

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 )

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

coherence

Lin A is finite-dimensional ;

end;
let K be Field;

let A be Subset of (m -VectSp_over K);

coherence

Lin A is finite-dimensional ;

Lm4: for n, m being Nat

for M being Matrix of n,m,F_Real holds lines M c= [#] (Lin (lines M))

proof end;

:: a Vector in Basis

theorem :: MATRTOP2:13

for n, m 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)

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)

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 n, m being Nat

for f being b

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 n, m being Nat

for f being b_{1} -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))}))) ) )

for f being b

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_{1} -element real-valued FinSequence

for M being Matrix of n,m,F_Real st M is without_repeated_line 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 ) )

for f being b

for M being Matrix of n,m,F_Real st M is without_repeated_line 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_{1} -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

for f being b

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

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_{1} -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) )

for f being b

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

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

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;

:: Mx2Tran Operator

theorem Th23: :: MATRTOP2:23

for n, m 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

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 n, m 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

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 n, m 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_{1} -element real-valued FinSequence holds (v |-- A) . f = (((Mx2Tran M) . v) |-- ((Mx2Tran M) .: A)) . ((Mx2Tran M) . f) ) )

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

proof end;

theorem Th26: :: MATRTOP2:26

for n, m 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

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 n, m 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

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;