:: Transformation tools for real linear spaces
:: by Kazuhisa Nakasho
::
:: Received July 23, 2022
:: Copyright (c) 2022-2025 Association of Mizar Users

registration

let n be Nat;

cluster REAL-NS n -> finite-dimensional ;

correctness
coherence
REAL-NS n is finite-dimensional ;
by REAL_NS2:62;

end;

theorem Th1: :: LOPBAN15:1

for X, Y being RealLinearSpace
for L being LinearOperator of X,Y
for F being FinSequence of X holds L . (Sum F) = Sum (L * F)

proof end;

theorem Th2: :: LOPBAN15:2

for X being finite-dimensional RealNormSpace
for Y being RealNormSpace
for L being LinearOperator of X,Y st dim X <> 0 holds
L is Lipschitzian

proof end;

theorem :: LOPBAN15:3

for X being finite-dimensional RealNormSpace
for Y being RealNormSpace st dim X <> 0 holds
LinearOperators (X,Y) = BoundedLinearOperators (X,Y)

proof end;

registration

cluster RNS_Real -> ;

coherence
( not RNS_Real is empty & RNS_Real is right_complementable & RNS_Real is Abelian & RNS_Real is add-associative & RNS_Real is right_zeroed & RNS_Real is vector-distributive & RNS_Real is scalar-distributive & RNS_Real is scalar-associative & RNS_Real is scalar-unital & RNS_Real is discerning & RNS_Real is reflexive & RNS_Real is RealNormSpace-like ) ;

end;

theorem :: LOPBAN15:4

for v, w being Element of RNS_Real
for v1, w1 being Element of REAL st v = v1 & w = w1 holds
v + w = v1 + w1 by BINOP_2:def 9;

theorem :: LOPBAN15:5

for v being Element of RNS_Real
for v1 being Element of REAL
for a being Real st v = v1 holds
a * v = a * v1 by BINOP_2:def 11;

::: DUALSP02:11 remove for X
::: see DUALSP03:3 for minus, repeated DUALSP02:11

theorem :: LOPBAN15:6

for v being Element of RNS_Real
for v1 being Element of REAL st v = v1 holds
||.v.|| = |.v1.| by EUCLID:def 2;

theorem Th9: :: LOPBAN15:7

ex f being LinearOperator of RNS_Real,(REAL-NS 1) st
( f is isomorphism & ( for x being Element of RNS_Real holds f . x = <*x*> ) )

proof end;

theorem :: LOPBAN15:8

( RNS_Real is finite-dimensional & dim RNS_Real = 1 )

proof end;

theorem Th11: :: LOPBAN15:9

for X being RealLinearSpace-Sequence
for v, w being Element of product (carr X)
for i being Element of dom (carr X) holds
( ([:(addop X):] . (v,w)) . i = the addF of (X . i) . ((v . i),(w . i)) & ( for vi, wi being VECTOR of (X . i) st vi = v . i & wi = w . i holds
([:(addop X):] . (v,w)) . i = vi + wi ) )

proof end;

theorem Th12: :: LOPBAN15:10

for X being RealLinearSpace-Sequence
for r being Element of REAL
for v being Element of product (carr X)
for i being Element of dom (carr X) holds
( ([:(multop X):] . (r,v)) . i = the Mult of (X . i) . (r,(v . i)) & ( for vi being VECTOR of (X . i) st vi = v . i holds
([:(multop X):] . (r,v)) . i = r * vi ) )

proof end;

theorem Th13: :: LOPBAN15:11

for n being Nat
for X being RealNormSpace-Sequence st X = n |-> RNS_Real holds
product X = REAL-NS n

proof end;

theorem :: LOPBAN15:12

for n being Nat
for X being RealNormSpace-Sequence st X = n |-> RNS_Real holds
( product X is finite-dimensional & dim (product X) = n )

proof end;

definition

let X be RealLinearSpace;
let Y be Subspace of X;
:: original: RLSp2RVSp
redefine func RLSp2RVSp Y -> Subspace of RLSp2RVSp X;
correctness
coherence
RLSp2RVSp Y is Subspace of RLSp2RVSp X;

proof end;

end;

theorem :: LOPBAN15:13

for X being RealLinearSpace
for Y being Subspace of X holds RLSp2RVSp Y is Subspace of RLSp2RVSp X ;

theorem Th16: :: LOPBAN15:14

for X being RealLinearSpace
for Y1, Y2 being Subspace of X holds RLSp2RVSp (Y1 + Y2) = (RLSp2RVSp Y1) + (RLSp2RVSp Y2)

proof end;

theorem Th17: :: LOPBAN15:15

for X being RealLinearSpace
for Y1, Y2 being Subspace of X holds RLSp2RVSp (Y1 /\ Y2) = (RLSp2RVSp Y1) /\ (RLSp2RVSp Y2)

proof end;

theorem Th18: :: LOPBAN15:16

for X being RealLinearSpace holds RLSp2RVSp ((0). X) = (0). (RLSp2RVSp X)

proof end;

theorem :: LOPBAN15:17

for X being RealLinearSpace
for Y1, Y2 being Subspace of X st Y1 /\ Y2 = (0). X holds
for B1 being linearly-independent Subset of Y1
for B2 being linearly-independent Subset of Y2 holds B1 \/ B2 is linearly-independent Subset of (Y1 + Y2)

proof end;

theorem Th20: :: LOPBAN15:18

for X being RealLinearSpace
for Y1, Y2 being Subspace of X st Y1 /\ Y2 = (0). X holds
for B1 being Basis of Y1
for B2 being Basis of Y2 holds B1 \/ B2 is Basis of Y1 + Y2

proof end;

theorem Th21: :: LOPBAN15:19

for X, Y being RealLinearSpace
for X1 being Subspace of X
for Y1 being Subspace of Y holds [:X1,Y1:] is Subspace of [:X,Y:]

proof end;

theorem Th22: :: LOPBAN15:20

for X, Y being RealLinearSpace
for X1, Y1 being Subspace of [:X,Y:] st X1 = [:X,((0). Y):] & Y1 = [:((0). X),Y:] holds
( X1 + Y1 = [:X,Y:] & X1 /\ Y1 = (0). [:X,Y:] )

proof end;

theorem Th23: :: LOPBAN15:21

for X, Y being RealLinearSpace ex f being LinearOperator of X,[:X,((0). Y):] st
( f is bijective & ( for x being Element of X holds f . x = [x,(0. Y)] ) )

proof end;

theorem Th24: :: LOPBAN15:22

for X, Y being RealLinearSpace ex f being LinearOperator of Y,[:((0). X),Y:] st
( f is bijective & ( for y being Element of Y holds f . y = [(0. X),y] ) )

proof end;

Lm1: for X being RealLinearSpace
for B being Basis of X holds not 0. X in B

proof end;

theorem Th25: :: LOPBAN15:23

for X, Y being RealLinearSpace
for BX being Basis of X
for BY being Basis of Y holds [:BX,{(0. Y)}:] \/ [:{(0. X)},BY:] is Basis of [:X,Y:]

proof end;

theorem Th26: :: LOPBAN15:24

for X, Y being finite-dimensional RealLinearSpace holds
( [:X,Y:] is finite-dimensional & dim [:X,Y:] = (dim X) + (dim Y) )

proof end;

theorem Th27: :: LOPBAN15:25

for X being finite-dimensional RealLinearSpace holds
( product <*X*> is finite-dimensional & dim (product <*X*>) = dim X )

proof end;

theorem :: LOPBAN15:26

for X being RealLinearSpace-Sequence
for d being FinSequence of NAT st len d = len X & ( for i being Element of dom X holds
( X . i is finite-dimensional & d . i = dim (X . i) ) ) holds
( product X is finite-dimensional & dim (product X) = Sum d )

proof end;