let K be Ring; for G, F being VectSp of K holds
( ( for x being set holds
( x is Vector of (product <*G,F*>) iff ex x1 being Vector of G ex x2 being Vector of F st x = <*x1,x2*> ) ) & ( for x, y being Vector of (product <*G,F*>)
for x1, y1 being Vector of G
for x2, y2 being Vector of F st x = <*x1,x2*> & y = <*y1,y2*> holds
x + y = <*(x1 + y1),(x2 + y2)*> ) & 0. (product <*G,F*>) = <*(0. G),(0. F)*> & ( for x being Vector of (product <*G,F*>)
for x1 being Vector of G
for x2 being Vector of F st x = <*x1,x2*> holds
- x = <*(- x1),(- x2)*> ) & ( for x being Vector of (product <*G,F*>)
for x1 being Vector of G
for x2 being Vector of F
for a being Element of K st x = <*x1,x2*> holds
a * x = <*(a * x1),(a * x2)*> ) )
let G, F be VectSp of K; ( ( for x being set holds
( x is Vector of (product <*G,F*>) iff ex x1 being Vector of G ex x2 being Vector of F st x = <*x1,x2*> ) ) & ( for x, y being Vector of (product <*G,F*>)
for x1, y1 being Vector of G
for x2, y2 being Vector of F st x = <*x1,x2*> & y = <*y1,y2*> holds
x + y = <*(x1 + y1),(x2 + y2)*> ) & 0. (product <*G,F*>) = <*(0. G),(0. F)*> & ( for x being Vector of (product <*G,F*>)
for x1 being Vector of G
for x2 being Vector of F st x = <*x1,x2*> holds
- x = <*(- x1),(- x2)*> ) & ( for x being Vector of (product <*G,F*>)
for x1 being Vector of G
for x2 being Vector of F
for a being Element of K st x = <*x1,x2*> holds
a * x = <*(a * x1),(a * x2)*> ) )
consider I being Function of [:G,F:],(product <*G,F*>) such that
A1:
( I is one-to-one & I is onto & ( for x being Vector of G
for y being Vector of F holds I . (x,y) = <*x,y*> ) & ( for v, w being Vector of [:G,F:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Vector of [:G,F:]
for r being Element of K holds I . (r * v) = r * (I . v) ) & 0. (product <*G,F*>) = I . (0. [:G,F:]) )
by Th12;
thus A2:
for x being set holds
( x is Vector of (product <*G,F*>) iff ex x1 being Vector of G ex x2 being Vector of F st x = <*x1,x2*> )
( ( for x, y being Vector of (product <*G,F*>)
for x1, y1 being Vector of G
for x2, y2 being Vector of F st x = <*x1,x2*> & y = <*y1,y2*> holds
x + y = <*(x1 + y1),(x2 + y2)*> ) & 0. (product <*G,F*>) = <*(0. G),(0. F)*> & ( for x being Vector of (product <*G,F*>)
for x1 being Vector of G
for x2 being Vector of F st x = <*x1,x2*> holds
- x = <*(- x1),(- x2)*> ) & ( for x being Vector of (product <*G,F*>)
for x1 being Vector of G
for x2 being Vector of F
for a being Element of K st x = <*x1,x2*> holds
a * x = <*(a * x1),(a * x2)*> ) )proof
let y be
set ;
( y is Vector of (product <*G,F*>) iff ex x1 being Vector of G ex x2 being Vector of F st y = <*x1,x2*> )
hereby ( ex x1 being Vector of G ex x2 being Vector of F st y = <*x1,x2*> implies y is Vector of (product <*G,F*>) )
assume
y is
Vector of
(product <*G,F*>)
;
ex x1 being Vector of G ex x2 being Vector of F st y = <*x1,x2*>then consider x being
Element of the
carrier of
[:G,F:] such that A3:
y = I . x
by A1, FUNCT_2:113;
consider x1 being
Vector of
G,
x2 being
Vector of
F such that A4:
x = [x1,x2]
by SUBSET_1:43;
take x1 =
x1;
ex x2 being Vector of F st y = <*x1,x2*>take x2 =
x2;
y = <*x1,x2*>
I . (
x1,
x2)
= <*x1,x2*>
by A1;
hence
y = <*x1,x2*>
by A3, A4;
verum
end;
hence
( ex
x1 being
Vector of
G ex
x2 being
Vector of
F st
y = <*x1,x2*> implies
y is
Vector of
(product <*G,F*>) )
;
verum
end;
thus A7:
for x, y being Vector of (product <*G,F*>)
for x1, y1 being Vector of G
for x2, y2 being Vector of F st x = <*x1,x2*> & y = <*y1,y2*> holds
x + y = <*(x1 + y1),(x2 + y2)*>
( 0. (product <*G,F*>) = <*(0. G),(0. F)*> & ( for x being Vector of (product <*G,F*>)
for x1 being Vector of G
for x2 being Vector of F st x = <*x1,x2*> holds
- x = <*(- x1),(- x2)*> ) & ( for x being Vector of (product <*G,F*>)
for x1 being Vector of G
for x2 being Vector of F
for a being Element of K st x = <*x1,x2*> holds
a * x = <*(a * x1),(a * x2)*> ) )proof
let x,
y be
Vector of
(product <*G,F*>);
for x1, y1 being Vector of G
for x2, y2 being Vector of F st x = <*x1,x2*> & y = <*y1,y2*> holds
x + y = <*(x1 + y1),(x2 + y2)*>let x1,
y1 be
Vector of
G;
for x2, y2 being Vector of F st x = <*x1,x2*> & y = <*y1,y2*> holds
x + y = <*(x1 + y1),(x2 + y2)*>let x2,
y2 be
Vector of
F;
( x = <*x1,x2*> & y = <*y1,y2*> implies x + y = <*(x1 + y1),(x2 + y2)*> )
assume A8:
(
x = <*x1,x2*> &
y = <*y1,y2*> )
;
x + y = <*(x1 + y1),(x2 + y2)*>
reconsider z =
[x1,x2],
w =
[y1,y2] as
Vector of
[:G,F:] ;
A9:
z + w = [(x1 + y1),(x2 + y2)]
by PRVECT_3:def 1;
(
I . (
(x1 + y1),
(x2 + y2))
= <*(x1 + y1),(x2 + y2)*> &
I . (
x1,
x2)
= <*x1,x2*> &
I . (
y1,
y2)
= <*y1,y2*> )
by A1;
hence
<*(x1 + y1),(x2 + y2)*> = x + y
by A1, A9, A8;
verum
end;
thus A10:
0. (product <*G,F*>) = <*(0. G),(0. F)*>
( ( for x being Vector of (product <*G,F*>)
for x1 being Vector of G
for x2 being Vector of F st x = <*x1,x2*> holds
- x = <*(- x1),(- x2)*> ) & ( for x being Vector of (product <*G,F*>)
for x1 being Vector of G
for x2 being Vector of F
for a being Element of K st x = <*x1,x2*> holds
a * x = <*(a * x1),(a * x2)*> ) )
thus
for x being Vector of (product <*G,F*>)
for x1 being Vector of G
for x2 being Vector of F st x = <*x1,x2*> holds
- x = <*(- x1),(- x2)*>
for x being Vector of (product <*G,F*>)
for x1 being Vector of G
for x2 being Vector of F
for a being Element of K st x = <*x1,x2*> holds
a * x = <*(a * x1),(a * x2)*>proof
let x be
Vector of
(product <*G,F*>);
for x1 being Vector of G
for x2 being Vector of F st x = <*x1,x2*> holds
- x = <*(- x1),(- x2)*>let x1 be
Vector of
G;
for x2 being Vector of F st x = <*x1,x2*> holds
- x = <*(- x1),(- x2)*>let x2 be
Vector of
F;
( x = <*x1,x2*> implies - x = <*(- x1),(- x2)*> )
assume A11:
x = <*x1,x2*>
;
- x = <*(- x1),(- x2)*>
reconsider y =
<*(- x1),(- x2)*> as
Vector of
(product <*G,F*>) by A2;
x + y =
<*(x1 + (- x1)),(x2 + (- x2))*>
by A7, A11
.=
<*(0. G),(x2 + (- x2))*>
by RLVECT_1:def 10
.=
0. (product <*G,F*>)
by A10, RLVECT_1:def 10
;
hence
- x = <*(- x1),(- x2)*>
by RLVECT_1:def 10;
verum
end;
thus
for x being Vector of (product <*G,F*>)
for x1 being Vector of G
for x2 being Vector of F
for a being Element of K st x = <*x1,x2*> holds
a * x = <*(a * x1),(a * x2)*>
verumproof
let x be
Vector of
(product <*G,F*>);
for x1 being Vector of G
for x2 being Vector of F
for a being Element of K st x = <*x1,x2*> holds
a * x = <*(a * x1),(a * x2)*>let x1 be
Vector of
G;
for x2 being Vector of F
for a being Element of K st x = <*x1,x2*> holds
a * x = <*(a * x1),(a * x2)*>let x2 be
Vector of
F;
for a being Element of K st x = <*x1,x2*> holds
a * x = <*(a * x1),(a * x2)*>let a be
Element of
K;
( x = <*x1,x2*> implies a * x = <*(a * x1),(a * x2)*> )
assume A12:
x = <*x1,x2*>
;
a * x = <*(a * x1),(a * x2)*>
reconsider y =
[x1,x2] as
Vector of
[:G,F:] ;
A13:
<*x1,x2*> = I . (
x1,
x2)
by A1;
I . (a * y) =
I . (
(a * x1),
(a * x2))
by YDef2
.=
<*(a * x1),(a * x2)*>
by A1
;
hence
a * x = <*(a * x1),(a * x2)*>
by A1, A12, A13;
verum
end;