:: The 3-fold Product Space of Real Normed Spaces and its Properties
:: by Hiroyuki Okazaki and Kazuhisa Nakasho
::
:: Received November 30, 2021
:: Copyright (c) 2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies 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, ARYTM_1, SQUARE_1, RVSUM_1, XXREAL_0, CARD_1,
SUPINF_2, TARSKI, PRVECT_1, PRVECT_2, ZFMISC_1, GROUP_2, ALGSTR_0,
REWRITE1, RELAT_2, METRIC_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XTUPLE_0, RELAT_1, FUNCT_1,
RELSET_1, FUNCT_2, BINOP_1, DOMAIN_1, NUMBERS, MULTOP_1, XCMPLX_0,
XXREAL_0, XREAL_0, SQUARE_1, CARD_3, FINSEQ_1, FINSEQ_2, RVSUM_1,
STRUCT_0, ALGSTR_0, PRE_TOPC, RLVECT_1, NORMSP_0, NORMSP_1, EUCLID,
LOPBAN_1, PRVECT_1, PRVECT_2, PRVECT_3;
constructors SQUARE_1, LOPBAN_1, RVSUM_1, PRVECT_2, TOPMETR, PRVECT_3,
MULTOP_1;
registrations RELSET_1, STRUCT_0, ORDINAL1, XREAL_0, FUNCT_1, NUMBERS,
XBOOLE_0, VALUED_0, PRVECT_2, FINSEQ_1, CARD_3, LOPBAN_1, RLVECT_1,
NORMSP_1, SUBSET_1, SQUARE_1, RVSUM_1, PRVECT_1, PRVECT_3;
requirements SUBSET, BOOLE, NUMERALS;
begin :: 3-Variable Function & 3-fold Cartesian product
reserve v,x,x1,x2,y,z for object,
X,X1,X2,X3 for set;
scheme :: PRVECT_4:sch 1
FuncEx3A{X, Y, W, Z() -> set, P[object,object,object,object]}:
ex f being Function of [:X(),Y(),W():],Z()
st for x,y,w be object
st x in X() & y in Y() & w in W() holds P[x,y,w,f.(x,y,w)]
provided
for x,y,w be object st x in X() & y in Y() & w in W()
ex z st z in Z() & P[x,y,w,z];
theorem :: PRVECT_4:1
for X,Y,Z be non empty set, D be Function
st dom D = {1,2,3} & D.1 = X & D.2 = Y & D.3 = Z
ex I be Function of [:X,Y,Z:],product D
st I is one-to-one & I is onto
& for x,y,z be object st x in X & y in Y & z in Z
holds I.(x,y,z) = <*x,y,z*>;
theorem :: PRVECT_4:2
for X,Y,Z be non empty set
ex I be Function of [:X,Y,Z:],product <*X,Y,Z*>
st I is one-to-one & I is onto
& for x,y,z be object st x in X & y in Y & z in Z
holds I.(x,y,z) = <*x,y,z*>;
begin :: 3-fold Product Space of Real Linear Spaces
definition let E,F,G be non empty addLoopStr;
func [:E,F,G:] -> strict non empty addLoopStr equals
:: PRVECT_4:def 1
[:[:E,F:],G:];
end;
definition
let E,F,G be non empty addLoopStr;
let e be Point of E, f be Point of F, g be Point of G;
redefine func [e,f,g] -> Element of [:E,F,G:];
end;
registration
let E,F,G be Abelian non empty addLoopStr;
cluster [:E,F,G:] -> Abelian;
end;
registration
let E,F,G be add-associative non empty addLoopStr;
cluster [:E,F,G:] -> add-associative;
end;
registration
let E,F,G be right_zeroed non empty addLoopStr;
cluster [:E,F,G:] -> right_zeroed;
end;
registration
let E,F,G be right_complementable non empty addLoopStr;
cluster [:E,F,G:] -> right_complementable;
end;
theorem :: PRVECT_4:3
for E,F,G be non empty addLoopStr holds
( for x be set holds
(x is Point of [:E,F,G:] iff
ex x1 be Point of E, x2 be Point of F, x3 be Point of G st x=[x1,x2,x3]) )
& ( for x1,y1 be Point of E, x2,y2 be Point of F, x3,y3 be Point of G
holds [x1,x2,x3]+[y1,y2,y3] = [x1+y1,x2+y2,x3+y3] )
& 0.[:E,F,G:] = [0.E,0.F,0.G];
theorem :: PRVECT_4:4
for E,F,G be add-associative right_zeroed
right_complementable non empty addLoopStr,
x1 be Point of E, x2 be Point of F, x3 be Point of G
holds -[x1,x2,x3] = [-x1,-x2,-x3];
definition let E,F,G be non empty RLSStruct;
func [:E,F,G:] -> strict non empty RLSStruct equals
:: PRVECT_4:def 2
[:[:E,F:],G:];
end;
definition
let E,F,G be non empty RLSStruct;
let e be Point of E, f be Point of F, g be Point of G;
redefine func [e,f,g] -> Element of [:E,F,G:];
end;
registration
let E,F,G be Abelian non empty RLSStruct;
cluster [:E,F,G:] -> Abelian;
end;
registration
let E,F,G be add-associative non empty RLSStruct;
cluster [:E,F,G:] -> add-associative;
end;
registration
let E,F,G be right_zeroed non empty RLSStruct;
cluster [:E,F,G:] -> right_zeroed;
end;
registration
let E,F,G be right_complementable non empty RLSStruct;
cluster [:E,F,G:] -> right_complementable;
end;
theorem :: PRVECT_4:5
for E,F,G be non empty RLSStruct holds
( for x be set holds
(x is Point of [:E,F,G:]
iff ex x1 be Point of E, x2 be Point of F,
x3 be Point of G st x=[x1,x2,x3]) )
& ( for x1,y1 be Point of E, x2,y2 be Point of F, x3,y3 be Point of G
holds [x1,x2,x3]+[y1,y2,y3] = [x1+y1,x2+y2,x3+y3] )
& 0.[:E,F,G:] = [0.E,0.F,0.G]
& ( for x1 be Point of E, x2 be Point of F, x3 be Point of G, a be Real
holds a*[x1,x2,x3] = [a*x1,a*x2,a*x3] );
theorem :: PRVECT_4:6
for E,F,G be add-associative right_zeroed
right_complementable non empty RLSStruct,
x1 be Point of E, x2 be Point of F, x3 be Point of G
holds -[x1,x2,x3] = [-x1,-x2,-x3];
registration
let E,F,G be vector-distributive non empty RLSStruct;
cluster [:E,F,G:] -> vector-distributive;
end;
registration
let E,F,G be scalar-distributive non empty RLSStruct;
cluster [:E,F,G:] -> scalar-distributive;
end;
registration
let E,F,G be scalar-associative non empty RLSStruct;
cluster [:E,F,G:] -> scalar-associative;
end;
registration
let E,F,G be scalar-unital non empty RLSStruct;
cluster [:E,F,G:] -> scalar-unital;
end;
registration
let E,F,G be Abelian add-associative right_zeroed right_complementable
scalar-distributive vector-distributive scalar-associative
scalar-unital non empty RLSStruct;
cluster <* E,F,G *> -> RealLinearSpace-yielding;
end;
theorem :: PRVECT_4:7
for X,Y,Z be RealLinearSpace holds
ex I be Function of [:X,Y,Z:],product <*X,Y,Z*>
st I is one-to-one & I is onto
& ( for x be Point of X, y be Point of Y, z be Point of Z
holds I.(x,y,z) = <*x,y,z*> )
& ( for v,w be Point of [:X,Y,Z:] holds I.(v+w)=(I.v) + (I.w) )
& ( for v be Point of [:X,Y,Z:], r be Real
holds I.(r*v)=r*(I.v) )
& I.(0.[:X,Y,Z:])=0.product <*X,Y,Z*>;
definition
let E,F,G be RealLinearSpace;
let e be Point of E, f be Point of F, g be Point of G;
redefine func <*e,f,g*> -> Element of product <*E,F,G*>;
end;
theorem :: PRVECT_4:8
for E,F,G be RealLinearSpace holds
( for x be set holds
( x is Point of product <*E,F,G*>
iff ex x1 be Point of E, x2 be Point of F, x3 be Point of G st
x=<* x1,x2,x3 *> ) )
& ( for x1,y1 be Point of E, x2,y2 be Point of F, x3,y3 be 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 be Point of E, x2 be Point of F, x3 be Point of G
holds -<* x1,x2,x3 *> = <* -x1,-x2,-x3 *> )
& ( for x1 be Point of E, x2 be Point of F, x3 be Point of G, a be Real
holds a*<*x1,x2,x3*> = <* a*x1,a*x2,a*x3 *> );
begin ::3-fold Product Space of Real Normed Spaces
definition let E,F,G be non empty NORMSTR;
func [:E,F,G:] -> strict non empty NORMSTR equals
:: PRVECT_4:def 3
[:[:E,F:],G:];
end;
definition
let E,F,G be non empty NORMSTR;
let e be Point of E, f be Point of F, g be Point of G;
redefine func [e,f,g] -> Element of [:E,F,G:];
end;
registration
let E,F,G be RealNormSpace;
cluster [:E,F,G:] -> reflexive discerning RealNormSpace-like
scalar-distributive vector-distributive scalar-associative scalar-unital
Abelian add-associative right_zeroed right_complementable;
end;
registration
let E,F,G be RealNormSpace;
cluster <*E,F,G*> -> RealNormSpace-yielding;
end;
theorem :: PRVECT_4:9
for E,F,G be RealNormSpace holds
( for x be set holds
( x is Point of [:E,F,G:]
iff ex x1 be Point of E,x2 be Point of F,
x3 be Point of G
st x=[x1,x2,x3]) )
& ( for x1,y1 be Point of E, x2,y2 be Point of F, x3,y3 be Point of G
holds [x1,x2,x3]+[y1,y2,y3] = [x1+y1,x2+y2,x3+y3] )
& 0.[:E,F,G:] = [0.E,0.F,0.G]
& ( for x1 be Point of E, x2 be Point of F,x3 be Point of G, a be Real
holds a*[x1,x2,x3] = [a*x1,a*x2,a*x3] )
& ( for x1 be Point of E, x2 be Point of F, x3 be Point of G
holds -[x1,x2,x3] = [-x1,-x2,-x3] )
& ( for x1 be Point of E, x2 be Point of F,x3 be Point of G
holds ||. [x1,x2,x3] .|| = sqrt( ||.x1.||^2 + ||.x2.||^2 + ||.x3.||^2 )
&
ex w be Element of REAL 3 st
w = <* ||.x1.||,||.x2.||,||.x3.|| *> & ||. [x1,x2,x3] .|| = |.w.| );
theorem :: PRVECT_4:10
for X,Y,Z be RealNormSpace
holds ex I be Function of [:X,Y,Z:],product <*X,Y,Z*>
st I is one-to-one & I is onto
& ( for x be Point of X, y be Point of Y, z be Point of Z
holds I.(x,y,z) = <*x,y,z*> )
& ( for v,w be Point of [:X,Y,Z:] holds I.(v+w) = I.v + I.w )
& ( for v be Point of [:X,Y,Z:], r be Real holds I.(r*v)=r*(I.v) )
& 0. product <*X,Y,Z*> = I.(0.[:X,Y,Z:])
& ( for v be Point of [:X,Y,Z:] holds ||. I.v .|| = ||.v.|| );
definition
let E,F,G be RealNormSpace;
let e be Point of E, f be Point of F, g be Point of G;
redefine func <*e,f,g*> -> Element of product <*E,F,G*>;
end;
theorem :: PRVECT_4:11
for E,F,G be RealNormSpace holds
( for x be set holds
( x is Point of product <*E,F,G*>
iff ex x1 be Point of E, x2 be Point of F,
x3 be Point of G st x=<* x1,x2,x3 *> ) )
& ( for x1,y1 be Point of E, x2,y2 be Point of F, x3,y3 be 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 be Point of E, x2 be Point of F, x3 be Point of G
holds -<*x1,x2,x3*> = <* -x1,-x2,-x3 *> )
& ( for x1 be Point of E, x2 be Point of F, x3 be Point of G, a be Real
holds a*<*x1,x2,x3*> = <* a*x1,a*x2,a*x3 *> )
& ( for x1 be Point of E, x2 be Point of F, x3 be Point of G
holds
||. <*x1,x2,x3*> .|| = sqrt (||.x1.||^2+||.x2.||^2+||.x3.||^2)
&
ex w be Element of REAL 3 st
w=<* ||.x1.||,||.x2.||,||.x3.|| *> & ||. <*x1,x2,x3*> .|| = |.w.| );
registration
let E,F,G be complete RealNormSpace;
cluster [:E,F,G:] -> complete;
end;