let X, Y, Z be RealLinearSpace; ex I being Function of [:X,Y,Z:],(product <*X,Y,Z*>) st
( I is one-to-one & I is onto & ( for x being Point of X
for y being Point of Y
for z being Point of Z holds I . (x,y,z) = <*x,y,z*> ) & ( for v, w being Point of [:X,Y,Z:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:X,Y,Z:]
for r being Real holds I . (r * v) = r * (I . v) ) & I . (0. [:X,Y,Z:]) = 0. (product <*X,Y,Z*>) )
set CarrX = the carrier of X;
set CarrY = the carrier of Y;
set CarrZ = the carrier of Z;
A1:
the carrier of [:X,Y,Z:] = [: the carrier of X, the carrier of Y, the carrier of Z:]
;
consider I being Function of [: the carrier of X, the carrier of Y, the carrier of Z:],(product <* the carrier of X, the carrier of Y, the carrier of Z*>) such that
A2:
( I is one-to-one & I is onto & ( for x, y, z being object st x in the carrier of X & y in the carrier of Y & z in the carrier of Z holds
I . (x,y,z) = <*x,y,z*> ) )
by Th5;
len (carr <*X,Y,Z*>) = len <*X,Y,Z*>
by PRVECT_1:def 11;
then A3:
len (carr <*X,Y,Z*>) = 3
by FINSEQ_1:45;
then A4:
dom (carr <*X,Y,Z*>) = {1,2,3}
by FINSEQ_1:def 3, FINSEQ_3:1;
len <*X,Y,Z*> = 3
by FINSEQ_1:45;
then A5:
dom <*X,Y,Z*> = {1,2,3}
by FINSEQ_1:def 3, FINSEQ_3:1;
A6:
( <*X,Y,Z*> . 1 = X & <*X,Y,Z*> . 2 = Y & <*X,Y,Z*> . 3 = Z )
;
( 1 in {1,2,3} & 2 in {1,2,3} & 3 in {1,2,3} )
by ENUMSET1:def 1;
then
( (carr <*X,Y,Z*>) . 1 = the carrier of X & (carr <*X,Y,Z*>) . 2 = the carrier of Y & (carr <*X,Y,Z*>) . 3 = the carrier of Z )
by A5, A6, PRVECT_1:def 11;
then A7:
carr <*X,Y,Z*> = <* the carrier of X, the carrier of Y, the carrier of Z*>
by A3, FINSEQ_1:45;
then reconsider I = I as Function of [:X,Y,Z:],(product <*X,Y,Z*>) ;
A8:
for x being Point of X
for y being Point of Y
for z being Point of Z holds I . (x,y,z) = <*x,y,z*>
by A2;
A9:
for v, w being Point of [:X,Y,Z:] holds I . (v + w) = (I . v) + (I . w)
proof
let v,
w be
Point of
[:X,Y,Z:];
I . (v + w) = (I . v) + (I . w)
A10:
the
carrier of
[:X,Y,Z:] = [: the carrier of X, the carrier of Y, the carrier of Z:]
;
consider x1 being
Point of
X,
y1 being
Point of
Y,
z1 being
Point of
Z such that A11:
v = [x1,y1,z1]
by A10, Lm1;
consider x2 being
Point of
X,
y2 being
Point of
Y,
z2 being
Point of
Z such that A12:
w = [x2,y2,z2]
by A10, Lm1;
(
I . v = I . (
x1,
y1,
z1) &
I . w = I . (
x2,
y2,
z2) )
by A11, A12;
then A13:
(
I . v = <*x1,y1,z1*> &
I . w = <*x2,y2,z2*> )
by A2;
A14:
I . (v + w) =
I . (
(x1 + x2),
(y1 + y2),
(z1 + z2))
by A11, A12, Th8
.=
<*(x1 + x2),(y1 + y2),(z1 + z2)*>
by A2
;
reconsider Iv =
I . v,
Iw =
I . w as
Element of
product (carr <*X,Y,Z*>) ;
reconsider j1 = 1,
j2 = 2,
j3 = 3 as
Element of
dom (carr <*X,Y,Z*>) by A4, ENUMSET1:def 1;
A16:
(addop <*X,Y,Z*>) . j1 = the
addF of
(<*X,Y,Z*> . j1)
by PRVECT_1:def 12;
A17:
([:(addop <*X,Y,Z*>):] . (Iv,Iw)) . j1 =
((addop <*X,Y,Z*>) . j1) . (
(Iv . j1),
(Iw . j1))
by PRVECT_1:def 8
.=
x1 + x2
by A16, A13
;
A18:
(addop <*X,Y,Z*>) . j2 = the
addF of
(<*X,Y,Z*> . j2)
by PRVECT_1:def 12;
A19:
(addop <*X,Y,Z*>) . j3 = the
addF of
(<*X,Y,Z*> . j3)
by PRVECT_1:def 12;
A20:
([:(addop <*X,Y,Z*>):] . (Iv,Iw)) . j2 =
((addop <*X,Y,Z*>) . j2) . (
(Iv . j2),
(Iw . j2))
by PRVECT_1:def 8
.=
y1 + y2
by A18, A13
;
A21:
([:(addop <*X,Y,Z*>):] . (Iv,Iw)) . j3 =
((addop <*X,Y,Z*>) . j3) . (
(Iv . j3),
(Iw . j3))
by PRVECT_1:def 8
.=
z1 + z2
by A19, A13
;
consider Ivw being
Function such that A22:
(
(I . v) + (I . w) = Ivw &
dom Ivw = dom (carr <*X,Y,Z*>) & ( for
i being
object st
i in dom (carr <*X,Y,Z*>) holds
Ivw . i in (carr <*X,Y,Z*>) . i ) )
by CARD_3:def 5;
A23:
dom Ivw = Seg 3
by A3, A22, FINSEQ_1:def 3;
then reconsider Ivw =
Ivw as
FinSequence by FINSEQ_1:def 2;
len Ivw = 3
by A23, FINSEQ_1:def 3;
hence
I . (v + w) = (I . v) + (I . w)
by A14, A22, A17, A20, A21, FINSEQ_1:45;
verum
end;
A24:
for v being Point of [:X,Y,Z:]
for r being Real holds I . (r * v) = r * (I . v)
proof
let v be
Point of
[:X,Y,Z:];
for r being Real holds I . (r * v) = r * (I . v)let r be
Real;
I . (r * v) = r * (I . v)
consider x1 being
Point of
X,
y1 being
Point of
Y,
z1 being
Point of
Z such that A25:
v = [x1,y1,z1]
by A1, Lm1;
A26:
I . v =
I . (
x1,
y1,
z1)
by A25
.=
<*x1,y1,z1*>
by A2
;
A27:
I . (r * v) =
I . (
(r * x1),
(r * y1),
(r * z1))
by A25, Th8
.=
<*(r * x1),(r * y1),(r * z1)*>
by A2
;
reconsider j1 = 1,
j2 = 2,
j3 = 3 as
Element of
dom (carr <*X,Y,Z*>) by A4, ENUMSET1:def 1;
A29:
(
(multop <*X,Y,Z*>) . j1 = the
Mult of
(<*X,Y,Z*> . j1) &
(multop <*X,Y,Z*>) . j2 = the
Mult of
(<*X,Y,Z*> . j2) &
(multop <*X,Y,Z*>) . j3 = the
Mult of
(<*X,Y,Z*> . j3) )
by PRVECT_2:def 8;
reconsider Iv =
I . v as
Element of
product (carr <*X,Y,Z*>) ;
reconsider rr =
r as
Element of
REAL by XREAL_0:def 1;
(
([:(multop <*X,Y,Z*>):] . (rr,Iv)) . j1 = ((multop <*X,Y,Z*>) . j1) . (
r,
(Iv . j1)) &
([:(multop <*X,Y,Z*>):] . (rr,Iv)) . j2 = ((multop <*X,Y,Z*>) . j2) . (
r,
(Iv . j2)) &
([:(multop <*X,Y,Z*>):] . (rr,Iv)) . j3 = ((multop <*X,Y,Z*>) . j3) . (
r,
(Iv . j3)) )
by PRVECT_2:def 2;
then A30:
(
([:(multop <*X,Y,Z*>):] . (rr,Iv)) . j1 = r * x1 &
([:(multop <*X,Y,Z*>):] . (rr,Iv)) . j2 = r * y1 &
([:(multop <*X,Y,Z*>):] . (rr,Iv)) . j3 = r * z1 )
by A29, A26;
consider Ivw being
Function such that A31:
(
r * (I . v) = Ivw &
dom Ivw = dom (carr <*X,Y,Z*>) & ( for
i being
object st
i in dom (carr <*X,Y,Z*>) holds
Ivw . i in (carr <*X,Y,Z*>) . i ) )
by CARD_3:def 5;
A32:
dom Ivw = Seg 3
by A3, A31, FINSEQ_1:def 3;
then reconsider Ivw =
Ivw as
FinSequence by FINSEQ_1:def 2;
len Ivw = 3
by A32, FINSEQ_1:def 3;
hence
I . (r * v) = r * (I . v)
by A27, A31, A30, FINSEQ_1:45;
verum
end;
I . (0. [:X,Y,Z:]) =
I . ((0. [:X,Y,Z:]) + (0. [:X,Y,Z:]))
.=
(I . (0. [:X,Y,Z:])) + (I . (0. [:X,Y,Z:]))
by A9
;
then (I . (0. [:X,Y,Z:])) - (I . (0. [:X,Y,Z:])) =
(I . (0. [:X,Y,Z:])) + ((I . (0. [:X,Y,Z:])) - (I . (0. [:X,Y,Z:])))
by RLVECT_1:28
.=
(I . (0. [:X,Y,Z:])) + (0. (product <*X,Y,Z*>))
by RLVECT_1:15
.=
I . (0. [:X,Y,Z:])
;
hence
ex I being Function of [:X,Y,Z:],(product <*X,Y,Z*>) st
( I is one-to-one & I is onto & ( for x being Point of X
for y being Point of Y
for z being Point of Z holds I . (x,y,z) = <*x,y,z*> ) & ( for v, w being Point of [:X,Y,Z:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:X,Y,Z:]
for r being Real holds I . (r * v) = r * (I . v) ) & I . (0. [:X,Y,Z:]) = 0. (product <*X,Y,Z*>) )
by A8, A9, A24, A2, A7, RLVECT_1:15; verum