:: by Hiroyuki Okazaki , Noboru Endou and Yasunari Shidama

::

:: Received August 17, 2010

:: Copyright (c) 2010-2021 Association of Mizar Users

theorem :: PRVECT_3:1

for D, E, F, G being non empty set ex I being Function of [:[:D,E:],[:F,G:]:],[:[:D,F:],[:E,G:]:] st

( I is one-to-one & I is onto & ( for d, e, f, g being set st d in D & e in E & f in F & g in G holds

I . ([d,e],[f,g]) = [[d,f],[e,g]] ) )

( I is one-to-one & I is onto & ( for d, e, f, g being set st d in D & e in E & f in F & g in G holds

I . ([d,e],[f,g]) = [[d,f],[e,g]] ) )

proof end;

theorem Th2: :: PRVECT_3:2

for X being non empty set

for D being Function st dom D = {1} & D . 1 = X holds

ex I being Function of X,(product D) st

( I is one-to-one & I is onto & ( for x being object st x in X holds

I . x = <*x*> ) )

for D being Function st dom D = {1} & D . 1 = X holds

ex I being Function of X,(product D) st

( I is one-to-one & I is onto & ( for x being object st x in X holds

I . x = <*x*> ) )

proof end;

theorem Th3: :: PRVECT_3:3

for X, Y being non empty set

for D being Function st dom D = {1,2} & D . 1 = X & D . 2 = Y holds

ex I being Function of [:X,Y:],(product D) st

( I is one-to-one & I is onto & ( for x, y being object st x in X & y in Y holds

I . (x,y) = <*x,y*> ) )

for D being Function st dom D = {1,2} & D . 1 = X & D . 2 = Y holds

ex I being Function of [:X,Y:],(product D) st

( I is one-to-one & I is onto & ( for x, y being object st x in X & y in Y holds

I . (x,y) = <*x,y*> ) )

proof end;

theorem Th4: :: PRVECT_3:4

for X being non empty set ex I being Function of X,(product <*X*>) st

( I is one-to-one & I is onto & ( for x being object st x in X holds

I . x = <*x*> ) )

( I is one-to-one & I is onto & ( for x being object st x in X holds

I . x = <*x*> ) )

proof end;

registration
end;

theorem Th5: :: PRVECT_3:5

for X, Y being non empty set ex I being Function of [:X,Y:],(product <*X,Y*>) st

( I is one-to-one & I is onto & ( for x, y being object st x in X & y in Y holds

I . (x,y) = <*x,y*> ) )

( I is one-to-one & I is onto & ( for x, y being object st x in X & y in Y holds

I . (x,y) = <*x,y*> ) )

proof end;

theorem Th6: :: PRVECT_3:6

for X, Y being non-empty non empty FinSequence ex I being Function of [:(product X),(product Y):],(product (X ^ Y)) st

( I is one-to-one & I is onto & ( for x, y being FinSequence st x in product X & y in product Y holds

I . (x,y) = x ^ y ) )

( I is one-to-one & I is onto & ( for x, y being FinSequence st x in product X & y in product Y holds

I . (x,y) = x ^ y ) )

proof end;

Lm1: for G, F being non empty 1-sorted

for x being set st x in [: the carrier of G, the carrier of F:] holds

ex x1 being Point of G ex x2 being Point of F st x = [x1,x2]

by SUBSET_1:43;

definition

let G, F be non empty addLoopStr ;

ex b_{1} being BinOp of [: the carrier of G, the carrier of F:] st

for g1, g2 being Point of G

for f1, f2 being Point of F holds b_{1} . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)]

for b_{1}, b_{2} being BinOp of [: the carrier of G, the carrier of F:] st ( for g1, g2 being Point of G

for f1, f2 being Point of F holds b_{1} . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] ) & ( for g1, g2 being Point of G

for f1, f2 being Point of F holds b_{2} . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] ) holds

b_{1} = b_{2}

end;
func prod_ADD (G,F) -> BinOp of [: the carrier of G, the carrier of F:] means :Def1: :: PRVECT_3:def 1

for g1, g2 being Point of G

for f1, f2 being Point of F holds it . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)];

existence for g1, g2 being Point of G

for f1, f2 being Point of F holds it . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)];

ex b

for g1, g2 being Point of G

for f1, f2 being Point of F holds b

proof end;

uniqueness for b

for f1, f2 being Point of F holds b

for f1, f2 being Point of F holds b

b

proof end;

:: deftheorem Def1 defines prod_ADD PRVECT_3:def 1 :

for G, F being non empty addLoopStr

for b_{3} being BinOp of [: the carrier of G, the carrier of F:] holds

( b_{3} = prod_ADD (G,F) iff for g1, g2 being Point of G

for f1, f2 being Point of F holds b_{3} . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] );

for G, F being non empty addLoopStr

for b

( b

for f1, f2 being Point of F holds b

definition

let G, F be non empty RLSStruct ;

ex b_{1} being Function of [:REAL,[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:] st

for r being Real

for g being Point of G

for f being Point of F holds b_{1} . (r,[g,f]) = [(r * g),(r * f)]

for b_{1}, b_{2} being Function of [:REAL,[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:] st ( for r being Real

for g being Point of G

for f being Point of F holds b_{1} . (r,[g,f]) = [(r * g),(r * f)] ) & ( for r being Real

for g being Point of G

for f being Point of F holds b_{2} . (r,[g,f]) = [(r * g),(r * f)] ) holds

b_{1} = b_{2}

end;
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 :Def2: :: PRVECT_3:def 2

for r being Real

for g being Point of G

for f being Point of F holds it . (r,[g,f]) = [(r * g),(r * f)];

existence for r being Real

for g being Point of G

for f being Point of F holds it . (r,[g,f]) = [(r * g),(r * f)];

ex b

for r being Real

for g being Point of G

for f being Point of F holds b

proof end;

uniqueness for b

for g being Point of G

for f being Point of F holds b

for g being Point of G

for f being Point of F holds b

b

proof end;

:: deftheorem Def2 defines prod_MLT PRVECT_3:def 2 :

for G, F being non empty RLSStruct

for b_{3} being Function of [:REAL,[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:] holds

( b_{3} = prod_MLT (G,F) iff for r being Real

for g being Point of G

for f being Point of F holds b_{3} . (r,[g,f]) = [(r * g),(r * f)] );

for G, F being non empty RLSStruct

for b

( b

for g being Point of G

for f being Point of F holds b

definition

let G, F be non empty addLoopStr ;

coherence

[(0. G),(0. F)] is Element of [: the carrier of G, the carrier of F:];

;

end;
func prod_ZERO (G,F) -> Element of [: the carrier of G, the carrier of F:] equals :: PRVECT_3:def 3

[(0. G),(0. F)];

correctness [(0. G),(0. F)];

coherence

[(0. G),(0. F)] is Element of [: the carrier of G, the carrier of F:];

;

:: deftheorem defines prod_ZERO PRVECT_3:def 3 :

for G, F being non empty addLoopStr holds prod_ZERO (G,F) = [(0. G),(0. F)];

for G, F being non empty addLoopStr holds prod_ZERO (G,F) = [(0. G),(0. F)];

definition

let G, F be non empty addLoopStr ;

coherence

addLoopStr(# [: the carrier of G, the carrier of F:],(prod_ADD (G,F)),(prod_ZERO (G,F)) #) is non empty strict addLoopStr ;

;

end;
func [:G,F:] -> non empty strict addLoopStr equals :: PRVECT_3:def 4

addLoopStr(# [: the carrier of G, the carrier of F:],(prod_ADD (G,F)),(prod_ZERO (G,F)) #);

correctness addLoopStr(# [: the carrier of G, the carrier of F:],(prod_ADD (G,F)),(prod_ZERO (G,F)) #);

coherence

addLoopStr(# [: the carrier of G, the carrier of F:],(prod_ADD (G,F)),(prod_ZERO (G,F)) #) is non empty strict addLoopStr ;

;

:: deftheorem defines [: PRVECT_3:def 4 :

for G, F being non empty addLoopStr holds [:G,F:] = addLoopStr(# [: the carrier of G, the carrier of F:],(prod_ADD (G,F)),(prod_ZERO (G,F)) #);

for G, F being non empty addLoopStr holds [:G,F:] = addLoopStr(# [: the carrier of G, the carrier of F:],(prod_ADD (G,F)),(prod_ZERO (G,F)) #);

definition

let G, F be non empty addLoopStr ;

let g be Element of G;

let f be Element of F;

:: original: [

redefine func [g,f] -> Element of [:G,F:];

coherence

[g,f] is Element of [:G,F:]

end;
let g be Element of G;

let f be Element of F;

:: original: [

redefine func [g,f] -> Element of [:G,F:];

coherence

[g,f] is Element of [:G,F:]

proof end;

registration
end;

registration

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

correctness

coherence

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

end;
correctness

coherence

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

proof end;

registration

let G, F be non empty right_zeroed addLoopStr ;

correctness

coherence

[:G,F:] is right_zeroed ;

end;
correctness

coherence

[:G,F:] is right_zeroed ;

proof end;

registration

let G, F be non empty right_complementable addLoopStr ;

correctness

coherence

[:G,F:] is right_complementable ;

end;
correctness

coherence

[:G,F:] is right_complementable ;

proof end;

theorem :: PRVECT_3:7

for G, F being non empty addLoopStr holds

( ( for x being set holds

( x is Point of [:G,F:] iff ex x1 being Point of G ex x2 being Point of F st x = [x1,x2] ) ) & ( for x, y being Point of [:G,F:]

for x1, y1 being Point of G

for x2, y2 being Point of F st x = [x1,x2] & y = [y1,y2] holds

x + y = [(x1 + y1),(x2 + y2)] ) & 0. [:G,F:] = [(0. G),(0. F)] ) by Lm1, Def1;

( ( for x being set holds

( x is Point of [:G,F:] iff ex x1 being Point of G ex x2 being Point of F st x = [x1,x2] ) ) & ( for x, y being Point of [:G,F:]

for x1, y1 being Point of G

for x2, y2 being Point of F st x = [x1,x2] & y = [y1,y2] holds

x + y = [(x1 + y1),(x2 + y2)] ) & 0. [:G,F:] = [(0. G),(0. F)] ) by Lm1, Def1;

theorem :: PRVECT_3:8

for G, F being non empty right_complementable add-associative right_zeroed addLoopStr

for x being Point of [:G,F:]

for x1 being Point of G

for x2 being Point of F st x = [x1,x2] holds

- x = [(- x1),(- x2)]

for x being Point of [:G,F:]

for x1 being Point of G

for x2 being Point of F st x = [x1,x2] holds

- x = [(- x1),(- x2)]

proof end;

registration

let G, F be non empty strict right_complementable Abelian add-associative right_zeroed addLoopStr ;

correctness

coherence

( [:G,F:] is strict & [:G,F:] is Abelian & [:G,F:] is add-associative & [:G,F:] is right_zeroed & [:G,F:] is right_complementable );

;

end;
correctness

coherence

( [:G,F:] is strict & [:G,F:] is Abelian & [:G,F:] is add-associative & [:G,F:] is right_zeroed & [:G,F:] is right_complementable );

;

definition

let G, F be non empty RLSStruct ;

coherence

RLSStruct(# [: the carrier of G, the carrier of F:],(prod_ZERO (G,F)),(prod_ADD (G,F)),(prod_MLT (G,F)) #) is non empty strict RLSStruct ;

;

end;
func [:G,F:] -> non empty strict 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)) #);

correctness RLSStruct(# [: the carrier of G, the carrier of F:],(prod_ZERO (G,F)),(prod_ADD (G,F)),(prod_MLT (G,F)) #);

coherence

RLSStruct(# [: the carrier of G, the carrier of F:],(prod_ZERO (G,F)),(prod_ADD (G,F)),(prod_MLT (G,F)) #) is non empty strict RLSStruct ;

;

:: deftheorem defines [: PRVECT_3:def 5 :

for G, F being non empty RLSStruct holds [:G,F:] = RLSStruct(# [: the carrier of G, the carrier of F:],(prod_ZERO (G,F)),(prod_ADD (G,F)),(prod_MLT (G,F)) #);

for G, F being non empty RLSStruct holds [:G,F:] = RLSStruct(# [: the carrier of G, the carrier of F:],(prod_ZERO (G,F)),(prod_ADD (G,F)),(prod_MLT (G,F)) #);

definition

let G, F be non empty RLSStruct ;

let g be Element of G;

let f be Element of F;

:: original: [

redefine func [g,f] -> Element of [:G,F:];

coherence

[g,f] is Element of [:G,F:]

end;
let g be Element of G;

let f be Element of F;

:: original: [

redefine func [g,f] -> Element of [:G,F:];

coherence

[g,f] is Element of [:G,F:]

proof end;

registration
end;

registration

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

correctness

coherence

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

end;
correctness

coherence

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

proof end;

registration

let G, F be non empty right_zeroed RLSStruct ;

correctness

coherence

[:G,F:] is right_zeroed ;

end;
correctness

coherence

[:G,F:] is right_zeroed ;

proof end;

registration

let G, F be non empty right_complementable RLSStruct ;

correctness

coherence

[:G,F:] is right_complementable ;

end;
correctness

coherence

[:G,F:] is right_complementable ;

proof end;

theorem Th9: :: PRVECT_3:9

for G, F being non empty RLSStruct holds

( ( for x being set holds

( x is Point of [:G,F:] iff ex x1 being Point of G ex x2 being Point of F st x = [x1,x2] ) ) & ( for x, y being Point of [:G,F:]

for x1, y1 being Point of G

for x2, y2 being 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 being Point of [:G,F:]

for x1 being Point of G

for x2 being Point of F

for a being Real st x = [x1,x2] holds

a * x = [(a * x1),(a * x2)] ) ) by Def2, Def1, Lm1;

( ( for x being set holds

( x is Point of [:G,F:] iff ex x1 being Point of G ex x2 being Point of F st x = [x1,x2] ) ) & ( for x, y being Point of [:G,F:]

for x1, y1 being Point of G

for x2, y2 being 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 being Point of [:G,F:]

for x1 being Point of G

for x2 being Point of F

for a being Real st x = [x1,x2] holds

a * x = [(a * x1),(a * x2)] ) ) by Def2, Def1, Lm1;

theorem :: PRVECT_3:10

for G, F being non empty right_complementable add-associative right_zeroed RLSStruct

for x being Point of [:G,F:]

for x1 being Point of G

for x2 being Point of F st x = [x1,x2] holds

- x = [(- x1),(- x2)]

for x being Point of [:G,F:]

for x1 being Point of G

for x2 being Point of F st x = [x1,x2] holds

- x = [(- x1),(- x2)]

proof end;

registration

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

correctness

coherence

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

end;
correctness

coherence

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

proof end;

registration

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

correctness

coherence

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

end;
correctness

coherence

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

proof end;

registration

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

correctness

coherence

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

end;
correctness

coherence

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

proof end;

registration

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

correctness

coherence

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

end;
correctness

coherence

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

proof end;

registration

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

correctness

coherence

<*G*> is RealLinearSpace-yielding ;

end;
correctness

coherence

<*G*> is RealLinearSpace-yielding ;

proof end;

registration

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

correctness

coherence

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

end;
correctness

coherence

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

proof end;

theorem Th11: :: PRVECT_3:11

for X being RealLinearSpace ex I being Function of X,(product <*X*>) st

( I is one-to-one & I is onto & ( for x being Point of X holds I . x = <*x*> ) & ( for v, w being Point of X holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of X

for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. X) = 0. (product <*X*>) )

( I is one-to-one & I is onto & ( for x being Point of X holds I . x = <*x*> ) & ( for v, w being Point of X holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of X

for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. X) = 0. (product <*X*>) )

proof end;

registration

let G, F be non empty RealLinearSpace-yielding FinSequence;

correctness

coherence

G ^ F is RealLinearSpace-yielding ;

end;
correctness

coherence

G ^ F is RealLinearSpace-yielding ;

proof end;

theorem Th12: :: PRVECT_3:12

for X, Y being RealLinearSpace ex I being Function of [:X,Y:],(product <*X,Y*>) st

( I is one-to-one & I is onto & ( for x being Point of X

for y being Point of Y holds I . (x,y) = <*x,y*> ) & ( for v, w being Point of [:X,Y:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:X,Y:]

for r being Real holds I . (r * v) = r * (I . v) ) & I . (0. [:X,Y:]) = 0. (product <*X,Y*>) )

( I is one-to-one & I is onto & ( for x being Point of X

for y being Point of Y holds I . (x,y) = <*x,y*> ) & ( for v, w being Point of [:X,Y:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:X,Y:]

for r being Real holds I . (r * v) = r * (I . v) ) & I . (0. [:X,Y:]) = 0. (product <*X,Y*>) )

proof end;

Lm2: for X being non-empty non empty FinSequence

for x being set st x in product X holds

x is FinSequence

proof end;

theorem Th13: :: PRVECT_3:13

for X, Y being RealLinearSpace-Sequence ex I being Function of [:(product X),(product Y):],(product (X ^ Y)) st

( I is one-to-one & I is onto & ( for x being Point of (product X)

for y being Point of (product Y) ex x1, y1 being FinSequence st

( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),(product Y):] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:(product X),(product Y):]

for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. [:(product X),(product Y):]) = 0. (product (X ^ Y)) )

( I is one-to-one & I is onto & ( for x being Point of (product X)

for y being Point of (product Y) ex x1, y1 being FinSequence st

( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),(product Y):] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:(product X),(product Y):]

for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. [:(product X),(product Y):]) = 0. (product (X ^ Y)) )

proof end;

theorem :: PRVECT_3:14

for G, F being RealLinearSpace holds

( ( for x being set holds

( x is Point of (product <*G,F*>) iff ex x1 being Point of G ex x2 being Point of F st x = <*x1,x2*> ) ) & ( for x, y being Point of (product <*G,F*>)

for x1, y1 being Point of G

for x2, y2 being 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 being Point of (product <*G,F*>)

for x1 being Point of G

for x2 being Point of F st x = <*x1,x2*> holds

- x = <*(- x1),(- x2)*> ) & ( for x being Point of (product <*G,F*>)

for x1 being Point of G

for x2 being Point of F

for a being Real st x = <*x1,x2*> holds

a * x = <*(a * x1),(a * x2)*> ) )

( ( for x being set holds

( x is Point of (product <*G,F*>) iff ex x1 being Point of G ex x2 being Point of F st x = <*x1,x2*> ) ) & ( for x, y being Point of (product <*G,F*>)

for x1, y1 being Point of G

for x2, y2 being 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 being Point of (product <*G,F*>)

for x1 being Point of G

for x2 being Point of F st x = <*x1,x2*> holds

- x = <*(- x1),(- x2)*> ) & ( for x being Point of (product <*G,F*>)

for x1 being Point of G

for x2 being Point of F

for a being Real st x = <*x1,x2*> holds

a * x = <*(a * x1),(a * x2)*> ) )

proof end;

definition

let G, F be non empty NORMSTR ;

ex b_{1} being Function of [: the carrier of G, the carrier of F:],REAL st

for g being Point of G

for f being Point of F ex v being Element of REAL 2 st

( v = <*||.g.||,||.f.||*> & b_{1} . (g,f) = |.v.| )

for b_{1}, b_{2} being Function of [: the carrier of G, the carrier of F:],REAL st ( for g being Point of G

for f being Point of F ex v being Element of REAL 2 st

( v = <*||.g.||,||.f.||*> & b_{1} . (g,f) = |.v.| ) ) & ( for g being Point of G

for f being Point of F ex v being Element of REAL 2 st

( v = <*||.g.||,||.f.||*> & b_{2} . (g,f) = |.v.| ) ) holds

b_{1} = b_{2}

end;
func prod_NORM (G,F) -> Function of [: the carrier of G, the carrier of F:],REAL means :Def6: :: PRVECT_3:def 6

for g being Point of G

for f being Point of F ex v being Element of REAL 2 st

( v = <*||.g.||,||.f.||*> & it . (g,f) = |.v.| );

existence for g being Point of G

for f being Point of F ex v being Element of REAL 2 st

( v = <*||.g.||,||.f.||*> & it . (g,f) = |.v.| );

ex b

for g being Point of G

for f being Point of F ex v being Element of REAL 2 st

( v = <*||.g.||,||.f.||*> & b

proof end;

uniqueness for b

for f being Point of F ex v being Element of REAL 2 st

( v = <*||.g.||,||.f.||*> & b

for f being Point of F ex v being Element of REAL 2 st

( v = <*||.g.||,||.f.||*> & b

b

proof end;

:: deftheorem Def6 defines prod_NORM PRVECT_3:def 6 :

for G, F being non empty NORMSTR

for b_{3} being Function of [: the carrier of G, the carrier of F:],REAL holds

( b_{3} = prod_NORM (G,F) iff for g being Point of G

for f being Point of F ex v being Element of REAL 2 st

( v = <*||.g.||,||.f.||*> & b_{3} . (g,f) = |.v.| ) );

for G, F being non empty NORMSTR

for b

( b

for f being Point of F ex v being Element of REAL 2 st

( v = <*||.g.||,||.f.||*> & b

definition

let G, F be non empty NORMSTR ;

coherence

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)) #) is non empty strict NORMSTR ;

;

end;
func [:G,F:] -> non empty strict 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)) #);

correctness 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)) #);

coherence

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)) #) is non empty strict NORMSTR ;

;

:: deftheorem defines [: PRVECT_3:def 7 :

for G, F being non empty NORMSTR holds [:G,F:] = 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)) #);

for G, F being non empty NORMSTR holds [:G,F:] = 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)) #);

definition

let G, F be non empty NORMSTR ;

let g be Element of G;

let f be Element of F;

:: original: [

redefine func [g,f] -> Element of [:G,F:];

coherence

[g,f] is Element of [:G,F:]

end;
let g be Element of G;

let f be Element of F;

:: original: [

redefine func [g,f] -> Element of [:G,F:];

coherence

[g,f] is Element of [:G,F:]

proof end;

registration

let G, F be RealNormSpace;

correctness

coherence

( [:G,F:] is reflexive & [:G,F:] is discerning & [:G,F:] is RealNormSpace-like );

end;
correctness

coherence

( [:G,F:] is reflexive & [:G,F:] is discerning & [:G,F:] is RealNormSpace-like );

proof end;

registration

let G, F be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR ;

coherence

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

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

correctness coherence

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

proof end;

registration

let G be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR ;

correctness

coherence

<*G*> is RealNormSpace-yielding ;

end;
correctness

coherence

<*G*> is RealNormSpace-yielding ;

proof end;

registration

let G, F be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR ;

correctness

coherence

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

end;
correctness

coherence

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

proof end;

theorem Th15: :: PRVECT_3:15

for X, Y being RealNormSpace ex I being Function of [:X,Y:],(product <*X,Y*>) st

( I is one-to-one & I is onto & ( for x being Point of X

for y being Point of Y holds I . (x,y) = <*x,y*> ) & ( for v, w being Point of [:X,Y:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:X,Y:]

for r being Real holds I . (r * v) = r * (I . v) ) & 0. (product <*X,Y*>) = I . (0. [:X,Y:]) & ( for v being Point of [:X,Y:] holds ||.(I . v).|| = ||.v.|| ) )

( I is one-to-one & I is onto & ( for x being Point of X

for y being Point of Y holds I . (x,y) = <*x,y*> ) & ( for v, w being Point of [:X,Y:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:X,Y:]

for r being Real holds I . (r * v) = r * (I . v) ) & 0. (product <*X,Y*>) = I . (0. [:X,Y:]) & ( for v being Point of [:X,Y:] holds ||.(I . v).|| = ||.v.|| ) )

proof end;

theorem Th16: :: PRVECT_3:16

for X being RealNormSpace ex I being Function of X,(product <*X*>) st

( I is one-to-one & I is onto & ( for x being Point of X holds I . x = <*x*> ) & ( for v, w being Point of X holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of X

for r being Element of REAL holds I . (r * v) = r * (I . v) ) & 0. (product <*X*>) = I . (0. X) & ( for v being Point of X holds ||.(I . v).|| = ||.v.|| ) )

( I is one-to-one & I is onto & ( for x being Point of X holds I . x = <*x*> ) & ( for v, w being Point of X holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of X

for r being Element of REAL holds I . (r * v) = r * (I . v) ) & 0. (product <*X*>) = I . (0. X) & ( for v being Point of X holds ||.(I . v).|| = ||.v.|| ) )

proof end;

registration

let G, F be non empty RealNormSpace-yielding FinSequence;

correctness

coherence

( not G ^ F is empty & G ^ F is RealNormSpace-yielding );

end;
correctness

coherence

( not G ^ F is empty & G ^ F is RealNormSpace-yielding );

proof end;

Lm3: for F1, F2 being FinSequence of REAL holds sqr (F1 ^ F2) = (sqr F1) ^ (sqr F2)

by RVSUM_1:144;

theorem Th17: :: PRVECT_3:17

for X, Y being RealNormSpace-Sequence ex I being Function of [:(product X),(product Y):],(product (X ^ Y)) st

( I is one-to-one & I is onto & ( for x being Point of (product X)

for y being Point of (product Y) ex x1, y1 being FinSequence st

( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),(product Y):] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:(product X),(product Y):]

for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. [:(product X),(product Y):]) = 0. (product (X ^ Y)) & ( for v being Point of [:(product X),(product Y):] holds ||.(I . v).|| = ||.v.|| ) )

( I is one-to-one & I is onto & ( for x being Point of (product X)

for y being Point of (product Y) ex x1, y1 being FinSequence st

( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),(product Y):] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:(product X),(product Y):]

for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. [:(product X),(product Y):]) = 0. (product (X ^ Y)) & ( for v being Point of [:(product X),(product Y):] holds ||.(I . v).|| = ||.v.|| ) )

proof end;

theorem Th18: :: PRVECT_3:18

for G, F being RealNormSpace holds

( ( for x being set holds

( x is Point of [:G,F:] iff ex x1 being Point of G ex x2 being Point of F st x = [x1,x2] ) ) & ( for x, y being Point of [:G,F:]

for x1, y1 being Point of G

for x2, y2 being 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 being Point of [:G,F:]

for x1 being Point of G

for x2 being Point of F st x = [x1,x2] holds

- x = [(- x1),(- x2)] ) & ( for x being Point of [:G,F:]

for x1 being Point of G

for x2 being Point of F

for a being Real st x = [x1,x2] holds

a * x = [(a * x1),(a * x2)] ) & ( for x being Point of [:G,F:]

for x1 being Point of G

for x2 being Point of F st x = [x1,x2] holds

ex w being Element of REAL 2 st

( w = <*||.x1.||,||.x2.||*> & ||.x.|| = |.w.| ) ) )

( ( for x being set holds

( x is Point of [:G,F:] iff ex x1 being Point of G ex x2 being Point of F st x = [x1,x2] ) ) & ( for x, y being Point of [:G,F:]

for x1, y1 being Point of G

for x2, y2 being 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 being Point of [:G,F:]

for x1 being Point of G

for x2 being Point of F st x = [x1,x2] holds

- x = [(- x1),(- x2)] ) & ( for x being Point of [:G,F:]

for x1 being Point of G

for x2 being Point of F

for a being Real st x = [x1,x2] holds

a * x = [(a * x1),(a * x2)] ) & ( for x being Point of [:G,F:]

for x1 being Point of G

for x2 being Point of F st x = [x1,x2] holds

ex w being Element of REAL 2 st

( w = <*||.x1.||,||.x2.||*> & ||.x.|| = |.w.| ) ) )

proof end;

theorem Th19: :: PRVECT_3:19

for G, F being RealNormSpace holds

( ( for x being set holds

( x is Point of (product <*G,F*>) iff ex x1 being Point of G ex x2 being Point of F st x = <*x1,x2*> ) ) & ( for x, y being Point of (product <*G,F*>)

for x1, y1 being Point of G

for x2, y2 being 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 being Point of (product <*G,F*>)

for x1 being Point of G

for x2 being Point of F st x = <*x1,x2*> holds

- x = <*(- x1),(- x2)*> ) & ( for x being Point of (product <*G,F*>)

for x1 being Point of G

for x2 being Point of F

for a being Real st x = <*x1,x2*> holds

a * x = <*(a * x1),(a * x2)*> ) & ( for x being Point of (product <*G,F*>)

for x1 being Point of G

for x2 being Point of F st x = <*x1,x2*> holds

ex w being Element of REAL 2 st

( w = <*||.x1.||,||.x2.||*> & ||.x.|| = |.w.| ) ) )

( ( for x being set holds

( x is Point of (product <*G,F*>) iff ex x1 being Point of G ex x2 being Point of F st x = <*x1,x2*> ) ) & ( for x, y being Point of (product <*G,F*>)

for x1, y1 being Point of G

for x2, y2 being 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 being Point of (product <*G,F*>)

for x1 being Point of G

for x2 being Point of F st x = <*x1,x2*> holds

- x = <*(- x1),(- x2)*> ) & ( for x being Point of (product <*G,F*>)

for x1 being Point of G

for x2 being Point of F

for a being Real st x = <*x1,x2*> holds

a * x = <*(a * x1),(a * x2)*> ) & ( for x being Point of (product <*G,F*>)

for x1 being Point of G

for x2 being Point of F st x = <*x1,x2*> holds

ex w being Element of REAL 2 st

( w = <*||.x1.||,||.x2.||*> & ||.x.|| = |.w.| ) ) )

proof end;

theorem :: PRVECT_3:20

for X, Y being RealNormSpace-Sequence ex I being Function of (product <*(product X),(product Y)*>),(product (X ^ Y)) st

( I is one-to-one & I is onto & ( for x being Point of (product X)

for y being Point of (product Y) ex x1, y1 being FinSequence st

( x = x1 & y = y1 & I . <*x,y*> = x1 ^ y1 ) ) & ( for v, w being Point of (product <*(product X),(product Y)*>) holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of (product <*(product X),(product Y)*>)

for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. (product <*(product X),(product Y)*>)) = 0. (product (X ^ Y)) & ( for v being Point of (product <*(product X),(product Y)*>) holds ||.(I . v).|| = ||.v.|| ) )

( I is one-to-one & I is onto & ( for x being Point of (product X)

for y being Point of (product Y) ex x1, y1 being FinSequence st

( x = x1 & y = y1 & I . <*x,y*> = x1 ^ y1 ) ) & ( for v, w being Point of (product <*(product X),(product Y)*>) holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of (product <*(product X),(product Y)*>)

for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. (product <*(product X),(product Y)*>)) = 0. (product (X ^ Y)) & ( for v being Point of (product <*(product X),(product Y)*>) holds ||.(I . v).|| = ||.v.|| ) )

proof end;

theorem Th21: :: PRVECT_3:21

for X, Y being RealLinearSpace ex I being Function of [:X,Y:],[:X,(product <*Y*>):] st

( I is one-to-one & I is onto & ( for x being Point of X

for y being Point of Y holds I . (x,y) = [x,<*y*>] ) & ( for v, w being Point of [:X,Y:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:X,Y:]

for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. [:X,Y:]) = 0. [:X,(product <*Y*>):] )

( I is one-to-one & I is onto & ( for x being Point of X

for y being Point of Y holds I . (x,y) = [x,<*y*>] ) & ( for v, w being Point of [:X,Y:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:X,Y:]

for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. [:X,Y:]) = 0. [:X,(product <*Y*>):] )

proof end;

theorem :: PRVECT_3:22

for X being RealLinearSpace-Sequence

for Y being RealLinearSpace ex I being Function of [:(product X),Y:],(product (X ^ <*Y*>)) st

( I is one-to-one & I is onto & ( for x being Point of (product X)

for y being Point of Y ex x1, y1 being FinSequence st

( x = x1 & <*y*> = y1 & I . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),Y:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:(product X),Y:]

for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) )

for Y being RealLinearSpace ex I being Function of [:(product X),Y:],(product (X ^ <*Y*>)) st

( I is one-to-one & I is onto & ( for x being Point of (product X)

for y being Point of Y ex x1, y1 being FinSequence st

( x = x1 & <*y*> = y1 & I . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),Y:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:(product X),Y:]

for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) )

proof end;

theorem Th23: :: PRVECT_3:23

for X, Y being RealNormSpace ex I being Function of [:X,Y:],[:X,(product <*Y*>):] st

( I is one-to-one & I is onto & ( for x being Point of X

for y being Point of Y holds I . (x,y) = [x,<*y*>] ) & ( for v, w being Point of [:X,Y:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:X,Y:]

for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. [:X,Y:]) = 0. [:X,(product <*Y*>):] & ( for v being Point of [:X,Y:] holds ||.(I . v).|| = ||.v.|| ) )

( I is one-to-one & I is onto & ( for x being Point of X

for y being Point of Y holds I . (x,y) = [x,<*y*>] ) & ( for v, w being Point of [:X,Y:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:X,Y:]

for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. [:X,Y:]) = 0. [:X,(product <*Y*>):] & ( for v being Point of [:X,Y:] holds ||.(I . v).|| = ||.v.|| ) )

proof end;

theorem :: PRVECT_3:24

for X being RealNormSpace-Sequence

for Y being RealNormSpace ex I being Function of [:(product X),Y:],(product (X ^ <*Y*>)) st

( I is one-to-one & I is onto & ( for x being Point of (product X)

for y being Point of Y ex x1, y1 being FinSequence st

( x = x1 & <*y*> = y1 & I . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),Y:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:(product X),Y:]

for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) & ( for v being Point of [:(product X),Y:] holds ||.(I . v).|| = ||.v.|| ) )

for Y being RealNormSpace ex I being Function of [:(product X),Y:],(product (X ^ <*Y*>)) st

( I is one-to-one & I is onto & ( for x being Point of (product X)

for y being Point of Y ex x1, y1 being FinSequence st

( x = x1 & <*y*> = y1 & I . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),Y:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:(product X),Y:]

for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) & ( for v being Point of [:(product X),Y:] holds ||.(I . v).|| = ||.v.|| ) )

proof end;