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