let K be Ring; for X, Y being VectSp of K ex I being Function of [:X,Y:],(product <*X,Y*>) st
( I is one-to-one & I is onto & ( for x being Vector of X
for y being Vector of Y holds I . (x,y) = <*x,y*> ) & ( for v, w being Vector of [:X,Y:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Vector of [:X,Y:]
for r being Element of K holds I . (r * v) = r * (I . v) ) & I . (0. [:X,Y:]) = 0. (product <*X,Y*>) )
let X, Y be VectSp of K; ex I being Function of [:X,Y:],(product <*X,Y*>) st
( I is one-to-one & I is onto & ( for x being Vector of X
for y being Vector of Y holds I . (x,y) = <*x,y*> ) & ( for v, w being Vector of [:X,Y:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Vector of [:X,Y:]
for r being Element of K 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
A1:
( I is one-to-one & I is onto & ( for x, y being object st x in the carrier of X & y in the carrier of Y holds
I . (x,y) = <*x,y*> ) )
by PRVECT_3:5;
len (carr <*X,Y*>) = len <*X,Y*>
by PRVECT_1:def 11;
then A2:
len (carr <*X,Y*>) = 2
by FINSEQ_1:44;
then A3:
dom (carr <*X,Y*>) = {1,2}
by FINSEQ_1:2, FINSEQ_1:def 3;
len <*X,Y*> = 2
by FINSEQ_1:44;
then A4:
dom <*X,Y*> = {1,2}
by FINSEQ_1:2, FINSEQ_1:def 3;
A5:
( <*X,Y*> . 1 = X & <*X,Y*> . 2 = Y )
by FINSEQ_1:44;
( 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 A4, A5, PRVECT_1:def 11;
then A6:
carr <*X,Y*> = <* the carrier of X, the carrier of Y*>
by A2, FINSEQ_1:44;
then reconsider I = I as Function of [:X,Y:],(product <*X,Y*>) ;
A7:
for x being Vector of X
for y being Vector of Y holds I . (x,y) = <*x,y*>
by A1;
A8:
for v, w being Vector of [:X,Y:] holds I . (v + w) = (I . v) + (I . w)
proof
let v,
w be
Vector of
[:X,Y:];
I . (v + w) = (I . v) + (I . w)
consider x1 being
Vector of
X,
y1 being
Vector of
Y such that A9:
v = [x1,y1]
by SUBSET_1:43;
consider x2 being
Vector of
X,
y2 being
Vector of
Y such that A10:
w = [x2,y2]
by SUBSET_1:43;
(
I . v = I . (
x1,
y1) &
I . w = I . (
x2,
y2) )
by A9, A10;
then A11:
(
I . v = <*x1,y1*> &
I . w = <*x2,y2*> )
by A1;
A12:
I . (v + w) =
I . (
(x1 + x2),
(y1 + y2))
by A9, A10, PRVECT_3:def 1
.=
<*(x1 + x2),(y1 + y2)*>
by A1
;
A13:
(
<*x1,y1*> . 1
= x1 &
<*x2,y2*> . 1
= x2 &
<*x1,y1*> . 2
= y1 &
<*x2,y2*> . 2
= y2 )
by FINSEQ_1:44;
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 A3, TARSKI:def 2;
A14:
(addop <*X,Y*>) . j1 = the
addF of
(<*X,Y*> . j1)
by PRVECT_1:def 12;
A15:
([:(addop <*X,Y*>):] . (Iv,Iw)) . j1 =
((addop <*X,Y*>) . j1) . (
(Iv . j1),
(Iw . j1))
by PRVECT_1:def 8
.=
x1 + x2
by A14, A11, A13, FINSEQ_1:44
;
A16:
(addop <*X,Y*>) . j2 = the
addF of
(<*X,Y*> . j2)
by PRVECT_1:def 12;
A17:
([:(addop <*X,Y*>):] . (Iv,Iw)) . j2 =
((addop <*X,Y*>) . j2) . (
(Iv . j2),
(Iw . j2))
by PRVECT_1:def 8
.=
y1 + y2
by A16, A11, A13, FINSEQ_1:44
;
consider Ivw being
Function such that A18:
(
(I . v) + (I . w) = Ivw &
dom Ivw = dom (carr <*X,Y*>) & ( for
i being
object st
i in dom (carr <*X,Y*>) holds
Ivw . i in (carr <*X,Y*>) . i ) )
by CARD_3:def 5;
A19:
dom Ivw = Seg 2
by A2, A18, FINSEQ_1:def 3;
then reconsider Ivw =
Ivw as
FinSequence by FINSEQ_1:def 2;
len Ivw = 2
by A19, FINSEQ_1:def 3;
hence
I . (v + w) = (I . v) + (I . w)
by A12, A18, A15, A17, FINSEQ_1:44;
verum
end;
A20:
for v being Vector of [:X,Y:]
for r being Element of K holds I . (r * v) = r * (I . v)
proof
let v be
Vector of
[:X,Y:];
for r being Element of K holds I . (r * v) = r * (I . v)let r be
Element of
K;
I . (r * v) = r * (I . v)
consider x1 being
Vector of
X,
y1 being
Vector of
Y such that A21:
v = [x1,y1]
by SUBSET_1:43;
A22:
I . v =
I . (
x1,
y1)
by A21
.=
<*x1,y1*>
by A1
;
A23:
I . (r * v) =
I . (
(r * x1),
(r * y1))
by A21, YDef2
.=
<*(r * x1),(r * y1)*>
by A1
;
A24:
(
<*x1,y1*> . 1
= x1 &
<*x1,y1*> . 2
= y1 )
by FINSEQ_1:44;
reconsider j1 = 1,
j2 = 2 as
Element of
dom (carr <*X,Y*>) by A3, TARSKI:def 2;
A25:
(
(multop <*X,Y*>) . j1 = the
lmult of
(<*X,Y*> . j1) &
(multop <*X,Y*>) . j2 = the
lmult of
(<*X,Y*> . j2) )
by Def8;
reconsider Iv =
I . v as
Element of
product (carr <*X,Y*>) ;
reconsider rr =
r as
Element of the
carrier of
K ;
(
([:(multop <*X,Y*>):] . (rr,Iv)) . j1 = ((multop <*X,Y*>) . j1) . (
r,
(Iv . j1)) &
([:(multop <*X,Y*>):] . (rr,Iv)) . j2 = ((multop <*X,Y*>) . j2) . (
r,
(Iv . j2)) )
by PRVECT_2:def 2;
then A26:
(
([:(multop <*X,Y*>):] . (rr,Iv)) . j1 = r * x1 &
([:(multop <*X,Y*>):] . (rr,Iv)) . j2 = r * y1 )
by A25, A22, A24, FINSEQ_1:44;
consider Ivw being
Function such that A27:
(
r * (I . v) = Ivw &
dom Ivw = dom (carr <*X,Y*>) & ( for
i being
object st
i in dom (carr <*X,Y*>) holds
Ivw . i in (carr <*X,Y*>) . i ) )
by CARD_3:def 5;
A28:
dom Ivw = Seg 2
by A2, A27, FINSEQ_1:def 3;
then reconsider Ivw =
Ivw as
FinSequence by FINSEQ_1:def 2;
len Ivw = 2
by A28, FINSEQ_1:def 3;
hence
I . (r * v) = r * (I . v)
by A23, A27, A26, FINSEQ_1:44;
verum
end;
I . (0. [:X,Y:]) =
I . ((0. [:X,Y:]) + (0. [:X,Y:]))
.=
(I . (0. [:X,Y:])) + (I . (0. [:X,Y:]))
by A8
;
then (I . (0. [:X,Y:])) - (I . (0. [:X,Y:])) =
(I . (0. [:X,Y:])) + ((I . (0. [:X,Y:])) - (I . (0. [:X,Y:])))
by RLVECT_1:28
.=
(I . (0. [:X,Y:])) + (0. (product <*X,Y*>))
by RLVECT_1:15
.=
I . (0. [:X,Y:])
;
hence
ex I being Function of [:X,Y:],(product <*X,Y*>) st
( I is one-to-one & I is onto & ( for x being Vector of X
for y being Vector of Y holds I . (x,y) = <*x,y*> ) & ( for v, w being Vector of [:X,Y:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Vector of [:X,Y:]
for r being Element of K holds I . (r * v) = r * (I . v) ) & I . (0. [:X,Y:]) = 0. (product <*X,Y*>) )
by A7, A8, A20, A1, A6, RLVECT_1:15; verum