:: Linear Transformations of Euclidean Topological Spaces. Part {II}
::  by Karol P\kak
::
:: Received October 26, 2010
:: Copyright (c) 2010-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies ALGSTR_0, ARYTM_1, ARYTM_3, CARD_1, CARD_3, CLASSES1, ENTROPY1,
      EUCLID, FINSEQ_1, FINSEQ_2, FINSEQ_4, FINSET_1, FUNCT_1, FUNCT_2,
      FVSUM_1, INCSP_1, LMOD_7, MATRIX_1, MATRIX_3, MATRIX13, MATRLIN,
      MATRLIN2, MESFUNC1, NAT_1, NUMBERS, ORDINAL4, PARTFUN1, PBOOLE, PRE_TOPC,
      PRVECT_1, QC_LANG1, RANKNULL, RELAT_1, RLAFFIN1, RLSUB_1, RLVECT_1,
      RLVECT_2, RLVECT_3, RLVECT_5, RVSUM_1, SEMI_AF1, STRUCT_0, SUBSET_1,
      SUPINF_2, TARSKI, TREES_1, VALUED_0, VALUED_1, VECTSP_1, VECTSP10,
      XBOOLE_0, XXREAL_0, FUNCT_7;
 notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, CARD_1, ORDINAL1, NUMBERS,
      XCMPLX_0, XXREAL_0, FINSET_1, FUNCT_1, RELSET_1, PARTFUN1, NAT_1,
      VALUED_0, FUNCT_2, FINSEQ_1, FINSEQ_2, FINSEQ_3, STRUCT_0, RLVECT_1,
      RLVECT_2, RLVECT_3, VECTSP_1, MATRIX_0, MATRIX_1, MATRIX_3, VECTSP_4,
      VECTSP_6, VECTSP_7, MATRIX13, RVSUM_1, ALGSTR_0, FVSUM_1, RANKNULL,
      PRE_TOPC, MATRIX_6, MATRLIN, MATRLIN2, NAT_D, EUCLID, GROUP_1, MATRIX11,
      FINSEQOP, ENTROPY1, RLSUB_1, RUSUB_4, PRVECT_1, RLAFFIN1, MATRTOP1;
 constructors BINARITH, ENTROPY1, FVSUM_1, LAPLACE, MATRIX_6, MATRIX11,
      MATRIX13, MATRLIN2, MATRTOP1, MONOID_0, RANKNULL, REALSET1, RELSET_1,
      RLAFFIN1, RLVECT_3, RUSUB_5, VECTSP10, MATRIX15, MATRIX_1, MATRIX_4,
      FUNCSDOM, PCOMPS_1, SQUARE_1, BINOP_2;
 registrations CARD_1, EUCLID, FINSEQ_1, FINSEQ_2, FINSET_1, FUNCT_1, FUNCT_2,
      MATRIX13, MATRLIN2, MATRTOP1, MEMBERED, MONOID_0, NAT_1, NUMBERS,
      PRVECT_1, RELAT_1, RELSET_1, RLAFFIN1, RLVECT_3, RVSUM_1, STRUCT_0,
      RLVECT_2, VALUED_0, VECTSP_1, VECTSP_9, XREAL_0, XXREAL_0, MATRIX_6,
      ORDINAL1;
 requirements ARITHM, NUMERALS, REAL, BOOLE, SUBSET;


begin :: Correspondence Between Euclidean Topological Space and Vector
      :: Space over F_Real

reserve X for set,
        n,m,k for Nat,
        K for Field,
        f for n-element real-valued FinSequence,
        M for Matrix of n,m,F_Real;

theorem :: MATRTOP2:1
  X is Linear_Combination of n-VectSp_over F_Real
iff
  X is Linear_Combination of TOP-REAL n;

theorem :: MATRTOP2:2
  for Lv be Linear_Combination of n-VectSp_over F_Real,
      Lr be Linear_Combination of TOP-REAL n st Lr = Lv
  holds Carrier Lr = Carrier Lv;

theorem :: MATRTOP2:3
  for F be FinSequence of TOP-REAL n,
      fr be Function of TOP-REAL n,REAL,
      Fv be FinSequence of n-VectSp_over F_Real,
      fv be Function of n-VectSp_over F_Real,F_Real st fr = fv & F = Fv
  holds fr(#)F = fv(#)Fv;

theorem :: MATRTOP2:4
  for F be FinSequence of TOP-REAL n,
      Fv be FinSequence of n-VectSp_over F_Real st Fv = F
  holds Sum F = Sum Fv;

theorem :: MATRTOP2:5
  for Lv be Linear_Combination of n-VectSp_over F_Real,
      Lr be Linear_Combination of TOP-REAL n st Lr = Lv
  holds Sum Lr = Sum Lv;

theorem :: MATRTOP2:6
  for Af be Subset of n-VectSp_over F_Real,
      Ar be Subset of TOP-REAL n st Af = Ar
  holds [#]Lin Ar = [#]Lin Af;

theorem :: MATRTOP2:7
  for Af be Subset of n-VectSp_over F_Real,
      Ar be Subset of TOP-REAL n st Af = Ar
  holds
    Af is linearly-independent
  iff
    Ar is linearly-independent;

theorem :: MATRTOP2:8
  for V be VectSp of K, W be Subspace of V, L be Linear_Combination of V
  holds L|the carrier of W is Linear_Combination of W;

theorem :: MATRTOP2:9
  for V be VectSp of K, A be linearly-independent Subset of V
  for L1,L2 be Linear_Combination of V st
     Carrier L1 c= A & Carrier L2 c= A & Sum L1 = Sum L2
  holds L1 = L2;

theorem :: MATRTOP2:10
  for V be RealLinearSpace, W be Subspace of V
  for L be Linear_Combination of V
  holds L|the carrier of W is Linear_Combination of W;

theorem :: MATRTOP2:11
  for U be Subspace of n-VectSp_over F_Real,
      W be Subspace of TOP-REAL n st [#]U = [#]W
  holds
    X is Linear_Combination of U
  iff
    X is Linear_Combination of W;

theorem :: MATRTOP2:12
  for U be Subspace of n-VectSp_over F_Real, W be Subspace of TOP-REAL n
  for LU be Linear_Combination of U, LW be Linear_Combination of W st LU = LW
  holds Carrier LU = Carrier LW & Sum LU = Sum LW;

registration
  let m,K;
  let A be Subset of m-VectSp_over K;
  cluster Lin A -> finite-dimensional;
end;

begin :: Correspondence Between the Mx2Tran Operator and Decomposition of
      :: a Vector in Basis

theorem :: MATRTOP2:13
  the_rank_of M = n implies M is OrdBasis of Lin lines M;

theorem :: MATRTOP2:14
  for V,W be VectSp of K
  for T be linear-transformation of V,W
  for A be Subset of V for L be Linear_Combination of A st T|A is one-to-one
  holds T.(Sum L) = Sum (T@L);

theorem :: MATRTOP2:15
  for S be Subset of Seg n st M|S is one-to-one & rng(M|S) = lines M
  ex L be Linear_Combination of lines M st
    Sum L = (Mx2Tran M).f &
    for k st k in S holds L.Line(M,k) = Sum Seq(f|M"{Line(M,k)});

theorem :: MATRTOP2:16
  M is without_repeated_line implies
  ex L be Linear_Combination of lines M st
    Sum L=(Mx2Tran M).f &
    for k st k in dom f holds L.Line(M,k)=f.k;

theorem :: MATRTOP2:17
  for B be OrdBasis of Lin lines M st B = M
  for Mf be Element of Lin lines M st Mf = (Mx2Tran M).f holds Mf|--B = f;

theorem :: MATRTOP2:18
  rng(Mx2Tran M) = [#]Lin lines M;

theorem :: MATRTOP2:19
  for F be one-to-one FinSequence of TOP-REAL n st
    rng F is linearly-independent
  ex M be Matrix of n,F_Real st M is invertible & M|len F = F;

theorem :: MATRTOP2:20
  for B be 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);

theorem :: MATRTOP2:21
  for F be one-to-one FinSequence of TOP-REAL n st
    rng F is linearly-independent
  for B be OrdBasis of n-VectSp_over F_Real st B = MX2FinS 1.(F_Real,n)
  for M be Matrix of n,F_Real st M is invertible & M|len F = F
  holds (Mx2Tran M).:[#]Lin rng(B|len F) = [#]Lin rng F;

theorem :: MATRTOP2:22
  for A,B be linearly-independent Subset of TOP-REAL n st card A = card B
  ex M be Matrix of n,F_Real st
   M is invertible & (Mx2Tran M).:[#]Lin A = [#]Lin B;

begin :: Preservation of Linear and Affine Independence of Vectors by the
      :: Mx2Tran Operator

theorem :: MATRTOP2:23
  for A be linearly-independent Subset of TOP-REAL n st the_rank_of M = n
  holds (Mx2Tran M).:A is linearly-independent;

theorem :: MATRTOP2:24
  for A be affinely-independent Subset of TOP-REAL n st the_rank_of M = n
  holds (Mx2Tran M).:A is affinely-independent;

theorem :: MATRTOP2:25
  for A be affinely-independent Subset of TOP-REAL n st the_rank_of M = n
  for v be Element of TOP-REAL n st v in Affin A holds
   (Mx2Tran M).v in Affin(Mx2Tran M).:A &
   for f holds (v|--A).f = ((Mx2Tran M).v|--(Mx2Tran M).:A).((Mx2Tran M).f);

theorem :: MATRTOP2:26
  for A be linearly-independent Subset of TOP-REAL m st the_rank_of M = n
  holds (Mx2Tran M)"A is linearly-independent;

theorem :: MATRTOP2:27
  for A be affinely-independent Subset of TOP-REAL m st the_rank_of M = n
  holds (Mx2Tran M)"A is affinely-independent;