:: 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;