:: Linear Combinations in Real Linear Space
:: by Wojciech A. Trybulec
::
:: Received April 8, 1990
:: Copyright (c) 1990-2015 Association of Mizar Users
definition
let
S
be
1-sorted
;
let
x
be
set
;
assume
A1
:
x
in
S
;
func
vector
(
S
,
x
)
->
Element
of
S
equals
:
Def1
:
:: RLVECT_2:def 1
x
;
coherence
x
is
Element
of
S
by
A1
;
end;
::
deftheorem
Def1
defines
vector
RLVECT_2:def 1 :
for
S
being
1-sorted
for
x
being
set
st
x
in
S
holds
vector
(
S
,
x
)
=
x
;
theorem
:: RLVECT_2:1
for
S
being non
empty
1-sorted
for
v
being
Element
of
S
holds
vector
(
S
,
v
)
=
v
by
Def1
,
RLVECT_1:1
;
theorem
Th2
:
:: RLVECT_2:2
for
V
being non
empty
right_complementable
Abelian
add-associative
right_zeroed
addLoopStr
for
F
,
G
,
H
being
FinSequence
of the
carrier
of
V
st
len
F
=
len
G
&
len
F
=
len
H
& ( for
k
being
Nat
st
k
in
dom
F
holds
H
.
k
=
(
F
/.
k
)
+
(
G
/.
k
)
) holds
Sum
H
=
(
Sum
F
)
+
(
Sum
G
)
proof
end;
theorem
:: RLVECT_2:3
for
V
being
RealLinearSpace
for
a
being
Real
for
F
,
G
being
FinSequence
of
V
st
len
F
=
len
G
& ( for
k
being
Nat
st
k
in
dom
F
holds
G
.
k
=
a
*
(
F
/.
k
)
) holds
Sum
G
=
a
*
(
Sum
F
)
proof
end;
theorem
Th4
:
:: RLVECT_2:4
for
V
being non
empty
right_complementable
Abelian
add-associative
right_zeroed
addLoopStr
for
F
,
G
being
FinSequence
of the
carrier
of
V
st
len
F
=
len
G
& ( for
k
being
Nat
st
k
in
dom
F
holds
G
.
k
=
-
(
F
/.
k
)
) holds
Sum
G
=
-
(
Sum
F
)
proof
end;
theorem
:: RLVECT_2:5
for
V
being non
empty
right_complementable
Abelian
add-associative
right_zeroed
addLoopStr
for
F
,
G
,
H
being
FinSequence
of the
carrier
of
V
st
len
F
=
len
G
&
len
F
=
len
H
& ( for
k
being
Nat
st
k
in
dom
F
holds
H
.
k
=
(
F
/.
k
)
-
(
G
/.
k
)
) holds
Sum
H
=
(
Sum
F
)
-
(
Sum
G
)
proof
end;
theorem
Th6
:
:: RLVECT_2:6
for
V
being non
empty
right_complementable
Abelian
add-associative
right_zeroed
addLoopStr
for
F
,
G
being
FinSequence
of the
carrier
of
V
for
f
being
Permutation
of
(
dom
F
)
st
len
F
=
len
G
& ( for
i
being
Nat
st
i
in
dom
G
holds
G
.
i
=
F
.
(
f
.
i
)
) holds
Sum
F
=
Sum
G
proof
end;
theorem
:: RLVECT_2:7
for
V
being non
empty
right_complementable
Abelian
add-associative
right_zeroed
addLoopStr
for
F
,
G
being
FinSequence
of the
carrier
of
V
for
f
being
Permutation
of
(
dom
F
)
st
G
=
F
*
f
holds
Sum
F
=
Sum
G
proof
end;
definition
let
V
be non
empty
addLoopStr
;
let
T
be
finite
Subset
of
V
;
assume
A1
: (
V
is
Abelian
&
V
is
add-associative
&
V
is
right_zeroed
) ;
func
Sum
T
->
Element
of
V
means
:
Def2
:
:: RLVECT_2:def 2
ex
F
being
FinSequence
of the
carrier
of
V
st
(
rng
F
=
T
&
F
is
one-to-one
&
it
=
Sum
F
);
existence
ex
b
1
being
Element
of
V
ex
F
being
FinSequence
of the
carrier
of
V
st
(
rng
F
=
T
&
F
is
one-to-one
&
b
1
=
Sum
F
)
proof
end;
uniqueness
for
b
1
,
b
2
being
Element
of
V
st ex
F
being
FinSequence
of the
carrier
of
V
st
(
rng
F
=
T
&
F
is
one-to-one
&
b
1
=
Sum
F
) & ex
F
being
FinSequence
of the
carrier
of
V
st
(
rng
F
=
T
&
F
is
one-to-one
&
b
2
=
Sum
F
) holds
b
1
=
b
2
by
A1
,
RLVECT_1:42
;
end;
::
deftheorem
Def2
defines
Sum
RLVECT_2:def 2 :
for
V
being non
empty
addLoopStr
for
T
being
finite
Subset
of
V
st
V
is
Abelian
&
V
is
add-associative
&
V
is
right_zeroed
holds
for
b
3
being
Element
of
V
holds
(
b
3
=
Sum
T
iff ex
F
being
FinSequence
of the
carrier
of
V
st
(
rng
F
=
T
&
F
is
one-to-one
&
b
3
=
Sum
F
) );
theorem
Th8
:
:: RLVECT_2:8
for
V
being non
empty
Abelian
add-associative
right_zeroed
addLoopStr
holds
Sum
(
{}
V
)
=
0.
V
proof
end;
theorem
:: RLVECT_2:9
for
V
being non
empty
right_complementable
Abelian
add-associative
right_zeroed
addLoopStr
for
v
being
Element
of
V
holds
Sum
{
v
}
=
v
proof
end;
theorem
:: RLVECT_2:10
for
V
being non
empty
right_complementable
Abelian
add-associative
right_zeroed
addLoopStr
for
v1
,
v2
being
Element
of
V
st
v1
<>
v2
holds
Sum
{
v1
,
v2
}
=
v1
+
v2
proof
end;
theorem
:: RLVECT_2:11
for
V
being non
empty
right_complementable
Abelian
add-associative
right_zeroed
addLoopStr
for
v1
,
v2
,
v3
being
Element
of
V
st
v1
<>
v2
&
v2
<>
v3
&
v1
<>
v3
holds
Sum
{
v1
,
v2
,
v3
}
=
(
v1
+
v2
)
+
v3
proof
end;
theorem
Th12
:
:: RLVECT_2:12
for
V
being non
empty
Abelian
add-associative
right_zeroed
addLoopStr
for
S
,
T
being
finite
Subset
of
V
st
T
misses
S
holds
Sum
(
T
\/
S
)
=
(
Sum
T
)
+
(
Sum
S
)
proof
end;
theorem
Th13
:
:: RLVECT_2:13
for
V
being non
empty
right_complementable
Abelian
add-associative
right_zeroed
addLoopStr
for
S
,
T
being
finite
Subset
of
V
holds
Sum
(
T
\/
S
)
=
(
(
Sum
T
)
+
(
Sum
S
)
)
-
(
Sum
(
T
/\
S
)
)
proof
end;
theorem
:: RLVECT_2:14
for
V
being non
empty
right_complementable
Abelian
add-associative
right_zeroed
addLoopStr
for
S
,
T
being
finite
Subset
of
V
holds
Sum
(
T
/\
S
)
=
(
(
Sum
T
)
+
(
Sum
S
)
)
-
(
Sum
(
T
\/
S
)
)
proof
end;
theorem
Th15
:
:: RLVECT_2:15
for
V
being non
empty
right_complementable
Abelian
add-associative
right_zeroed
addLoopStr
for
S
,
T
being
finite
Subset
of
V
holds
Sum
(
T
\
S
)
=
(
Sum
(
T
\/
S
)
)
-
(
Sum
S
)
proof
end;
theorem
Th16
:
:: RLVECT_2:16
for
V
being non
empty
right_complementable
Abelian
add-associative
right_zeroed
addLoopStr
for
S
,
T
being
finite
Subset
of
V
holds
Sum
(
T
\
S
)
=
(
Sum
T
)
-
(
Sum
(
T
/\
S
)
)
proof
end;
theorem
:: RLVECT_2:17
for
V
being non
empty
right_complementable
Abelian
add-associative
right_zeroed
addLoopStr
for
S
,
T
being
finite
Subset
of
V
holds
Sum
(
T
\+\
S
)
=
(
Sum
(
T
\/
S
)
)
-
(
Sum
(
T
/\
S
)
)
proof
end;
theorem
:: RLVECT_2:18
for
V
being non
empty
Abelian
add-associative
right_zeroed
addLoopStr
for
S
,
T
being
finite
Subset
of
V
holds
Sum
(
T
\+\
S
)
=
(
Sum
(
T
\
S
)
)
+
(
Sum
(
S
\
T
)
)
by
Th12
,
XBOOLE_1:82
;
reconsider
zz
=
0
as
Element
of
REAL
by
XREAL_0:def 1
;
definition
let
V
be non
empty
ZeroStr
;
mode
Linear_Combination
of
V
->
Element
of
Funcs
( the
carrier
of
V
,
REAL
)
means
:
Def3
:
:: RLVECT_2:def 3
ex
T
being
finite
Subset
of
V
st
for
v
being
Element
of
V
st not
v
in
T
holds
it
.
v
=
0
;
existence
ex
b
1
being
Element
of
Funcs
( the
carrier
of
V
,
REAL
) ex
T
being
finite
Subset
of
V
st
for
v
being
Element
of
V
st not
v
in
T
holds
b
1
.
v
=
0
proof
end;
end;
::
deftheorem
Def3
defines
Linear_Combination
RLVECT_2:def 3 :
for
V
being non
empty
ZeroStr
for
b
2
being
Element
of
Funcs
( the
carrier
of
V
,
REAL
) holds
(
b
2
is
Linear_Combination
of
V
iff ex
T
being
finite
Subset
of
V
st
for
v
being
Element
of
V
st not
v
in
T
holds
b
2
.
v
=
0
);
notation
let
V
be non
empty
addLoopStr
;
let
L
be
Element
of
Funcs
( the
carrier
of
V
,
REAL
);
synonym
Carrier
L
for
support
V
;
end;
Lm1
:
now
:: thesis:
for
V
being non
empty
addLoopStr
for
L
being
Element
of
Funcs
( the
carrier
of
V
,
REAL
) holds
Carrier
c=
the
carrier
of
V
let
V
be non
empty
addLoopStr
;
:: thesis:
for
L
being
Element
of
Funcs
( the
carrier
of
V
,
REAL
) holds
Carrier
c=
the
carrier
of
V
let
L
be
Element
of
Funcs
( the
carrier
of
V
,
REAL
);
:: thesis:
Carrier
c=
the
carrier
of
V
A1
:
support
L
c=
dom
L
by
PRE_POLY:37
;
thus
Carrier
c=
the
carrier
of
V
:: thesis:
verum
proof
let
x
be
object
;
:: according to
TARSKI:def 3
:: thesis:
( not
x
in
Carrier
or
x
in
the
carrier
of
V
)
assume
x
in
support
L
;
:: thesis:
x
in
the
carrier
of
V
then
x
in
dom
L
by
A1
;
hence
x
in
the
carrier
of
V
;
:: thesis:
verum
end;
end;
definition
let
V
be non
empty
addLoopStr
;
let
L
be
Element
of
Funcs
( the
carrier
of
V
,
REAL
);
:: original:
Carrier
redefine
func
Carrier
L
->
Subset
of
V
equals
:: RLVECT_2:def 4
{
v
where
v
is
Element
of
V
:
L
.
v
<>
0
}
;
coherence
Carrier
is
Subset
of
V
by
Lm1
;
compatibility
for
b
1
being
Subset
of
V
holds
(
b
1
=
Carrier
iff
b
1
=
{
v
where
v
is
Element
of
V
:
L
.
v
<>
0
}
)
proof
end;
end;
::
deftheorem
defines
Carrier
RLVECT_2:def 4 :
for
V
being non
empty
addLoopStr
for
L
being
Element
of
Funcs
( the
carrier
of
V
,
REAL
) holds
Carrier
L
=
{
v
where
v
is
Element
of
V
:
L
.
v
<>
0
}
;
registration
let
V
be non
empty
addLoopStr
;
let
L
be
Linear_Combination
of
V
;
cluster
Carrier
->
finite
;
coherence
Carrier
L
is
finite
proof
end;
end;
theorem
:: RLVECT_2:19
for
V
being non
empty
addLoopStr
for
L
being
Linear_Combination
of
V
for
v
being
Element
of
V
holds
(
L
.
v
=
0
iff not
v
in
Carrier
L
)
proof
end;
definition
let
V
be non
empty
addLoopStr
;
func
ZeroLC
V
->
Linear_Combination
of
V
means
:
Def5
:
:: RLVECT_2:def 5
Carrier
it
=
{}
;
existence
ex
b
1
being
Linear_Combination
of
V
st
Carrier
b
1
=
{}
proof
end;
uniqueness
for
b
1
,
b
2
being
Linear_Combination
of
V
st
Carrier
b
1
=
{}
&
Carrier
b
2
=
{}
holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def5
defines
ZeroLC
RLVECT_2:def 5 :
for
V
being non
empty
addLoopStr
for
b
2
being
Linear_Combination
of
V
holds
(
b
2
=
ZeroLC
V
iff
Carrier
b
2
=
{}
);
theorem
Th20
:
:: RLVECT_2:20
for
V
being non
empty
addLoopStr
for
v
being
Element
of
V
holds
(
ZeroLC
V
)
.
v
=
0
proof
end;
definition
let
V
be non
empty
addLoopStr
;
let
A
be
Subset
of
V
;
mode
Linear_Combination
of
A
->
Linear_Combination
of
V
means
:
Def6
:
:: RLVECT_2:def 6
Carrier
it
c=
A
;
existence
ex
b
1
being
Linear_Combination
of
V
st
Carrier
b
1
c=
A
proof
end;
end;
::
deftheorem
Def6
defines
Linear_Combination
RLVECT_2:def 6 :
for
V
being non
empty
addLoopStr
for
A
being
Subset
of
V
for
b
3
being
Linear_Combination
of
V
holds
(
b
3
is
Linear_Combination
of
A
iff
Carrier
b
3
c=
A
);
theorem
:: RLVECT_2:21
for
V
being
RealLinearSpace
for
A
,
B
being
Subset
of
V
for
l
being
Linear_Combination
of
A
st
A
c=
B
holds
l
is
Linear_Combination
of
B
proof
end;
theorem
Th22
:
:: RLVECT_2:22
for
V
being
RealLinearSpace
for
A
being
Subset
of
V
holds
ZeroLC
V
is
Linear_Combination
of
A
proof
end;
theorem
Th23
:
:: RLVECT_2:23
for
V
being
RealLinearSpace
for
l
being
Linear_Combination
of
{}
the
carrier
of
V
holds
l
=
ZeroLC
V
proof
end;
definition
let
V
be
RealLinearSpace
;
let
F
be
FinSequence
of
V
;
let
f
be
Function
of the
carrier
of
V
,
REAL
;
func
f
(#)
F
->
FinSequence
of the
carrier
of
V
means
:
Def7
:
:: RLVECT_2:def 7
(
len
it
=
len
F
& ( for
i
being
Nat
st
i
in
dom
it
holds
it
.
i
=
(
f
.
(
F
/.
i
)
)
*
(
F
/.
i
)
) );
existence
ex
b
1
being
FinSequence
of the
carrier
of
V
st
(
len
b
1
=
len
F
& ( for
i
being
Nat
st
i
in
dom
b
1
holds
b
1
.
i
=
(
f
.
(
F
/.
i
)
)
*
(
F
/.
i
)
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
FinSequence
of the
carrier
of
V
st
len
b
1
=
len
F
& ( for
i
being
Nat
st
i
in
dom
b
1
holds
b
1
.
i
=
(
f
.
(
F
/.
i
)
)
*
(
F
/.
i
)
) &
len
b
2
=
len
F
& ( for
i
being
Nat
st
i
in
dom
b
2
holds
b
2
.
i
=
(
f
.
(
F
/.
i
)
)
*
(
F
/.
i
)
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def7
defines
(#)
RLVECT_2:def 7 :
for
V
being
RealLinearSpace
for
F
being
FinSequence
of
V
for
f
being
Function
of the
carrier
of
V
,
REAL
for
b
4
being
FinSequence
of the
carrier
of
V
holds
(
b
4
=
f
(#)
F
iff (
len
b
4
=
len
F
& ( for
i
being
Nat
st
i
in
dom
b
4
holds
b
4
.
i
=
(
f
.
(
F
/.
i
)
)
*
(
F
/.
i
)
) ) );
theorem
Th24
:
:: RLVECT_2:24
for
i
being
Nat
for
V
being
RealLinearSpace
for
v
being
VECTOR
of
V
for
F
being
FinSequence
of
V
for
f
being
Function
of the
carrier
of
V
,
REAL
st
i
in
dom
F
&
v
=
F
.
i
holds
(
f
(#)
F
)
.
i
=
(
f
.
v
)
*
v
proof
end;
theorem
:: RLVECT_2:25
for
V
being
RealLinearSpace
for
f
being
Function
of the
carrier
of
V
,
REAL
holds
f
(#)
(
<*>
the
carrier
of
V
)
=
<*>
the
carrier
of
V
proof
end;
theorem
Th26
:
:: RLVECT_2:26
for
V
being
RealLinearSpace
for
v
being
VECTOR
of
V
for
f
being
Function
of the
carrier
of
V
,
REAL
holds
f
(#)
<*
v
*>
=
<*
(
(
f
.
v
)
*
v
)
*>
proof
end;
theorem
Th27
:
:: RLVECT_2:27
for
V
being
RealLinearSpace
for
v1
,
v2
being
VECTOR
of
V
for
f
being
Function
of the
carrier
of
V
,
REAL
holds
f
(#)
<*
v1
,
v2
*>
=
<*
(
(
f
.
v1
)
*
v1
)
,
(
(
f
.
v2
)
*
v2
)
*>
proof
end;
theorem
:: RLVECT_2:28
for
V
being
RealLinearSpace
for
v1
,
v2
,
v3
being
VECTOR
of
V
for
f
being
Function
of the
carrier
of
V
,
REAL
holds
f
(#)
<*
v1
,
v2
,
v3
*>
=
<*
(
(
f
.
v1
)
*
v1
)
,
(
(
f
.
v2
)
*
v2
)
,
(
(
f
.
v3
)
*
v3
)
*>
proof
end;
definition
let
V
be
RealLinearSpace
;
let
L
be
Linear_Combination
of
V
;
func
Sum
L
->
Element
of
V
means
:
Def8
:
:: RLVECT_2:def 8
ex
F
being
FinSequence
of
V
st
(
F
is
one-to-one
&
rng
F
=
Carrier
L
&
it
=
Sum
(
L
(#)
F
)
);
existence
ex
b
1
being
Element
of
V
ex
F
being
FinSequence
of
V
st
(
F
is
one-to-one
&
rng
F
=
Carrier
L
&
b
1
=
Sum
(
L
(#)
F
)
)
proof
end;
uniqueness
for
b
1
,
b
2
being
Element
of
V
st ex
F
being
FinSequence
of
V
st
(
F
is
one-to-one
&
rng
F
=
Carrier
L
&
b
1
=
Sum
(
L
(#)
F
)
) & ex
F
being
FinSequence
of
V
st
(
F
is
one-to-one
&
rng
F
=
Carrier
L
&
b
2
=
Sum
(
L
(#)
F
)
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def8
defines
Sum
RLVECT_2:def 8 :
for
V
being
RealLinearSpace
for
L
being
Linear_Combination
of
V
for
b
3
being
Element
of
V
holds
(
b
3
=
Sum
L
iff ex
F
being
FinSequence
of
V
st
(
F
is
one-to-one
&
rng
F
=
Carrier
L
&
b
3
=
Sum
(
L
(#)
F
)
) );
Lm2
:
for
V
being
RealLinearSpace
holds
Sum
(
ZeroLC
V
)
=
0.
V
proof
end;
theorem
:: RLVECT_2:29
for
V
being
RealLinearSpace
for
A
being
Subset
of
V
holds
( (
A
<>
{}
&
A
is
linearly-closed
) iff for
l
being
Linear_Combination
of
A
holds
Sum
l
in
A
)
proof
end;
theorem
:: RLVECT_2:30
for
V
being
RealLinearSpace
holds
Sum
(
ZeroLC
V
)
=
0.
V
by
Lm2
;
theorem
:: RLVECT_2:31
for
V
being
RealLinearSpace
for
l
being
Linear_Combination
of
{}
the
carrier
of
V
holds
Sum
l
=
0.
V
proof
end;
theorem
Th32
:
:: RLVECT_2:32
for
V
being
RealLinearSpace
for
v
being
VECTOR
of
V
for
l
being
Linear_Combination
of
{
v
}
holds
Sum
l
=
(
l
.
v
)
*
v
proof
end;
theorem
Th33
:
:: RLVECT_2:33
for
V
being
RealLinearSpace
for
v1
,
v2
being
VECTOR
of
V
st
v1
<>
v2
holds
for
l
being
Linear_Combination
of
{
v1
,
v2
}
holds
Sum
l
=
(
(
l
.
v1
)
*
v1
)
+
(
(
l
.
v2
)
*
v2
)
proof
end;
theorem
:: RLVECT_2:34
for
V
being
RealLinearSpace
for
L
being
Linear_Combination
of
V
st
Carrier
L
=
{}
holds
Sum
L
=
0.
V
proof
end;
theorem
:: RLVECT_2:35
for
V
being
RealLinearSpace
for
v
being
VECTOR
of
V
for
L
being
Linear_Combination
of
V
st
Carrier
L
=
{
v
}
holds
Sum
L
=
(
L
.
v
)
*
v
proof
end;
theorem
:: RLVECT_2:36
for
V
being
RealLinearSpace
for
v1
,
v2
being
VECTOR
of
V
for
L
being
Linear_Combination
of
V
st
Carrier
L
=
{
v1
,
v2
}
&
v1
<>
v2
holds
Sum
L
=
(
(
L
.
v1
)
*
v1
)
+
(
(
L
.
v2
)
*
v2
)
proof
end;
definition
let
V
be non
empty
addLoopStr
;
let
L1
,
L2
be
Linear_Combination
of
V
;
:: original:
=
redefine
pred
L1
=
L2
means
:: RLVECT_2:def 9
for
v
being
Element
of
V
holds
L1
.
v
=
L2
.
v
;
compatibility
(
L1
=
L2
iff for
v
being
Element
of
V
holds
L1
.
v
=
L2
.
v
)
;
end;
::
deftheorem
defines
=
RLVECT_2:def 9 :
for
V
being non
empty
addLoopStr
for
L1
,
L2
being
Linear_Combination
of
V
holds
(
L1
=
L2
iff for
v
being
Element
of
V
holds
L1
.
v
=
L2
.
v
);
definition
let
V
be non
empty
addLoopStr
;
let
L1
,
L2
be
Linear_Combination
of
V
;
:: original:
+
redefine
func
L1
+
L2
->
Linear_Combination
of
V
means
:
Def10
:
:: RLVECT_2:def 10
for
v
being
Element
of
V
holds
it
.
v
=
(
L1
.
v
)
+
(
L2
.
v
)
;
coherence
L1
+
L2
is
Linear_Combination
of
V
proof
end;
compatibility
for
b
1
being
Linear_Combination
of
V
holds
(
b
1
=
L1
+
L2
iff for
v
being
Element
of
V
holds
b
1
.
v
=
(
L1
.
v
)
+
(
L2
.
v
)
)
proof
end;
end;
::
deftheorem
Def10
defines
+
RLVECT_2:def 10 :
for
V
being non
empty
addLoopStr
for
L1
,
L2
,
b
4
being
Linear_Combination
of
V
holds
(
b
4
=
L1
+
L2
iff for
v
being
Element
of
V
holds
b
4
.
v
=
(
L1
.
v
)
+
(
L2
.
v
)
);
theorem
Th37
:
:: RLVECT_2:37
for
V
being
RealLinearSpace
for
L1
,
L2
being
Linear_Combination
of
V
holds
Carrier
(
L1
+
L2
)
c=
(
Carrier
L1
)
\/
(
Carrier
L2
)
proof
end;
theorem
Th38
:
:: RLVECT_2:38
for
V
being
RealLinearSpace
for
A
being
Subset
of
V
for
L1
,
L2
being
Linear_Combination
of
V
st
L1
is
Linear_Combination
of
A
&
L2
is
Linear_Combination
of
A
holds
L1
+
L2
is
Linear_Combination
of
A
proof
end;
theorem
:: RLVECT_2:39
for
V
being non
empty
addLoopStr
for
L1
,
L2
being
Linear_Combination
of
V
holds
L1
+
L2
=
L2
+
L1
;
theorem
Th40
:
:: RLVECT_2:40
for
V
being
RealLinearSpace
for
L1
,
L2
,
L3
being
Linear_Combination
of
V
holds
L1
+
(
L2
+
L3
)
=
(
L1
+
L2
)
+
L3
proof
end;
theorem
Th41
:
:: RLVECT_2:41
for
V
being
RealLinearSpace
for
L
being
Linear_Combination
of
V
holds
(
L
+
(
ZeroLC
V
)
=
L
&
(
ZeroLC
V
)
+
L
=
L
)
proof
end;
definition
let
V
be
RealLinearSpace
;
let
a
be
Real
;
let
L
be
Linear_Combination
of
V
;
func
a
*
L
->
Linear_Combination
of
V
means
:
Def11
:
:: RLVECT_2:def 11
for
v
being
VECTOR
of
V
holds
it
.
v
=
a
*
(
L
.
v
)
;
existence
ex
b
1
being
Linear_Combination
of
V
st
for
v
being
VECTOR
of
V
holds
b
1
.
v
=
a
*
(
L
.
v
)
proof
end;
uniqueness
for
b
1
,
b
2
being
Linear_Combination
of
V
st ( for
v
being
VECTOR
of
V
holds
b
1
.
v
=
a
*
(
L
.
v
)
) & ( for
v
being
VECTOR
of
V
holds
b
2
.
v
=
a
*
(
L
.
v
)
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def11
defines
*
RLVECT_2:def 11 :
for
V
being
RealLinearSpace
for
a
being
Real
for
L
,
b
4
being
Linear_Combination
of
V
holds
(
b
4
=
a
*
L
iff for
v
being
VECTOR
of
V
holds
b
4
.
v
=
a
*
(
L
.
v
)
);
theorem
Th42
:
:: RLVECT_2:42
for
V
being
RealLinearSpace
for
a
being
Real
for
L
being
Linear_Combination
of
V
st
a
<>
0
holds
Carrier
(
a
*
L
)
=
Carrier
L
proof
end;
theorem
Th43
:
:: RLVECT_2:43
for
V
being
RealLinearSpace
for
L
being
Linear_Combination
of
V
holds
0
*
L
=
ZeroLC
V
proof
end;
theorem
Th44
:
:: RLVECT_2:44
for
V
being
RealLinearSpace
for
a
being
Real
for
A
being
Subset
of
V
for
L
being
Linear_Combination
of
V
st
L
is
Linear_Combination
of
A
holds
a
*
L
is
Linear_Combination
of
A
proof
end;
theorem
Th45
:
:: RLVECT_2:45
for
V
being
RealLinearSpace
for
a
,
b
being
Real
for
L
being
Linear_Combination
of
V
holds
(
a
+
b
)
*
L
=
(
a
*
L
)
+
(
b
*
L
)
proof
end;
theorem
Th46
:
:: RLVECT_2:46
for
V
being
RealLinearSpace
for
a
being
Real
for
L1
,
L2
being
Linear_Combination
of
V
holds
a
*
(
L1
+
L2
)
=
(
a
*
L1
)
+
(
a
*
L2
)
proof
end;
theorem
Th47
:
:: RLVECT_2:47
for
V
being
RealLinearSpace
for
a
,
b
being
Real
for
L
being
Linear_Combination
of
V
holds
a
*
(
b
*
L
)
=
(
a
*
b
)
*
L
proof
end;
theorem
Th48
:
:: RLVECT_2:48
for
V
being
RealLinearSpace
for
L
being
Linear_Combination
of
V
holds 1
*
L
=
L
proof
end;
definition
let
V
be
RealLinearSpace
;
let
L
be
Linear_Combination
of
V
;
func
-
L
->
Linear_Combination
of
V
equals
:: RLVECT_2:def 12
(
-
1
)
*
L
;
correctness
coherence
(
-
1
)
*
L
is
Linear_Combination
of
V
;
;
end;
::
deftheorem
defines
-
RLVECT_2:def 12 :
for
V
being
RealLinearSpace
for
L
being
Linear_Combination
of
V
holds
-
L
=
(
-
1
)
*
L
;
theorem
Th49
:
:: RLVECT_2:49
for
V
being
RealLinearSpace
for
v
being
VECTOR
of
V
for
L
being
Linear_Combination
of
V
holds
(
-
L
)
.
v
=
-
(
L
.
v
)
proof
end;
theorem
:: RLVECT_2:50
for
V
being
RealLinearSpace
for
L1
,
L2
being
Linear_Combination
of
V
st
L1
+
L2
=
ZeroLC
V
holds
L2
=
-
L1
proof
end;
theorem
:: RLVECT_2:51
for
V
being
RealLinearSpace
for
L
being
Linear_Combination
of
V
holds
Carrier
(
-
L
)
=
Carrier
L
by
Th42
;
theorem
:: RLVECT_2:52
for
V
being
RealLinearSpace
for
A
being
Subset
of
V
for
L
being
Linear_Combination
of
V
st
L
is
Linear_Combination
of
A
holds
-
L
is
Linear_Combination
of
A
by
Th44
;
theorem
:: RLVECT_2:53
for
V
being
RealLinearSpace
for
L
being
Linear_Combination
of
V
holds
-
(
-
L
)
=
L
proof
end;
definition
let
V
be
RealLinearSpace
;
let
L1
,
L2
be
Linear_Combination
of
V
;
func
L1
-
L2
->
Linear_Combination
of
V
equals
:: RLVECT_2:def 13
L1
+
(
-
L2
)
;
correctness
coherence
L1
+
(
-
L2
)
is
Linear_Combination
of
V
;
;
end;
::
deftheorem
defines
-
RLVECT_2:def 13 :
for
V
being
RealLinearSpace
for
L1
,
L2
being
Linear_Combination
of
V
holds
L1
-
L2
=
L1
+
(
-
L2
)
;
theorem
Th54
:
:: RLVECT_2:54
for
V
being
RealLinearSpace
for
v
being
VECTOR
of
V
for
L1
,
L2
being
Linear_Combination
of
V
holds
(
L1
-
L2
)
.
v
=
(
L1
.
v
)
-
(
L2
.
v
)
proof
end;
theorem
:: RLVECT_2:55
for
V
being
RealLinearSpace
for
L1
,
L2
being
Linear_Combination
of
V
holds
Carrier
(
L1
-
L2
)
c=
(
Carrier
L1
)
\/
(
Carrier
L2
)
proof
end;
theorem
:: RLVECT_2:56
for
V
being
RealLinearSpace
for
A
being
Subset
of
V
for
L1
,
L2
being
Linear_Combination
of
V
st
L1
is
Linear_Combination
of
A
&
L2
is
Linear_Combination
of
A
holds
L1
-
L2
is
Linear_Combination
of
A
proof
end;
theorem
Th57
:
:: RLVECT_2:57
for
V
being
RealLinearSpace
for
L
being
Linear_Combination
of
V
holds
L
-
L
=
ZeroLC
V
proof
end;
definition
let
V
be
RealLinearSpace
;
func
LinComb
V
->
set
means
:
Def14
:
:: RLVECT_2:def 14
for
x
being
set
holds
(
x
in
it
iff
x
is
Linear_Combination
of
V
);
existence
ex
b
1
being
set
st
for
x
being
set
holds
(
x
in
b
1
iff
x
is
Linear_Combination
of
V
)
proof
end;
uniqueness
for
b
1
,
b
2
being
set
st ( for
x
being
set
holds
(
x
in
b
1
iff
x
is
Linear_Combination
of
V
) ) & ( for
x
being
set
holds
(
x
in
b
2
iff
x
is
Linear_Combination
of
V
) ) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def14
defines
LinComb
RLVECT_2:def 14 :
for
V
being
RealLinearSpace
for
b
2
being
set
holds
(
b
2
=
LinComb
V
iff for
x
being
set
holds
(
x
in
b
2
iff
x
is
Linear_Combination
of
V
) );
registration
let
V
be
RealLinearSpace
;
cluster
LinComb
V
->
non
empty
;
coherence
not
LinComb
V
is
empty
proof
end;
end;
definition
let
V
be
RealLinearSpace
;
let
e
be
Element
of
LinComb
V
;
func
@
e
->
Linear_Combination
of
V
equals
:: RLVECT_2:def 15
e
;
coherence
e
is
Linear_Combination
of
V
by
Def14
;
end;
::
deftheorem
defines
@
RLVECT_2:def 15 :
for
V
being
RealLinearSpace
for
e
being
Element
of
LinComb
V
holds
@
e
=
e
;
definition
let
V
be
RealLinearSpace
;
let
L
be
Linear_Combination
of
V
;
func
@
L
->
Element
of
LinComb
V
equals
:: RLVECT_2:def 16
L
;
coherence
L
is
Element
of
LinComb
V
by
Def14
;
end;
::
deftheorem
defines
@
RLVECT_2:def 16 :
for
V
being
RealLinearSpace
for
L
being
Linear_Combination
of
V
holds
@
L
=
L
;
definition
let
V
be
RealLinearSpace
;
func
LCAdd
V
->
BinOp
of
(
LinComb
V
)
means
:
Def17
:
:: RLVECT_2:def 17
for
e1
,
e2
being
Element
of
LinComb
V
holds
it
.
(
e1
,
e2
)
=
(
@
e1
)
+
(
@
e2
)
;
existence
ex
b
1
being
BinOp
of
(
LinComb
V
)
st
for
e1
,
e2
being
Element
of
LinComb
V
holds
b
1
.
(
e1
,
e2
)
=
(
@
e1
)
+
(
@
e2
)
proof
end;
uniqueness
for
b
1
,
b
2
being
BinOp
of
(
LinComb
V
)
st ( for
e1
,
e2
being
Element
of
LinComb
V
holds
b
1
.
(
e1
,
e2
)
=
(
@
e1
)
+
(
@
e2
)
) & ( for
e1
,
e2
being
Element
of
LinComb
V
holds
b
2
.
(
e1
,
e2
)
=
(
@
e1
)
+
(
@
e2
)
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def17
defines
LCAdd
RLVECT_2:def 17 :
for
V
being
RealLinearSpace
for
b
2
being
BinOp
of
(
LinComb
V
)
holds
(
b
2
=
LCAdd
V
iff for
e1
,
e2
being
Element
of
LinComb
V
holds
b
2
.
(
e1
,
e2
)
=
(
@
e1
)
+
(
@
e2
)
);
definition
let
V
be
RealLinearSpace
;
func
LCMult
V
->
Function
of
[:
REAL
,
(
LinComb
V
)
:]
,
(
LinComb
V
)
means
:
Def18
:
:: RLVECT_2:def 18
for
a
being
Real
for
e
being
Element
of
LinComb
V
holds
it
.
[
a
,
e
]
=
a
*
(
@
e
)
;
existence
ex
b
1
being
Function
of
[:
REAL
,
(
LinComb
V
)
:]
,
(
LinComb
V
)
st
for
a
being
Real
for
e
being
Element
of
LinComb
V
holds
b
1
.
[
a
,
e
]
=
a
*
(
@
e
)
proof
end;
uniqueness
for
b
1
,
b
2
being
Function
of
[:
REAL
,
(
LinComb
V
)
:]
,
(
LinComb
V
)
st ( for
a
being
Real
for
e
being
Element
of
LinComb
V
holds
b
1
.
[
a
,
e
]
=
a
*
(
@
e
)
) & ( for
a
being
Real
for
e
being
Element
of
LinComb
V
holds
b
2
.
[
a
,
e
]
=
a
*
(
@
e
)
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def18
defines
LCMult
RLVECT_2:def 18 :
for
V
being
RealLinearSpace
for
b
2
being
Function
of
[:
REAL
,
(
LinComb
V
)
:]
,
(
LinComb
V
)
holds
(
b
2
=
LCMult
V
iff for
a
being
Real
for
e
being
Element
of
LinComb
V
holds
b
2
.
[
a
,
e
]
=
a
*
(
@
e
)
);
definition
let
V
be
RealLinearSpace
;
func
LC_RLSpace
V
->
RLSStruct
equals
:: RLVECT_2:def 19
RLSStruct
(#
(
LinComb
V
)
,
(
@
(
ZeroLC
V
)
)
,
(
LCAdd
V
)
,
(
LCMult
V
)
#);
coherence
RLSStruct
(#
(
LinComb
V
)
,
(
@
(
ZeroLC
V
)
)
,
(
LCAdd
V
)
,
(
LCMult
V
)
#) is
RLSStruct
;
end;
::
deftheorem
defines
LC_RLSpace
RLVECT_2:def 19 :
for
V
being
RealLinearSpace
holds
LC_RLSpace
V
=
RLSStruct
(#
(
LinComb
V
)
,
(
@
(
ZeroLC
V
)
)
,
(
LCAdd
V
)
,
(
LCMult
V
)
#);
registration
let
V
be
RealLinearSpace
;
cluster
LC_RLSpace
V
->
non
empty
strict
;
coherence
(
LC_RLSpace
V
is
strict
& not
LC_RLSpace
V
is
empty
)
;
end;
registration
let
V
be
RealLinearSpace
;
cluster
LC_RLSpace
V
->
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
;
coherence
(
LC_RLSpace
V
is
Abelian
&
LC_RLSpace
V
is
add-associative
&
LC_RLSpace
V
is
right_zeroed
&
LC_RLSpace
V
is
right_complementable
&
LC_RLSpace
V
is
vector-distributive
&
LC_RLSpace
V
is
scalar-distributive
&
LC_RLSpace
V
is
scalar-associative
&
LC_RLSpace
V
is
scalar-unital
)
proof
end;
end;
theorem
:: RLVECT_2:58
for
V
being
RealLinearSpace
holds the
carrier
of
(
LC_RLSpace
V
)
=
LinComb
V
;
theorem
:: RLVECT_2:59
for
V
being
RealLinearSpace
holds
0.
(
LC_RLSpace
V
)
=
ZeroLC
V
;
theorem
:: RLVECT_2:60
for
V
being
RealLinearSpace
holds the
addF
of
(
LC_RLSpace
V
)
=
LCAdd
V
;
theorem
:: RLVECT_2:61
for
V
being
RealLinearSpace
holds the
Mult
of
(
LC_RLSpace
V
)
=
LCMult
V
;
theorem
Th62
:
:: RLVECT_2:62
for
V
being
RealLinearSpace
for
L1
,
L2
being
Linear_Combination
of
V
holds
(
vector
(
(
LC_RLSpace
V
)
,
L1
)
)
+
(
vector
(
(
LC_RLSpace
V
)
,
L2
)
)
=
L1
+
L2
proof
end;
theorem
Th63
:
:: RLVECT_2:63
for
V
being
RealLinearSpace
for
a
being
Real
for
L
being
Linear_Combination
of
V
holds
a
*
(
vector
(
(
LC_RLSpace
V
)
,
L
)
)
=
a
*
L
proof
end;
theorem
Th64
:
:: RLVECT_2:64
for
V
being
RealLinearSpace
for
L
being
Linear_Combination
of
V
holds
-
(
vector
(
(
LC_RLSpace
V
)
,
L
)
)
=
-
L
proof
end;
theorem
:: RLVECT_2:65
for
V
being
RealLinearSpace
for
L1
,
L2
being
Linear_Combination
of
V
holds
(
vector
(
(
LC_RLSpace
V
)
,
L1
)
)
-
(
vector
(
(
LC_RLSpace
V
)
,
L2
)
)
=
L1
-
L2
proof
end;
definition
let
V
be
RealLinearSpace
;
let
A
be
Subset
of
V
;
func
LC_RLSpace
A
->
strict
Subspace
of
LC_RLSpace
V
means
:: RLVECT_2:def 20
the
carrier
of
it
=
{
l
where
l
is
Linear_Combination
of
A
: verum
}
;
existence
ex
b
1
being
strict
Subspace
of
LC_RLSpace
V
st the
carrier
of
b
1
=
{
l
where
l
is
Linear_Combination
of
A
: verum
}
proof
end;
uniqueness
for
b
1
,
b
2
being
strict
Subspace
of
LC_RLSpace
V
st the
carrier
of
b
1
=
{
l
where
l
is
Linear_Combination
of
A
: verum
}
& the
carrier
of
b
2
=
{
l
where
l
is
Linear_Combination
of
A
: verum
}
holds
b
1
=
b
2
by
RLSUB_1:30
;
end;
::
deftheorem
defines
LC_RLSpace
RLVECT_2:def 20 :
for
V
being
RealLinearSpace
for
A
being
Subset
of
V
for
b
3
being
strict
Subspace
of
LC_RLSpace
V
holds
(
b
3
=
LC_RLSpace
A
iff the
carrier
of
b
3
=
{
l
where
l
is
Linear_Combination
of
A
: verum
}
);
theorem
Th66
:
:: RLVECT_2:66
for
R
being non
empty
right_complementable
Abelian
add-associative
right_zeroed
well-unital
distributive
associative
doubleLoopStr
for
a
being
Element
of
R
for
V
being non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
ModuleStr
over
R
for
F
,
G
being
FinSequence
of
V
st
len
F
=
len
G
& ( for
k
being
Nat
for
v
being
Element
of
V
st
k
in
dom
F
&
v
=
G
.
k
holds
F
.
k
=
a
*
v
) holds
Sum
F
=
a
*
(
Sum
G
)
proof
end;
theorem
:: RLVECT_2:67
for
R
being non
empty
right_complementable
Abelian
add-associative
right_zeroed
well-unital
distributive
associative
doubleLoopStr
for
a
being
Element
of
R
for
V
being non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
ModuleStr
over
R
for
F
,
G
being
FinSequence
of
V
st
len
F
=
len
G
& ( for
k
being
Nat
st
k
in
dom
F
holds
G
.
k
=
a
*
(
F
/.
k
)
) holds
Sum
G
=
a
*
(
Sum
F
)
proof
end;
theorem
:: RLVECT_2:68
for
R
being non
empty
right_complementable
Abelian
add-associative
right_zeroed
well-unital
distributive
associative
doubleLoopStr
for
V
being non
empty
right_complementable
Abelian
add-associative
right_zeroed
ModuleStr
over
R
for
F
,
G
,
H
being
FinSequence
of
V
st
len
F
=
len
G
&
len
F
=
len
H
& ( for
k
being
Nat
st
k
in
dom
F
holds
H
.
k
=
(
F
/.
k
)
-
(
G
/.
k
)
) holds
Sum
H
=
(
Sum
F
)
-
(
Sum
G
)
proof
end;
theorem
:: RLVECT_2:69
for
R
being non
empty
right_complementable
Abelian
add-associative
right_zeroed
well-unital
distributive
associative
doubleLoopStr
for
a
being
Element
of
R
for
V
being non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
ModuleStr
over
R
holds
a
*
(
Sum
(
<*>
the
carrier
of
V
)
)
=
0.
V
proof
end;
theorem
:: RLVECT_2:70
for
R
being non
empty
right_complementable
Abelian
add-associative
right_zeroed
well-unital
distributive
associative
doubleLoopStr
for
a
being
Element
of
R
for
V
being non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
ModuleStr
over
R
for
v
,
u
being
Element
of
V
holds
a
*
(
Sum
<*
v
,
u
*>
)
=
(
a
*
v
)
+
(
a
*
u
)
proof
end;
theorem
:: RLVECT_2:71
for
R
being non
empty
right_complementable
Abelian
add-associative
right_zeroed
well-unital
distributive
associative
doubleLoopStr
for
a
being
Element
of
R
for
V
being non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
ModuleStr
over
R
for
v
,
u
,
w
being
Element
of
V
holds
a
*
(
Sum
<*
v
,
u
,
w
*>
)
=
(
(
a
*
v
)
+
(
a
*
u
)
)
+
(
a
*
w
)
proof
end;