:: by Hiroyuki Okazaki and Kazuhisa Nakasho

::

:: Received November 30, 2021

:: Copyright (c) 2021 Association of Mizar Users

scheme :: PRVECT_4:sch 1

FuncEx3A{ F_{1}() -> set , F_{2}() -> set , F_{3}() -> set , F_{4}() -> set , P_{1}[ object , object , object , object ] } :

FuncEx3A{ F

ex f being Function of [:F_{1}(),F_{2}(),F_{3}():],F_{4}() st

for x, y, w being object st x in F_{1}() & y in F_{2}() & w in F_{3}() holds

P_{1}[x,y,w,f . (x,y,w)]

providedfor x, y, w being object st x in F

P

A1:
for x, y, w being object st x in F_{1}() & y in F_{2}() & w in F_{3}() holds

ex z being object st

( z in F_{4}() & P_{1}[x,y,w,z] )

ex z being object st

( z in F

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*> ) )

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*> ) )

( 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
end;

:: deftheorem defines [: PRVECT_4:def 1 :

for E, F, G being non empty addLoopStr holds [:E,F,G:] = [:[:E,F:],G:];

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

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

registration
end;

registration
end;

registration

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

coherence

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

end;
coherence

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

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)] )

( ( 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)]

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

:: deftheorem defines [: PRVECT_4:def 2 :

for E, F, G being non empty RLSStruct holds [:E,F,G:] = [:[:E,F:],G:];

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

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

registration
end;

registration
end;

registration

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

coherence

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

end;
coherence

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

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)] ) )

( ( 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)]

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 ;

correctness

coherence

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

;

end;
correctness

coherence

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

;

registration

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

correctness

coherence

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

;

end;
correctness

coherence

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

;

registration

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

correctness

coherence

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

;

end;
correctness

coherence

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

;

registration

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

correctness

coherence

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

;

end;
correctness

coherence

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

;

registration

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

correctness

coherence

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

end;
correctness

coherence

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

proof 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*>) )

( 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*>)

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

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)*> ) )

( ( 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
end;

:: deftheorem defines [: PRVECT_4:def 3 :

for E, F, G being non empty NORMSTR holds [:E,F,G:] = [:[:E,F:],G:];

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

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

registration

let E, F, G be RealNormSpace;

( [: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;
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 ) ;

registration

let E, F, G be RealNormSpace;

correctness

coherence

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

end;
correctness

coherence

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

proof 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.| ) ) ) )

( ( 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.|| ) )

( 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*>)

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

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.| ) ) ) )

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