:: MATRTOP1 semantic presentation
begin
registration
let X, Y be set ;
let F be positive-yielding PartFunc of X,REAL;
clusterF | Y -> positive-yielding ;
coherence
F | Y is positive-yielding
proof
let r be real number ; :: according to PARTFUN3:def_1 ::_thesis: ( not r in rng (F | Y) or not r <= 0 )
assume A1: r in rng (F | Y) ; ::_thesis: not r <= 0
rng (F | Y) c= rng F by RELAT_1:70;
hence not r <= 0 by A1, PARTFUN3:def_1; ::_thesis: verum
end;
end;
registration
let X, Y be set ;
let F be negative-yielding PartFunc of X,REAL;
clusterF | Y -> negative-yielding ;
coherence
F | Y is negative-yielding
proof
let r be real number ; :: according to PARTFUN3:def_2 ::_thesis: ( not r in rng (F | Y) or not 0 <= r )
assume A1: r in rng (F | Y) ; ::_thesis: not 0 <= r
rng (F | Y) c= rng F by RELAT_1:70;
hence not 0 <= r by A1, PARTFUN3:def_2; ::_thesis: verum
end;
end;
registration
let X, Y be set ;
let F be nonpositive-yielding PartFunc of X,REAL;
clusterF | Y -> nonpositive-yielding ;
coherence
F | Y is nonpositive-yielding
proof
let r be real number ; :: according to PARTFUN3:def_3 ::_thesis: ( not r in rng (F | Y) or r <= 0 )
assume A1: r in rng (F | Y) ; ::_thesis: r <= 0
rng (F | Y) c= rng F by RELAT_1:70;
hence r <= 0 by A1, PARTFUN3:def_3; ::_thesis: verum
end;
end;
registration
let X, Y be set ;
let F be nonnegative-yielding PartFunc of X,REAL;
clusterF | Y -> nonnegative-yielding ;
coherence
F | Y is nonnegative-yielding
proof
let r be real number ; :: according to PARTFUN3:def_4 ::_thesis: ( not r in rng (F | Y) or 0 <= r )
assume A1: r in rng (F | Y) ; ::_thesis: 0 <= r
rng (F | Y) c= rng F by RELAT_1:70;
hence 0 <= r by A1, PARTFUN3:def_4; ::_thesis: verum
end;
end;
registration
let rf be real-valued FinSequence;
cluster sqrt rf -> FinSequence-like ;
coherence
sqrt rf is FinSequence-like
proof
( dom rf = dom (sqrt rf) & ex n being Nat st dom rf = Seg n ) by FINSEQ_1:def_2, PARTFUN3:def_5;
hence sqrt rf is FinSequence-like by FINSEQ_1:def_2; ::_thesis: verum
end;
end;
definition
let rf be real-valued FinSequence;
func @ rf -> FinSequence of F_Real equals :: MATRTOP1:def 1
rf;
coherence
rf is FinSequence of F_Real
proof
rng rf c= REAL ;
hence rf is FinSequence of F_Real by FINSEQ_1:def_4; ::_thesis: verum
end;
end;
:: deftheorem defines @ MATRTOP1:def_1_:_
for rf being real-valued FinSequence holds @ rf = rf;
definition
let p be FinSequence of F_Real;
func @ p -> FinSequence of REAL equals :: MATRTOP1:def 2
p;
coherence
p is FinSequence of REAL ;
end;
:: deftheorem defines @ MATRTOP1:def_2_:_
for p being FinSequence of F_Real holds @ p = p;
theorem :: MATRTOP1:1
for rf1, rf2 being real-valued FinSequence holds (@ rf1) + (@ rf2) = rf1 + rf2 by RVSUM_1:def_4;
theorem Th2: :: MATRTOP1:2
for rf1, rf2 being real-valued FinSequence holds sqrt (rf1 ^ rf2) = (sqrt rf1) ^ (sqrt rf2)
proof
let rf1, rf2 be real-valued FinSequence; ::_thesis: sqrt (rf1 ^ rf2) = (sqrt rf1) ^ (sqrt rf2)
set rf12 = rf1 ^ rf2;
set s12 = sqrt (rf1 ^ rf2);
set s1 = sqrt rf1;
set s2 = sqrt rf2;
A1: dom (sqrt (rf1 ^ rf2)) = dom (rf1 ^ rf2) by PARTFUN3:def_5;
A2: dom (sqrt rf2) = dom rf2 by PARTFUN3:def_5;
then A3: len (sqrt rf2) = len rf2 by FINSEQ_3:29;
A4: dom (sqrt rf1) = dom rf1 by PARTFUN3:def_5;
then A5: len (sqrt rf1) = len rf1 by FINSEQ_3:29;
A6: for n being Nat st 1 <= n & n <= len (sqrt (rf1 ^ rf2)) holds
(sqrt (rf1 ^ rf2)) . n = ((sqrt rf1) ^ (sqrt rf2)) . n
proof
let n be Nat; ::_thesis: ( 1 <= n & n <= len (sqrt (rf1 ^ rf2)) implies (sqrt (rf1 ^ rf2)) . n = ((sqrt rf1) ^ (sqrt rf2)) . n )
assume ( 1 <= n & n <= len (sqrt (rf1 ^ rf2)) ) ; ::_thesis: (sqrt (rf1 ^ rf2)) . n = ((sqrt rf1) ^ (sqrt rf2)) . n
then A7: n in dom (sqrt (rf1 ^ rf2)) by FINSEQ_3:25;
then A8: (sqrt (rf1 ^ rf2)) . n = sqrt ((rf1 ^ rf2) . n) by PARTFUN3:def_5;
percases ( n in dom rf1 or ex m being Nat st
( m in dom rf2 & n = (len rf1) + m ) ) by A1, A7, FINSEQ_1:25;
supposeA9: n in dom rf1 ; ::_thesis: (sqrt (rf1 ^ rf2)) . n = ((sqrt rf1) ^ (sqrt rf2)) . n
then ( (rf1 ^ rf2) . n = rf1 . n & (sqrt rf1) . n = sqrt (rf1 . n) ) by A4, FINSEQ_1:def_7, PARTFUN3:def_5;
hence (sqrt (rf1 ^ rf2)) . n = ((sqrt rf1) ^ (sqrt rf2)) . n by A4, A8, A9, FINSEQ_1:def_7; ::_thesis: verum
end;
suppose ex m being Nat st
( m in dom rf2 & n = (len rf1) + m ) ; ::_thesis: (sqrt (rf1 ^ rf2)) . n = ((sqrt rf1) ^ (sqrt rf2)) . n
then consider m being Nat such that
A10: ( m in dom rf2 & n = (len rf1) + m ) ;
( (rf1 ^ rf2) . n = rf2 . m & (sqrt rf2) . m = sqrt (rf2 . m) ) by A2, A10, FINSEQ_1:def_7, PARTFUN3:def_5;
hence (sqrt (rf1 ^ rf2)) . n = ((sqrt rf1) ^ (sqrt rf2)) . n by A2, A5, A8, A10, FINSEQ_1:def_7; ::_thesis: verum
end;
end;
end;
len (sqrt (rf1 ^ rf2)) = len (rf1 ^ rf2) by A1, FINSEQ_3:29;
then len (sqrt (rf1 ^ rf2)) = (len (sqrt rf1)) + (len (sqrt rf2)) by A5, A3, FINSEQ_1:22;
then len (sqrt (rf1 ^ rf2)) = len ((sqrt rf1) ^ (sqrt rf2)) by FINSEQ_1:22;
hence sqrt (rf1 ^ rf2) = (sqrt rf1) ^ (sqrt rf2) by A6, FINSEQ_1:14; ::_thesis: verum
end;
theorem Th3: :: MATRTOP1:3
for r being real number holds sqrt <*r*> = <*(sqrt r)*>
proof
let r be real number ; ::_thesis: sqrt <*r*> = <*(sqrt r)*>
set R = <*r*>;
A1: <*r*> . 1 = r by FINSEQ_1:40;
A2: dom <*r*> = dom (sqrt <*r*>) by PARTFUN3:def_5;
then A3: len <*r*> = len (sqrt <*r*>) by FINSEQ_3:29;
( 1 in Seg 1 & dom <*r*> = Seg 1 ) by FINSEQ_1:38;
then ( len <*r*> = 1 & (sqrt <*r*>) . 1 = sqrt r ) by A2, A1, FINSEQ_1:40, PARTFUN3:def_5;
hence sqrt <*r*> = <*(sqrt r)*> by A3, FINSEQ_1:40; ::_thesis: verum
end;
theorem Th4: :: MATRTOP1:4
for rf being real-valued FinSequence holds sqrt (rf ^2) = abs rf
proof
let rf be real-valued FinSequence; ::_thesis: sqrt (rf ^2) = abs rf
set F = rf ^2 ;
set S = sqrt (rf ^2);
A1: dom (sqrt (rf ^2)) = dom (rf ^2) by PARTFUN3:def_5;
A2: ( dom (abs rf) = dom rf & dom (rf ^2) = dom rf ) by VALUED_1:11, VALUED_1:def_11;
now__::_thesis:_for_x_being_set_st_x_in_dom_(abs_rf)_holds_
(abs_rf)_._x_=_(sqrt_(rf_^2))_._x
let x be set ; ::_thesis: ( x in dom (abs rf) implies (abs rf) . x = (sqrt (rf ^2)) . x )
reconsider fx = rf . x as Real by XREAL_0:def_1;
A3: ( fx >= 0 or fx < 0 ) ;
assume A4: x in dom (abs rf) ; ::_thesis: (abs rf) . x = (sqrt (rf ^2)) . x
then ( (rf ^2) . x = fx ^2 & (sqrt (rf ^2)) . x = sqrt ((rf ^2) . x) ) by A2, A1, PARTFUN3:def_5, VALUED_1:11;
then A5: ( ( (sqrt (rf ^2)) . x = fx & fx >= 0 ) or ( (sqrt (rf ^2)) . x = - fx & fx < 0 ) ) by A3, SQUARE_1:22, SQUARE_1:23;
(abs rf) . x = abs fx by A4, VALUED_1:def_11;
hence (abs rf) . x = (sqrt (rf ^2)) . x by A5, ABSVALUE:def_1; ::_thesis: verum
end;
hence sqrt (rf ^2) = abs rf by A2, A1, FUNCT_1:2; ::_thesis: verum
end;
theorem Th5: :: MATRTOP1:5
for rf being real-valued FinSequence st rf is nonnegative-yielding holds
sqrt (Sum rf) <= Sum (sqrt rf)
proof
let rf be real-valued FinSequence; ::_thesis: ( rf is nonnegative-yielding implies sqrt (Sum rf) <= Sum (sqrt rf) )
defpred S1[ Nat] means for f being real-valued FinSequence st len f = $1 & f is nonnegative-yielding holds
( sqrt (Sum f) <= Sum (sqrt f) & 0 <= Sum f );
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
set n1 = n + 1;
let f be real-valued FinSequence; ::_thesis: ( len f = n + 1 & f is nonnegative-yielding implies ( sqrt (Sum f) <= Sum (sqrt f) & 0 <= Sum f ) )
assume that
A3: len f = n + 1 and
A4: f is nonnegative-yielding ; ::_thesis: ( sqrt (Sum f) <= Sum (sqrt f) & 0 <= Sum f )
rng f c= REAL ;
then reconsider F = f as FinSequence of REAL by FINSEQ_1:def_4;
reconsider fn = F | n as FinSequence of REAL ;
A5: F = fn ^ <*(F . (n + 1))*> by A3, FINSEQ_3:55;
then sqrt F = (sqrt fn) ^ (sqrt <*(F . (n + 1))*>) by Th2
.= (sqrt fn) ^ <*(sqrt (F . (n + 1)))*> by Th3 ;
then A6: Sum (sqrt F) = (Sum (sqrt fn)) + (sqrt (F . (n + 1))) by RVSUM_1:74;
A7: len fn = n by A3, FINSEQ_3:53;
then sqrt (Sum fn) <= Sum (sqrt fn) by A2, A4;
then A8: (sqrt (Sum fn)) + (sqrt (f . (n + 1))) <= Sum (sqrt F) by A6, XREAL_1:6;
A9: Sum f = (Sum fn) + (f . (n + 1)) by A5, RVSUM_1:74;
n + 1 >= 1 by NAT_1:11;
then n + 1 in dom f by A3, FINSEQ_3:25;
then f . (n + 1) in rng f by FUNCT_1:def_3;
then A10: f . (n + 1) >= 0 by A4, PARTFUN3:def_4;
A11: Sum fn >= 0 by A2, A4, A7;
then sqrt (Sum f) <= (sqrt (Sum fn)) + (sqrt (f . (n + 1))) by A9, A10, SQUARE_1:59;
hence ( sqrt (Sum f) <= Sum (sqrt f) & 0 <= Sum f ) by A9, A11, A10, A8, XXREAL_0:2; ::_thesis: verum
end;
A12: S1[ 0 ]
proof
let f be real-valued FinSequence; ::_thesis: ( len f = 0 & f is nonnegative-yielding implies ( sqrt (Sum f) <= Sum (sqrt f) & 0 <= Sum f ) )
assume that
A13: len f = 0 and
f is nonnegative-yielding ; ::_thesis: ( sqrt (Sum f) <= Sum (sqrt f) & 0 <= Sum f )
dom f = dom (sqrt f) by PARTFUN3:def_5;
then len f = len (sqrt f) by FINSEQ_3:29;
then A14: sqrt f = <*> REAL by A13;
f = <*> REAL by A13;
hence ( sqrt (Sum f) <= Sum (sqrt f) & 0 <= Sum f ) by A14, RVSUM_1:72, SQUARE_1:17; ::_thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch_2(A12, A1);
then S1[ len rf] ;
hence ( rf is nonnegative-yielding implies sqrt (Sum rf) <= Sum (sqrt rf) ) ; ::_thesis: verum
end;
theorem :: MATRTOP1:6
for F being Function ex X being set st
( X c= dom F & rng F = rng (F | X) & F | X is one-to-one )
proof
let F be Function; ::_thesis: ex X being set st
( X c= dom F & rng F = rng (F | X) & F | X is one-to-one )
defpred S1[ set , set ] means F . $2 = $1;
A1: for x being set st x in rng F holds
ex y being set st
( y in dom F & S1[x,y] ) by FUNCT_1:def_3;
consider g being Function of (rng F),(dom F) such that
A2: for x being set st x in rng F holds
S1[x,g . x] from FUNCT_2:sch_1(A1);
take X = rng g; ::_thesis: ( X c= dom F & rng F = rng (F | X) & F | X is one-to-one )
set FX = F | X;
( dom F = {} iff rng F = {} ) by RELAT_1:42;
then A3: dom g = rng F by FUNCT_2:def_1;
thus A4: X c= dom F by RELAT_1:def_19; ::_thesis: ( rng F = rng (F | X) & F | X is one-to-one )
A5: rng F c= rng (F | X)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng F or y in rng (F | X) )
assume y in rng F ; ::_thesis: y in rng (F | X)
then ( g . y in X & F . (g . y) = y ) by A2, A3, FUNCT_1:def_3;
hence y in rng (F | X) by A4, FUNCT_1:50; ::_thesis: verum
end;
rng (F | X) c= rng F by RELAT_1:70;
hence rng F = rng (F | X) by A5, XBOOLE_0:def_10; ::_thesis: F | X is one-to-one
now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_(F_|_X)_&_x2_in_dom_(F_|_X)_&_(F_|_X)_._x1_=_(F_|_X)_._x2_holds_
x1_=_x2
let x1, x2 be set ; ::_thesis: ( x1 in dom (F | X) & x2 in dom (F | X) & (F | X) . x1 = (F | X) . x2 implies x1 = x2 )
assume that
A6: x1 in dom (F | X) and
A7: x2 in dom (F | X) and
A8: (F | X) . x1 = (F | X) . x2 ; ::_thesis: x1 = x2
A9: ( (F | X) . x1 = F . x1 & (F | X) . x2 = F . x2 ) by A6, A7, FUNCT_1:47;
A10: dom (F | X) c= X by RELAT_1:58;
then consider y1 being set such that
A11: y1 in dom g and
A12: g . y1 = x1 by A6, FUNCT_1:def_3;
consider y2 being set such that
A13: ( y2 in dom g & g . y2 = x2 ) by A7, A10, FUNCT_1:def_3;
F . x1 = y1 by A2, A3, A11, A12;
hence x1 = x2 by A2, A3, A8, A9, A12, A13; ::_thesis: verum
end;
hence F | X is one-to-one by FUNCT_1:def_4; ::_thesis: verum
end;
registration
let cf be complex-valued FinSequence;
let X be set ;
clustercf - X -> complex-valued ;
coherence
cf - X is complex-valued
proof
( rng cf c= COMPLEX & rng (cf - X) c= rng cf ) by FINSEQ_3:66, VALUED_0:def_1;
then rng (cf - X) c= COMPLEX by XBOOLE_1:1;
hence cf - X is complex-valued by VALUED_0:def_1; ::_thesis: verum
end;
end;
registration
let rf be real-valued FinSequence;
let X be set ;
clusterrf - X -> real-valued ;
coherence
rf - X is real-valued
proof
rng (rf - X) c= rng rf by FINSEQ_3:66;
then rng (rf - X) c= REAL by XBOOLE_1:1;
hence rf - X is real-valued by VALUED_0:def_3; ::_thesis: verum
end;
end;
registration
let cf be complex-valued FinSubsequence;
cluster Seq cf -> complex-valued ;
coherence
Seq cf is complex-valued ;
end;
registration
let rf be real-valued FinSubsequence;
cluster Seq rf -> real-valued ;
coherence
Seq rf is real-valued ;
end;
theorem Th7: :: MATRTOP1:7
for X being set
for f, f1 being FinSequence
for P being Permutation of (dom f) st f1 = f * P holds
ex Q being Permutation of (dom (f - X)) st f1 - X = (f - X) * Q
proof
let X be set ; ::_thesis: for f, f1 being FinSequence
for P being Permutation of (dom f) st f1 = f * P holds
ex Q being Permutation of (dom (f - X)) st f1 - X = (f - X) * Q
let f, f1 be FinSequence; ::_thesis: for P being Permutation of (dom f) st f1 = f * P holds
ex Q being Permutation of (dom (f - X)) st f1 - X = (f - X) * Q
let P be Permutation of (dom f); ::_thesis: ( f1 = f * P implies ex Q being Permutation of (dom (f - X)) st f1 - X = (f - X) * Q )
assume A1: f1 = f * P ; ::_thesis: ex Q being Permutation of (dom (f - X)) st f1 - X = (f - X) * Q
reconsider p = P as one-to-one Function ;
A2: rng P = dom f by FUNCT_2:def_3;
then A3: dom (p ") = dom f by FUNCT_1:33;
A4: P .: (f1 " X) = P .: (P " (f " X)) by A1, RELAT_1:146
.= f " X by A2, FUNCT_1:77, RELAT_1:132 ;
A5: dom P = dom f by FUNCT_2:52;
then A6: dom f1 = dom f by A1, A2, RELAT_1:27;
set DfX = (dom f1) \ (f1 " X);
set DX = (dom f) \ (f " X);
A7: card ((dom f) \ (f " X)) = (card (dom f)) - (card (f " X)) by CARD_2:44, RELAT_1:132;
A8: dom f = Seg (len f) by FINSEQ_1:def_3;
then A9: dom (Sgm ((dom f) \ (f " X))) = Seg (card ((dom f) \ (f " X))) by FINSEQ_3:40, XBOOLE_1:36;
A10: p " (f " X) = (p ") .: (f " X) by FUNCT_1:85;
f1 " X = P " (f " X) by A1, RELAT_1:146;
then A11: f " X,f1 " X are_equipotent by A3, A10, CARD_1:33, RELAT_1:132;
A12: (dom f1) \ (f1 " X) c= dom f1 by XBOOLE_1:36;
A13: rng (P * (Sgm ((dom f1) \ (f1 " X)))) = P .: (rng (Sgm ((dom f1) \ (f1 " X)))) by RELAT_1:127
.= P .: ((dom f1) \ (f1 " X)) by A6, A8, A12, FINSEQ_1:def_13
.= (P .: (dom P)) \ (P .: (f1 " X)) by A5, A6, FUNCT_1:64
.= (dom f) \ (f " X) by A4, A2, RELAT_1:113 ;
reconsider SDX = Sgm ((dom f) \ (f " X)) as one-to-one Function by A8, FINSEQ_3:92, XBOOLE_1:36;
A14: dom (SDX ") = rng SDX by FUNCT_1:33;
card (dom f) = len f by CARD_1:62;
then A15: dom (f - X) = dom SDX by A7, A9, FINSEQ_3:62;
card ((dom f1) \ (f1 " X)) = (card (dom f1)) - (card (f1 " X)) by CARD_2:44, RELAT_1:132;
then card ((dom f) \ (f " X)) = card ((dom f1) \ (f1 " X)) by A11, A6, A7, CARD_1:5;
then A16: dom SDX = dom (Sgm ((dom f1) \ (f1 " X))) by A6, A8, A9, FINSEQ_3:40, XBOOLE_1:36;
(dom f) \ (f " X) c= dom f by XBOOLE_1:36;
then A17: rng (Sgm ((dom f) \ (f " X))) = (dom f) \ (f " X) by A8, FINSEQ_1:def_13;
rng (SDX ") = dom SDX by FUNCT_1:33;
then A18: rng ((SDX ") * (P * (Sgm ((dom f1) \ (f1 " X))))) = dom SDX by A17, A14, A13, RELAT_1:28;
rng (Sgm ((dom f1) \ (f1 " X))) = (dom f1) \ (f1 " X) by A6, A8, A12, FINSEQ_1:def_13;
then dom (P * (Sgm ((dom f1) \ (f1 " X)))) = dom (Sgm ((dom f1) \ (f1 " X))) by A5, A6, RELAT_1:27, XBOOLE_1:36;
then dom ((SDX ") * (P * (Sgm ((dom f1) \ (f1 " X))))) = dom (Sgm ((dom f1) \ (f1 " X))) by A17, A14, A13, RELAT_1:27;
then reconsider Q = (SDX ") * (P * (Sgm ((dom f1) \ (f1 " X)))) as Function of (dom (f - X)),(dom (f - X)) by A18, A15, A16, FUNCT_2:1;
A19: Q is onto by A18, A15, FUNCT_2:def_3;
Sgm ((dom f1) \ (f1 " X)) is one-to-one by A6, A8, FINSEQ_3:92, XBOOLE_1:36;
then reconsider Q = Q as Permutation of (dom (f - X)) by A19;
SDX * (SDX ") = id ((dom f) \ (f " X)) by A17, FUNCT_1:39;
then A20: SDX * Q = (id ((dom f) \ (f " X))) * (P * (Sgm ((dom f1) \ (f1 " X)))) by RELAT_1:36
.= P * (Sgm ((dom f1) \ (f1 " X))) by A13, RELAT_1:53 ;
(f - X) * Q = (f * SDX) * Q by FINSEQ_3:def_1
.= f * (P * (Sgm ((dom f1) \ (f1 " X)))) by A20, RELAT_1:36
.= f1 * (Sgm ((dom f1) \ (f1 " X))) by A1, RELAT_1:36
.= f1 - X by FINSEQ_3:def_1 ;
hence ex Q being Permutation of (dom (f - X)) st f1 - X = (f - X) * Q ; ::_thesis: verum
end;
theorem :: MATRTOP1:8
for X being set
for cf, cf1 being complex-valued FinSequence
for P being Permutation of (dom cf) st cf1 = cf * P holds
Sum (cf1 - X) = Sum (cf - X)
proof
let X be set ; ::_thesis: for cf, cf1 being complex-valued FinSequence
for P being Permutation of (dom cf) st cf1 = cf * P holds
Sum (cf1 - X) = Sum (cf - X)
let cf, cf1 be complex-valued FinSequence; ::_thesis: for P being Permutation of (dom cf) st cf1 = cf * P holds
Sum (cf1 - X) = Sum (cf - X)
rng (cf1 - X) c= COMPLEX by VALUED_0:def_1;
then reconsider fPX = cf1 - X as FinSequence of COMPLEX by FINSEQ_1:def_4;
rng (cf - X) c= COMPLEX by VALUED_0:def_1;
then reconsider fX = cf - X as FinSequence of COMPLEX by FINSEQ_1:def_4;
let P be Permutation of (dom cf); ::_thesis: ( cf1 = cf * P implies Sum (cf1 - X) = Sum (cf - X) )
assume A1: cf1 = cf * P ; ::_thesis: Sum (cf1 - X) = Sum (cf - X)
consider Q being Permutation of (dom (cf - X)) such that
A2: cf1 - X = (cf - X) * Q by A1, Th7;
thus Sum (cf1 - X) = addcomplex "**" fPX by RVSUM_1:def_11
.= addcomplex "**" fX by A2, FINSOP_1:7
.= Sum (cf - X) by RVSUM_1:def_11 ; ::_thesis: verum
end;
theorem Th9: :: MATRTOP1:9
for X being set
for f, f1 being FinSubsequence
for P being Permutation of (dom f) st f1 = f * P holds
ex Q being Permutation of (dom (Seq (f1 | (P " X)))) st Seq (f | X) = (Seq (f1 | (P " X))) * Q
proof
let X be set ; ::_thesis: for f, f1 being FinSubsequence
for P being Permutation of (dom f) st f1 = f * P holds
ex Q being Permutation of (dom (Seq (f1 | (P " X)))) st Seq (f | X) = (Seq (f1 | (P " X))) * Q
let f, f1 be FinSubsequence; ::_thesis: for P being Permutation of (dom f) st f1 = f * P holds
ex Q being Permutation of (dom (Seq (f1 | (P " X)))) st Seq (f | X) = (Seq (f1 | (P " X))) * Q
consider n being Nat such that
A1: dom f c= Seg n by FINSEQ_1:def_12;
let P be Permutation of (dom f); ::_thesis: ( f1 = f * P implies ex Q being Permutation of (dom (Seq (f1 | (P " X)))) st Seq (f | X) = (Seq (f1 | (P " X))) * Q )
assume A2: f1 = f * P ; ::_thesis: ex Q being Permutation of (dom (Seq (f1 | (P " X)))) st Seq (f | X) = (Seq (f1 | (P " X))) * Q
set SPX = Sgm (P " X);
A3: P " X c= dom P by RELAT_1:132;
then A4: dom (P | (P " X)) = P " X by RELAT_1:62;
A5: dom P = dom f by FUNCT_2:52;
then A6: Sgm (P " X) is one-to-one by A1, A3, FINSEQ_3:92, XBOOLE_1:1;
set dfX = (dom f) /\ X;
set SdX = Sgm ((dom f) /\ X);
A7: (dom f) /\ X c= dom f by XBOOLE_1:17;
then (dom f) /\ X c= Seg n by A1, XBOOLE_1:1;
then A8: rng (Sgm ((dom f) /\ X)) = (dom f) /\ X by FINSEQ_1:def_13;
A9: rng P = dom f by FUNCT_2:def_3;
then A10: P " X = P " ((dom f) /\ X) by RELAT_1:133;
then A11: P " X = (P ") .: ((dom f) /\ X) by FUNCT_1:85;
set PS = (P | (P " X)) * (Sgm (P " X));
A12: P | (P " X) is one-to-one by FUNCT_1:52;
P " X c= Seg n by A1, A5, A3, XBOOLE_1:1;
then A13: rng (Sgm (P " X)) = P " X by FINSEQ_1:def_13;
rng (P | (P " X)) = P .: (P " ((dom f) /\ X)) by A10, RELAT_1:115
.= (dom f) /\ X by A9, FUNCT_1:77, XBOOLE_1:17 ;
then A14: rng ((P | (P " X)) * (Sgm (P " X))) = (dom f) /\ X by A4, A13, RELAT_1:28;
A15: dom (((P | (P " X)) * (Sgm (P " X))) ") = (dom f) /\ X by A6, A12, FUNCT_1:33, A14;
dom (P ") = rng P by FUNCT_1:33;
then (dom f) /\ X,(P ") .: ((dom f) /\ X) are_equipotent by A9, CARD_1:33, XBOOLE_1:17;
then card ((dom f) /\ X) = card (P " X) by A11, CARD_1:5;
then A16: dom (Sgm (P " X)) = Seg (card ((dom f) /\ X)) by A1, A5, A3, FINSEQ_3:40, XBOOLE_1:1;
then dom ((P | (P " X)) * (Sgm (P " X))) = Seg (card ((dom f) /\ X)) by A4, A13, RELAT_1:27;
then rng (((P | (P " X)) * (Sgm (P " X))) ") = Seg (card ((dom f) /\ X)) by A6, A12, FUNCT_1:33;
then A17: rng ((((P | (P " X)) * (Sgm (P " X))) ") * (Sgm ((dom f) /\ X))) = Seg (card ((dom f) /\ X)) by A15, A8, RELAT_1:28;
dom f1 = dom P by A2, A9, RELAT_1:27;
then A18: dom (f1 | (P " X)) = P " X by RELAT_1:62, RELAT_1:132;
then A19: dom (Seq (f1 | (P " X))) = Seg (card ((dom f) /\ X)) by A16, A13, RELAT_1:27;
dom (Sgm ((dom f) /\ X)) = Seg (card ((dom f) /\ X)) by A1, A7, FINSEQ_3:40, XBOOLE_1:1;
then dom ((((P | (P " X)) * (Sgm (P " X))) ") * (Sgm ((dom f) /\ X))) = Seg (card ((dom f) /\ X)) by A15, A8, RELAT_1:27;
then reconsider PSS = (((P | (P " X)) * (Sgm (P " X))) ") * (Sgm ((dom f) /\ X)) as Function of (dom (Seq (f1 | (P " X)))),(dom (Seq (f1 | (P " X)))) by A19, A17, FUNCT_2:1;
A20: PSS is onto by A19, A17, FUNCT_2:def_3;
Sgm ((dom f) /\ X) is one-to-one by A1, A7, FINSEQ_3:92, XBOOLE_1:1;
then reconsider PSS = PSS as Permutation of (dom (Seq (f1 | (P " X)))) by A6, A12, A20;
A21: ((P | (P " X)) * (Sgm (P " X))) * PSS = (((P | (P " X)) * (Sgm (P " X))) * (((P | (P " X)) * (Sgm (P " X))) ")) * (Sgm ((dom f) /\ X)) by RELAT_1:36
.= (id ((dom f) /\ X)) * (Sgm ((dom f) /\ X)) by A6, A12, A14, FUNCT_1:39 ;
set fX = f | X;
A22: f | X = f | ((dom f) /\ X) by RELAT_1:157;
take PSS ; ::_thesis: Seq (f | X) = (Seq (f1 | (P " X))) * PSS
f1 | (P " X) = f * (P | (P " X)) by A2, RELAT_1:83;
hence (Seq (f1 | (P " X))) * PSS = (f * ((P | (P " X)) * (Sgm (P " X)))) * PSS by A18, RELAT_1:36
.= f * ((id ((dom f) /\ X)) * (Sgm ((dom f) /\ X))) by A21, RELAT_1:36
.= (f * (id ((dom f) /\ X))) * (Sgm ((dom f) /\ X)) by RELAT_1:36
.= (f | X) * (Sgm ((dom f) /\ X)) by A22, RELAT_1:65
.= Seq (f | X) by RELAT_1:61 ;
::_thesis: verum
end;
theorem :: MATRTOP1:10
for X being set
for cf, cf1 being complex-valued FinSubsequence
for P being Permutation of (dom cf) st cf1 = cf * P holds
Sum (Seq (cf | X)) = Sum (Seq (cf1 | (P " X)))
proof
let X be set ; ::_thesis: for cf, cf1 being complex-valued FinSubsequence
for P being Permutation of (dom cf) st cf1 = cf * P holds
Sum (Seq (cf | X)) = Sum (Seq (cf1 | (P " X)))
let cf, cf1 be complex-valued FinSubsequence; ::_thesis: for P being Permutation of (dom cf) st cf1 = cf * P holds
Sum (Seq (cf | X)) = Sum (Seq (cf1 | (P " X)))
rng (Seq (cf | X)) c= COMPLEX by VALUED_0:def_1;
then reconsider SfX = Seq (cf | X) as FinSequence of COMPLEX by FINSEQ_1:def_4;
let P be Permutation of (dom cf); ::_thesis: ( cf1 = cf * P implies Sum (Seq (cf | X)) = Sum (Seq (cf1 | (P " X))) )
assume A1: cf1 = cf * P ; ::_thesis: Sum (Seq (cf | X)) = Sum (Seq (cf1 | (P " X)))
consider Q being Permutation of (dom (Seq (cf1 | (P " X)))) such that
A2: Seq (cf | X) = (Seq (cf1 | (P " X))) * Q by A1, Th9;
rng (Seq (cf1 | (P " X))) c= COMPLEX by VALUED_0:def_1;
then reconsider SfPX = Seq (cf1 | (P " X)) as FinSequence of COMPLEX by FINSEQ_1:def_4;
thus Sum (Seq (cf1 | (P " X))) = addcomplex "**" SfPX by RVSUM_1:def_11
.= addcomplex "**" SfX by A2, FINSOP_1:7
.= Sum (Seq (cf | X)) by RVSUM_1:def_11 ; ::_thesis: verum
end;
theorem Th11: :: MATRTOP1:11
for X, Y being set
for f being FinSubsequence
for n being Element of NAT st ( for i being Nat holds
( i + n in X iff i in Y ) ) holds
(n Shift f) | X = n Shift (f | Y)
proof
let X, Y be set ; ::_thesis: for f being FinSubsequence
for n being Element of NAT st ( for i being Nat holds
( i + n in X iff i in Y ) ) holds
(n Shift f) | X = n Shift (f | Y)
let f be FinSubsequence; ::_thesis: for n being Element of NAT st ( for i being Nat holds
( i + n in X iff i in Y ) ) holds
(n Shift f) | X = n Shift (f | Y)
let n be Element of NAT ; ::_thesis: ( ( for i being Nat holds
( i + n in X iff i in Y ) ) implies (n Shift f) | X = n Shift (f | Y) )
assume A1: for i being Nat holds
( i + n in X iff i in Y ) ; ::_thesis: (n Shift f) | X = n Shift (f | Y)
set fY = f | Y;
set nf = n Shift f;
set nfX = (n Shift f) | X;
set nfY = n Shift (f | Y);
A2: dom (n Shift (f | Y)) = { (n + k) where k is Element of NAT : k in dom (f | Y) } by PNPROC_1:def_14;
A3: now__::_thesis:_for_x_being_set_st_x_in_dom_(n_Shift_(f_|_Y))_holds_
((n_Shift_f)_|_X)_._x_=_(n_Shift_(f_|_Y))_._x
let x be set ; ::_thesis: ( x in dom (n Shift (f | Y)) implies ((n Shift f) | X) . x = (n Shift (f | Y)) . x )
assume x in dom (n Shift (f | Y)) ; ::_thesis: ((n Shift f) | X) . x = (n Shift (f | Y)) . x
then consider k being Element of NAT such that
A4: x = n + k and
A5: k in dom (f | Y) by A2;
A6: k in dom f by A5, RELAT_1:57;
A7: k in Y by A5, RELAT_1:57;
then x in X by A1, A4;
hence ((n Shift f) | X) . x = (n Shift f) . x by FUNCT_1:49
.= f . k by A4, A6, PNPROC_1:def_14
.= (f | Y) . k by A7, FUNCT_1:49
.= (n Shift (f | Y)) . x by A4, A5, PNPROC_1:def_14 ;
::_thesis: verum
end;
A8: dom (n Shift f) = { (n + k) where k is Element of NAT : k in dom f } by PNPROC_1:def_14;
A9: dom (n Shift (f | Y)) c= dom ((n Shift f) | X)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (n Shift (f | Y)) or x in dom ((n Shift f) | X) )
assume x in dom (n Shift (f | Y)) ; ::_thesis: x in dom ((n Shift f) | X)
then consider k being Element of NAT such that
A10: x = n + k and
A11: k in dom (f | Y) by A2;
k in Y by A11, RELAT_1:57;
then A12: x in X by A1, A10;
k in dom f by A11, RELAT_1:57;
then x in dom (n Shift f) by A8, A10;
hence x in dom ((n Shift f) | X) by A12, RELAT_1:57; ::_thesis: verum
end;
dom ((n Shift f) | X) c= dom (n Shift (f | Y))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom ((n Shift f) | X) or x in dom (n Shift (f | Y)) )
assume A13: x in dom ((n Shift f) | X) ; ::_thesis: x in dom (n Shift (f | Y))
then x in dom (n Shift f) by RELAT_1:57;
then consider k being Element of NAT such that
A14: x = n + k and
A15: k in dom f by A8;
x in X by A13, RELAT_1:57;
then k in Y by A1, A14;
then k in dom (f | Y) by A15, RELAT_1:57;
hence x in dom (n Shift (f | Y)) by A2, A14; ::_thesis: verum
end;
then dom (n Shift (f | Y)) = dom ((n Shift f) | X) by A9, XBOOLE_0:def_10;
hence (n Shift f) | X = n Shift (f | Y) by A3, FUNCT_1:2; ::_thesis: verum
end;
theorem Th12: :: MATRTOP1:12
for X being set
for f1, f2 being FinSequence ex Y being Subset of NAT st
( Seq ((f1 ^ f2) | X) = (Seq (f1 | X)) ^ (Seq (f2 | Y)) & ( for n being Nat st n > 0 holds
( n in Y iff n + (len f1) in X /\ (dom (f1 ^ f2)) ) ) )
proof
let X be set ; ::_thesis: for f1, f2 being FinSequence ex Y being Subset of NAT st
( Seq ((f1 ^ f2) | X) = (Seq (f1 | X)) ^ (Seq (f2 | Y)) & ( for n being Nat st n > 0 holds
( n in Y iff n + (len f1) in X /\ (dom (f1 ^ f2)) ) ) )
let f1, f2 be FinSequence; ::_thesis: ex Y being Subset of NAT st
( Seq ((f1 ^ f2) | X) = (Seq (f1 | X)) ^ (Seq (f2 | Y)) & ( for n being Nat st n > 0 holds
( n in Y iff n + (len f1) in X /\ (dom (f1 ^ f2)) ) ) )
set f12 = f1 ^ f2;
set n1 = len f1;
set n2 = len f2;
set X12 = X /\ (dom (f1 ^ f2));
set X1 = (X /\ (dom (f1 ^ f2))) /\ (Seg (len f1));
set X2 = (X /\ (dom (f1 ^ f2))) \ (Seg (len f1));
set Y2 = { i where i is Element of NAT : i + (len f1) in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) } ;
{ i where i is Element of NAT : i + (len f1) in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) } c= NAT
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { i where i is Element of NAT : i + (len f1) in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) } or x in NAT )
assume x in { i where i is Element of NAT : i + (len f1) in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) } ; ::_thesis: x in NAT
then ex i being Element of NAT st
( i = x & i + (len f1) in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) ) ;
hence x in NAT ; ::_thesis: verum
end;
then reconsider Y2 = { i where i is Element of NAT : i + (len f1) in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) } as Subset of NAT ;
set Sf2 = (len f1) Shift f2;
A1: f1 ^ f2 = f1 \/ ((len f1) Shift f2) by PNPROC_1:61;
take Y2 ; ::_thesis: ( Seq ((f1 ^ f2) | X) = (Seq (f1 | X)) ^ (Seq (f2 | Y2)) & ( for n being Nat st n > 0 holds
( n in Y2 iff n + (len f1) in X /\ (dom (f1 ^ f2)) ) ) )
A2: (X /\ (dom (f1 ^ f2))) /\ (dom ((len f1) Shift f2)) c= (X /\ (dom (f1 ^ f2))) \ (Seg (len f1))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X /\ (dom (f1 ^ f2))) /\ (dom ((len f1) Shift f2)) or x in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) )
assume A3: x in (X /\ (dom (f1 ^ f2))) /\ (dom ((len f1) Shift f2)) ; ::_thesis: x in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1))
then x in dom ((len f1) Shift f2) by XBOOLE_0:def_4;
then x in { ((len f1) + k) where k is Element of NAT : k in dom f2 } by PNPROC_1:def_14;
then consider k being Element of NAT such that
A4: x = (len f1) + k and
A5: k in dom f2 ;
1 <= k by A5, FINSEQ_3:25;
then 1 + (len f1) <= k + (len f1) by XREAL_1:6;
then len f1 < k + (len f1) by NAT_1:13;
then A6: not x in Seg (len f1) by A4, FINSEQ_1:1;
x in X /\ (dom (f1 ^ f2)) by A3, XBOOLE_0:def_4;
hence x in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) by A6, XBOOLE_0:def_5; ::_thesis: verum
end;
A7: now__::_thesis:_for_i_being_Nat_holds_
(_(_i_+_(len_f1)_in_(X_/\_(dom_(f1_^_f2)))_\_(Seg_(len_f1))_implies_i_in_Y2_)_&_(_i_in_Y2_implies_i_+_(len_f1)_in_(X_/\_(dom_(f1_^_f2)))_\_(Seg_(len_f1))_)_)
let i be Nat; ::_thesis: ( ( i + (len f1) in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) implies i in Y2 ) & ( i in Y2 implies i + (len f1) in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) ) )
thus ( i + (len f1) in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) implies i in Y2 ) ::_thesis: ( i in Y2 implies i + (len f1) in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) )
proof
assume A8: i + (len f1) in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) ; ::_thesis: i in Y2
i in NAT by ORDINAL1:def_12;
hence i in Y2 by A8; ::_thesis: verum
end;
assume i in Y2 ; ::_thesis: i + (len f1) in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1))
then ex j being Element of NAT st
( i = j & j + (len f1) in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) ) ;
hence i + (len f1) in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) ; ::_thesis: verum
end;
( f1 | ((X /\ (dom (f1 ^ f2))) /\ (Seg (len f1))) c= f1 & f2 | Y2 c= f2 ) by RELAT_1:59;
then consider ss being FinSubsequence such that
A9: ( ss = (f1 | ((X /\ (dom (f1 ^ f2))) /\ (Seg (len f1)))) \/ ((len f1) Shift (f2 | Y2)) & (Seq (f1 | ((X /\ (dom (f1 ^ f2))) /\ (Seg (len f1))))) ^ (Seq (f2 | Y2)) = Seq ss ) by PNPROC_1:79;
A10: dom f1 = Seg (len f1) by FINSEQ_1:def_3;
then (dom (f1 ^ f2)) /\ (Seg (len f1)) = Seg (len f1) by FINSEQ_1:26, XBOOLE_1:28;
then A11: f1 | X = f1 | (X /\ ((dom (f1 ^ f2)) /\ (Seg (len f1)))) by A10, RELAT_1:157
.= f1 | ((X /\ (dom (f1 ^ f2))) /\ (Seg (len f1))) by XBOOLE_1:16 ;
(X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) c= (X /\ (dom (f1 ^ f2))) /\ (dom ((len f1) Shift f2))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) or x in (X /\ (dom (f1 ^ f2))) /\ (dom ((len f1) Shift f2)) )
assume A12: x in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) ; ::_thesis: x in (X /\ (dom (f1 ^ f2))) /\ (dom ((len f1) Shift f2))
then A13: not x in Seg (len f1) by XBOOLE_0:def_5;
A14: x in X /\ (dom (f1 ^ f2)) by A12, XBOOLE_0:def_5;
then x in dom (f1 ^ f2) by XBOOLE_0:def_4;
then consider k being Nat such that
A15: ( k in dom f2 & x = (len f1) + k ) by A10, A13, FINSEQ_1:25;
x in { ((len f1) + i) where i is Element of NAT : i in dom f2 } by A15;
then x in dom ((len f1) Shift f2) by PNPROC_1:def_14;
hence x in (X /\ (dom (f1 ^ f2))) /\ (dom ((len f1) Shift f2)) by A14, XBOOLE_0:def_4; ::_thesis: verum
end;
then A16: (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) = (X /\ (dom (f1 ^ f2))) /\ (dom ((len f1) Shift f2)) by A2, XBOOLE_0:def_10;
(f1 ^ f2) | X = (f1 ^ f2) | (X /\ (dom (f1 ^ f2))) by RELAT_1:157;
then (f1 ^ f2) | X = (f1 ^ f2) * (id (X /\ (dom (f1 ^ f2)))) by RELAT_1:65
.= (f1 * (id (X /\ (dom (f1 ^ f2))))) \/ (((len f1) Shift f2) * (id (X /\ (dom (f1 ^ f2))))) by A1, RELAT_1:32
.= (f1 | (X /\ (dom (f1 ^ f2)))) \/ (((len f1) Shift f2) * (id (X /\ (dom (f1 ^ f2))))) by RELAT_1:65
.= (f1 | (X /\ (dom (f1 ^ f2)))) \/ (((len f1) Shift f2) | (X /\ (dom (f1 ^ f2)))) by RELAT_1:65
.= (f1 | (X /\ (dom (f1 ^ f2)))) \/ (((len f1) Shift f2) | ((X /\ (dom (f1 ^ f2))) \ (Seg (len f1)))) by A16, RELAT_1:157
.= (f1 | ((X /\ (dom (f1 ^ f2))) /\ (Seg (len f1)))) \/ (((len f1) Shift f2) | ((X /\ (dom (f1 ^ f2))) \ (Seg (len f1)))) by A10, RELAT_1:157 ;
hence Seq ((f1 ^ f2) | X) = (Seq (f1 | X)) ^ (Seq (f2 | Y2)) by A7, A11, A9, Th11; ::_thesis: for n being Nat st n > 0 holds
( n in Y2 iff n + (len f1) in X /\ (dom (f1 ^ f2)) )
let n be Nat; ::_thesis: ( n > 0 implies ( n in Y2 iff n + (len f1) in X /\ (dom (f1 ^ f2)) ) )
assume n > 0 ; ::_thesis: ( n in Y2 iff n + (len f1) in X /\ (dom (f1 ^ f2)) )
then n + (len f1) > 0 + (len f1) by XREAL_1:6;
then A17: not n + (len f1) in Seg (len f1) by FINSEQ_1:1;
hereby ::_thesis: ( n + (len f1) in X /\ (dom (f1 ^ f2)) implies n in Y2 )
assume n in Y2 ; ::_thesis: n + (len f1) in X /\ (dom (f1 ^ f2))
then n + (len f1) in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) by A7;
hence n + (len f1) in X /\ (dom (f1 ^ f2)) by XBOOLE_0:def_5; ::_thesis: verum
end;
assume n + (len f1) in X /\ (dom (f1 ^ f2)) ; ::_thesis: n in Y2
then n + (len f1) in (X /\ (dom (f1 ^ f2))) \ (Seg (len f1)) by A17, XBOOLE_0:def_5;
hence n in Y2 by A7; ::_thesis: verum
end;
theorem :: MATRTOP1:13
for X being set
for g1, f1, g2, f2 being FinSequence st len g1 = len f1 & len g2 <= len f2 holds
Seq ((f1 ^ f2) | ((g1 ^ g2) " X)) = (Seq (f1 | (g1 " X))) ^ (Seq (f2 | (g2 " X)))
proof
let X be set ; ::_thesis: for g1, f1, g2, f2 being FinSequence st len g1 = len f1 & len g2 <= len f2 holds
Seq ((f1 ^ f2) | ((g1 ^ g2) " X)) = (Seq (f1 | (g1 " X))) ^ (Seq (f2 | (g2 " X)))
let g1, f1, g2, f2 be FinSequence; ::_thesis: ( len g1 = len f1 & len g2 <= len f2 implies Seq ((f1 ^ f2) | ((g1 ^ g2) " X)) = (Seq (f1 | (g1 " X))) ^ (Seq (f2 | (g2 " X))) )
assume that
A1: len f1 = len g1 and
A2: len g2 <= len f2 ; ::_thesis: Seq ((f1 ^ f2) | ((g1 ^ g2) " X)) = (Seq (f1 | (g1 " X))) ^ (Seq (f2 | (g2 " X)))
set f12 = f1 ^ f2;
set g12 = g1 ^ g2;
A3: ( dom (f1 ^ f2) = Seg (len (f1 ^ f2)) & dom (g1 ^ g2) = Seg (len (g1 ^ g2)) ) by FINSEQ_1:def_3;
set g12X = (g1 ^ g2) " X;
consider Y being Subset of NAT such that
A4: Seq ((f1 ^ f2) | ((g1 ^ g2) " X)) = (Seq (f1 | ((g1 ^ g2) " X))) ^ (Seq (f2 | Y)) and
A5: for n being Nat st n > 0 holds
( n in Y iff n + (len f1) in ((g1 ^ g2) " X) /\ (dom (f1 ^ f2)) ) by Th12;
A6: Y /\ (dom f2) c= g2 " X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y /\ (dom f2) or x in g2 " X )
assume A7: x in Y /\ (dom f2) ; ::_thesis: x in g2 " X
then reconsider i = x as Nat ;
x in dom f2 by A7, XBOOLE_0:def_4;
then A8: i > 0 by FINSEQ_3:25;
then i + (len f1) > (len f1) + 0 by XREAL_1:6;
then A9: not i + (len f1) in dom g1 by A1, FINSEQ_3:25;
x in Y by A7, XBOOLE_0:def_4;
then i + (len f1) in ((g1 ^ g2) " X) /\ (dom (f1 ^ f2)) by A5, A8;
then A10: i + (len f1) in (g1 ^ g2) " X by XBOOLE_0:def_4;
then A11: (g1 ^ g2) . (i + (len f1)) in X by FUNCT_1:def_7;
i + (len f1) in dom (g1 ^ g2) by A10, FUNCT_1:def_7;
then A12: ex j being Nat st
( j in dom g2 & i + (len f1) = (len g1) + j ) by A9, FINSEQ_1:25;
then (g1 ^ g2) . (i + (len f1)) = g2 . i by A1, FINSEQ_1:def_7;
hence x in g2 " X by A1, A11, A12, FUNCT_1:def_7; ::_thesis: verum
end;
A13: dom f1 = dom g1 by A1, FINSEQ_3:29;
A14: g1 " X c= ((g1 ^ g2) " X) /\ (dom f1)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in g1 " X or x in ((g1 ^ g2) " X) /\ (dom f1) )
assume A15: x in g1 " X ; ::_thesis: x in ((g1 ^ g2) " X) /\ (dom f1)
then A16: x in dom g1 by FUNCT_1:def_7;
A17: g1 . x in X by A15, FUNCT_1:def_7;
( dom g1 c= dom (g1 ^ g2) & (g1 ^ g2) . x = g1 . x ) by A16, FINSEQ_1:26, FINSEQ_1:def_7;
then x in (g1 ^ g2) " X by A16, A17, FUNCT_1:def_7;
hence x in ((g1 ^ g2) " X) /\ (dom f1) by A13, A16, XBOOLE_0:def_4; ::_thesis: verum
end;
( len (f1 ^ f2) = (len f1) + (len f2) & len (g1 ^ g2) = (len g1) + (len g2) ) by FINSEQ_1:22;
then len (g1 ^ g2) <= len (f1 ^ f2) by A1, A2, XREAL_1:6;
then A18: dom (g1 ^ g2) c= dom (f1 ^ f2) by A3, FINSEQ_1:5;
((g1 ^ g2) " X) /\ (dom f1) c= g1 " X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((g1 ^ g2) " X) /\ (dom f1) or x in g1 " X )
assume A19: x in ((g1 ^ g2) " X) /\ (dom f1) ; ::_thesis: x in g1 " X
then x in (g1 ^ g2) " X by XBOOLE_0:def_4;
then A20: (g1 ^ g2) . x in X by FUNCT_1:def_7;
A21: x in dom f1 by A19, XBOOLE_0:def_4;
then (g1 ^ g2) . x = g1 . x by A13, FINSEQ_1:def_7;
hence x in g1 " X by A13, A21, A20, FUNCT_1:def_7; ::_thesis: verum
end;
then ((g1 ^ g2) " X) /\ (dom f1) = g1 " X by A14, XBOOLE_0:def_10;
then A22: f1 | (g1 " X) = f1 | ((g1 ^ g2) " X) by RELAT_1:157;
( dom f2 = Seg (len f2) & dom g2 = Seg (len g2) ) by FINSEQ_1:def_3;
then A23: dom g2 c= dom f2 by A2, FINSEQ_1:5;
g2 " X c= Y /\ (dom f2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in g2 " X or x in Y /\ (dom f2) )
assume A24: x in g2 " X ; ::_thesis: x in Y /\ (dom f2)
then A25: x in dom g2 by FUNCT_1:def_7;
then reconsider i = x as Nat ;
A26: g2 . x in X by A24, FUNCT_1:def_7;
A27: i + (len g1) in dom (g1 ^ g2) by A25, FINSEQ_1:28;
(g1 ^ g2) . (i + (len g1)) = g2 . i by A25, FINSEQ_1:def_7;
then i + (len g1) in (g1 ^ g2) " X by A26, A27, FUNCT_1:def_7;
then A28: i + (len g1) in ((g1 ^ g2) " X) /\ (dom (f1 ^ f2)) by A18, A27, XBOOLE_0:def_4;
i > 0 by A25, FINSEQ_3:25;
then i in Y by A1, A5, A28;
hence x in Y /\ (dom f2) by A23, A25, XBOOLE_0:def_4; ::_thesis: verum
end;
then Y /\ (dom f2) = g2 " X by A6, XBOOLE_0:def_10;
hence Seq ((f1 ^ f2) | ((g1 ^ g2) " X)) = (Seq (f1 | (g1 " X))) ^ (Seq (f2 | (g2 " X))) by A4, A22, RELAT_1:157; ::_thesis: verum
end;
theorem :: MATRTOP1:14
for X being set
for n, m being Nat
for D being non empty set
for M being Matrix of n,m,D holds M - X is Matrix of n -' (card (M " X)),m,D
proof
let X be set ; ::_thesis: for n, m being Nat
for D being non empty set
for M being Matrix of n,m,D holds M - X is Matrix of n -' (card (M " X)),m,D
let n, m be Nat; ::_thesis: for D being non empty set
for M being Matrix of n,m,D holds M - X is Matrix of n -' (card (M " X)),m,D
let D be non empty set ; ::_thesis: for M being Matrix of n,m,D holds M - X is Matrix of n -' (card (M " X)),m,D
let M be Matrix of n,m,D; ::_thesis: M - X is Matrix of n -' (card (M " X)),m,D
A1: rng (M - X) c= rng M by FINSEQ_3:66;
rng M c= D * by FINSEQ_1:def_4;
then rng (M - X) c= D * by A1, XBOOLE_1:1;
then reconsider MX = M - X as FinSequence of D * by FINSEQ_1:def_4;
A2: len MX = (len M) - (card (M " X)) by FINSEQ_3:59;
then len M >= card (M " X) by XREAL_1:49;
then A3: ( len M = n & len MX = (len M) -' (card (M " X)) ) by A2, MATRIX_1:def_2, XREAL_1:233;
percases ( len MX = 0 or len MX > 0 ) ;
supposeA4: len MX = 0 ; ::_thesis: M - X is Matrix of n -' (card (M " X)),m,D
then MX = {} ;
hence M - X is Matrix of n -' (card (M " X)),m,D by A3, A4, MATRIX_1:13; ::_thesis: verum
end;
suppose len MX > 0 ; ::_thesis: M - X is Matrix of n -' (card (M " X)),m,D
A5: for x being set st x in rng MX holds
ex s being FinSequence st
( s = x & len s = m )
proof
let x be set ; ::_thesis: ( x in rng MX implies ex s being FinSequence st
( s = x & len s = m ) )
consider nn being Nat such that
A6: for x being set st x in rng M holds
ex p being FinSequence of D st
( x = p & len p = nn ) by MATRIX_1:9;
assume A7: x in rng MX ; ::_thesis: ex s being FinSequence st
( s = x & len s = m )
then ex p being FinSequence of D st
( x = p & len p = nn ) by A1, A6;
then reconsider p = x as FinSequence of D ;
len p = m by A1, A7, MATRIX_1:def_2;
hence ex s being FinSequence st
( s = x & len s = m ) ; ::_thesis: verum
end;
then reconsider MX = MX as Matrix of D by MATRIX_1:def_1;
now__::_thesis:_for_p_being_FinSequence_of_D_st_p_in_rng_MX_holds_
len_p_=_m
let p be FinSequence of D; ::_thesis: ( p in rng MX implies len p = m )
assume p in rng MX ; ::_thesis: len p = m
then ex s being FinSequence st
( s = p & len s = m ) by A5;
hence len p = m ; ::_thesis: verum
end;
hence M - X is Matrix of n -' (card (M " X)),m,D by A3, MATRIX_1:def_2; ::_thesis: verum
end;
end;
end;
theorem Th15: :: MATRTOP1:15
for n, m being Nat
for F being Function of (Seg n),(Seg n)
for D being non empty set
for M being Matrix of n,m,D
for i being Nat st i in Seg (width M) holds
Col ((M * F),i) = (Col (M,i)) * F
proof
let n, m be Nat; ::_thesis: for F being Function of (Seg n),(Seg n)
for D being non empty set
for M being Matrix of n,m,D
for i being Nat st i in Seg (width M) holds
Col ((M * F),i) = (Col (M,i)) * F
let F be Function of (Seg n),(Seg n); ::_thesis: for D being non empty set
for M being Matrix of n,m,D
for i being Nat st i in Seg (width M) holds
Col ((M * F),i) = (Col (M,i)) * F
let D be non empty set ; ::_thesis: for M being Matrix of n,m,D
for i being Nat st i in Seg (width M) holds
Col ((M * F),i) = (Col (M,i)) * F
let M be Matrix of n,m,D; ::_thesis: for i being Nat st i in Seg (width M) holds
Col ((M * F),i) = (Col (M,i)) * F
let i be Nat; ::_thesis: ( i in Seg (width M) implies Col ((M * F),i) = (Col (M,i)) * F )
assume A1: i in Seg (width M) ; ::_thesis: Col ((M * F),i) = (Col (M,i)) * F
A2: len M = n by MATRIX_1:def_2;
then A3: dom M = Seg n by FINSEQ_1:def_3;
len (Col (M,i)) = n by A2, CARD_1:def_7;
then A4: dom (Col (M,i)) = Seg n by FINSEQ_1:def_3;
( dom F = Seg n & rng F c= Seg n ) by FUNCT_2:52, RELAT_1:def_19;
then A5: dom ((Col (M,i)) * F) = Seg n by A4, RELAT_1:27;
A6: len (M * F) = n by MATRIX_1:def_2;
then A7: dom (M * F) = Seg n by FINSEQ_1:def_3;
A8: now__::_thesis:_for_x_being_set_st_x_in_Seg_n_holds_
((Col_(M,i))_*_F)_._x_=_(Col_((M_*_F),i))_._x
let x be set ; ::_thesis: ( x in Seg n implies ((Col (M,i)) * F) . x = (Col ((M * F),i)) . x )
assume A9: x in Seg n ; ::_thesis: ((Col (M,i)) * F) . x = (Col ((M * F),i)) . x
then reconsider j = x as Element of NAT ;
Indices M = [:(dom M),(Seg (width M)):] by MATRIX_1:def_4;
then A10: [j,i] in Indices M by A1, A3, A9, ZFMISC_1:87;
A11: F . x in Seg n by A4, A5, A9, FUNCT_1:11;
then reconsider Fj = F . x as Element of NAT ;
thus ((Col (M,i)) * F) . x = (Col (M,i)) . Fj by A5, A9, FUNCT_1:12
.= M * (Fj,i) by A3, A11, MATRIX_1:def_8
.= (M * F) * (j,i) by A10, MATRIX11:def_4
.= (Col ((M * F),i)) . x by A7, A9, MATRIX_1:def_8 ; ::_thesis: verum
end;
len (Col ((M * F),i)) = n by A6, CARD_1:def_7;
then dom (Col ((M * F),i)) = Seg n by FINSEQ_1:def_3;
hence Col ((M * F),i) = (Col (M,i)) * F by A5, A8, FUNCT_1:2; ::_thesis: verum
end;
Lm1: for n, m being Nat
for K being Field
for A being Matrix of n,m,K st ( n = 0 implies m = 0 ) & the_rank_of A = n holds
ex B being Matrix of m -' n,m,K st the_rank_of (A ^ B) = m
proof
let n, m be Nat; ::_thesis: for K being Field
for A being Matrix of n,m,K st ( n = 0 implies m = 0 ) & the_rank_of A = n holds
ex B being Matrix of m -' n,m,K st the_rank_of (A ^ B) = m
let K be Field; ::_thesis: for A being Matrix of n,m,K st ( n = 0 implies m = 0 ) & the_rank_of A = n holds
ex B being Matrix of m -' n,m,K st the_rank_of (A ^ B) = m
let A be Matrix of n,m,K; ::_thesis: ( ( n = 0 implies m = 0 ) & the_rank_of A = n implies ex B being Matrix of m -' n,m,K st the_rank_of (A ^ B) = m )
set V = m -VectSp_over K;
set L = lines A;
assume that
A1: ( n = 0 implies m = 0 ) and
A2: the_rank_of A = n ; ::_thesis: ex B being Matrix of m -' n,m,K st the_rank_of (A ^ B) = m
A3: len A = n by A1, MATRIX13:1;
lines A is linearly-independent by A2, MATRIX13:121;
then consider B being Subset of (m -VectSp_over K) such that
A4: lines A c= B and
A5: B is linearly-independent and
A6: Lin B = VectSpStr(# the carrier of (m -VectSp_over K), the addF of (m -VectSp_over K), the ZeroF of (m -VectSp_over K), the lmult of (m -VectSp_over K) #) by VECTSP_7:17;
reconsider B = B as finite Subset of (m -VectSp_over K) by A5, VECTSP_9:21;
B is Basis of m -VectSp_over K by A5, A6, VECTSP_7:def_3;
then A7: card B = dim (m -VectSp_over K) by VECTSP_9:def_1
.= m by MATRIX13:112 ;
width A = m by A1, MATRIX13:1;
then A8: m - n >= 0 by A2, MATRIX13:74, XREAL_1:48;
then A9: m - n = m -' n by XREAL_0:def_2;
A10: A is without_repeated_line by A2, MATRIX13:121;
then A11: len A = card (lines A) by FINSEQ_4:62;
set BL = B \ (lines A);
consider p being FinSequence such that
A12: rng p = B \ (lines A) and
A13: p is one-to-one by FINSEQ_4:58;
reconsider p = p as FinSequence of (m -VectSp_over K) by A12, FINSEQ_1:def_4;
len p = card (B \ (lines A)) by A12, A13, FINSEQ_4:62
.= (card B) - (card (lines A)) by A4, CARD_2:44
.= m -' n by A3, A11, A7, A8, XREAL_0:def_2 ;
then reconsider P = FinS2MX p as Matrix of m -' n,m,K ;
rng A misses rng P by A12, XBOOLE_1:79;
then A14: A ^ P is without_repeated_line by A10, A13, FINSEQ_3:91;
take P ; ::_thesis: the_rank_of (A ^ P) = m
lines (A ^ P) = (lines A) \/ (rng P) by FINSEQ_1:31
.= (lines A) \/ B by A12, XBOOLE_1:39
.= B by A4, XBOOLE_1:12 ;
hence the_rank_of (A ^ P) = m by A5, A9, A14, MATRIX13:121; ::_thesis: verum
end;
theorem Th16: :: MATRTOP1:16
for n, m being Nat
for K being Field
for A being Matrix of n,m,K st the_rank_of A = n holds
ex B being Matrix of m -' n,m,K st the_rank_of (A ^ B) = m
proof
let n, m be Nat; ::_thesis: for K being Field
for A being Matrix of n,m,K st the_rank_of A = n holds
ex B being Matrix of m -' n,m,K st the_rank_of (A ^ B) = m
let K be Field; ::_thesis: for A being Matrix of n,m,K st the_rank_of A = n holds
ex B being Matrix of m -' n,m,K st the_rank_of (A ^ B) = m
let A be Matrix of n,m,K; ::_thesis: ( the_rank_of A = n implies ex B being Matrix of m -' n,m,K st the_rank_of (A ^ B) = m )
assume A1: the_rank_of A = n ; ::_thesis: ex B being Matrix of m -' n,m,K st the_rank_of (A ^ B) = m
percases ( n = 0 or n > 0 ) ;
supposeA2: n = 0 ; ::_thesis: ex B being Matrix of m -' n,m,K st the_rank_of (A ^ B) = m
then m -' n = m - n by XREAL_0:def_2;
then reconsider ONE = 1. (K,m) as Matrix of m -' n,m,K by A2;
1. (K,m) is invertible by MATRIX_6:8;
then Det (1. (K,m)) <> 0. K by LAPLACE:34;
then A3: the_rank_of ONE = m by MATRIX13:83;
len A = 0 by A2, MATRIX_1:def_2;
then A is empty ;
then A ^ ONE = ONE by FINSEQ_1:34;
hence ex B being Matrix of m -' n,m,K st the_rank_of (A ^ B) = m by A3; ::_thesis: verum
end;
suppose n > 0 ; ::_thesis: ex B being Matrix of m -' n,m,K st the_rank_of (A ^ B) = m
hence ex B being Matrix of m -' n,m,K st the_rank_of (A ^ B) = m by A1, Lm1; ::_thesis: verum
end;
end;
end;
theorem :: MATRTOP1:17
for n, m being Nat
for K being Field
for A being Matrix of n,m,K st the_rank_of A = m holds
ex B being Matrix of n,n -' m,K st the_rank_of (A ^^ B) = n
proof
let n, m be Nat; ::_thesis: for K being Field
for A being Matrix of n,m,K st the_rank_of A = m holds
ex B being Matrix of n,n -' m,K st the_rank_of (A ^^ B) = n
let K be Field; ::_thesis: for A being Matrix of n,m,K st the_rank_of A = m holds
ex B being Matrix of n,n -' m,K st the_rank_of (A ^^ B) = n
let A be Matrix of n,m,K; ::_thesis: ( the_rank_of A = m implies ex B being Matrix of n,n -' m,K st the_rank_of (A ^^ B) = n )
assume A1: the_rank_of A = m ; ::_thesis: ex B being Matrix of n,n -' m,K st the_rank_of (A ^^ B) = n
A2: len A = n by MATRIX_1:def_2;
percases ( m = 0 or m > 0 ) ;
supposeA3: m = 0 ; ::_thesis: ex B being Matrix of n,n -' m,K st the_rank_of (A ^^ B) = n
then n -' m = n - m by XREAL_0:def_2;
then reconsider ONE = 1. (K,n) as Matrix of n,n -' m,K by A3;
A4: len (1. (K,n)) = n by MATRIX_1:24;
1. (K,n) is invertible by MATRIX_6:8;
then Det (1. (K,n)) <> 0. K by LAPLACE:34;
then A5: the_rank_of ONE = n by MATRIX13:83;
width A = m by A3, MATRIX13:1;
then A ^^ ONE = ONE by A2, A3, A4, MATRIX15:22;
hence ex B being Matrix of n,n -' m,K st the_rank_of (A ^^ B) = n by A5; ::_thesis: verum
end;
supposeA6: m > 0 ; ::_thesis: ex B being Matrix of n,n -' m,K st the_rank_of (A ^^ B) = n
n - m >= 0 by A1, A2, MATRIX13:74, XREAL_1:48;
then A7: n -' m = n - m by XREAL_0:def_2;
A8: n > 0 by A1, A2, A6, MATRIX13:74;
then A9: width A = m by MATRIX13:1;
percases ( n = m or n <> m ) ;
supposeA10: n = m ; ::_thesis: ex B being Matrix of n,n -' m,K st the_rank_of (A ^^ B) = n
take B = the Matrix of n,n -' m,K; ::_thesis: the_rank_of (A ^^ B) = n
( len B = n & width B = 0 ) by A6, A7, A10, MATRIX_1:23;
hence the_rank_of (A ^^ B) = n by A1, A2, A10, MATRIX15:22; ::_thesis: verum
end;
supposeA11: n <> m ; ::_thesis: ex B being Matrix of n,n -' m,K st the_rank_of (A ^^ B) = n
A12: width (A @) = n by A2, A6, A9, MATRIX_2:10;
len (A @) = m by A6, A9, MATRIX_2:10;
then reconsider A1 = A @ as Matrix of m,n,K by A12, MATRIX_2:7;
the_rank_of A1 = m by A1, MATRIX13:84;
then consider B being Matrix of n -' m,n,K such that
A13: the_rank_of (A1 ^ B) = n by Th16;
A14: n -' m <> 0 by A7, A11;
then A15: width B = n by MATRIX13:1;
then A16: len (B @) = n by A8, MATRIX_2:10;
len B = n -' m by A14, MATRIX13:1;
then width (B @) = n -' m by A8, A15, MATRIX_2:10;
then reconsider B1 = B @ as Matrix of n,n -' m,K by A16, MATRIX_2:7;
A1 @ = A by A2, A6, A8, A9, MATRIX_2:13;
then A17: (A1 ^ B) @ = A ^^ B1 by A12, A15, MATRLIN:28;
the_rank_of ((A1 ^ B) @) = n by A13, MATRIX13:84;
hence ex B being Matrix of n,n -' m,K st the_rank_of (A ^^ B) = n by A17; ::_thesis: verum
end;
end;
end;
end;
end;
Lm2: for n being Nat
for f being b1 -element real-valued FinSequence holds f is Point of (TOP-REAL n)
proof
let n be Nat; ::_thesis: for f being n -element real-valued FinSequence holds f is Point of (TOP-REAL n)
let f be n -element real-valued FinSequence; ::_thesis: f is Point of (TOP-REAL n)
( len f = n & @ (@ f) = f ) by CARD_1:def_7;
hence f is Point of (TOP-REAL n) by TOPREAL3:46; ::_thesis: verum
end;
begin
definition
let n, m be Nat;
let M be Matrix of n,m,F_Real;
func Mx2Tran M -> Function of (TOP-REAL n),(TOP-REAL m) means :Def3: :: MATRTOP1:def 3
for f being n -element real-valued FinSequence holds it . f = Line (((LineVec2Mx (@ f)) * M),1) if n <> 0
otherwise for f being n -element real-valued FinSequence holds it . f = 0. (TOP-REAL m);
existence
( ( n <> 0 implies ex b1 being Function of (TOP-REAL n),(TOP-REAL m) st
for f being n -element real-valued FinSequence holds b1 . f = Line (((LineVec2Mx (@ f)) * M),1) ) & ( not n <> 0 implies ex b1 being Function of (TOP-REAL n),(TOP-REAL m) st
for f being n -element real-valued FinSequence holds b1 . f = 0. (TOP-REAL m) ) )
proof
set Tm = TOP-REAL m;
set Tn = TOP-REAL n;
A1: now__::_thesis:_(_n_<>_0_implies_ex_F_being_Function_of_(TOP-REAL_n),(TOP-REAL_m)_st_
for_f_being_n_-element_real-valued_FinSequence_holds_F_._f_=_Line_(((LineVec2Mx_(@_f))_*_M),1)_)
assume A2: n <> 0 ; ::_thesis: ex F being Function of (TOP-REAL n),(TOP-REAL m) st
for f being n -element real-valued FinSequence holds F . f = Line (((LineVec2Mx (@ f)) * M),1)
defpred S1[ Element of (TOP-REAL n), Element of (TOP-REAL m)] means $2 = Line (((LineVec2Mx (@ $1)) * M),1);
A3: for x being Element of (TOP-REAL n) ex y being Element of (TOP-REAL m) st S1[x,y]
proof
let x be Element of (TOP-REAL n); ::_thesis: ex y being Element of (TOP-REAL m) st S1[x,y]
set L = LineVec2Mx (@ x);
set LL = Line (((LineVec2Mx (@ x)) * M),1);
len x = n by CARD_1:def_7;
then A4: width (LineVec2Mx (@ x)) = n by MATRIX13:1;
( len M = n & width M = m ) by A2, MATRIX13:1;
then width ((LineVec2Mx (@ x)) * M) = m by A4, MATRIX_3:def_4;
then Line (((LineVec2Mx (@ x)) * M),1) in REAL m ;
then reconsider LL = Line (((LineVec2Mx (@ x)) * M),1) as Element of (TOP-REAL m) by EUCLID:22;
S1[x,LL] ;
hence ex y being Element of (TOP-REAL m) st S1[x,y] ; ::_thesis: verum
end;
consider F being Function of (TOP-REAL n),(TOP-REAL m) such that
A5: for x being Element of (TOP-REAL n) holds S1[x,F . x] from FUNCT_2:sch_3(A3);
take F = F; ::_thesis: for f being n -element real-valued FinSequence holds F . f = Line (((LineVec2Mx (@ f)) * M),1)
let f be n -element real-valued FinSequence; ::_thesis: F . f = Line (((LineVec2Mx (@ f)) * M),1)
( @ f is FinSequence of REAL & len f = n ) by CARD_1:def_7;
then f is Element of n -tuples_on REAL by FINSEQ_2:92;
then f in REAL n ;
then f is Element of (TOP-REAL n) by EUCLID:22;
hence F . f = Line (((LineVec2Mx (@ f)) * M),1) by A5; ::_thesis: verum
end;
now__::_thesis:_(_n_=_0_implies_ex_F_being_Function_of_(TOP-REAL_n),(TOP-REAL_m)_st_
for_f_being_n_-element_real-valued_FinSequence_holds_F_._f_=_0._(TOP-REAL_m)_)
assume n = 0 ; ::_thesis: ex F being Function of (TOP-REAL n),(TOP-REAL m) st
for f being n -element real-valued FinSequence holds F . f = 0. (TOP-REAL m)
defpred S1[ Element of (TOP-REAL n), Element of (TOP-REAL m)] means $2 = 0. (TOP-REAL m);
A6: for x being Element of (TOP-REAL n) ex y being Element of (TOP-REAL m) st S1[x,y] ;
consider F being Function of (TOP-REAL n),(TOP-REAL m) such that
A7: for x being Element of (TOP-REAL n) holds S1[x,F . x] from FUNCT_2:sch_3(A6);
take F = F; ::_thesis: for f being n -element real-valued FinSequence holds F . f = 0. (TOP-REAL m)
let f be n -element real-valued FinSequence; ::_thesis: F . f = 0. (TOP-REAL m)
( @ f is FinSequence of REAL & len f = n ) by CARD_1:def_7;
then f is Element of n -tuples_on REAL by FINSEQ_2:92;
then f in REAL n ;
then f is Element of (TOP-REAL n) by EUCLID:22;
hence F . f = 0. (TOP-REAL m) by A7; ::_thesis: verum
end;
hence ( ( n <> 0 implies ex b1 being Function of (TOP-REAL n),(TOP-REAL m) st
for f being n -element real-valued FinSequence holds b1 . f = Line (((LineVec2Mx (@ f)) * M),1) ) & ( not n <> 0 implies ex b1 being Function of (TOP-REAL n),(TOP-REAL m) st
for f being n -element real-valued FinSequence holds b1 . f = 0. (TOP-REAL m) ) ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of (TOP-REAL n),(TOP-REAL m) holds
( ( n <> 0 & ( for f being n -element real-valued FinSequence holds b1 . f = Line (((LineVec2Mx (@ f)) * M),1) ) & ( for f being n -element real-valued FinSequence holds b2 . f = Line (((LineVec2Mx (@ f)) * M),1) ) implies b1 = b2 ) & ( not n <> 0 & ( for f being n -element real-valued FinSequence holds b1 . f = 0. (TOP-REAL m) ) & ( for f being n -element real-valued FinSequence holds b2 . f = 0. (TOP-REAL m) ) implies b1 = b2 ) )
proof
let F1, F2 be Function of (TOP-REAL n),(TOP-REAL m); ::_thesis: ( ( n <> 0 & ( for f being n -element real-valued FinSequence holds F1 . f = Line (((LineVec2Mx (@ f)) * M),1) ) & ( for f being n -element real-valued FinSequence holds F2 . f = Line (((LineVec2Mx (@ f)) * M),1) ) implies F1 = F2 ) & ( not n <> 0 & ( for f being n -element real-valued FinSequence holds F1 . f = 0. (TOP-REAL m) ) & ( for f being n -element real-valued FinSequence holds F2 . f = 0. (TOP-REAL m) ) implies F1 = F2 ) )
A8: now__::_thesis:_(_n_<>_0_&_(_for_f_being_n_-element_real-valued_FinSequence_holds_F1_._f_=_Line_(((LineVec2Mx_(@_f))_*_M),1)_)_&_(_for_f_being_n_-element_real-valued_FinSequence_holds_F2_._f_=_Line_(((LineVec2Mx_(@_f))_*_M),1)_)_implies_F1_=_F2_)
assume n <> 0 ; ::_thesis: ( ( for f being n -element real-valued FinSequence holds F1 . f = Line (((LineVec2Mx (@ f)) * M),1) ) & ( for f being n -element real-valued FinSequence holds F2 . f = Line (((LineVec2Mx (@ f)) * M),1) ) implies F1 = F2 )
assume A9: for f being n -element real-valued FinSequence holds F1 . f = Line (((LineVec2Mx (@ f)) * M),1) ; ::_thesis: ( ( for f being n -element real-valued FinSequence holds F2 . f = Line (((LineVec2Mx (@ f)) * M),1) ) implies F1 = F2 )
assume A10: for f being n -element real-valued FinSequence holds F2 . f = Line (((LineVec2Mx (@ f)) * M),1) ; ::_thesis: F1 = F2
now__::_thesis:_for_x_being_Element_of_(TOP-REAL_n)_holds_F1_._x_=_F2_._x
let x be Element of (TOP-REAL n); ::_thesis: F1 . x = F2 . x
thus F1 . x = Line (((LineVec2Mx (@ x)) * M),1) by A9
.= F2 . x by A10 ; ::_thesis: verum
end;
hence F1 = F2 by FUNCT_2:63; ::_thesis: verum
end;
now__::_thesis:_(_n_=_0_&_(_for_f_being_n_-element_real-valued_FinSequence_holds_F1_._f_=_0._(TOP-REAL_m)_)_&_(_for_f_being_n_-element_real-valued_FinSequence_holds_F2_._f_=_0._(TOP-REAL_m)_)_implies_F1_=_F2_)
assume n = 0 ; ::_thesis: ( ( for f being n -element real-valued FinSequence holds F1 . f = 0. (TOP-REAL m) ) & ( for f being n -element real-valued FinSequence holds F2 . f = 0. (TOP-REAL m) ) implies F1 = F2 )
assume A11: for f being n -element real-valued FinSequence holds F1 . f = 0. (TOP-REAL m) ; ::_thesis: ( ( for f being n -element real-valued FinSequence holds F2 . f = 0. (TOP-REAL m) ) implies F1 = F2 )
assume A12: for f being n -element real-valued FinSequence holds F2 . f = 0. (TOP-REAL m) ; ::_thesis: F1 = F2
now__::_thesis:_for_x_being_Element_of_(TOP-REAL_n)_holds_F1_._x_=_F2_._x
let x be Element of (TOP-REAL n); ::_thesis: F1 . x = F2 . x
thus F1 . x = 0. (TOP-REAL m) by A11
.= F2 . x by A12 ; ::_thesis: verum
end;
hence F1 = F2 by FUNCT_2:63; ::_thesis: verum
end;
hence ( ( n <> 0 & ( for f being n -element real-valued FinSequence holds F1 . f = Line (((LineVec2Mx (@ f)) * M),1) ) & ( for f being n -element real-valued FinSequence holds F2 . f = Line (((LineVec2Mx (@ f)) * M),1) ) implies F1 = F2 ) & ( not n <> 0 & ( for f being n -element real-valued FinSequence holds F1 . f = 0. (TOP-REAL m) ) & ( for f being n -element real-valued FinSequence holds F2 . f = 0. (TOP-REAL m) ) implies F1 = F2 ) ) by A8; ::_thesis: verum
end;
correctness
consistency
for b1 being Function of (TOP-REAL n),(TOP-REAL m) holds verum;
;
end;
:: deftheorem Def3 defines Mx2Tran MATRTOP1:def_3_:_
for n, m being Nat
for M being Matrix of n,m,F_Real
for b4 being Function of (TOP-REAL n),(TOP-REAL m) holds
( ( n <> 0 implies ( b4 = Mx2Tran M iff for f being b1 -element real-valued FinSequence holds b4 . f = Line (((LineVec2Mx (@ f)) * M),1) ) ) & ( not n <> 0 implies ( b4 = Mx2Tran M iff for f being b1 -element real-valued FinSequence holds b4 . f = 0. (TOP-REAL m) ) ) );
Lm3: now__::_thesis:_for_n,_m_being_Nat
for_M_being_Matrix_of_n,m,F_Real
for_x_being_set_holds_(Mx2Tran_M)_._x_is_real-valued_FinSequence
let n, m be Nat; ::_thesis: for M being Matrix of n,m,F_Real
for x being set holds (Mx2Tran b5) . b6 is real-valued FinSequence
let M be Matrix of n,m,F_Real; ::_thesis: for x being set holds (Mx2Tran b4) . b5 is real-valued FinSequence
let x be set ; ::_thesis: (Mx2Tran b3) . b4 is real-valued FinSequence
set T = Mx2Tran M;
percases ( x in dom (Mx2Tran M) or not x in dom (Mx2Tran M) ) ;
supposeA1: x in dom (Mx2Tran M) ; ::_thesis: (Mx2Tran b3) . b4 is real-valued FinSequence
A2: rng (Mx2Tran M) c= the carrier of (TOP-REAL m) by RELAT_1:def_19;
(Mx2Tran M) . x in rng (Mx2Tran M) by A1, FUNCT_1:def_3;
hence (Mx2Tran M) . x is real-valued FinSequence by A2; ::_thesis: verum
end;
suppose not x in dom (Mx2Tran M) ; ::_thesis: (Mx2Tran b3) . b4 is real-valued FinSequence
hence (Mx2Tran M) . x is real-valued FinSequence by FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
registration
let n, m be Nat;
let M be Matrix of n,m,F_Real;
let x be set ;
cluster(Mx2Tran M) . x -> Relation-like Function-like ;
coherence
( (Mx2Tran M) . x is Function-like & (Mx2Tran M) . x is Relation-like ) by Lm3;
cluster(Mx2Tran M) . x -> FinSequence-like real-valued ;
coherence
( (Mx2Tran M) . x is real-valued & (Mx2Tran M) . x is FinSequence-like ) by Lm3;
end;
registration
let n, m be Nat;
let M be Matrix of n,m,F_Real;
let f be n -element real-valued FinSequence;
cluster(Mx2Tran M) . f -> m -element ;
coherence
(Mx2Tran M) . f is m -element
proof
set T = Mx2Tran M;
( @ f is FinSequence of REAL & len f = n ) by CARD_1:def_7;
then f is Element of n -tuples_on REAL by FINSEQ_2:92;
then f in REAL n ;
then f in the carrier of (TOP-REAL n) by EUCLID:22;
then f in dom (Mx2Tran M) by FUNCT_2:def_1;
then A1: (Mx2Tran M) . f in rng (Mx2Tran M) by FUNCT_1:def_3;
rng (Mx2Tran M) c= the carrier of (TOP-REAL m) by RELAT_1:def_19;
hence (Mx2Tran M) . f is m -element by A1; ::_thesis: verum
end;
end;
theorem Th18: :: MATRTOP1:18
for i, m, n being Nat
for f being b3 -element real-valued FinSequence
for M being Matrix of n,m,F_Real st 1 <= i & i <= m & n <> 0 holds
((Mx2Tran M) . f) . i = (@ f) "*" (Col (M,i))
proof
let i, m, n be Nat; ::_thesis: for f being n -element real-valued FinSequence
for M being Matrix of n,m,F_Real st 1 <= i & i <= m & n <> 0 holds
((Mx2Tran M) . f) . i = (@ f) "*" (Col (M,i))
let f be n -element real-valued FinSequence; ::_thesis: for M being Matrix of n,m,F_Real st 1 <= i & i <= m & n <> 0 holds
((Mx2Tran M) . f) . i = (@ f) "*" (Col (M,i))
let M be Matrix of n,m,F_Real; ::_thesis: ( 1 <= i & i <= m & n <> 0 implies ((Mx2Tran M) . f) . i = (@ f) "*" (Col (M,i)) )
assume that
A1: ( 1 <= i & i <= m ) and
A2: n <> 0 ; ::_thesis: ((Mx2Tran M) . f) . i = (@ f) "*" (Col (M,i))
A3: len M = n by A2, MATRIX13:1;
set Lf = LineVec2Mx (@ f);
set LfM = (LineVec2Mx (@ f)) * M;
len f = n by CARD_1:def_7;
then A4: width (LineVec2Mx (@ f)) = n by MATRIX13:1;
width M = m by A2, MATRIX13:1;
then A5: width ((LineVec2Mx (@ f)) * M) = m by A4, A3, MATRIX_3:def_4;
len (LineVec2Mx (@ f)) = 1 by MATRIX13:1;
then len ((LineVec2Mx (@ f)) * M) = 1 by A4, A3, MATRIX_3:def_4;
then A6: [1,i] in Indices ((LineVec2Mx (@ f)) * M) by A1, A5, MATRIX_1:36;
set LM = Line (((LineVec2Mx (@ f)) * M),1);
( i in Seg m & (Mx2Tran M) . f = Line (((LineVec2Mx (@ f)) * M),1) ) by A1, A2, Def3, FINSEQ_1:1;
hence ((Mx2Tran M) . f) . i = ((LineVec2Mx (@ f)) * M) * (1,i) by A5, MATRIX_1:def_7
.= (Line ((LineVec2Mx (@ f)),1)) "*" (Col (M,i)) by A4, A3, A6, MATRIX_3:def_4
.= (@ f) "*" (Col (M,i)) by MATRIX15:25 ;
::_thesis: verum
end;
theorem Th19: :: MATRTOP1:19
for n being Nat
for K being Field holds len (MX2FinS (1. (K,n))) = n
proof
let n be Nat; ::_thesis: for K being Field holds len (MX2FinS (1. (K,n))) = n
let K be Field; ::_thesis: len (MX2FinS (1. (K,n))) = n
MX2FinS (1. (K,n)) is OrdBasis of n -VectSp_over K by MATRLIN2:45;
hence len (MX2FinS (1. (K,n))) = dim (n -VectSp_over K) by MATRLIN2:21
.= n by MATRIX13:112 ;
::_thesis: verum
end;
theorem Th20: :: MATRTOP1:20
for n, m being Nat
for M being Matrix of n,m,F_Real
for Bn being OrdBasis of n -VectSp_over F_Real
for Bm being OrdBasis of m -VectSp_over F_Real st Bn = MX2FinS (1. (F_Real,n)) & Bm = MX2FinS (1. (F_Real,m)) holds
for M1 being Matrix of len Bn, len Bm,F_Real st M1 = M holds
Mx2Tran M = Mx2Tran (M1,Bn,Bm)
proof
let n, m be Nat; ::_thesis: for M being Matrix of n,m,F_Real
for Bn being OrdBasis of n -VectSp_over F_Real
for Bm being OrdBasis of m -VectSp_over F_Real st Bn = MX2FinS (1. (F_Real,n)) & Bm = MX2FinS (1. (F_Real,m)) holds
for M1 being Matrix of len Bn, len Bm,F_Real st M1 = M holds
Mx2Tran M = Mx2Tran (M1,Bn,Bm)
let M be Matrix of n,m,F_Real; ::_thesis: for Bn being OrdBasis of n -VectSp_over F_Real
for Bm being OrdBasis of m -VectSp_over F_Real st Bn = MX2FinS (1. (F_Real,n)) & Bm = MX2FinS (1. (F_Real,m)) holds
for M1 being Matrix of len Bn, len Bm,F_Real st M1 = M holds
Mx2Tran M = Mx2Tran (M1,Bn,Bm)
let Bn be OrdBasis of n -VectSp_over F_Real; ::_thesis: for Bm being OrdBasis of m -VectSp_over F_Real st Bn = MX2FinS (1. (F_Real,n)) & Bm = MX2FinS (1. (F_Real,m)) holds
for M1 being Matrix of len Bn, len Bm,F_Real st M1 = M holds
Mx2Tran M = Mx2Tran (M1,Bn,Bm)
let Bm be OrdBasis of m -VectSp_over F_Real; ::_thesis: ( Bn = MX2FinS (1. (F_Real,n)) & Bm = MX2FinS (1. (F_Real,m)) implies for M1 being Matrix of len Bn, len Bm,F_Real st M1 = M holds
Mx2Tran M = Mx2Tran (M1,Bn,Bm) )
assume that
A1: Bn = MX2FinS (1. (F_Real,n)) and
A2: Bm = MX2FinS (1. (F_Real,m)) ; ::_thesis: for M1 being Matrix of len Bn, len Bm,F_Real st M1 = M holds
Mx2Tran M = Mx2Tran (M1,Bn,Bm)
set T = Mx2Tran M;
let M1 be Matrix of len Bn, len Bm,F_Real; ::_thesis: ( M1 = M implies Mx2Tran M = Mx2Tran (M1,Bn,Bm) )
assume A3: M1 = M ; ::_thesis: Mx2Tran M = Mx2Tran (M1,Bn,Bm)
set Tb = Mx2Tran (M1,Bn,Bm);
dom (Mx2Tran (M1,Bn,Bm)) = the carrier of (n -VectSp_over F_Real) by FUNCT_2:def_1;
then A4: dom (Mx2Tran (M1,Bn,Bm)) = REAL n by MATRIX13:102
.= the carrier of (TOP-REAL n) by EUCLID:22 ;
A5: for x being set st x in dom (Mx2Tran M) holds
(Mx2Tran M) . x = (Mx2Tran (M1,Bn,Bm)) . x
proof
let x be set ; ::_thesis: ( x in dom (Mx2Tran M) implies (Mx2Tran M) . x = (Mx2Tran (M1,Bn,Bm)) . x )
assume x in dom (Mx2Tran M) ; ::_thesis: (Mx2Tran M) . x = (Mx2Tran (M1,Bn,Bm)) . x
then reconsider v = x as Element of (TOP-REAL n) by FUNCT_2:def_1;
reconsider g = v as Vector of (n -VectSp_over F_Real) by A4, FUNCT_2:def_1;
set L = LineVec2Mx (@ v);
len v = n by CARD_1:def_7;
then A6: ( len (LineVec2Mx (@ v)) = 1 & width (LineVec2Mx (@ v)) = n ) by MATRIX13:1;
A7: len Bn = n by A1, Th19;
A8: len Bm = m by A2, Th19;
percases ( n = 0 or n > 0 ) ;
supposeA9: n = 0 ; ::_thesis: (Mx2Tran M) . x = (Mx2Tran (M1,Bn,Bm)) . x
then (Mx2Tran (M1,Bn,Bm)) . g = 0. (m -VectSp_over F_Real) by A1, Th19, MATRLIN2:33
.= m |-> (0. F_Real) by MATRIX13:102
.= 0* m
.= 0. (TOP-REAL m) by EUCLID:70
.= (Mx2Tran M) . v by A9, Def3 ;
hence (Mx2Tran M) . x = (Mx2Tran (M1,Bn,Bm)) . x ; ::_thesis: verum
end;
supposeA10: n > 0 ; ::_thesis: (Mx2Tran M) . x = (Mx2Tran (M1,Bn,Bm)) . x
A11: ((Mx2Tran (M1,Bn,Bm)) . g) |-- Bm = (Mx2Tran (M1,Bn,Bm)) . g by A2, A8, MATRLIN2:46;
A12: ( g |-- Bn = g & AutMt ((Mx2Tran (M1,Bn,Bm)),Bn,Bm) = M ) by A1, A3, A7, MATRLIN2:36, MATRLIN2:46;
( 1 in dom (LineVec2Mx (@ v)) & len M = width (LineVec2Mx (@ v)) ) by A10, A6, FINSEQ_3:25, MATRIX13:1;
then LineVec2Mx (Line (((LineVec2Mx (@ v)) * M),1)) = (LineVec2Mx (Line ((LineVec2Mx (@ v)),1))) * M by MATRLIN2:35
.= (LineVec2Mx (@ v)) * M by MATRIX15:25
.= LineVec2Mx (((Mx2Tran (M1,Bn,Bm)) . g) |-- Bm) by A7, A10, A12, MATRLIN2:31 ;
hence (Mx2Tran (M1,Bn,Bm)) . x = Line ((LineVec2Mx (Line (((LineVec2Mx (@ v)) * M),1))),1) by A11, MATRIX15:25
.= Line (((LineVec2Mx (@ v)) * M),1) by MATRIX15:25
.= (Mx2Tran M) . x by A10, Def3 ;
::_thesis: verum
end;
end;
end;
dom (Mx2Tran M) = the carrier of (TOP-REAL n) by FUNCT_2:def_1;
hence Mx2Tran M = Mx2Tran (M1,Bn,Bm) by A4, A5, FUNCT_1:2; ::_thesis: verum
end;
theorem :: MATRTOP1:21
for m, n being Nat
for f being b2 -element real-valued FinSequence
for M being Matrix of n,m,F_Real
for P being Permutation of (Seg n) holds
( (Mx2Tran M) . f = (Mx2Tran (M * P)) . (f * P) & f * P is b2 -element FinSequence of REAL )
proof
let m, n be Nat; ::_thesis: for f being n -element real-valued FinSequence
for M being Matrix of n,m,F_Real
for P being Permutation of (Seg n) holds
( (Mx2Tran M) . f = (Mx2Tran (M * P)) . (f * P) & f * P is n -element FinSequence of REAL )
let f be n -element real-valued FinSequence; ::_thesis: for M being Matrix of n,m,F_Real
for P being Permutation of (Seg n) holds
( (Mx2Tran M) . f = (Mx2Tran (M * P)) . (f * P) & f * P is n -element FinSequence of REAL )
let M be Matrix of n,m,F_Real; ::_thesis: for P being Permutation of (Seg n) holds
( (Mx2Tran M) . f = (Mx2Tran (M * P)) . (f * P) & f * P is n -element FinSequence of REAL )
let P be Permutation of (Seg n); ::_thesis: ( (Mx2Tran M) . f = (Mx2Tran (M * P)) . (f * P) & f * P is n -element FinSequence of REAL )
A1: len f = n by CARD_1:def_7;
then A2: ( rng P = Seg n & dom f = Seg n ) by FINSEQ_1:def_3, FUNCT_2:def_3;
dom P = Seg n by FUNCT_2:52;
then A3: dom (f * P) = Seg n by A2, RELAT_1:27;
then reconsider fP = f * P as FinSequence by FINSEQ_1:def_2;
rng (f * P) = rng f by A2, RELAT_1:28;
then reconsider fP = fP as FinSequence of REAL by FINSEQ_1:def_4;
A4: len fP = n by A1, A3, FINSEQ_1:def_3;
then A5: fP is n -element by CARD_1:def_7;
(Mx2Tran M) . f = (Mx2Tran (M * P)) . (f * P)
proof
percases ( n <> 0 or n = 0 ) ;
supposeA6: n <> 0 ; ::_thesis: (Mx2Tran M) . f = (Mx2Tran (M * P)) . (f * P)
then A7: width M = m by MATRIX13:1;
set MP = M * P;
A8: len M = n by A6, MATRIX13:1;
A9: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_m_holds_
((Mx2Tran_(M_*_P))_._fP)_._i_=_((Mx2Tran_M)_._f)_._i
let i be Nat; ::_thesis: ( 1 <= i & i <= m implies ((Mx2Tran (M * P)) . fP) . i = ((Mx2Tran M) . f) . i )
assume A10: ( 1 <= i & i <= m ) ; ::_thesis: ((Mx2Tran (M * P)) . fP) . i = ((Mx2Tran M) . f) . i
then i in Seg m by FINSEQ_1:1;
then A11: mlt ((@ fP),(Col ((M * P),i))) = the multF of F_Real .: (fP,((Col (M,i)) * P)) by A7, Th15
.= (mlt ((@ f),(Col (M,i)))) * P by FUNCOP_1:25 ;
len (Col (M,i)) = n by A8, CARD_1:def_7;
then len (mlt ((@ f),(Col (M,i)))) = n by A1, MATRIX_3:6;
then A12: dom (mlt ((@ f),(Col (M,i)))) = Seg n by FINSEQ_1:def_3;
((Mx2Tran (M * P)) . fP) . i = (@ fP) "*" (Col ((M * P),i)) by A6, A5, A10, Th18
.= the addF of F_Real "**" (mlt ((@ fP),(Col ((M * P),i)))) ;
hence ((Mx2Tran (M * P)) . fP) . i = (@ f) "*" (Col (M,i)) by A12, A11, FINSOP_1:7
.= ((Mx2Tran M) . f) . i by A6, A10, Th18 ;
::_thesis: verum
end;
( len ((Mx2Tran M) . f) = m & len ((Mx2Tran (M * P)) . fP) = m ) by A5, CARD_1:def_7;
hence (Mx2Tran M) . f = (Mx2Tran (M * P)) . (f * P) by A9, FINSEQ_1:14; ::_thesis: verum
end;
supposeA13: n = 0 ; ::_thesis: (Mx2Tran M) . f = (Mx2Tran (M * P)) . (f * P)
hence (Mx2Tran M) . f = 0. (TOP-REAL m) by Def3
.= (Mx2Tran (M * P)) . (f * P) by A13, Def3 ;
::_thesis: verum
end;
end;
end;
hence ( (Mx2Tran M) . f = (Mx2Tran (M * P)) . (f * P) & f * P is n -element FinSequence of REAL ) by A4, CARD_1:def_7; ::_thesis: verum
end;
theorem Th22: :: MATRTOP1:22
for n, m being Nat
for f1, f2 being b1 -element real-valued FinSequence
for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (f1 + f2) = ((Mx2Tran M) . f1) + ((Mx2Tran M) . f2)
proof
let n, m be Nat; ::_thesis: for f1, f2 being n -element real-valued FinSequence
for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (f1 + f2) = ((Mx2Tran M) . f1) + ((Mx2Tran M) . f2)
let f1, f2 be n -element real-valued FinSequence; ::_thesis: for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (f1 + f2) = ((Mx2Tran M) . f1) + ((Mx2Tran M) . f2)
let M be Matrix of n,m,F_Real; ::_thesis: (Mx2Tran M) . (f1 + f2) = ((Mx2Tran M) . f1) + ((Mx2Tran M) . f2)
set f12 = f1 + f2;
set T = Mx2Tran M;
percases ( n <> 0 or n = 0 ) ;
supposeA1: n <> 0 ; ::_thesis: (Mx2Tran M) . (f1 + f2) = ((Mx2Tran M) . f1) + ((Mx2Tran M) . f2)
percases ( m = 0 or m > 0 ) ;
supposeA2: m = 0 ; ::_thesis: (Mx2Tran M) . (f1 + f2) = ((Mx2Tran M) . f1) + ((Mx2Tran M) . f2)
(Mx2Tran M) . (f1 + f2) = 0.REAL 0 by A2;
hence (Mx2Tran M) . (f1 + f2) = ((Mx2Tran M) . f1) + ((Mx2Tran M) . f2) by A2; ::_thesis: verum
end;
suppose m > 0 ; ::_thesis: (Mx2Tran M) . (f1 + f2) = ((Mx2Tran M) . f1) + ((Mx2Tran M) . f2)
then A3: m >= 1 by NAT_1:14;
A4: len M = n by A1, MATRIX13:1;
set L2 = LineVec2Mx (@ f2);
set L1 = LineVec2Mx (@ f1);
A5: len (LineVec2Mx (@ f2)) = 1 by MATRIX13:1;
A6: len f2 = n by CARD_1:def_7;
then A7: width (LineVec2Mx (@ f2)) = n by MATRIX13:1;
A8: width M = m by A1, MATRIX13:1;
then A9: width ((LineVec2Mx (@ f2)) * M) = m by A7, A4, MATRIX_3:def_4;
A10: len f1 = n by CARD_1:def_7;
then A11: width (LineVec2Mx (@ f1)) = n by MATRIX13:1;
then A12: width ((LineVec2Mx (@ f1)) * M) = m by A4, A8, MATRIX_3:def_4;
A13: len (LineVec2Mx (@ f1)) = 1 by MATRIX13:1;
then len ((LineVec2Mx (@ f1)) * M) = 1 by A11, A4, MATRIX_3:def_4;
then A14: [1,1] in Indices ((LineVec2Mx (@ f1)) * M) by A12, A3, MATRIX_1:36;
A15: ( @ ((Mx2Tran M) . f1) = Line (((LineVec2Mx (@ f1)) * M),1) & @ ((Mx2Tran M) . f2) = Line (((LineVec2Mx (@ f2)) * M),1) ) by A1, Def3;
@ (f1 + f2) = (@ f1) + (@ f2) by RVSUM_1:def_4;
then (LineVec2Mx (@ (f1 + f2))) * M = ((LineVec2Mx (@ f1)) + (LineVec2Mx (@ f2))) * M by A10, A6, MATRIX15:27
.= ((LineVec2Mx (@ f1)) * M) + ((LineVec2Mx (@ f2)) * M) by A1, A13, A5, A11, A7, A4, MATRIX_4:63 ;
hence (Mx2Tran M) . (f1 + f2) = Line ((((LineVec2Mx (@ f1)) * M) + ((LineVec2Mx (@ f2)) * M)),1) by A1, Def3
.= (Line (((LineVec2Mx (@ f1)) * M),1)) + (Line (((LineVec2Mx (@ f2)) * M),1)) by A12, A9, A14, MATRIX_4:59
.= ((Mx2Tran M) . f1) + ((Mx2Tran M) . f2) by A15, RVSUM_1:def_4 ;
::_thesis: verum
end;
end;
end;
supposeA16: n = 0 ; ::_thesis: (Mx2Tran M) . (f1 + f2) = ((Mx2Tran M) . f1) + ((Mx2Tran M) . f2)
A17: 0. (TOP-REAL m) = 0* m by EUCLID:70
.= m |-> 0 ;
then A18: (Mx2Tran M) . f2 = m |-> 0 by A16, Def3;
thus (Mx2Tran M) . (f1 + f2) = m |-> (0 + 0) by A16, A17, Def3
.= (m |-> 0) + (m |-> 0) by RVSUM_1:14
.= ((Mx2Tran M) . f1) + ((Mx2Tran M) . f2) by A16, A18 ; ::_thesis: verum
end;
end;
end;
theorem Th23: :: MATRTOP1:23
for n, m being Nat
for r being real number
for f being b1 -element real-valued FinSequence
for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (r * f) = r * ((Mx2Tran M) . f)
proof
let n, m be Nat; ::_thesis: for r being real number
for f being n -element real-valued FinSequence
for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (r * f) = r * ((Mx2Tran M) . f)
let r be real number ; ::_thesis: for f being n -element real-valued FinSequence
for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (r * f) = r * ((Mx2Tran M) . f)
let f be n -element real-valued FinSequence; ::_thesis: for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (r * f) = r * ((Mx2Tran M) . f)
let M be Matrix of n,m,F_Real; ::_thesis: (Mx2Tran M) . (r * f) = r * ((Mx2Tran M) . f)
set rf = r * f;
set T = Mx2Tran M;
percases ( n <> 0 or n = 0 ) ;
supposeA1: n <> 0 ; ::_thesis: (Mx2Tran M) . (r * f) = r * ((Mx2Tran M) . f)
percases ( m = 0 or m > 0 ) ;
supposeA2: m = 0 ; ::_thesis: (Mx2Tran M) . (r * f) = r * ((Mx2Tran M) . f)
then (Mx2Tran M) . (r * f) = 0.REAL 0 ;
hence (Mx2Tran M) . (r * f) = r * ((Mx2Tran M) . f) by A2; ::_thesis: verum
end;
suppose m > 0 ; ::_thesis: (Mx2Tran M) . (r * f) = r * ((Mx2Tran M) . f)
reconsider R = r as Element of F_Real by XREAL_0:def_1;
set Lr = LineVec2Mx (@ (r * f));
set L = LineVec2Mx (@ f);
A3: R * (@ f) = @ (r * f) by MATRIXR1:17;
len f = n by CARD_1:def_7;
then A4: width (LineVec2Mx (@ f)) = n by MATRIX13:1;
A5: len M = n by A1, MATRIX13:1;
len (LineVec2Mx (@ f)) = 1 by MATRIX13:1;
then A6: len ((LineVec2Mx (@ f)) * M) = 1 by A4, A5, MATRIX_3:def_4;
(Mx2Tran M) . (@ f) = Line (((LineVec2Mx (@ f)) * M),1) by A1, Def3;
hence r * ((Mx2Tran M) . f) = R * (Line (((LineVec2Mx (@ f)) * M),1)) by MATRIXR1:17
.= Line ((R * ((LineVec2Mx (@ f)) * M)),1) by A6, MATRIXR1:20
.= Line (((R * (LineVec2Mx (@ f))) * M),1) by A4, A5, MATRIX15:1
.= Line (((LineVec2Mx (@ (r * f))) * M),1) by A3, MATRIX15:29
.= (Mx2Tran M) . (r * f) by A1, Def3 ;
::_thesis: verum
end;
end;
end;
supposeA7: n = 0 ; ::_thesis: (Mx2Tran M) . (r * f) = r * ((Mx2Tran M) . f)
A8: 0. (TOP-REAL m) = 0* m by EUCLID:70
.= m |-> 0 ;
hence (Mx2Tran M) . (r * f) = m |-> (r * 0) by A7, Def3
.= r * (m |-> 0) by RVSUM_1:48
.= r * ((Mx2Tran M) . f) by A7, A8, Def3 ;
::_thesis: verum
end;
end;
end;
theorem Th24: :: MATRTOP1:24
for n, m being Nat
for f1, f2 being b1 -element real-valued FinSequence
for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (f1 - f2) = ((Mx2Tran M) . f1) - ((Mx2Tran M) . f2)
proof
let n, m be Nat; ::_thesis: for f1, f2 being n -element real-valued FinSequence
for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (f1 - f2) = ((Mx2Tran M) . f1) - ((Mx2Tran M) . f2)
let f1, f2 be n -element real-valued FinSequence; ::_thesis: for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (f1 - f2) = ((Mx2Tran M) . f1) - ((Mx2Tran M) . f2)
let M be Matrix of n,m,F_Real; ::_thesis: (Mx2Tran M) . (f1 - f2) = ((Mx2Tran M) . f1) - ((Mx2Tran M) . f2)
f1 - f2 = f1 + (- f2) by RVSUM_1:31
.= f1 + ((- 1) * f2) by RVSUM_1:54 ;
hence (Mx2Tran M) . (f1 - f2) = ((Mx2Tran M) . f1) + ((Mx2Tran M) . ((- 1) * f2)) by Th22
.= ((Mx2Tran M) . f1) + ((- 1) * ((Mx2Tran M) . f2)) by Th23
.= ((Mx2Tran M) . f1) + (- ((Mx2Tran M) . f2)) by RVSUM_1:54
.= ((Mx2Tran M) . f1) - ((Mx2Tran M) . f2) by RVSUM_1:31 ;
::_thesis: verum
end;
theorem :: MATRTOP1:25
for n, m being Nat
for f being b1 -element real-valued FinSequence
for M1, M2 being Matrix of n,m,F_Real holds (Mx2Tran (M1 + M2)) . f = ((Mx2Tran M1) . f) + ((Mx2Tran M2) . f)
proof
let n, m be Nat; ::_thesis: for f being n -element real-valued FinSequence
for M1, M2 being Matrix of n,m,F_Real holds (Mx2Tran (M1 + M2)) . f = ((Mx2Tran M1) . f) + ((Mx2Tran M2) . f)
let f be n -element real-valued FinSequence; ::_thesis: for M1, M2 being Matrix of n,m,F_Real holds (Mx2Tran (M1 + M2)) . f = ((Mx2Tran M1) . f) + ((Mx2Tran M2) . f)
let M1, M2 be Matrix of n,m,F_Real; ::_thesis: (Mx2Tran (M1 + M2)) . f = ((Mx2Tran M1) . f) + ((Mx2Tran M2) . f)
set T12 = Mx2Tran (M1 + M2);
set T2 = Mx2Tran M2;
set T1 = Mx2Tran M1;
percases ( n <> 0 or n = 0 ) ;
supposeA1: n <> 0 ; ::_thesis: (Mx2Tran (M1 + M2)) . f = ((Mx2Tran M1) . f) + ((Mx2Tran M2) . f)
percases ( m = 0 or m > 0 ) ;
supposeA2: m = 0 ; ::_thesis: (Mx2Tran (M1 + M2)) . f = ((Mx2Tran M1) . f) + ((Mx2Tran M2) . f)
then (Mx2Tran (M1 + M2)) . f = 0.REAL 0 ;
hence (Mx2Tran (M1 + M2)) . f = ((Mx2Tran M1) . f) + ((Mx2Tran M2) . f) by A2; ::_thesis: verum
end;
supposeA3: m > 0 ; ::_thesis: (Mx2Tran (M1 + M2)) . f = ((Mx2Tran M1) . f) + ((Mx2Tran M2) . f)
set L = LineVec2Mx (@ f);
len f = n by CARD_1:def_7;
then A4: width (LineVec2Mx (@ f)) = n by MATRIX13:1;
A5: ( len M2 = n & width M2 = m ) by A1, MATRIX13:1;
then A6: width ((LineVec2Mx (@ f)) * M2) = m by A4, MATRIX_3:def_4;
A7: 1 <= m by A3, NAT_1:14;
A8: len M1 = n by A1, MATRIX13:1;
A9: width M1 = m by A1, MATRIX13:1;
then A10: width ((LineVec2Mx (@ f)) * M1) = m by A4, A8, MATRIX_3:def_4;
A11: len (LineVec2Mx (@ f)) = 1 by MATRIX13:1;
then len ((LineVec2Mx (@ f)) * M1) = 1 by A4, A8, MATRIX_3:def_4;
then A12: [1,1] in Indices ((LineVec2Mx (@ f)) * M1) by A10, A7, MATRIX_1:36;
( @ ((Mx2Tran M1) . f) = Line (((LineVec2Mx (@ f)) * M1),1) & @ ((Mx2Tran M2) . f) = Line (((LineVec2Mx (@ f)) * M2),1) ) by A1, Def3;
hence ((Mx2Tran M1) . f) + ((Mx2Tran M2) . f) = (Line (((LineVec2Mx (@ f)) * M1),1)) + (Line (((LineVec2Mx (@ f)) * M2),1)) by RVSUM_1:def_4
.= Line ((((LineVec2Mx (@ f)) * M1) + ((LineVec2Mx (@ f)) * M2)),1) by A10, A6, A12, MATRIX_4:59
.= Line (((LineVec2Mx (@ f)) * (M1 + M2)),1) by A1, A11, A4, A8, A9, A5, MATRIX_4:62
.= (Mx2Tran (M1 + M2)) . f by A1, Def3 ;
::_thesis: verum
end;
end;
end;
supposeA13: n = 0 ; ::_thesis: (Mx2Tran (M1 + M2)) . f = ((Mx2Tran M1) . f) + ((Mx2Tran M2) . f)
A14: 0. (TOP-REAL m) = 0* m by EUCLID:70
.= m |-> 0 ;
then A15: (Mx2Tran M2) . f = m |-> 0 by A13, Def3;
thus (Mx2Tran (M1 + M2)) . f = m |-> (0 + 0) by A13, A14, Def3
.= (m |-> 0) + (m |-> 0) by RVSUM_1:14
.= ((Mx2Tran M1) . f) + ((Mx2Tran M2) . f) by A13, A14, A15, Def3 ; ::_thesis: verum
end;
end;
end;
theorem :: MATRTOP1:26
for n, m being Nat
for r being real number
for R being Element of F_Real
for f being b1 -element real-valued FinSequence
for M being Matrix of n,m,F_Real st r = R holds
r * ((Mx2Tran M) . f) = (Mx2Tran (R * M)) . f
proof
let n, m be Nat; ::_thesis: for r being real number
for R being Element of F_Real
for f being n -element real-valued FinSequence
for M being Matrix of n,m,F_Real st r = R holds
r * ((Mx2Tran M) . f) = (Mx2Tran (R * M)) . f
let r be real number ; ::_thesis: for R being Element of F_Real
for f being n -element real-valued FinSequence
for M being Matrix of n,m,F_Real st r = R holds
r * ((Mx2Tran M) . f) = (Mx2Tran (R * M)) . f
let R be Element of F_Real; ::_thesis: for f being n -element real-valued FinSequence
for M being Matrix of n,m,F_Real st r = R holds
r * ((Mx2Tran M) . f) = (Mx2Tran (R * M)) . f
let f be n -element real-valued FinSequence; ::_thesis: for M being Matrix of n,m,F_Real st r = R holds
r * ((Mx2Tran M) . f) = (Mx2Tran (R * M)) . f
let M be Matrix of n,m,F_Real; ::_thesis: ( r = R implies r * ((Mx2Tran M) . f) = (Mx2Tran (R * M)) . f )
set L = LineVec2Mx (@ f);
set RM = R * M;
set T = Mx2Tran M;
set TR = Mx2Tran (R * M);
assume A1: r = R ; ::_thesis: r * ((Mx2Tran M) . f) = (Mx2Tran (R * M)) . f
percases ( n <> 0 or n = 0 ) ;
supposeA2: n <> 0 ; ::_thesis: r * ((Mx2Tran M) . f) = (Mx2Tran (R * M)) . f
A3: len M = n by A2, MATRIX13:1;
len f = n by CARD_1:def_7;
then A4: width (LineVec2Mx (@ f)) = n by MATRIX13:1;
len (LineVec2Mx (@ f)) = 1 by MATRIX13:1;
then A5: len ((LineVec2Mx (@ f)) * M) = 1 by A4, A3, MATRIX_3:def_4;
(Mx2Tran M) . f = Line (((LineVec2Mx (@ f)) * M),1) by A2, Def3;
hence r * ((Mx2Tran M) . f) = R * (Line (((LineVec2Mx (@ f)) * M),1)) by A1, MATRIXR1:17
.= Line ((R * ((LineVec2Mx (@ f)) * M)),1) by A5, MATRIXR1:20
.= Line (((LineVec2Mx (@ f)) * (R * M)),1) by A4, A3, MATRIXR1:22
.= (Mx2Tran (R * M)) . f by A2, Def3 ;
::_thesis: verum
end;
supposeA6: n = 0 ; ::_thesis: r * ((Mx2Tran M) . f) = (Mx2Tran (R * M)) . f
A7: 0. (TOP-REAL m) = 0* m by EUCLID:70
.= m |-> 0 ;
hence r * ((Mx2Tran M) . f) = r * (m |-> 0) by A6, Def3
.= m |-> (r * 0) by RVSUM_1:48
.= (Mx2Tran (R * M)) . f by A6, A7, Def3 ;
::_thesis: verum
end;
end;
end;
theorem Th27: :: MATRTOP1:27
for n, m being Nat
for p1, p2 being Point of (TOP-REAL n)
for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (p1 + p2) = ((Mx2Tran M) . p1) + ((Mx2Tran M) . p2) by Th22;
theorem Th28: :: MATRTOP1:28
for n, m being Nat
for p1, p2 being Point of (TOP-REAL n)
for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (p1 - p2) = ((Mx2Tran M) . p1) - ((Mx2Tran M) . p2) by Th24;
theorem Th29: :: MATRTOP1:29
for n, m being Nat
for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (0. (TOP-REAL n)) = 0. (TOP-REAL m)
proof
let n, m be Nat; ::_thesis: for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (0. (TOP-REAL n)) = 0. (TOP-REAL m)
let M be Matrix of n,m,F_Real; ::_thesis: (Mx2Tran M) . (0. (TOP-REAL n)) = 0. (TOP-REAL m)
set TRn = the Element of (TOP-REAL n);
set MT = Mx2Tran M;
0. (TOP-REAL n) = the Element of (TOP-REAL n) - the Element of (TOP-REAL n) by EUCLID:42;
hence (Mx2Tran M) . (0. (TOP-REAL n)) = ((Mx2Tran M) . the Element of (TOP-REAL n)) - ((Mx2Tran M) . the Element of (TOP-REAL n)) by Th28
.= 0. (TOP-REAL m) by EUCLID:42 ;
::_thesis: verum
end;
theorem :: MATRTOP1:30
for m, n being Nat
for p being Point of (TOP-REAL n)
for M being Matrix of n,m,F_Real
for A being Subset of (TOP-REAL n) holds (Mx2Tran M) .: (p + A) = ((Mx2Tran M) . p) + ((Mx2Tran M) .: A)
proof
let m, n be Nat; ::_thesis: for p being Point of (TOP-REAL n)
for M being Matrix of n,m,F_Real
for A being Subset of (TOP-REAL n) holds (Mx2Tran M) .: (p + A) = ((Mx2Tran M) . p) + ((Mx2Tran M) .: A)
let p be Point of (TOP-REAL n); ::_thesis: for M being Matrix of n,m,F_Real
for A being Subset of (TOP-REAL n) holds (Mx2Tran M) .: (p + A) = ((Mx2Tran M) . p) + ((Mx2Tran M) .: A)
let M be Matrix of n,m,F_Real; ::_thesis: for A being Subset of (TOP-REAL n) holds (Mx2Tran M) .: (p + A) = ((Mx2Tran M) . p) + ((Mx2Tran M) .: A)
set TRn = TOP-REAL n;
set TRm = TOP-REAL m;
set MT = Mx2Tran M;
let A be Subset of (TOP-REAL n); ::_thesis: (Mx2Tran M) .: (p + A) = ((Mx2Tran M) . p) + ((Mx2Tran M) .: A)
A1: dom (Mx2Tran M) = [#] (TOP-REAL n) by FUNCT_2:def_1;
thus (Mx2Tran M) .: (p + A) c= ((Mx2Tran M) . p) + ((Mx2Tran M) .: A) :: according to XBOOLE_0:def_10 ::_thesis: ((Mx2Tran M) . p) + ((Mx2Tran M) .: A) c= (Mx2Tran M) .: (p + A)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (Mx2Tran M) .: (p + A) or y in ((Mx2Tran M) . p) + ((Mx2Tran M) .: A) )
assume y in (Mx2Tran M) .: (p + A) ; ::_thesis: y in ((Mx2Tran M) . p) + ((Mx2Tran M) .: A)
then consider x being set such that
x in dom (Mx2Tran M) and
A2: x in p + A and
A3: (Mx2Tran M) . x = y by FUNCT_1:def_6;
x in { (p + w) where w is Element of (TOP-REAL n) : w in A } by A2, RUSUB_4:def_8;
then consider w being Element of (TOP-REAL n) such that
A4: ( x = p + w & w in A ) ;
( (Mx2Tran M) . w in (Mx2Tran M) .: A & (Mx2Tran M) . x = ((Mx2Tran M) . p) + ((Mx2Tran M) . w) ) by A1, A4, Th27, FUNCT_1:def_6;
then (Mx2Tran M) . x in { (((Mx2Tran M) . p) + u) where u is Element of (TOP-REAL m) : u in (Mx2Tran M) .: A } ;
hence y in ((Mx2Tran M) . p) + ((Mx2Tran M) .: A) by A3, RUSUB_4:def_8; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in ((Mx2Tran M) . p) + ((Mx2Tran M) .: A) or y in (Mx2Tran M) .: (p + A) )
assume y in ((Mx2Tran M) . p) + ((Mx2Tran M) .: A) ; ::_thesis: y in (Mx2Tran M) .: (p + A)
then y in { (((Mx2Tran M) . p) + u) where u is Element of (TOP-REAL m) : u in (Mx2Tran M) .: A } by RUSUB_4:def_8;
then consider u being Element of (TOP-REAL m) such that
A5: y = ((Mx2Tran M) . p) + u and
A6: u in (Mx2Tran M) .: A ;
consider w being set such that
w in dom (Mx2Tran M) and
A7: w in A and
A8: (Mx2Tran M) . w = u by A6, FUNCT_1:def_6;
reconsider w = w as Element of (TOP-REAL n) by A7;
p + w in { (p + L) where L is Element of (TOP-REAL n) : L in A } by A7;
then A9: p + w in p + A by RUSUB_4:def_8;
y = (Mx2Tran M) . (p + w) by A5, A8, Th27;
hence y in (Mx2Tran M) .: (p + A) by A1, A9, FUNCT_1:def_6; ::_thesis: verum
end;
theorem :: MATRTOP1:31
for n, m being Nat
for p being Point of (TOP-REAL n)
for M being Matrix of n,m,F_Real
for A being Subset of (TOP-REAL m) holds (Mx2Tran M) " (((Mx2Tran M) . p) + A) = p + ((Mx2Tran M) " A)
proof
let n, m be Nat; ::_thesis: for p being Point of (TOP-REAL n)
for M being Matrix of n,m,F_Real
for A being Subset of (TOP-REAL m) holds (Mx2Tran M) " (((Mx2Tran M) . p) + A) = p + ((Mx2Tran M) " A)
let p be Point of (TOP-REAL n); ::_thesis: for M being Matrix of n,m,F_Real
for A being Subset of (TOP-REAL m) holds (Mx2Tran M) " (((Mx2Tran M) . p) + A) = p + ((Mx2Tran M) " A)
let M be Matrix of n,m,F_Real; ::_thesis: for A being Subset of (TOP-REAL m) holds (Mx2Tran M) " (((Mx2Tran M) . p) + A) = p + ((Mx2Tran M) " A)
set MT = Mx2Tran M;
set TRn = TOP-REAL n;
set TRm = TOP-REAL m;
let A be Subset of (TOP-REAL m); ::_thesis: (Mx2Tran M) " (((Mx2Tran M) . p) + A) = p + ((Mx2Tran M) " A)
set w = p;
set MTw = (Mx2Tran M) . p;
A1: p + ((Mx2Tran M) " A) = { (p + v) where v is Element of (TOP-REAL n) : v in (Mx2Tran M) " A } by RUSUB_4:def_8;
A2: ((Mx2Tran M) . p) + A = { (((Mx2Tran M) . p) + v) where v is Element of (TOP-REAL m) : v in A } by RUSUB_4:def_8;
A3: dom (Mx2Tran M) = [#] (TOP-REAL n) by FUNCT_2:def_1;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: p + ((Mx2Tran M) " A) c= (Mx2Tran M) " (((Mx2Tran M) . p) + A)
let x be set ; ::_thesis: ( x in (Mx2Tran M) " (((Mx2Tran M) . p) + A) implies x in p + ((Mx2Tran M) " A) )
assume A4: x in (Mx2Tran M) " (((Mx2Tran M) . p) + A) ; ::_thesis: x in p + ((Mx2Tran M) " A)
then reconsider f = x as Element of (TOP-REAL n) ;
(Mx2Tran M) . x in ((Mx2Tran M) . p) + A by A4, FUNCT_1:def_7;
then consider v being Element of (TOP-REAL m) such that
A5: (Mx2Tran M) . x = ((Mx2Tran M) . p) + v and
A6: v in A by A2;
((Mx2Tran M) . f) - ((Mx2Tran M) . p) = (v + ((Mx2Tran M) . p)) - ((Mx2Tran M) . p) by A5
.= v + (((Mx2Tran M) . p) - ((Mx2Tran M) . p)) by RLVECT_1:28
.= v + (0. (TOP-REAL m)) by RLVECT_1:15
.= v by RLVECT_1:4 ;
then v = (Mx2Tran M) . (f - p) by Th28;
then A7: f - p in (Mx2Tran M) " A by A3, A6, FUNCT_1:def_7;
p + (f - p) = (f - p) + p
.= f - (p - p) by RLVECT_1:29
.= f - (0. (TOP-REAL n)) by RLVECT_1:15
.= f by RLVECT_1:13 ;
hence x in p + ((Mx2Tran M) " A) by A1, A7; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in p + ((Mx2Tran M) " A) or x in (Mx2Tran M) " (((Mx2Tran M) . p) + A) )
assume x in p + ((Mx2Tran M) " A) ; ::_thesis: x in (Mx2Tran M) " (((Mx2Tran M) . p) + A)
then consider v being Element of (TOP-REAL n) such that
A8: x = p + v and
A9: v in (Mx2Tran M) " A by A1;
A10: (Mx2Tran M) . v in A by A9, FUNCT_1:def_7;
(Mx2Tran M) . (p + v) = ((Mx2Tran M) . p) + ((Mx2Tran M) . v) by Th27;
then (Mx2Tran M) . x in ((Mx2Tran M) . p) + A by A2, A8, A10;
hence x in (Mx2Tran M) " (((Mx2Tran M) . p) + A) by A3, A8, FUNCT_1:def_7; ::_thesis: verum
end;
theorem Th32: :: MATRTOP1:32
for n, m, k being Nat
for A being Matrix of n,m,F_Real
for B being Matrix of width A,k,F_Real st ( n = 0 implies m = 0 ) & ( m = 0 implies k = 0 ) holds
(Mx2Tran B) * (Mx2Tran A) = Mx2Tran (A * B)
proof
let n, m, k be Nat; ::_thesis: for A being Matrix of n,m,F_Real
for B being Matrix of width A,k,F_Real st ( n = 0 implies m = 0 ) & ( m = 0 implies k = 0 ) holds
(Mx2Tran B) * (Mx2Tran A) = Mx2Tran (A * B)
let A be Matrix of n,m,F_Real; ::_thesis: for B being Matrix of width A,k,F_Real st ( n = 0 implies m = 0 ) & ( m = 0 implies k = 0 ) holds
(Mx2Tran B) * (Mx2Tran A) = Mx2Tran (A * B)
let B be Matrix of width A,k,F_Real; ::_thesis: ( ( n = 0 implies m = 0 ) & ( m = 0 implies k = 0 ) implies (Mx2Tran B) * (Mx2Tran A) = Mx2Tran (A * B) )
assume that
A1: ( n = 0 implies m = 0 ) and
A2: ( m = 0 implies k = 0 ) ; ::_thesis: (Mx2Tran B) * (Mx2Tran A) = Mx2Tran (A * B)
reconsider Bk = MX2FinS (1. (F_Real,k)) as OrdBasis of k -VectSp_over F_Real by MATRLIN2:45;
reconsider Bm = MX2FinS (1. (F_Real,m)) as OrdBasis of m -VectSp_over F_Real by MATRLIN2:45;
reconsider Bn = MX2FinS (1. (F_Real,n)) as OrdBasis of n -VectSp_over F_Real by MATRLIN2:45;
A3: len A = n by A1, MATRIX13:1;
A4: len Bn = n by Th19;
then reconsider A1 = A as Matrix of len Bn, len Bm,F_Real by Th19;
A5: Mx2Tran A = Mx2Tran (A1,Bn,Bm) by Th20;
A6: width A = m by A1, MATRIX13:1;
then A7: width B = k by A2, MATRIX13:1;
then reconsider AB = A * B as Matrix of len Bn, len Bk,F_Real by A3, A4, Th19;
len Bm = m by Th19;
then reconsider B1 = B as Matrix of len Bm, len Bk,F_Real by A6, Th19;
A8: len B1 = m by A2, A6, MATRIX13:1;
Mx2Tran (A * B) = Mx2Tran (AB,Bn,Bk) by A3, A7, Th20;
then Mx2Tran (A * B) = (Mx2Tran (B1,Bm,Bk)) * (Mx2Tran (A1,Bn,Bm)) by A6, A8, MATRLIN2:40;
hence (Mx2Tran B) * (Mx2Tran A) = Mx2Tran (A * B) by A6, A5, Th20; ::_thesis: verum
end;
theorem Th33: :: MATRTOP1:33
for n being Nat holds Mx2Tran (1. (F_Real,n)) = id (TOP-REAL n)
proof
let n be Nat; ::_thesis: Mx2Tran (1. (F_Real,n)) = id (TOP-REAL n)
set V = n -VectSp_over F_Real;
reconsider Bn = MX2FinS (1. (F_Real,n)) as OrdBasis of n -VectSp_over F_Real by MATRLIN2:45;
A1: len Bn = n by Th19;
then reconsider ONE = 1. (F_Real,n) as Matrix of len Bn, len Bn,F_Real ;
A2: Mx2Tran (1. (F_Real,n)) = Mx2Tran (ONE,Bn,Bn) by Th20;
A3: [#] (TOP-REAL n) = dom (Mx2Tran (1. (F_Real,n))) by FUNCT_2:def_1
.= [#] (n -VectSp_over F_Real) by A2, FUNCT_2:def_1 ;
thus Mx2Tran (1. (F_Real,n)) = Mx2Tran ((AutMt ((id (n -VectSp_over F_Real)),Bn,Bn)),Bn,Bn) by A1, Th20, MATRLIN2:28
.= id (TOP-REAL n) by A3, MATRLIN2:34 ; ::_thesis: verum
end;
theorem Th34: :: MATRTOP1:34
for n, m being Nat
for M1, M2 being Matrix of n,m,F_Real st Mx2Tran M1 = Mx2Tran M2 holds
M1 = M2
proof
let n, m be Nat; ::_thesis: for M1, M2 being Matrix of n,m,F_Real st Mx2Tran M1 = Mx2Tran M2 holds
M1 = M2
let M1, M2 be Matrix of n,m,F_Real; ::_thesis: ( Mx2Tran M1 = Mx2Tran M2 implies M1 = M2 )
assume A1: Mx2Tran M1 = Mx2Tran M2 ; ::_thesis: M1 = M2
set Vn = n -VectSp_over F_Real;
set Vm = m -VectSp_over F_Real;
reconsider Bn = MX2FinS (1. (F_Real,n)) as OrdBasis of n -VectSp_over F_Real by MATRLIN2:45;
reconsider Bm = MX2FinS (1. (F_Real,m)) as OrdBasis of m -VectSp_over F_Real by MATRLIN2:45;
len Bn = n by Th19;
then reconsider A1 = M1, B1 = M2 as Matrix of len Bn, len Bm,F_Real by Th19;
A2: Mx2Tran (A1,Bn,Bm) = Mx2Tran M1 by Th20
.= Mx2Tran (B1,Bn,Bm) by A1, Th20 ;
thus M1 = AutMt ((Mx2Tran (A1,Bn,Bm)),Bn,Bm) by MATRLIN2:36
.= M2 by A2, MATRLIN2:36 ; ::_thesis: verum
end;
theorem Th35: :: MATRTOP1:35
for n, m, k being Nat
for f being b1 -element real-valued FinSequence
for A being Matrix of n,m,F_Real
for B being Matrix of k,m,F_Real holds
( (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = (Mx2Tran A) . f & (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = (Mx2Tran A) . f )
proof
let n, m, k be Nat; ::_thesis: for f being n -element real-valued FinSequence
for A being Matrix of n,m,F_Real
for B being Matrix of k,m,F_Real holds
( (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = (Mx2Tran A) . f & (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = (Mx2Tran A) . f )
let f be n -element real-valued FinSequence; ::_thesis: for A being Matrix of n,m,F_Real
for B being Matrix of k,m,F_Real holds
( (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = (Mx2Tran A) . f & (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = (Mx2Tran A) . f )
let A be Matrix of n,m,F_Real; ::_thesis: for B being Matrix of k,m,F_Real holds
( (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = (Mx2Tran A) . f & (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = (Mx2Tran A) . f )
let B be Matrix of k,m,F_Real; ::_thesis: ( (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = (Mx2Tran A) . f & (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = (Mx2Tran A) . f )
reconsider k0 = k |-> 0 as k -element FinSequence of REAL ;
A1: len B = k by MATRIX_1:def_2;
set kf = k0 ^ f;
percases ( n <> 0 or n = 0 ) ;
supposeA2: n <> 0 ; ::_thesis: ( (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = (Mx2Tran A) . f & (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = (Mx2Tran A) . f )
then A3: width A = m by MATRIX13:1;
A4: ( len f = n & len k0 = k ) by CARD_1:def_7;
then len (k0 ^ f) = n + k by FINSEQ_1:22;
then A5: k0 ^ f is n + k -element by CARD_1:def_7;
A6: len A = n by A2, MATRIX13:1;
thus (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = (Mx2Tran A) . f ::_thesis: (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = (Mx2Tran A) . f
proof
set fk = f ^ k0;
len (f ^ k0) = n + k by A4, FINSEQ_1:22;
then A7: f ^ k0 is n + k -element by CARD_1:def_7;
percases ( k = 0 or k <> 0 ) ;
supposeA8: k = 0 ; ::_thesis: (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = (Mx2Tran A) . f
then B is empty by A1;
then A9: Mx2Tran (A ^ B) = Mx2Tran A by A8, FINSEQ_1:34;
k0 is empty by A8;
hence (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = (Mx2Tran A) . f by A9, FINSEQ_1:34; ::_thesis: verum
end;
supposeA10: k <> 0 ; ::_thesis: (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = (Mx2Tran A) . f
set Mab = Mx2Tran (A ^ B);
set Ma = Mx2Tran A;
A11: width B = m by A10, MATRIX_1:23;
A12: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_m_holds_
((Mx2Tran_A)_._f)_._i_=_((Mx2Tran_(A_^_B))_._(f_^_k0))_._i
let i be Nat; ::_thesis: ( 1 <= i & i <= m implies ((Mx2Tran A) . f) . i = ((Mx2Tran (A ^ B)) . (f ^ k0)) . i )
reconsider S1 = Sum (mlt ((@ k0),(Col (B,i)))), S2 = Sum (mlt ((@ f),(Col (A,i)))) as Element of F_Real ;
assume A13: ( 1 <= i & i <= m ) ; ::_thesis: ((Mx2Tran A) . f) . i = ((Mx2Tran (A ^ B)) . (f ^ k0)) . i
then A14: i in Seg m by FINSEQ_1:1;
mlt ((@ k0),(Col (B,i))) = (0. F_Real) * (Col (B,i)) by A1, FVSUM_1:66
.= k |-> (0. F_Real) by A1, FVSUM_1:58 ;
then A15: Sum (mlt ((@ k0),(Col (B,i)))) = Sum (k |-> 0) by MATRPROB:36
.= 0. F_Real by RVSUM_1:81 ;
A16: ( len (Col (A,i)) = n & len (Col (B,i)) = k ) by A6, A1, MATRIX_1:def_8;
mlt ((@ (f ^ k0)),(Col ((A ^ B),i))) = mlt (((@ f) ^ (@ k0)),((Col (A,i)) ^ (Col (B,i)))) by A3, A11, A14, MATRLIN:26
.= (mlt ((@ f),(Col (A,i)))) ^ (mlt ((@ k0),(Col (B,i)))) by A4, A16, MATRIX14:7 ;
then Sum (mlt ((@ (f ^ k0)),(Col ((A ^ B),i)))) = addreal . ((Sum (mlt ((@ f),(Col (A,i))))),(Sum (mlt ((@ k0),(Col (B,i)))))) by FINSOP_1:5
.= (Sum (mlt ((@ f),(Col (A,i))))) + (Sum (mlt ((@ k0),(Col (B,i))))) by BINOP_2:def_9
.= (@ f) "*" (Col (A,i)) by A15 ;
hence ((Mx2Tran A) . f) . i = (@ (f ^ k0)) "*" (Col ((A ^ B),i)) by A2, A13, Th18
.= ((Mx2Tran (A ^ B)) . (f ^ k0)) . i by A2, A7, A13, Th18 ;
::_thesis: verum
end;
( len ((Mx2Tran (A ^ B)) . (f ^ k0)) = m & len ((Mx2Tran A) . f) = m ) by A7, CARD_1:def_7;
hence (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = (Mx2Tran A) . f by A12, FINSEQ_1:14; ::_thesis: verum
end;
end;
end;
percases ( k = 0 or k <> 0 ) ;
supposeA17: k = 0 ; ::_thesis: (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = (Mx2Tran A) . f
then B is empty by A1;
then A18: Mx2Tran (B ^ A) = Mx2Tran A by A17, FINSEQ_1:34;
k0 is empty by A17;
hence (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = (Mx2Tran A) . f by A18, FINSEQ_1:34; ::_thesis: verum
end;
supposeA19: k <> 0 ; ::_thesis: (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = (Mx2Tran A) . f
set Mba = Mx2Tran (B ^ A);
set Ma = Mx2Tran A;
A20: width B = m by A19, MATRIX_1:23;
A21: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_m_holds_
((Mx2Tran_A)_._f)_._i_=_((Mx2Tran_(B_^_A))_._(k0_^_f))_._i
let i be Nat; ::_thesis: ( 1 <= i & i <= m implies ((Mx2Tran A) . f) . i = ((Mx2Tran (B ^ A)) . (k0 ^ f)) . i )
reconsider S1 = Sum (mlt ((@ k0),(Col (B,i)))), S2 = Sum (mlt ((@ f),(Col (A,i)))) as Element of F_Real ;
assume A22: ( 1 <= i & i <= m ) ; ::_thesis: ((Mx2Tran A) . f) . i = ((Mx2Tran (B ^ A)) . (k0 ^ f)) . i
then A23: i in Seg m by FINSEQ_1:1;
mlt ((@ k0),(Col (B,i))) = (0. F_Real) * (Col (B,i)) by A1, FVSUM_1:66
.= k |-> (0. F_Real) by A1, FVSUM_1:58 ;
then A24: Sum (mlt ((@ k0),(Col (B,i)))) = Sum (k |-> 0) by MATRPROB:36
.= 0. F_Real by RVSUM_1:81 ;
A25: ( len (Col (A,i)) = n & len (Col (B,i)) = k ) by A6, A1, MATRIX_1:def_8;
mlt ((@ (k0 ^ f)),(Col ((B ^ A),i))) = mlt (((@ k0) ^ (@ f)),((Col (B,i)) ^ (Col (A,i)))) by A3, A20, A23, MATRLIN:26
.= (mlt ((@ k0),(Col (B,i)))) ^ (mlt ((@ f),(Col (A,i)))) by A4, A25, MATRIX14:7 ;
then Sum (mlt ((@ (k0 ^ f)),(Col ((B ^ A),i)))) = addreal . ((Sum (mlt ((@ k0),(Col (B,i))))),(Sum (mlt ((@ f),(Col (A,i)))))) by FINSOP_1:5
.= (Sum (mlt ((@ f),(Col (A,i))))) + (0. F_Real) by A24, BINOP_2:def_9
.= (@ f) "*" (Col (A,i)) ;
hence ((Mx2Tran A) . f) . i = (@ (k0 ^ f)) "*" (Col ((B ^ A),i)) by A2, A22, Th18
.= ((Mx2Tran (B ^ A)) . (k0 ^ f)) . i by A2, A5, A22, Th18 ;
::_thesis: verum
end;
( len ((Mx2Tran (B ^ A)) . (k0 ^ f)) = m & len ((Mx2Tran A) . f) = m ) by A5, CARD_1:def_7;
hence (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = (Mx2Tran A) . f by A21, FINSEQ_1:14; ::_thesis: verum
end;
end;
end;
supposeA26: n = 0 ; ::_thesis: ( (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = (Mx2Tran A) . f & (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = (Mx2Tran A) . f )
A27: 0. (TOP-REAL k) = 0* k by EUCLID:70
.= k |-> 0 ;
f = {} by A26;
then A28: ( f ^ (k |-> 0) = k |-> 0 & (k |-> 0) ^ f = k |-> 0 ) by FINSEQ_1:34;
thus (Mx2Tran (A ^ B)) . (f ^ (k |-> 0)) = 0. (TOP-REAL m) by A27, A28, Th29, A26
.= (Mx2Tran A) . f by A26, Def3 ; ::_thesis: (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = (Mx2Tran A) . f
thus (Mx2Tran (B ^ A)) . ((k |-> 0) ^ f) = 0. (TOP-REAL m) by A27, A28, Th29, A26
.= (Mx2Tran A) . f by A26, Def3 ; ::_thesis: verum
end;
end;
end;
theorem :: MATRTOP1:36
for n, m, k being Nat
for f being b1 -element real-valued FinSequence
for A being Matrix of n,m,F_Real
for B being Matrix of k,m,F_Real
for g being b3 -element real-valued FinSequence holds (Mx2Tran (A ^ B)) . (f ^ g) = ((Mx2Tran A) . f) + ((Mx2Tran B) . g)
proof
let n, m, k be Nat; ::_thesis: for f being n -element real-valued FinSequence
for A being Matrix of n,m,F_Real
for B being Matrix of k,m,F_Real
for g being k -element real-valued FinSequence holds (Mx2Tran (A ^ B)) . (f ^ g) = ((Mx2Tran A) . f) + ((Mx2Tran B) . g)
let f be n -element real-valued FinSequence; ::_thesis: for A being Matrix of n,m,F_Real
for B being Matrix of k,m,F_Real
for g being k -element real-valued FinSequence holds (Mx2Tran (A ^ B)) . (f ^ g) = ((Mx2Tran A) . f) + ((Mx2Tran B) . g)
A1: len f = n by CARD_1:def_7;
rng f c= REAL ;
then f is FinSequence of REAL by FINSEQ_1:def_4;
then reconsider F = f, n0 = n |-> 0 as Element of n -tuples_on REAL by A1, FINSEQ_2:92;
let A be Matrix of n,m,F_Real; ::_thesis: for B being Matrix of k,m,F_Real
for g being k -element real-valued FinSequence holds (Mx2Tran (A ^ B)) . (f ^ g) = ((Mx2Tran A) . f) + ((Mx2Tran B) . g)
let B be Matrix of k,m,F_Real; ::_thesis: for g being k -element real-valued FinSequence holds (Mx2Tran (A ^ B)) . (f ^ g) = ((Mx2Tran A) . f) + ((Mx2Tran B) . g)
let g be k -element real-valued FinSequence; ::_thesis: (Mx2Tran (A ^ B)) . (f ^ g) = ((Mx2Tran A) . f) + ((Mx2Tran B) . g)
A2: len g = k by CARD_1:def_7;
rng g c= REAL ;
then g is FinSequence of REAL by FINSEQ_1:def_4;
then reconsider G = g, k0 = k |-> 0 as Element of k -tuples_on REAL by A2, FINSEQ_2:92;
len (n |-> 0) = n by CARD_1:def_7;
then len (n0 ^ G) = n + k by A2, FINSEQ_1:22;
then A3: n0 ^ G is n + k -element by CARD_1:def_7;
len (k |-> 0) = k by CARD_1:def_7;
then len (F ^ k0) = n + k by A1, FINSEQ_1:22;
then A4: F ^ k0 is n + k -element by CARD_1:def_7;
f = F + n0 by RVSUM_1:16;
then ( g = G + k0 & f = addreal .: (f,n0) ) by RVSUM_1:16, RVSUM_1:def_4;
then f ^ g = (addreal .: (F,n0)) ^ (addreal .: (k0,G)) by RVSUM_1:def_4
.= addreal .: ((F ^ k0),(n0 ^ G)) by FINSEQOP:11
.= (F ^ k0) + (n0 ^ G) by RVSUM_1:def_4 ;
hence (Mx2Tran (A ^ B)) . (f ^ g) = ((Mx2Tran (A ^ B)) . (F ^ k0)) + ((Mx2Tran (A ^ B)) . (n0 ^ G)) by A4, A3, Th22
.= ((Mx2Tran A) . f) + ((Mx2Tran (A ^ B)) . (n0 ^ G)) by Th35
.= ((Mx2Tran A) . f) + ((Mx2Tran B) . g) by Th35 ;
::_thesis: verum
end;
theorem :: MATRTOP1:37
for n, k, m being Nat
for f being b1 -element real-valued FinSequence
for A being Matrix of n,k,F_Real
for B being Matrix of n,m,F_Real st ( n = 0 implies k + m = 0 ) holds
(Mx2Tran (A ^^ B)) . f = ((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)
proof
let n, k, m be Nat; ::_thesis: for f being n -element real-valued FinSequence
for A being Matrix of n,k,F_Real
for B being Matrix of n,m,F_Real st ( n = 0 implies k + m = 0 ) holds
(Mx2Tran (A ^^ B)) . f = ((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)
let f be n -element real-valued FinSequence; ::_thesis: for A being Matrix of n,k,F_Real
for B being Matrix of n,m,F_Real st ( n = 0 implies k + m = 0 ) holds
(Mx2Tran (A ^^ B)) . f = ((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)
let A be Matrix of n,k,F_Real; ::_thesis: for B being Matrix of n,m,F_Real st ( n = 0 implies k + m = 0 ) holds
(Mx2Tran (A ^^ B)) . f = ((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)
let B be Matrix of n,m,F_Real; ::_thesis: ( ( n = 0 implies k + m = 0 ) implies (Mx2Tran (A ^^ B)) . f = ((Mx2Tran A) . f) ^ ((Mx2Tran B) . f) )
set L = LineVec2Mx (@ f);
set MAB = (Mx2Tran (A ^^ B)) . f;
set MA = (Mx2Tran A) . f;
set MB = (Mx2Tran B) . f;
A1: len ((Mx2Tran A) . f) = k by CARD_1:def_7;
assume A2: ( n = 0 implies k + m = 0 ) ; ::_thesis: (Mx2Tran (A ^^ B)) . f = ((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)
then ( n = 0 implies k = 0 ) ;
then A3: width A = k by MATRIX13:1;
( n = 0 implies m = 0 ) by A2;
then A4: width B = m by MATRIX13:1;
A5: len ((Mx2Tran B) . f) = m by CARD_1:def_7;
then A6: len (((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)) = k + m by A1, FINSEQ_1:22;
A7: for i being Nat st 1 <= i & i <= k + m holds
(((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)) . i = ((Mx2Tran (A ^^ B)) . f) . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= k + m implies (((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)) . i = ((Mx2Tran (A ^^ B)) . f) . i )
assume that
A8: 1 <= i and
A9: i <= k + m ; ::_thesis: (((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)) . i = ((Mx2Tran (A ^^ B)) . f) . i
A10: i in dom (((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)) by A6, A8, A9, FINSEQ_3:25;
A11: ((Mx2Tran (A ^^ B)) . f) . i = (@ f) "*" (Col ((A ^^ B),i)) by A2, A3, A4, A8, A9, Th18;
percases ( i in dom ((Mx2Tran A) . f) or ex j being Nat st
( j in dom ((Mx2Tran B) . f) & i = (len ((Mx2Tran A) . f)) + j ) ) by A10, FINSEQ_1:25;
supposeA12: i in dom ((Mx2Tran A) . f) ; ::_thesis: (((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)) . i = ((Mx2Tran (A ^^ B)) . f) . i
then i <= k by A1, FINSEQ_3:25;
then A13: ((Mx2Tran A) . f) . i = (@ f) "*" (Col (A,i)) by A2, A8, Th18;
( i in Seg (width A) & (((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)) . i = ((Mx2Tran A) . f) . i ) by A3, A1, A12, FINSEQ_1:def_3, FINSEQ_1:def_7;
hence (((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)) . i = ((Mx2Tran (A ^^ B)) . f) . i by A11, A13, MATRIX15:16; ::_thesis: verum
end;
suppose ex j being Nat st
( j in dom ((Mx2Tran B) . f) & i = (len ((Mx2Tran A) . f)) + j ) ; ::_thesis: (((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)) . i = ((Mx2Tran (A ^^ B)) . f) . i
then consider j being Nat such that
A14: j in dom ((Mx2Tran B) . f) and
A15: i = (len ((Mx2Tran A) . f)) + j ;
( 1 <= j & j <= m ) by A5, A14, FINSEQ_3:25;
then A16: ((Mx2Tran B) . f) . j = (@ f) "*" (Col (B,j)) by A2, Th18;
( j in Seg (width B) & (((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)) . i = ((Mx2Tran B) . f) . j ) by A4, A5, A14, A15, FINSEQ_1:def_3, FINSEQ_1:def_7;
hence (((Mx2Tran A) . f) ^ ((Mx2Tran B) . f)) . i = ((Mx2Tran (A ^^ B)) . f) . i by A3, A1, A11, A15, A16, MATRIX15:17; ::_thesis: verum
end;
end;
end;
len ((Mx2Tran (A ^^ B)) . f) = k + m by A3, A4, CARD_1:def_7;
hence (Mx2Tran (A ^^ B)) . f = ((Mx2Tran A) . f) ^ ((Mx2Tran B) . f) by A6, A7, FINSEQ_1:14; ::_thesis: verum
end;
theorem :: MATRTOP1:38
for m, n being Nat
for f being b2 -element real-valued FinSequence
for M being Matrix of n,m,F_Real st M = (1. (F_Real,m)) | n holds
((Mx2Tran M) . f) | n = f
proof
let m, n be Nat; ::_thesis: for f being n -element real-valued FinSequence
for M being Matrix of n,m,F_Real st M = (1. (F_Real,m)) | n holds
((Mx2Tran M) . f) | n = f
let f be n -element real-valued FinSequence; ::_thesis: for M being Matrix of n,m,F_Real st M = (1. (F_Real,m)) | n holds
((Mx2Tran M) . f) | n = f
let M be Matrix of n,m,F_Real; ::_thesis: ( M = (1. (F_Real,m)) | n implies ((Mx2Tran M) . f) | n = f )
set ONE = 1. (F_Real,m);
assume A1: M = (1. (F_Real,m)) | n ; ::_thesis: ((Mx2Tran M) . f) | n = f
percases ( n = 0 or n > 0 ) ;
supposeA2: n = 0 ; ::_thesis: ((Mx2Tran M) . f) | n = f
then ((Mx2Tran M) . f) | n is empty ;
hence ((Mx2Tran M) . f) | n = f by A2; ::_thesis: verum
end;
supposeA3: n > 0 ; ::_thesis: ((Mx2Tran M) . f) | n = f
set TRm = TOP-REAL m;
set V = m -VectSp_over F_Real;
A4: len (1. (F_Real,m)) = m by MATRIX_1:24;
A5: len f = n by CARD_1:def_7;
consider A being FinSequence such that
A6: 1. (F_Real,m) = M ^ A by A1, FINSEQ_1:80;
1. (F_Real,m) = MX2FinS (1. (F_Real,m)) ;
then reconsider A = A as FinSequence of (m -VectSp_over F_Real) by A6, FINSEQ_1:36;
set L = len A;
len M = n by A3, MATRIX13:1;
then n + (len A) = m by A4, A6, FINSEQ_1:22;
then A7: f ^ ((len A) |-> 0) is Element of (TOP-REAL m) by Lm2;
set A1 = FinS2MX A;
A8: (f ^ ((len A) |-> 0)) | n = (f ^ ((len A) |-> 0)) | (dom f) by A5, FINSEQ_1:def_3
.= f by FINSEQ_1:21 ;
(Mx2Tran (M ^ (FinS2MX A))) . (f ^ ((len A) |-> 0)) = (Mx2Tran (1. (F_Real,m))) . (f ^ ((len A) |-> 0)) by A3, A4, A6, MATRIX13:1
.= (id (TOP-REAL m)) . (f ^ ((len A) |-> 0)) by Th33
.= f ^ ((len A) |-> 0) by A7, FUNCT_1:18 ;
hence ((Mx2Tran M) . f) | n = f by A8, Th35; ::_thesis: verum
end;
end;
end;
begin
theorem Th39: :: MATRTOP1:39
for m, n being Nat
for M being Matrix of n,m,F_Real holds
( Mx2Tran M is one-to-one iff the_rank_of M = n )
proof
let m, n be Nat; ::_thesis: for M being Matrix of n,m,F_Real holds
( Mx2Tran M is one-to-one iff the_rank_of M = n )
let M be Matrix of n,m,F_Real; ::_thesis: ( Mx2Tran M is one-to-one iff the_rank_of M = n )
set MM = Mx2Tran M;
percases ( ( n = 0 iff m = 0 ) or ( n = 0 & m <> 0 ) or ( n <> 0 & m = 0 ) ) ;
supposeA1: ( n = 0 iff m = 0 ) ; ::_thesis: ( Mx2Tran M is one-to-one iff the_rank_of M = n )
set nV = n -VectSp_over F_Real;
set mV = m -VectSp_over F_Real;
reconsider Bn = MX2FinS (1. (F_Real,n)) as OrdBasis of n -VectSp_over F_Real by MATRLIN2:45;
reconsider Bm = MX2FinS (1. (F_Real,m)) as OrdBasis of m -VectSp_over F_Real by MATRLIN2:45;
A2: len Bn = n by Th19;
then reconsider M1 = M as Matrix of len Bn, len Bm,F_Real by Th19;
A3: len M1 = n by A1, MATRIX13:1;
A4: len Bm = m by Th19;
set T = Mx2Tran (M1,Bn,Bm);
A5: ( Mx2Tran (M1,Bn,Bm) is one-to-one iff ker (Mx2Tran (M1,Bn,Bm)) = (0). (n -VectSp_over F_Real) ) by MATRLIN2:43;
A6: width M1 = m by A1, MATRIX13:1;
percases ( m = 0 or m > 0 ) ;
supposeA7: m = 0 ; ::_thesis: ( Mx2Tran M is one-to-one iff the_rank_of M = n )
A8: the carrier of (TOP-REAL 0) = {(0. (TOP-REAL 0))} by EUCLID:22, EUCLID:77;
then rng (Mx2Tran M) c= {(0. (TOP-REAL 0))} by A7, RELAT_1:def_19;
then rng (Mx2Tran M) = {(0. (TOP-REAL 0))} by ZFMISC_1:33;
then ( card {(0. (TOP-REAL 0))} = card {(0. (TOP-REAL 0))} & Mx2Tran M is onto ) by A7, A8, FUNCT_2:def_3;
hence ( Mx2Tran M is one-to-one iff the_rank_of M = n ) by A1, A3, A7, A8, MATRIX13:74, STIRL2_1:60; ::_thesis: verum
end;
supposeA9: m > 0 ; ::_thesis: ( Mx2Tran M is one-to-one iff the_rank_of M = n )
then reconsider SS = Space_of_Solutions_of (M1 @) as Subspace of n -VectSp_over F_Real by A3, A6, MATRIX_2:10;
A10: width (M1 @) = n by A3, A6, A9, MATRIX_2:10;
hereby ::_thesis: ( the_rank_of M = n implies Mx2Tran M is one-to-one )
assume A11: Mx2Tran M is one-to-one ; ::_thesis: the_rank_of M = n
[#] SS c= {(0. (n -VectSp_over F_Real))}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [#] SS or x in {(0. (n -VectSp_over F_Real))} )
assume A12: x in [#] SS ; ::_thesis: x in {(0. (n -VectSp_over F_Real))}
then reconsider v = x as Vector of (n -VectSp_over F_Real) by VECTSP_4:10;
v = v |-- Bn by A2, MATRLIN2:46;
then v |-- Bn in SS by A12, STRUCT_0:def_5;
then v in ker (Mx2Tran (M1,Bn,Bm)) by A1, A2, A4, A9, MATRLIN2:41;
then v = 0. (n -VectSp_over F_Real) by A5, A11, Th20, VECTSP_4:35;
hence x in {(0. (n -VectSp_over F_Real))} by TARSKI:def_1; ::_thesis: verum
end;
then [#] SS = {(0. (n -VectSp_over F_Real))} by ZFMISC_1:33;
then SS = (0). (n -VectSp_over F_Real) by VECTSP_4:def_3;
then dim SS = 0 by RANKNULL:16;
then 0 = n - (the_rank_of (M1 @)) by A1, A9, A10, MATRIX15:68;
hence the_rank_of M = n by MATRIX13:84; ::_thesis: verum
end;
A13: the_rank_of (M1 @) = the_rank_of M by MATRIX13:84;
assume the_rank_of M = n ; ::_thesis: Mx2Tran M is one-to-one
then dim SS = n - n by A1, A9, A10, A13, MATRIX15:68;
then A14: SS is trivial by MATRLIN2:42;
[#] (ker (Mx2Tran (M1,Bn,Bm))) c= {(0. (n -VectSp_over F_Real))}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [#] (ker (Mx2Tran (M1,Bn,Bm))) or x in {(0. (n -VectSp_over F_Real))} )
assume A15: x in [#] (ker (Mx2Tran (M1,Bn,Bm))) ; ::_thesis: x in {(0. (n -VectSp_over F_Real))}
then reconsider v = x as Vector of (n -VectSp_over F_Real) by VECTSP_4:10;
v in ker (Mx2Tran (M1,Bn,Bm)) by A15, STRUCT_0:def_5;
then v |-- Bn in SS by A1, A2, A4, A9, MATRLIN2:41;
then v in SS by A2, MATRLIN2:46;
then v in the carrier of SS by STRUCT_0:def_5;
then v = 0. SS by A14, STRUCT_0:def_18;
then v = 0. (n -VectSp_over F_Real) by VECTSP_4:11;
hence x in {(0. (n -VectSp_over F_Real))} by TARSKI:def_1; ::_thesis: verum
end;
then [#] (ker (Mx2Tran (M1,Bn,Bm))) = {(0. (n -VectSp_over F_Real))} by ZFMISC_1:33;
hence Mx2Tran M is one-to-one by A5, Th20, VECTSP_4:def_3; ::_thesis: verum
end;
end;
end;
supposeA16: ( n = 0 & m <> 0 ) ; ::_thesis: ( Mx2Tran M is one-to-one iff the_rank_of M = n )
A17: now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_(Mx2Tran_M)_&_x2_in_dom_(Mx2Tran_M)_&_(Mx2Tran_M)_._x1_=_(Mx2Tran_M)_._x2_holds_
x1_=_x2
let x1, x2 be set ; ::_thesis: ( x1 in dom (Mx2Tran M) & x2 in dom (Mx2Tran M) & (Mx2Tran M) . x1 = (Mx2Tran M) . x2 implies x1 = x2 )
assume A18: ( x1 in dom (Mx2Tran M) & x2 in dom (Mx2Tran M) & (Mx2Tran M) . x1 = (Mx2Tran M) . x2 ) ; ::_thesis: x1 = x2
A19: dom (Mx2Tran M) = [#] (TOP-REAL 0) by A16, FUNCT_2:def_1
.= {(0. (TOP-REAL 0))} by EUCLID:22, EUCLID:77 ;
hence x1 = 0. (TOP-REAL 0) by A18, TARSKI:def_1
.= x2 by A18, A19, TARSKI:def_1 ;
::_thesis: verum
end;
len M = n by MATRIX_1:def_2;
hence ( Mx2Tran M is one-to-one iff the_rank_of M = n ) by A17, A16, FUNCT_1:def_4, MATRIX13:74; ::_thesis: verum
end;
supposeA20: ( n <> 0 & m = 0 ) ; ::_thesis: ( Mx2Tran M is one-to-one iff the_rank_of M = n )
reconsider x1 = n |-> 1 as Point of (TOP-REAL n) by Lm2;
reconsider x2 = n |-> 2 as Point of (TOP-REAL n) by Lm2;
A21: dom (Mx2Tran M) = [#] (TOP-REAL n) by FUNCT_2:def_1;
A22: (Mx2Tran M) . x1 = 0. (TOP-REAL 0) by A20
.= (Mx2Tran M) . x2 by A20 ;
A23: x1 <> x2
proof
assume A24: x1 = x2 ; ::_thesis: contradiction
A25: x1 = (Seg n) --> 1 by FINSEQ_2:def_2
.= [:(Seg n),{1}:] by FUNCOP_1:def_2 ;
x2 = (Seg n) --> 2 by FINSEQ_2:def_2
.= [:(Seg n),{2}:] by FUNCOP_1:def_2 ;
then {1} = {2} by A24, A25, A20, ZFMISC_1:110;
then 2 in {1} by TARSKI:def_1;
hence contradiction by TARSKI:def_1; ::_thesis: verum
end;
width M = m by A20, MATRIX13:1;
hence ( Mx2Tran M is one-to-one iff the_rank_of M = n ) by A23, A20, A22, A21, FUNCT_1:def_4, MATRIX13:74; ::_thesis: verum
end;
end;
end;
theorem Th40: :: MATRTOP1:40
for n being Nat
for A being Matrix of n,F_Real holds
( Mx2Tran A is one-to-one iff Det A <> 0. F_Real )
proof
let n be Nat; ::_thesis: for A being Matrix of n,F_Real holds
( Mx2Tran A is one-to-one iff Det A <> 0. F_Real )
let A be Matrix of n,F_Real; ::_thesis: ( Mx2Tran A is one-to-one iff Det A <> 0. F_Real )
( Mx2Tran A is one-to-one iff the_rank_of A = n ) by Th39;
hence ( Mx2Tran A is one-to-one iff Det A <> 0. F_Real ) by MATRIX13:83; ::_thesis: verum
end;
theorem Th41: :: MATRTOP1:41
for n, m being Nat
for M being Matrix of n,m,F_Real holds
( Mx2Tran M is onto iff the_rank_of M = m )
proof
let n, m be Nat; ::_thesis: for M being Matrix of n,m,F_Real holds
( Mx2Tran M is onto iff the_rank_of M = m )
let M be Matrix of n,m,F_Real; ::_thesis: ( Mx2Tran M is onto iff the_rank_of M = m )
set MM = Mx2Tran M;
set nV = n -VectSp_over F_Real;
set mV = m -VectSp_over F_Real;
reconsider Bn = MX2FinS (1. (F_Real,n)) as OrdBasis of n -VectSp_over F_Real by MATRLIN2:45;
reconsider Bm = MX2FinS (1. (F_Real,m)) as OrdBasis of m -VectSp_over F_Real by MATRLIN2:45;
A1: [#] (m -VectSp_over F_Real) = REAL m by MATRIX13:102
.= [#] (TOP-REAL m) by EUCLID:22 ;
len Bn = n by Th19;
then reconsider M1 = M as Matrix of len Bn, len Bm,F_Real by Th19;
set T = Mx2Tran (M1,Bn,Bm);
A2: dom (Mx2Tran (M1,Bn,Bm)) = [#] (n -VectSp_over F_Real) by FUNCT_2:def_1;
A3: [#] (im (Mx2Tran (M1,Bn,Bm))) = (Mx2Tran (M1,Bn,Bm)) .: ([#] (n -VectSp_over F_Real)) by RANKNULL:def_2
.= rng (Mx2Tran (M1,Bn,Bm)) by A2, RELAT_1:113 ;
A4: Mx2Tran M = Mx2Tran (M1,Bn,Bm) by Th20;
hereby ::_thesis: ( the_rank_of M = m implies Mx2Tran M is onto )
assume Mx2Tran M is onto ; ::_thesis: the_rank_of M = m
then [#] (im (Mx2Tran (M1,Bn,Bm))) = [#] ((Omega). (m -VectSp_over F_Real)) by A4, A1, A3, FUNCT_2:def_3;
then rank (Mx2Tran (M1,Bn,Bm)) = dim ((Omega). (m -VectSp_over F_Real)) by VECTSP_4:29
.= m by MATRIX13:112 ;
hence the_rank_of M = m by MATRLIN2:49; ::_thesis: verum
end;
A5: dim (m -VectSp_over F_Real) = m by MATRIX13:112;
assume the_rank_of M = m ; ::_thesis: Mx2Tran M is onto
then m = rank (Mx2Tran (M1,Bn,Bm)) by MATRLIN2:49
.= dim (im (Mx2Tran (M1,Bn,Bm))) ;
then (Omega). (im (Mx2Tran (M1,Bn,Bm))) = (Omega). (m -VectSp_over F_Real) by A5, VECTSP_9:28;
hence Mx2Tran M is onto by A4, A1, A3, FUNCT_2:def_3; ::_thesis: verum
end;
theorem Th42: :: MATRTOP1:42
for n being Nat
for A being Matrix of n,F_Real holds
( Mx2Tran A is onto iff Det A <> 0. F_Real )
proof
let n be Nat; ::_thesis: for A being Matrix of n,F_Real holds
( Mx2Tran A is onto iff Det A <> 0. F_Real )
let A be Matrix of n,F_Real; ::_thesis: ( Mx2Tran A is onto iff Det A <> 0. F_Real )
( Mx2Tran A is onto iff the_rank_of A = n ) by Th41;
hence ( Mx2Tran A is onto iff Det A <> 0. F_Real ) by MATRIX13:83; ::_thesis: verum
end;
theorem Th43: :: MATRTOP1:43
for n being Nat
for A, B being Matrix of n,F_Real st Det A <> 0. F_Real holds
( (Mx2Tran A) " = Mx2Tran B iff A ~ = B )
proof
let n be Nat; ::_thesis: for A, B being Matrix of n,F_Real st Det A <> 0. F_Real holds
( (Mx2Tran A) " = Mx2Tran B iff A ~ = B )
A1: ( n = 0 implies n = 0 ) ;
let A, B be Matrix of n,F_Real; ::_thesis: ( Det A <> 0. F_Real implies ( (Mx2Tran A) " = Mx2Tran B iff A ~ = B ) )
assume A2: Det A <> 0. F_Real ; ::_thesis: ( (Mx2Tran A) " = Mx2Tran B iff A ~ = B )
A3: A is invertible by A2, LAPLACE:34;
set MA = Mx2Tran A;
set MB = Mx2Tran B;
A4: width B = n by MATRIX_1:24;
reconsider ma = Mx2Tran A, mb = Mx2Tran B as Function ;
A5: ( width A = n & len A = n ) by MATRIX_1:24;
A6: Mx2Tran A is one-to-one by A2, Th40;
hereby ::_thesis: ( A ~ = B implies (Mx2Tran A) " = Mx2Tran B )
assume (Mx2Tran A) " = Mx2Tran B ; ::_thesis: A ~ = B
then A7: mb * ma = id (dom ma) by A6, FUNCT_1:39
.= id (TOP-REAL n) by FUNCT_2:def_1
.= Mx2Tran (1. (F_Real,n)) by Th33 ;
(Mx2Tran B) * (Mx2Tran A) = Mx2Tran (A * B) by A5, A4, A1, Th32;
then B is_reverse_of A by A3, A7, Th34, MATRIX_6:38;
hence A ~ = B by A3, MATRIX_6:def_4; ::_thesis: verum
end;
assume A8: A ~ = B ; ::_thesis: (Mx2Tran A) " = Mx2Tran B
Mx2Tran A is onto by A2, Th42;
then A9: ( dom (Mx2Tran B) = [#] (TOP-REAL n) & rng (Mx2Tran A) = [#] (TOP-REAL n) ) by FUNCT_2:def_1, FUNCT_2:def_3;
A10: n in NAT by ORDINAL1:def_12;
(Mx2Tran B) * (Mx2Tran A) = Mx2Tran (A * B) by A5, A4, A1, Th32
.= Mx2Tran (1. (F_Real,n)) by A3, A10, A8, MATRIX14:18
.= id (TOP-REAL n) by Th33
.= id (dom (Mx2Tran A)) by FUNCT_2:def_1 ;
hence (Mx2Tran A) " = Mx2Tran B by A6, A9, FUNCT_1:41; ::_thesis: verum
end;
Lm4: for n, m being Nat
for M being Matrix of n,m,F_Real
for f being b1 -element real-valued FinSequence ex L being b2 -element FinSequence of REAL st
( |.((Mx2Tran M) . f).| <= (Sum L) * |.f.| & ( for i being Nat st i in dom L holds
L . i = |.(@ (Col (M,i))).| ) )
proof
let n, m be Nat; ::_thesis: for M being Matrix of n,m,F_Real
for f being n -element real-valued FinSequence ex L being m -element FinSequence of REAL st
( |.((Mx2Tran M) . f).| <= (Sum L) * |.f.| & ( for i being Nat st i in dom L holds
L . i = |.(@ (Col (M,i))).| ) )
let M be Matrix of n,m,F_Real; ::_thesis: for f being n -element real-valued FinSequence ex L being m -element FinSequence of REAL st
( |.((Mx2Tran M) . f).| <= (Sum L) * |.f.| & ( for i being Nat st i in dom L holds
L . i = |.(@ (Col (M,i))).| ) )
let f be n -element real-valued FinSequence; ::_thesis: ex L being m -element FinSequence of REAL st
( |.((Mx2Tran M) . f).| <= (Sum L) * |.f.| & ( for i being Nat st i in dom L holds
L . i = |.(@ (Col (M,i))).| ) )
set Lf = LineVec2Mx (@ f);
set LfM = (LineVec2Mx (@ f)) * M;
set LM = Line (((LineVec2Mx (@ f)) * M),1);
deffunc H1( Nat) -> Element of REAL = |.(@ (Col (M,$1))).|;
consider L being FinSequence such that
A1: ( len L = m & ( for k being Nat st k in dom L holds
L . k = H1(k) ) ) from FINSEQ_1:sch_2();
rng L c= REAL
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng L or y in REAL )
assume y in rng L ; ::_thesis: y in REAL
then consider x being set such that
A2: x in dom L and
A3: L . x = y by FUNCT_1:def_3;
reconsider x = x as Nat by A2;
L . x = H1(x) by A1, A2;
hence y in REAL by A3; ::_thesis: verum
end;
then L is FinSequence of REAL by FINSEQ_1:def_4;
then reconsider L1 = L as Element of m -tuples_on REAL by A1, FINSEQ_2:92;
take L1 ; ::_thesis: ( |.((Mx2Tran M) . f).| <= (Sum L1) * |.f.| & ( for i being Nat st i in dom L1 holds
L1 . i = |.(@ (Col (M,i))).| ) )
percases ( n <> 0 or n = 0 ) ;
supposeA4: n <> 0 ; ::_thesis: ( |.((Mx2Tran M) . f).| <= (Sum L1) * |.f.| & ( for i being Nat st i in dom L1 holds
L1 . i = |.(@ (Col (M,i))).| ) )
then A5: len M = n by MATRIX13:1;
(Mx2Tran M) . f = Line (((LineVec2Mx (@ f)) * M),1) by A4, Def3;
then A6: len (Line (((LineVec2Mx (@ f)) * M),1)) = m by CARD_1:def_7;
A7: |.((Mx2Tran M) . f).| = sqrt (Sum (sqr (@ (Line (((LineVec2Mx (@ f)) * M),1))))) by A4, Def3;
reconsider LM = Line (((LineVec2Mx (@ f)) * M),1) as Element of m -tuples_on REAL by A6, FINSEQ_2:92;
len (abs LM) = m by CARD_1:def_7;
then reconsider aLM = abs LM as Element of m -tuples_on REAL by FINSEQ_2:92;
A8: len f = n by CARD_1:def_7;
then A9: width (LineVec2Mx (@ f)) = n by MATRIX13:1;
width M = m by A4, MATRIX13:1;
then A10: width ((LineVec2Mx (@ f)) * M) = m by A5, A9, MATRIX_3:def_4;
len (LineVec2Mx (@ f)) = 1 by MATRIX13:1;
then A11: len ((LineVec2Mx (@ f)) * M) = 1 by A5, A9, MATRIX_3:def_4;
now__::_thesis:_for_i_being_Nat_st_i_in_Seg_m_holds_
aLM_._i_<=_(|.f.|_*_L1)_._i
let i be Nat; ::_thesis: ( i in Seg m implies aLM . i <= (|.f.| * L1) . i )
A12: len (Col (M,i)) = n by A5, MATRIX_1:def_8;
then A13: abs |(f,(@ (Col (M,i))))| <= |.f.| * H1(i) by A8, EUCLID_2:15;
assume A14: i in Seg m ; ::_thesis: aLM . i <= (|.f.| * L1) . i
then A15: ( 1 <= i & i <= m ) by FINSEQ_1:1;
then A16: [1,i] in Indices ((LineVec2Mx (@ f)) * M) by A11, A10, MATRIX_1:36;
i in dom L by A1, A15, FINSEQ_3:25;
then A17: L . i = H1(i) by A1;
LM . i = ((LineVec2Mx (@ f)) * M) * (1,i) by A10, A14, MATRIX_1:def_7
.= (Line ((LineVec2Mx (@ f)),1)) "*" (Col (M,i)) by A5, A9, A16, MATRIX_3:def_4
.= Sum (mlt ((@ f),(Col (M,i)))) by MATRIX15:25
.= Sum (mlt (f,(@ (Col (M,i))))) by A8, A12, MATRPROB:35, MATRPROB:36
.= |(f,(@ (Col (M,i))))| by RVSUM_1:def_16 ;
then aLM . i <= |.f.| * H1(i) by A13, VALUED_1:18;
hence aLM . i <= (|.f.| * L1) . i by A17, RVSUM_1:44; ::_thesis: verum
end;
then A18: Sum aLM <= Sum (|.f.| * L1) by RVSUM_1:82;
sqr LM = LM (#) LM by VALUED_1:def_8;
then sqrt (Sum (sqr LM)) <= Sum (sqrt (sqr LM)) by Th5;
then ( Sum (|.f.| * L1) = |.f.| * (Sum L1) & sqrt (Sum (sqr LM)) <= Sum aLM ) by Th4, RVSUM_1:87;
hence ( |.((Mx2Tran M) . f).| <= (Sum L1) * |.f.| & ( for i being Nat st i in dom L1 holds
L1 . i = |.(@ (Col (M,i))).| ) ) by A7, A1, A18, XXREAL_0:2; ::_thesis: verum
end;
supposeA19: n = 0 ; ::_thesis: ( |.((Mx2Tran M) . f).| <= (Sum L1) * |.f.| & ( for i being Nat st i in dom L1 holds
L1 . i = |.(@ (Col (M,i))).| ) )
now__::_thesis:_for_i_being_Nat_st_i_in_dom_L1_holds_
0_<=_L1_._i
let i be Nat; ::_thesis: ( i in dom L1 implies 0 <= L1 . i )
assume i in dom L1 ; ::_thesis: 0 <= L1 . i
then L1 . i = |.(@ (Col (M,i))).| by A1;
hence 0 <= L1 . i ; ::_thesis: verum
end;
then A20: Sum L1 >= 0 by RVSUM_1:84;
|.((Mx2Tran M) . f).| = |.(0. (TOP-REAL m)).| by A19, Def3
.= 0 by EUCLID_2:39 ;
hence ( |.((Mx2Tran M) . f).| <= (Sum L1) * |.f.| & ( for i being Nat st i in dom L1 holds
L1 . i = |.(@ (Col (M,i))).| ) ) by A1, A20; ::_thesis: verum
end;
end;
end;
theorem Th44: :: MATRTOP1:44
for m, n being Nat
for M being Matrix of n,m,F_Real ex L being b1 -element FinSequence of REAL st
( ( for i being Nat st i in dom L holds
L . i = |.(@ (Col (M,i))).| ) & ( for f being b2 -element real-valued FinSequence holds |.((Mx2Tran M) . f).| <= (Sum L) * |.f.| ) )
proof
let m, n be Nat; ::_thesis: for M being Matrix of n,m,F_Real ex L being m -element FinSequence of REAL st
( ( for i being Nat st i in dom L holds
L . i = |.(@ (Col (M,i))).| ) & ( for f being n -element real-valued FinSequence holds |.((Mx2Tran M) . f).| <= (Sum L) * |.f.| ) )
let M be Matrix of n,m,F_Real; ::_thesis: ex L being m -element FinSequence of REAL st
( ( for i being Nat st i in dom L holds
L . i = |.(@ (Col (M,i))).| ) & ( for f being n -element real-valued FinSequence holds |.((Mx2Tran M) . f).| <= (Sum L) * |.f.| ) )
set F = the n -element real-valued FinSequence;
consider L being m -element FinSequence of REAL such that
|.((Mx2Tran M) . the n -element real-valued FinSequence).| <= (Sum L) * |. the n -element real-valued FinSequence.| and
A1: for i being Nat st i in dom L holds
L . i = |.(@ (Col (M,i))).| by Lm4;
take L ; ::_thesis: ( ( for i being Nat st i in dom L holds
L . i = |.(@ (Col (M,i))).| ) & ( for f being n -element real-valued FinSequence holds |.((Mx2Tran M) . f).| <= (Sum L) * |.f.| ) )
thus for i being Nat st i in dom L holds
L . i = |.(@ (Col (M,i))).| by A1; ::_thesis: for f being n -element real-valued FinSequence holds |.((Mx2Tran M) . f).| <= (Sum L) * |.f.|
let f be n -element real-valued FinSequence; ::_thesis: |.((Mx2Tran M) . f).| <= (Sum L) * |.f.|
consider L1 being m -element FinSequence of REAL such that
A2: |.((Mx2Tran M) . f).| <= (Sum L1) * |.f.| and
A3: for i being Nat st i in dom L1 holds
L1 . i = |.(@ (Col (M,i))).| by Lm4;
( len L1 = m & len L = m ) by CARD_1:def_7;
then A4: dom L = dom L1 by FINSEQ_3:29;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_L_holds_
L_._i_=_L1_._i
let i be Nat; ::_thesis: ( i in dom L implies L . i = L1 . i )
assume A5: i in dom L ; ::_thesis: L . i = L1 . i
hence L . i = |.(@ (Col (M,i))).| by A1
.= L1 . i by A3, A4, A5 ;
::_thesis: verum
end;
hence |.((Mx2Tran M) . f).| <= (Sum L) * |.f.| by A2, A4, FINSEQ_1:13; ::_thesis: verum
end;
theorem Th45: :: MATRTOP1:45
for m, n being Nat
for M being Matrix of n,m,F_Real ex L being Real st
( L > 0 & ( for f being b2 -element real-valued FinSequence holds |.((Mx2Tran M) . f).| <= L * |.f.| ) )
proof
let m, n be Nat; ::_thesis: for M being Matrix of n,m,F_Real ex L being Real st
( L > 0 & ( for f being n -element real-valued FinSequence holds |.((Mx2Tran M) . f).| <= L * |.f.| ) )
let M be Matrix of n,m,F_Real; ::_thesis: ex L being Real st
( L > 0 & ( for f being n -element real-valued FinSequence holds |.((Mx2Tran M) . f).| <= L * |.f.| ) )
consider L being m -element FinSequence of REAL such that
A1: for i being Nat st i in dom L holds
L . i = |.(@ (Col (M,i))).| and
A2: for f being n -element real-valued FinSequence holds |.((Mx2Tran M) . f).| <= (Sum L) * |.f.| by Th44;
take S1 = 1 + (Sum L); ::_thesis: ( S1 > 0 & ( for f being n -element real-valued FinSequence holds |.((Mx2Tran M) . f).| <= S1 * |.f.| ) )
now__::_thesis:_for_i_being_Nat_st_i_in_dom_L_holds_
0_<=_L_._i
let i be Nat; ::_thesis: ( i in dom L implies 0 <= L . i )
assume i in dom L ; ::_thesis: 0 <= L . i
then L . i = |.(@ (Col (M,i))).| by A1;
hence 0 <= L . i ; ::_thesis: verum
end;
then Sum L >= 0 by RVSUM_1:84;
hence S1 > 0 ; ::_thesis: for f being n -element real-valued FinSequence holds |.((Mx2Tran M) . f).| <= S1 * |.f.|
let f be n -element real-valued FinSequence; ::_thesis: |.((Mx2Tran M) . f).| <= S1 * |.f.|
Sum L <= S1 by XREAL_1:29;
then A3: (Sum L) * |.f.| <= S1 * |.f.| by XREAL_1:64;
|.((Mx2Tran M) . f).| <= (Sum L) * |.f.| by A2;
hence |.((Mx2Tran M) . f).| <= S1 * |.f.| by A3, XXREAL_0:2; ::_thesis: verum
end;
theorem :: MATRTOP1:46
for m, n being Nat
for M being Matrix of n,m,F_Real st the_rank_of M = n holds
ex L being Real st
( L > 0 & ( for f being b2 -element real-valued FinSequence holds |.f.| <= L * |.((Mx2Tran M) . f).| ) )
proof
let m, n be Nat; ::_thesis: for M being Matrix of n,m,F_Real st the_rank_of M = n holds
ex L being Real st
( L > 0 & ( for f being n -element real-valued FinSequence holds |.f.| <= L * |.((Mx2Tran M) . f).| ) )
let M be Matrix of n,m,F_Real; ::_thesis: ( the_rank_of M = n implies ex L being Real st
( L > 0 & ( for f being n -element real-valued FinSequence holds |.f.| <= L * |.((Mx2Tran M) . f).| ) ) )
assume A1: the_rank_of M = n ; ::_thesis: ex L being Real st
( L > 0 & ( for f being n -element real-valued FinSequence holds |.f.| <= L * |.((Mx2Tran M) . f).| ) )
percases ( n <> 0 or n = 0 ) ;
supposeA2: n <> 0 ; ::_thesis: ex L being Real st
( L > 0 & ( for f being n -element real-valued FinSequence holds |.f.| <= L * |.((Mx2Tran M) . f).| ) )
consider N being Matrix of m -' n,m,F_Real such that
A3: the_rank_of (M ^ N) = m by A1, Th16;
width M = m by A2, MATRIX13:1;
then m - n >= 0 by A1, MATRIX13:74, XREAL_1:48;
then A4: m - n = m -' n by XREAL_0:def_2;
then reconsider MN = M ^ N as Matrix of m,F_Real ;
A5: dom (id (TOP-REAL m)) = [#] (TOP-REAL m) by RELAT_1:45;
set mn = (m -' n) |-> 0;
A6: ( m = 0 iff m = 0 ) ;
sqr ((m -' n) |-> 0) = (m -' n) |-> (0 ^2) by RVSUM_1:56
.= (m -' n) |-> (0* 0) ;
then A7: Sum (sqr ((m -' n) |-> 0)) = (m -' n) * 0 by RVSUM_1:80;
set MN1 = MN ~ ;
consider L being Real such that
A8: L > 0 and
A9: for f being m -element real-valued FinSequence holds |.((Mx2Tran (MN ~)) . f).| <= L * |.f.| by Th45;
take L ; ::_thesis: ( L > 0 & ( for f being n -element real-valued FinSequence holds |.f.| <= L * |.((Mx2Tran M) . f).| ) )
thus L > 0 by A8; ::_thesis: for f being n -element real-valued FinSequence holds |.f.| <= L * |.((Mx2Tran M) . f).|
let f be n -element real-valued FinSequence; ::_thesis: |.f.| <= L * |.((Mx2Tran M) . f).|
set fm = f ^ ((m -' n) |-> 0);
set Mfm = (Mx2Tran MN) . (f ^ ((m -' n) |-> 0));
A10: (Mx2Tran MN) . (f ^ ((m -' n) |-> 0)) = (Mx2Tran M) . f by A4, Th35;
Det MN <> 0. F_Real by A3, MATRIX13:83;
then A11: MN is invertible by LAPLACE:34;
reconsider MN2 = MN ~ as Matrix of width MN,m,F_Real by MATRIX_1:24;
A12: ( width (MN ~) = m & len MN = m ) by MATRIX_1:24;
A13: (Mx2Tran (MN ~)) * (Mx2Tran MN) = (Mx2Tran MN2) * (Mx2Tran MN) by MATRIX_1:24
.= Mx2Tran (MN * MN2) by A6, Th32
.= Mx2Tran (1. (F_Real,m)) by A11, A12, MATRIX14:18
.= id (TOP-REAL m) by Th33 ;
( f = @ (@ f) & (m -' n) |-> 0 = @ (@ ((m -' n) |-> 0)) ) ;
then sqr (f ^ ((m -' n) |-> 0)) = (sqr f) ^ (sqr ((m -' n) |-> 0)) by RVSUM_1:144;
then Sum (sqr (f ^ ((m -' n) |-> 0))) = (Sum (sqr f)) + (Sum (sqr ((m -' n) |-> 0))) by RVSUM_1:75
.= Sum (sqr f) by A7 ;
then A14: |.(f ^ ((m -' n) |-> 0)).| = |.f.| ;
A15: f ^ ((m -' n) |-> 0) is Point of (TOP-REAL m) by A4, Lm2;
then f ^ ((m -' n) |-> 0) = (id (TOP-REAL m)) . (f ^ ((m -' n) |-> 0)) by FUNCT_1:17
.= (Mx2Tran (MN ~)) . ((Mx2Tran MN) . (f ^ ((m -' n) |-> 0))) by A15, A13, A5, FUNCT_1:12 ;
hence |.f.| <= L * |.((Mx2Tran M) . f).| by A9, A10, A14; ::_thesis: verum
end;
supposeA16: n = 0 ; ::_thesis: ex L being Real st
( L > 0 & ( for f being n -element real-valued FinSequence holds |.f.| <= L * |.((Mx2Tran M) . f).| ) )
A17: |.(0* n).| = 0 by EUCLID:7;
take L = 1; ::_thesis: ( L > 0 & ( for f being n -element real-valued FinSequence holds |.f.| <= L * |.((Mx2Tran M) . f).| ) )
thus ( L > 0 & ( for f being n -element real-valued FinSequence holds |.f.| <= L * |.((Mx2Tran M) . f).| ) ) by A16, A17; ::_thesis: verum
end;
end;
end;
theorem Th47: :: MATRTOP1:47
for n, m being Nat
for M being Matrix of n,m,F_Real holds Mx2Tran M is continuous
proof
let n, m be Nat; ::_thesis: for M being Matrix of n,m,F_Real holds Mx2Tran M is continuous
let M be Matrix of n,m,F_Real; ::_thesis: Mx2Tran M is continuous
set Tn = TOP-REAL n;
set Tm = TOP-REAL m;
set TM = Mx2Tran M;
A1: n in NAT by ORDINAL1:def_12;
consider L being Real such that
A2: L > 0 and
A3: for f being n -element real-valued FinSequence holds |.((Mx2Tran M) . f).| <= L * |.f.| by Th45;
let x be Point of (TOP-REAL n); :: according to BORSUK_1:def_1 ::_thesis: for b1 being a_neighborhood of (Mx2Tran M) . x ex b2 being a_neighborhood of x st K782( the carrier of (TOP-REAL n), the carrier of (TOP-REAL m),(Mx2Tran M),b2) c= b1
let U be a_neighborhood of (Mx2Tran M) . x; ::_thesis: ex b1 being a_neighborhood of x st K782( the carrier of (TOP-REAL n), the carrier of (TOP-REAL m),(Mx2Tran M),b1) c= U
reconsider TMx = (Mx2Tran M) . x as Point of (TOP-REAL m) ;
reconsider tmx = TMx as Point of (Euclid m) by EUCLID:67;
reconsider X = x as Point of (Euclid n) by EUCLID:67;
A4: m in NAT by ORDINAL1:def_12;
tmx in Int U by CONNSP_2:def_1;
then consider r being real number such that
A5: r > 0 and
A6: Ball (tmx,r) c= U by GOBOARD6:5;
reconsider B = Ball (X,(r / L)) as Subset of (TOP-REAL n) by EUCLID:67;
r / L > 0 by A5, A2, XREAL_1:139;
then x in Int B by GOBOARD6:5;
then reconsider Bx = B as a_neighborhood of x by CONNSP_2:def_1;
take Bx ; ::_thesis: K782( the carrier of (TOP-REAL n), the carrier of (TOP-REAL m),(Mx2Tran M),Bx) c= U
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in K782( the carrier of (TOP-REAL n), the carrier of (TOP-REAL m),(Mx2Tran M),Bx) or y in U )
assume y in (Mx2Tran M) .: Bx ; ::_thesis: y in U
then consider p being set such that
p in dom (Mx2Tran M) and
A7: p in Bx and
A8: (Mx2Tran M) . p = y by FUNCT_1:def_6;
reconsider p = p as Point of (TOP-REAL n) by A7;
A9: (r / L) * L = r by A2, XCMPLX_1:87;
reconsider TMp = (Mx2Tran M) . p as Point of (TOP-REAL m) ;
reconsider tmp = TMp as Point of (Euclid m) by EUCLID:67;
dist (tmx,tmp) = |.(((Mx2Tran M) . x) - ((Mx2Tran M) . p)).| by A4, SPPOL_1:39
.= |.((Mx2Tran M) . (x - p)).| by Th28 ;
then A10: dist (tmx,tmp) <= L * |.(x - p).| by A3;
reconsider P = p as Point of (Euclid n) by EUCLID:67;
dist (X,P) < r / L by A7, METRIC_1:11;
then A11: (dist (X,P)) * L < (r / L) * L by A2, XREAL_1:68;
dist (X,P) = |.(x - p).| by A1, SPPOL_1:39;
then dist (tmx,tmp) < r by A11, A9, A10, XXREAL_0:2;
then tmp in Ball (tmx,r) by METRIC_1:11;
hence y in U by A6, A8; ::_thesis: verum
end;
registration
let n be Nat;
let K be Field;
cluster Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like tabular invertible for Matrix of n,n, the carrier of K;
existence
ex b1 being Matrix of n,K st b1 is invertible
proof
1. (K,n) is invertible by MATRIX_6:8;
hence ex b1 being Matrix of n,K st b1 is invertible ; ::_thesis: verum
end;
end;
registration
let n be Nat;
let A be invertible Matrix of n,F_Real;
cluster Mx2Tran A -> being_homeomorphism ;
coherence
Mx2Tran A is being_homeomorphism
proof
set T = Mx2Tran A;
A1: ( Mx2Tran A is continuous & Mx2Tran (A ~) is continuous ) by Th47;
A2: Det A <> 0. F_Real by LAPLACE:34;
then A3: (Mx2Tran A) " = Mx2Tran (A ~) by Th43;
A4: ( Mx2Tran A is onto & Mx2Tran A is one-to-one ) by A2, Th40, Th42;
then A5: rng (Mx2Tran A) = [#] (TOP-REAL n) by FUNCT_2:def_3;
( dom (Mx2Tran A) = [#] (TOP-REAL n) & (Mx2Tran A) /" = (Mx2Tran A) " ) by A4, FUNCT_2:def_1, TOPS_2:def_4;
hence Mx2Tran A is being_homeomorphism by A4, A3, A1, A5, TOPS_2:def_5; ::_thesis: verum
end;
end;