let X, Y, Z be RealLinearSpace; :: thesis: 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 ) by FINSEQ_1:45;

( 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)

for r being Real holds I . (r * v) = r * (I . v)

.= (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; :: thesis: verum

( 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 ) by FINSEQ_1:45;

( 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

A24:
for v being Point of [:X,Y,Z:]
let v, w be Point of [:X,Y,Z:]; :: thesis: 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 ;

A15: ( <*x1,y1,z1*> . 1 = x1 & <*x2,y2,z2*> . 1 = x2 & <*x1,y1,z1*> . 2 = y1 & <*x2,y2,z2*> . 2 = y2 & <*x1,y1,z1*> . 3 = z1 & <*x2,y2,z2*> . 3 = z2 ) by FINSEQ_1:45;

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, A15, FINSEQ_1:45 ;

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, A15, FINSEQ_1:45 ;

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, A15, FINSEQ_1:45 ;

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; :: thesis: verum

end;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 ;

A15: ( <*x1,y1,z1*> . 1 = x1 & <*x2,y2,z2*> . 1 = x2 & <*x1,y1,z1*> . 2 = y1 & <*x2,y2,z2*> . 2 = y2 & <*x1,y1,z1*> . 3 = z1 & <*x2,y2,z2*> . 3 = z2 ) by FINSEQ_1:45;

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, A15, FINSEQ_1:45 ;

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, A15, FINSEQ_1:45 ;

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, A15, FINSEQ_1:45 ;

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; :: thesis: verum

for r being Real holds I . (r * v) = r * (I . v)

proof

I . (0. [:X,Y,Z:]) =
I . ((0. [:X,Y,Z:]) + (0. [:X,Y,Z:]))
let v be Point of [:X,Y,Z:]; :: thesis: for r being Real holds I . (r * v) = r * (I . v)

let r be Real; :: thesis: 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 ;

A28: ( <*x1,y1,z1*> . 1 = x1 & <*x1,y1,z1*> . 2 = y1 & <*x1,y1,z1*> . 3 = z1 ) by FINSEQ_1:45;

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, A28, FINSEQ_1:45;

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; :: thesis: verum

end;let r be Real; :: thesis: 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 ;

A28: ( <*x1,y1,z1*> . 1 = x1 & <*x1,y1,z1*> . 2 = y1 & <*x1,y1,z1*> . 3 = z1 ) by FINSEQ_1:45;

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, A28, FINSEQ_1:45;

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; :: thesis: verum

.= (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; :: thesis: verum