:: 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{ F1() -> set , F2() -> set , F3() -> set , F4() -> set , P1[ object , object , object , object ] } :
ex f being Function of [:F1(),F2(),F3():],F4() st
for x, y, w being object st x in F1() & y in F2() & w in F3() holds
P1[x,y,w,f . (x,y,w)]
provided
A1: for x, y, w being object st x in F1() & y in F2() & w in F3() holds
ex z being object st
( z in F4() & P1[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;