:: Real Vector Space and Related Notions :: by Kazuhisa Nakasho , Hiroyuki Okazaki and Yasunari Shidama :: :: Received June 30, 2021 :: Copyright (c) 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, EUCLID, FINSEQ_1, FINSEQ_2, FINSEQ_4, FINSET_1, FUNCT_1, FUNCT_2, MATRIX_1, MATRIX13, MATRLIN, MATRLIN2, MESFUNC1, NAT_1, NUMBERS, PARTFUN1, PRE_TOPC, PRVECT_1, RANKNULL, RELAT_1, RLAFFIN1, RLSUB_1, RLVECT_1, RLVECT_2, RLVECT_3, RLVECT_5, SEMI_AF1, STRUCT_0, SUBSET_1, SUPINF_2, TARSKI, VALUED_0, VALUED_1, VECTSP_1, XBOOLE_0, XXREAL_0, REAL_NS1, FUNCSDOM, FUNCOP_1, ZFMISC_1, REAL_1, NORMSP_2, PCOMPS_1, METRIC_1, RUSUB_4, MATRIX_6, SETFAM_1, BINOP_2, MSSUBFAM, UNIALG_1, COMPLEX1, NORMSP_1, REALSET1, MATRIXR1, MATRIXR2, LOPBAN_1, DUALSP01; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1, REALSET1, FINSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, VALUED_0, BINOP_2, FINSEQ_1, FINSEQ_2, FINSEQOP, RVSUM_1, MATRIX_0, STRUCT_0, ALGSTR_0, PRE_TOPC, RLVECT_1, RLSUB_1, VECTSP_1, FUNCSDOM, RLVECT_2, METRIC_1, RLVECT_3, VECTSP_4, NORMSP_0, NORMSP_1, VECTSP_6, VECTSP_7, MATRIX_1, FVSUM_1, MATRLIN, PCOMPS_1, RLVECT_5, RUSUB_4, EUCLID, LOPBAN_1, VECTSP_9, RANKNULL, PRVECT_1, MATRIXR1, RLAFFIN1, MATRIX_6, MATRIXR2, MATRIX13, MATRLIN2, REAL_NS1, NORMSP_2, MATRTOP1, DUALSP01; constructors FVSUM_1, MATRIX_6, MATRIX13, MATRLIN2, MATRTOP1, MONOID_0, RANKNULL, REALSET1, RELSET_1, RLAFFIN1, RLVECT_3, RUSUB_5, VECTSP10, PCOMPS_1, BINOP_2, REAL_NS1, RLVECT_5, REAL_1, VECTSP_9, NORMSP_2, MATRIXR2, LOPBAN_1, DUALSP01, FINSOP_1; registrations CARD_1, EUCLID, FINSEQ_1, FINSEQ_2, FINSET_1, FUNCT_1, FUNCT_2, MATRIX13, MATRLIN, MEMBERED, MONOID_0, NAT_1, NUMBERS, PRVECT_1, RELAT_1, RELSET_1, RLAFFIN1, RLVECT_3, RVSUM_1, STRUCT_0, VALUED_0, VECTSP_1, XREAL_0, ORDINAL1, REAL_NS1, RLVECT_5, RUSUB_4, XBOOLE_0, RLAFFIN3; requirements NUMERALS, BOOLE, SUBSET; begin :: Common properties between norm and topology :: in finite dimensional linear spaces 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 :: REAL_NS2:1 the RLSStruct of TOP-REAL n = the RLSStruct of REAL-NS n; theorem :: REAL_NS2:2 Euclid n = MetricSpaceNorm REAL-NS n; theorem :: REAL_NS2:3 the TopStruct of TOP-REAL n = TopSpaceNorm REAL-NS n; theorem :: REAL_NS2:4 the carrier of TOP-REAL n = the carrier of REAL-NS n; theorem :: REAL_NS2:5 the carrier of (n -VectSp_over F_Real) = the carrier of REAL-NS n; theorem :: REAL_NS2:6 0.(TOP-REAL n) = 0.(REAL-NS n); theorem :: REAL_NS2:7 for p,q be Element of TOP-REAL n, f,g be Element of REAL-NS n st p=f & q=g holds p+q = f+g; theorem :: REAL_NS2:8 for r be Real, q be Element of TOP-REAL n, g be Element of REAL-NS n st q = g holds r*q = r*g; theorem :: REAL_NS2:9 for q be Element of TOP-REAL n, g be Element of REAL-NS n st q = g holds -q = -g; theorem :: REAL_NS2:10 for p,q be Element of TOP-REAL n, f,g be Element of REAL-NS n st p = f & q = g holds p-q = f-g; theorem :: REAL_NS2:11 for X be set for n be Nat holds X is Linear_Combination of REAL-NS n iff X is Linear_Combination of TOP-REAL n; theorem :: REAL_NS2:12 for X be set for n be Nat holds X is Linear_Combination of REAL-NS n iff X is Linear_Combination of n-VectSp_over F_Real; theorem :: REAL_NS2:13 for Lv be Linear_Combination of TOP-REAL n, Lr be Linear_Combination of REAL-NS n st Lr = Lv holds Carrier Lr = Carrier Lv; theorem :: REAL_NS2:14 for Lv be Linear_Combination of n-VectSp_over F_Real, Lr be Linear_Combination of REAL-NS n st Lr = Lv holds Carrier Lr = Carrier Lv; theorem :: REAL_NS2:15 for F be set holds F is Subset of TOP-REAL n iff F is Subset of REAL-NS n; theorem :: REAL_NS2:16 for F be set holds F is Subset of REAL-NS n iff F is Subset of n-VectSp_over F_Real; theorem :: REAL_NS2:17 for F be set holds F is FinSequence of TOP-REAL n iff F is FinSequence of REAL-NS n; theorem :: REAL_NS2:18 for F be set holds F is Function of TOP-REAL n, REAL iff F is Function of REAL-NS n, REAL; theorem :: REAL_NS2:19 for Fr be FinSequence of TOP-REAL n, fr be Function of TOP-REAL n,REAL, Fv be FinSequence of REAL-NS n, fv be Function of REAL-NS n,REAL st fr = fv & Fr = Fv holds fr(#)Fr = fv(#)Fv; theorem :: REAL_NS2:20 for F be FinSequence of REAL-NS n, fr be Function of REAL-NS 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 :: REAL_NS2:21 for Ft be FinSequence of TOP-REAL n, Fr be FinSequence of REAL-NS n st Ft = Fr holds Sum Ft = Sum Fr; theorem :: REAL_NS2:22 for F be FinSequence of REAL-NS n, Fv be FinSequence of n-VectSp_over F_Real st Fv = F holds Sum F = Sum Fv; theorem :: REAL_NS2:23 for Lr be Linear_Combination of REAL-NS n, Lt be Linear_Combination of TOP-REAL n st Lr = Lt holds Sum Lr = Sum Lt; theorem :: REAL_NS2:24 for Lv be Linear_Combination of n-VectSp_over F_Real, Lr be Linear_Combination of REAL-NS n st Lr = Lv holds Sum Lr = Sum Lv; theorem :: REAL_NS2:25 for Ar be Subset of REAL-NS n, At be Subset of TOP-REAL n st Ar = At holds for X be object holds X is Linear_Combination of Ar iff X is Linear_Combination of At; theorem :: REAL_NS2:26 for Ar be Subset of REAL-NS n, At be Subset of TOP-REAL n st Ar = At holds [#]Lin Ar = [#]Lin At; theorem :: REAL_NS2:27 for Af be Subset of n-VectSp_over F_Real, Ar be Subset of REAL-NS n st Af = Ar holds [#]Lin Ar = [#]Lin Af; theorem :: REAL_NS2:28 for Ar be Subset of REAL-NS n, At be Subset of TOP-REAL n st Ar = At holds Ar is linearly-independent iff At is linearly-independent; theorem :: REAL_NS2:29 for Af be Subset of n-VectSp_over F_Real, Ar be Subset of REAL-NS n st Af = Ar holds Af is linearly-independent iff Ar is linearly-independent; theorem :: REAL_NS2:30 for X be object holds X is Subspace of REAL-NS n iff X is Subspace of TOP-REAL n; theorem :: REAL_NS2:31 for X be set, U be Subspace of REAL-NS n, W be Subspace of n -VectSp_over F_Real st [#] U = [#] W holds X is Linear_Combination of U iff X is Linear_Combination of W; theorem :: REAL_NS2:32 for F be one-to-one FinSequence of REAL-NS n st rng F is linearly-independent holds ex M be Matrix of n,F_Real st M is invertible & M | len F = F; theorem :: REAL_NS2:33 for M be Matrix of n,F_Real for N be Matrix of n,REAL st N = MXF2MXR M holds M is invertible iff N is invertible; theorem :: REAL_NS2:34 for M be Matrix of n,REAL holds M is invertible iff MXR2MXF M is invertible; theorem :: REAL_NS2:35 for F be one-to-one FinSequence of REAL-NS n st rng F is linearly-independent holds ex M be Matrix of n,REAL st M is invertible & M | len F = F; theorem :: REAL_NS2:36 for F be one-to-one FinSequence of REAL-NS n st rng F is linearly-independent holds for B be OrdBasis of n -VectSp_over F_Real st B = MX2FinS(1. (F_Real,n)) holds 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 :: REAL_NS2:37 for A,B be linearly-independent Subset of REAL-NS n st card A = card B holds ex M be Matrix of n,F_Real st M is invertible & (Mx2Tran M) .: ([#] (Lin A)) = [#] (Lin B); theorem :: REAL_NS2:38 for n, m be Nat for M be Matrix of n,m,F_Real for A be linearly-independent Subset of REAL-NS n st the_rank_of M = n holds (Mx2Tran M) .: A is linearly-independent; theorem :: REAL_NS2:39 for p be Element of TOP-REAL n, f be Element of REAL-NS n, H be Subset of TOP-REAL n, I be Subset of REAL-NS n st p = f & H = I holds p + H = f + I; theorem :: REAL_NS2:40 for Ar be Subset of REAL-NS n, At be Subset of TOP-REAL n st Ar = At holds Ar is Affine iff At is Affine; theorem :: REAL_NS2:41 for X be set holds X is affinely-independent Subset of REAL-NS n iff X is affinely-independent Subset of TOP-REAL n; theorem :: REAL_NS2:42 for n, m be Nat for M be Matrix of n,m,F_Real for A be affinely-independent Subset of REAL-NS n st the_rank_of M = n holds (Mx2Tran M) .: A is affinely-independent; theorem :: REAL_NS2:43 for Ar be Subset of REAL-NS n, At be Subset of TOP-REAL n st Ar = At holds Affin Ar = Affin At; theorem :: REAL_NS2:44 for L be Linear_Combination of REAL-NS n, S be Linear_Combination of TOP-REAL n st L = S holds sum L = sum S; theorem :: REAL_NS2:45 for Ar be Subset of REAL-NS n, At be Subset of TOP-REAL n, v be Element of REAL-NS n, w be Element of TOP-REAL n st Ar = At & v = w & v in Affin Ar & Ar is affinely-independent holds v |-- Ar = w |-- At; theorem :: REAL_NS2:46 for n, m be Nat for M be Matrix of n,m,F_Real for A be affinely-independent Subset of REAL-NS n st the_rank_of M = n holds for v be Element of REAL-NS n st v in Affin A holds (Mx2Tran M).v in Affin((Mx2Tran M) .: A) & (for f be n -element real-valued FinSequence holds (v |-- A).f = (((Mx2Tran M).v) |-- ((Mx2Tran M) .: A)) . ((Mx2Tran M).f)); theorem :: REAL_NS2:47 for n, m be Nat for M be Matrix of n,m,F_Real for A be linearly-independent Subset of REAL-NS m st the_rank_of M = n holds (Mx2Tran M) " A is linearly-independent; theorem :: REAL_NS2:48 for n, m be Nat for M be Matrix of n,m,F_Real for A be affinely-independent Subset of REAL-NS m st the_rank_of M = n holds (Mx2Tran M) " A is affinely-independent; theorem :: REAL_NS2:49 for V be RealLinearSpace, W be strict Subspace of V holds W is strict Subspace of (Omega). V; theorem :: REAL_NS2:50 for X be set holds X is Basis of n -VectSp_over F_Real iff X is Basis of TOP-REAL n; theorem :: REAL_NS2:51 for n be non empty Nat holds RealFuncAdd Seg n = product(the addF of F_Real,n); theorem :: REAL_NS2:52 for n be non empty Nat holds RealFuncExtMult(Seg n) = n -Mult_over F_Real; theorem :: REAL_NS2:53 ::: see also RLAFFIN3:4, not really used here TOP-REAL n is finite-dimensional & dim TOP-REAL n = n; theorem :: REAL_NS2:54 for n be non empty Nat holds the carrier of (TOP-REAL n) = the carrier of (n -VectSp_over F_Real) & 0. (TOP-REAL n) = 0. (n -VectSp_over F_Real) & the addF of (TOP-REAL n) = the addF of (n -VectSp_over F_Real) & the Mult of (TOP-REAL n) = the lmult of (n -VectSp_over F_Real); theorem :: REAL_NS2:55 for n be non empty Nat, xv, yv be Element of n -VectSp_over F_Real, xt, yt be Element of TOP-REAL n st xv = xt & yv = yt holds xv + yv = xt + yt; theorem :: REAL_NS2:56 for n be non empty Nat, af be Element of F_Real, at be Real, xv be Element of n -VectSp_over F_Real, xt be Element of TOP-REAL n st af = at & xv = xt holds af * xv = at * xt; theorem :: REAL_NS2:57 for n be non empty Nat, xv be Element of n -VectSp_over F_Real, xt be Element of TOP-REAL n st xv = xt holds -xv = -xt; theorem :: REAL_NS2:58 for n be non empty Nat, xv, yv be Element of n -VectSp_over F_Real, xt, yt be Element of TOP-REAL n st xv = xt & yv = yt holds xv - yv = xt - yt; theorem :: REAL_NS2:59 for n be non empty Nat for At be Subset of TOP-REAL n, Ar be Subset of n -VectSp_over F_Real st At = Ar holds the carrier of Lin At = the carrier of (Lin Ar) & 0.(Lin At) = 0.(Lin Ar) & the addF of Lin At = the addF of (Lin Ar) & the Mult of Lin At = the lmult of (Lin Ar); theorem :: REAL_NS2:60 for At be Subset of TOP-REAL n, Ar be Subset of REAL-NS n st At = Ar holds Lin At = Lin Ar; theorem :: REAL_NS2:61 for X be set holds X is Basis of TOP-REAL n iff X is Basis of REAL-NS n; theorem :: REAL_NS2:62 REAL-NS n is finite-dimensional & dim (REAL-NS n) = n; begin :: Finite dimensional vector spaces over real field registration cluster finite-dimensional for RealNormSpace; end; theorem :: REAL_NS2:63 for K be Field, V be finite-dimensional VectSp of K, b be OrdBasis of V holds ex T be linear-transformation of V, (dim V) -VectSp_over K st T is bijective & for x be Element of V holds T.x = x |-- b; theorem :: REAL_NS2:64 for K be Field, V be finite-dimensional VectSp of K ex T be linear-transformation of V, (dim V) -VectSp_over K st T is bijective; theorem :: REAL_NS2:65 for K be Field, V,W be finite-dimensional VectSp of K holds dim V = dim W iff ex T be linear-transformation of V, W st T is bijective; theorem :: REAL_NS2:66 for X be RealLinearSpace holds the carrier of X = the carrier of (RLSp2RVSp X) & the ZeroF of X = the ZeroF of (RLSp2RVSp X) & the addF of X = the addF of (RLSp2RVSp X) & the Mult of X = the lmult of (RLSp2RVSp X); theorem :: REAL_NS2:67 for X be strict RealLinearSpace holds RVSp2RLSp RLSp2RVSp X = X; theorem :: REAL_NS2:68 for X be strict VectSp of F_Real holds RLSp2RVSp RVSp2RLSp X = X; theorem :: REAL_NS2:69 for V be RealLinearSpace, F be set holds F is Subset of V iff F is Subset of RLSp2RVSp(V); theorem :: REAL_NS2:70 for V be RealLinearSpace, F be set holds F is FinSequence of V iff F is FinSequence of RLSp2RVSp(V); theorem :: REAL_NS2:71 for V be RealLinearSpace, F be set holds F is Function of V,REAL iff F is Function of RLSp2RVSp(V),REAL; theorem :: REAL_NS2:72 for T be RealLinearSpace, X be set holds X is Linear_Combination of RLSp2RVSp(T) iff X is Linear_Combination of T; theorem :: REAL_NS2:73 for T be RealLinearSpace, Lv be Linear_Combination of RLSp2RVSp(T), Lr be Linear_Combination of T st Lr = Lv holds Carrier Lr = Carrier Lv; theorem :: REAL_NS2:74 for V be RealLinearSpace, Fr be FinSequence of V, fr be Function of V,REAL, Fv be FinSequence of RLSp2RVSp(V), fv be Function of RLSp2RVSp(V),F_Real st fr = fv & Fr = Fv holds fr(#)Fr = fv(#)Fv; theorem :: REAL_NS2:75 for T be RealLinearSpace, Ft be FinSequence of T, Fr be FinSequence of RLSp2RVSp(T) st Ft = Fr holds Sum Ft = Sum Fr; theorem :: REAL_NS2:76 for T be RealLinearSpace, Lv be Linear_Combination of RLSp2RVSp(T), Lr be Linear_Combination of T st Lr = Lv holds Sum Lr = Sum Lv; theorem :: REAL_NS2:77 for T be RealLinearSpace, Af be Subset of RLSp2RVSp(T), Ar be Subset of T st Af = Ar holds [#] (Lin Ar) = [#] (Lin Af); theorem :: REAL_NS2:78 for T be RealLinearSpace, Af be Subset of RLSp2RVSp(T), Ar be Subset of T st Af = Ar holds Af is linearly-independent iff Ar is linearly-independent; theorem :: REAL_NS2:79 for T be RealLinearSpace for X be set for U be Subspace of RLSp2RVSp(T) for W be Subspace of T st [#] U = [#] W holds X is Linear_Combination of U iff X is Linear_Combination of W; theorem :: REAL_NS2:80 for W be RealLinearSpace, X be set holds X is Basis of RLSp2RVSp(W) iff X is Basis of W; theorem :: REAL_NS2:81 for W be RealLinearSpace st W is finite-dimensional holds RLSp2RVSp(W) is finite-dimensional & dim RLSp2RVSp(W) = dim W; theorem :: REAL_NS2:82 for W be RealLinearSpace holds W is finite-dimensional iff RLSp2RVSp(W) is finite-dimensional; theorem :: REAL_NS2:83 for n be non empty Nat holds RLSp2RVSp(RealVectSpace(Seg n)) = n -VectSp_over F_Real; theorem :: REAL_NS2:84 for V,W be RealLinearSpace, X be set holds X is LinearOperator of V,W iff X is linear-transformation of RLSp2RVSp(V),RLSp2RVSp(W); theorem :: REAL_NS2:85 for X, Y be RealLinearSpace, L be LinearOperator of X,Y st L is bijective holds ex K be LinearOperator of Y,X st K = L" & K is one-to-one onto; theorem :: REAL_NS2:86 for X,Y,Z be RealLinearSpace, L be LinearOperator of X,Y, K be LinearOperator of Y,Z holds K*L is LinearOperator of X,Z; theorem :: REAL_NS2:87 for V,W be RealLinearSpace, A be Subset of V, T be LinearOperator of V,W st T is bijective holds A is Basis of V iff T.:A is Basis of W; theorem :: REAL_NS2:88 for V be finite-dimensional RealLinearSpace, W be RealLinearSpace st (ex T be LinearOperator of V,W st T is bijective) holds W is finite-dimensional & dim W = dim V; theorem :: REAL_NS2:89 for V be finite-dimensional RealLinearSpace st dim V <> 0 ex T be LinearOperator of V, RealVectSpace(Seg(dim V)) st T is bijective; theorem :: REAL_NS2:90 for V,W be finite-dimensional RealLinearSpace st dim V <> 0 holds dim V = dim W iff ex T be LinearOperator of V, W st T is bijective;