let X be RealLinearSpace; ex I being Function of X,(product <*X*>) st
( I is one-to-one & I is onto & ( for x being Point of X holds I . x = <*x*> ) & ( for v, w being Point of X holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of X
for r being Element of REAL 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
P1:
( I is one-to-one & I is onto & ( for x being set st x in the carrier of X holds
I . x = <*x*> ) )
by Th002AB;
len (carr <*X*>) = len <*X*>
by PRVECT_2:def 4;
then Q0:
len (carr <*X*>) = 1
by FINSEQ_1:57;
Q2:
dom <*X*> = {1}
by FINSEQ_1:def 8, FINSEQ_1:4;
Q20:
<*X*> . 1 = X
by FINSEQ_1:def 8;
1 in {1}
by TARSKI:def 1;
then
(carr <*X*>) . 1 = the carrier of X
by Q2, Q20, PRVECT_2:def 4;
then P4:
carr <*X*> = <* the carrier of X*>
by Q0, FINSEQ_1:57;
then reconsider I = I as Function of X,(product <*X*>) ;
P2:
for x being Point of X holds I . x = <*x*>
by P1;
P5:
for v, w being Point of X holds I . (v + w) = (I . v) + (I . w)
proof
let v,
w be
Point of
X;
I . (v + w) = (I . v) + (I . w)
P55:
(
I . v = <*v*> &
I . w = <*w*> &
I . (v + w) = <*(v + w)*> )
by P1;
P58:
(
<*v*> . 1
= v &
<*w*> . 1
= w )
by FINSEQ_1:57;
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 Q0, FINSEQ_1:4, FINSEQ_1:def 3;
X1:
(addop <*X*>) . j1 = the
addF of
(<*X*> . j1)
by PRVECT_2:def 5;
X2:
([:(addop <*X*>):] . (Iv,Iw)) . j1 =
((addop <*X*>) . j1) . (
(Iv . j1),
(Iw . j1))
by PRVECT_1:def 10
.=
v + w
by X1, P55, P58, FINSEQ_1:57
;
consider Ivw being
Function such that XX1:
(
(I . v) + (I . w) = Ivw &
dom Ivw = dom (carr <*X*>) & ( for
i being
set st
i in dom (carr <*X*>) holds
Ivw . i in (carr <*X*>) . i ) )
by CARD_3:def 5;
X5:
dom Ivw = Seg 1
by Q0, XX1, FINSEQ_1:def 3;
then reconsider Ivw =
Ivw as
FinSequence by FINSEQ_1:def 2;
len Ivw = 1
by FINSEQ_1:def 3, X5;
hence
I . (v + w) = (I . v) + (I . w)
by P55, XX1, X2, FINSEQ_1:57;
verum
end;
P6:
for v being Point of X
for r being Element of REAL holds I . (r * v) = r * (I . v)
proof
let v be
Point of
X;
for r being Element of REAL holds I . (r * v) = r * (I . v)let r be
Element of
REAL ;
I . (r * v) = r * (I . v)
P55:
(
I . v = <*v*> &
I . (r * v) = <*(r * v)*> )
by P1;
P58:
<*v*> . 1
= v
by FINSEQ_1:57;
1
in {1}
by TARSKI:def 1;
then reconsider j1 = 1 as
Element of
dom (carr <*X*>) by Q0, FINSEQ_1:4, FINSEQ_1:def 3;
X1:
(multop <*X*>) . j1 = the
Mult of
(<*X*> . j1)
by PRVECT_2:def 8;
reconsider Iv =
I . v as
Element of
product (carr <*X*>) ;
X2:
([:(multop <*X*>):] . (r,Iv)) . j1 =
((multop <*X*>) . j1) . (
r,
(Iv . j1))
by PRVECT_2:def 2
.=
r * v
by X1, P55, P58, FINSEQ_1:57
;
consider Ivw being
Function such that XX1:
(
r * (I . v) = Ivw &
dom Ivw = dom (carr <*X*>) & ( for
i being
set st
i in dom (carr <*X*>) holds
Ivw . i in (carr <*X*>) . i ) )
by CARD_3:def 5;
X5:
dom Ivw = Seg 1
by Q0, XX1, FINSEQ_1:def 3;
then reconsider Ivw =
Ivw as
FinSequence by FINSEQ_1:def 2;
len Ivw = 1
by FINSEQ_1:def 3, X5;
hence
I . (r * v) = r * (I . v)
by P55, XX1, X2, FINSEQ_1:57;
verum
end;
I . (0. X) =
I . ((0. X) + (0. X))
by RLVECT_1:def 7
.=
(I . (0. X)) + (I . (0. X))
by P5
;
then (I . (0. X)) - (I . (0. X)) =
(I . (0. X)) + ((I . (0. X)) - (I . (0. X)))
by RLVECT_1:42
.=
(I . (0. X)) + (0. (product <*X*>))
by RLVECT_1:28
.=
I . (0. X)
by RLVECT_1:def 7
;
then
0. (product <*X*>) = I . (0. X)
by RLVECT_1:28;
hence
ex I being Function of X,(product <*X*>) st
( I is one-to-one & I is onto & ( for x being Point of X holds I . x = <*x*> ) & ( for v, w being Point of X holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of X
for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. X) = 0. (product <*X*>) )
by P1, P2, P4, P5, P6; verum