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


theorem Th1: :: REAL_NS2:1
for n being Nat holds RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the addF of (TOP-REAL n), the Mult of (TOP-REAL n) #) = RLSStruct(# the carrier of (REAL-NS n), the ZeroF of (REAL-NS n), the addF of (REAL-NS n), the Mult of (REAL-NS n) #)
proof end;

Lm1: for n being Nat holds the carrier of (n -VectSp_over F_Real) = the carrier of (TOP-REAL n)
proof end;

theorem Th2: :: REAL_NS2:2
for n being Nat holds Euclid n = MetricSpaceNorm (REAL-NS n)
proof end;

theorem :: REAL_NS2:3
for n being Nat holds TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceNorm (REAL-NS n)
proof end;

theorem Th4: :: REAL_NS2:4
for n being Nat holds the carrier of (TOP-REAL n) = the carrier of (REAL-NS n)
proof end;

Lm2: for n being Nat holds the carrier of (n -VectSp_over F_Real) = the carrier of (TOP-REAL n)
proof end;

theorem Th5: :: REAL_NS2:5
for n being Nat holds the carrier of (n -VectSp_over F_Real) = the carrier of (REAL-NS n)
proof end;

theorem Th6: :: REAL_NS2:6
for n being Nat holds 0. (TOP-REAL n) = 0. (REAL-NS n)
proof end;

theorem Th7: :: REAL_NS2:7
for n being Nat
for p, q being Element of (TOP-REAL n)
for f, g being Element of (REAL-NS n) st p = f & q = g holds
p + q = f + g
proof end;

theorem Th8: :: REAL_NS2:8
for n being Nat
for r being Real
for q being Element of (TOP-REAL n)
for g being Element of (REAL-NS n) st q = g holds
r * q = r * g
proof end;

theorem Th9: :: REAL_NS2:9
for n being Nat
for q being Element of (TOP-REAL n)
for g being Element of (REAL-NS n) st q = g holds
- q = - g
proof end;

theorem :: REAL_NS2:10
for n being Nat
for p, q being Element of (TOP-REAL n)
for f, g being Element of (REAL-NS n) st p = f & q = g holds
p - q = f - g
proof end;

theorem Th11: :: REAL_NS2:11
for X being set
for n being Nat holds
( X is Linear_Combination of REAL-NS n iff X is Linear_Combination of TOP-REAL n )
proof end;

theorem :: REAL_NS2:12
for X being set
for n being Nat holds
( X is Linear_Combination of REAL-NS n iff X is Linear_Combination of n -VectSp_over F_Real )
proof end;

theorem :: REAL_NS2:13
for n being Nat
for Lv being Linear_Combination of TOP-REAL n
for Lr being Linear_Combination of REAL-NS n st Lr = Lv holds
Carrier Lr = Carrier Lv ;

theorem :: REAL_NS2:14
for n being Nat
for Lv being Linear_Combination of n -VectSp_over F_Real
for Lr being Linear_Combination of REAL-NS n st Lr = Lv holds
Carrier Lr = Carrier Lv
proof end;

theorem :: REAL_NS2:15
for n being Nat
for F being set holds
( F is Subset of (TOP-REAL n) iff F is Subset of (REAL-NS n) ) by Th4;

theorem :: REAL_NS2:16
for n being Nat
for F being set holds
( F is Subset of (REAL-NS n) iff F is Subset of (n -VectSp_over F_Real) ) by Th5;

theorem :: REAL_NS2:17
for n being Nat
for F being set holds
( F is FinSequence of (TOP-REAL n) iff F is FinSequence of (REAL-NS n) ) by Th4;

theorem Th18: :: REAL_NS2:18
for n being Nat
for F being set holds
( F is Function of (TOP-REAL n),REAL iff F is Function of (REAL-NS n),REAL )
proof end;

theorem Th19: :: REAL_NS2:19
for n being Nat
for Fr being FinSequence of (TOP-REAL n)
for fr being Function of (TOP-REAL n),REAL
for Fv being FinSequence of (REAL-NS n)
for fv being Function of (REAL-NS n),REAL st fr = fv & Fr = Fv holds
fr (#) Fr = fv (#) Fv
proof end;

theorem :: REAL_NS2:20
for n being Nat
for F being FinSequence of (REAL-NS n)
for fr being Function of (REAL-NS 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 Th21: :: REAL_NS2:21
for n being Nat
for Ft being FinSequence of (TOP-REAL n)
for Fr being FinSequence of (REAL-NS n) st Ft = Fr holds
Sum Ft = Sum Fr
proof end;

theorem :: REAL_NS2:22
for n being Nat
for F being FinSequence of (REAL-NS n)
for Fv being FinSequence of (n -VectSp_over F_Real) st Fv = F holds
Sum F = Sum Fv
proof end;

theorem Th23: :: REAL_NS2:23
for n being Nat
for Lr being Linear_Combination of REAL-NS n
for Lt being Linear_Combination of TOP-REAL n st Lr = Lt holds
Sum Lr = Sum Lt
proof end;

theorem :: REAL_NS2:24
for n being Nat
for Lv being Linear_Combination of n -VectSp_over F_Real
for Lr being Linear_Combination of REAL-NS n st Lr = Lv holds
Sum Lr = Sum Lv
proof end;

theorem Th25: :: REAL_NS2:25
for n being Nat
for Ar being Subset of (REAL-NS n)
for At being Subset of (TOP-REAL n) st Ar = At holds
for X being object holds
( X is Linear_Combination of Ar iff X is Linear_Combination of At )
proof end;

theorem Th26: :: REAL_NS2:26
for n being Nat
for Ar being Subset of (REAL-NS n)
for At being Subset of (TOP-REAL n) st Ar = At holds
[#] (Lin Ar) = [#] (Lin At)
proof end;

theorem :: REAL_NS2:27
for n being Nat
for Af being Subset of (n -VectSp_over F_Real)
for Ar being Subset of (REAL-NS n) st Af = Ar holds
[#] (Lin Ar) = [#] (Lin Af)
proof end;

theorem Th28: :: REAL_NS2:28
for n being Nat
for Ar being Subset of (REAL-NS n)
for At being Subset of (TOP-REAL n) st Ar = At holds
( Ar is linearly-independent iff At is linearly-independent )
proof end;

theorem :: REAL_NS2:29
for n being Nat
for Af being Subset of (n -VectSp_over F_Real)
for Ar being Subset of (REAL-NS n) st Af = Ar holds
( Af is linearly-independent iff Ar is linearly-independent )
proof end;

theorem Th30: :: REAL_NS2:30
for n being Nat
for X being object holds
( X is Subspace of REAL-NS n iff X is Subspace of TOP-REAL n )
proof end;

theorem :: REAL_NS2:31
for n being Nat
for X being set
for U being Subspace of REAL-NS n
for W being Subspace of n -VectSp_over F_Real st [#] U = [#] W holds
( X is Linear_Combination of U iff X is Linear_Combination of W )
proof end;

theorem Th32: :: REAL_NS2:32
for n being Nat
for F being one-to-one FinSequence of (REAL-NS 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 Th33: :: REAL_NS2:33
for n being Nat
for M being Matrix of n,F_Real
for N being Matrix of n,REAL st N = MXF2MXR M holds
( M is invertible iff N is invertible )
proof end;

theorem :: REAL_NS2:34
for n being Nat
for M being Matrix of n,REAL holds
( M is invertible iff MXR2MXF M is invertible )
proof end;

theorem :: REAL_NS2:35
for n being Nat
for F being one-to-one FinSequence of (REAL-NS n) st rng F is linearly-independent holds
ex M being Matrix of n,REAL st
( M is invertible & M | (len F) = F )
proof end;

theorem :: REAL_NS2:36
for n being Nat
for F being one-to-one FinSequence of (REAL-NS 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 :: REAL_NS2:37
for n being Nat
for A, B being linearly-independent Subset of (REAL-NS 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;

theorem :: REAL_NS2:38
for n, m being Nat
for M being Matrix of n,m,F_Real
for A being linearly-independent Subset of (REAL-NS n) st the_rank_of M = n holds
(Mx2Tran M) .: A is linearly-independent
proof end;

theorem Th39: :: REAL_NS2:39
for n being Nat
for p being Element of (TOP-REAL n)
for f being Element of (REAL-NS n)
for H being Subset of (TOP-REAL n)
for I being Subset of (REAL-NS n) st p = f & H = I holds
p + H = f + I
proof end;

theorem Th40: :: REAL_NS2:40
for n being Nat
for Ar being Subset of (REAL-NS n)
for At being Subset of (TOP-REAL n) st Ar = At holds
( Ar is Affine iff At is Affine )
proof end;

theorem Th41: :: REAL_NS2:41
for n being Nat
for X being set holds
( X is affinely-independent Subset of (REAL-NS n) iff X is affinely-independent Subset of (TOP-REAL n) )
proof end;

theorem :: REAL_NS2:42
for n, m being Nat
for M being Matrix of n,m,F_Real
for A being affinely-independent Subset of (REAL-NS n) st the_rank_of M = n holds
(Mx2Tran M) .: A is affinely-independent
proof end;

theorem Th43: :: REAL_NS2:43
for n being Nat
for Ar being Subset of (REAL-NS n)
for At being Subset of (TOP-REAL n) st Ar = At holds
Affin Ar = Affin At
proof end;

theorem Th44: :: REAL_NS2:44
for n being Nat
for L being Linear_Combination of REAL-NS n
for S being Linear_Combination of TOP-REAL n st L = S holds
sum L = sum S
proof end;

theorem Th45: :: REAL_NS2:45
for n being Nat
for Ar being Subset of (REAL-NS n)
for At being Subset of (TOP-REAL n)
for v being Element of (REAL-NS n)
for w being Element of (TOP-REAL n) st Ar = At & v = w & v in Affin Ar & Ar is affinely-independent holds
v |-- Ar = w |-- At
proof end;

theorem :: REAL_NS2:46
for n, m being Nat
for M being Matrix of n,m,F_Real
for A being affinely-independent Subset of (REAL-NS n) st the_rank_of M = n holds
for v being Element of (REAL-NS n) st v in Affin A holds
( (Mx2Tran M) . v in Affin ((Mx2Tran M) .: A) & ( for f being b1 -element real-valued FinSequence holds (v |-- A) . f = (((Mx2Tran M) . v) |-- ((Mx2Tran M) .: A)) . ((Mx2Tran M) . f) ) )
proof end;

theorem :: REAL_NS2:47
for n, m being Nat
for M being Matrix of n,m,F_Real
for A being linearly-independent Subset of (REAL-NS m) st the_rank_of M = n holds
(Mx2Tran M) " A is linearly-independent
proof end;

theorem :: REAL_NS2:48
for n, m being Nat
for M being Matrix of n,m,F_Real
for A being affinely-independent Subset of (REAL-NS m) st the_rank_of M = n holds
(Mx2Tran M) " A is affinely-independent
proof end;

theorem Th49: :: REAL_NS2:49
for V being RealLinearSpace
for W being strict Subspace of V holds W is strict Subspace of (Omega). V
proof end;

theorem Th50: :: REAL_NS2:50
for n being Nat
for X being set holds
( X is Basis of (n -VectSp_over F_Real) iff X is Basis of TOP-REAL n )
proof end;

theorem Th51: :: REAL_NS2:51
for n being non empty Nat holds RealFuncAdd (Seg n) = product ( the addF of F_Real,n)
proof end;

theorem Th52: :: REAL_NS2:52
for n being non empty Nat holds RealFuncExtMult (Seg n) = n -Mult_over F_Real
proof end;

theorem Th53: :: REAL_NS2:53
for n being Nat holds
( TOP-REAL n is finite-dimensional & dim (TOP-REAL n) = n )
proof end;

theorem Th54: :: REAL_NS2:54
for n being 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) )
proof end;

theorem :: REAL_NS2:55
for n being non empty Nat
for xv, yv being Element of (n -VectSp_over F_Real)
for xt, yt being Element of (TOP-REAL n) st xv = xt & yv = yt holds
xv + yv = xt + yt by Th54;

theorem :: REAL_NS2:56
for n being non empty Nat
for af being Element of F_Real
for at being Real
for xv being Element of (n -VectSp_over F_Real)
for xt being Element of (TOP-REAL n) st af = at & xv = xt holds
af * xv = at * xt by Th54;

theorem Th57: :: REAL_NS2:57
for n being non empty Nat
for xv being Element of (n -VectSp_over F_Real)
for xt being Element of (TOP-REAL n) st xv = xt holds
- xv = - xt
proof end;

theorem :: REAL_NS2:58
for n being non empty Nat
for xv, yv being Element of (n -VectSp_over F_Real)
for xt, yt being Element of (TOP-REAL n) st xv = xt & yv = yt holds
xv - yv = xt - yt
proof end;

theorem :: REAL_NS2:59
for n being non empty Nat
for At being Subset of (TOP-REAL n)
for Ar being 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) )
proof end;

theorem :: REAL_NS2:60
for n being Nat
for At being Subset of (TOP-REAL n)
for Ar being Subset of (REAL-NS n) st At = Ar holds
Lin At = Lin Ar
proof end;

theorem Th61: :: REAL_NS2:61
for n being Nat
for X being set holds
( X is Basis of TOP-REAL n iff X is Basis of REAL-NS n )
proof end;

theorem Th62: :: REAL_NS2:62
for n being Nat holds
( REAL-NS n is finite-dimensional & dim (REAL-NS n) = n )
proof end;

registration
cluster non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V303() RealNormSpace-like finite-dimensional for NORMSTR ;
existence
ex b1 being RealNormSpace st b1 is finite-dimensional
proof end;
end;

theorem Th63: :: REAL_NS2:63
for K being Field
for V being finite-dimensional VectSp of K
for b being OrdBasis of V ex T being linear-transformation of V,((dim V) -VectSp_over K) st
( T is bijective & ( for x being Element of V holds T . x = x |-- b ) )
proof end;

theorem Th64: :: REAL_NS2:64
for K being Field
for V being finite-dimensional VectSp of K ex T being linear-transformation of V,((dim V) -VectSp_over K) st T is bijective
proof end;

theorem :: REAL_NS2:65
for K being Field
for V, W being finite-dimensional VectSp of K holds
( dim V = dim W iff ex T being linear-transformation of V,W st T is bijective )
proof end;

theorem :: REAL_NS2:66
for X being 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 being strict RealLinearSpace holds RVSp2RLSp (RLSp2RVSp X) = X ;

theorem :: REAL_NS2:68
for X being strict VectSp of F_Real holds RLSp2RVSp (RVSp2RLSp X) = X ;

theorem :: REAL_NS2:69
for V being RealLinearSpace
for F being set holds
( F is Subset of V iff F is Subset of (RLSp2RVSp V) ) ;

theorem :: REAL_NS2:70
for V being RealLinearSpace
for F being set holds
( F is FinSequence of V iff F is FinSequence of (RLSp2RVSp V) ) ;

theorem :: REAL_NS2:71
for V being RealLinearSpace
for F being set holds
( F is Function of V,REAL iff F is Function of (RLSp2RVSp V),REAL ) ;

theorem Th72: :: REAL_NS2:72
for T being RealLinearSpace
for X being set holds
( X is Linear_Combination of RLSp2RVSp T iff X is Linear_Combination of T )
proof end;

theorem Th73: :: REAL_NS2:73
for T being RealLinearSpace
for Lv being Linear_Combination of RLSp2RVSp T
for Lr being Linear_Combination of T st Lr = Lv holds
Carrier Lr = Carrier Lv
proof end;

theorem Th74: :: REAL_NS2:74
for V being RealLinearSpace
for Fr being FinSequence of V
for fr being Function of V,REAL
for Fv being FinSequence of (RLSp2RVSp V)
for fv being Function of (RLSp2RVSp V),F_Real st fr = fv & Fr = Fv holds
fr (#) Fr = fv (#) Fv
proof end;

theorem :: REAL_NS2:75
for T being RealLinearSpace
for Ft being FinSequence of T
for Fr being FinSequence of (RLSp2RVSp T) st Ft = Fr holds
Sum Ft = Sum Fr ;

theorem Th76: :: REAL_NS2:76
for T being RealLinearSpace
for Lv being Linear_Combination of RLSp2RVSp T
for Lr being Linear_Combination of T st Lr = Lv holds
Sum Lr = Sum Lv
proof end;

theorem Th77: :: REAL_NS2:77
for T being RealLinearSpace
for Af being Subset of (RLSp2RVSp T)
for Ar being Subset of T st Af = Ar holds
[#] (Lin Ar) = [#] (Lin Af)
proof end;

theorem Th78: :: REAL_NS2:78
for T being RealLinearSpace
for Af being Subset of (RLSp2RVSp T)
for Ar being Subset of T st Af = Ar holds
( Af is linearly-independent iff Ar is linearly-independent )
proof end;

theorem :: REAL_NS2:79
for T being RealLinearSpace
for X being set
for U being Subspace of RLSp2RVSp T
for W being Subspace of T st [#] U = [#] W holds
( X is Linear_Combination of U iff X is Linear_Combination of W )
proof end;

theorem Th80: :: REAL_NS2:80
for W being RealLinearSpace
for X being set holds
( X is Basis of (RLSp2RVSp W) iff X is Basis of W )
proof end;

theorem Th81: :: REAL_NS2:81
for W being RealLinearSpace st W is finite-dimensional holds
( RLSp2RVSp W is finite-dimensional & dim (RLSp2RVSp W) = dim W )
proof end;

theorem :: REAL_NS2:82
for W being RealLinearSpace holds
( W is finite-dimensional iff RLSp2RVSp W is finite-dimensional )
proof end;

theorem Th83: :: REAL_NS2:83
for n being non empty Nat holds RLSp2RVSp (RealVectSpace (Seg n)) = n -VectSp_over F_Real
proof end;

theorem Th84: :: REAL_NS2:84
for V, W being RealLinearSpace
for X being set holds
( X is LinearOperator of V,W iff X is linear-transformation of (RLSp2RVSp V),(RLSp2RVSp W) )
proof end;

theorem Th85: :: REAL_NS2:85
for X, Y being RealLinearSpace
for L being LinearOperator of X,Y st L is bijective holds
ex K being LinearOperator of Y,X st
( K = L " & K is one-to-one & K is onto )
proof end;

theorem Th86: :: REAL_NS2:86
for X, Y, Z being RealLinearSpace
for L being LinearOperator of X,Y
for K being LinearOperator of Y,Z holds K * L is LinearOperator of X,Z
proof end;

theorem Th87: :: REAL_NS2:87
for V, W being RealLinearSpace
for A being Subset of V
for T being LinearOperator of V,W st T is bijective holds
( A is Basis of V iff T .: A is Basis of W )
proof end;

theorem Th88: :: REAL_NS2:88
for V being finite-dimensional RealLinearSpace
for W being RealLinearSpace st ex T being LinearOperator of V,W st T is bijective holds
( W is finite-dimensional & dim W = dim V )
proof end;

theorem Th89: :: REAL_NS2:89
for V being finite-dimensional RealLinearSpace st dim V <> 0 holds
ex T being LinearOperator of V,(RealVectSpace (Seg (dim V))) st T is bijective
proof end;

theorem :: REAL_NS2:90
for V, W being finite-dimensional RealLinearSpace st dim V <> 0 holds
( dim V = dim W iff ex T being LinearOperator of V,W st T is bijective )
proof end;