let E, F, G be RealLinearSpace; ( ( for x being set holds
( x is Point of (product <*E,F,G*>) iff ex x1 being Point of E ex x2 being Point of F ex x3 being Point of G st x = <*x1,x2,x3*> ) ) & ( for x1, y1 being Point of E
for x2, y2 being Point of F
for x3, y3 being Point of G holds <*x1,x2,x3*> + <*y1,y2,y3*> = <*(x1 + y1),(x2 + y2),(x3 + y3)*> ) & 0. (product <*E,F,G*>) = <*(0. E),(0. F),(0. G)*> & ( for x1 being Point of E
for x2 being Point of F
for x3 being Point of G holds - <*x1,x2,x3*> = <*(- x1),(- x2),(- x3)*> ) & ( for x1 being Point of E
for x2 being Point of F
for x3 being Point of G
for a being Real holds a * <*x1,x2,x3*> = <*(a * x1),(a * x2),(a * x3)*> ) )
A1:
the carrier of [:E,F,G:] = [: the carrier of E, the carrier of F, the carrier of G:]
;
consider I being Function of [:E,F,G:],(product <*E,F,G*>) such that
A2:
( I is one-to-one & I is onto & ( for x being Point of E
for y being Point of F
for z being Point of G holds I . (x,y,z) = <*x,y,z*> ) & ( for v, w being Point of [:E,F,G:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:E,F,G:]
for r being Real holds I . (r * v) = r * (I . v) ) & 0. (product <*E,F,G*>) = I . (0. [:E,F,G:]) )
by Th11;
thus
for x being set holds
( x is Point of (product <*E,F,G*>) iff ex x1 being Point of E ex x2 being Point of F ex x3 being Point of G st x = <*x1,x2,x3*> )
( ( for x1, y1 being Point of E
for x2, y2 being Point of F
for x3, y3 being Point of G holds <*x1,x2,x3*> + <*y1,y2,y3*> = <*(x1 + y1),(x2 + y2),(x3 + y3)*> ) & 0. (product <*E,F,G*>) = <*(0. E),(0. F),(0. G)*> & ( for x1 being Point of E
for x2 being Point of F
for x3 being Point of G holds - <*x1,x2,x3*> = <*(- x1),(- x2),(- x3)*> ) & ( for x1 being Point of E
for x2 being Point of F
for x3 being Point of G
for a being Real holds a * <*x1,x2,x3*> = <*(a * x1),(a * x2),(a * x3)*> ) )proof
let y be
set ;
( y is Point of (product <*E,F,G*>) iff ex x1 being Point of E ex x2 being Point of F ex x3 being Point of G st y = <*x1,x2,x3*> )
hereby ( ex x1 being Point of E ex x2 being Point of F ex x3 being Point of G st y = <*x1,x2,x3*> implies y is Point of (product <*E,F,G*>) )
assume
y is
Point of
(product <*E,F,G*>)
;
ex x1 being Point of E ex x2 being Point of F ex x3 being Point of G st y = <*x1,x2,x3*>then
y in the
carrier of
(product <*E,F,G*>)
;
then
y in rng I
by A2, FUNCT_2:def 3;
then consider x being
Element of the
carrier of
[:E,F,G:] such that A4:
y = I . x
by FUNCT_2:113;
consider x1 being
Point of
E,
x2 being
Point of
F,
x3 being
Point of
G such that A5:
x = [x1,x2,x3]
by A1, Lm1;
take x1 =
x1;
ex x2 being Point of F ex x3 being Point of G st y = <*x1,x2,x3*>take x2 =
x2;
ex x3 being Point of G st y = <*x1,x2,x3*>take x3 =
x3;
y = <*x1,x2,x3*>
I . (
x1,
x2,
x3)
= <*x1,x2,x3*>
by A2;
hence
y = <*x1,x2,x3*>
by A4, A5;
verum
end;
thus
( ex
x1 being
Point of
E ex
x2 being
Point of
F ex
x3 being
Point of
G st
y = <*x1,x2,x3*> implies
y is
Point of
(product <*E,F,G*>) )
;
verum
end;
thus A8:
for x1, y1 being Point of E
for x2, y2 being Point of F
for x3, y3 being Point of G holds <*x1,x2,x3*> + <*y1,y2,y3*> = <*(x1 + y1),(x2 + y2),(x3 + y3)*>
( 0. (product <*E,F,G*>) = <*(0. E),(0. F),(0. G)*> & ( for x1 being Point of E
for x2 being Point of F
for x3 being Point of G holds - <*x1,x2,x3*> = <*(- x1),(- x2),(- x3)*> ) & ( for x1 being Point of E
for x2 being Point of F
for x3 being Point of G
for a being Real holds a * <*x1,x2,x3*> = <*(a * x1),(a * x2),(a * x3)*> ) )proof
let x1,
y1 be
Point of
E;
for x2, y2 being Point of F
for x3, y3 being Point of G holds <*x1,x2,x3*> + <*y1,y2,y3*> = <*(x1 + y1),(x2 + y2),(x3 + y3)*>let x2,
y2 be
Point of
F;
for x3, y3 being Point of G holds <*x1,x2,x3*> + <*y1,y2,y3*> = <*(x1 + y1),(x2 + y2),(x3 + y3)*>let x3,
y3 be
Point of
G;
<*x1,x2,x3*> + <*y1,y2,y3*> = <*(x1 + y1),(x2 + y2),(x3 + y3)*>
A10:
[x1,x2,x3] + [y1,y2,y3] = [(x1 + y1),(x2 + y2),(x3 + y3)]
by Th8;
(
I . (
(x1 + y1),
(x2 + y2),
(x3 + y3))
= <*(x1 + y1),(x2 + y2),(x3 + y3)*> &
I . (
x1,
x2,
x3)
= <*x1,x2,x3*> &
I . (
y1,
y2,
y3)
= <*y1,y2,y3*> )
by A2;
hence
<*x1,x2,x3*> + <*y1,y2,y3*> = <*(x1 + y1),(x2 + y2),(x3 + y3)*>
by A2, A10;
verum
end;
thus A11:
0. (product <*E,F,G*>) = <*(0. E),(0. F),(0. G)*>
( ( for x1 being Point of E
for x2 being Point of F
for x3 being Point of G holds - <*x1,x2,x3*> = <*(- x1),(- x2),(- x3)*> ) & ( for x1 being Point of E
for x2 being Point of F
for x3 being Point of G
for a being Real holds a * <*x1,x2,x3*> = <*(a * x1),(a * x2),(a * x3)*> ) )
thus
for x1 being Point of E
for x2 being Point of F
for x3 being Point of G holds - <*x1,x2,x3*> = <*(- x1),(- x2),(- x3)*>
for x1 being Point of E
for x2 being Point of F
for x3 being Point of G
for a being Real holds a * <*x1,x2,x3*> = <*(a * x1),(a * x2),(a * x3)*>proof
let x1 be
Point of
E;
for x2 being Point of F
for x3 being Point of G holds - <*x1,x2,x3*> = <*(- x1),(- x2),(- x3)*>let x2 be
Point of
F;
for x3 being Point of G holds - <*x1,x2,x3*> = <*(- x1),(- x2),(- x3)*>let x3 be
Point of
G;
- <*x1,x2,x3*> = <*(- x1),(- x2),(- x3)*>
<*x1,x2,x3*> + <*(- x1),(- x2),(- x3)*> =
<*(x1 + (- x1)),(x2 + (- x2)),(x3 + (- x3))*>
by A8
.=
<*(0. E),(x2 + (- x2)),(x3 + (- x3))*>
by RLVECT_1:def 10
.=
<*(0. E),(0. F),(x3 + (- x3))*>
by RLVECT_1:def 10
.=
0. (product <*E,F,G*>)
by A11, RLVECT_1:def 10
;
hence
- <*x1,x2,x3*> = <*(- x1),(- x2),(- x3)*>
by RLVECT_1:def 10;
verum
end;
let x1 be Point of E; for x2 being Point of F
for x3 being Point of G
for a being Real holds a * <*x1,x2,x3*> = <*(a * x1),(a * x2),(a * x3)*>
let x2 be Point of F; for x3 being Point of G
for a being Real holds a * <*x1,x2,x3*> = <*(a * x1),(a * x2),(a * x3)*>
let x3 be Point of G; for a being Real holds a * <*x1,x2,x3*> = <*(a * x1),(a * x2),(a * x3)*>
let a be Real; a * <*x1,x2,x3*> = <*(a * x1),(a * x2),(a * x3)*>
A14:
<*x1,x2,x3*> = I . (x1,x2,x3)
by A2;
I . (a * [x1,x2,x3]) =
I . ((a * x1),(a * x2),(a * x3))
by Th8
.=
<*(a * x1),(a * x2),(a * x3)*>
by A2
;
hence
a * <*x1,x2,x3*> = <*(a * x1),(a * x2),(a * x3)*>
by A2, A14; verum