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

scheme :: PRVECT_4:sch 1
FuncEx3A{ F₁() -> set , F₂() -> set , F₃() -> set , F₄() -> set , P₁[ object , object , object , object ] } :

ex f being Function of [:F₁(),F₂(),F₃():],F₄() st
for x, y, w being object st x in F₁() & y in F₂() & w in F₃() holds
P₁[x,y,w,f . (x,y,w)]

provided

A1: for x, y, w being object st x in F₁() & y in F₂() & w in F₃() holds
ex z being object st
( z in F₄() & P₁[x,y,w,z] )

proof end;

theorem Th4: :: PRVECT_4:1

for X, Y, Z being non empty set
for D being Function st dom D = {1,2,3} & D . 1 = X & D . 2 = Y & D . 3 = Z holds
ex I being Function of [:X,Y,Z:],(product D) st
( I is one-to-one & I is onto & ( for x, y, z being object st x in X & y in Y & z in Z holds
I . (x,y,z) = <*x,y,z*> ) )

proof end;

theorem Th5: :: PRVECT_4:2

for X, Y, Z being non empty set ex I being Function of [:X,Y,Z:],(product <*X,Y,Z*>) st
( I is one-to-one & I is onto & ( for x, y, z being object st x in X & y in Y & z in Z holds
I . (x,y,z) = <*x,y,z*> ) )

proof end;

definition

let E, F, G be non empty addLoopStr ;

func [:E,F,G:] -> non empty strict addLoopStr equals :: PRVECT_4:def 1
[:[:E,F:],G:];

coherence
[:[:E,F:],G:] is non empty strict addLoopStr ;

end;

:: deftheorem defines [: PRVECT_4:def 1 :
for E, F, G being non empty addLoopStr holds [:E,F,G:] = [:[:E,F:],G:];

definition

let E, F, G be non empty addLoopStr ;
let e be Point of E;
let f be Point of F;
let g be Point of G;
:: original: [
redefine func [e,f,g] -> Element of [:E,F,G:];
coherence
[e,f,g] is Element of [:E,F,G:]

proof end;

end;

registration

let E, F, G be non empty Abelian addLoopStr ;

cluster [:E,F,G:] -> non empty strict Abelian ;

coherence
[:E,F,G:] is Abelian ;

end;

registration

let E, F, G be non empty add-associative addLoopStr ;

cluster [:E,F,G:] -> non empty strict add-associative ;

coherence
[:E,F,G:] is add-associative ;

end;

registration

let E, F, G be non empty right_zeroed addLoopStr ;

cluster [:E,F,G:] -> non empty strict right_zeroed ;

coherence
[:E,F,G:] is right_zeroed ;

end;

registration

let E, F, G be non empty right_complementable addLoopStr ;

cluster [:E,F,G:] -> non empty strict right_complementable ;

coherence
[:E,F,G:] is right_complementable ;

end;

theorem :: PRVECT_4:3

for E, F, G being non empty addLoopStr holds
( ( for x being set holds
( x is Point of [: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. [:E,F,G:] = [(0. E),(0. F),(0. G)] )

proof end;

theorem :: PRVECT_4:4

for E, F, G being non empty right_complementable add-associative right_zeroed addLoopStr
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)]

proof end;

definition

let E, F, G be non empty RLSStruct ;

func [:E,F,G:] -> non empty strict RLSStruct equals :: PRVECT_4:def 2
[:[:E,F:],G:];

coherence
[:[:E,F:],G:] is non empty strict RLSStruct ;

end;

:: deftheorem defines [: PRVECT_4:def 2 :
for E, F, G being non empty RLSStruct holds [:E,F,G:] = [:[:E,F:],G:];

definition

let E, F, G be non empty RLSStruct ;
let e be Point of E;
let f be Point of F;
let g be Point of G;
:: original: [
redefine func [e,f,g] -> Element of [:E,F,G:];
coherence
[e,f,g] is Element of [:E,F,G:]

proof end;

end;

registration

let E, F, G be non empty Abelian RLSStruct ;

cluster [:E,F,G:] -> non empty strict Abelian ;

coherence
[:E,F,G:] is Abelian ;

end;

registration

let E, F, G be non empty add-associative RLSStruct ;

cluster [:E,F,G:] -> non empty strict add-associative ;

coherence
[:E,F,G:] is add-associative ;

end;

registration

let E, F, G be non empty right_zeroed RLSStruct ;

cluster [:E,F,G:] -> non empty strict right_zeroed ;

coherence
[:E,F,G:] is right_zeroed ;

end;

registration

let E, F, G be non empty right_complementable RLSStruct ;

cluster [:E,F,G:] -> non empty right_complementable strict ;

coherence
[:E,F,G:] is right_complementable ;

end;

theorem Th8: :: PRVECT_4:5

for E, F, G being non empty RLSStruct holds
( ( for x being set holds
( x is Point of [: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. [: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
for a being Real holds a * [x1,x2,x3] = [(a * x1),(a * x2),(a * x3)] ) )

proof end;

theorem :: PRVECT_4:6

for E, F, G being non empty right_complementable add-associative right_zeroed RLSStruct
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)]

proof end;

registration

let E, F, G be non empty vector-distributive RLSStruct ;

cluster [:E,F,G:] -> non empty strict vector-distributive ;

correctness
coherence
[:E,F,G:] is vector-distributive ;
;

end;

registration

let E, F, G be non empty scalar-distributive RLSStruct ;

cluster [:E,F,G:] -> non empty strict scalar-distributive ;

correctness
coherence
[:E,F,G:] is scalar-distributive ;
;

end;

registration

let E, F, G be non empty scalar-associative RLSStruct ;

cluster [:E,F,G:] -> non empty strict scalar-associative ;

correctness
coherence
[:E,F,G:] is scalar-associative ;
;

end;

registration

let E, F, G be non empty scalar-unital RLSStruct ;

cluster [:E,F,G:] -> non empty strict scalar-unital ;

correctness
coherence
[:E,F,G:] is scalar-unital ;
;

end;

registration

let E, F, G be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ;

cluster <*E,F,G*> -> RealLinearSpace-yielding ;

correctness
coherence
<*E,F,G*> is RealLinearSpace-yielding ;

proof end;

end;

Lm1: for E, F, G being 1-sorted
for x being object st x in [: the carrier of E, the carrier of F, the carrier of G:] holds
ex x1 being Point of E ex x2 being Point of F ex x3 being Point of G st x = [x1,x2,x3]

proof end;

theorem Th11: :: PRVECT_4:7

for X, Y, Z being RealLinearSpace ex I being Function of [:X,Y,Z:],(product <*X,Y,Z*>) st
( I is one-to-one & I is onto & ( for x being Point of X
for y being Point of Y
for z being Point of Z holds I . (x,y,z) = <*x,y,z*> ) & ( for v, w being Point of [:X,Y,Z:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:X,Y,Z:]
for r being Real holds I . (r * v) = r * (I . v) ) & I . (0. [:X,Y,Z:]) = 0. (product <*X,Y,Z*>) )

proof end;

definition

let E, F, G be RealLinearSpace;
let e be Point of E;
let f be Point of F;
let g be Point of G;
:: original: <*
redefine func <*e,f,g*> -> Element of (product <*E,F,G*>);
coherence
<*e,f,g*> is Element of (product <*E,F,G*>)

proof end;

end;

theorem :: PRVECT_4:8

for E, F, G being RealLinearSpace holds
( ( 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 end;

definition

let E, F, G be non empty NORMSTR ;

func [:E,F,G:] -> non empty strict NORMSTR equals :: PRVECT_4:def 3
[:[:E,F:],G:];

coherence
[:[:E,F:],G:] is non empty strict NORMSTR ;

end;

:: deftheorem defines [: PRVECT_4:def 3 :
for E, F, G being non empty NORMSTR holds [:E,F,G:] = [:[:E,F:],G:];

definition

let E, F, G be non empty NORMSTR ;
let e be Point of E;
let f be Point of F;
let g be Point of G;
:: original: [
redefine func [e,f,g] -> Element of [:E,F,G:];
coherence
[e,f,g] is Element of [:E,F,G:]

proof end;

end;

registration

let E, F, G be RealNormSpace;

cluster [:E,F,G:] -> non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive strict RealNormSpace-like ;

coherence
( [:E,F,G:] is reflexive & [:E,F,G:] is discerning & [:E,F,G:] is RealNormSpace-like & [:E,F,G:] is scalar-distributive & [:E,F,G:] is vector-distributive & [:E,F,G:] is scalar-associative & [:E,F,G:] is scalar-unital & [:E,F,G:] is Abelian & [:E,F,G:] is add-associative & [:E,F,G:] is right_zeroed & [:E,F,G:] is right_complementable ) ;

end;

registration

let E, F, G be RealNormSpace;

cluster <*E,F,G*> -> RealNormSpace-yielding ;

correctness
coherence
<*E,F,G*> is RealNormSpace-yielding ;

proof end;

end;

theorem Th14: :: PRVECT_4:9

for E, F, G being RealNormSpace holds
( ( for x being set holds
( x is Point of [: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. [: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
for a being Real holds a * [x1,x2,x3] = [(a * x1),(a * x2),(a * x3)] ) & ( 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 holds
( ||.[x1,x2,x3].|| = sqrt (((||.x1.|| ^2) + (||.x2.|| ^2)) + (||.x3.|| ^2)) & ex w being Element of REAL 3 st
( w = <*||.x1.||,||.x2.||,||.x3.||*> & ||.[x1,x2,x3].|| = |.w.| ) ) ) )

proof end;

theorem Th15: :: PRVECT_4:10

for X, Y, Z being RealNormSpace ex I being Function of [:X,Y,Z:],(product <*X,Y,Z*>) st
( I is one-to-one & I is onto & ( for x being Point of X
for y being Point of Y
for z being Point of Z holds I . (x,y,z) = <*x,y,z*> ) & ( for v, w being Point of [:X,Y,Z:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:X,Y,Z:]
for r being Real holds I . (r * v) = r * (I . v) ) & 0. (product <*X,Y,Z*>) = I . (0. [:X,Y,Z:]) & ( for v being Point of [:X,Y,Z:] holds ||.(I . v).|| = ||.v.|| ) )

proof end;

definition

let E, F, G be RealNormSpace;
let e be Point of E;
let f be Point of F;
let g be Point of G;
:: original: <*
redefine func <*e,f,g*> -> Element of (product <*E,F,G*>);
coherence
<*e,f,g*> is Element of (product <*E,F,G*>)

proof end;

end;

theorem :: PRVECT_4:11

for E, F, G being RealNormSpace holds
( ( 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)*> ) & ( for x1 being Point of E
for x2 being Point of F
for x3 being Point of G holds
( ||.<*x1,x2,x3*>.|| = sqrt (((||.x1.|| ^2) + (||.x2.|| ^2)) + (||.x3.|| ^2)) & ex w being Element of REAL 3 st
( w = <*||.x1.||,||.x2.||,||.x3.||*> & ||.<*x1,x2,x3*>.|| = |.w.| ) ) ) )

proof end;

registration

let E, F, G be complete RealNormSpace;

cluster [:E,F,G:] -> non empty strict complete ;

coherence
[:E,F,G:] is complete ;

end;