:: PRVECT_3 semantic presentation
begin
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]] ) )
proof
let D, E, F, G be non empty set ; ::_thesis: 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]] ) )
defpred S1[ set , set , set ] means ex d, e, f, g being set st
( d in D & e in E & f in F & g in G & $1 = [d,e] & $2 = [f,g] & $3 = [[d,f],[e,g]] );
A1: for x, y being set st x in [:D,E:] & y in [:F,G:] holds
ex z being set st
( z in [:[:D,F:],[:E,G:]:] & S1[x,y,z] )
proof
let x, y be set ; ::_thesis: ( x in [:D,E:] & y in [:F,G:] implies ex z being set st
( z in [:[:D,F:],[:E,G:]:] & S1[x,y,z] ) )
assume A2: ( x in [:D,E:] & y in [:F,G:] ) ; ::_thesis: ex z being set st
( z in [:[:D,F:],[:E,G:]:] & S1[x,y,z] )
consider d, e being set such that
A3: ( d in D & e in E & x = [d,e] ) by A2, ZFMISC_1:def_2;
consider f, g being set such that
A4: ( f in F & g in G & y = [f,g] ) by A2, ZFMISC_1:def_2;
( [d,f] in [:D,F:] & [e,g] in [:E,G:] ) by A3, A4, ZFMISC_1:87;
then [[d,f],[e,g]] in [:[:D,F:],[:E,G:]:] by ZFMISC_1:87;
hence ex z being set st
( z in [:[:D,F:],[:E,G:]:] & S1[x,y,z] ) by A3, A4; ::_thesis: verum
end;
consider I being Function of [:[:D,E:],[:F,G:]:],[:[:D,F:],[:E,G:]:] such that
A5: for x, y being set st x in [:D,E:] & y in [:F,G:] holds
S1[x,y,I . (x,y)] from BINOP_1:sch_1(A1);
A6: 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
let d, e, f, g be set ; ::_thesis: ( d in D & e in E & f in F & g in G implies I . ([d,e],[f,g]) = [[d,f],[e,g]] )
assume A7: ( d in D & e in E & f in F & g in G ) ; ::_thesis: I . ([d,e],[f,g]) = [[d,f],[e,g]]
A8: ( [d,e] in [:D,E:] & [f,g] in [:F,G:] ) by A7, ZFMISC_1:87;
consider d1, e1, f1, g1 being set such that
A9: ( d1 in D & e1 in E & f1 in F & g1 in G & [d,e] = [d1,e1] & [f,g] = [f1,g1] & I . ([d,e],[f,g]) = [[d1,f1],[e1,g1]] ) by A8, A5;
( d1 = d & e1 = e & f1 = f & g1 = g ) by A9, XTUPLE_0:1;
hence I . ([d,e],[f,g]) = [[d,f],[e,g]] by A9; ::_thesis: verum
end;
A10: I is one-to-one
proof
now__::_thesis:_for_z1,_z2_being_set_st_z1_in_[:[:D,E:],[:F,G:]:]_&_z2_in_[:[:D,E:],[:F,G:]:]_&_I_._z1_=_I_._z2_holds_
z1_=_z2
let z1, z2 be set ; ::_thesis: ( z1 in [:[:D,E:],[:F,G:]:] & z2 in [:[:D,E:],[:F,G:]:] & I . z1 = I . z2 implies z1 = z2 )
assume A11: ( z1 in [:[:D,E:],[:F,G:]:] & z2 in [:[:D,E:],[:F,G:]:] & I . z1 = I . z2 ) ; ::_thesis: z1 = z2
consider de1, fg1 being set such that
A12: ( de1 in [:D,E:] & fg1 in [:F,G:] & z1 = [de1,fg1] ) by A11, ZFMISC_1:def_2;
consider d1, e1 being set such that
A13: ( d1 in D & e1 in E & de1 = [d1,e1] ) by A12, ZFMISC_1:def_2;
consider f1, g1 being set such that
A14: ( f1 in F & g1 in G & fg1 = [f1,g1] ) by A12, ZFMISC_1:def_2;
consider de2, fg2 being set such that
A15: ( de2 in [:D,E:] & fg2 in [:F,G:] & z2 = [de2,fg2] ) by A11, ZFMISC_1:def_2;
consider d2, e2 being set such that
A16: ( d2 in D & e2 in E & de2 = [d2,e2] ) by A15, ZFMISC_1:def_2;
consider f2, g2 being set such that
A17: ( f2 in F & g2 in G & fg2 = [f2,g2] ) by A15, ZFMISC_1:def_2;
[[d1,f1],[e1,g1]] = I . ([d1,e1],[f1,g1]) by A6, A13, A14
.= I . ([d2,e2],[f2,g2]) by A11, A12, A13, A14, A15, A16, A17
.= [[d2,f2],[e2,g2]] by A6, A16, A17 ;
then ( [d1,f1] = [d2,f2] & [e1,g1] = [e2,g2] ) by XTUPLE_0:1;
then ( d1 = d2 & f1 = f2 & e1 = e2 & g1 = g2 ) by XTUPLE_0:1;
hence z1 = z2 by A12, A13, A14, A15, A16, A17; ::_thesis: verum
end;
hence I is one-to-one by FUNCT_2:19; ::_thesis: verum
end;
I is onto
proof
now__::_thesis:_for_w_being_set_st_w_in_[:[:D,F:],[:E,G:]:]_holds_
w_in_rng_I
let w be set ; ::_thesis: ( w in [:[:D,F:],[:E,G:]:] implies w in rng I )
assume A18: w in [:[:D,F:],[:E,G:]:] ; ::_thesis: w in rng I
consider df, eg being set such that
A19: ( df in [:D,F:] & eg in [:E,G:] & w = [df,eg] ) by A18, ZFMISC_1:def_2;
consider d, f being set such that
A20: ( d in D & f in F & df = [d,f] ) by A19, ZFMISC_1:def_2;
consider e, g being set such that
A21: ( e in E & g in G & eg = [e,g] ) by A19, ZFMISC_1:def_2;
A22: ( [d,e] in [:D,E:] & [f,g] in [:F,G:] ) by A20, A21, ZFMISC_1:87;
reconsider z = [[d,e],[f,g]] as Element of [:[:D,E:],[:F,G:]:] by A22, ZFMISC_1:87;
w = I . ([d,e],[f,g]) by A6, A19, A20, A21;
then w = I . z ;
hence w in rng I by FUNCT_2:112; ::_thesis: verum
end;
then [:[:D,F:],[:E,G:]:] c= rng I by TARSKI:def_3;
then [:[:D,F:],[:E,G:]:] = rng I by XBOOLE_0:def_10;
hence I is onto by FUNCT_2:def_3; ::_thesis: verum
end;
hence 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]] ) ) by A6, A10; ::_thesis: verum
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 set st x in X holds
I . x = <*x*> ) )
proof
let X be non empty set ; ::_thesis: 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 set st x in X holds
I . x = <*x*> ) )
let D be Function; ::_thesis: ( dom D = {1} & D . 1 = X implies ex I being Function of X,(product D) st
( I is one-to-one & I is onto & ( for x being set st x in X holds
I . x = <*x*> ) ) )
assume A1: ( dom D = {1} & D . 1 = X ) ; ::_thesis: ex I being Function of X,(product D) st
( I is one-to-one & I is onto & ( for x being set st x in X holds
I . x = <*x*> ) )
defpred S1[ set , set ] means $2 = <*$1*>;
A2: for x being set st x in X holds
ex z being set st
( z in product D & S1[x,z] )
proof
let x be set ; ::_thesis: ( x in X implies ex z being set st
( z in product D & S1[x,z] ) )
assume A3: x in X ; ::_thesis: ex z being set st
( z in product D & S1[x,z] )
A4: dom <*x*> = Seg (len <*x*>) by FINSEQ_1:def_3
.= {1} by FINSEQ_1:2, FINSEQ_1:40 ;
now__::_thesis:_for_i_being_set_st_i_in_dom_<*x*>_holds_
<*x*>_._i_in_D_._i
let i be set ; ::_thesis: ( i in dom <*x*> implies <*x*> . i in D . i )
assume i in dom <*x*> ; ::_thesis: <*x*> . i in D . i
then i = 1 by A4, TARSKI:def_1;
hence <*x*> . i in D . i by A1, A3, FINSEQ_1:40; ::_thesis: verum
end;
then <*x*> in product D by A4, A1, CARD_3:9;
hence ex z being set st
( z in product D & S1[x,z] ) ; ::_thesis: verum
end;
consider I being Function of X,(product D) such that
A5: for x being set st x in X holds
S1[x,I . x] from FUNCT_2:sch_1(A2);
now__::_thesis:_not_{}_in_rng_D
assume {} in rng D ; ::_thesis: contradiction
then ex x being set st
( x in dom D & D . x = {} ) by FUNCT_1:def_3;
hence contradiction by A1, TARSKI:def_1; ::_thesis: verum
end;
then A6: product D <> {} by CARD_3:26;
now__::_thesis:_for_z1,_z2_being_set_st_z1_in_X_&_z2_in_X_&_I_._z1_=_I_._z2_holds_
z1_=_z2
let z1, z2 be set ; ::_thesis: ( z1 in X & z2 in X & I . z1 = I . z2 implies z1 = z2 )
assume A7: ( z1 in X & z2 in X & I . z1 = I . z2 ) ; ::_thesis: z1 = z2
<*z1*> = I . z1 by A5, A7
.= <*z2*> by A5, A7 ;
hence z1 = z2 by FINSEQ_1:76; ::_thesis: verum
end;
then A8: I is one-to-one by A6, FUNCT_2:19;
now__::_thesis:_for_w_being_set_st_w_in_product_D_holds_
w_in_rng_I
let w be set ; ::_thesis: ( w in product D implies w in rng I )
assume w in product D ; ::_thesis: w in rng I
then consider g being Function such that
A9: ( w = g & dom g = dom D & ( for i being set st i in dom D holds
g . i in D . i ) ) by CARD_3:def_5;
reconsider g = g as FinSequence by A1, A9, FINSEQ_1:2, FINSEQ_1:def_2;
set x = g . 1;
A10: len g = 1 by A1, A9, FINSEQ_1:2, FINSEQ_1:def_3;
1 in dom D by A1, TARSKI:def_1;
then A11: ( g . 1 in X & w = <*(g . 1)*> ) by A9, A10, A1, FINSEQ_1:40;
then w = I . (g . 1) by A5;
hence w in rng I by A11, A6, FUNCT_2:112; ::_thesis: verum
end;
then product D c= rng I by TARSKI:def_3;
then product D = rng I by XBOOLE_0:def_10;
then I is onto by FUNCT_2:def_3;
hence ex I being Function of X,(product D) st
( I is one-to-one & I is onto & ( for x being set st x in X holds
I . x = <*x*> ) ) by A5, A8; ::_thesis: verum
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 set st x in X & y in Y holds
I . (x,y) = <*x,y*> ) )
proof
let X, Y be non empty set ; ::_thesis: 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 set st x in X & y in Y holds
I . (x,y) = <*x,y*> ) )
let D be Function; ::_thesis: ( dom D = {1,2} & D . 1 = X & D . 2 = Y implies ex I being Function of [:X,Y:],(product D) st
( I is one-to-one & I is onto & ( for x, y being set st x in X & y in Y holds
I . (x,y) = <*x,y*> ) ) )
assume A1: ( dom D = {1,2} & D . 1 = X & D . 2 = Y ) ; ::_thesis: ex I being Function of [:X,Y:],(product D) st
( I is one-to-one & I is onto & ( for x, y being set st x in X & y in Y holds
I . (x,y) = <*x,y*> ) )
defpred S1[ set , set , set ] means $3 = <*$1,$2*>;
A2: for x, y being set st x in X & y in Y holds
ex z being set st
( z in product D & S1[x,y,z] )
proof
let x, y be set ; ::_thesis: ( x in X & y in Y implies ex z being set st
( z in product D & S1[x,y,z] ) )
assume A3: ( x in X & y in Y ) ; ::_thesis: ex z being set st
( z in product D & S1[x,y,z] )
A4: dom <*x,y*> = Seg (len <*x,y*>) by FINSEQ_1:def_3
.= {1,2} by FINSEQ_1:2, FINSEQ_1:44 ;
now__::_thesis:_for_i_being_set_st_i_in_dom_<*x,y*>_holds_
<*x,y*>_._i_in_D_._i
let i be set ; ::_thesis: ( i in dom <*x,y*> implies <*x,y*> . i in D . i )
assume i in dom <*x,y*> ; ::_thesis: <*x,y*> . i in D . i
then ( i = 1 or i = 2 ) by A4, TARSKI:def_2;
hence <*x,y*> . i in D . i by A1, A3, FINSEQ_1:44; ::_thesis: verum
end;
then <*x,y*> in product D by A4, A1, CARD_3:9;
hence ex z being set st
( z in product D & S1[x,y,z] ) ; ::_thesis: verum
end;
consider I being Function of [:X,Y:],(product D) such that
A5: for x, y being set st x in X & y in Y holds
S1[x,y,I . (x,y)] from BINOP_1:sch_1(A2);
now__::_thesis:_not_{}_in_rng_D
assume {} in rng D ; ::_thesis: contradiction
then ex x being set st
( x in dom D & D . x = {} ) by FUNCT_1:def_3;
hence contradiction by A1, TARSKI:def_2; ::_thesis: verum
end;
then A6: product D <> {} by CARD_3:26;
now__::_thesis:_for_z1,_z2_being_set_st_z1_in_[:X,Y:]_&_z2_in_[:X,Y:]_&_I_._z1_=_I_._z2_holds_
z1_=_z2
let z1, z2 be set ; ::_thesis: ( z1 in [:X,Y:] & z2 in [:X,Y:] & I . z1 = I . z2 implies z1 = z2 )
assume A7: ( z1 in [:X,Y:] & z2 in [:X,Y:] & I . z1 = I . z2 ) ; ::_thesis: z1 = z2
then consider x1, y1 being set such that
A8: ( x1 in X & y1 in Y & z1 = [x1,y1] ) by ZFMISC_1:def_2;
consider x2, y2 being set such that
A9: ( x2 in X & y2 in Y & z2 = [x2,y2] ) by A7, ZFMISC_1:def_2;
<*x1,y1*> = I . (x1,y1) by A5, A8
.= I . (x2,y2) by A7, A8, A9
.= <*x2,y2*> by A5, A9 ;
then ( x1 = x2 & y1 = y2 ) by FINSEQ_1:77;
hence z1 = z2 by A8, A9; ::_thesis: verum
end;
then A10: I is one-to-one by A6, FUNCT_2:19;
now__::_thesis:_for_w_being_set_st_w_in_product_D_holds_
w_in_rng_I
let w be set ; ::_thesis: ( w in product D implies w in rng I )
assume w in product D ; ::_thesis: w in rng I
then consider g being Function such that
A11: ( w = g & dom g = dom D & ( for i being set st i in dom D holds
g . i in D . i ) ) by CARD_3:def_5;
reconsider g = g as FinSequence by A1, A11, FINSEQ_1:2, FINSEQ_1:def_2;
set x = g . 1;
set y = g . 2;
A12: len g = 2 by A1, A11, FINSEQ_1:2, FINSEQ_1:def_3;
( 1 in dom D & 2 in dom D ) by A1, TARSKI:def_2;
then A13: ( g . 1 in X & g . 2 in Y & w = <*(g . 1),(g . 2)*> ) by A11, A12, A1, FINSEQ_1:44;
reconsider z = [(g . 1),(g . 2)] as Element of [:X,Y:] by A13, ZFMISC_1:87;
w = I . ((g . 1),(g . 2)) by A5, A13
.= I . z ;
hence w in rng I by A6, FUNCT_2:112; ::_thesis: verum
end;
then product D c= rng I by TARSKI:def_3;
then product D = rng I by XBOOLE_0:def_10;
then I is onto by FUNCT_2:def_3;
hence ex I being Function of [:X,Y:],(product D) st
( I is one-to-one & I is onto & ( for x, y being set st x in X & y in Y holds
I . (x,y) = <*x,y*> ) ) by A5, A10; ::_thesis: verum
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 set st x in X holds
I . x = <*x*> ) )
proof
let X be non empty set ; ::_thesis: ex I being Function of X,(product <*X*>) st
( I is one-to-one & I is onto & ( for x being set st x in X holds
I . x = <*x*> ) )
( dom <*X*> = {1} & <*X*> . 1 = X ) by FINSEQ_1:2, FINSEQ_1:38, FINSEQ_1:40;
hence ex I being Function of X,(product <*X*>) st
( I is one-to-one & I is onto & ( for x being set st x in X holds
I . x = <*x*> ) ) by Th2; ::_thesis: verum
end;
registration
let X, Y be non empty non-empty FinSequence;
clusterX ^ Y -> non-empty ;
correctness
coherence
X ^ Y is non-empty ;
proof
now__::_thesis:_for_z_being_set_st_z_in_dom_(X_^_Y)_holds_
not_(X_^_Y)_._z_is_empty
let z be set ; ::_thesis: ( z in dom (X ^ Y) implies not (X ^ Y) . b1 is empty )
assume A1: z in dom (X ^ Y) ; ::_thesis: not (X ^ Y) . b1 is empty
then reconsider k = z as Element of NAT ;
percases ( k in dom X or ex n being Nat st
( n in dom Y & k = (len X) + n ) ) by A1, FINSEQ_1:25;
supposeA2: k in dom X ; ::_thesis: not (X ^ Y) . b1 is empty
then X . k = (X ^ Y) . k by FINSEQ_1:def_7;
hence not (X ^ Y) . z is empty by A2; ::_thesis: verum
end;
suppose ex n being Nat st
( n in dom Y & k = (len X) + n ) ; ::_thesis: not (X ^ Y) . b1 is empty
then consider n being Nat such that
A3: ( n in dom Y & k = (len X) + n ) ;
Y . n = (X ^ Y) . k by A3, FINSEQ_1:def_7;
hence not (X ^ Y) . z is empty by A3; ::_thesis: verum
end;
end;
end;
hence X ^ Y is non-empty by FUNCT_1:def_9; ::_thesis: verum
end;
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 set st x in X & y in Y holds
I . (x,y) = <*x,y*> ) )
proof
let X, Y be non empty set ; ::_thesis: ex I being Function of [:X,Y:],(product <*X,Y*>) st
( I is one-to-one & I is onto & ( for x, y being set st x in X & y in Y holds
I . (x,y) = <*x,y*> ) )
( dom <*X,Y*> = {1,2} & <*X,Y*> . 1 = X & <*X,Y*> . 2 = Y ) by FINSEQ_1:2, FINSEQ_1:44, FINSEQ_1:89;
hence ex I being Function of [:X,Y:],(product <*X,Y*>) st
( I is one-to-one & I is onto & ( for x, y being set st x in X & y in Y holds
I . (x,y) = <*x,y*> ) ) by Th3; ::_thesis: verum
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 ) )
proof
let X, Y be non empty non-empty FinSequence; ::_thesis: 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 ) )
defpred S1[ set , set , set ] means ex x, y being FinSequence st
( x = $1 & y = $2 & $3 = x ^ y );
A1: for x, y being set st x in product X & y in product Y holds
ex z being set st
( z in product (X ^ Y) & S1[x,y,z] )
proof
let x, y be set ; ::_thesis: ( x in product X & y in product Y implies ex z being set st
( z in product (X ^ Y) & S1[x,y,z] ) )
assume A2: ( x in product X & y in product Y ) ; ::_thesis: ex z being set st
( z in product (X ^ Y) & S1[x,y,z] )
then consider g being Function such that
A3: ( x = g & dom g = dom X & ( for z being set st z in dom X holds
g . z in X . z ) ) by CARD_3:def_5;
A4: dom g = Seg (len X) by A3, FINSEQ_1:def_3;
then reconsider g = g as FinSequence by FINSEQ_1:def_2;
consider h being Function such that
A5: ( y = h & dom h = dom Y & ( for z being set st z in dom Y holds
h . z in Y . z ) ) by A2, CARD_3:def_5;
A6: dom h = Seg (len Y) by A5, FINSEQ_1:def_3;
then reconsider h = h as FinSequence by FINSEQ_1:def_2;
A7: ( len g = len X & len h = len Y ) by A4, A6, FINSEQ_1:def_3;
A8: dom (g ^ h) = Seg ((len g) + (len h)) by FINSEQ_1:def_7
.= Seg (len (X ^ Y)) by A7, FINSEQ_1:22
.= dom (X ^ Y) by FINSEQ_1:def_3 ;
for z being set st z in dom (X ^ Y) holds
(g ^ h) . z in (X ^ Y) . z
proof
let z be set ; ::_thesis: ( z in dom (X ^ Y) implies (g ^ h) . z in (X ^ Y) . z )
assume A9: z in dom (X ^ Y) ; ::_thesis: (g ^ h) . z in (X ^ Y) . z
then reconsider k = z as Element of NAT ;
percases ( k in dom X or ex n being Nat st
( n in dom Y & k = (len X) + n ) ) by A9, FINSEQ_1:25;
supposeA10: k in dom X ; ::_thesis: (g ^ h) . z in (X ^ Y) . z
then A11: g . k in X . k by A3;
g . k = (g ^ h) . k by A10, A3, FINSEQ_1:def_7;
hence (g ^ h) . z in (X ^ Y) . z by A11, A10, FINSEQ_1:def_7; ::_thesis: verum
end;
suppose ex n being Nat st
( n in dom Y & k = (len X) + n ) ; ::_thesis: (g ^ h) . z in (X ^ Y) . z
then consider n being Nat such that
A12: ( n in dom Y & k = (len X) + n ) ;
A13: h . n in Y . n by A12, A5;
h . n = (g ^ h) . k by A12, A7, A5, FINSEQ_1:def_7;
hence (g ^ h) . z in (X ^ Y) . z by A13, A12, FINSEQ_1:def_7; ::_thesis: verum
end;
end;
end;
then g ^ h in product (X ^ Y) by A8, CARD_3:9;
hence ex z being set st
( z in product (X ^ Y) & S1[x,y,z] ) by A3, A5; ::_thesis: verum
end;
consider I being Function of [:(product X),(product Y):],(product (X ^ Y)) such that
A14: for x, y being set st x in product X & y in product Y holds
S1[x,y,I . (x,y)] from BINOP_1:sch_1(A1);
A15: for x, y being FinSequence st x in product X & y in product Y holds
I . (x,y) = x ^ y
proof
let x, y be FinSequence; ::_thesis: ( x in product X & y in product Y implies I . (x,y) = x ^ y )
assume ( x in product X & y in product Y ) ; ::_thesis: I . (x,y) = x ^ y
then ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 ) by A14;
hence I . (x,y) = x ^ y ; ::_thesis: verum
end;
now__::_thesis:_for_z1,_z2_being_set_st_z1_in_[:(product_X),(product_Y):]_&_z2_in_[:(product_X),(product_Y):]_&_I_._z1_=_I_._z2_holds_
z1_=_z2
let z1, z2 be set ; ::_thesis: ( z1 in [:(product X),(product Y):] & z2 in [:(product X),(product Y):] & I . z1 = I . z2 implies z1 = z2 )
assume A16: ( z1 in [:(product X),(product Y):] & z2 in [:(product X),(product Y):] & I . z1 = I . z2 ) ; ::_thesis: z1 = z2
consider x1, y1 being set such that
A17: ( x1 in product X & y1 in product Y & z1 = [x1,y1] ) by A16, ZFMISC_1:def_2;
consider x2, y2 being set such that
A18: ( x2 in product X & y2 in product Y & z2 = [x2,y2] ) by A16, ZFMISC_1:def_2;
consider xx1, yy1 being FinSequence such that
A19: ( xx1 = x1 & yy1 = y1 & I . (x1,y1) = xx1 ^ yy1 ) by A14, A17;
consider xx2, yy2 being FinSequence such that
A20: ( xx2 = x2 & yy2 = y2 & I . (x2,y2) = xx2 ^ yy2 ) by A14, A18;
A21: dom xx1 = dom X by A17, A19, CARD_3:9
.= dom xx2 by A18, A20, CARD_3:9 ;
xx1 = (xx1 ^ yy1) | (dom xx1) by FINSEQ_1:21
.= xx2 by A16, A17, A18, A19, A20, A21, FINSEQ_1:21 ;
hence z1 = z2 by A16, A17, A18, A19, A20, FINSEQ_1:33; ::_thesis: verum
end;
then A22: I is one-to-one by FUNCT_2:19;
now__::_thesis:_for_w_being_set_st_w_in_product_(X_^_Y)_holds_
w_in_rng_I
let w be set ; ::_thesis: ( w in product (X ^ Y) implies w in rng I )
assume w in product (X ^ Y) ; ::_thesis: w in rng I
then consider g being Function such that
A23: ( w = g & dom g = dom (X ^ Y) & ( for i being set st i in dom (X ^ Y) holds
g . i in (X ^ Y) . i ) ) by CARD_3:def_5;
A24: dom g = Seg (len (X ^ Y)) by A23, FINSEQ_1:def_3;
then reconsider g = g as FinSequence by FINSEQ_1:def_2;
set x = g | (len X);
set y = g /^ (len X);
A25: g is FinSequence of rng g by FINSEQ_1:def_4;
rng g <> {} by A23, RELAT_1:42;
then A26: (g | (len X)) ^ (g /^ (len X)) = g by A25, RFINSEQ:8;
A27: len (X ^ Y) = (len X) + (len Y) by FINSEQ_1:22;
then A28: len X <= len (X ^ Y) by NAT_1:11;
A29: len g = len (X ^ Y) by A24, FINSEQ_1:def_3;
then len (g | (len X)) = len X by A27, FINSEQ_1:59, NAT_1:11;
then A30: dom (g | (len X)) = Seg (len X) by FINSEQ_1:def_3
.= dom X by FINSEQ_1:def_3 ;
for z being set st z in dom X holds
(g | (len X)) . z in X . z
proof
let z be set ; ::_thesis: ( z in dom X implies (g | (len X)) . z in X . z )
assume A31: z in dom X ; ::_thesis: (g | (len X)) . z in X . z
then reconsider k = z as Element of NAT ;
A32: dom X c= dom (X ^ Y) by FINSEQ_1:26;
A33: (g | (len X)) . k = g . k by A31, A26, A30, FINSEQ_1:def_7;
X . k = (X ^ Y) . k by A31, FINSEQ_1:def_7;
hence (g | (len X)) . z in X . z by A33, A23, A31, A32; ::_thesis: verum
end;
then A34: g | (len X) in product X by A30, CARD_3:9;
dom (g | (len X)) = Seg (len X) by A30, FINSEQ_1:def_3;
then A35: len (g | (len X)) = len X by FINSEQ_1:def_3;
len (g /^ (len X)) = (len g) - (len X) by A28, A29, RFINSEQ:def_1
.= len Y by A29, A27 ;
then Seg (len (g /^ (len X))) = dom Y by FINSEQ_1:def_3;
then A36: dom (g /^ (len X)) = dom Y by FINSEQ_1:def_3;
for z being set st z in dom Y holds
(g /^ (len X)) . z in Y . z
proof
let z be set ; ::_thesis: ( z in dom Y implies (g /^ (len X)) . z in Y . z )
assume A37: z in dom Y ; ::_thesis: (g /^ (len X)) . z in Y . z
then reconsider k = z as Element of NAT ;
A38: (g /^ (len X)) . k = g . ((len X) + k) by A37, A26, A35, A36, FINSEQ_1:def_7;
Y . k = (X ^ Y) . ((len X) + k) by A37, FINSEQ_1:def_7;
hence (g /^ (len X)) . z in Y . z by A38, A23, A37, FINSEQ_1:28; ::_thesis: verum
end;
then A39: g /^ (len X) in product Y by A36, CARD_3:9;
reconsider z = [(g | (len X)),(g /^ (len X))] as Element of [:(product X),(product Y):] by A34, A39, ZFMISC_1:87;
w = I . ((g | (len X)),(g /^ (len X))) by A23, A26, A15, A34, A39
.= I . z ;
hence w in rng I by FUNCT_2:112; ::_thesis: verum
end;
then product (X ^ Y) c= rng I by TARSKI:def_3;
then product (X ^ Y) = rng I by XBOOLE_0:def_10;
then I is onto by FUNCT_2:def_3;
hence 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 ) ) by A15, A22; ::_thesis: verum
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 ;
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
ex b1 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 b1 . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)]
proof
defpred S1[ set , set , set ] means ex g1, g2 being Point of G ex f1, f2 being Point of F st
( $1 = [g1,f1] & $2 = [g2,f2] & $3 = [(g1 + g2),(f1 + f2)] );
A1: for x, y being set st x in [: the carrier of G, the carrier of F:] & y in [: the carrier of G, the carrier of F:] holds
ex z being set st
( z in [: the carrier of G, the carrier of F:] & S1[x,y,z] )
proof
let x, y be set ; ::_thesis: ( x in [: the carrier of G, the carrier of F:] & y in [: the carrier of G, the carrier of F:] implies ex z being set st
( z in [: the carrier of G, the carrier of F:] & S1[x,y,z] ) )
assume A2: ( x in [: the carrier of G, the carrier of F:] & y in [: the carrier of G, the carrier of F:] ) ; ::_thesis: ex z being set st
( z in [: the carrier of G, the carrier of F:] & S1[x,y,z] )
then consider x1 being Point of G, x2 being Point of F such that
A3: x = [x1,x2] by Lm1;
consider y1 being Point of G, y2 being Point of F such that
A4: y = [y1,y2] by Lm1, A2;
reconsider z = [(x1 + y1),(x2 + y2)] as Element of [: the carrier of G, the carrier of F:] ;
( z in [: the carrier of G, the carrier of F:] & S1[x,y,z] ) by A3, A4;
hence ex z being set st
( z in [: the carrier of G, the carrier of F:] & S1[x,y,z] ) ; ::_thesis: verum
end;
consider ADGF being Function of [:[: the carrier of G, the carrier of F:],[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:] such that
A5: for x, y being set st x in [: the carrier of G, the carrier of F:] & y in [: the carrier of G, the carrier of F:] holds
S1[x,y,ADGF . (x,y)] from BINOP_1:sch_1(A1);
now__::_thesis:_for_g1,_g2_being_Point_of_G
for_f1,_f2_being_Point_of_F_holds_ADGF_._([g1,f1],[g2,f2])_=_[(g1_+_g2),(f1_+_f2)]
let g1, g2 be Point of G; ::_thesis: for f1, f2 being Point of F holds ADGF . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)]
let f1, f2 be Point of F; ::_thesis: ADGF . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)]
consider gg1, gg2 being Point of G, ff1, ff2 being Point of F such that
A6: ( [g1,f1] = [gg1,ff1] & [g2,f2] = [gg2,ff2] & ADGF . ([g1,f1],[g2,f2]) = [(gg1 + gg2),(ff1 + ff2)] ) by A5;
( g1 = gg1 & f1 = ff1 & g2 = gg2 & f2 = ff2 ) by A6, XTUPLE_0:1;
hence ADGF . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] by A6; ::_thesis: verum
end;
hence ex b1 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 b1 . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] ; ::_thesis: verum
end;
uniqueness
for b1, b2 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 b1 . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] ) & ( for g1, g2 being Point of G
for f1, f2 being Point of F holds b2 . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] ) holds
b1 = b2
proof
let H1, H2 be BinOp of [: the carrier of G, the carrier of F:]; ::_thesis: ( ( for g1, g2 being Point of G
for f1, f2 being Point of F holds H1 . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] ) & ( for g1, g2 being Point of G
for f1, f2 being Point of F holds H2 . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] ) implies H1 = H2 )
assume A7: for g1, g2 being Point of G
for f1, f2 being Point of F holds H1 . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] ; ::_thesis: ( ex g1, g2 being Point of G ex f1, f2 being Point of F st not H2 . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] or H1 = H2 )
assume A8: for g1, g2 being Point of G
for f1, f2 being Point of F holds H2 . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] ; ::_thesis: H1 = H2
now__::_thesis:_for_x,_y_being_Element_of_[:_the_carrier_of_G,_the_carrier_of_F:]_holds_H1_._(x,y)_=_H2_._(x,y)
let x, y be Element of [: the carrier of G, the carrier of F:]; ::_thesis: H1 . (x,y) = H2 . (x,y)
consider x1 being Point of G, x2 being Point of F such that
A9: x = [x1,x2] by Lm1;
consider y1 being Point of G, y2 being Point of F such that
A10: y = [y1,y2] by Lm1;
thus H1 . (x,y) = [(x1 + y1),(x2 + y2)] by A7, A9, A10
.= H2 . (x,y) by A8, A9, A10 ; ::_thesis: verum
end;
hence H1 = H2 by BINOP_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines prod_ADD PRVECT_3:def_1_:_
for G, F being non empty addLoopStr
for b3 being BinOp of [: the carrier of G, the carrier of F:] holds
( b3 = prod_ADD (G,F) iff for g1, g2 being Point of G
for f1, f2 being Point of F holds b3 . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] );
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 :Def2: :: PRVECT_3:def 2
for r being Element of REAL
for g being Point of G
for f being Point of F holds it . (r,[g,f]) = [(r * g),(r * f)];
existence
ex b1 being Function of [:REAL,[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:] st
for r being Element of REAL
for g being Point of G
for f being Point of F holds b1 . (r,[g,f]) = [(r * g),(r * f)]
proof
defpred S1[ set , set , set ] means ex r being Element of REAL ex g being Point of G ex f being Point of F st
( r = $1 & $2 = [g,f] & $3 = [(r * g),(r * f)] );
set CarrG = the carrier of G;
set CarrF = the carrier of F;
A1: for x, y being set st x in REAL & y in [: the carrier of G, the carrier of F:] holds
ex z being set st
( z in [: the carrier of G, the carrier of F:] & S1[x,y,z] )
proof
let x, y be set ; ::_thesis: ( x in REAL & y in [: the carrier of G, the carrier of F:] implies ex z being set st
( z in [: the carrier of G, the carrier of F:] & S1[x,y,z] ) )
assume A2: ( x in REAL & y in [: the carrier of G, the carrier of F:] ) ; ::_thesis: ex z being set st
( z in [: the carrier of G, the carrier of F:] & S1[x,y,z] )
then reconsider r = x as Element of REAL ;
consider y1 being Point of G, y2 being Point of F such that
A3: y = [y1,y2] by A2, Lm1;
set z = [(r * y1),(r * y2)];
( [(r * y1),(r * y2)] in [: the carrier of G, the carrier of F:] & S1[x,y,[(r * y1),(r * y2)]] ) by A3;
hence ex z being set st
( z in [: the carrier of G, the carrier of F:] & S1[x,y,z] ) ; ::_thesis: verum
end;
consider MLTGF being Function of [:REAL,[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:] such that
A4: for x, y being set st x in REAL & y in [: the carrier of G, the carrier of F:] holds
S1[x,y,MLTGF . (x,y)] from BINOP_1:sch_1(A1);
now__::_thesis:_for_r_being_Element_of_REAL_
for_g_being_Point_of_G
for_f_being_Point_of_F_holds_MLTGF_._(r,[g,f])_=_[(r_*_g),(r_*_f)]
let r be Element of REAL ; ::_thesis: for g being Point of G
for f being Point of F holds MLTGF . (r,[g,f]) = [(r * g),(r * f)]
let g be Point of G; ::_thesis: for f being Point of F holds MLTGF . (r,[g,f]) = [(r * g),(r * f)]
let f be Point of F; ::_thesis: MLTGF . (r,[g,f]) = [(r * g),(r * f)]
S1[r,[g,f],MLTGF . (r,[g,f])] by A4;
then consider rr being Element of REAL , gg being Point of G, ff being Point of F such that
A5: ( rr = r & [g,f] = [gg,ff] & MLTGF . (r,[g,f]) = [(rr * gg),(r * ff)] ) ;
( g = gg & f = ff ) by A5, XTUPLE_0:1;
hence MLTGF . (r,[g,f]) = [(r * g),(r * f)] by A5; ::_thesis: verum
end;
hence ex b1 being Function of [:REAL,[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:] st
for r being Element of REAL
for g being Point of G
for f being Point of F holds b1 . (r,[g,f]) = [(r * g),(r * f)] ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of [:REAL,[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:] st ( for r being Element of REAL
for g being Point of G
for f being Point of F holds b1 . (r,[g,f]) = [(r * g),(r * f)] ) & ( for r being Element of REAL
for g being Point of G
for f being Point of F holds b2 . (r,[g,f]) = [(r * g),(r * f)] ) holds
b1 = b2
proof
let H1, H2 be Function of [:REAL,[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:]; ::_thesis: ( ( for r being Element of REAL
for g being Point of G
for f being Point of F holds H1 . (r,[g,f]) = [(r * g),(r * f)] ) & ( for r being Element of REAL
for g being Point of G
for f being Point of F holds H2 . (r,[g,f]) = [(r * g),(r * f)] ) implies H1 = H2 )
assume A6: for r being Element of REAL
for g being Point of G
for f being Point of F holds H1 . (r,[g,f]) = [(r * g),(r * f)] ; ::_thesis: ( ex r being Element of REAL ex g being Point of G ex f being Point of F st not H2 . (r,[g,f]) = [(r * g),(r * f)] or H1 = H2 )
assume A7: for r being Element of REAL
for g being Point of G
for f being Point of F holds H2 . (r,[g,f]) = [(r * g),(r * f)] ; ::_thesis: H1 = H2
now__::_thesis:_for_r_being_Element_of_REAL_
for_x_being_Element_of_[:_the_carrier_of_G,_the_carrier_of_F:]_holds_H1_._(r,x)_=_H2_._(r,x)
let r be Element of REAL ; ::_thesis: for x being Element of [: the carrier of G, the carrier of F:] holds H1 . (r,x) = H2 . (r,x)
let x be Element of [: the carrier of G, the carrier of F:]; ::_thesis: H1 . (r,x) = H2 . (r,x)
consider x1 being Point of G, x2 being Point of F such that
A8: x = [x1,x2] by Lm1;
thus H1 . (r,x) = [(r * x1),(r * x2)] by A6, A8
.= H2 . (r,x) by A7, A8 ; ::_thesis: verum
end;
hence H1 = H2 by BINOP_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines prod_MLT PRVECT_3:def_2_:_
for G, F being non empty RLSStruct
for b3 being Function of [:REAL,[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:] holds
( b3 = prod_MLT (G,F) iff for r being Element of REAL
for g being Point of G
for f being Point of F holds b3 . (r,[g,f]) = [(r * g),(r * f)] );
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)];
correctness
coherence
[(0. G),(0. F)] is Element of [: the carrier of G, the carrier of F:];
;
end;
:: deftheorem defines prod_ZERO PRVECT_3:def_3_:_
for G, F being non empty addLoopStr holds prod_ZERO (G,F) = [(0. G),(0. F)];
definition
let G, F be non empty addLoopStr ;
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
coherence
addLoopStr(# [: the carrier of G, the carrier of F:],(prod_ADD (G,F)),(prod_ZERO (G,F)) #) is non empty strict addLoopStr ;
;
end;
:: 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)) #);
registration
let G, F be non empty Abelian addLoopStr ;
cluster[:G,F:] -> non empty strict Abelian ;
correctness
coherence
[:G,F:] is Abelian ;
proof
let x, y be Element of [:G,F:]; :: according to RLVECT_1:def_2 ::_thesis: x + y = y + x
consider x1 being Point of G, x2 being Point of F such that
A1: x = [x1,x2] by Lm1;
consider y1 being Point of G, y2 being Point of F such that
A2: y = [y1,y2] by Lm1;
thus x + y = [(x1 + y1),(x2 + y2)] by A1, A2, Def1
.= y + x by A1, A2, Def1 ; ::_thesis: verum
end;
end;
registration
let G, F be non empty add-associative addLoopStr ;
cluster[:G,F:] -> non empty strict add-associative ;
correctness
coherence
[:G,F:] is add-associative ;
proof
let x, y, z be Element of [:G,F:]; :: according to RLVECT_1:def_3 ::_thesis: (x + y) + z = x + (y + z)
consider x1 being Point of G, x2 being Point of F such that
A1: x = [x1,x2] by Lm1;
consider y1 being Point of G, y2 being Point of F such that
A2: y = [y1,y2] by Lm1;
consider z1 being Point of G, z2 being Point of F such that
A3: z = [z1,z2] by Lm1;
A4: ( (x1 + y1) + z1 = x1 + (y1 + z1) & (x2 + y2) + z2 = x2 + (y2 + z2) ) by RLVECT_1:def_3;
thus (x + y) + z = (prod_ADD (G,F)) . ([(x1 + y1),(x2 + y2)],[z1,z2]) by A1, A2, A3, Def1
.= [((x1 + y1) + z1),((x2 + y2) + z2)] by Def1
.= (prod_ADD (G,F)) . ([x1,x2],[(y1 + z1),(y2 + z2)]) by A4, Def1
.= x + (y + z) by A1, A2, A3, Def1 ; ::_thesis: verum
end;
end;
registration
let G, F be non empty right_zeroed addLoopStr ;
cluster[:G,F:] -> non empty strict right_zeroed ;
correctness
coherence
[:G,F:] is right_zeroed ;
proof
let x be Element of [:G,F:]; :: according to RLVECT_1:def_4 ::_thesis: x + (0. [:G,F:]) = x
consider x1 being Point of G, x2 being Point of F such that
A1: x = [x1,x2] by Lm1;
( x1 + (0. G) = x1 & x2 + (0. F) = x2 ) by RLVECT_1:def_4;
hence x + (0. [:G,F:]) = x by A1, Def1; ::_thesis: verum
end;
end;
registration
let G, F be non empty right_complementable addLoopStr ;
cluster[:G,F:] -> non empty strict right_complementable ;
correctness
coherence
[:G,F:] is right_complementable ;
proof
let x be Element of [:G,F:]; :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
consider x1 being Point of G, x2 being Point of F such that
A1: x = [x1,x2] by Lm1;
consider y1 being Point of G such that
A2: x1 + y1 = 0. G by ALGSTR_0:def_11;
consider y2 being Point of F such that
A3: x2 + y2 = 0. F by ALGSTR_0:def_11;
reconsider y = [y1,y2] as Element of [:G,F:] ;
take y ; :: according to ALGSTR_0:def_11 ::_thesis: x + y = 0. [:G,F:]
thus x + y = 0. [:G,F:] by A1, A2, A3, Def1; ::_thesis: verum
end;
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;
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)]
proof
let G, F be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: 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)]
let x be Point of [:G,F:]; ::_thesis: for x1 being Point of G
for x2 being Point of F st x = [x1,x2] holds
- x = [(- x1),(- x2)]
let x1 be Point of G; ::_thesis: for x2 being Point of F st x = [x1,x2] holds
- x = [(- x1),(- x2)]
let x2 be Point of F; ::_thesis: ( x = [x1,x2] implies - x = [(- x1),(- x2)] )
assume A1: x = [x1,x2] ; ::_thesis: - x = [(- x1),(- x2)]
reconsider y = [(- x1),(- x2)] as Point of [:G,F:] ;
x + y = [(x1 + (- x1)),(x2 + (- x2))] by A1, Def1
.= [(0. G),(x2 + (- x2))] by RLVECT_1:def_10
.= 0. [:G,F:] by RLVECT_1:def_10 ;
hence - x = [(- x1),(- x2)] by RLVECT_1:def_10; ::_thesis: verum
end;
registration
let G, F be non empty strict right_complementable Abelian add-associative right_zeroed addLoopStr ;
cluster[:G,F:] -> non empty strict right_complementable Abelian add-associative right_zeroed ;
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;
definition
let G, F be non empty RLSStruct ;
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
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;
:: 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)) #);
registration
let G, F be non empty Abelian RLSStruct ;
cluster[:G,F:] -> non empty strict Abelian ;
correctness
coherence
[:G,F:] is Abelian ;
proof
let x, y be Element of [:G,F:]; :: according to RLVECT_1:def_2 ::_thesis: x + y = y + x
consider x1 being Point of G, x2 being Point of F such that
A1: x = [x1,x2] by Lm1;
consider y1 being Point of G, y2 being Point of F such that
A2: y = [y1,y2] by Lm1;
x + y = [(x1 + y1),(x2 + y2)] by A1, A2, Def1;
hence x + y = y + x by A1, A2, Def1; ::_thesis: verum
end;
end;
registration
let G, F be non empty add-associative RLSStruct ;
cluster[:G,F:] -> non empty strict add-associative ;
correctness
coherence
[:G,F:] is add-associative ;
proof
let x, y, z be Element of [:G,F:]; :: according to RLVECT_1:def_3 ::_thesis: (x + y) + z = x + (y + z)
consider x1 being Point of G, x2 being Point of F such that
A1: x = [x1,x2] by Lm1;
consider y1 being Point of G, y2 being Point of F such that
A2: y = [y1,y2] by Lm1;
consider z1 being Point of G, z2 being Point of F such that
A3: z = [z1,z2] by Lm1;
A4: ( (x1 + y1) + z1 = x1 + (y1 + z1) & (x2 + y2) + z2 = x2 + (y2 + z2) ) by RLVECT_1:def_3;
thus (x + y) + z = (prod_ADD (G,F)) . ([(x1 + y1),(x2 + y2)],[z1,z2]) by A1, A2, A3, Def1
.= [(x1 + (y1 + z1)),(x2 + (y2 + z2))] by A4, Def1
.= (prod_ADD (G,F)) . ([x1,x2],[(y1 + z1),(y2 + z2)]) by Def1
.= x + (y + z) by A1, A2, A3, Def1 ; ::_thesis: verum
end;
end;
registration
let G, F be non empty right_zeroed RLSStruct ;
cluster[:G,F:] -> non empty strict right_zeroed ;
correctness
coherence
[:G,F:] is right_zeroed ;
proof
let x be Element of [:G,F:]; :: according to RLVECT_1:def_4 ::_thesis: x + (0. [:G,F:]) = x
consider x1 being Point of G, x2 being Point of F such that
A1: x = [x1,x2] by Lm1;
( x1 + (0. G) = x1 & x2 + (0. F) = x2 ) by RLVECT_1:def_4;
hence x + (0. [:G,F:]) = x by A1, Def1; ::_thesis: verum
end;
end;
registration
let G, F be non empty right_complementable RLSStruct ;
cluster[:G,F:] -> non empty right_complementable strict ;
correctness
coherence
[:G,F:] is right_complementable ;
proof
let x be Element of [:G,F:]; :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
consider x1 being Point of G, x2 being Point of F such that
A1: x = [x1,x2] by Lm1;
consider y1 being Point of G such that
A2: x1 + y1 = 0. G by ALGSTR_0:def_11;
consider y2 being Point of F such that
A3: x2 + y2 = 0. F by ALGSTR_0:def_11;
reconsider y = [y1,y2] as Element of [:G,F:] ;
take y ; :: according to ALGSTR_0:def_11 ::_thesis: x + y = 0. [:G,F:]
thus x + y = 0. [:G,F:] by A1, A2, A3, Def1; ::_thesis: verum
end;
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 number st x = [x1,x2] holds
a * x = [(a * x1),(a * x2)] ) )
proof
let G, F be non empty RLSStruct ; ::_thesis: ( ( 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 number 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
for a being real number st x = [x1,x2] holds
a * x = [(a * x1),(a * x2)]
proof
let x be Point of [:G,F:]; ::_thesis: for x1 being Point of G
for x2 being Point of F
for a being real number st x = [x1,x2] holds
a * x = [(a * x1),(a * x2)]
let x1 be Point of G; ::_thesis: for x2 being Point of F
for a being real number st x = [x1,x2] holds
a * x = [(a * x1),(a * x2)]
let x2 be Point of F; ::_thesis: for a being real number st x = [x1,x2] holds
a * x = [(a * x1),(a * x2)]
let a be real number ; ::_thesis: ( x = [x1,x2] implies a * x = [(a * x1),(a * x2)] )
reconsider a0 = a as Element of REAL by XREAL_0:def_1;
assume A1: x = [x1,x2] ; ::_thesis: a * x = [(a * x1),(a * x2)]
a * x = (prod_MLT (G,F)) . (a0,x) ;
hence a * x = [(a * x1),(a * x2)] by A1, Def2; ::_thesis: verum
end;
hence ( ( 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 number st x = [x1,x2] holds
a * x = [(a * x1),(a * x2)] ) ) by Def1, Lm1; ::_thesis: verum
end;
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)]
proof
let G, F be non empty right_complementable add-associative right_zeroed RLSStruct ; ::_thesis: 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)]
let x be Point of [:G,F:]; ::_thesis: for x1 being Point of G
for x2 being Point of F st x = [x1,x2] holds
- x = [(- x1),(- x2)]
let x1 be Point of G; ::_thesis: for x2 being Point of F st x = [x1,x2] holds
- x = [(- x1),(- x2)]
let x2 be Point of F; ::_thesis: ( x = [x1,x2] implies - x = [(- x1),(- x2)] )
assume A1: x = [x1,x2] ; ::_thesis: - x = [(- x1),(- x2)]
reconsider y = [(- x1),(- x2)] as Point of [:G,F:] ;
x + y = [(x1 + (- x1)),(x2 + (- x2))] by A1, Def1
.= [(0. G),(x2 + (- x2))] by RLVECT_1:def_10
.= 0. [:G,F:] by RLVECT_1:def_10 ;
hence - x = [(- x1),(- x2)] by RLVECT_1:def_10; ::_thesis: verum
end;
registration
let G, F be non empty vector-distributive RLSStruct ;
cluster[:G,F:] -> non empty strict vector-distributive ;
correctness
coherence
[:G,F:] is vector-distributive ;
proof
let a0 be real number ; :: according to RLVECT_1:def_5 ::_thesis: for b1, b2 being Element of the carrier of [:G,F:] holds a0 * (b1 + b2) = (a0 * b1) + (a0 * b2)
let x, y be VECTOR of [:G,F:]; ::_thesis: a0 * (x + y) = (a0 * x) + (a0 * y)
reconsider a = a0 as Element of REAL by XREAL_0:def_1;
consider x1 being Point of G, x2 being Point of F such that
A1: x = [x1,x2] by Lm1;
consider y1 being Point of G, y2 being Point of F such that
A2: y = [y1,y2] by Lm1;
A3: ( a * (x1 + y1) = (a0 * x1) + (a0 * y1) & a * (x2 + y2) = (a0 * x2) + (a0 * y2) ) by RLVECT_1:def_5;
thus a0 * (x + y) = (prod_MLT (G,F)) . (a,[(x1 + y1),(x2 + y2)]) by A1, A2, Def1
.= [(a * (x1 + y1)),(a * (x2 + y2))] by Def2
.= (prod_ADD (G,F)) . ([(a * x1),(a * x2)],[(a * y1),(a * y2)]) by A3, Def1
.= (prod_ADD (G,F)) . (((prod_MLT (G,F)) . (a,[x1,x2])),[(a * y1),(a * y2)]) by Def2
.= (a0 * x) + (a0 * y) by A1, A2, Def2 ; ::_thesis: verum
end;
end;
registration
let G, F be non empty scalar-distributive RLSStruct ;
cluster[:G,F:] -> non empty strict scalar-distributive ;
correctness
coherence
[:G,F:] is scalar-distributive ;
proof
let a0, b0 be real number ; :: according to RLVECT_1:def_6 ::_thesis: for b1 being Element of the carrier of [:G,F:] holds (a0 + b0) * b1 = (a0 * b1) + (b0 * b1)
let x be VECTOR of [:G,F:]; ::_thesis: (a0 + b0) * x = (a0 * x) + (b0 * x)
reconsider a = a0, b = b0 as Element of REAL by XREAL_0:def_1;
consider x1 being Point of G, x2 being Point of F such that
A1: x = [x1,x2] by Lm1;
A2: ( (a + b) * x1 = (a0 * x1) + (b0 * x1) & (a + b) * x2 = (a0 * x2) + (b0 * x2) ) by RLVECT_1:def_6;
thus (a0 + b0) * x = [((a + b) * x1),((a + b) * x2)] by A1, Def2
.= (prod_ADD (G,F)) . ([(a * x1),(a * x2)],[(b * x1),(b * x2)]) by A2, Def1
.= (prod_ADD (G,F)) . (((prod_MLT (G,F)) . (a,[x1,x2])),[(b * x1),(b * x2)]) by Def2
.= (a0 * x) + (b0 * x) by A1, Def2 ; ::_thesis: verum
end;
end;
registration
let G, F be non empty scalar-associative RLSStruct ;
cluster[:G,F:] -> non empty strict scalar-associative ;
correctness
coherence
[:G,F:] is scalar-associative ;
proof
let a0, b0 be real number ; :: according to RLVECT_1:def_7 ::_thesis: for b1 being Element of the carrier of [:G,F:] holds (a0 * b0) * b1 = a0 * (b0 * b1)
let x be VECTOR of [:G,F:]; ::_thesis: (a0 * b0) * x = a0 * (b0 * x)
reconsider a = a0, b = b0 as Element of REAL by XREAL_0:def_1;
consider x1 being Point of G, x2 being Point of F such that
A1: x = [x1,x2] by Lm1;
A2: ( (a * b) * x1 = a0 * (b0 * x1) & (a * b) * x2 = a0 * (b0 * x2) ) by RLVECT_1:def_7;
thus (a0 * b0) * x = [((a * b) * x1),((a * b) * x2)] by A1, Def2
.= (prod_MLT (G,F)) . (a,[(b * x1),(b * x2)]) by A2, Def2
.= a0 * (b0 * x) by A1, Def2 ; ::_thesis: verum
end;
end;
registration
let G, F be non empty scalar-unital RLSStruct ;
cluster[:G,F:] -> non empty strict scalar-unital ;
correctness
coherence
[:G,F:] is scalar-unital ;
proof
let x be VECTOR of [:G,F:]; :: according to RLVECT_1:def_8 ::_thesis: 1 * x = x
consider x1 being Point of G, x2 being Point of F such that
A1: x = [x1,x2] by Lm1;
( 1 * x1 = x1 & 1 * x2 = x2 ) by RLVECT_1:def_8;
hence 1 * x = x by A1, Def2; ::_thesis: verum
end;
end;
registration
let G be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ;
cluster<*G*> -> RealLinearSpace-yielding ;
correctness
coherence
<*G*> is RealLinearSpace-yielding ;
proof
let S be set ; :: according to PRVECT_2:def_3 ::_thesis: ( not S in rng <*G*> or S is RLSStruct )
assume S in rng <*G*> ; ::_thesis: S is RLSStruct
then consider i being set such that
A1: ( i in dom <*G*> & <*G*> . i = S ) by FUNCT_1:def_3;
reconsider i = i as Element of NAT by A1;
dom <*G*> = {1} by FINSEQ_1:2, FINSEQ_1:def_8;
then i = 1 by A1, TARSKI:def_1;
hence S is RealLinearSpace by A1, FINSEQ_1:40; ::_thesis: verum
end;
end;
registration
let G, F be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ;
cluster<*G,F*> -> RealLinearSpace-yielding ;
correctness
coherence
<*G,F*> is RealLinearSpace-yielding ;
proof
let S be set ; :: according to PRVECT_2:def_3 ::_thesis: ( not S in rng <*G,F*> or S is RLSStruct )
assume S in rng <*G,F*> ; ::_thesis: S is RLSStruct
then consider i being set such that
A1: ( i in dom <*G,F*> & <*G,F*> . i = S ) by FUNCT_1:def_3;
dom <*G,F*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89;
then ( i = 1 or i = 2 ) by A1, TARSKI:def_2;
hence S is RealLinearSpace by A1, FINSEQ_1:44; ::_thesis: verum
end;
end;
begin
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*>) )
proof
let X be RealLinearSpace; ::_thesis: 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*>) )
set CarrX = the carrier of X;
consider I being Function of the carrier of X,(product <* the carrier of X*>) such that
A1: ( I is one-to-one & I is onto & ( for x being set st x in the carrier of X holds
I . x = <*x*> ) ) by Th4;
len (carr <*X*>) = len <*X*> by PRVECT_2:def_4;
then A2: len (carr <*X*>) = 1 by FINSEQ_1:40;
A3: dom <*X*> = {1} by FINSEQ_1:2, FINSEQ_1:def_8;
A4: <*X*> . 1 = X by FINSEQ_1:def_8;
1 in {1} by TARSKI:def_1;
then (carr <*X*>) . 1 = the carrier of X by A3, A4, PRVECT_2:def_4;
then A5: carr <*X*> = <* the carrier of X*> by A2, FINSEQ_1:40;
then reconsider I = I as Function of X,(product <*X*>) ;
A6: for x being Point of X holds I . x = <*x*> by A1;
A7: for v, w being Point of X holds I . (v + w) = (I . v) + (I . w)
proof
let v, w be Point of X; ::_thesis: I . (v + w) = (I . v) + (I . w)
A8: ( I . v = <*v*> & I . w = <*w*> & I . (v + w) = <*(v + w)*> ) by A1;
A9: ( <*v*> . 1 = v & <*w*> . 1 = w ) by FINSEQ_1:40;
reconsider Iv = I . v, Iw = I . w as Element of product (carr <*X*>) ;
1 in {1} by TARSKI:def_1;
then reconsider j1 = 1 as Element of dom (carr <*X*>) by A2, FINSEQ_1:2, FINSEQ_1:def_3;
A10: (addop <*X*>) . j1 = the addF of (<*X*> . j1) by PRVECT_2:def_5;
A11: ([:(addop <*X*>):] . (Iv,Iw)) . j1 = ((addop <*X*>) . j1) . ((Iv . j1),(Iw . j1)) by PRVECT_1:def_8
.= v + w by A10, A8, A9, FINSEQ_1:40 ;
consider Ivw being Function such that
A12: ( (I . v) + (I . w) = Ivw & dom Ivw = dom (carr <*X*>) & ( for i being set st i in dom (carr <*X*>) holds
Ivw . i in (carr <*X*>) . i ) ) by CARD_3:def_5;
A13: dom Ivw = Seg 1 by A2, A12, FINSEQ_1:def_3;
then reconsider Ivw = Ivw as FinSequence by FINSEQ_1:def_2;
len Ivw = 1 by A13, FINSEQ_1:def_3;
hence I . (v + w) = (I . v) + (I . w) by A8, A12, A11, FINSEQ_1:40; ::_thesis: verum
end;
A14: for v being Point of X
for r being Element of REAL holds I . (r * v) = r * (I . v)
proof
let v be Point of X; ::_thesis: for r being Element of REAL holds I . (r * v) = r * (I . v)
let r be Element of REAL ; ::_thesis: I . (r * v) = r * (I . v)
A15: ( I . v = <*v*> & I . (r * v) = <*(r * v)*> ) by A1;
A16: <*v*> . 1 = v by FINSEQ_1:40;
1 in {1} by TARSKI:def_1;
then reconsider j1 = 1 as Element of dom (carr <*X*>) by A2, FINSEQ_1:2, FINSEQ_1:def_3;
A17: (multop <*X*>) . j1 = the Mult of (<*X*> . j1) by PRVECT_2:def_8;
reconsider Iv = I . v as Element of product (carr <*X*>) ;
A18: ([:(multop <*X*>):] . (r,Iv)) . j1 = ((multop <*X*>) . j1) . (r,(Iv . j1)) by PRVECT_2:def_2
.= r * v by A17, A15, A16, FINSEQ_1:40 ;
consider Ivw being Function such that
A19: ( r * (I . v) = Ivw & dom Ivw = dom (carr <*X*>) & ( for i being set st i in dom (carr <*X*>) holds
Ivw . i in (carr <*X*>) . i ) ) by CARD_3:def_5;
A20: dom Ivw = Seg 1 by A2, A19, FINSEQ_1:def_3;
then reconsider Ivw = Ivw as FinSequence by FINSEQ_1:def_2;
len Ivw = 1 by A20, FINSEQ_1:def_3;
hence I . (r * v) = r * (I . v) by A15, A19, A18, FINSEQ_1:40; ::_thesis: verum
end;
I . (0. X) = I . ((0. X) + (0. X)) by RLVECT_1:def_4
.= (I . (0. X)) + (I . (0. X)) by A7 ;
then (I . (0. X)) - (I . (0. X)) = (I . (0. X)) + ((I . (0. X)) - (I . (0. X))) by RLVECT_1:28
.= (I . (0. X)) + (0. (product <*X*>)) by RLVECT_1:15
.= I . (0. X) by RLVECT_1:def_4 ;
then 0. (product <*X*>) = I . (0. X) by RLVECT_1:15;
hence 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*>) ) by A1, A6, A5, A7, A14; ::_thesis: verum
end;
registration
let G, F be non empty RealLinearSpace-yielding FinSequence;
clusterG ^ F -> RealLinearSpace-yielding ;
correctness
coherence
G ^ F is RealLinearSpace-yielding ;
proof
let S be set ; :: according to PRVECT_2:def_3 ::_thesis: ( not S in rng (G ^ F) or S is RLSStruct )
assume S in rng (G ^ F) ; ::_thesis: S is RLSStruct
then consider i being set such that
A1: ( i in dom (G ^ F) & (G ^ F) . i = S ) by FUNCT_1:def_3;
reconsider i = i as Element of NAT by A1;
percases ( i in dom G or ex n being Nat st
( n in dom F & i = (len G) + n ) ) by A1, FINSEQ_1:25;
supposeA2: i in dom G ; ::_thesis: S is RLSStruct
then A3: (G ^ F) . i = G . i by FINSEQ_1:def_7;
G . i in rng G by A2, FUNCT_1:3;
hence S is RealLinearSpace by A3, A1, PRVECT_2:def_3; ::_thesis: verum
end;
suppose ex n being Nat st
( n in dom F & i = (len G) + n ) ; ::_thesis: S is RLSStruct
then consider n being Nat such that
A4: ( n in dom F & i = (len G) + n ) ;
A5: (G ^ F) . i = F . n by A4, FINSEQ_1:def_7;
F . n in rng F by A4, FUNCT_1:3;
hence S is RealLinearSpace by A5, A1, PRVECT_2:def_3; ::_thesis: verum
end;
end;
end;
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 Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. [:X,Y:]) = 0. (product <*X,Y*>) )
proof
let X, Y be RealLinearSpace; ::_thesis: 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 Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. [:X,Y:]) = 0. (product <*X,Y*>) )
set CarrX = the carrier of X;
set CarrY = the carrier of Y;
consider I being Function of [: the carrier of X, the carrier of Y:],(product <* the carrier of X, the carrier of Y*>) such that
A1: ( I is one-to-one & I is onto & ( for x, y being set st x in the carrier of X & y in the carrier of Y holds
I . (x,y) = <*x,y*> ) ) by Th5;
len (carr <*X,Y*>) = len <*X,Y*> by PRVECT_2:def_4;
then A2: len (carr <*X,Y*>) = 2 by FINSEQ_1:44;
then A3: dom (carr <*X,Y*>) = {1,2} by FINSEQ_1:2, FINSEQ_1:def_3;
len <*X,Y*> = 2 by FINSEQ_1:44;
then A4: dom <*X,Y*> = {1,2} by FINSEQ_1:2, FINSEQ_1:def_3;
A5: ( <*X,Y*> . 1 = X & <*X,Y*> . 2 = Y ) by FINSEQ_1:44;
( 1 in {1,2} & 2 in {1,2} ) by TARSKI:def_2;
then ( (carr <*X,Y*>) . 1 = the carrier of X & (carr <*X,Y*>) . 2 = the carrier of Y ) by A4, A5, PRVECT_2:def_4;
then A6: carr <*X,Y*> = <* the carrier of X, the carrier of Y*> by A2, FINSEQ_1:44;
then reconsider I = I as Function of [:X,Y:],(product <*X,Y*>) ;
A7: for x being Point of X
for y being Point of Y holds I . (x,y) = <*x,y*> by A1;
A8: for v, w being Point of [:X,Y:] holds I . (v + w) = (I . v) + (I . w)
proof
let v, w be Point of [:X,Y:]; ::_thesis: I . (v + w) = (I . v) + (I . w)
consider x1 being Point of X, y1 being Point of Y such that
A9: v = [x1,y1] by Lm1;
consider x2 being Point of X, y2 being Point of Y such that
A10: w = [x2,y2] by Lm1;
( I . v = I . (x1,y1) & I . w = I . (x2,y2) ) by A9, A10;
then A11: ( I . v = <*x1,y1*> & I . w = <*x2,y2*> ) by A1;
A12: I . (v + w) = I . ((x1 + x2),(y1 + y2)) by A9, A10, Def1
.= <*(x1 + x2),(y1 + y2)*> by A1 ;
A13: ( <*x1,y1*> . 1 = x1 & <*x2,y2*> . 1 = x2 & <*x1,y1*> . 2 = y1 & <*x2,y2*> . 2 = y2 ) by FINSEQ_1:44;
reconsider Iv = I . v, Iw = I . w as Element of product (carr <*X,Y*>) ;
reconsider j1 = 1, j2 = 2 as Element of dom (carr <*X,Y*>) by A3, TARSKI:def_2;
A14: (addop <*X,Y*>) . j1 = the addF of (<*X,Y*> . j1) by PRVECT_2:def_5;
A15: ([:(addop <*X,Y*>):] . (Iv,Iw)) . j1 = ((addop <*X,Y*>) . j1) . ((Iv . j1),(Iw . j1)) by PRVECT_1:def_8
.= x1 + x2 by A14, A11, A13, FINSEQ_1:44 ;
A16: (addop <*X,Y*>) . j2 = the addF of (<*X,Y*> . j2) by PRVECT_2:def_5;
A17: ([:(addop <*X,Y*>):] . (Iv,Iw)) . j2 = ((addop <*X,Y*>) . j2) . ((Iv . j2),(Iw . j2)) by PRVECT_1:def_8
.= y1 + y2 by A16, A11, A13, FINSEQ_1:44 ;
consider Ivw being Function such that
A18: ( (I . v) + (I . w) = Ivw & dom Ivw = dom (carr <*X,Y*>) & ( for i being set st i in dom (carr <*X,Y*>) holds
Ivw . i in (carr <*X,Y*>) . i ) ) by CARD_3:def_5;
A19: dom Ivw = Seg 2 by A2, A18, FINSEQ_1:def_3;
then reconsider Ivw = Ivw as FinSequence by FINSEQ_1:def_2;
len Ivw = 2 by A19, FINSEQ_1:def_3;
hence I . (v + w) = (I . v) + (I . w) by A12, A18, A15, A17, FINSEQ_1:44; ::_thesis: verum
end;
A20: for v being Point of [:X,Y:]
for r being Element of REAL holds I . (r * v) = r * (I . v)
proof
let v be Point of [:X,Y:]; ::_thesis: for r being Element of REAL holds I . (r * v) = r * (I . v)
let r be Element of REAL ; ::_thesis: I . (r * v) = r * (I . v)
consider x1 being Point of X, y1 being Point of Y such that
A21: v = [x1,y1] by Lm1;
A22: I . v = I . (x1,y1) by A21
.= <*x1,y1*> by A1 ;
A23: I . (r * v) = I . ((r * x1),(r * y1)) by A21, Def2
.= <*(r * x1),(r * y1)*> by A1 ;
A24: ( <*x1,y1*> . 1 = x1 & <*x1,y1*> . 2 = y1 ) by FINSEQ_1:44;
reconsider j1 = 1, j2 = 2 as Element of dom (carr <*X,Y*>) by A3, TARSKI:def_2;
A25: ( (multop <*X,Y*>) . j1 = the Mult of (<*X,Y*> . j1) & (multop <*X,Y*>) . j2 = the Mult of (<*X,Y*> . j2) ) by PRVECT_2:def_8;
reconsider Iv = I . v as Element of product (carr <*X,Y*>) ;
( ([:(multop <*X,Y*>):] . (r,Iv)) . j1 = ((multop <*X,Y*>) . j1) . (r,(Iv . j1)) & ([:(multop <*X,Y*>):] . (r,Iv)) . j2 = ((multop <*X,Y*>) . j2) . (r,(Iv . j2)) ) by PRVECT_2:def_2;
then A26: ( ([:(multop <*X,Y*>):] . (r,Iv)) . j1 = r * x1 & ([:(multop <*X,Y*>):] . (r,Iv)) . j2 = r * y1 ) by A25, A22, A24, FINSEQ_1:44;
consider Ivw being Function such that
A27: ( r * (I . v) = Ivw & dom Ivw = dom (carr <*X,Y*>) & ( for i being set st i in dom (carr <*X,Y*>) holds
Ivw . i in (carr <*X,Y*>) . i ) ) by CARD_3:def_5;
A28: dom Ivw = Seg 2 by A2, A27, FINSEQ_1:def_3;
then reconsider Ivw = Ivw as FinSequence by FINSEQ_1:def_2;
len Ivw = 2 by A28, FINSEQ_1:def_3;
hence I . (r * v) = r * (I . v) by A23, A27, A26, FINSEQ_1:44; ::_thesis: verum
end;
I . (0. [:X,Y:]) = I . ((0. [:X,Y:]) + (0. [:X,Y:])) by RLVECT_1:def_4
.= (I . (0. [:X,Y:])) + (I . (0. [:X,Y:])) by A8 ;
then (I . (0. [:X,Y:])) - (I . (0. [:X,Y:])) = (I . (0. [:X,Y:])) + ((I . (0. [:X,Y:])) - (I . (0. [:X,Y:]))) by RLVECT_1:28
.= (I . (0. [:X,Y:])) + (0. (product <*X,Y*>)) by RLVECT_1:15
.= I . (0. [:X,Y:]) by RLVECT_1:def_4 ;
then 0. (product <*X,Y*>) = I . (0. [:X,Y:]) by RLVECT_1:15;
hence 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 Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. [:X,Y:]) = 0. (product <*X,Y*>) ) by A7, A8, A20, A1, A6; ::_thesis: verum
end;
Lm2: for X being non empty non-empty FinSequence
for x being set st x in product X holds
x is FinSequence
proof
let X be non empty non-empty FinSequence; ::_thesis: for x being set st x in product X holds
x is FinSequence
let x be set ; ::_thesis: ( x in product X implies x is FinSequence )
assume x in product X ; ::_thesis: x is FinSequence
then consider g being Function such that
A1: ( x = g & dom g = dom X & ( for i being set st i in dom X holds
g . i in X . i ) ) by CARD_3:def_5;
dom g = Seg (len X) by A1, FINSEQ_1:def_3;
hence x is FinSequence by A1, FINSEQ_1:def_2; ::_thesis: verum
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)) )
proof
let X, Y be RealLinearSpace-Sequence; ::_thesis: 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)) )
reconsider CX = carr X, CY = carr Y as non empty non-empty FinSequence ;
A1: ( len CX = len X & len CY = len Y & len (carr (X ^ Y)) = len (X ^ Y) ) by PRVECT_2:def_4;
consider I being Function of [:(product CX),(product CY):],(product (CX ^ CY)) such that
A2: ( I is one-to-one & I is onto & ( for x, y being FinSequence st x in product CX & y in product CY holds
I . (x,y) = x ^ y ) ) by Th6;
set PX = product X;
set PY = product Y;
( len (carr (X ^ Y)) = (len X) + (len Y) & len (CX ^ CY) = (len X) + (len Y) ) by A1, FINSEQ_1:22;
then A3: dom (carr (X ^ Y)) = dom (CX ^ CY) by FINSEQ_3:29;
A4: for k being Nat st k in dom (carr (X ^ Y)) holds
(carr (X ^ Y)) . k = (CX ^ CY) . k
proof
let k be Nat; ::_thesis: ( k in dom (carr (X ^ Y)) implies (carr (X ^ Y)) . k = (CX ^ CY) . k )
assume A5: k in dom (carr (X ^ Y)) ; ::_thesis: (carr (X ^ Y)) . k = (CX ^ CY) . k
then reconsider k1 = k as Element of dom (X ^ Y) by A1, FINSEQ_3:29;
A6: (carr (X ^ Y)) . k = the carrier of ((X ^ Y) . k1) by PRVECT_2:def_4;
A7: k in dom (X ^ Y) by A1, A5, FINSEQ_3:29;
percases ( k in dom X or ex n being Nat st
( n in dom Y & k = (len X) + n ) ) by A7, FINSEQ_1:25;
supposeA8: k in dom X ; ::_thesis: (carr (X ^ Y)) . k = (CX ^ CY) . k
then A9: k in dom CX by A1, FINSEQ_3:29;
reconsider k2 = k1 as Element of dom X by A8;
thus (carr (X ^ Y)) . k = the carrier of (X . k2) by A6, FINSEQ_1:def_7
.= CX . k by PRVECT_2:def_4
.= (CX ^ CY) . k by A9, FINSEQ_1:def_7 ; ::_thesis: verum
end;
suppose ex n being Nat st
( n in dom Y & k = (len X) + n ) ; ::_thesis: (carr (X ^ Y)) . k = (CX ^ CY) . k
then consider n being Nat such that
A10: ( n in dom Y & k = (len X) + n ) ;
A11: n in dom CY by A1, A10, FINSEQ_3:29;
reconsider n1 = n as Element of dom Y by A10;
thus (carr (X ^ Y)) . k = the carrier of (Y . n1) by A6, A10, FINSEQ_1:def_7
.= CY . n by PRVECT_2:def_4
.= (CX ^ CY) . k by A11, A10, A1, FINSEQ_1:def_7 ; ::_thesis: verum
end;
end;
end;
then A12: carr (X ^ Y) = CX ^ CY by A3, FINSEQ_1:13;
reconsider I = I as Function of [:(product X),(product Y):],(product (X ^ Y)) by A3, A4, FINSEQ_1:13;
A13: 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 )
proof
let x be Point of (product X); ::_thesis: for y being Point of (product Y) ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 )
let y be Point of (product Y); ::_thesis: ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 )
reconsider x1 = x, y1 = y as FinSequence by Lm2;
I . (x,y) = x1 ^ y1 by A2;
hence ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 ) ; ::_thesis: verum
end;
A14: for v, w being Point of [:(product X),(product Y):] holds I . (v + w) = (I . v) + (I . w)
proof
let v, w be Point of [:(product X),(product Y):]; ::_thesis: I . (v + w) = (I . v) + (I . w)
consider x1 being Point of (product X), y1 being Point of (product Y) such that
A15: v = [x1,y1] by Lm1;
consider x2 being Point of (product X), y2 being Point of (product Y) such that
A16: w = [x2,y2] by Lm1;
reconsider xx1 = x1, xx2 = x2 as FinSequence by Lm2;
reconsider yy1 = y1, yy2 = y2 as FinSequence by Lm2;
reconsider xx12 = x1 + x2, yy12 = y1 + y2 as FinSequence by Lm2;
A17: ( dom xx1 = dom CX & dom xx2 = dom CX & dom xx12 = dom CX & dom yy1 = dom CY & dom yy2 = dom CY & dom yy12 = dom CY ) by CARD_3:9;
( I . v = I . (x1,y1) & I . w = I . (x2,y2) ) by A15, A16;
then A18: ( I . v = xx1 ^ yy1 & I . w = xx2 ^ yy2 ) by A2;
I . (v + w) = I . ((x1 + x2),(y1 + y2)) by A15, A16, Def1;
then A19: I . (v + w) = xx12 ^ yy12 by A2;
then A20: dom (xx12 ^ yy12) = dom (carr (X ^ Y)) by CARD_3:9;
reconsider Iv = I . v, Iw = I . w as Element of product (carr (X ^ Y)) ;
reconsider Ivw = (I . v) + (I . w) as FinSequence by Lm2;
A21: dom Ivw = dom (carr (X ^ Y)) by CARD_3:9;
for j0 being Nat st j0 in dom Ivw holds
Ivw . j0 = (xx12 ^ yy12) . j0
proof
let j0 be Nat; ::_thesis: ( j0 in dom Ivw implies Ivw . j0 = (xx12 ^ yy12) . j0 )
assume j0 in dom Ivw ; ::_thesis: Ivw . j0 = (xx12 ^ yy12) . j0
then reconsider j = j0 as Element of dom (carr (X ^ Y)) by CARD_3:9;
A22: Ivw . j0 = ((addop (X ^ Y)) . j) . ((Iv . j),(Iw . j)) by PRVECT_1:def_8
.= the addF of ((X ^ Y) . j) . ((Iv . j),(Iw . j)) by PRVECT_2:def_5 ;
percases ( j0 in dom CX or ex n being Nat st
( n in dom CY & j0 = (len CX) + n ) ) by A22, A3, FINSEQ_1:25;
supposeA23: j0 in dom CX ; ::_thesis: Ivw . j0 = (xx12 ^ yy12) . j0
then j0 in dom X by A1, FINSEQ_3:29;
then A24: (X ^ Y) . j = X . j0 by FINSEQ_1:def_7;
A25: ( Iv . j = xx1 . j & Iw . j = xx2 . j ) by A23, A17, A18, FINSEQ_1:def_7;
A26: (xx12 ^ yy12) . j0 = xx12 . j0 by A23, A17, FINSEQ_1:def_7;
reconsider j1 = j0 as Element of dom (carr X) by A23;
the addF of ((X ^ Y) . j) . ((Iv . j),(Iw . j)) = ((addop X) . j1) . ((xx1 . j1),(xx2 . j1)) by A24, A25, PRVECT_2:def_5
.= (xx12 ^ yy12) . j0 by A26, PRVECT_1:def_8 ;
hence Ivw . j0 = (xx12 ^ yy12) . j0 by A22; ::_thesis: verum
end;
suppose ex n being Nat st
( n in dom CY & j0 = (len CX) + n ) ; ::_thesis: Ivw . j0 = (xx12 ^ yy12) . j0
then consider n being Nat such that
A27: ( n in dom CY & j0 = (len CX) + n ) ;
A28: ( len CX = len xx1 & len CX = len xx2 & len CX = len xx12 ) by A17, FINSEQ_3:29;
n in dom Y by A1, A27, FINSEQ_3:29;
then A29: (X ^ Y) . j = Y . n by A27, A1, FINSEQ_1:def_7;
A30: ( Iv . j = yy1 . n & Iw . j = yy2 . n ) by A17, A18, A27, A28, FINSEQ_1:def_7;
A31: (xx12 ^ yy12) . j0 = yy12 . n by A27, A28, A17, FINSEQ_1:def_7;
reconsider j1 = n as Element of dom (carr Y) by A27;
the addF of ((X ^ Y) . j) . ((Iv . j),(Iw . j)) = ((addop Y) . j1) . ((yy1 . j1),(yy2 . j1)) by A29, A30, PRVECT_2:def_5
.= (xx12 ^ yy12) . j0 by A31, PRVECT_1:def_8 ;
hence Ivw . j0 = (xx12 ^ yy12) . j0 by A22; ::_thesis: verum
end;
end;
end;
hence I . (v + w) = (I . v) + (I . w) by A19, A20, A21, FINSEQ_1:13; ::_thesis: verum
end;
A32: for v being Point of [:(product X),(product Y):]
for r being Element of REAL holds I . (r * v) = r * (I . v)
proof
let v be Point of [:(product X),(product Y):]; ::_thesis: for r being Element of REAL holds I . (r * v) = r * (I . v)
let r be Element of REAL ; ::_thesis: I . (r * v) = r * (I . v)
consider x1 being Point of (product X), y1 being Point of (product Y) such that
A33: v = [x1,y1] by Lm1;
reconsider xx1 = x1, yy1 = y1 as FinSequence by Lm2;
reconsider rxx1 = r * x1, ryy1 = r * y1 as FinSequence by Lm2;
A34: ( dom xx1 = dom CX & dom yy1 = dom CY & dom rxx1 = dom CX & dom ryy1 = dom CY ) by CARD_3:9;
A35: I . v = I . (x1,y1) by A33
.= xx1 ^ yy1 by A2 ;
A36: I . (r * v) = I . ((r * x1),(r * y1)) by A33, Def2
.= rxx1 ^ ryy1 by A2 ;
reconsider Iv = I . v as Element of product (carr (X ^ Y)) ;
reconsider rIv = r * (I . v) as FinSequence by Lm2;
A37: dom rIv = dom (carr (X ^ Y)) by CARD_3:9;
A38: dom (rxx1 ^ ryy1) = dom (carr (X ^ Y)) by A36, CARD_3:9;
for j0 being Nat st j0 in dom rIv holds
rIv . j0 = (rxx1 ^ ryy1) . j0
proof
let j0 be Nat; ::_thesis: ( j0 in dom rIv implies rIv . j0 = (rxx1 ^ ryy1) . j0 )
assume A39: j0 in dom rIv ; ::_thesis: rIv . j0 = (rxx1 ^ ryy1) . j0
then reconsider j = j0 as Element of dom (carr (X ^ Y)) by CARD_3:9;
A40: rIv . j0 = ((multop (X ^ Y)) . j) . (r,(Iv . j)) by PRVECT_2:def_2
.= the Mult of ((X ^ Y) . j) . (r,(Iv . j)) by PRVECT_2:def_8 ;
percases ( j0 in dom CX or ex n being Nat st
( n in dom CY & j0 = (len CX) + n ) ) by A3, A39, A37, FINSEQ_1:25;
supposeA41: j0 in dom CX ; ::_thesis: rIv . j0 = (rxx1 ^ ryy1) . j0
then j0 in dom X by A1, FINSEQ_3:29;
then A42: (X ^ Y) . j = X . j0 by FINSEQ_1:def_7;
A43: Iv . j = xx1 . j by A41, A34, A35, FINSEQ_1:def_7;
A44: (rxx1 ^ ryy1) . j0 = rxx1 . j0 by A41, A34, FINSEQ_1:def_7;
reconsider j1 = j0 as Element of dom (carr X) by A41;
the Mult of ((X ^ Y) . j) . (r,(Iv . j)) = ((multop X) . j1) . (r,(xx1 . j1)) by A42, A43, PRVECT_2:def_8
.= (rxx1 ^ ryy1) . j0 by A44, PRVECT_2:def_2 ;
hence rIv . j0 = (rxx1 ^ ryy1) . j0 by A40; ::_thesis: verum
end;
suppose ex n being Nat st
( n in dom CY & j0 = (len CX) + n ) ; ::_thesis: rIv . j0 = (rxx1 ^ ryy1) . j0
then consider n being Nat such that
A45: ( n in dom CY & j0 = (len CX) + n ) ;
A46: ( len CX = len xx1 & len CX = len rxx1 ) by A34, FINSEQ_3:29;
n in dom Y by A45, A1, FINSEQ_3:29;
then A47: (X ^ Y) . j = Y . n by A45, A1, FINSEQ_1:def_7;
A48: Iv . j = yy1 . n by A35, A45, A34, A46, FINSEQ_1:def_7;
A49: (rxx1 ^ ryy1) . j0 = ryy1 . n by A45, A46, A34, FINSEQ_1:def_7;
reconsider j1 = n as Element of dom (carr Y) by A45;
the Mult of ((X ^ Y) . j) . (r,(Iv . j)) = ((multop Y) . j1) . (r,(yy1 . j1)) by A47, A48, PRVECT_2:def_8
.= (rxx1 ^ ryy1) . j0 by A49, PRVECT_2:def_2 ;
hence rIv . j0 = (rxx1 ^ ryy1) . j0 by A40; ::_thesis: verum
end;
end;
end;
hence I . (r * v) = r * (I . v) by A36, A38, A37, FINSEQ_1:13; ::_thesis: verum
end;
I . (0. [:(product X),(product Y):]) = I . ((0. [:(product X),(product Y):]) + (0. [:(product X),(product Y):])) by RLVECT_1:def_4
.= (I . (0. [:(product X),(product Y):])) + (I . (0. [:(product X),(product Y):])) by A14 ;
then (I . (0. [:(product X),(product Y):])) - (I . (0. [:(product X),(product Y):])) = (I . (0. [:(product X),(product Y):])) + ((I . (0. [:(product X),(product Y):])) - (I . (0. [:(product X),(product Y):]))) by RLVECT_1:28
.= (I . (0. [:(product X),(product Y):])) + (0. (product (X ^ Y))) by RLVECT_1:15
.= I . (0. [:(product X),(product Y):]) by RLVECT_1:def_4 ;
then 0. (product (X ^ Y)) = I . (0. [:(product X),(product Y):]) by RLVECT_1:15;
hence 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)) ) by A13, A14, A32, A2, A12; ::_thesis: verum
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 number st x = <*x1,x2*> holds
a * x = <*(a * x1),(a * x2)*> ) )
proof
let G, F be RealLinearSpace; ::_thesis: ( ( 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 number st x = <*x1,x2*> holds
a * x = <*(a * x1),(a * x2)*> ) )
consider I being Function of [:G,F:],(product <*G,F*>) such that
A1: ( I is one-to-one & I is onto & ( for x being Point of G
for y being Point of F holds I . (x,y) = <*x,y*> ) & ( for v, w being Point of [:G,F:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:G,F:]
for r being Element of REAL holds I . (r * v) = r * (I . v) ) & 0. (product <*G,F*>) = I . (0. [:G,F:]) ) by Th12;
thus A2: 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*> ) ::_thesis: ( ( 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 number st x = <*x1,x2*> holds
a * x = <*(a * x1),(a * x2)*> ) )
proof
let y be set ; ::_thesis: ( y is Point of (product <*G,F*>) iff ex x1 being Point of G ex x2 being Point of F st y = <*x1,x2*> )
hereby ::_thesis: ( ex x1 being Point of G ex x2 being Point of F st y = <*x1,x2*> implies y is Point of (product <*G,F*>) )
assume y is Point of (product <*G,F*>) ; ::_thesis: ex x1 being Point of G ex x2 being Point of F st y = <*x1,x2*>
then y in the carrier of (product <*G,F*>) ;
then y in rng I by A1, FUNCT_2:def_3;
then consider x being Element of the carrier of [:G,F:] such that
A3: y = I . x by FUNCT_2:113;
consider x1 being Point of G, x2 being Point of F such that
A4: x = [x1,x2] by Lm1;
take x1 = x1; ::_thesis: ex x2 being Point of F st y = <*x1,x2*>
take x2 = x2; ::_thesis: y = <*x1,x2*>
I . (x1,x2) = <*x1,x2*> by A1;
hence y = <*x1,x2*> by A3, A4; ::_thesis: verum
end;
now__::_thesis:_(_ex_x1_being_Point_of_G_ex_x2_being_Point_of_F_st_y_=_<*x1,x2*>_implies_y_is_Point_of_(product_<*G,F*>)_)
assume ex x1 being Point of G ex x2 being Point of F st y = <*x1,x2*> ; ::_thesis: y is Point of (product <*G,F*>)
then consider x1 being Point of G, x2 being Point of F such that
A5: y = <*x1,x2*> ;
A6: I . [x1,x2] in rng I by FUNCT_2:112;
I . (x1,x2) = <*x1,x2*> by A1;
hence y is Point of (product <*G,F*>) by A5, A6; ::_thesis: verum
end;
hence ( ex x1 being Point of G ex x2 being Point of F st y = <*x1,x2*> implies y is Point of (product <*G,F*>) ) ; ::_thesis: verum
end;
thus A7: 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)*> ::_thesis: ( 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 number st x = <*x1,x2*> holds
a * x = <*(a * x1),(a * x2)*> ) )
proof
let x, y be Point of (product <*G,F*>); ::_thesis: 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)*>
let x1, y1 be Point of G; ::_thesis: for x2, y2 being Point of F st x = <*x1,x2*> & y = <*y1,y2*> holds
x + y = <*(x1 + y1),(x2 + y2)*>
let x2, y2 be Point of F; ::_thesis: ( x = <*x1,x2*> & y = <*y1,y2*> implies x + y = <*(x1 + y1),(x2 + y2)*> )
assume A8: ( x = <*x1,x2*> & y = <*y1,y2*> ) ; ::_thesis: x + y = <*(x1 + y1),(x2 + y2)*>
reconsider z = [x1,x2], w = [y1,y2] as Point of [:G,F:] ;
A9: z + w = [(x1 + y1),(x2 + y2)] by Def1;
( I . ((x1 + y1),(x2 + y2)) = <*(x1 + y1),(x2 + y2)*> & I . (x1,x2) = <*x1,x2*> & I . (y1,y2) = <*y1,y2*> ) by A1;
hence <*(x1 + y1),(x2 + y2)*> = x + y by A1, A9, A8; ::_thesis: verum
end;
thus A10: 0. (product <*G,F*>) = <*(0. G),(0. F)*> ::_thesis: ( ( 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 number st x = <*x1,x2*> holds
a * x = <*(a * x1),(a * x2)*> ) )
proof
I . ((0. G),(0. F)) = <*(0. G),(0. F)*> by A1;
hence 0. (product <*G,F*>) = <*(0. G),(0. F)*> by A1; ::_thesis: verum
end;
thus 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)*> ::_thesis: for x being Point of (product <*G,F*>)
for x1 being Point of G
for x2 being Point of F
for a being real number st x = <*x1,x2*> holds
a * x = <*(a * x1),(a * x2)*>
proof
let x be Point of (product <*G,F*>); ::_thesis: for x1 being Point of G
for x2 being Point of F st x = <*x1,x2*> holds
- x = <*(- x1),(- x2)*>
let x1 be Point of G; ::_thesis: for x2 being Point of F st x = <*x1,x2*> holds
- x = <*(- x1),(- x2)*>
let x2 be Point of F; ::_thesis: ( x = <*x1,x2*> implies - x = <*(- x1),(- x2)*> )
assume A11: x = <*x1,x2*> ; ::_thesis: - x = <*(- x1),(- x2)*>
reconsider y = <*(- x1),(- x2)*> as Point of (product <*G,F*>) by A2;
x + y = <*(x1 + (- x1)),(x2 + (- x2))*> by A7, A11
.= <*(0. G),(x2 + (- x2))*> by RLVECT_1:def_10
.= 0. (product <*G,F*>) by A10, RLVECT_1:def_10 ;
hence - x = <*(- x1),(- x2)*> by RLVECT_1:def_10; ::_thesis: verum
end;
thus for x being Point of (product <*G,F*>)
for x1 being Point of G
for x2 being Point of F
for a being real number st x = <*x1,x2*> holds
a * x = <*(a * x1),(a * x2)*> ::_thesis: verum
proof
let x be Point of (product <*G,F*>); ::_thesis: for x1 being Point of G
for x2 being Point of F
for a being real number st x = <*x1,x2*> holds
a * x = <*(a * x1),(a * x2)*>
let x1 be Point of G; ::_thesis: for x2 being Point of F
for a being real number st x = <*x1,x2*> holds
a * x = <*(a * x1),(a * x2)*>
let x2 be Point of F; ::_thesis: for a being real number st x = <*x1,x2*> holds
a * x = <*(a * x1),(a * x2)*>
let a be real number ; ::_thesis: ( x = <*x1,x2*> implies a * x = <*(a * x1),(a * x2)*> )
assume A12: x = <*x1,x2*> ; ::_thesis: a * x = <*(a * x1),(a * x2)*>
reconsider a0 = a as Element of REAL by XREAL_0:def_1;
reconsider y = [x1,x2] as Point of [:G,F:] ;
A13: <*x1,x2*> = I . (x1,x2) by A1;
I . (a * y) = I . ((a0 * x1),(a0 * x2)) by Th9
.= <*(a0 * x1),(a0 * x2)*> by A1 ;
hence a * x = <*(a * x1),(a * x2)*> by A1, A12, A13; ::_thesis: verum
end;
end;
begin
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 :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
ex b1 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.||*> & b1 . (g,f) = |.v.| )
proof
defpred S1[ set , set , set ] means ex g being Point of G ex f being Point of F ex v being Element of REAL 2 st
( $1 = g & $2 = f & v = <*||.g.||,||.f.||*> & $3 = |.v.| );
A1: for x, y being set st x in the carrier of G & y in the carrier of F holds
ex z being set st
( z in REAL & S1[x,y,z] )
proof
let x, y be set ; ::_thesis: ( x in the carrier of G & y in the carrier of F implies ex z being set st
( z in REAL & S1[x,y,z] ) )
assume A2: ( x in the carrier of G & y in the carrier of F ) ; ::_thesis: ex z being set st
( z in REAL & S1[x,y,z] )
then reconsider g = x as Point of G ;
reconsider f = y as Point of F by A2;
reconsider v = <*||.g.||,||.f.||*> as Element of REAL 2 by FINSEQ_2:101;
|.v.| in REAL ;
hence ex z being set st
( z in REAL & S1[x,y,z] ) ; ::_thesis: verum
end;
consider NORMGF being Function of [: the carrier of G, the carrier of F:],REAL such that
A3: for x, y being set st x in the carrier of G & y in the carrier of F holds
S1[x,y,NORMGF . (x,y)] from BINOP_1:sch_1(A1);
now__::_thesis:_for_g_being_Point_of_G
for_f_being_Point_of_F_ex_v_being_Element_of_REAL_2_st_
(_v_=_<*||.g.||,||.f.||*>_&_NORMGF_._(g,f)_=_|.v.|_)
let g be Point of G; ::_thesis: for f being Point of F ex v being Element of REAL 2 st
( v = <*||.g.||,||.f.||*> & NORMGF . (g,f) = |.v.| )
let f be Point of F; ::_thesis: ex v being Element of REAL 2 st
( v = <*||.g.||,||.f.||*> & NORMGF . (g,f) = |.v.| )
ex gg being Point of G ex ff being Point of F ex v being Element of REAL 2 st
( g = gg & f = ff & v = <*||.gg.||,||.ff.||*> & NORMGF . (g,f) = |.v.| ) by A3;
hence ex v being Element of REAL 2 st
( v = <*||.g.||,||.f.||*> & NORMGF . (g,f) = |.v.| ) ; ::_thesis: verum
end;
hence ex b1 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.||*> & b1 . (g,f) = |.v.| ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 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.||*> & b1 . (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.||*> & b2 . (g,f) = |.v.| ) ) holds
b1 = b2
proof
let H1, H2 be Function of [: the carrier of G, the carrier of F:],REAL; ::_thesis: ( ( for g being Point of G
for f being Point of F ex v being Element of REAL 2 st
( v = <*||.g.||,||.f.||*> & H1 . (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.||*> & H2 . (g,f) = |.v.| ) ) implies H1 = H2 )
assume A4: for g being Point of G
for f being Point of F ex v being Element of REAL 2 st
( v = <*||.g.||,||.f.||*> & H1 . (g,f) = |.v.| ) ; ::_thesis: ( ex g being Point of G ex f being Point of F st
for v being Element of REAL 2 holds
( not v = <*||.g.||,||.f.||*> or not H2 . (g,f) = |.v.| ) or H1 = H2 )
assume A5: for g being Point of G
for f being Point of F ex v being Element of REAL 2 st
( v = <*||.g.||,||.f.||*> & H2 . (g,f) = |.v.| ) ; ::_thesis: H1 = H2
now__::_thesis:_for_g_being_Element_of_the_carrier_of_G
for_f_being_Element_of_the_carrier_of_F_holds_H1_._(g,f)_=_H2_._(g,f)
let g be Element of the carrier of G; ::_thesis: for f being Element of the carrier of F holds H1 . (g,f) = H2 . (g,f)
let f be Element of the carrier of F; ::_thesis: H1 . (g,f) = H2 . (g,f)
A6: ex v1 being Element of REAL 2 st
( v1 = <*||.g.||,||.f.||*> & H1 . (g,f) = |.v1.| ) by A4;
ex v2 being Element of REAL 2 st
( v2 = <*||.g.||,||.f.||*> & H2 . (g,f) = |.v2.| ) by A5;
hence H1 . (g,f) = H2 . (g,f) by A6; ::_thesis: verum
end;
hence H1 = H2 by BINOP_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines prod_NORM PRVECT_3:def_6_:_
for G, F being non empty NORMSTR
for b3 being Function of [: the carrier of G, the carrier of F:],REAL holds
( b3 = 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.||*> & b3 . (g,f) = |.v.| ) );
definition
let G, F be non empty NORMSTR ;
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
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;
:: 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)) #);
registration
let G, F be RealNormSpace;
cluster[:G,F:] -> non empty discerning reflexive strict RealNormSpace-like ;
correctness
coherence
( [:G,F:] is reflexive & [:G,F:] is discerning & [:G,F:] is RealNormSpace-like );
proof
now__::_thesis:_for_x_being_Point_of_[:G,F:]_st_x_=_0._[:G,F:]_holds_
||.x.||_=_0
let x be Point of [:G,F:]; ::_thesis: ( x = 0. [:G,F:] implies ||.x.|| = 0 )
consider x1 being Point of G, x2 being Point of F such that
A1: x = [x1,x2] by Lm1;
consider v being Element of REAL 2 such that
A2: ( v = <*||.x1.||,||.x2.||*> & (prod_NORM (G,F)) . (x1,x2) = |.v.| ) by Def6;
assume x = 0. [:G,F:] ; ::_thesis: ||.x.|| = 0
then ( x1 = 0. G & x2 = 0. F ) by A1, XTUPLE_0:1;
then ( ||.x1.|| = 0 & ||.x2.|| = 0 ) ;
then v = 0* 2 by A2, FINSEQ_2:61;
hence ||.x.|| = 0 by A2, A1, EUCLID:7; ::_thesis: verum
end;
then ||.(0. [:G,F:]).|| = 0 ;
hence [:G,F:] is reflexive by NORMSP_0:def_6; ::_thesis: ( [:G,F:] is discerning & [:G,F:] is RealNormSpace-like )
now__::_thesis:_for_x_being_Point_of_[:G,F:]_st_||.x.||_=_0_holds_
x_=_0._[:G,F:]
let x be Point of [:G,F:]; ::_thesis: ( ||.x.|| = 0 implies x = 0. [:G,F:] )
consider x1 being Point of G, x2 being Point of F such that
A3: x = [x1,x2] by Lm1;
consider v being Element of REAL 2 such that
A4: ( v = <*||.x1.||,||.x2.||*> & (prod_NORM (G,F)) . (x1,x2) = |.v.| ) by Def6;
assume ||.x.|| = 0 ; ::_thesis: x = 0. [:G,F:]
then v = 0* 2 by A4, A3, EUCLID:8;
then A5: v = <*0,0*> by FINSEQ_2:61;
( ||.x1.|| = v . 1 & ||.x2.|| = v . 2 ) by A4, FINSEQ_1:44;
then ( ||.x1.|| = 0 & ||.x2.|| = 0 ) by A5, FINSEQ_1:44;
then ( x1 = 0. G & x2 = 0. F ) by NORMSP_0:def_5;
hence x = 0. [:G,F:] by A3; ::_thesis: verum
end;
hence [:G,F:] is discerning by NORMSP_0:def_5; ::_thesis: [:G,F:] is RealNormSpace-like
now__::_thesis:_for_x,_y_being_Point_of_[:G,F:]
for_a_being_Real_holds_
(_||.(a_*_x).||_=_(abs_a)_*_||.x.||_&_||.(x_+_y).||_<=_||.x.||_+_||.y.||_)
let x, y be Point of [:G,F:]; ::_thesis: for a being Real holds
( ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )
let a be Real; ::_thesis: ( ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )
consider x1 being Point of G, x2 being Point of F such that
A6: x = [x1,x2] by Lm1;
consider y1 being Point of G, y2 being Point of F such that
A7: y = [y1,y2] by Lm1;
consider v being Element of REAL 2 such that
A8: ( v = <*||.x1.||,||.x2.||*> & (prod_NORM (G,F)) . (x1,x2) = |.v.| ) by Def6;
consider z being Element of REAL 2 such that
A9: ( z = <*||.y1.||,||.y2.||*> & (prod_NORM (G,F)) . (y1,y2) = |.z.| ) by Def6;
thus ||.(a * x).|| = (abs a) * ||.x.|| ::_thesis: ||.(x + y).|| <= ||.x.|| + ||.y.||
proof
consider w being Element of REAL 2 such that
A10: ( w = <*||.(a * x1).||,||.(a * x2).||*> & (prod_NORM (G,F)) . ((a * x1),(a * x2)) = |.w.| ) by Def6;
reconsider aa = abs a, xx1 = ||.x1.||, xx2 = ||.x2.|| as real number ;
( ||.(a * x1).|| = (abs a) * ||.x1.|| & ||.(a * x2).|| = (abs a) * ||.x2.|| ) by NORMSP_1:def_1;
then w = aa * |[xx1,xx2]| by A10, EUCLID:58
.= (abs a) * v by A8, EUCLID:65 ;
then |.w.| = (abs (abs a)) * |.v.| by EUCLID:11
.= (abs a) * |.v.| ;
hence ||.(a * x).|| = (abs a) * ||.x.|| by A8, A10, A6, Def2; ::_thesis: verum
end;
thus ||.(x + y).|| <= ||.x.|| + ||.y.|| ::_thesis: verum
proof
consider w being Element of REAL 2 such that
A11: ( w = <*||.(x1 + y1).||,||.(x2 + y2).||*> & (prod_NORM (G,F)) . ((x1 + y1),(x2 + y2)) = |.w.| ) by Def6;
A12: ||.(x + y).|| = |.w.| by A11, A6, A7, Def1;
A13: ( ||.(x1 + y1).|| <= ||.x1.|| + ||.y1.|| & ||.(x2 + y2).|| <= ||.x2.|| + ||.y2.|| ) by NORMSP_1:def_1;
set t = <*(||.x1.|| + ||.y1.||),(||.x2.|| + ||.y2.||)*>;
reconsider t = <*(||.x1.|| + ||.y1.||),(||.x2.|| + ||.y2.||)*> as FinSequence of REAL ;
A14: ( len w = 2 & len t = 2 ) by A11, FINSEQ_1:44;
now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_Seg_(len_w)_holds_
(_0_<=_w_._i_&_w_._i_<=_t_._i_)
let i be Element of NAT ; ::_thesis: ( i in Seg (len w) implies ( 0 <= w . b1 & w . b1 <= t . b1 ) )
assume i in Seg (len w) ; ::_thesis: ( 0 <= w . b1 & w . b1 <= t . b1 )
then A15: i in Seg 2 by A11, FINSEQ_1:44;
percases ( i = 1 or i = 2 ) by A15, FINSEQ_1:2, TARSKI:def_2;
supposeA16: i = 1 ; ::_thesis: ( 0 <= w . b1 & w . b1 <= t . b1 )
then w . i = ||.(x1 + y1).|| by A11, FINSEQ_1:44;
hence ( 0 <= w . i & w . i <= t . i ) by A13, A16, FINSEQ_1:44, NORMSP_1:4; ::_thesis: verum
end;
supposeA17: i = 2 ; ::_thesis: ( 0 <= w . b1 & w . b1 <= t . b1 )
then w . i = ||.(x2 + y2).|| by A11, FINSEQ_1:44;
hence ( 0 <= w . i & w . i <= t . i ) by A13, A17, FINSEQ_1:44, NORMSP_1:4; ::_thesis: verum
end;
end;
end;
then A18: |.w.| <= |.t.| by A14, PRVECT_2:2;
t = |[||.x1.||,||.x2.||]| + |[||.y1.||,||.y2.||]| by EUCLID:56
.= v + z by A8, A9, EUCLID:64 ;
then |.t.| <= |.v.| + |.z.| by EUCLID:12;
hence ||.(x + y).|| <= ||.x.|| + ||.y.|| by A12, A6, A8, A7, A9, A18, XXREAL_0:2; ::_thesis: verum
end;
end;
hence [:G,F:] is RealNormSpace-like by NORMSP_1:def_1; ::_thesis: verum
end;
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 ;
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
reconsider G0 = G, F0 = F as RealLinearSpace ;
RLSStruct(# the carrier of [:G,F:], the ZeroF of [:G,F:], the addF of [:G,F:], the Mult of [:G,F:] #) = [:G0,F0:] ;
hence ( [: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 ) by RSSPACE3:2; ::_thesis: verum
end;
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 ;
cluster<*G*> -> RealNormSpace-yielding ;
correctness
coherence
<*G*> is RealNormSpace-yielding ;
proof
let S be set ; :: according to PRVECT_2:def_10 ::_thesis: ( not S in rng <*G*> or S is NORMSTR )
assume S in rng <*G*> ; ::_thesis: S is NORMSTR
then consider i being set such that
A1: ( i in dom <*G*> & <*G*> . i = S ) by FUNCT_1:def_3;
reconsider i = i as Element of NAT by A1;
len <*G*> = 1 by FINSEQ_1:40;
then dom <*G*> = {1} by FINSEQ_1:2, FINSEQ_1:def_3;
then i = 1 by A1, TARSKI:def_1;
hence S is RealNormSpace by A1, FINSEQ_1:40; ::_thesis: verum
end;
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 ;
cluster<*G,F*> -> RealNormSpace-yielding ;
correctness
coherence
<*G,F*> is RealNormSpace-yielding ;
proof
let S be set ; :: according to PRVECT_2:def_10 ::_thesis: ( not S in rng <*G,F*> or S is NORMSTR )
assume S in rng <*G,F*> ; ::_thesis: S is NORMSTR
then consider i being set such that
A1: ( i in dom <*G,F*> & <*G,F*> . i = S ) by FUNCT_1:def_3;
reconsider i = i as Element of NAT by A1;
dom <*G,F*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89;
then ( i = 1 or i = 2 ) by A1, TARSKI:def_2;
hence S is RealNormSpace by A1, FINSEQ_1:44; ::_thesis: verum
end;
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 Element of 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
let X, Y be RealNormSpace; ::_thesis: 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 Element of 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.|| ) )
reconsider X0 = X, Y0 = Y as RealLinearSpace ;
consider I0 being Function of [:X0,Y0:],(product <*X0,Y0*>) such that
A1: ( I0 is one-to-one & I0 is onto & ( for x being Point of X
for y being Point of Y holds I0 . (x,y) = <*x,y*> ) & ( for v, w being Point of [:X0,Y0:] holds I0 . (v + w) = (I0 . v) + (I0 . w) ) & ( for v being Point of [:X0,Y0:]
for r being Element of REAL holds I0 . (r * v) = r * (I0 . v) ) & 0. (product <*X0,Y0*>) = I0 . (0. [:X0,Y0:]) ) by Th12;
A2: product <*X,Y*> = NORMSTR(# (product (carr <*X,Y*>)),(zeros <*X,Y*>),[:(addop <*X,Y*>):],[:(multop <*X,Y*>):],(productnorm <*X,Y*>) #) by PRVECT_2:6;
then reconsider I = I0 as Function of [:X,Y:],(product <*X,Y*>) ;
take I ; ::_thesis: ( 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) ) & 0. (product <*X,Y*>) = I . (0. [:X,Y:]) & ( for v being Point of [:X,Y:] holds ||.(I . v).|| = ||.v.|| ) )
thus ( 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*> ) ) by A1, A2; ::_thesis: ( ( 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) ) & 0. (product <*X,Y*>) = I . (0. [:X,Y:]) & ( for v being Point of [:X,Y:] holds ||.(I . v).|| = ||.v.|| ) )
thus for v, w being Point of [:X,Y:] holds I . (v + w) = (I . v) + (I . w) ::_thesis: ( ( for v being Point of [:X,Y:]
for r being Element of 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
let v, w be Point of [:X,Y:]; ::_thesis: I . (v + w) = (I . v) + (I . w)
reconsider v0 = v, w0 = w as Point of [:X0,Y0:] ;
thus I . (v + w) = I0 . (v0 + w0)
.= (I0 . v0) + (I0 . w0) by A1
.= (I . v) + (I . w) by A2 ; ::_thesis: verum
end;
thus for v being Point of [:X,Y:]
for r being Element of REAL holds I . (r * v) = r * (I . v) ::_thesis: ( 0. (product <*X,Y*>) = I . (0. [:X,Y:]) & ( for v being Point of [:X,Y:] holds ||.(I . v).|| = ||.v.|| ) )
proof
let v be Point of [:X,Y:]; ::_thesis: for r being Element of REAL holds I . (r * v) = r * (I . v)
let r be Element of REAL ; ::_thesis: I . (r * v) = r * (I . v)
reconsider v0 = v as Point of [:X0,Y0:] ;
thus I . (r * v) = I0 . (r * v0)
.= r * (I0 . v0) by A1
.= r * (I . v) by A2 ; ::_thesis: verum
end;
thus 0. (product <*X,Y*>) = I . (0. [:X,Y:]) by A1, A2; ::_thesis: for v being Point of [:X,Y:] holds ||.(I . v).|| = ||.v.||
for v being Point of [:X,Y:] holds ||.(I . v).|| = ||.v.||
proof
let v be Point of [:X,Y:]; ::_thesis: ||.(I . v).|| = ||.v.||
consider x1 being Point of X, y1 being Point of Y such that
A3: v = [x1,y1] by Lm1;
consider v1 being Element of REAL 2 such that
A4: ( v1 = <*||.x1.||,||.y1.||*> & (prod_NORM (X,Y)) . (x1,y1) = |.v1.| ) by Def6;
A5: I . v = I . (x1,y1) by A3
.= <*x1,y1*> by A1 ;
reconsider Iv = I . v as Element of product (carr <*X,Y*>) by A2;
A6: ( <*x1,y1*> . 1 = x1 & <*x1,y1*> . 2 = y1 ) by FINSEQ_1:44;
( 1 in {1,2} & 2 in {1,2} ) by TARSKI:def_2;
then reconsider j1 = 1, j2 = 2 as Element of dom <*X,Y*> by FINSEQ_1:2, FINSEQ_1:89;
A7: (normsequence (<*X,Y*>,Iv)) . j1 = the normF of (<*X,Y*> . j1) . (Iv . j1) by PRVECT_2:def_11
.= ||.x1.|| by A5, A6, FINSEQ_1:44 ;
A8: (normsequence (<*X,Y*>,Iv)) . j2 = the normF of (<*X,Y*> . j2) . (Iv . j2) by PRVECT_2:def_11
.= ||.y1.|| by A5, A6, FINSEQ_1:44 ;
len (normsequence (<*X,Y*>,Iv)) = len <*X,Y*> by PRVECT_2:def_11
.= 2 by FINSEQ_1:44 ;
then normsequence (<*X,Y*>,Iv) = v1 by A4, A7, A8, FINSEQ_1:44;
hence ||.(I . v).|| = ||.v.|| by A4, A3, A2, PRVECT_2:def_12; ::_thesis: verum
end;
hence for v being Point of [:X,Y:] holds ||.(I . v).|| = ||.v.|| ; ::_thesis: verum
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.|| ) )
proof
let X be RealNormSpace; ::_thesis: 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.|| ) )
reconsider X0 = X as RealLinearSpace ;
consider I0 being Function of X0,(product <*X0*>) such that
A1: ( I0 is one-to-one & I0 is onto & ( for x being Point of X holds I0 . x = <*x*> ) & ( for v, w being Point of X0 holds I0 . (v + w) = (I0 . v) + (I0 . w) ) & ( for v being Point of X0
for r being Element of REAL holds I0 . (r * v) = r * (I0 . v) ) & 0. (product <*X0*>) = I0 . (0. X0) ) by Th11;
A2: product <*X*> = NORMSTR(# (product (carr <*X*>)),(zeros <*X*>),[:(addop <*X*>):],[:(multop <*X*>):],(productnorm <*X*>) #) by PRVECT_2:6;
then reconsider I = I0 as Function of X,(product <*X*>) ;
take I ; ::_thesis: ( 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.|| ) )
thus ( I is one-to-one & I is onto & ( for x being Point of X holds I . x = <*x*> ) ) by A1, A2; ::_thesis: ( ( 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.|| ) )
thus for v, w being Point of X holds I . (v + w) = (I . v) + (I . w) ::_thesis: ( ( 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
let v, w be Point of X; ::_thesis: I . (v + w) = (I . v) + (I . w)
reconsider v0 = v, w0 = w as Point of X0 ;
thus I . (v + w) = (I0 . v0) + (I0 . w0) by A1
.= (I . v) + (I . w) by A2 ; ::_thesis: verum
end;
thus for v being Point of X
for r being Element of REAL holds I . (r * v) = r * (I . v) ::_thesis: ( 0. (product <*X*>) = I . (0. X) & ( for v being Point of X holds ||.(I . v).|| = ||.v.|| ) )
proof
let v be Point of X; ::_thesis: for r being Element of REAL holds I . (r * v) = r * (I . v)
let r be Element of REAL ; ::_thesis: I . (r * v) = r * (I . v)
reconsider v0 = v as Point of X0 ;
thus I . (r * v) = r * (I0 . v0) by A1
.= r * (I . v) by A2 ; ::_thesis: verum
end;
thus 0. (product <*X*>) = I . (0. X) by A1, A2; ::_thesis: for v being Point of X holds ||.(I . v).|| = ||.v.||
thus for v being Point of X holds ||.(I . v).|| = ||.v.|| ::_thesis: verum
proof
let v be Point of X; ::_thesis: ||.(I . v).|| = ||.v.||
len <*||.v.||*> = 1 by FINSEQ_1:40;
then reconsider v1 = <*||.v.||*> as Element of REAL 1 by FINSEQ_2:92;
A3: |.v1.| = sqrt (Sum <*(||.v.|| ^2)*>) by RVSUM_1:55
.= sqrt (||.v.|| ^2) by RVSUM_1:73
.= ||.v.|| by NORMSP_1:4, SQUARE_1:22 ;
A4: I . v = <*v*> by A1;
reconsider Iv = I . v as Element of product (carr <*X*>) by A2;
A5: <*v*> . 1 = v by FINSEQ_1:40;
1 in {1} by TARSKI:def_1;
then reconsider j1 = 1 as Element of dom <*X*> by FINSEQ_1:2, FINSEQ_1:def_8;
A6: (normsequence (<*X*>,Iv)) . j1 = the normF of (<*X*> . j1) . (Iv . j1) by PRVECT_2:def_11
.= ||.v.|| by A4, A5, FINSEQ_1:40 ;
len (normsequence (<*X*>,Iv)) = len <*X*> by PRVECT_2:def_11
.= 1 by FINSEQ_1:40 ;
then normsequence (<*X*>,Iv) = v1 by A6, FINSEQ_1:40;
hence ||.(I . v).|| = ||.v.|| by A3, A2, PRVECT_2:def_12; ::_thesis: verum
end;
end;
registration
let G, F be non empty RealNormSpace-yielding FinSequence;
clusterG ^ F -> non empty RealNormSpace-yielding ;
correctness
coherence
( not G ^ F is empty & G ^ F is RealNormSpace-yielding );
proof
for S being set st S in rng (G ^ F) holds
S is RealNormSpace
proof
let S be set ; ::_thesis: ( S in rng (G ^ F) implies S is RealNormSpace )
assume S in rng (G ^ F) ; ::_thesis: S is RealNormSpace
then consider i being set such that
A1: ( i in dom (G ^ F) & (G ^ F) . i = S ) by FUNCT_1:def_3;
reconsider i = i as Element of NAT by A1;
percases ( i in dom G or ex n being Nat st
( n in dom F & i = (len G) + n ) ) by A1, FINSEQ_1:25;
supposeA2: i in dom G ; ::_thesis: S is RealNormSpace
then G . i in rng G by FUNCT_1:3;
then G . i is RealNormSpace by PRVECT_2:def_10;
hence S is RealNormSpace by A1, A2, FINSEQ_1:def_7; ::_thesis: verum
end;
suppose ex n being Nat st
( n in dom F & i = (len G) + n ) ; ::_thesis: S is RealNormSpace
then consider n being Nat such that
A3: ( n in dom F & i = (len G) + n ) ;
F . n in rng F by A3, FUNCT_1:3;
then F . n is RealNormSpace by PRVECT_2:def_10;
hence S is RealNormSpace by A1, A3, FINSEQ_1:def_7; ::_thesis: verum
end;
end;
end;
hence ( not G ^ F is empty & G ^ F is RealNormSpace-yielding ) by PRVECT_2:def_10; ::_thesis: verum
end;
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.|| ) )
proof
let X, Y be RealNormSpace-Sequence; ::_thesis: 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.|| ) )
reconsider X0 = X, Y0 = Y as RealLinearSpace-Sequence ;
set PX = product X;
set PY = product Y;
set PX0 = product X0;
set PY0 = product Y0;
reconsider CX = carr X, CY = carr Y as non empty non-empty FinSequence ;
reconsider CX0 = carr X0, CY0 = carr Y0 as non empty non-empty FinSequence ;
A1: ( product X = NORMSTR(# (product (carr X)),(zeros X),[:(addop X):],[:(multop X):],(productnorm X) #) & product Y = NORMSTR(# (product (carr Y)),(zeros Y),[:(addop Y):],[:(multop Y):],(productnorm Y) #) ) by PRVECT_2:6;
A2: for g1, g2 being Point of (product X)
for f1, f2 being Point of (product Y) holds (prod_ADD ((product X0),(product Y0))) . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)]
proof
let g1, g2 be Point of (product X); ::_thesis: for f1, f2 being Point of (product Y) holds (prod_ADD ((product X0),(product Y0))) . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)]
let f1, f2 be Point of (product Y); ::_thesis: (prod_ADD ((product X0),(product Y0))) . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)]
reconsider g10 = g1, g20 = g2 as Point of (product X0) by A1;
reconsider f10 = f1, f20 = f2 as Point of (product Y0) by A1;
( g10 + g20 = g1 + g2 & f10 + f20 = f1 + f2 ) by A1;
hence (prod_ADD ((product X0),(product Y0))) . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] by Def1; ::_thesis: verum
end;
A3: for r being Element of REAL
for g being Point of (product X)
for f being Point of (product Y) holds (prod_MLT ((product X0),(product Y0))) . (r,[g,f]) = [(r * g),(r * f)]
proof
let r be Element of REAL ; ::_thesis: for g being Point of (product X)
for f being Point of (product Y) holds (prod_MLT ((product X0),(product Y0))) . (r,[g,f]) = [(r * g),(r * f)]
let g be Point of (product X); ::_thesis: for f being Point of (product Y) holds (prod_MLT ((product X0),(product Y0))) . (r,[g,f]) = [(r * g),(r * f)]
let f be Point of (product Y); ::_thesis: (prod_MLT ((product X0),(product Y0))) . (r,[g,f]) = [(r * g),(r * f)]
reconsider g0 = g as Point of (product X0) by A1;
reconsider f0 = f as Point of (product Y0) by A1;
( r * g0 = r * g & r * f0 = r * f ) by A1;
hence (prod_MLT ((product X0),(product Y0))) . (r,[g,f]) = [(r * g),(r * f)] by Def2; ::_thesis: verum
end;
A4: ( len (carr (X ^ Y)) = len (X ^ Y) & len (carr (X0 ^ Y0)) = len (X0 ^ Y0) & len CX = len X & len CY = len Y & len CX0 = len X0 & len CY0 = len Y0 ) by PRVECT_2:def_4;
consider I0 being Function of [:(product X0),(product Y0):],(product (X0 ^ Y0)) such that
A5: ( I0 is one-to-one & I0 is onto & ( for x being Point of (product X0)
for y being Point of (product Y0) ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I0 . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X0),(product Y0):] holds I0 . (v + w) = (I0 . v) + (I0 . w) ) & ( for v being Point of [:(product X0),(product Y0):]
for r being Element of REAL holds I0 . (r * v) = r * (I0 . v) ) & 0. (product (X0 ^ Y0)) = I0 . (0. [:(product X0),(product Y0):]) ) by Th13;
A6: product (X ^ Y) = NORMSTR(# (product (carr (X ^ Y))),(zeros (X ^ Y)),[:(addop (X ^ Y)):],[:(multop (X ^ Y)):],(productnorm (X ^ Y)) #) by PRVECT_2:6;
then reconsider I = I0 as Function of [:(product X),(product Y):],(product (X ^ Y)) by A1;
take I ; ::_thesis: ( 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.|| ) )
thus ( I is one-to-one & I is onto ) by A5, A6; ::_thesis: ( ( 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.|| ) )
thus 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 ) by A1, A5; ::_thesis: ( ( 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.|| ) )
A7: for x, y being FinSequence st x in the carrier of (product X) & y in the carrier of (product Y) holds
I . (x,y) = x ^ y
proof
let x, y be FinSequence; ::_thesis: ( x in the carrier of (product X) & y in the carrier of (product Y) implies I . (x,y) = x ^ y )
assume ( x in the carrier of (product X) & y in the carrier of (product Y) ) ; ::_thesis: I . (x,y) = x ^ y
then ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 ) by A1, A5;
hence I . (x,y) = x ^ y ; ::_thesis: verum
end;
thus for v, w being Point of [:(product X),(product Y):] holds I . (v + w) = (I . v) + (I . w) ::_thesis: ( ( 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
let v, w be Point of [:(product X),(product Y):]; ::_thesis: I . (v + w) = (I . v) + (I . w)
reconsider v0 = v, w0 = w as Point of [:(product X0),(product Y0):] by A1;
v + w = v0 + w0 by A2, A1, Def1;
then I . (v + w) = (I0 . v0) + (I0 . w0) by A5;
hence I . (v + w) = (I . v) + (I . w) by A6; ::_thesis: verum
end;
thus for v being Point of [:(product X),(product Y):]
for r being Element of REAL holds I . (r * v) = r * (I . v) ::_thesis: ( I . (0. [:(product X),(product Y):]) = 0. (product (X ^ Y)) & ( for v being Point of [:(product X),(product Y):] holds ||.(I . v).|| = ||.v.|| ) )
proof
let v be Point of [:(product X),(product Y):]; ::_thesis: for r being Element of REAL holds I . (r * v) = r * (I . v)
let r be Element of REAL ; ::_thesis: I . (r * v) = r * (I . v)
reconsider v0 = v as Point of [:(product X0),(product Y0):] by A1;
r * v = r * v0 by A3, A1, Def2;
then I . (r * v) = r * (I0 . v0) by A5;
hence I . (r * v) = r * (I . v) by A6; ::_thesis: verum
end;
thus 0. (product (X ^ Y)) = I . (0. [:(product X),(product Y):]) by A1, A5, A6; ::_thesis: for v being Point of [:(product X),(product Y):] holds ||.(I . v).|| = ||.v.||
for v being Point of [:(product X),(product Y):] holds ||.(I . v).|| = ||.v.||
proof
let v be Point of [:(product X),(product Y):]; ::_thesis: ||.(I . v).|| = ||.v.||
consider x1 being Point of (product X), y1 being Point of (product Y) such that
A8: v = [x1,y1] by Lm1;
consider v1 being Element of REAL 2 such that
A9: ( v1 = <*||.x1.||,||.y1.||*> & (prod_NORM ((product X),(product Y))) . (x1,y1) = |.v1.| ) by Def6;
reconsider Ix1 = x1, Iy1 = y1 as FinSequence by A1, Lm2;
A10: ( dom Ix1 = dom (carr X) & dom Iy1 = dom (carr Y) ) by A1, CARD_3:9;
A11: I . v = I . (x1,y1) by A8
.= Ix1 ^ Iy1 by A7 ;
reconsider Iv = I . v as Element of product (carr (X ^ Y)) by A6;
reconsider Ix = x1 as Element of product (carr X) by A1;
reconsider Iy = y1 as Element of product (carr Y) by A1;
A12: ||.(I . v).|| = |.(normsequence ((X ^ Y),Iv)).| by A6, PRVECT_2:def_12
.= sqrt (Sum (sqr (normsequence ((X ^ Y),Iv)))) ;
A13: ( len (normsequence ((X ^ Y),Iv)) = len (X ^ Y) & len (normsequence (X,Ix)) = len X & len (normsequence (Y,Iy)) = len Y ) by PRVECT_2:def_11;
A14: |.v1.| = sqrt (Sum <*(||.x1.|| ^2),(||.y1.|| ^2)*>) by A9, TOPREAL6:11
.= sqrt ((||.x1.|| ^2) + (||.y1.|| ^2)) by RVSUM_1:77 ;
A15: ( 0 <= Sum (sqr (normsequence (X,Ix))) & 0 <= Sum (sqr (normsequence (Y,Iy))) ) by RVSUM_1:86;
( ||.x1.|| ^2 = |.(normsequence (X,Ix)).| ^2 & ||.y1.|| ^2 = |.(normsequence (Y,Iy)).| ^2 ) by A1, PRVECT_2:def_12;
then A16: ( ||.x1.|| ^2 = Sum (sqr (normsequence (X,Ix))) & ||.y1.|| ^2 = Sum (sqr (normsequence (Y,Iy))) ) by A15, SQUARE_1:def_2;
len (normsequence ((X ^ Y),Iv)) = (len (normsequence (X,Ix))) + (len (normsequence (Y,Iy))) by A13, FINSEQ_1:22
.= len ((normsequence (X,Ix)) ^ (normsequence (Y,Iy))) by FINSEQ_1:22 ;
then A17: dom (normsequence ((X ^ Y),Iv)) = dom ((normsequence (X,Ix)) ^ (normsequence (Y,Iy))) by FINSEQ_3:29;
for k being Nat st k in dom (normsequence ((X ^ Y),Iv)) holds
(normsequence ((X ^ Y),Iv)) . k = ((normsequence (X,Ix)) ^ (normsequence (Y,Iy))) . k
proof
let k be Nat; ::_thesis: ( k in dom (normsequence ((X ^ Y),Iv)) implies (normsequence ((X ^ Y),Iv)) . k = ((normsequence (X,Ix)) ^ (normsequence (Y,Iy))) . k )
assume k in dom (normsequence ((X ^ Y),Iv)) ; ::_thesis: (normsequence ((X ^ Y),Iv)) . k = ((normsequence (X,Ix)) ^ (normsequence (Y,Iy))) . k
then A18: k in Seg (len (normsequence ((X ^ Y),Iv))) by FINSEQ_1:def_3;
then A19: k in dom (X ^ Y) by A13, FINSEQ_1:def_3;
reconsider k1 = k as Element of dom (X ^ Y) by A18, A13, FINSEQ_1:def_3;
A20: (normsequence ((X ^ Y),Iv)) . k = the normF of ((X ^ Y) . k1) . (Iv . k1) by PRVECT_2:def_11;
A21: ( dom Ix1 = Seg (len (carr X)) & dom Iy1 = Seg (len (carr Y)) ) by A10, FINSEQ_1:def_3;
then A22: ( dom Ix1 = dom X & dom Iy1 = dom Y ) by A4, FINSEQ_1:def_3;
percases ( k in dom X or ex n being Nat st
( n in dom Y & k = (len X) + n ) ) by A19, FINSEQ_1:25;
supposeA23: k in dom X ; ::_thesis: (normsequence ((X ^ Y),Iv)) . k = ((normsequence (X,Ix)) ^ (normsequence (Y,Iy))) . k
len X = len (normsequence (X,Ix)) by PRVECT_2:def_11;
then A24: k in dom (normsequence (X,Ix)) by A23, FINSEQ_3:29;
reconsider k2 = k1 as Element of dom X by A23;
A25: Iv . k = Ix1 . k by A23, A22, A11, FINSEQ_1:def_7;
thus (normsequence ((X ^ Y),Iv)) . k = the normF of (X . k2) . (Iv . k2) by A20, FINSEQ_1:def_7
.= (normsequence (X,Ix)) . k2 by A25, PRVECT_2:def_11
.= ((normsequence (X,Ix)) ^ (normsequence (Y,Iy))) . k by A24, FINSEQ_1:def_7 ; ::_thesis: verum
end;
suppose ex n being Nat st
( n in dom Y & k = (len X) + n ) ; ::_thesis: (normsequence ((X ^ Y),Iv)) . k = ((normsequence (X,Ix)) ^ (normsequence (Y,Iy))) . k
then consider n being Nat such that
A26: ( n in dom Y & k = (len X) + n ) ;
len Y = len (normsequence (Y,Iy)) by PRVECT_2:def_11;
then A27: n in dom (normsequence (Y,Iy)) by A26, FINSEQ_3:29;
reconsider n1 = n as Element of dom Y by A26;
len Ix1 = len X by A21, A4, FINSEQ_1:def_3;
then A28: Iv . k = Iy1 . n by A11, A26, A22, FINSEQ_1:def_7;
thus (normsequence ((X ^ Y),Iv)) . k = the normF of (Y . n1) . (Iv . k1) by A20, A26, FINSEQ_1:def_7
.= (normsequence (Y,Iy)) . n1 by A28, PRVECT_2:def_11
.= ((normsequence (X,Ix)) ^ (normsequence (Y,Iy))) . k by A27, A26, A13, FINSEQ_1:def_7 ; ::_thesis: verum
end;
end;
end;
then normsequence ((X ^ Y),Iv) = (normsequence (X,Ix)) ^ (normsequence (Y,Iy)) by A17, FINSEQ_1:13;
then sqr (normsequence ((X ^ Y),Iv)) = (sqr (normsequence (X,Ix))) ^ (sqr (normsequence (Y,Iy))) by Lm3;
hence ||.(I . v).|| = ||.v.|| by A14, A12, A16, A9, A8, RVSUM_1:75; ::_thesis: verum
end;
hence for v being Point of [:(product X),(product Y):] holds ||.(I . v).|| = ||.v.|| ; ::_thesis: verum
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 number 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
let G, F be RealNormSpace; ::_thesis: ( ( 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 number 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.| ) ) )
thus 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] ) by Lm1; ::_thesis: ( ( 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 number 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.| ) ) )
thus 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)] by Def1; ::_thesis: ( 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 number 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.| ) ) )
thus 0. [:G,F:] = [(0. G),(0. F)] ; ::_thesis: ( ( 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 number 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.| ) ) )
thus 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)] ::_thesis: ( ( for x being Point of [:G,F:]
for x1 being Point of G
for x2 being Point of F
for a being real number 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
let x be Point of [:G,F:]; ::_thesis: for x1 being Point of G
for x2 being Point of F st x = [x1,x2] holds
- x = [(- x1),(- x2)]
let x1 be Point of G; ::_thesis: for x2 being Point of F st x = [x1,x2] holds
- x = [(- x1),(- x2)]
let x2 be Point of F; ::_thesis: ( x = [x1,x2] implies - x = [(- x1),(- x2)] )
assume A1: x = [x1,x2] ; ::_thesis: - x = [(- x1),(- x2)]
reconsider y = [(- x1),(- x2)] as Point of [:G,F:] ;
x + y = [(x1 + (- x1)),(x2 + (- x2))] by A1, Def1
.= [(0. G),(x2 + (- x2))] by RLVECT_1:def_10
.= 0. [:G,F:] by RLVECT_1:def_10 ;
hence - x = [(- x1),(- x2)] by RLVECT_1:def_10; ::_thesis: verum
end;
thus for x being Point of [:G,F:]
for x1 being Point of G
for x2 being Point of F
for a being real number st x = [x1,x2] holds
a * x = [(a * x1),(a * x2)] ::_thesis: 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
let x be Point of [:G,F:]; ::_thesis: for x1 being Point of G
for x2 being Point of F
for a being real number st x = [x1,x2] holds
a * x = [(a * x1),(a * x2)]
let x1 be Point of G; ::_thesis: for x2 being Point of F
for a being real number st x = [x1,x2] holds
a * x = [(a * x1),(a * x2)]
let x2 be Point of F; ::_thesis: for a being real number st x = [x1,x2] holds
a * x = [(a * x1),(a * x2)]
let a be real number ; ::_thesis: ( x = [x1,x2] implies a * x = [(a * x1),(a * x2)] )
assume A2: x = [x1,x2] ; ::_thesis: a * x = [(a * x1),(a * x2)]
reconsider a0 = a as Element of REAL by XREAL_0:def_1;
thus a * x = (prod_MLT (G,F)) . (a0,x)
.= [(a * x1),(a * x2)] by A2, Def2 ; ::_thesis: verum
end;
thus 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.| ) ::_thesis: verum
proof
let x be Point of [:G,F:]; ::_thesis: 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.| )
let x1 be Point of G; ::_thesis: for x2 being Point of F st x = [x1,x2] holds
ex w being Element of REAL 2 st
( w = <*||.x1.||,||.x2.||*> & ||.x.|| = |.w.| )
let x2 be Point of F; ::_thesis: ( x = [x1,x2] implies ex w being Element of REAL 2 st
( w = <*||.x1.||,||.x2.||*> & ||.x.|| = |.w.| ) )
assume A3: x = [x1,x2] ; ::_thesis: ex w being Element of REAL 2 st
( w = <*||.x1.||,||.x2.||*> & ||.x.|| = |.w.| )
ex w being Element of REAL 2 st
( w = <*||.x1.||,||.x2.||*> & (prod_NORM (G,F)) . (x1,x2) = |.w.| ) by Def6;
hence ex w being Element of REAL 2 st
( w = <*||.x1.||,||.x2.||*> & ||.x.|| = |.w.| ) by A3; ::_thesis: verum
end;
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 number 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
let G, F be RealNormSpace; ::_thesis: ( ( 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 number 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.| ) ) )
consider I being Function of [:G,F:],(product <*G,F*>) such that
A1: ( I is one-to-one & I is onto & ( for x being Point of G
for y being Point of F holds I . (x,y) = <*x,y*> ) & ( for v, w being Point of [:G,F:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:G,F:]
for r being Element of REAL holds I . (r * v) = r * (I . v) ) & 0. (product <*G,F*>) = I . (0. [:G,F:]) & ( for v being Point of [:G,F:] holds ||.(I . v).|| = ||.v.|| ) ) by Th15;
thus A2: 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*> ) ::_thesis: ( ( 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 number 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
let y be set ; ::_thesis: ( y is Point of (product <*G,F*>) iff ex x1 being Point of G ex x2 being Point of F st y = <*x1,x2*> )
hereby ::_thesis: ( ex x1 being Point of G ex x2 being Point of F st y = <*x1,x2*> implies y is Point of (product <*G,F*>) )
assume y is Point of (product <*G,F*>) ; ::_thesis: ex x1 being Point of G ex x2 being Point of F st y = <*x1,x2*>
then y in the carrier of (product <*G,F*>) ;
then y in rng I by A1, FUNCT_2:def_3;
then consider x being Element of the carrier of [:G,F:] such that
A3: y = I . x by FUNCT_2:113;
consider x1 being Point of G, x2 being Point of F such that
A4: x = [x1,x2] by Lm1;
take x1 = x1; ::_thesis: ex x2 being Point of F st y = <*x1,x2*>
take x2 = x2; ::_thesis: y = <*x1,x2*>
I . (x1,x2) = <*x1,x2*> by A1;
hence y = <*x1,x2*> by A3, A4; ::_thesis: verum
end;
hereby ::_thesis: verum
assume ex x1 being Point of G ex x2 being Point of F st y = <*x1,x2*> ; ::_thesis: y is Point of (product <*G,F*>)
then consider x1 being Point of G, x2 being Point of F such that
A5: y = <*x1,x2*> ;
A6: I . [x1,x2] in rng I by FUNCT_2:112;
I . (x1,x2) = <*x1,x2*> by A1;
hence y is Point of (product <*G,F*>) by A5, A6; ::_thesis: verum
end;
end;
thus A7: 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)*> ::_thesis: ( 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 number 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
let x, y be Point of (product <*G,F*>); ::_thesis: 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)*>
let x1, y1 be Point of G; ::_thesis: for x2, y2 being Point of F st x = <*x1,x2*> & y = <*y1,y2*> holds
x + y = <*(x1 + y1),(x2 + y2)*>
let x2, y2 be Point of F; ::_thesis: ( x = <*x1,x2*> & y = <*y1,y2*> implies x + y = <*(x1 + y1),(x2 + y2)*> )
assume A8: ( x = <*x1,x2*> & y = <*y1,y2*> ) ; ::_thesis: x + y = <*(x1 + y1),(x2 + y2)*>
reconsider z = [x1,x2], w = [y1,y2] as Point of [:G,F:] ;
A9: z + w = [(x1 + y1),(x2 + y2)] by Def1;
A10: I . ((x1 + y1),(x2 + y2)) = <*(x1 + y1),(x2 + y2)*> by A1;
( I . (x1,x2) = <*x1,x2*> & I . (y1,y2) = <*y1,y2*> ) by A1;
hence <*(x1 + y1),(x2 + y2)*> = x + y by A1, A9, A10, A8; ::_thesis: verum
end;
thus A11: 0. (product <*G,F*>) = <*(0. G),(0. F)*> ::_thesis: ( ( 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 number 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
I . ((0. G),(0. F)) = <*(0. G),(0. F)*> by A1;
hence 0. (product <*G,F*>) = <*(0. G),(0. F)*> by A1; ::_thesis: verum
end;
thus 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)*> ::_thesis: ( ( for x being Point of (product <*G,F*>)
for x1 being Point of G
for x2 being Point of F
for a being real number 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
let x be Point of (product <*G,F*>); ::_thesis: for x1 being Point of G
for x2 being Point of F st x = <*x1,x2*> holds
- x = <*(- x1),(- x2)*>
let x1 be Point of G; ::_thesis: for x2 being Point of F st x = <*x1,x2*> holds
- x = <*(- x1),(- x2)*>
let x2 be Point of F; ::_thesis: ( x = <*x1,x2*> implies - x = <*(- x1),(- x2)*> )
assume A12: x = <*x1,x2*> ; ::_thesis: - x = <*(- x1),(- x2)*>
reconsider y = <*(- x1),(- x2)*> as Point of (product <*G,F*>) by A2;
x + y = <*(x1 + (- x1)),(x2 + (- x2))*> by A7, A12
.= <*(0. G),(x2 + (- x2))*> by RLVECT_1:def_10
.= 0. (product <*G,F*>) by A11, RLVECT_1:def_10 ;
hence - x = <*(- x1),(- x2)*> by RLVECT_1:def_10; ::_thesis: verum
end;
thus for x being Point of (product <*G,F*>)
for x1 being Point of G
for x2 being Point of F
for a being real number st x = <*x1,x2*> holds
a * x = <*(a * x1),(a * x2)*> ::_thesis: 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
let x be Point of (product <*G,F*>); ::_thesis: for x1 being Point of G
for x2 being Point of F
for a being real number st x = <*x1,x2*> holds
a * x = <*(a * x1),(a * x2)*>
let x1 be Point of G; ::_thesis: for x2 being Point of F
for a being real number st x = <*x1,x2*> holds
a * x = <*(a * x1),(a * x2)*>
let x2 be Point of F; ::_thesis: for a being real number st x = <*x1,x2*> holds
a * x = <*(a * x1),(a * x2)*>
let a be real number ; ::_thesis: ( x = <*x1,x2*> implies a * x = <*(a * x1),(a * x2)*> )
assume A13: x = <*x1,x2*> ; ::_thesis: a * x = <*(a * x1),(a * x2)*>
reconsider a0 = a as Element of REAL by XREAL_0:def_1;
reconsider y = [x1,x2] as Point of [:G,F:] ;
A14: <*x1,x2*> = I . (x1,x2) by A1;
I . (a * y) = I . ((a0 * x1),(a0 * x2)) by Th18
.= <*(a0 * x1),(a0 * x2)*> by A1 ;
hence a * x = <*(a * x1),(a * x2)*> by A13, A14, A1; ::_thesis: verum
end;
thus 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.| ) ::_thesis: verum
proof
let x be Point of (product <*G,F*>); ::_thesis: 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.| )
let x1 be Point of G; ::_thesis: for x2 being Point of F st x = <*x1,x2*> holds
ex w being Element of REAL 2 st
( w = <*||.x1.||,||.x2.||*> & ||.x.|| = |.w.| )
let x2 be Point of F; ::_thesis: ( x = <*x1,x2*> implies ex w being Element of REAL 2 st
( w = <*||.x1.||,||.x2.||*> & ||.x.|| = |.w.| ) )
assume A15: x = <*x1,x2*> ; ::_thesis: ex w being Element of REAL 2 st
( w = <*||.x1.||,||.x2.||*> & ||.x.|| = |.w.| )
reconsider y = [x1,x2] as Point of [:G,F:] ;
consider w being Element of REAL 2 such that
A16: ( w = <*||.x1.||,||.x2.||*> & ||.y.|| = |.w.| ) by Th18;
take w ; ::_thesis: ( w = <*||.x1.||,||.x2.||*> & ||.x.|| = |.w.| )
A17: I . y = I . (x1,x2)
.= x by A1, A15 ;
thus w = <*||.x1.||,||.x2.||*> by A16; ::_thesis: ||.x.|| = |.w.|
thus ||.x.|| = |.w.| by A1, A16, A17; ::_thesis: verum
end;
end;
registration
let X, Y be complete RealNormSpace;
cluster[:X,Y:] -> non empty strict complete ;
coherence
[:X,Y:] is complete
proof
A1: dom <*X,Y*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89;
now__::_thesis:_for_i_being_Element_of_dom_<*X,Y*>_holds_<*X,Y*>_._i_is_complete
let i be Element of dom <*X,Y*>; ::_thesis: <*X,Y*> . i is complete
( i = 1 or i = 2 ) by A1, TARSKI:def_2;
hence <*X,Y*> . i is complete by FINSEQ_1:44; ::_thesis: verum
end;
then A2: product <*X,Y*> is complete by PRVECT_2:14;
consider I being Function of [:X,Y:],(product <*X,Y*>) such that
A3: ( 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) ) & 0. (product <*X,Y*>) = I . (0. [:X,Y:]) & ( for v being Point of [:X,Y:] holds ||.(I . v).|| = ||.v.|| ) ) by Th15;
A4: now__::_thesis:_for_v,_w_being_Point_of_[:X,Y:]_holds_I_._(v_-_w)_=_(I_._v)_-_(I_._w)
let v, w be Point of [:X,Y:]; ::_thesis: I . (v - w) = (I . v) - (I . w)
thus I . (v - w) = I . (v + ((- 1) * w)) by RLVECT_1:16
.= (I . v) + (I . ((- 1) * w)) by A3
.= (I . v) + ((- 1) * (I . w)) by A3
.= (I . v) - (I . w) by RLVECT_1:16 ; ::_thesis: verum
end;
A5: now__::_thesis:_for_v,_w_being_Point_of_[:X,Y:]_holds_||.((I_._v)_-_(I_._w)).||_=_||.(v_-_w).||
let v, w be Point of [:X,Y:]; ::_thesis: ||.((I . v) - (I . w)).|| = ||.(v - w).||
thus ||.((I . v) - (I . w)).|| = ||.(I . (v - w)).|| by A4
.= ||.(v - w).|| by A3 ; ::_thesis: verum
end;
now__::_thesis:_for_seq_being_sequence_of_[:X,Y:]_st_seq_is_Cauchy_sequence_by_Norm_holds_
seq_is_convergent
let seq be sequence of [:X,Y:]; ::_thesis: ( seq is Cauchy_sequence_by_Norm implies seq is convergent )
assume A6: seq is Cauchy_sequence_by_Norm ; ::_thesis: seq is convergent
reconsider Iseq = I * seq as sequence of (product <*X,Y*>) ;
now__::_thesis:_for_r_being_Real_st_r_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_n,_m_being_Element_of_NAT_st_n_>=_k_&_m_>=_k_holds_
||.((Iseq_._n)_-_(Iseq_._m)).||_<_r
let r be Real; ::_thesis: ( r > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((Iseq . n) - (Iseq . m)).|| < r )
assume r > 0 ; ::_thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((Iseq . n) - (Iseq . m)).|| < r
then consider k being Element of NAT such that
A7: for n, m being Element of NAT st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r by A6, RSSPACE3:8;
take k = k; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds
||.((Iseq . n) - (Iseq . m)).|| < r
hereby ::_thesis: verum
let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies ||.((Iseq . n) - (Iseq . m)).|| < r )
assume ( n >= k & m >= k ) ; ::_thesis: ||.((Iseq . n) - (Iseq . m)).|| < r
then A8: ||.((seq . n) - (seq . m)).|| < r by A7;
NAT = dom seq by FUNCT_2:def_1;
then ( Iseq . n = I . (seq . n) & Iseq . m = I . (seq . m) ) by FUNCT_1:13;
hence ||.((Iseq . n) - (Iseq . m)).|| < r by A8, A5; ::_thesis: verum
end;
end;
then Iseq is Cauchy_sequence_by_Norm by RSSPACE3:8;
then A9: Iseq is convergent by A2, LOPBAN_1:def_15;
( dom (I ") = rng I & rng (I ") = dom I ) by A3, FUNCT_1:33;
then ( dom (I ") = the carrier of (product <*X,Y*>) & rng (I ") = the carrier of [:X,Y:] ) by A3, FUNCT_2:def_1, FUNCT_2:def_3;
then reconsider Lseq = (I ") . (lim Iseq) as Point of [:X,Y:] by FUNCT_1:3;
rng I = the carrier of (product <*X,Y*>) by A3, FUNCT_2:def_3;
then A10: I . Lseq = lim Iseq by A3, FUNCT_1:35;
now__::_thesis:_for_r_being_Real_st_0_<_r_holds_
ex_m_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_m_<=_n_holds_
||.((seq_._n)_-_Lseq).||_<_r
let r be Real; ::_thesis: ( 0 < r implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((seq . n) - Lseq).|| < r )
assume 0 < r ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((seq . n) - Lseq).|| < r
then consider m being Element of NAT such that
A11: for n being Element of NAT st m <= n holds
||.((Iseq . n) - (lim Iseq)).|| < r by A9, NORMSP_1:def_7;
take m = m; ::_thesis: for n being Element of NAT st m <= n holds
||.((seq . n) - Lseq).|| < r
thus for n being Element of NAT st m <= n holds
||.((seq . n) - Lseq).|| < r ::_thesis: verum
proof
let n be Element of NAT ; ::_thesis: ( m <= n implies ||.((seq . n) - Lseq).|| < r )
assume m <= n ; ::_thesis: ||.((seq . n) - Lseq).|| < r
then A12: ||.((Iseq . n) - (lim Iseq)).|| < r by A11;
NAT = dom seq by FUNCT_2:def_1;
then Iseq . n = I . (seq . n) by FUNCT_1:13;
hence ||.((seq . n) - Lseq).|| < r by A10, A5, A12; ::_thesis: verum
end;
end;
hence seq is convergent by NORMSP_1:def_6; ::_thesis: verum
end;
hence [:X,Y:] is complete by LOPBAN_1:def_15; ::_thesis: verum
end;
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.|| ) )
proof
let X, Y be RealNormSpace-Sequence; ::_thesis: 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.|| ) )
set PX = product X;
set PY = product Y;
set PXY = product (X ^ Y);
consider K being Function of [:(product X),(product Y):],(product (X ^ Y)) such that
A1: ( K is one-to-one & K 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 & K . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),(product Y):] holds K . (v + w) = (K . v) + (K . w) ) & ( for v being Point of [:(product X),(product Y):]
for r being Element of REAL holds K . (r * v) = r * (K . v) ) & K . (0. [:(product X),(product Y):]) = 0. (product (X ^ Y)) & ( for v being Point of [:(product X),(product Y):] holds ||.(K . v).|| = ||.v.|| ) ) by Th17;
consider J being Function of [:(product X),(product Y):],(product <*(product X),(product Y)*>) such that
A2: ( J is one-to-one & J is onto & ( for x being Point of (product X)
for y being Point of (product Y) holds J . (x,y) = <*x,y*> ) & ( for v, w being Point of [:(product X),(product Y):] holds J . (v + w) = (J . v) + (J . w) ) & ( for v being Point of [:(product X),(product Y):]
for r being Element of REAL holds J . (r * v) = r * (J . v) ) & 0. (product <*(product X),(product Y)*>) = J . (0. [:(product X),(product Y):]) & ( for v being Point of [:(product X),(product Y):] holds ||.(J . v).|| = ||.v.|| ) ) by Th15;
A3: rng J = the carrier of (product <*(product X),(product Y)*>) by A2, FUNCT_2:def_3;
then reconsider JB = J " as Function of the carrier of (product <*(product X),(product Y)*>), the carrier of [:(product X),(product Y):] by A2, FUNCT_2:25;
A4: ( dom (J ") = rng J & rng (J ") = dom J ) by A2, FUNCT_1:33;
then A5: dom (J ") = the carrier of (product <*(product X),(product Y)*>) by A2, FUNCT_2:def_3;
A6: rng (J ") = the carrier of [:(product X),(product Y):] by A4, FUNCT_2:def_1;
reconsider I = K * JB as Function of (product <*(product X),(product Y)*>),(product (X ^ Y)) ;
take I ; ::_thesis: ( 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.|| ) )
thus I is one-to-one by A1, A2; ::_thesis: ( 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.|| ) )
rng K = the carrier of (product (X ^ Y)) by A1, FUNCT_2:def_3;
then rng I = the carrier of (product (X ^ Y)) by A6, FUNCT_2:14;
hence I is onto by FUNCT_2:def_3; ::_thesis: ( ( 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.|| ) )
thus 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 ) ::_thesis: ( ( 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
let x be Point of (product X); ::_thesis: for y being Point of (product Y) ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I . <*x,y*> = x1 ^ y1 )
let y be Point of (product Y); ::_thesis: ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I . <*x,y*> = x1 ^ y1 )
consider x1, y1 being FinSequence such that
A7: ( x = x1 & y = y1 & K . (x,y) = x1 ^ y1 ) by A1;
A8: J . (x,y) = <*x,y*> by A2;
[x,y] in the carrier of [:(product X),(product Y):] ;
then A9: [x,y] in dom J by FUNCT_2:def_1;
<*x,y*> is Point of (product <*(product X),(product Y)*>) by Th19;
then I . <*x,y*> = K . (JB . (J . [x,y])) by A8, A5, FUNCT_1:13;
then I . <*x,y*> = x1 ^ y1 by A7, A9, A2, FUNCT_1:34;
hence ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I . <*x,y*> = x1 ^ y1 ) by A7; ::_thesis: verum
end;
thus for v, w being Point of (product <*(product X),(product Y)*>) holds I . (v + w) = (I . v) + (I . w) ::_thesis: ( ( 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
let v, w be Point of (product <*(product X),(product Y)*>); ::_thesis: I . (v + w) = (I . v) + (I . w)
consider x being Element of the carrier of [:(product X),(product Y):] such that
A10: v = J . x by A3, FUNCT_2:113;
consider y being Element of the carrier of [:(product X),(product Y):] such that
A11: w = J . y by A3, FUNCT_2:113;
( x in the carrier of [:(product X),(product Y):] & y in the carrier of [:(product X),(product Y):] & x + y in the carrier of [:(product X),(product Y):] ) ;
then ( x in dom J & y in dom J & x + y in dom J ) by FUNCT_2:def_1;
then A12: ( JB . v = x & JB . w = y & JB . (J . (x + y)) = x + y ) by A10, A11, A2, FUNCT_1:34;
( v in rng J & w in rng J ) by A3;
then A13: ( v in dom JB & w in dom JB ) by A2, FUNCT_1:33;
v + w = J . (x + y) by A10, A11, A2;
then I . (v + w) = K . (x + y) by A12, A5, FUNCT_1:13
.= (K . x) + (K . y) by A1
.= ((K * JB) . v) + (K . (JB . w)) by A12, A13, FUNCT_1:13 ;
hence I . (v + w) = (I . v) + (I . w) by A13, FUNCT_1:13; ::_thesis: verum
end;
thus for v being Point of (product <*(product X),(product Y)*>)
for r being Element of REAL holds I . (r * v) = r * (I . v) ::_thesis: ( 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
let v be Point of (product <*(product X),(product Y)*>); ::_thesis: for r being Element of REAL holds I . (r * v) = r * (I . v)
let r be Element of REAL ; ::_thesis: I . (r * v) = r * (I . v)
consider x being Element of the carrier of [:(product X),(product Y):] such that
A14: v = J . x by A3, FUNCT_2:113;
x in the carrier of [:(product X),(product Y):] ;
then x in dom J by FUNCT_2:def_1;
then A15: JB . v = x by A14, A2, FUNCT_1:34;
v in rng J by A3;
then A16: v in dom JB by A2, FUNCT_1:33;
r * x in the carrier of [:(product X),(product Y):] ;
then A17: r * x in dom J by FUNCT_2:def_1;
r * v = J . (r * x) by A14, A2;
then I . (r * v) = K . (JB . (J . (r * x))) by A5, FUNCT_1:13;
hence I . (r * v) = K . (r * x) by A17, A2, FUNCT_1:34
.= r * (K . x) by A1
.= r * (I . v) by A15, A16, FUNCT_1:13 ;
::_thesis: verum
end;
thus I . (0. (product <*(product X),(product Y)*>)) = 0. (product (X ^ Y)) ::_thesis: for v being Point of (product <*(product X),(product Y)*>) holds ||.(I . v).|| = ||.v.||
proof
0. [:(product X),(product Y):] in the carrier of [:(product X),(product Y):] ;
then A18: 0. [:(product X),(product Y):] in dom J by FUNCT_2:def_1;
0. (product <*(product X),(product Y)*>) in rng J by A3;
then 0. (product <*(product X),(product Y)*>) in dom JB by A2, FUNCT_1:33;
then I . (0. (product <*(product X),(product Y)*>)) = K . (JB . (J . (0. [:(product X),(product Y):]))) by A2, FUNCT_1:13;
hence I . (0. (product <*(product X),(product Y)*>)) = 0. (product (X ^ Y)) by A1, A18, A2, FUNCT_1:34; ::_thesis: verum
end;
thus for v being Point of (product <*(product X),(product Y)*>) holds ||.(I . v).|| = ||.v.|| ::_thesis: verum
proof
let v be Point of (product <*(product X),(product Y)*>); ::_thesis: ||.(I . v).|| = ||.v.||
consider x being Element of the carrier of [:(product X),(product Y):] such that
A19: v = J . x by A3, FUNCT_2:113;
x in the carrier of [:(product X),(product Y):] ;
then A20: x in dom J by FUNCT_2:def_1;
v in rng J by A3;
then v in dom JB by A2, FUNCT_1:33;
then I . v = K . (JB . (J . x)) by A19, FUNCT_1:13
.= K . x by A20, A2, FUNCT_1:34 ;
then ||.(I . v).|| = ||.x.|| by A1;
hence ||.(I . v).|| = ||.v.|| by A2, A19; ::_thesis: verum
end;
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*>):] )
proof
let X, Y be RealLinearSpace; ::_thesis: 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*>):] )
consider J being Function of Y,(product <*Y*>) such that
A1: ( J is one-to-one & J is onto & ( for y being Point of Y holds J . y = <*y*> ) & ( for v, w being Point of Y holds J . (v + w) = (J . v) + (J . w) ) & ( for v being Point of Y
for r being Element of REAL holds J . (r * v) = r * (J . v) ) & J . (0. Y) = 0. (product <*Y*>) ) by Th11;
defpred S1[ set , set , set ] means $3 = [$1,<*$2*>];
A2: for x, y being set st x in the carrier of X & y in the carrier of Y holds
ex z being set st
( z in the carrier of [:X,(product <*Y*>):] & S1[x,y,z] )
proof
let x, y be set ; ::_thesis: ( x in the carrier of X & y in the carrier of Y implies ex z being set st
( z in the carrier of [:X,(product <*Y*>):] & S1[x,y,z] ) )
assume A3: ( x in the carrier of X & y in the carrier of Y ) ; ::_thesis: ex z being set st
( z in the carrier of [:X,(product <*Y*>):] & S1[x,y,z] )
then reconsider y0 = y as Point of Y ;
J . y0 = <*y0*> by A1;
then [x,<*y*>] in [: the carrier of X, the carrier of (product <*Y*>):] by A3, ZFMISC_1:87;
hence ex z being set st
( z in the carrier of [:X,(product <*Y*>):] & S1[x,y,z] ) ; ::_thesis: verum
end;
consider I being Function of [: the carrier of X, the carrier of Y:], the carrier of [:X,(product <*Y*>):] such that
A4: for x, y being set st x in the carrier of X & y in the carrier of Y holds
S1[x,y,I . (x,y)] from BINOP_1:sch_1(A2);
reconsider I = I as Function of [:X,Y:],[:X,(product <*Y*>):] ;
take I ; ::_thesis: ( 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*>):] )
now__::_thesis:_for_z1,_z2_being_set_st_z1_in_the_carrier_of_[:X,Y:]_&_z2_in_the_carrier_of_[:X,Y:]_&_I_._z1_=_I_._z2_holds_
z1_=_z2
let z1, z2 be set ; ::_thesis: ( z1 in the carrier of [:X,Y:] & z2 in the carrier of [:X,Y:] & I . z1 = I . z2 implies z1 = z2 )
assume A5: ( z1 in the carrier of [:X,Y:] & z2 in the carrier of [:X,Y:] & I . z1 = I . z2 ) ; ::_thesis: z1 = z2
consider x1, y1 being set such that
A6: ( x1 in the carrier of X & y1 in the carrier of Y & z1 = [x1,y1] ) by A5, ZFMISC_1:def_2;
consider x2, y2 being set such that
A7: ( x2 in the carrier of X & y2 in the carrier of Y & z2 = [x2,y2] ) by A5, ZFMISC_1:def_2;
[x1,<*y1*>] = I . (x1,y1) by A4, A6
.= I . (x2,y2) by A5, A6, A7
.= [x2,<*y2*>] by A4, A7 ;
then ( x1 = x2 & <*y1*> = <*y2*> ) by XTUPLE_0:1;
hence z1 = z2 by A6, A7, FINSEQ_1:76; ::_thesis: verum
end;
hence I is one-to-one by FUNCT_2:19; ::_thesis: ( 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*>):] )
now__::_thesis:_for_w_being_set_st_w_in_the_carrier_of_[:X,(product_<*Y*>):]_holds_
w_in_rng_I
let w be set ; ::_thesis: ( w in the carrier of [:X,(product <*Y*>):] implies w in rng I )
assume w in the carrier of [:X,(product <*Y*>):] ; ::_thesis: w in rng I
then consider x, y1 being set such that
A8: ( x in the carrier of X & y1 in the carrier of (product <*Y*>) & w = [x,y1] ) by ZFMISC_1:def_2;
y1 in rng J by A1, A8, FUNCT_2:def_3;
then consider y being set such that
A9: ( y in the carrier of Y & y1 = J . y ) by FUNCT_2:11;
reconsider z = [x,y] as Element of [: the carrier of X, the carrier of Y:] by A8, A9, ZFMISC_1:87;
J . y = <*y*> by A9, A1;
then w = I . (x,y) by A4, A8, A9;
then w = I . z ;
hence w in rng I by FUNCT_2:4; ::_thesis: verum
end;
then the carrier of [:X,(product <*Y*>):] c= rng I by TARSKI:def_3;
then the carrier of [:X,(product <*Y*>):] = rng I by XBOOLE_0:def_10;
hence I is onto by FUNCT_2:def_3; ::_thesis: ( ( 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*>):] )
thus for x being Point of X
for y being Point of Y holds I . (x,y) = [x,<*y*>] by A4; ::_thesis: ( ( 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*>):] )
thus for v, w being Point of [:X,Y:] holds I . (v + w) = (I . v) + (I . w) ::_thesis: ( ( 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
let v, w be Point of [:X,Y:]; ::_thesis: I . (v + w) = (I . v) + (I . w)
consider x1 being Point of X, x2 being Point of Y such that
A10: v = [x1,x2] by Lm1;
consider y1 being Point of X, y2 being Point of Y such that
A11: w = [y1,y2] by Lm1;
A12: I . (v + w) = I . ((x1 + y1),(x2 + y2)) by A10, A11, Def1
.= [(x1 + y1),<*(x2 + y2)*>] by A4 ;
( I . v = I . (x1,x2) & I . w = I . (y1,y2) ) by A10, A11;
then A13: ( I . v = [x1,<*x2*>] & I . w = [y1,<*y2*>] ) by A4;
A14: ( J . x2 = <*x2*> & J . y2 = <*y2*> ) by A1;
then reconsider xx2 = <*x2*> as Point of (product <*Y*>) ;
reconsider yy2 = <*y2*> as Point of (product <*Y*>) by A14;
<*(x2 + y2)*> = J . (x2 + y2) by A1
.= xx2 + yy2 by A14, A1 ;
hence (I . v) + (I . w) = I . (v + w) by A12, A13, Def1; ::_thesis: verum
end;
thus for v being Point of [:X,Y:]
for r being Element of REAL holds I . (r * v) = r * (I . v) ::_thesis: I . (0. [:X,Y:]) = 0. [:X,(product <*Y*>):]
proof
let v be Point of [:X,Y:]; ::_thesis: for r being Element of REAL holds I . (r * v) = r * (I . v)
let r be Element of REAL ; ::_thesis: I . (r * v) = r * (I . v)
consider x1 being Point of X, x2 being Point of Y such that
A15: v = [x1,x2] by Lm1;
A16: I . (r * v) = I . ((r * x1),(r * x2)) by A15, Th9
.= [(r * x1),<*(r * x2)*>] by A4 ;
A17: I . v = I . (x1,x2) by A15
.= [x1,<*x2*>] by A4 ;
A18: J . x2 = <*x2*> by A1;
then reconsider xx2 = <*x2*> as Point of (product <*Y*>) ;
<*(r * x2)*> = J . (r * x2) by A1
.= r * xx2 by A18, A1 ;
hence r * (I . v) = I . (r * v) by A16, A17, Th9; ::_thesis: verum
end;
A19: <*(0. Y)*> = 0. (product <*Y*>) by A1;
I . (0. [:X,Y:]) = I . ((0. X),(0. Y)) ;
hence I . (0. [:X,Y:]) = 0. [:X,(product <*Y*>):] by A19, A4; ::_thesis: verum
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*>)) )
proof
let X be RealLinearSpace-Sequence; ::_thesis: 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*>)) )
let Y be RealLinearSpace; ::_thesis: 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*>)) )
consider I being Function of [:(product X),Y:],[:(product X),(product <*Y*>):] such that
A1: ( I is one-to-one & I is onto & ( for x being Point of (product X)
for y being Point of Y holds I . (x,y) = [x,<*y*>] ) & ( 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),(product <*Y*>):] ) by Th21;
consider J being Function of [:(product X),(product <*Y*>):],(product (X ^ <*Y*>)) such that
A2: ( J is one-to-one & J 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 & J . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),(product <*Y*>):] holds J . (v + w) = (J . v) + (J . w) ) & ( for v being Point of [:(product X),(product <*Y*>):]
for r being Element of REAL holds J . (r * v) = r * (J . v) ) & J . (0. [:(product X),(product <*Y*>):]) = 0. (product (X ^ <*Y*>)) ) by Th13;
set K = J * I;
reconsider K = J * I as Function of [:(product X),Y:],(product (X ^ <*Y*>)) ;
take K ; ::_thesis: ( K is one-to-one & K 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 & K . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),Y:] holds K . (v + w) = (K . v) + (K . w) ) & ( for v being Point of [:(product X),Y:]
for r being Element of REAL holds K . (r * v) = r * (K . v) ) & K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) )
thus K is one-to-one by A1, A2; ::_thesis: ( K 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 & K . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),Y:] holds K . (v + w) = (K . v) + (K . w) ) & ( for v being Point of [:(product X),Y:]
for r being Element of REAL holds K . (r * v) = r * (K . v) ) & K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) )
A3: rng J = the carrier of (product (X ^ <*Y*>)) by A2, FUNCT_2:def_3;
rng I = the carrier of [:(product X),(product <*Y*>):] by A1, FUNCT_2:def_3;
then rng (J * I) = J .: the carrier of [:(product X),(product <*Y*>):] by RELAT_1:127
.= the carrier of (product (X ^ <*Y*>)) by A3, RELSET_1:22 ;
hence K is onto by FUNCT_2:def_3; ::_thesis: ( ( for x being Point of (product X)
for y being Point of Y ex x1, y1 being FinSequence st
( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),Y:] holds K . (v + w) = (K . v) + (K . w) ) & ( for v being Point of [:(product X),Y:]
for r being Element of REAL holds K . (r * v) = r * (K . v) ) & K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) )
thus for x being Point of (product X)
for y being Point of Y ex x1, y1 being FinSequence st
( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 ) ::_thesis: ( ( for v, w being Point of [:(product X),Y:] holds K . (v + w) = (K . v) + (K . w) ) & ( for v being Point of [:(product X),Y:]
for r being Element of REAL holds K . (r * v) = r * (K . v) ) & K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) )
proof
let x be Point of (product X); ::_thesis: for y being Point of Y ex x1, y1 being FinSequence st
( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 )
let y be Point of Y; ::_thesis: ex x1, y1 being FinSequence st
( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 )
A4: I . (x,y) = [x,<*y*>] by A1;
[x,y] in the carrier of [:(product X),Y:] ;
then [x,<*y*>] in the carrier of [:(product X),(product <*Y*>):] by A4, FUNCT_2:5;
then reconsider yy = <*y*> as Point of (product <*Y*>) by ZFMISC_1:87;
consider x1, y1 being FinSequence such that
A5: ( x = x1 & yy = y1 & J . (x,yy) = x1 ^ y1 ) by A2;
J . (x,yy) = J . (I . [x,y]) by A4
.= K . (x,y) by FUNCT_2:15 ;
hence ex x1, y1 being FinSequence st
( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 ) by A5; ::_thesis: verum
end;
thus for v, w being Point of [:(product X),Y:] holds K . (v + w) = (K . v) + (K . w) ::_thesis: ( ( for v being Point of [:(product X),Y:]
for r being Element of REAL holds K . (r * v) = r * (K . v) ) & K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) )
proof
let v, w be Point of [:(product X),Y:]; ::_thesis: K . (v + w) = (K . v) + (K . w)
thus K . (v + w) = J . (I . (v + w)) by FUNCT_2:15
.= J . ((I . v) + (I . w)) by A1
.= (J . (I . v)) + (J . (I . w)) by A2
.= (K . v) + (J . (I . w)) by FUNCT_2:15
.= (K . v) + (K . w) by FUNCT_2:15 ; ::_thesis: verum
end;
thus for v being Point of [:(product X),Y:]
for r being Element of REAL holds K . (r * v) = r * (K . v) ::_thesis: K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>))
proof
let v be Point of [:(product X),Y:]; ::_thesis: for r being Element of REAL holds K . (r * v) = r * (K . v)
let r be Element of REAL ; ::_thesis: K . (r * v) = r * (K . v)
thus K . (r * v) = J . (I . (r * v)) by FUNCT_2:15
.= J . (r * (I . v)) by A1
.= r * (J . (I . v)) by A2
.= r * (K . v) by FUNCT_2:15 ; ::_thesis: verum
end;
thus K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) by A1, A2, FUNCT_2:15; ::_thesis: verum
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.|| ) )
proof
let X, Y be RealNormSpace; ::_thesis: 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.|| ) )
consider J being Function of Y,(product <*Y*>) such that
A1: ( J is one-to-one & J is onto & ( for y being Point of Y holds J . y = <*y*> ) & ( for v, w being Point of Y holds J . (v + w) = (J . v) + (J . w) ) & ( for v being Point of Y
for r being Element of REAL holds J . (r * v) = r * (J . v) ) & J . (0. Y) = 0. (product <*Y*>) & ( for v being Point of Y holds ||.(J . v).|| = ||.v.|| ) ) by Th16;
defpred S1[ set , set , set ] means $3 = [$1,<*$2*>];
A2: for x, y being set st x in the carrier of X & y in the carrier of Y holds
ex z being set st
( z in the carrier of [:X,(product <*Y*>):] & S1[x,y,z] )
proof
let x, y be set ; ::_thesis: ( x in the carrier of X & y in the carrier of Y implies ex z being set st
( z in the carrier of [:X,(product <*Y*>):] & S1[x,y,z] ) )
assume A3: ( x in the carrier of X & y in the carrier of Y ) ; ::_thesis: ex z being set st
( z in the carrier of [:X,(product <*Y*>):] & S1[x,y,z] )
then reconsider y0 = y as Point of Y ;
J . y0 = <*y0*> by A1;
then [x,<*y*>] in [: the carrier of X, the carrier of (product <*Y*>):] by A3, ZFMISC_1:87;
hence ex z being set st
( z in the carrier of [:X,(product <*Y*>):] & S1[x,y,z] ) ; ::_thesis: verum
end;
consider I being Function of [: the carrier of X, the carrier of Y:], the carrier of [:X,(product <*Y*>):] such that
A4: for x, y being set st x in the carrier of X & y in the carrier of Y holds
S1[x,y,I . (x,y)] from BINOP_1:sch_1(A2);
reconsider I = I as Function of [:X,Y:],[:X,(product <*Y*>):] ;
take I ; ::_thesis: ( 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.|| ) )
thus I is one-to-one ::_thesis: ( 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
now__::_thesis:_for_z1,_z2_being_set_st_z1_in_the_carrier_of_[:X,Y:]_&_z2_in_the_carrier_of_[:X,Y:]_&_I_._z1_=_I_._z2_holds_
z1_=_z2
let z1, z2 be set ; ::_thesis: ( z1 in the carrier of [:X,Y:] & z2 in the carrier of [:X,Y:] & I . z1 = I . z2 implies z1 = z2 )
assume A5: ( z1 in the carrier of [:X,Y:] & z2 in the carrier of [:X,Y:] & I . z1 = I . z2 ) ; ::_thesis: z1 = z2
then consider x1, y1 being set such that
A6: ( x1 in the carrier of X & y1 in the carrier of Y & z1 = [x1,y1] ) by ZFMISC_1:def_2;
consider x2, y2 being set such that
A7: ( x2 in the carrier of X & y2 in the carrier of Y & z2 = [x2,y2] ) by A5, ZFMISC_1:def_2;
A8: [x1,<*y1*>] = I . (x1,y1) by A4, A6
.= I . (x2,y2) by A5, A6, A7
.= [x2,<*y2*>] by A4, A7 ;
then <*y1*> = <*y2*> by XTUPLE_0:1;
then y1 = y2 by FINSEQ_1:76;
hence z1 = z2 by A6, A7, A8, XTUPLE_0:1; ::_thesis: verum
end;
hence I is one-to-one by FUNCT_2:19; ::_thesis: verum
end;
thus I is onto ::_thesis: ( ( 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
now__::_thesis:_for_w_being_set_st_w_in_the_carrier_of_[:X,(product_<*Y*>):]_holds_
w_in_rng_I
let w be set ; ::_thesis: ( w in the carrier of [:X,(product <*Y*>):] implies w in rng I )
assume w in the carrier of [:X,(product <*Y*>):] ; ::_thesis: w in rng I
then consider x, y1 being set such that
A9: ( x in the carrier of X & y1 in the carrier of (product <*Y*>) & w = [x,y1] ) by ZFMISC_1:def_2;
y1 in rng J by A1, A9, FUNCT_2:def_3;
then consider y being set such that
A10: ( y in the carrier of Y & y1 = J . y ) by FUNCT_2:11;
A11: J . y = <*y*> by A10, A1;
reconsider z = [x,y] as Element of [: the carrier of X, the carrier of Y:] by A9, A10, ZFMISC_1:87;
w = I . (x,y) by A4, A9, A10, A11
.= I . z ;
hence w in rng I by FUNCT_2:4; ::_thesis: verum
end;
then the carrier of [:X,(product <*Y*>):] c= rng I by TARSKI:def_3;
then the carrier of [:X,(product <*Y*>):] = rng I by XBOOLE_0:def_10;
hence I is onto by FUNCT_2:def_3; ::_thesis: verum
end;
thus for x being Point of X
for y being Point of Y holds I . (x,y) = [x,<*y*>] by A4; ::_thesis: ( ( 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.|| ) )
thus for v, w being Point of [:X,Y:] holds I . (v + w) = (I . v) + (I . w) ::_thesis: ( ( 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
let v, w be Point of [:X,Y:]; ::_thesis: I . (v + w) = (I . v) + (I . w)
consider x1 being Point of X, x2 being Point of Y such that
A12: v = [x1,x2] by Lm1;
consider y1 being Point of X, y2 being Point of Y such that
A13: w = [y1,y2] by Lm1;
A14: I . (v + w) = I . ((x1 + y1),(x2 + y2)) by A12, A13, Def1
.= [(x1 + y1),<*(x2 + y2)*>] by A4 ;
( I . v = I . (x1,x2) & I . w = I . (y1,y2) ) by A12, A13;
then A15: ( I . v = [x1,<*x2*>] & I . w = [y1,<*y2*>] ) by A4;
A16: ( J . x2 = <*x2*> & J . y2 = <*y2*> ) by A1;
then reconsider xx2 = <*x2*> as Point of (product <*Y*>) ;
reconsider yy2 = <*y2*> as Point of (product <*Y*>) by A16;
<*(x2 + y2)*> = J . (x2 + y2) by A1
.= xx2 + yy2 by A16, A1 ;
hence (I . v) + (I . w) = I . (v + w) by A14, A15, Def1; ::_thesis: verum
end;
thus for v being Point of [:X,Y:]
for r being Element of REAL holds I . (r * v) = r * (I . v) ::_thesis: ( I . (0. [:X,Y:]) = 0. [:X,(product <*Y*>):] & ( for v being Point of [:X,Y:] holds ||.(I . v).|| = ||.v.|| ) )
proof
let v be Point of [:X,Y:]; ::_thesis: for r being Element of REAL holds I . (r * v) = r * (I . v)
let r be Element of REAL ; ::_thesis: I . (r * v) = r * (I . v)
consider x1 being Point of X, x2 being Point of Y such that
A17: v = [x1,x2] by Lm1;
A18: I . (r * v) = I . ((r * x1),(r * x2)) by A17, Th18
.= [(r * x1),<*(r * x2)*>] by A4 ;
A19: I . v = I . (x1,x2) by A17
.= [x1,<*x2*>] by A4 ;
A20: J . x2 = <*x2*> by A1;
then reconsider xx2 = <*x2*> as Point of (product <*Y*>) ;
<*(r * x2)*> = J . (r * x2) by A1
.= r * xx2 by A20, A1 ;
hence r * (I . v) = I . (r * v) by A18, A19, Th18; ::_thesis: verum
end;
A21: <*(0. Y)*> = 0. (product <*Y*>) by A1;
I . (0. [:X,Y:]) = I . ((0. X),(0. Y)) ;
hence I . (0. [:X,Y:]) = 0. [:X,(product <*Y*>):] by A21, A4; ::_thesis: for v being Point of [:X,Y:] holds ||.(I . v).|| = ||.v.||
thus for v being Point of [:X,Y:] holds ||.(I . v).|| = ||.v.|| ::_thesis: verum
proof
let v be Point of [:X,Y:]; ::_thesis: ||.(I . v).|| = ||.v.||
consider x1 being Point of X, x2 being Point of Y such that
A22: v = [x1,x2] by Lm1;
A23: J . x2 = <*x2*> by A1;
then reconsider xx2 = <*x2*> as Point of (product <*Y*>) ;
A24: ex w being Element of REAL 2 st
( w = <*||.x1.||,||.x2.||*> & ||.v.|| = |.w.| ) by A22, Th18;
I . v = I . (x1,x2) by A22
.= [x1,<*x2*>] by A4 ;
then ex s being Element of REAL 2 st
( s = <*||.x1.||,||.xx2.||*> & ||.(I . v).|| = |.s.| ) by Th18;
hence ||.(I . v).|| = ||.v.|| by A23, A1, A24; ::_thesis: verum
end;
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.|| ) )
proof
let X be RealNormSpace-Sequence; ::_thesis: 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.|| ) )
let Y be RealNormSpace; ::_thesis: 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.|| ) )
consider I being Function of [:(product X),Y:],[:(product X),(product <*Y*>):] such that
A1: ( I is one-to-one & I is onto & ( for x being Point of (product X)
for y being Point of Y holds I . (x,y) = [x,<*y*>] ) & ( 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),(product <*Y*>):] & ( for v being Point of [:(product X),Y:] holds ||.(I . v).|| = ||.v.|| ) ) by Th23;
consider J being Function of [:(product X),(product <*Y*>):],(product (X ^ <*Y*>)) such that
A2: ( J is one-to-one & J 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 & J . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),(product <*Y*>):] holds J . (v + w) = (J . v) + (J . w) ) & ( for v being Point of [:(product X),(product <*Y*>):]
for r being Element of REAL holds J . (r * v) = r * (J . v) ) & J . (0. [:(product X),(product <*Y*>):]) = 0. (product (X ^ <*Y*>)) & ( for v being Point of [:(product X),(product <*Y*>):] holds ||.(J . v).|| = ||.v.|| ) ) by Th17;
set K = J * I;
reconsider K = J * I as Function of [:(product X),Y:],(product (X ^ <*Y*>)) ;
take K ; ::_thesis: ( K is one-to-one & K 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 & K . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),Y:] holds K . (v + w) = (K . v) + (K . w) ) & ( for v being Point of [:(product X),Y:]
for r being Element of REAL holds K . (r * v) = r * (K . v) ) & K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) & ( for v being Point of [:(product X),Y:] holds ||.(K . v).|| = ||.v.|| ) )
thus K is one-to-one by A1, A2; ::_thesis: ( K 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 & K . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),Y:] holds K . (v + w) = (K . v) + (K . w) ) & ( for v being Point of [:(product X),Y:]
for r being Element of REAL holds K . (r * v) = r * (K . v) ) & K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) & ( for v being Point of [:(product X),Y:] holds ||.(K . v).|| = ||.v.|| ) )
A3: rng J = the carrier of (product (X ^ <*Y*>)) by A2, FUNCT_2:def_3;
rng I = the carrier of [:(product X),(product <*Y*>):] by A1, FUNCT_2:def_3;
then rng (J * I) = J .: the carrier of [:(product X),(product <*Y*>):] by RELAT_1:127
.= the carrier of (product (X ^ <*Y*>)) by A3, RELSET_1:22 ;
hence K is onto by FUNCT_2:def_3; ::_thesis: ( ( for x being Point of (product X)
for y being Point of Y ex x1, y1 being FinSequence st
( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),Y:] holds K . (v + w) = (K . v) + (K . w) ) & ( for v being Point of [:(product X),Y:]
for r being Element of REAL holds K . (r * v) = r * (K . v) ) & K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) & ( for v being Point of [:(product X),Y:] holds ||.(K . v).|| = ||.v.|| ) )
thus for x being Point of (product X)
for y being Point of Y ex x1, y1 being FinSequence st
( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 ) ::_thesis: ( ( for v, w being Point of [:(product X),Y:] holds K . (v + w) = (K . v) + (K . w) ) & ( for v being Point of [:(product X),Y:]
for r being Element of REAL holds K . (r * v) = r * (K . v) ) & K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) & ( for v being Point of [:(product X),Y:] holds ||.(K . v).|| = ||.v.|| ) )
proof
let x be Point of (product X); ::_thesis: for y being Point of Y ex x1, y1 being FinSequence st
( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 )
let y be Point of Y; ::_thesis: ex x1, y1 being FinSequence st
( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 )
A4: I . (x,y) = [x,<*y*>] by A1;
[x,y] in the carrier of [:(product X),Y:] ;
then [x,<*y*>] in the carrier of [:(product X),(product <*Y*>):] by A4, FUNCT_2:5;
then reconsider yy = <*y*> as Point of (product <*Y*>) by ZFMISC_1:87;
consider x1, y1 being FinSequence such that
A5: ( x = x1 & yy = y1 & J . (x,yy) = x1 ^ y1 ) by A2;
J . (x,yy) = J . (I . [x,y]) by A4
.= K . (x,y) by FUNCT_2:15 ;
hence ex x1, y1 being FinSequence st
( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 ) by A5; ::_thesis: verum
end;
thus for v, w being Point of [:(product X),Y:] holds K . (v + w) = (K . v) + (K . w) ::_thesis: ( ( for v being Point of [:(product X),Y:]
for r being Element of REAL holds K . (r * v) = r * (K . v) ) & K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) & ( for v being Point of [:(product X),Y:] holds ||.(K . v).|| = ||.v.|| ) )
proof
let v, w be Point of [:(product X),Y:]; ::_thesis: K . (v + w) = (K . v) + (K . w)
thus K . (v + w) = J . (I . (v + w)) by FUNCT_2:15
.= J . ((I . v) + (I . w)) by A1
.= (J . (I . v)) + (J . (I . w)) by A2
.= (K . v) + (J . (I . w)) by FUNCT_2:15
.= (K . v) + (K . w) by FUNCT_2:15 ; ::_thesis: verum
end;
thus for v being Point of [:(product X),Y:]
for r being Element of REAL holds K . (r * v) = r * (K . v) ::_thesis: ( K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) & ( for v being Point of [:(product X),Y:] holds ||.(K . v).|| = ||.v.|| ) )
proof
let v be Point of [:(product X),Y:]; ::_thesis: for r being Element of REAL holds K . (r * v) = r * (K . v)
let r be Element of REAL ; ::_thesis: K . (r * v) = r * (K . v)
thus K . (r * v) = J . (I . (r * v)) by FUNCT_2:15
.= J . (r * (I . v)) by A1
.= r * (J . (I . v)) by A2
.= r * (K . v) by FUNCT_2:15 ; ::_thesis: verum
end;
thus K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) by A1, A2, FUNCT_2:15; ::_thesis: for v being Point of [:(product X),Y:] holds ||.(K . v).|| = ||.v.||
thus for v being Point of [:(product X),Y:] holds ||.(K . v).|| = ||.v.|| ::_thesis: verum
proof
let v be Point of [:(product X),Y:]; ::_thesis: ||.(K . v).|| = ||.v.||
thus ||.(K . v).|| = ||.(J . (I . v)).|| by FUNCT_2:15
.= ||.(I . v).|| by A2
.= ||.v.|| by A1 ; ::_thesis: verum
end;
end;