let K be Ring; for X being VectSp of K ex I being Function of X,(product <*X*>) st
( I is one-to-one & I is onto & ( for x being Vector of X holds I . x = <*x*> ) & ( for v, w being Vector of X holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Vector of X
for r being Element of the carrier of K holds I . (r * v) = r * (I . v) ) & I . (0. X) = 0. (product <*X*>) )
let X be VectSp of K; ex I being Function of X,(product <*X*>) st
( I is one-to-one & I is onto & ( for x being Vector of X holds I . x = <*x*> ) & ( for v, w being Vector of X holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Vector of X
for r being Element of the carrier of K holds I . (r * v) = r * (I . v) ) & I . (0. X) = 0. (product <*X*>) )
set CarrX = the carrier of X;
consider I being Function of the carrier of X,(product <* the carrier of X*>) such that
A1:
( I is one-to-one & I is onto & ( for x being object st x in the carrier of X holds
I . x = <*x*> ) )
by PRVECT_3:4;
len (carr <*X*>) = len <*X*>
by PRVECT_1:def 11;
then A2:
len (carr <*X*>) = 1
by FINSEQ_1:40;
A3:
dom <*X*> = {1}
by FINSEQ_1:2, FINSEQ_1:def 8;
A4:
<*X*> . 1 = X
by FINSEQ_1:def 8;
1 in {1}
by TARSKI:def 1;
then
(carr <*X*>) . 1 = the carrier of X
by A3, A4, PRVECT_1:def 11;
then A5:
carr <*X*> = <* the carrier of X*>
by A2, FINSEQ_1:40;
then reconsider I = I as Function of X,(product <*X*>) ;
A6:
for x being Vector of X holds I . x = <*x*>
by A1;
A7:
for v, w being Vector of X holds I . (v + w) = (I . v) + (I . w)
proof
let v,
w be
Vector of
X;
I . (v + w) = (I . v) + (I . w)
A8:
(
I . v = <*v*> &
I . w = <*w*> &
I . (v + w) = <*(v + w)*> )
by A1;
A9:
(
<*v*> . 1
= v &
<*w*> . 1
= w )
by FINSEQ_1:40;
reconsider Iv =
I . v,
Iw =
I . w as
Element of
product (carr <*X*>) ;
1
in {1}
by TARSKI:def 1;
then reconsider j1 = 1 as
Element of
dom (carr <*X*>) by A2, FINSEQ_1:2, FINSEQ_1:def 3;
A10:
(addop <*X*>) . j1 = the
addF of
(<*X*> . j1)
by PRVECT_1:def 12;
A11:
([:(addop <*X*>):] . (Iv,Iw)) . j1 =
((addop <*X*>) . j1) . (
(Iv . j1),
(Iw . j1))
by PRVECT_1:def 8
.=
v + w
by A10, A8, A9, FINSEQ_1:40
;
consider Ivw being
Function such that A12:
(
(I . v) + (I . w) = Ivw &
dom Ivw = dom (carr <*X*>) & ( for
i being
object st
i in dom (carr <*X*>) holds
Ivw . i in (carr <*X*>) . i ) )
by CARD_3:def 5;
A13:
dom Ivw = Seg 1
by A2, A12, FINSEQ_1:def 3;
then reconsider Ivw =
Ivw as
FinSequence by FINSEQ_1:def 2;
len Ivw = 1
by A13, FINSEQ_1:def 3;
hence
I . (v + w) = (I . v) + (I . w)
by A8, A12, A11, FINSEQ_1:40;
verum
end;
A14:
for v being Vector of X
for r being Element of the carrier of K holds I . (r * v) = r * (I . v)
proof
let v be
Vector of
X;
for r being Element of the carrier of K holds I . (r * v) = r * (I . v)let r be
Element of the
carrier of
K;
I . (r * v) = r * (I . v)
A15:
(
I . v = <*v*> &
I . (r * v) = <*(r * v)*> )
by A1;
A16:
<*v*> . 1
= v
by FINSEQ_1:40;
1
in {1}
by TARSKI:def 1;
then reconsider j1 = 1 as
Element of
dom (carr <*X*>) by A2, FINSEQ_1:2, FINSEQ_1:def 3;
A17:
(multop <*X*>) . j1 = the
lmult of
(<*X*> . j1)
by Def8;
reconsider Iv =
I . v as
Element of
product (carr <*X*>) ;
A18:
([:(multop <*X*>):] . (r,Iv)) . j1 =
((multop <*X*>) . j1) . (
r,
(Iv . j1))
by PRVECT_2:def 2
.=
r * v
by A17, A15, A16, FINSEQ_1:40
;
consider Ivw being
Function such that A19:
(
r * (I . v) = Ivw &
dom Ivw = dom (carr <*X*>) & ( for
i being
object st
i in dom (carr <*X*>) holds
Ivw . i in (carr <*X*>) . i ) )
by CARD_3:def 5;
A20:
dom Ivw = Seg 1
by A2, A19, FINSEQ_1:def 3;
then reconsider Ivw =
Ivw as
FinSequence by FINSEQ_1:def 2;
len Ivw = 1
by A20, FINSEQ_1:def 3;
hence
I . (r * v) = r * (I . v)
by A15, A19, A18, FINSEQ_1:40;
verum
end;
I . (0. X) =
I . ((0. X) + (0. X))
.=
(I . (0. X)) + (I . (0. X))
by A7
;
then (I . (0. X)) - (I . (0. X)) =
(I . (0. X)) + ((I . (0. X)) - (I . (0. X)))
by RLVECT_1:28
.=
(I . (0. X)) + (0. (product <*X*>))
by RLVECT_1:15
.=
I . (0. X)
;
hence
ex I being Function of X,(product <*X*>) st
( I is one-to-one & I is onto & ( for x being Vector of X holds I . x = <*x*> ) & ( for v, w being Vector of X holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Vector of X
for r being Element of the carrier of K holds I . (r * v) = r * (I . v) ) & I . (0. X) = 0. (product <*X*>) )
by A1, A6, A5, A7, A14, RLVECT_1:15; verum