:: Some Standard Examples of Vector Spaces
:: by Christoph Schwarzweller and Agnieszka Rowi\'nska-Schwarzweller
::
:: Received December 24, 2024
:: Copyright (c) 2024-2025 Association of Mizar Users

theorem lemiso: :: VECTSP13:1

for X, Y being non empty finite set st card Y = card X holds
ex f being Function of X,Y st f is bijective

proof end;

registration

let L be non empty addLoopStr ;
let n be Nat;
let u, v be n -element FinSequence of the carrier of L;

cluster u + v -> n -element ;

coherence
u + v is n -element

proof end;

end;

registration

let M be non empty multMagma ;
let n be Nat;
let u be n -element FinSequence of the carrier of M;
let a be Element of M;

cluster a * u -> n -element ;

coherence
a * u is n -element

proof end;

end;

theorem Lm1: :: VECTSP13:2

for R being non empty Abelian addLoopStr
for n being Nat
for u, v being Tuple of n, the carrier of R holds u + v = v + u

proof end;

theorem Lm2: :: VECTSP13:3

for R being non empty add-associative addLoopStr
for n being Nat
for u, v, w being Tuple of n, the carrier of R holds (u + v) + w = u + (v + w)

proof end;

dtr: for F being Field
for V being VectSp of F holds
( V is trivial iff the carrier of V = {(0. V)} )

proof end;

registration

let F be Field;

cluster non empty trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital -> trivial finite-dimensional for ModuleStr over F;

coherence
for b₁ being trivial VectSp of F holds b₁ is finite-dimensional

proof end;

end;

registration

let F be Field;
let V be non trivial VectSp of F;

cluster non empty finite linearly-independent for Element of bool the carrier of V;

existence
ex b₁ being Subset of V st
( not b₁ is empty & b₁ is finite & b₁ is linearly-independent )

proof end;

end;

registration

let F be Field;
let V be non trivial finite-dimensional VectSp of F;

cluster base -> non empty for Element of bool the carrier of V;

coherence
for b₁ being Basis of V holds not b₁ is empty

proof end;

end;

definition

let F be Field;
let U, V be VectSp of F;
let B be non empty Subset of U;
let f be Function of B,V;
:: original: rng
redefine func rng f -> Subset of V;
coherence
rng f is Subset of V

proof end;

end;

theorem lembas1: :: VECTSP13:4

for F being Field
for U being VectSp of F
for B being linearly-independent Subset of U
for w being Element of U st w in B holds
for l being Linear_Combination of B st Sum l = w holds
( Carrier l = {w} & l . w = 1. F )

proof end;

theorem canlinsurj1: :: VECTSP13:5

for F being Field
for U, V being VectSp of F
for B being Subset of U
for A being Subset of V
for T being linear-transformation of U,V st T .: B c= A holds
for l being Linear_Combination of B holds T . (Sum l) in Lin A

proof end;

theorem canLinuni: :: VECTSP13:6

for F being Field
for U, V being VectSp of F
for B being Basis of U
for T1, T2 being linear-transformation of U,V st T1 | B = T2 | B holds
T1 = T2

proof end;

definition

let F be Field;
let U, V be VectSp of F;
let B be non empty finite Subset of U;
let l be Linear_Combination of B;
let f be Function of B,V;
let v be Element of V;

func Expand (f,l,v) -> FinSequence of the carrier of F equals :: VECTSP13:def 1
l * (canFS (f " {v}));

coherence
l * (canFS (f " {v})) is FinSequence of the carrier of F

proof end;

end;

:: deftheorem defines Expand VECTSP13:def 1 :
for F being Field
for U, V being VectSp of F
for B being non empty finite Subset of U
for l being Linear_Combination of B
for f being Function of B,V
for v being Element of V holds Expand (f,l,v) = l * (canFS (f " {v}));

definition

let F be Field;
let U, V be VectSp of F;
let B be non empty finite Subset of U;
let l be Linear_Combination of B;
let f be Function of B,V;

func f (#) l -> Linear_Combination of rng f means :defK: :: VECTSP13:def 2
for v being Element of V holds it . v = Sum (Expand (f,l,v));

existence
ex b₁ being Linear_Combination of rng f st
for v being Element of V holds b₁ . v = Sum (Expand (f,l,v))

proof end;

uniqueness
for b₁, b₂ being Linear_Combination of rng f st ( for v being Element of V holds b₁ . v = Sum (Expand (f,l,v)) ) & ( for v being Element of V holds b₂ . v = Sum (Expand (f,l,v)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defK defines (#) VECTSP13:def 2 :
for F being Field
for U, V being VectSp of F
for B being non empty finite Subset of U
for l being Linear_Combination of B
for f being Function of B,V
for b₇ being Linear_Combination of rng f holds
( b₇ = f (#) l iff for v being Element of V holds b₇ . v = Sum (Expand (f,l,v)) );

canlininj1: for F being Field
for U, V being VectSp of F
for B being non empty finite Subset of U
for f being Function of B,V
for l2 being Linear_Combination of rng f ex l1 being Linear_Combination of B st
for u being Element of U st u in B holds
l1 . u = l2 . (f . u)

proof end;

definition

let F be Field;
let U, V be VectSp of F;
let B be non empty finite Subset of U;
let f be Function of B,V;
let l be Linear_Combination of rng f;

func l (#) f -> Linear_Combination of B means :defK1: :: VECTSP13:def 3
for u being Element of U st u in B holds
it . u = l . (f . u);

existence
ex b₁ being Linear_Combination of B st
for u being Element of U st u in B holds
b₁ . u = l . (f . u) by canlininj1;
uniqueness
for b₁, b₂ being Linear_Combination of B st ( for u being Element of U st u in B holds
b₁ . u = l . (f . u) ) & ( for u being Element of U st u in B holds
b₂ . u = l . (f . u) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defK1 defines (#) VECTSP13:def 3 :
for F being Field
for U, V being VectSp of F
for B being non empty finite Subset of U
for f being Function of B,V
for l being Linear_Combination of rng f
for b₇ being Linear_Combination of B holds
( b₇ = l (#) f iff for u being Element of U st u in B holds
b₇ . u = l . (f . u) );

XXX1: for F being Field
for U, V being VectSp of F
for B being non empty Subset of U
for f being Function of B,V st f is one-to-one holds
for v being Element of V st v in rng f holds
f " {v} = {((f ") . v)}

proof end;

theorem XXX2: :: VECTSP13:7

for F being Field
for U, V being VectSp of F
for B being non empty finite Subset of U
for f being Function of B,V st f is one-to-one holds
for l being Linear_Combination of B
for v being Element of V st v in rng f holds
(f (#) l) . v = l . ((f ") . v)

proof end;

theorem XXX3: :: VECTSP13:8

for F being Field
for U, V being VectSp of F
for B being non empty finite Subset of U
for f being Function of B,V st f is one-to-one holds
for l being Linear_Combination of B holds (f (#) l) (#) f = l

proof end;

theorem XXX4: :: VECTSP13:9

for F being Field
for U, V being VectSp of F
for B being non empty finite Subset of U
for f being Function of B,V st f is one-to-one holds
for l being Linear_Combination of rng f holds f (#) (l (#) f) = l

proof end;

lemadd2b: for F being Field
for U, V being VectSp of F
for B being non empty finite Subset of U
for f being Function of B,V
for l being Linear_Combination of B
for v being Element of V st not v in rng f holds
(f (#) l) . v = 0. F

proof end;

theorem lemadd2a: :: VECTSP13:10

for F being Field
for U, V being VectSp of F
for B being non empty finite Subset of U
for f being Function of B,V
for l being Linear_Combination of B holds Carrier (f (#) l) c= f .: (Carrier l)

proof end;

theorem lemadd2: :: VECTSP13:11

for F being Field
for U, V being VectSp of F
for B being non empty finite Subset of U
for b being Element of B
for f being Function of B,V
for l being Linear_Combination of B st Carrier l = {b} holds
( Carrier (f (#) l) = {(f . b)} & Sum (f (#) l) = (l . b) * (f . b) )

proof end;

theorem lemaddx: :: VECTSP13:12

for F being Field
for U, V being VectSp of F
for B being non empty finite Subset of U
for f being Function of B,V
for l1, l2, l3 being Linear_Combination of B st l3 = l1 + l2 holds
f (#) l3 = (f (#) l1) + (f (#) l2)

proof end;

lemadd: for F being Field
for U, V being VectSp of F
for B being non empty finite Subset of U
for f being Function of B,V
for l1, l2, l3 being Linear_Combination of B st l3 = l1 + l2 holds
Sum (f (#) l3) = (Sum (f (#) l1)) + (Sum (f (#) l2))

proof end;

theorem lemmultx: :: VECTSP13:13

for F being Field
for U, V being VectSp of F
for B being non empty finite Subset of U
for f being Function of B,V
for l1, l2 being Linear_Combination of B
for a being Element of F st l2 = a * l1 holds
f (#) l2 = a * (f (#) l1)

proof end;

lemmult: for F being Field
for U, V being VectSp of F
for B being non empty finite Subset of U
for f being Function of B,V
for l1, l2 being Linear_Combination of B
for a being Element of F st a * l1 = l2 holds
Sum (f (#) l2) = a * (Sum (f (#) l1))

proof end;

theorem :: VECTSP13:14

for F being Field
for U, V being VectSp of F
for B being non empty finite Subset of U
for f being Function of B,V
for l1, l2 being Linear_Combination of B st l2 = - l1 holds
f (#) l2 = - (f (#) l1) by lemmultx;

theorem lemminusx: :: VECTSP13:15

for F being Field
for U, V being VectSp of F
for B being non empty finite Subset of U
for f being Function of B,V
for l1, l2, l3 being Linear_Combination of B st l3 = l1 - l2 holds
f (#) l3 = (f (#) l1) - (f (#) l2)

proof end;

lemminus: for F being Field
for U, V being VectSp of F
for B being non empty finite Subset of U
for f being Function of B,V
for l1, l2, l3 being Linear_Combination of B st l3 = l1 - l2 holds
Sum (f (#) l3) = (Sum (f (#) l1)) - (Sum (f (#) l2))

proof end;

theorem lembas: :: VECTSP13:16

for F being Field
for U, V being VectSp of F
for B being non empty finite Subset of U st B is linearly-independent holds
for w being Element of U st w in B holds
for l being Linear_Combination of B st Sum l = w holds
for f being Function of B,V holds Sum (f (#) l) = f . w

proof end;

definition

let F be Field;
let U be finite-dimensional VectSp of F;
let V be VectSp of F;
let B be Basis of U;
let f be Function of B,V;

func canLinTrans f -> linear-transformation of U,V means :defcl: :: VECTSP13:def 4
it | B = f;

existence
ex b₁ being linear-transformation of U,V st b₁ | B = f

proof end;

uniqueness
for b₁, b₂ being linear-transformation of U,V st b₁ | B = f & b₂ | B = f holds
b₁ = b₂ by canLinuni;

end;

:: deftheorem defcl defines canLinTrans VECTSP13:def 4 :
for F being Field
for U being finite-dimensional VectSp of F
for V being VectSp of F
for B being Basis of U
for f being Function of B,V
for b₆ being linear-transformation of U,V holds
( b₆ = canLinTrans f iff b₆ | B = f );

theorem CLS: :: VECTSP13:17

for F being Field
for U being non trivial finite-dimensional VectSp of F
for V being VectSp of F
for B being Basis of U
for f being Function of B,V
for l being Linear_Combination of B holds (canLinTrans f) . (Sum l) = Sum (f (#) l)

proof end;

theorem :: VECTSP13:18

for F being Field
for U, V being finite-dimensional VectSp of F
for B being Basis of U
for f being Function of B,V
for T being linear-transformation of U,V holds
( T = canLinTrans f iff for u being Element of U st u in B holds
T . u = f . u )

proof end;

theorem canlinsurj2: :: VECTSP13:19

for F being Field
for U, V being finite-dimensional VectSp of F
for B being Basis of U
for f being Function of B,V holds (canLinTrans f) .: B c= rng f

proof end;

theorem canlinsurj3: :: VECTSP13:20

for F being Field
for U being non trivial finite-dimensional VectSp of F
for V being finite-dimensional VectSp of F
for B being Basis of U
for f being Function of B,V
for l2 being Linear_Combination of rng f ex l1 being Linear_Combination of B st (canLinTrans f) . (Sum l1) = Sum l2

proof end;

theorem canlinsurj: :: VECTSP13:21

for F being Field
for U being non trivial finite-dimensional VectSp of F
for V being finite-dimensional VectSp of F
for B being Basis of U
for f being Function of B,V holds im (canLinTrans f) = Lin (rng f)

proof end;

XXX4a: for F being Field
for U being non trivial finite-dimensional VectSp of F
for V being finite-dimensional VectSp of F
for B being Basis of U
for f being Function of B,V st f is one-to-one holds
for l being Linear_Combination of rng f holds (canLinTrans f) . (Sum (l (#) f)) = Sum l

proof end;

canLininjrngA: for F being Field
for U being non trivial finite-dimensional VectSp of F
for V being finite-dimensional VectSp of F
for B being Basis of U
for f being Function of B,V st canLinTrans f is one-to-one holds
rng f is linearly-independent

proof end;

canLininjrngB: for F being Field
for U being non trivial finite-dimensional VectSp of F
for V being finite-dimensional VectSp of F
for B being Basis of U
for f being Function of B,V st f is one-to-one & rng f is linearly-independent holds
canLinTrans f is one-to-one

proof end;

theorem canLininj: :: VECTSP13:22

for F being Field
for U being non trivial finite-dimensional VectSp of F
for V being finite-dimensional VectSp of F
for B being Basis of U
for f being Function of B,V holds
( canLinTrans f is one-to-one iff ( rng f is linearly-independent & f is one-to-one ) )

proof end;

definition

let R be Ring;
let n be Nat;

func vector_add (n,R) -> BinOp of (n -tuples_on the carrier of R) means :Defa: :: VECTSP13:def 5
for u, v being Tuple of n, the carrier of R holds it . (u,v) = u + v;

existence
ex b₁ being BinOp of (n -tuples_on the carrier of R) st
for u, v being Tuple of n, the carrier of R holds b₁ . (u,v) = u + v

proof end;

uniqueness
for b₁, b₂ being BinOp of (n -tuples_on the carrier of R) st ( for u, v being Tuple of n, the carrier of R holds b₁ . (u,v) = u + v ) & ( for u, v being Tuple of n, the carrier of R holds b₂ . (u,v) = u + v ) holds
b₁ = b₂

proof end;

func vector_mult (n,R) -> Function of [: the carrier of R,(n -tuples_on the carrier of R):],(n -tuples_on the carrier of R) means :Defm: :: VECTSP13:def 6
for a being Element of R
for u being Tuple of n, the carrier of R holds it . (a,u) = a * u;

existence
ex b₁ being Function of [: the carrier of R,(n -tuples_on the carrier of R):],(n -tuples_on the carrier of R) st
for a being Element of R
for u being Tuple of n, the carrier of R holds b₁ . (a,u) = a * u

proof end;

uniqueness
for b₁, b₂ being Function of [: the carrier of R,(n -tuples_on the carrier of R):],(n -tuples_on the carrier of R) st ( for a being Element of R
for u being Tuple of n, the carrier of R holds b₁ . (a,u) = a * u ) & ( for a being Element of R
for u being Tuple of n, the carrier of R holds b₂ . (a,u) = a * u ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Defa defines vector_add VECTSP13:def 5 :
for R being Ring
for n being Nat
for b₃ being BinOp of (n -tuples_on the carrier of R) holds
( b₃ = vector_add (n,R) iff for u, v being Tuple of n, the carrier of R holds b₃ . (u,v) = u + v );

:: deftheorem Defm defines vector_mult VECTSP13:def 6 :
for R being Ring
for n being Nat
for b₃ being Function of [: the carrier of R,(n -tuples_on the carrier of R):],(n -tuples_on the carrier of R) holds
( b₃ = vector_mult (n,R) iff for a being Element of R
for u being Tuple of n, the carrier of R holds b₃ . (a,u) = a * u );

definition

let R be Ring;
let n be Nat;

func R ^* n -> strict ModuleStr over R means :DEF: :: VECTSP13:def 7
( the carrier of it = n -tuples_on the carrier of R & the addF of it = vector_add (n,R) & the ZeroF of it = n |-> (0. R) & the lmult of it = vector_mult (n,R) );

existence
ex b₁ being strict ModuleStr over R st
( the carrier of b₁ = n -tuples_on the carrier of R & the addF of b₁ = vector_add (n,R) & the ZeroF of b₁ = n |-> (0. R) & the lmult of b₁ = vector_mult (n,R) )

proof end;

uniqueness
for b₁, b₂ being strict ModuleStr over R st the carrier of b₁ = n -tuples_on the carrier of R & the addF of b₁ = vector_add (n,R) & the ZeroF of b₁ = n |-> (0. R) & the lmult of b₁ = vector_mult (n,R) & the carrier of b₂ = n -tuples_on the carrier of R & the addF of b₂ = vector_add (n,R) & the ZeroF of b₂ = n |-> (0. R) & the lmult of b₂ = vector_mult (n,R) holds
b₁ = b₂ ;

end;

:: deftheorem DEF defines ^* VECTSP13:def 7 :
for R being Ring
for n being Nat
for b₃ being strict ModuleStr over R holds
( b₃ = R ^* n iff ( the carrier of b₃ = n -tuples_on the carrier of R & the addF of b₃ = vector_add (n,R) & the ZeroF of b₃ = n |-> (0. R) & the lmult of b₃ = vector_mult (n,R) ) );

registration

let R be Ring;
let n be Nat;

cluster R ^* n -> non empty strict ;

coherence
not R ^* n is empty

proof end;

end;

registration

let R be Ring;
let n be Nat;

cluster R ^* n -> right_complementable Abelian add-associative right_zeroed strict ;

coherence
( R ^* n is Abelian & R ^* n is add-associative & R ^* n is right_zeroed & R ^* n is right_complementable )

proof end;

end;

registration

let R be Ring;
let n be Nat;

cluster R ^* n -> strict vector-distributive scalar-distributive scalar-associative ;

coherence
( R ^* n is scalar-distributive & R ^* n is scalar-associative & R ^* n is vector-distributive )

proof end;

end;

registration

let R be commutative Ring;
let n be Nat;

cluster R ^* n -> strict scalar-unital ;

coherence
R ^* n is scalar-unital

proof end;

end;

definition

let R be Ring;
let n, i be Nat;

func i _th_unit_vector (n,R) -> Element of n -tuples_on the carrier of R equals :: VECTSP13:def 8
Replace ((n |-> (0. R)),i,(1. R));

coherence
Replace ((n |-> (0. R)),i,(1. R)) is Element of n -tuples_on the carrier of R

proof end;

end;

:: deftheorem defines _th_unit_vector VECTSP13:def 8 :
for R being Ring
for n, i being Nat holds i _th_unit_vector (n,R) = Replace ((n |-> (0. R)),i,(1. R));

theorem u1: :: VECTSP13:23

for R being Ring
for n, i being Nat st 1 <= i & i <= n holds
( (i _th_unit_vector (n,R)) . i = 1. R & ( for j being Nat st 1 <= j & j <= n & j <> i holds
(i _th_unit_vector (n,R)) . j = 0. R ) )

proof end;

theorem u2: :: VECTSP13:24

for R being non degenerated Ring
for n, i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n holds
( i _th_unit_vector (n,R) = j _th_unit_vector (n,R) iff i = j )

proof end;

definition

let R be Ring;
let n be Nat;

func Base (R,n) -> Subset of (R ^* n) equals :: VECTSP13:def 9
{ (i _th_unit_vector (n,R)) where i is Nat : ( 1 <= i & i <= n ) } ;

coherence
{ (i _th_unit_vector (n,R)) where i is Nat : ( 1 <= i & i <= n ) } is Subset of (R ^* n)

proof end;

end;

:: deftheorem defines Base VECTSP13:def 9 :
for R being Ring
for n being Nat holds Base (R,n) = { (i _th_unit_vector (n,R)) where i is Nat : ( 1 <= i & i <= n ) } ;

registration

let R be Ring;
let n be Nat;

cluster Base (R,n) -> finite ;

coherence
Base (R,n) is finite

proof end;

end;

theorem cardB: :: VECTSP13:25

for R being non degenerated Ring
for n being Nat holds card (Base (R,n)) = n

proof end;

lemBB: for R being Ring
for n being Nat
for u being Element of (R ^* n)
for v being Element of n -tuples_on the carrier of R
for a being Element of R st u = v holds
a * u = a * v

proof end;

lemBA: for R being Ring
for n being Nat
for v being Element of n -tuples_on the carrier of R
for a being Element of R
for i being Nat st 1 <= i & i <= n holds
( (a * (i _th_unit_vector (n,R))) . i = a & ( for j being Nat st j <> i & 1 <= j & j <= n holds
(a * (j _th_unit_vector (n,R))) . i = 0. R ) )

proof end;

lemBC: for R being Ring
for n being Nat
for u, v being Element of (R ^* n)
for a, b being Element of n -tuples_on the carrier of R st u = a & v = b holds
a + b = u + v

proof end;

theorem lemBase: :: VECTSP13:26

for R being non degenerated commutative Ring
for n being Nat
for l being Linear_Combination of Base (R,n)
for v being Tuple of n, the carrier of R
for i being Nat st v = Sum l & 1 <= i & i <= n holds
v . i = l . (i _th_unit_vector (n,R))

proof end;

registration

let R be non degenerated commutative Ring;
let n be Nat;

cluster Base (R,n) -> linearly-independent ;

coherence
Base (R,n) is linearly-independent

proof end;

end;

lemspan1: for R being non degenerated commutative Ring
for n being Nat
for o being Element of (R ^* n) ex l being Linear_Combination of Base (R,n) st Sum l = o

proof end;

theorem lemspan: :: VECTSP13:27

for R being non degenerated commutative Ring
for n being Nat holds Lin (Base (R,n)) = R ^* n

proof end;

registration

let R be non degenerated commutative Ring;
let n be Nat;

cluster Base (R,n) -> base ;

coherence
Base (R,n) is base

proof end;

end;

registration

let F be Field;
let n be Nat;

cluster F ^* n -> strict finite-dimensional ;

coherence
F ^* n is finite-dimensional

proof end;

end;

theorem DimF: :: VECTSP13:28

for F being Field
for n being Nat holds dim (F ^* n) = n

proof end;

definition

let R be Ring;
let U, V be VectSp of R;

pred U,V are_isomorphic means :: VECTSP13:def 10
ex T being linear-transformation of U,V st T is bijective ;

end;

:: deftheorem defines are_isomorphic VECTSP13:def 10 :
for R being Ring
for U, V being VectSp of R holds
( U,V are_isomorphic iff ex T being linear-transformation of U,V st T is bijective );

theorem UisoV: :: VECTSP13:29

for F being Field
for U, V being finite-dimensional VectSp of F holds
( U,V are_isomorphic iff dim U = dim V )

proof end;

theorem :: VECTSP13:30

for F being Field
for U being finite-dimensional VectSp of F holds U,F ^* (dim U) are_isomorphic

proof end;

theorem Fin1: :: VECTSP13:31

for R being finite Ring
for n being Nat holds card the carrier of (R ^* n) = (card the carrier of R) |^ n

proof end;

registration

let R be finite Ring;
let n be Nat;

cluster R ^* n -> finite strict ;

coherence
R ^* n is finite

proof end;

end;

definition

let X be non empty set ;
let L be non empty addLoopStr ;
let f, g be Function of X,L;

func f '+' g -> Function of X,L means :defp: :: VECTSP13:def 11
for x being Element of X holds it . x = (f . x) + (g . x);

existence
ex b₁ being Function of X,L st
for x being Element of X holds b₁ . x = (f . x) + (g . x)

proof end;

uniqueness
for b₁, b₂ being Function of X,L st ( for x being Element of X holds b₁ . x = (f . x) + (g . x) ) & ( for x being Element of X holds b₂ . x = (f . x) + (g . x) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defp defines '+' VECTSP13:def 11 :
for X being non empty set
for L being non empty addLoopStr
for f, g, b₅ being Function of X,L holds
( b₅ = f '+' g iff for x being Element of X holds b₅ . x = (f . x) + (g . x) );

definition

let X be non empty set ;
let L be non empty Abelian addLoopStr ;
let f, g be Function of X,L;
:: original: '+'
redefine func f '+' g -> Function of X,L;
commutativity
for f, g being Function of X,L holds f '+' g = g '+' f

proof end;

end;

definition

let X be non empty set ;
let L be non empty addLoopStr ;
let f be Function of X,L;

func '-' f -> Function of X,L means :defm: :: VECTSP13:def 12
for x being Element of X holds it . x = - (f . x);

existence
ex b₁ being Function of X,L st
for x being Element of X holds b₁ . x = - (f . x)

proof end;

uniqueness
for b₁, b₂ being Function of X,L st ( for x being Element of X holds b₁ . x = - (f . x) ) & ( for x being Element of X holds b₂ . x = - (f . x) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defm defines '-' VECTSP13:def 12 :
for X being non empty set
for L being non empty addLoopStr
for f, b₄ being Function of X,L holds
( b₄ = '-' f iff for x being Element of X holds b₄ . x = - (f . x) );

definition

let X be non empty set ;
let L be non empty multLoopStr ;
let f be Function of X,L;
let a be Element of L;

func a '*' f -> Function of X,L means :defmu: :: VECTSP13:def 13
for x being Element of X holds it . x = a * (f . x);

existence
ex b₁ being Function of X,L st
for x being Element of X holds b₁ . x = a * (f . x)

proof end;

uniqueness
for b₁, b₂ being Function of X,L st ( for x being Element of X holds b₁ . x = a * (f . x) ) & ( for x being Element of X holds b₂ . x = a * (f . x) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defmu defines '*' VECTSP13:def 13 :
for X being non empty set
for L being non empty multLoopStr
for f being Function of X,L
for a being Element of L
for b₅ being Function of X,L holds
( b₅ = a '*' f iff for x being Element of X holds b₅ . x = a * (f . x) );

registration

let X be non empty set ;
let L be non empty left_unital multLoopStr ;
let f be Function of X,L;

reduce (1. L) '*' f to f;

reducibility
(1. L) '*' f = f

proof end;

end;

theorem ass: :: VECTSP13:32

for X being non empty set
for L being non empty add-associative addLoopStr
for f, g, h being Function of X,L holds (f '+' g) '+' h = f '+' (g '+' h)

proof end;

theorem rc: :: VECTSP13:33

for X being non empty set
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for f being Function of X,L holds f '+' ('-' f) = X --> (0. L)

proof end;

theorem sd: :: VECTSP13:34

for X being non empty set
for L being non empty left-distributive doubleLoopStr
for a, b being Element of L
for f being Function of X,L holds (a + b) '*' f = (a '*' f) '+' (b '*' f)

proof end;

theorem sa: :: VECTSP13:35

for X being non empty set
for L being non empty associative multLoopStr
for a, b being Element of L
for f being Function of X,L holds (a * b) '*' f = a '*' (b '*' f)

proof end;

theorem vd: :: VECTSP13:36

for X being non empty set
for L being non empty right-distributive doubleLoopStr
for a being Element of L
for f, g being Function of X,L holds a '*' (f '+' g) = (a '*' f) '+' (a '*' g)

proof end;

definition

let X be non empty set ;
let L be non empty addLoopStr ;

func mapAdd (X,L) -> BinOp of (Funcs (X, the carrier of L)) means :dA: :: VECTSP13:def 14
for f, g being Function of X,L holds it . (f,g) = f '+' g;

existence
ex b₁ being BinOp of (Funcs (X, the carrier of L)) st
for f, g being Function of X,L holds b₁ . (f,g) = f '+' g

proof end;

uniqueness
for b₁, b₂ being BinOp of (Funcs (X, the carrier of L)) st ( for f, g being Function of X,L holds b₁ . (f,g) = f '+' g ) & ( for f, g being Function of X,L holds b₂ . (f,g) = f '+' g ) holds
b₁ = b₂

proof end;

end;

:: deftheorem dA defines mapAdd VECTSP13:def 14 :
for X being non empty set
for L being non empty addLoopStr
for b₃ being BinOp of (Funcs (X, the carrier of L)) holds
( b₃ = mapAdd (X,L) iff for f, g being Function of X,L holds b₃ . (f,g) = f '+' g );

definition

let X be non empty set ;
let L be non empty multLoopStr ;

func mapMult (X,L) -> Function of [: the carrier of L,(Funcs (X, the carrier of L)):],(Funcs (X, the carrier of L)) means :dM: :: VECTSP13:def 15
for f being Function of X,L
for a being Element of L holds it . (a,f) = a '*' f;

existence
ex b₁ being Function of [: the carrier of L,(Funcs (X, the carrier of L)):],(Funcs (X, the carrier of L)) st
for f being Function of X,L
for a being Element of L holds b₁ . (a,f) = a '*' f

proof end;

uniqueness
for b₁, b₂ being Function of [: the carrier of L,(Funcs (X, the carrier of L)):],(Funcs (X, the carrier of L)) st ( for f being Function of X,L
for a being Element of L holds b₁ . (a,f) = a '*' f ) & ( for f being Function of X,L
for a being Element of L holds b₂ . (a,f) = a '*' f ) holds
b₁ = b₂

proof end;

end;

:: deftheorem dM defines mapMult VECTSP13:def 15 :
for X being non empty set
for L being non empty multLoopStr
for b₃ being Function of [: the carrier of L,(Funcs (X, the carrier of L)):],(Funcs (X, the carrier of L)) holds
( b₃ = mapMult (X,L) iff for f being Function of X,L
for a being Element of L holds b₃ . (a,f) = a '*' f );

definition

let X be non empty set ;
let L be non empty doubleLoopStr ;

func Maps (X,L) -> strict ModuleStr over L means :defmap: :: VECTSP13:def 16
( the carrier of it = Funcs (X, the carrier of L) & the addF of it = mapAdd (X,L) & the ZeroF of it = X --> (0. L) & the lmult of it = mapMult (X,L) );

existence
ex b₁ being strict ModuleStr over L st
( the carrier of b₁ = Funcs (X, the carrier of L) & the addF of b₁ = mapAdd (X,L) & the ZeroF of b₁ = X --> (0. L) & the lmult of b₁ = mapMult (X,L) )

proof end;

uniqueness
for b₁, b₂ being strict ModuleStr over L st the carrier of b₁ = Funcs (X, the carrier of L) & the addF of b₁ = mapAdd (X,L) & the ZeroF of b₁ = X --> (0. L) & the lmult of b₁ = mapMult (X,L) & the carrier of b₂ = Funcs (X, the carrier of L) & the addF of b₂ = mapAdd (X,L) & the ZeroF of b₂ = X --> (0. L) & the lmult of b₂ = mapMult (X,L) holds
b₁ = b₂ ;

end;

:: deftheorem defmap defines Maps VECTSP13:def 16 :
for X being non empty set
for L being non empty doubleLoopStr
for b₃ being strict ModuleStr over L holds
( b₃ = Maps (X,L) iff ( the carrier of b₃ = Funcs (X, the carrier of L) & the addF of b₃ = mapAdd (X,L) & the ZeroF of b₃ = X --> (0. L) & the lmult of b₃ = mapMult (X,L) ) );

definition

let X, L be non empty doubleLoopStr ;

func Maps (X,L) -> object equals :: VECTSP13:def 17
Maps ( the carrier of X,L);

coherence
Maps ( the carrier of X,L) is object ;

end;

:: deftheorem defines Maps VECTSP13:def 17 :
for X, L being non empty doubleLoopStr holds Maps (X,L) = Maps ( the carrier of X,L);

registration

let X be non empty set ;
let L be non empty doubleLoopStr ;

cluster Maps (X,L) -> non empty strict ;

coherence
not Maps (X,L) is empty

proof end;

end;

registration

let X be non empty set ;
let L be non empty Abelian doubleLoopStr ;

cluster Maps (X,L) -> Abelian strict ;

coherence
Maps (X,L) is Abelian

proof end;

end;

registration

let X be non empty set ;
let L be non empty add-associative doubleLoopStr ;

cluster Maps (X,L) -> add-associative strict ;

coherence
Maps (X,L) is add-associative

proof end;

end;

registration

let X be non empty set ;
let L be non empty right_zeroed doubleLoopStr ;

cluster Maps (X,L) -> right_zeroed strict ;

coherence
Maps (X,L) is right_zeroed

proof end;

end;

registration

let X be non empty set ;
let L be non empty right_complementable add-associative right_zeroed doubleLoopStr ;

cluster Maps (X,L) -> right_complementable strict ;

coherence
Maps (X,L) is right_complementable

proof end;

end;

registration

let X be non empty set ;
let L be non empty left-distributive doubleLoopStr ;

cluster Maps (X,L) -> strict scalar-distributive ;

coherence
Maps (X,L) is scalar-distributive

proof end;

end;

registration

let X be non empty set ;
let L be non empty associative doubleLoopStr ;

cluster Maps (X,L) -> strict scalar-associative ;

coherence
Maps (X,L) is scalar-associative

proof end;

end;

registration

let X be non empty set ;
let L be non empty right-distributive doubleLoopStr ;

cluster Maps (X,L) -> strict vector-distributive ;

coherence
Maps (X,L) is vector-distributive

proof end;

end;

registration

let X be non empty set ;
let L be non empty left_unital doubleLoopStr ;

cluster Maps (X,L) -> strict scalar-unital ;

coherence
Maps (X,L) is scalar-unital

proof end;

end;

definition

let X be non empty set ;
let R be non empty 1-sorted ;
let L be non empty ModuleStr over R;
let f be Function of X,L;
let a be Element of R;

func a '*' f -> Function of X,L means :defmu: :: VECTSP13:def 18
for x being Element of X holds it . x = a * (f . x);

existence
ex b₁ being Function of X,L st
for x being Element of X holds b₁ . x = a * (f . x)

proof end;

uniqueness
for b₁, b₂ being Function of X,L st ( for x being Element of X holds b₁ . x = a * (f . x) ) & ( for x being Element of X holds b₂ . x = a * (f . x) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defmu defines '*' VECTSP13:def 18 :
for X being non empty set
for R being non empty 1-sorted
for L being non empty ModuleStr over R
for f being Function of X,L
for a being Element of R
for b₆ being Function of X,L holds
( b₆ = a '*' f iff for x being Element of X holds b₆ . x = a * (f . x) );

registration

let X be non empty set ;
let R be Ring;
let L be non empty scalar-unital ModuleStr over R;
let f be Function of X,L;

reduce (1. R) '*' f to f;

reducibility
(1. R) '*' f = f

proof end;

end;

theorem sd: :: VECTSP13:37

for X being non empty set
for R being Ring
for L being non empty scalar-distributive ModuleStr over R
for a, b being Element of R
for f being Function of X,L holds (a + b) '*' f = (a '*' f) '+' (b '*' f)

proof end;

theorem sa: :: VECTSP13:38

for X being non empty set
for R being Ring
for L being non empty scalar-associative ModuleStr over R
for a, b being Element of R
for f being Function of X,L holds (a * b) '*' f = a '*' (b '*' f)

proof end;

theorem vd: :: VECTSP13:39

for X being non empty set
for R being Ring
for L being non empty vector-distributive ModuleStr over R
for a, b being Element of R
for f, g being Function of X,L holds a '*' (f '+' g) = (a '*' f) '+' (a '*' g)

proof end;

definition

let X be non empty set ;
let R be non empty addLoopStr ;
let L be non empty ModuleStr over R;

func mapAdd (X,L) -> BinOp of (Funcs (X, the carrier of L)) means :dA: :: VECTSP13:def 19
for f, g being Function of X,L holds it . (f,g) = f '+' g;

existence
ex b₁ being BinOp of (Funcs (X, the carrier of L)) st
for f, g being Function of X,L holds b₁ . (f,g) = f '+' g

proof end;

uniqueness
for b₁, b₂ being BinOp of (Funcs (X, the carrier of L)) st ( for f, g being Function of X,L holds b₁ . (f,g) = f '+' g ) & ( for f, g being Function of X,L holds b₂ . (f,g) = f '+' g ) holds
b₁ = b₂

proof end;

end;

:: deftheorem dA defines mapAdd VECTSP13:def 19 :
for X being non empty set
for R being non empty addLoopStr
for L being non empty ModuleStr over R
for b₄ being BinOp of (Funcs (X, the carrier of L)) holds
( b₄ = mapAdd (X,L) iff for f, g being Function of X,L holds b₄ . (f,g) = f '+' g );

definition

let X be non empty set ;
let R be non empty multLoopStr ;
let L be non empty ModuleStr over R;

func mapMult (X,L) -> Function of [: the carrier of R,(Funcs (X, the carrier of L)):],(Funcs (X, the carrier of L)) means :dM: :: VECTSP13:def 20
for f being Function of X,L
for a being Element of R holds it . (a,f) = a '*' f;

existence
ex b₁ being Function of [: the carrier of R,(Funcs (X, the carrier of L)):],(Funcs (X, the carrier of L)) st
for f being Function of X,L
for a being Element of R holds b₁ . (a,f) = a '*' f

proof end;

uniqueness
for b₁, b₂ being Function of [: the carrier of R,(Funcs (X, the carrier of L)):],(Funcs (X, the carrier of L)) st ( for f being Function of X,L
for a being Element of R holds b₁ . (a,f) = a '*' f ) & ( for f being Function of X,L
for a being Element of R holds b₂ . (a,f) = a '*' f ) holds
b₁ = b₂

proof end;

end;

:: deftheorem dM defines mapMult VECTSP13:def 20 :
for X being non empty set
for R being non empty multLoopStr
for L being non empty ModuleStr over R
for b₄ being Function of [: the carrier of R,(Funcs (X, the carrier of L)):],(Funcs (X, the carrier of L)) holds
( b₄ = mapMult (X,L) iff for f being Function of X,L
for a being Element of R holds b₄ . (a,f) = a '*' f );

definition

let X be non empty set ;
let R be non empty doubleLoopStr ;
let L be non empty ModuleStr over R;

func Maps (X,L) -> strict ModuleStr over R means :defmap: :: VECTSP13:def 21
( the carrier of it = Funcs (X, the carrier of L) & the addF of it = mapAdd (X,L) & the ZeroF of it = X --> (0. L) & the lmult of it = mapMult (X,L) );

existence
ex b₁ being strict ModuleStr over R st
( the carrier of b₁ = Funcs (X, the carrier of L) & the addF of b₁ = mapAdd (X,L) & the ZeroF of b₁ = X --> (0. L) & the lmult of b₁ = mapMult (X,L) )

proof end;

uniqueness
for b₁, b₂ being strict ModuleStr over R st the carrier of b₁ = Funcs (X, the carrier of L) & the addF of b₁ = mapAdd (X,L) & the ZeroF of b₁ = X --> (0. L) & the lmult of b₁ = mapMult (X,L) & the carrier of b₂ = Funcs (X, the carrier of L) & the addF of b₂ = mapAdd (X,L) & the ZeroF of b₂ = X --> (0. L) & the lmult of b₂ = mapMult (X,L) holds
b₁ = b₂ ;

end;

:: deftheorem defmap defines Maps VECTSP13:def 21 :
for X being non empty set
for R being non empty doubleLoopStr
for L being non empty ModuleStr over R
for b₄ being strict ModuleStr over R holds
( b₄ = Maps (X,L) iff ( the carrier of b₄ = Funcs (X, the carrier of L) & the addF of b₄ = mapAdd (X,L) & the ZeroF of b₄ = X --> (0. L) & the lmult of b₄ = mapMult (X,L) ) );

definition

let R be non empty doubleLoopStr ;
let L1, L2 be non empty ModuleStr over R;

func Maps (L1,L2) -> object equals :: VECTSP13:def 22
Maps ( the carrier of L1,L2);

coherence
Maps ( the carrier of L1,L2) is object ;

end;

:: deftheorem defines Maps VECTSP13:def 22 :
for R being non empty doubleLoopStr
for L1, L2 being non empty ModuleStr over R holds Maps (L1,L2) = Maps ( the carrier of L1,L2);

registration

let X be non empty set ;
let R be non empty doubleLoopStr ;
let L be non empty ModuleStr over R;

cluster Maps (X,L) -> non empty strict ;

coherence
not Maps (X,L) is empty

proof end;

end;

registration

let X be non empty set ;
let R be Ring;
let L be non empty Abelian ModuleStr over R;

cluster Maps (X,L) -> Abelian strict ;

coherence
Maps (X,L) is Abelian

proof end;

end;

registration

let X be non empty set ;
let R be Ring;
let L be non empty add-associative ModuleStr over R;

cluster Maps (X,L) -> add-associative strict ;

coherence
Maps (X,L) is add-associative

proof end;

end;

registration

let X be non empty set ;
let R be Ring;
let L be non empty right_zeroed ModuleStr over R;

cluster Maps (X,L) -> right_zeroed strict ;

coherence
Maps (X,L) is right_zeroed

proof end;

end;

registration

let X be non empty set ;
let R be Ring;
let L be non empty right_complementable add-associative right_zeroed ModuleStr over R;

cluster Maps (X,L) -> right_complementable strict ;

coherence
Maps (X,L) is right_complementable

proof end;

end;

registration

let X be non empty set ;
let R be Ring;
let L be non empty scalar-distributive ModuleStr over R;

cluster Maps (X,L) -> strict scalar-distributive ;

coherence
Maps (X,L) is scalar-distributive

proof end;

end;

registration

let X be non empty set ;
let R be Ring;
let L be non empty scalar-associative ModuleStr over R;

cluster Maps (X,L) -> strict scalar-associative ;

coherence
Maps (X,L) is scalar-associative

proof end;

end;

registration

let X be non empty set ;
let R be Ring;
let L be non empty vector-distributive ModuleStr over R;

cluster Maps (X,L) -> strict vector-distributive ;

coherence
Maps (X,L) is vector-distributive

proof end;

end;

registration

let X be non empty set ;
let R be Ring;
let L be non empty scalar-unital ModuleStr over R;

cluster Maps (X,L) -> strict scalar-unital ;

coherence
Maps (X,L) is scalar-unital

proof end;

end;

definition

let R be Ring;
let U, V be VectSp of R;
:: original: Maps
redefine func Maps (U,V) -> VectSp of R;
coherence
Maps (U,V) is VectSp of R ;

end;

theorem LT1: :: VECTSP13:40

for R being commutative Ring
for U, V being VectSp of R
for f, g being linear-transformation of U,V holds f '+' g is linear-transformation of U,V

proof end;

theorem LT2: :: VECTSP13:41

for R being commutative Ring
for U, V being VectSp of R
for f being linear-transformation of U,V
for a being Element of R holds a '*' f is linear-transformation of U,V

proof end;

definition

let F be Field;
let U, V be VectSp of F;

func LinTrans (U,V) -> strict Subspace of Maps (U,V) means :: VECTSP13:def 23
the carrier of it = { f where f is linear-transformation of U,V : verum } ;

existence
ex b₁ being strict Subspace of Maps (U,V) st the carrier of b₁ = { f where f is linear-transformation of U,V : verum }

proof end;

uniqueness
for b₁, b₂ being strict Subspace of Maps (U,V) st the carrier of b₁ = { f where f is linear-transformation of U,V : verum } & the carrier of b₂ = { f where f is linear-transformation of U,V : verum } holds
b₁ = b₂ by VECTSP_4:29;

end;

:: deftheorem defines LinTrans VECTSP13:def 23 :
for F being Field
for U, V being VectSp of F
for b₄ being strict Subspace of Maps (U,V) holds
( b₄ = LinTrans (U,V) iff the carrier of b₄ = { f where f is linear-transformation of U,V : verum } );

definition

let F be Field;
let V be VectSp of F;

func End V -> Subspace of Maps (V,V) equals :: VECTSP13:def 24
LinTrans (V,V);

coherence
LinTrans (V,V) is Subspace of Maps (V,V) ;

end;

:: deftheorem defines End VECTSP13:def 24 :
for F being Field
for V being VectSp of F holds End V = LinTrans (V,V);