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