:: Cartesian Products of Family of Real Linear Spaces :: by Hiroyuki Okazaki , Noboru Endou and Yasunari Shidama :: :: Received August 17, 2010 :: Copyright (c) 2010-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, 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 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; constructors REAL_1, SQUARE_1, RSSPACE3, COMPLEX1, LOPBAN_1, RVSUM_1, BINOP_2, PRVECT_2, FINSEQ_4, RFINSEQ, FINSEQOP, TOPMETR; 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, PRVECT_1; requirements SUBSET, BOOLE, NUMERALS, ARITHM; begin :: Preliminaries reserve G,F for RealLinearSpace; theorem :: PRVECT_3:1 for D,E,F,G be non empty set ex I be Function of [: [:D,E:],[:F,G:] :], [:[:D,F:],[:E,G:]:] st I is one-to-one & I is onto & for d,e,f,g be set st d in D & e in E & f in F & g in G holds I.([d,e],[f,g]) = [[d,f],[e,g]]; theorem :: PRVECT_3:2 for X be non empty set, D be Function st dom D = {1} & D.1 = X ex I be Function of X,product D st I is one-to-one & I is onto & for x be object st x in X holds I.x = <*x*>; theorem :: PRVECT_3:3 for X,Y be non empty set, D be Function st dom D = {1,2} & D.1 = X & D.2 = Y ex I be Function of [:X,Y:],product D st I is one-to-one & I is onto & for x,y be object st x in X & y in Y holds I.(x,y) = <*x,y*>; theorem :: PRVECT_3:4 for X be non empty set ex I be Function of X,product <*X*> st I is one-to-one & I is onto & for x be object st x in X holds I.x = <*x*>; registration let X,Y be non-empty non empty FinSequence; cluster X^Y -> non-empty; end; theorem :: PRVECT_3:5 for X,Y be non empty set ex I be Function of [:X,Y:],product <*X,Y*> st I is one-to-one & I is onto & for x,y be object st x in X & y in Y holds I.(x,y) = <*x,y*>; theorem :: PRVECT_3:6 for X,Y be non-empty non empty FinSequence ex I be Function of [: product X,product Y :],product(X^Y) st I is one-to-one & I is onto & for x,y be FinSequence st x in product X & y in product Y holds I.(x,y) = x^y; definition let G,F be non empty addLoopStr; func prod_ADD(G,F) -> BinOp of [:the carrier of G,the carrier of F:] means :: PRVECT_3:def 1 for g1,g2 be Point of G, f1,f2 be Point of F holds it.([g1,f1],[g2,f2]) = [g1+g2,f1+f2]; end; definition let G,F be non empty RLSStruct; func prod_MLT(G,F) -> Function of [:REAL, [:the carrier of G,the carrier of F:] :], [:the carrier of G,the carrier of F:] means :: PRVECT_3:def 2 for r be Real, g be Point of G, f be Point of F holds it.(r,[g,f]) = [r*g,r*f]; end; definition let G,F be non empty addLoopStr; func prod_ZERO(G,F) -> Element of [:the carrier of G,the carrier of F:] equals :: PRVECT_3:def 3 [0.G,0.F]; end; definition let G,F be non empty addLoopStr; func [:G,F:] -> strict non empty addLoopStr equals :: PRVECT_3:def 4 addLoopStr (# [:the carrier of G,the carrier of F:], prod_ADD(G,F), prod_ZERO(G,F) #); end; definition let G,F be non empty addLoopStr; let g be Element of G, f be Element of F; redefine func [g,f] -> Element of [:G,F:]; end; registration let G,F be Abelian non empty addLoopStr; cluster [:G,F:] -> Abelian; end; registration let G,F be add-associative non empty addLoopStr; cluster [:G,F:] -> add-associative; end; registration let G,F be right_zeroed non empty addLoopStr; cluster [:G,F:] -> right_zeroed; end; registration let G,F be right_complementable non empty addLoopStr; cluster [:G,F:] -> right_complementable; end; theorem :: PRVECT_3:7 for G,F be non empty addLoopStr holds ( for x be set holds (x is Point of [:G,F:] iff ex x1 be Point of G, x2 be Point of F st x=[x1,x2]) ) & ( for x,y be Point of [:G,F:], x1,y1 be Point of G ,x2,y2 be Point of F st x=[x1,x2] & y=[y1,y2] holds x+y = [x1+y1,x2+y2] ) & 0.[:G,F:] = [0.G,0.F]; theorem :: PRVECT_3:8 for G,F be add-associative right_zeroed right_complementable non empty addLoopStr, x be Point of [:G,F:], x1 be Point of G, x2 be Point of F st x=[x1,x2] holds -x = [-x1,-x2]; registration let G,F be Abelian add-associative right_zeroed right_complementable strict non empty addLoopStr; cluster [:G,F:] -> strict Abelian add-associative right_zeroed right_complementable; end; definition let G,F be non empty RLSStruct; func [:G,F:] -> strict non empty RLSStruct equals :: PRVECT_3:def 5 RLSStruct (# [:the carrier of G,the carrier of F:], prod_ZERO(G,F), prod_ADD(G,F), prod_MLT(G,F) #); end; definition let G,F be non empty RLSStruct; let g be Element of G, f be Element of F; redefine func [g,f] -> Element of [:G,F:]; end; registration let G,F be Abelian non empty RLSStruct; cluster [:G,F:] -> Abelian; end; registration let G,F be add-associative non empty RLSStruct; cluster [:G,F:] -> add-associative; end; registration let G,F be right_zeroed non empty RLSStruct; cluster [:G,F:] -> right_zeroed; end; registration let G,F be right_complementable non empty RLSStruct; cluster [:G,F:] -> right_complementable; end; theorem :: PRVECT_3:9 for G,F be non empty RLSStruct holds ( for x be set holds (x is Point of [:G,F:] iff ex x1 be Point of G, x2 be Point of F st x=[x1,x2]) ) & ( for x,y be Point of [:G,F:], x1,y1 be Point of G, x2,y2 be 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 be Point of [:G,F:], x1 be Point of G, x2 be Point of F, a be Real st x=[x1,x2] holds a*x = [a*x1,a*x2] ); theorem :: PRVECT_3:10 for G,F be add-associative right_zeroed right_complementable non empty RLSStruct, x be Point of [:G,F:], x1 be Point of G, x2 be Point of F st x=[x1,x2] holds -x = [-x1,-x2]; registration let G,F be vector-distributive non empty RLSStruct; cluster [:G,F:] -> vector-distributive; end; registration let G,F be scalar-distributive non empty RLSStruct; cluster [:G,F:] -> scalar-distributive; end; registration let G,F be scalar-associative non empty RLSStruct; cluster [:G,F:] -> scalar-associative; end; registration let G,F be scalar-unital non empty RLSStruct; cluster [:G,F:] -> scalar-unital; end; registration let G be Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty RLSStruct; cluster <* G *> -> RealLinearSpace-yielding; end; registration let G,F be Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty RLSStruct; cluster <* G,F *> -> RealLinearSpace-yielding; end; begin :: Cartesian Product of Real Linear Spaces theorem :: PRVECT_3:11 for X be RealLinearSpace holds ex I be Function of X, product <*X*> st I is one-to-one & I is onto & ( for x be Point of X holds I.x = <*x*> ) & ( for v,w be Point of X holds I.(v+w) = I.v + I.w ) & ( for v be Point of X, r be Element of REAL holds I.(r*v)=r*(I.v) ) & I.(0.X)=0.product <*X*>; registration let G,F be non empty RealLinearSpace-yielding FinSequence; cluster G^F -> RealLinearSpace-yielding; end; theorem :: PRVECT_3:12 for X,Y be RealLinearSpace holds ex I be Function of [:X,Y:],product <*X,Y*> st I is one-to-one & I is onto & ( for x be Point of X, y be Point of Y holds I.(x,y) = <*x,y*> ) & ( for v,w be Point of [:X,Y:] holds I.(v+w)=(I.v) + (I.w) ) & ( for v be Point of [:X,Y:], r be Real holds I.(r*v)=r*(I.v) ) & I.(0.[:X,Y:])=0.product <*X,Y*>; theorem :: PRVECT_3:13 for X,Y be non empty RealLinearSpace-Sequence holds ex I be Function of [:product X,product Y:],product (X^Y) st I is one-to-one & I is onto & ( for x be Point of product X, y be Point of product Y holds ex x1,y1 be FinSequence st x=x1 & y=y1 & I.(x,y) = x1^y1 ) & ( for v,w be Point of [:product X,product Y:] holds I.(v+w) = I.v + I.w ) & ( for v be Point of [:product X,product Y:], r be Element of REAL holds I.(r*v)=r*(I.v) ) & I.(0.[:product X,product Y:]) = 0.product (X^Y); theorem :: PRVECT_3:14 for G,F be RealLinearSpace holds ( for x be set holds ( x is Point of product <*G,F*> iff ex x1 be Point of G, x2 be Point of F st x=<* x1,x2 *> ) ) & ( for x,y be Point of product <*G,F*>, x1,y1 be Point of G ,x2,y2 be 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 be Point of product <*G,F*>, x1 be Point of G, x2 be Point of F st x=<* x1,x2 *> holds -x = <* -x1,-x2 *> ) & ( for x be Point of product <*G,F*>, x1 be Point of G, x2 be Point of F, a be Real st x = <*x1,x2*> holds a*x = <* a*x1,a*x2 *> ); begin :: Cartesian Product of Real Normed Linear Spaces definition let G,F be non empty NORMSTR; func prod_NORM(G,F) -> Function of [:the carrier of G,the carrier of F:], REAL means :: PRVECT_3:def 6 for g be Point of G, f be Point of F holds ex v be Element of REAL 2 st v= <* ||.g.||,||.f.|| *> & it.(g,f) = |.v.|; end; definition let G,F be non empty NORMSTR; func [:G,F:] -> strict non empty NORMSTR equals :: PRVECT_3:def 7 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) #); end; definition let G,F be non empty NORMSTR; let g be Element of G, f be Element of F; redefine func [g,f] -> Element of [:G,F:]; end; registration let G,F be RealNormSpace; cluster [:G,F:] -> reflexive discerning RealNormSpace-like; end; registration let G,F be reflexive discerning RealNormSpace-like scalar-distributive vector-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable non empty NORMSTR; cluster [:G,F:] -> strict reflexive discerning RealNormSpace-like scalar-distributive vector-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable; end; registration let G be reflexive discerning RealNormSpace-like scalar-distributive vector-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable non empty NORMSTR; cluster <*G*> -> RealNormSpace-yielding; end; registration let G,F be reflexive discerning RealNormSpace-like scalar-distributive vector-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable non empty NORMSTR; cluster <*G,F*> -> RealNormSpace-yielding; end; theorem :: PRVECT_3:15 for X,Y be RealNormSpace holds ex I be Function of [:X,Y:],product <*X,Y*> st I is one-to-one & I is onto & ( for x be Point of X, y be Point of Y holds I.(x,y) = <*x,y*> ) & ( for v,w be Point of [:X,Y:] holds I.(v+w) = I.v + I.w ) & ( for v be Point of [:X,Y:], r be Real holds I.(r*v)=r*(I.v) ) & 0. product <*X,Y*> = I.(0.[:X,Y:]) & ( for v be Point of [:X,Y:] holds ||. I.v .|| = ||.v.|| ); theorem :: PRVECT_3:16 for X be RealNormSpace holds ex I be Function of X ,product <*X*> st I is one-to-one & I is onto & ( for x be Point of X holds I.x = <*x*> ) & ( for v,w be Point of X holds I.(v+w) = I.v + I.w ) & ( for v be Point of X, r be Element of REAL holds I.(r*v)=r*(I.v) ) & 0. product <*X*> = I.(0.X) & ( for v be Point of X holds ||. I.v .|| = ||.v.|| ); registration let G,F be non empty RealNormSpace-yielding FinSequence; cluster G^F -> non empty RealNormSpace-yielding; end; theorem :: PRVECT_3:17 for X,Y be non empty RealNormSpace-Sequence holds ex I be Function of [:product X,product Y:],product (X^Y) st I is one-to-one & I is onto & ( for x be Point of product X, y be Point of product Y holds ex x1,y1 be FinSequence st x=x1 & y=y1 & I.(x,y) = x1^y1 ) & ( for v,w be Point of [:product X,product Y:] holds I.(v+w) = I.v + I.w ) & ( for v be Point of [:product X,product Y:], r be Element of REAL holds I.(r*v)=r*(I.v) ) & I.(0.[:product X,product Y:]) = 0.product (X^Y) & ( for v be Point of [:product X,product Y:] holds ||. I.v .|| = ||.v.|| ); theorem :: PRVECT_3:18 for G,F be RealNormSpace holds ( for x be set holds ( x is Point of [:G,F:] iff ex x1 be Point of G ,x2 be Point of F st x=[x1,x2]) ) & ( for x,y be Point of [:G,F:], x1,y1 be Point of G, x2,y2 be 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 be Point of [:G,F:], x1 be Point of G, x2 be Point of F st x=[x1,x2] holds -x = [-x1,-x2] ) & ( for x be Point of [:G,F:], x1 be Point of G, x2 be Point of F, a be Real st x=[x1,x2] holds a*x = [a*x1,a*x2] ) & ( for x be Point of [:G,F:], x1 be Point of G, x2 be Point of F st x=[x1,x2] holds ex w be Element of REAL 2 st w=<* ||.x1.||,||.x2.|| *> & ||.x.|| = |.w.| ); theorem :: PRVECT_3:19 for G,F be RealNormSpace holds ( for x be set holds ( x is Point of product <*G,F*> iff ex x1 be Point of G, x2 be Point of F st x=<* x1,x2 *> ) ) & ( for x,y be Point of product <*G,F*>, x1,y1 be Point of G, x2,y2 be 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 be Point of product <*G,F*>, x1 be Point of G, x2 be Point of F st x=<*x1,x2*> holds -x = <* -x1,-x2 *> ) & ( for x be Point of product <*G,F*>, x1 be Point of G, x2 be Point of F, a be Real st x=<*x1,x2*> holds a*x = <* a*x1,a*x2 *> ) & ( for x be Point of product <*G,F*>, x1 be Point of G, x2 be Point of F st x=<*x1,x2*> holds ex w be Element of REAL 2 st w=<* ||.x1.||,||.x2.|| *> & ||.x.|| = |.w.| ); registration let X,Y be complete RealNormSpace; cluster [:X,Y:] -> complete; end; theorem :: PRVECT_3:20 for X,Y be non empty RealNormSpace-Sequence holds ex I be Function of product <* product X,product Y *>,product (X^Y) st I is one-to-one & I is onto & ( for x be Point of product X, y be Point of product Y holds ex x1,y1 be FinSequence st x=x1 & y=y1 & I.<*x,y*> = x1^y1 ) & ( for v,w be Point of product <* product X,product Y *> holds I.(v+w) = I.v + I.w ) & ( for v be Point of product <* product X,product Y *>, r be Element of REAL holds I.(r*v)=r*(I.v) ) & I.(0.(product <* product X,product Y *>)) = 0.product (X^Y) & ( for v be Point of product <* product X,product Y *> holds ||. I.v .|| = ||.v.|| ); theorem :: PRVECT_3:21 for X,Y be non empty RealLinearSpace holds ex I be Function of [:X,Y:],[:X,product <*Y*>:] st I is one-to-one & I is onto & ( for x be Point of X, y be Point of Y holds I.(x,y) = [x,<*y*>] ) & ( for v,w be Point of [:X,Y:] holds I.(v+w) = I.v + I.w ) & ( for v be Point of [:X,Y:], r be Element of REAL holds I.(r*v)=r*(I.v) ) & I.(0.[:X,Y:]) = 0.([:X,product<*Y*>:]); theorem :: PRVECT_3:22 for X be non empty RealLinearSpace-Sequence, Y be RealLinearSpace holds ex I be Function of [:product X,Y:],product(X^<*Y*>) st I is one-to-one & I is onto & ( for x be Point of product X, y be Point of Y ex x1,y1 be FinSequence st x=x1 & <*y*> =y1 & I.(x,y) = x1^y1 ) & ( for v,w be Point of [:product X,Y:] holds I.(v+w) = I.v + I.w ) & ( for v be Point of [:product X,Y:], r be Element of REAL holds I.(r*v)=r*(I.v) ) & I.(0.[:product X,Y:]) = 0.product (X^<*Y*>); theorem :: PRVECT_3:23 for X ,Y be non empty RealNormSpace ex I be Function of [:X,Y:],[:X,product<*Y*>:] st I is one-to-one & I is onto & ( for x be Point of X, y be Point of Y holds I.(x,y) = [x,<*y*>] ) & ( for v,w be Point of [:X,Y:] holds I.(v+w) = I.v + I.w ) & ( for v be Point of [:X,Y:], r be Element of REAL holds I.(r*v)=r*(I.v) ) & I.(0.[:X,Y:]) = 0.([:X,product <*Y*>:]) & ( for v be Point of [:X,Y:] holds ||. I.v .|| = ||.v.|| ); theorem :: PRVECT_3:24 for X be non empty RealNormSpace-Sequence, Y be RealNormSpace ex I be Function of [:product X,Y:],product(X^<*Y*>) st I is one-to-one & I is onto & ( for x be Point of product X, y be Point of Y ex x1,y1 be FinSequence st x=x1 & <*y*>=y1 & I.(x,y) = x1^y1 ) & ( for v,w be Point of [:product X,Y:] holds I.(v+w) = I.v + I.w ) & ( for v be Point of [:product X,Y:], r be Element of REAL holds I.(r*v)=r*(I.v) ) & I.(0.[:product X,Y:]) = 0.product(X^<*Y*>) & ( for v be Point of [:product X,Y:] holds ||. I.v .|| = ||.v.|| );