environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, CARD_3, FUNCT_1, RELAT_1, FUNCT_2, FINSEQ_1, PRE_TOPC, XBOOLE_0, NORMSP_0, STRUCT_0, RLVECT_1, NORMSP_1, COMPLEX1, ARYTM_3, REAL_1, PRVECT_3, RFINSEQ, ARYTM_1, SQUARE_1, RVSUM_1, XXREAL_0, CARD_1, SUPINF_2, SEQ_2, ORDINAL2, TARSKI, NAT_1, PRVECT_1, PRVECT_2, ZFMISC_1, ORDINAL4, GROUP_2, ALGSTR_0, BINOP_1, EUCLID, REWRITE1, RSSPACE3, RELAT_2, METRIC_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, SQUARE_1, NAT_1, COMPLEX1, CARD_3, FINSEQ_1, FINSEQ_2, FINSEQ_4, RVSUM_1, RFINSEQ, STRUCT_0, ALGSTR_0, PRE_TOPC, RLVECT_1, NORMSP_0, NORMSP_1, EUCLID, RSSPACE3, LOPBAN_1, PRVECT_1, PRVECT_2;
definitions PRVECT_2, RLVECT_1, ALGSTR_0;
theorems TARSKI, XBOOLE_0, XREAL_0, RLVECT_1, FINSEQ_1, FINSEQ_2, RVSUM_1, NORMSP_0, RFINSEQ, NAT_1, TOPREAL6, SQUARE_1, RELSET_1, RELAT_1, FUNCT_1, FUNCT_2, NORMSP_1, LOPBAN_1, CARD_3, ALGSTR_0, EUCLID, RSSPACE3, XXREAL_0, PRVECT_1, PRVECT_2, ZFMISC_1, FINSEQ_3, SUBSET_1, XTUPLE_0, ORDINAL1;
schemes FUNCT_2, BINOP_1;
registrations RELSET_1, STRUCT_0, ORDINAL1, XREAL_0, FUNCT_1, FUNCT_2, NUMBERS, XBOOLE_0, VALUED_0, EUCLID, PRVECT_2, ALGSTR_0, FINSEQ_1, CARD_3, NORMSP_0, LOPBAN_1, RLVECT_1, NORMSP_1, RELAT_1, SUBSET_1, SQUARE_1, RVSUM_1;
constructors HIDDEN, REAL_1, SQUARE_1, RSSPACE3, COMPLEX1, LOPBAN_1, RVSUM_1, BINOP_2, PRVECT_2, FINSEQ_4, RFINSEQ, FINSEQOP, TOPMETR;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS, ARITHM;
equalities EUCLID, PRVECT_2, BINOP_1, RLVECT_1, ALGSTR_0, NORMSP_0, STRUCT_0;
expansions PRVECT_2, BINOP_1, NORMSP_0;
theorem
for
D,
E,
F,
G being non
empty set ex
I being
Function of
[:[:D,E:],[:F,G:]:],
[:[:D,F:],[:E,G:]:] st
(
I is
one-to-one &
I is
onto & ( for
d,
e,
f,
g being
set st
d in D &
e in E &
f in F &
g in G holds
I . (
[d,e],
[f,g])
= [[d,f],[e,g]] ) )
Lm1:
for G, F being non empty 1-sorted
for x being set st x in [: the carrier of G, the carrier of F:] holds
ex x1 being Point of G ex x2 being Point of F st x = [x1,x2]
by SUBSET_1:43;
definition
let G,
F be non
empty addLoopStr ;
existence
ex b1 being BinOp of [: the carrier of G, the carrier of F:] st
for g1, g2 being Point of G
for f1, f2 being Point of F holds b1 . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)]
uniqueness
for b1, b2 being BinOp of [: the carrier of G, the carrier of F:] st ( for g1, g2 being Point of G
for f1, f2 being Point of F holds b1 . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] ) & ( for g1, g2 being Point of G
for f1, f2 being Point of F holds b2 . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] ) holds
b1 = b2
end;
definition
let G,
F be non
empty RLSStruct ;
existence
ex b1 being Function of [:REAL,[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:] st
for r being Real
for g being Point of G
for f being Point of F holds b1 . (r,[g,f]) = [(r * g),(r * f)]
uniqueness
for b1, b2 being Function of [:REAL,[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:] st ( for r being Real
for g being Point of G
for f being Point of F holds b1 . (r,[g,f]) = [(r * g),(r * f)] ) & ( for r being Real
for g being Point of G
for f being Point of F holds b2 . (r,[g,f]) = [(r * g),(r * f)] ) holds
b1 = b2
end;
theorem
for
G,
F being non
empty addLoopStr holds
( ( for
x being
set holds
(
x is
Point of
[:G,F:] iff ex
x1 being
Point of
G ex
x2 being
Point of
F st
x = [x1,x2] ) ) & ( for
x,
y being
Point of
[:G,F:] for
x1,
y1 being
Point of
G for
x2,
y2 being
Point of
F st
x = [x1,x2] &
y = [y1,y2] holds
x + y = [(x1 + y1),(x2 + y2)] ) &
0. [:G,F:] = [(0. G),(0. F)] )
by Lm1, Def1;
theorem Th9:
for
G,
F being non
empty RLSStruct holds
( ( for
x being
set holds
(
x is
Point of
[:G,F:] iff ex
x1 being
Point of
G ex
x2 being
Point of
F st
x = [x1,x2] ) ) & ( for
x,
y being
Point of
[:G,F:] for
x1,
y1 being
Point of
G for
x2,
y2 being
Point of
F st
x = [x1,x2] &
y = [y1,y2] holds
x + y = [(x1 + y1),(x2 + y2)] ) &
0. [:G,F:] = [(0. G),(0. F)] & ( for
x being
Point of
[:G,F:] for
x1 being
Point of
G for
x2 being
Point of
F for
a being
Real st
x = [x1,x2] holds
a * x = [(a * x1),(a * x2)] ) )
by Def2, Def1, Lm1;
theorem Th12:
for
X,
Y being
RealLinearSpace ex
I being
Function of
[:X,Y:],
(product <*X,Y*>) st
(
I is
one-to-one &
I is
onto & ( for
x being
Point of
X for
y being
Point of
Y holds
I . (
x,
y)
= <*x,y*> ) & ( for
v,
w being
Point of
[:X,Y:] holds
I . (v + w) = (I . v) + (I . w) ) & ( for
v being
Point of
[:X,Y:] for
r being
Real holds
I . (r * v) = r * (I . v) ) &
I . (0. [:X,Y:]) = 0. (product <*X,Y*>) )
Lm2:
for X being non-empty non empty FinSequence
for x being set st x in product X holds
x is FinSequence
theorem
for
G,
F being
RealLinearSpace holds
( ( for
x being
set holds
(
x is
Point of
(product <*G,F*>) iff ex
x1 being
Point of
G ex
x2 being
Point of
F st
x = <*x1,x2*> ) ) & ( for
x,
y being
Point of
(product <*G,F*>) for
x1,
y1 being
Point of
G for
x2,
y2 being
Point 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
Point of
(product <*G,F*>) for
x1 being
Point of
G for
x2 being
Point of
F st
x = <*x1,x2*> holds
- x = <*(- x1),(- x2)*> ) & ( for
x being
Point of
(product <*G,F*>) for
x1 being
Point of
G for
x2 being
Point of
F for
a being
Real st
x = <*x1,x2*> holds
a * x = <*(a * x1),(a * x2)*> ) )
definition
let G,
F be non
empty NORMSTR ;
existence
ex b1 being Function of [: the carrier of G, the carrier of F:],REAL st
for g being Point of G
for f being Point of F ex v being Element of REAL 2 st
( v = <*||.g.||,||.f.||*> & b1 . (g,f) = |.v.| )
uniqueness
for b1, b2 being Function of [: the carrier of G, the carrier of F:],REAL st ( for g being Point of G
for f being Point of F ex v being Element of REAL 2 st
( v = <*||.g.||,||.f.||*> & b1 . (g,f) = |.v.| ) ) & ( for g being Point of G
for f being Point of F ex v being Element of REAL 2 st
( v = <*||.g.||,||.f.||*> & b2 . (g,f) = |.v.| ) ) holds
b1 = b2
end;
definition
let G,
F be non
empty NORMSTR ;
func [:G,F:] -> non
empty strict NORMSTR equals
NORMSTR(#
[: the carrier of G, the carrier of F:],
(prod_ZERO (G,F)),
(prod_ADD (G,F)),
(prod_MLT (G,F)),
(prod_NORM (G,F)) #);
correctness
coherence
NORMSTR(# [: the carrier of G, the carrier of F:],(prod_ZERO (G,F)),(prod_ADD (G,F)),(prod_MLT (G,F)),(prod_NORM (G,F)) #) is non empty strict NORMSTR ;
;
end;
::
deftheorem defines
[: PRVECT_3:def 7 :
for G, F being non empty NORMSTR holds [:G,F:] = NORMSTR(# [: the carrier of G, the carrier of F:],(prod_ZERO (G,F)),(prod_ADD (G,F)),(prod_MLT (G,F)),(prod_NORM (G,F)) #);
registration
let G,
F be non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR ;
correctness
coherence
( [:G,F:] is strict & [:G,F:] is reflexive & [:G,F:] is discerning & [:G,F:] is RealNormSpace-like & [:G,F:] is scalar-distributive & [:G,F:] is vector-distributive & [:G,F:] is scalar-associative & [:G,F:] is scalar-unital & [:G,F:] is Abelian & [:G,F:] is add-associative & [:G,F:] is right_zeroed & [:G,F:] is right_complementable );
end;
theorem Th15:
for
X,
Y being
RealNormSpace ex
I being
Function of
[:X,Y:],
(product <*X,Y*>) st
(
I is
one-to-one &
I is
onto & ( for
x being
Point of
X for
y being
Point of
Y holds
I . (
x,
y)
= <*x,y*> ) & ( for
v,
w being
Point of
[:X,Y:] holds
I . (v + w) = (I . v) + (I . w) ) & ( for
v being
Point of
[:X,Y:] for
r being
Real holds
I . (r * v) = r * (I . v) ) &
0. (product <*X,Y*>) = I . (0. [:X,Y:]) & ( for
v being
Point of
[:X,Y:] holds
||.(I . v).|| = ||.v.|| ) )
Lm3:
for F1, F2 being FinSequence of REAL holds sqr (F1 ^ F2) = (sqr F1) ^ (sqr F2)
by RVSUM_1:144;
theorem Th17:
for
X,
Y being
RealNormSpace-Sequence ex
I being
Function of
[:(product X),(product Y):],
(product (X ^ Y)) st
(
I is
one-to-one &
I is
onto & ( for
x being
Point of
(product X) for
y being
Point of
(product Y) ex
x1,
y1 being
FinSequence st
(
x = x1 &
y = y1 &
I . (
x,
y)
= x1 ^ y1 ) ) & ( for
v,
w being
Point of
[:(product X),(product Y):] holds
I . (v + w) = (I . v) + (I . w) ) & ( for
v being
Point of
[:(product X),(product Y):] for
r being
Element of
REAL holds
I . (r * v) = r * (I . v) ) &
I . (0. [:(product X),(product Y):]) = 0. (product (X ^ Y)) & ( for
v being
Point of
[:(product X),(product Y):] holds
||.(I . v).|| = ||.v.|| ) )
theorem Th18:
for
G,
F being
RealNormSpace holds
( ( for
x being
set holds
(
x is
Point of
[:G,F:] iff ex
x1 being
Point of
G ex
x2 being
Point of
F st
x = [x1,x2] ) ) & ( for
x,
y being
Point of
[:G,F:] for
x1,
y1 being
Point of
G for
x2,
y2 being
Point of
F st
x = [x1,x2] &
y = [y1,y2] holds
x + y = [(x1 + y1),(x2 + y2)] ) &
0. [:G,F:] = [(0. G),(0. F)] & ( for
x being
Point of
[:G,F:] for
x1 being
Point of
G for
x2 being
Point of
F st
x = [x1,x2] holds
- x = [(- x1),(- x2)] ) & ( for
x being
Point of
[:G,F:] for
x1 being
Point of
G for
x2 being
Point of
F for
a being
Real st
x = [x1,x2] holds
a * x = [(a * x1),(a * x2)] ) & ( for
x being
Point of
[:G,F:] for
x1 being
Point of
G for
x2 being
Point of
F st
x = [x1,x2] holds
ex
w being
Element of
REAL 2 st
(
w = <*||.x1.||,||.x2.||*> &
||.x.|| = |.w.| ) ) )
theorem Th19:
for
G,
F being
RealNormSpace holds
( ( for
x being
set holds
(
x is
Point of
(product <*G,F*>) iff ex
x1 being
Point of
G ex
x2 being
Point of
F st
x = <*x1,x2*> ) ) & ( for
x,
y being
Point of
(product <*G,F*>) for
x1,
y1 being
Point of
G for
x2,
y2 being
Point 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
Point of
(product <*G,F*>) for
x1 being
Point of
G for
x2 being
Point of
F st
x = <*x1,x2*> holds
- x = <*(- x1),(- x2)*> ) & ( for
x being
Point of
(product <*G,F*>) for
x1 being
Point of
G for
x2 being
Point of
F for
a being
Real st
x = <*x1,x2*> holds
a * x = <*(a * x1),(a * x2)*> ) & ( for
x being
Point of
(product <*G,F*>) for
x1 being
Point of
G for
x2 being
Point of
F st
x = <*x1,x2*> holds
ex
w being
Element of
REAL 2 st
(
w = <*||.x1.||,||.x2.||*> &
||.x.|| = |.w.| ) ) )
theorem
for
X,
Y being
RealNormSpace-Sequence ex
I being
Function of
(product <*(product X),(product Y)*>),
(product (X ^ Y)) st
(
I is
one-to-one &
I is
onto & ( for
x being
Point of
(product X) for
y being
Point of
(product Y) ex
x1,
y1 being
FinSequence st
(
x = x1 &
y = y1 &
I . <*x,y*> = x1 ^ y1 ) ) & ( for
v,
w being
Point of
(product <*(product X),(product Y)*>) holds
I . (v + w) = (I . v) + (I . w) ) & ( for
v being
Point of
(product <*(product X),(product Y)*>) for
r being
Element of
REAL holds
I . (r * v) = r * (I . v) ) &
I . (0. (product <*(product X),(product Y)*>)) = 0. (product (X ^ Y)) & ( for
v being
Point of
(product <*(product X),(product Y)*>) holds
||.(I . v).|| = ||.v.|| ) )
theorem Th21:
for
X,
Y being
RealLinearSpace ex
I being
Function of
[:X,Y:],
[:X,(product <*Y*>):] st
(
I is
one-to-one &
I is
onto & ( for
x being
Point of
X for
y being
Point of
Y holds
I . (
x,
y)
= [x,<*y*>] ) & ( for
v,
w being
Point of
[:X,Y:] holds
I . (v + w) = (I . v) + (I . w) ) & ( for
v being
Point of
[:X,Y:] for
r being
Element of
REAL holds
I . (r * v) = r * (I . v) ) &
I . (0. [:X,Y:]) = 0. [:X,(product <*Y*>):] )
theorem Th23:
for
X,
Y being
RealNormSpace ex
I being
Function of
[:X,Y:],
[:X,(product <*Y*>):] st
(
I is
one-to-one &
I is
onto & ( for
x being
Point of
X for
y being
Point of
Y holds
I . (
x,
y)
= [x,<*y*>] ) & ( for
v,
w being
Point of
[:X,Y:] holds
I . (v + w) = (I . v) + (I . w) ) & ( for
v being
Point of
[:X,Y:] for
r being
Element of
REAL holds
I . (r * v) = r * (I . v) ) &
I . (0. [:X,Y:]) = 0. [:X,(product <*Y*>):] & ( for
v being
Point of
[:X,Y:] holds
||.(I . v).|| = ||.v.|| ) )