:: MATRLIN semantic presentation begin definition let D be non empty set ; let k be Nat; let M be Matrix of D; :: original: Del redefine func Del (M,k) -> Matrix of D; coherence Del (M,k) is Matrix of D proof ex n being Nat st for x being set st x in rng (Del (M,k)) holds ex p being FinSequence of D st ( x = p & len p = n ) proof consider n being Nat such that A1: for x being set st x in rng M holds ex p being FinSequence of D st ( x = p & len p = n ) by MATRIX_1:9; take n ; ::_thesis: for x being set st x in rng (Del (M,k)) holds ex p being FinSequence of D st ( x = p & len p = n ) let x be set ; ::_thesis: ( x in rng (Del (M,k)) implies ex p being FinSequence of D st ( x = p & len p = n ) ) assume A2: x in rng (Del (M,k)) ; ::_thesis: ex p being FinSequence of D st ( x = p & len p = n ) Del (M,k) is FinSequence of D * by FINSEQ_3:105; then rng (Del (M,k)) c= D * by FINSEQ_1:def_4; then reconsider p = x as FinSequence of D by A2, FINSEQ_1:def_11; take p ; ::_thesis: ( x = p & len p = n ) rng (Del (M,k)) c= rng M by FINSEQ_3:106; then ex p1 being FinSequence of D st ( x = p1 & len p1 = n ) by A1, A2; hence ( x = p & len p = n ) ; ::_thesis: verum end; hence Del (M,k) is Matrix of D by MATRIX_1:9; ::_thesis: verum end; end; theorem Th1: :: MATRLIN:1 for n being Nat for M being FinSequence st len M = n + 1 holds len (Del (M,(n + 1))) = n proof let n be Nat; ::_thesis: for M being FinSequence st len M = n + 1 holds len (Del (M,(n + 1))) = n let M be FinSequence; ::_thesis: ( len M = n + 1 implies len (Del (M,(n + 1))) = n ) assume A1: len M = n + 1 ; ::_thesis: len (Del (M,(n + 1))) = n then n + 1 in Seg (len M) by FINSEQ_1:4; then n + 1 in dom M by FINSEQ_1:def_3; hence len (Del (M,(n + 1))) = n by A1, FINSEQ_3:109; ::_thesis: verum end; theorem Th2: :: MATRLIN:2 for n, m being Nat for D being non empty set for M being Matrix of n + 1,m,D for M1 being Matrix of D holds ( ( n > 0 implies width M = width (Del (M,(n + 1))) ) & ( M1 = <*(M . (n + 1))*> implies width M = width M1 ) ) proof let n, m be Nat; ::_thesis: for D being non empty set for M being Matrix of n + 1,m,D for M1 being Matrix of D holds ( ( n > 0 implies width M = width (Del (M,(n + 1))) ) & ( M1 = <*(M . (n + 1))*> implies width M = width M1 ) ) let D be non empty set ; ::_thesis: for M being Matrix of n + 1,m,D for M1 being Matrix of D holds ( ( n > 0 implies width M = width (Del (M,(n + 1))) ) & ( M1 = <*(M . (n + 1))*> implies width M = width M1 ) ) let M be Matrix of n + 1,m,D; ::_thesis: for M1 being Matrix of D holds ( ( n > 0 implies width M = width (Del (M,(n + 1))) ) & ( M1 = <*(M . (n + 1))*> implies width M = width M1 ) ) let M1 be Matrix of D; ::_thesis: ( ( n > 0 implies width M = width (Del (M,(n + 1))) ) & ( M1 = <*(M . (n + 1))*> implies width M = width M1 ) ) A1: len M = n + 1 by MATRIX_1:def_2; then n + 1 in Seg (len M) by FINSEQ_1:4; then n + 1 in dom M by FINSEQ_1:def_3; then A2: M . (n + 1) = Line (M,(n + 1)) by MATRIX_2:16; now__::_thesis:_(_n_>_0_implies_width_M_=_width_(Del_(M,(n_+_1)))_) assume A3: n > 0 ; ::_thesis: width M = width (Del (M,(n + 1))) len (Del (M,(n + 1))) = n by A1, Th1; then consider s being FinSequence such that A4: s in rng (Del (M,(n + 1))) and A5: len s = width (Del (M,(n + 1))) by A3, MATRIX_1:def_3; consider n1 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 = n1 ) by MATRIX_1:9; consider s1 being FinSequence such that A7: s1 in rng M and A8: len s1 = width M by A1, MATRIX_1:def_3; A9: ex p2 being FinSequence of D st ( s1 = p2 & len p2 = n1 ) by A7, A6; rng (Del (M,(n + 1))) c= rng M by FINSEQ_3:106; then ex p1 being FinSequence of D st ( s = p1 & len p1 = n1 ) by A4, A6; hence width M = width (Del (M,(n + 1))) by A5, A8, A9; ::_thesis: verum end; hence ( n > 0 implies width M = width (Del (M,(n + 1))) ) ; ::_thesis: ( M1 = <*(M . (n + 1))*> implies width M = width M1 ) assume M1 = <*(M . (n + 1))*> ; ::_thesis: width M = width M1 then reconsider M2 = M1 as Matrix of 1, len (Line (M,(n + 1))),D by A2, MATRIX_1:11; thus width M = len (Line (M,(n + 1))) by MATRIX_1:def_7 .= width M2 by MATRIX_1:23 .= width M1 ; ::_thesis: verum end; theorem Th3: :: MATRLIN:3 for n, m being Nat for D being non empty set for M being Matrix of n + 1,m,D holds Del (M,(n + 1)) is Matrix of n,m,D proof let n, m be Nat; ::_thesis: for D being non empty set for M being Matrix of n + 1,m,D holds Del (M,(n + 1)) is Matrix of n,m,D let D be non empty set ; ::_thesis: for M being Matrix of n + 1,m,D holds Del (M,(n + 1)) is Matrix of n,m,D let M be Matrix of n + 1,m,D; ::_thesis: Del (M,(n + 1)) is Matrix of n,m,D A1: len M = n + 1 by MATRIX_1:def_2; then A2: len (Del (M,(n + 1))) = n by Th1; percases ( n = 0 or n > 0 ) ; supposeA3: n = 0 ; ::_thesis: Del (M,(n + 1)) is Matrix of n,m,D then Del (M,(n + 1)) = {} by A2; hence Del (M,(n + 1)) is Matrix of n,m,D by A3, MATRIX_1:13; ::_thesis: verum end; supposeA4: n > 0 ; ::_thesis: Del (M,(n + 1)) is Matrix of n,m,D width M = m by A1, MATRIX_1:20; then width (Del (M,(n + 1))) = m by A4, Th2; hence Del (M,(n + 1)) is Matrix of n,m,D by A2, A4, MATRIX_1:20; ::_thesis: verum end; end; end; theorem Th4: :: MATRLIN:4 for M being FinSequence st M <> {} holds M = (Del (M,(len M))) ^ <*(M . (len M))*> proof let M be FinSequence; ::_thesis: ( M <> {} implies M = (Del (M,(len M))) ^ <*(M . (len M))*> ) assume M <> {} ; ::_thesis: M = (Del (M,(len M))) ^ <*(M . (len M))*> then consider q being FinSequence, x being set such that A1: M = q ^ <*x*> by FINSEQ_1:46; A2: len M = (len q) + (len <*x*>) by A1, FINSEQ_1:22 .= (len q) + 1 by FINSEQ_1:39 ; then A3: len (Del (M,(len M))) = len q by Th1; A4: dom q = Seg (len q) by FINSEQ_1:def_3; A5: now__::_thesis:_for_i_being_Nat_st_i_in_dom_q_holds_ (Del_(M,(len_M)))_._i_=_q_._i let i be Nat; ::_thesis: ( i in dom q implies (Del (M,(len M))) . i = q . i ) assume A6: i in dom q ; ::_thesis: (Del (M,(len M))) . i = q . i then i <= len q by A4, FINSEQ_1:1; then ( i in NAT & i < len M ) by A2, NAT_1:13, ORDINAL1:def_12; hence (Del (M,(len M))) . i = M . i by FINSEQ_3:110 .= q . i by A1, A6, FINSEQ_1:def_7 ; ::_thesis: verum end; M . (len M) = x by A1, A2, FINSEQ_1:42; hence M = (Del (M,(len M))) ^ <*(M . (len M))*> by A1, A3, A5, FINSEQ_2:9; ::_thesis: verum end; definition let D be non empty set ; let P be FinSequence of D; :: original: <* redefine func<*P*> -> Matrix of 1, len P,D; coherence <*P*> is Matrix of 1, len P,D by MATRIX_1:11; end; begin begin theorem Th5: :: MATRLIN:5 for K being Field for V being VectSp of K for KL1, KL2 being Linear_Combination of V for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Sum KL1 = Sum KL2 holds KL1 = KL2 proof let K be Field; ::_thesis: for V being VectSp of K for KL1, KL2 being Linear_Combination of V for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Sum KL1 = Sum KL2 holds KL1 = KL2 let V be VectSp of K; ::_thesis: for KL1, KL2 being Linear_Combination of V for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Sum KL1 = Sum KL2 holds KL1 = KL2 let KL1, KL2 be Linear_Combination of V; ::_thesis: for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Sum KL1 = Sum KL2 holds KL1 = KL2 let X be Subset of V; ::_thesis: ( X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Sum KL1 = Sum KL2 implies KL1 = KL2 ) assume that A1: X is linearly-independent and A2: ( Carrier KL1 c= X & Carrier KL2 c= X ) and A3: Sum KL1 = Sum KL2 ; ::_thesis: KL1 = KL2 (Sum KL1) - (Sum KL2) = 0. V by A3, VECTSP_1:19; then A4: ( KL1 - KL2 is Linear_Combination of Carrier (KL1 - KL2) & Sum (KL1 - KL2) = 0. V ) by VECTSP_6:7, VECTSP_6:47; A5: Carrier (KL1 - KL2) c= (Carrier KL1) \/ (Carrier KL2) by VECTSP_6:41; (Carrier KL1) \/ (Carrier KL2) c= X by A2, XBOOLE_1:8; then A6: Carrier (KL1 - KL2) is linearly-independent by A1, A5, VECTSP_7:1, XBOOLE_1:1; now__::_thesis:_for_v_being_Vector_of_V_holds_KL1_._v_=_KL2_._v let v be Vector of V; ::_thesis: KL1 . v = KL2 . v not v in Carrier (KL1 - KL2) by A6, A4, VECTSP_7:def_1; then (KL1 - KL2) . v = 0. K by VECTSP_6:2; then (KL1 . v) - (KL2 . v) = 0. K by VECTSP_6:40; hence KL1 . v = KL2 . v by RLVECT_1:21; ::_thesis: verum end; hence KL1 = KL2 by VECTSP_6:def_7; ::_thesis: verum end; theorem Th6: :: MATRLIN:6 for K being Field for V being VectSp of K for KL1, KL2, KL3 being Linear_Combination of V for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Carrier KL3 c= X & Sum KL1 = (Sum KL2) + (Sum KL3) holds KL1 = KL2 + KL3 proof let K be Field; ::_thesis: for V being VectSp of K for KL1, KL2, KL3 being Linear_Combination of V for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Carrier KL3 c= X & Sum KL1 = (Sum KL2) + (Sum KL3) holds KL1 = KL2 + KL3 let V be VectSp of K; ::_thesis: for KL1, KL2, KL3 being Linear_Combination of V for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Carrier KL3 c= X & Sum KL1 = (Sum KL2) + (Sum KL3) holds KL1 = KL2 + KL3 let KL1, KL2, KL3 be Linear_Combination of V; ::_thesis: for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Carrier KL3 c= X & Sum KL1 = (Sum KL2) + (Sum KL3) holds KL1 = KL2 + KL3 let X be Subset of V; ::_thesis: ( X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Carrier KL3 c= X & Sum KL1 = (Sum KL2) + (Sum KL3) implies KL1 = KL2 + KL3 ) assume that A1: ( X is linearly-independent & Carrier KL1 c= X ) and A2: ( Carrier KL2 c= X & Carrier KL3 c= X ) and A3: Sum KL1 = (Sum KL2) + (Sum KL3) ; ::_thesis: KL1 = KL2 + KL3 ( Carrier (KL2 + KL3) c= (Carrier KL2) \/ (Carrier KL3) & (Carrier KL2) \/ (Carrier KL3) c= X ) by A2, VECTSP_6:23, XBOOLE_1:8; then A4: Carrier (KL2 + KL3) c= X by XBOOLE_1:1; Sum KL1 = Sum (KL2 + KL3) by A3, VECTSP_6:44; hence KL1 = KL2 + KL3 by A1, A4, Th5; ::_thesis: verum end; theorem Th7: :: MATRLIN:7 for K being Field for V being VectSp of K for a being Element of K for KL1, KL2 being Linear_Combination of V for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & a <> 0. K & Sum KL1 = a * (Sum KL2) holds KL1 = a * KL2 proof let K be Field; ::_thesis: for V being VectSp of K for a being Element of K for KL1, KL2 being Linear_Combination of V for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & a <> 0. K & Sum KL1 = a * (Sum KL2) holds KL1 = a * KL2 let V be VectSp of K; ::_thesis: for a being Element of K for KL1, KL2 being Linear_Combination of V for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & a <> 0. K & Sum KL1 = a * (Sum KL2) holds KL1 = a * KL2 let a be Element of K; ::_thesis: for KL1, KL2 being Linear_Combination of V for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & a <> 0. K & Sum KL1 = a * (Sum KL2) holds KL1 = a * KL2 let KL1, KL2 be Linear_Combination of V; ::_thesis: for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & a <> 0. K & Sum KL1 = a * (Sum KL2) holds KL1 = a * KL2 let X be Subset of V; ::_thesis: ( X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & a <> 0. K & Sum KL1 = a * (Sum KL2) implies KL1 = a * KL2 ) assume that A1: ( X is linearly-independent & Carrier KL1 c= X ) and A2: ( Carrier KL2 c= X & a <> 0. K & Sum KL1 = a * (Sum KL2) ) ; ::_thesis: KL1 = a * KL2 ( Carrier (a * KL2) c= X & Sum KL1 = Sum (a * KL2) ) by A2, VECTSP_6:29, VECTSP_6:45; hence KL1 = a * KL2 by A1, Th5; ::_thesis: verum end; theorem Th8: :: MATRLIN:8 for K being Field for V being VectSp of K for W being Element of V for b2 being Basis of V ex KL being Linear_Combination of V st ( W = Sum KL & Carrier KL c= b2 ) proof let K be Field; ::_thesis: for V being VectSp of K for W being Element of V for b2 being Basis of V ex KL being Linear_Combination of V st ( W = Sum KL & Carrier KL c= b2 ) let V be VectSp of K; ::_thesis: for W being Element of V for b2 being Basis of V ex KL being Linear_Combination of V st ( W = Sum KL & Carrier KL c= b2 ) let W be Element of V; ::_thesis: for b2 being Basis of V ex KL being Linear_Combination of V st ( W = Sum KL & Carrier KL c= b2 ) let b2 be Basis of V; ::_thesis: ex KL being Linear_Combination of V st ( W = Sum KL & Carrier KL c= b2 ) W in VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) by RLVECT_1:1; then W in Lin b2 by VECTSP_7:def_3; then consider KL1 being Linear_Combination of b2 such that A1: W = Sum KL1 by VECTSP_7:7; take KL = KL1; ::_thesis: ( W = Sum KL & Carrier KL c= b2 ) thus W = Sum KL by A1; ::_thesis: Carrier KL c= b2 thus Carrier KL c= b2 by VECTSP_6:def_4; ::_thesis: verum end; definition let K be Field; let V be VectSp of K; attrV is finite-dimensional means :Def1: :: MATRLIN:def 1 ex A being finite Subset of V st A is Basis of V; end; :: deftheorem Def1 defines finite-dimensional MATRLIN:def_1_:_ for K being Field for V being VectSp of K holds ( V is finite-dimensional iff ex A being finite Subset of V st A is Basis of V ); registration let K be Field; cluster non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed finite-dimensional for VectSpStr over K; existence ex b1 being VectSp of K st ( b1 is strict & b1 is finite-dimensional ) proof set V = the VectSp of K; take (0). the VectSp of K ; ::_thesis: ( (0). the VectSp of K is strict & (0). the VectSp of K is finite-dimensional ) thus (0). the VectSp of K is strict ; ::_thesis: (0). the VectSp of K is finite-dimensional take A = {} the carrier of ((0). the VectSp of K); :: according to MATRLIN:def_1 ::_thesis: A is Basis of (0). the VectSp of K Lin A = (0). ((0). the VectSp of K) by VECTSP_7:9; then Lin A = VectSpStr(# the carrier of ((0). the VectSp of K), the addF of ((0). the VectSp of K), the ZeroF of ((0). the VectSp of K), the lmult of ((0). the VectSp of K) #) by VECTSP_4:36; hence A is Basis of (0). the VectSp of K by VECTSP_7:def_3; ::_thesis: verum end; end; definition let K be Field; let V be finite-dimensional VectSp of K; mode OrdBasis of V -> FinSequence of V means :Def2: :: MATRLIN:def 2 ( it is one-to-one & rng it is Basis of V ); existence ex b1 being FinSequence of V st ( b1 is one-to-one & rng b1 is Basis of V ) proof consider A being finite Subset of V such that A1: A is Basis of V by Def1; consider p being FinSequence such that A2: rng p = A and A3: p is one-to-one by FINSEQ_4:58; reconsider p = p as FinSequence of V by A2, FINSEQ_1:def_4; take f = p; ::_thesis: ( f is one-to-one & rng f is Basis of V ) thus f is one-to-one by A3; ::_thesis: rng f is Basis of V thus rng f is Basis of V by A1, A2; ::_thesis: verum end; end; :: deftheorem Def2 defines OrdBasis MATRLIN:def_2_:_ for K being Field for V being finite-dimensional VectSp of K for b3 being FinSequence of V holds ( b3 is OrdBasis of V iff ( b3 is one-to-one & rng b3 is Basis of V ) ); definition let K be non empty doubleLoopStr ; let V1, V2 be non empty VectSpStr over K; let f1, f2 be Function of V1,V2; funcf1 + f2 -> Function of V1,V2 means :Def3: :: MATRLIN:def 3 for v being Element of V1 holds it . v = (f1 . v) + (f2 . v); existence ex b1 being Function of V1,V2 st for v being Element of V1 holds b1 . v = (f1 . v) + (f2 . v) proof deffunc H1( Element of V1) -> Element of the carrier of V2 = (f1 . $1) + (f2 . $1); consider F being Function of V1,V2 such that A1: for v being Element of V1 holds F . v = H1(v) from FUNCT_2:sch_4(); reconsider F = F as Function of V1,V2 ; take F ; ::_thesis: for v being Element of V1 holds F . v = (f1 . v) + (f2 . v) thus for v being Element of V1 holds F . v = (f1 . v) + (f2 . v) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Function of V1,V2 st ( for v being Element of V1 holds b1 . v = (f1 . v) + (f2 . v) ) & ( for v being Element of V1 holds b2 . v = (f1 . v) + (f2 . v) ) holds b1 = b2 proof let F, G be Function of V1,V2; ::_thesis: ( ( for v being Element of V1 holds F . v = (f1 . v) + (f2 . v) ) & ( for v being Element of V1 holds G . v = (f1 . v) + (f2 . v) ) implies F = G ) assume that A2: for v being Element of V1 holds F . v = (f1 . v) + (f2 . v) and A3: for v being Element of V1 holds G . v = (f1 . v) + (f2 . v) ; ::_thesis: F = G now__::_thesis:_for_v_being_Element_of_V1_holds_F_._v_=_G_._v let v be Element of V1; ::_thesis: F . v = G . v thus F . v = (f1 . v) + (f2 . v) by A2 .= G . v by A3 ; ::_thesis: verum end; hence F = G by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def3 defines + MATRLIN:def_3_:_ for K being non empty doubleLoopStr for V1, V2 being non empty VectSpStr over K for f1, f2, b6 being Function of V1,V2 holds ( b6 = f1 + f2 iff for v being Element of V1 holds b6 . v = (f1 . v) + (f2 . v) ); definition let K be non empty doubleLoopStr ; let V1, V2 be non empty VectSpStr over K; let f be Function of V1,V2; let a be Element of K; funca * f -> Function of V1,V2 means :Def4: :: MATRLIN:def 4 for v being Element of V1 holds it . v = a * (f . v); existence ex b1 being Function of V1,V2 st for v being Element of V1 holds b1 . v = a * (f . v) proof deffunc H1( Element of V1) -> Element of the carrier of V2 = a * (f . $1); consider F being Function of V1,V2 such that A1: for v being Element of V1 holds F . v = H1(v) from FUNCT_2:sch_4(); reconsider F = F as Function of V1,V2 ; take F ; ::_thesis: for v being Element of V1 holds F . v = a * (f . v) thus for v being Element of V1 holds F . v = a * (f . v) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Function of V1,V2 st ( for v being Element of V1 holds b1 . v = a * (f . v) ) & ( for v being Element of V1 holds b2 . v = a * (f . v) ) holds b1 = b2 proof let F, G be Function of V1,V2; ::_thesis: ( ( for v being Element of V1 holds F . v = a * (f . v) ) & ( for v being Element of V1 holds G . v = a * (f . v) ) implies F = G ) assume that A2: for v being Element of V1 holds F . v = a * (f . v) and A3: for v being Element of V1 holds G . v = a * (f . v) ; ::_thesis: F = G now__::_thesis:_for_v_being_Element_of_V1_holds_F_._v_=_G_._v let v be Element of V1; ::_thesis: F . v = G . v thus F . v = a * (f . v) by A2 .= G . v by A3 ; ::_thesis: verum end; hence F = G by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def4 defines * MATRLIN:def_4_:_ for K being non empty doubleLoopStr for V1, V2 being non empty VectSpStr over K for f being Function of V1,V2 for a being Element of K for b6 being Function of V1,V2 holds ( b6 = a * f iff for v being Element of V1 holds b6 . v = a * (f . v) ); theorem Th9: :: MATRLIN:9 for K being Field for V1 being finite-dimensional VectSp of K for a being Element of V1 for F being FinSequence of V1 for G being FinSequence of K st len F = len G & ( for k being Nat for v being Element of K st k in dom F & v = G . k holds F . k = v * a ) holds Sum F = (Sum G) * a proof let K be Field; ::_thesis: for V1 being finite-dimensional VectSp of K for a being Element of V1 for F being FinSequence of V1 for G being FinSequence of K st len F = len G & ( for k being Nat for v being Element of K st k in dom F & v = G . k holds F . k = v * a ) holds Sum F = (Sum G) * a let V1 be finite-dimensional VectSp of K; ::_thesis: for a being Element of V1 for F being FinSequence of V1 for G being FinSequence of K st len F = len G & ( for k being Nat for v being Element of K st k in dom F & v = G . k holds F . k = v * a ) holds Sum F = (Sum G) * a let a be Element of V1; ::_thesis: for F being FinSequence of V1 for G being FinSequence of K st len F = len G & ( for k being Nat for v being Element of K st k in dom F & v = G . k holds F . k = v * a ) holds Sum F = (Sum G) * a let F be FinSequence of V1; ::_thesis: for G being FinSequence of K st len F = len G & ( for k being Nat for v being Element of K st k in dom F & v = G . k holds F . k = v * a ) holds Sum F = (Sum G) * a let G be FinSequence of K; ::_thesis: ( len F = len G & ( for k being Nat for v being Element of K st k in dom F & v = G . k holds F . k = v * a ) implies Sum F = (Sum G) * a ) defpred S1[ Nat] means for H being FinSequence of V1 for I being FinSequence of K st len H = len I & len H = $1 & ( for k being Nat for v being Element of K st k in dom H & v = I . k holds H . k = v * a ) holds Sum H = (Sum I) * a; 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: for H being FinSequence of V1 for I being FinSequence of K st len H = len I & len H = n & ( for k being Nat for v being Element of K st k in dom H & v = I . k holds H . k = v * a ) holds Sum H = (Sum I) * a ; ::_thesis: S1[n + 1] let H be FinSequence of V1; ::_thesis: for I being FinSequence of K st len H = len I & len H = n + 1 & ( for k being Nat for v being Element of K st k in dom H & v = I . k holds H . k = v * a ) holds Sum H = (Sum I) * a let I be FinSequence of K; ::_thesis: ( len H = len I & len H = n + 1 & ( for k being Nat for v being Element of K st k in dom H & v = I . k holds H . k = v * a ) implies Sum H = (Sum I) * a ) assume that A3: len H = len I and A4: len H = n + 1 and A5: for k being Nat for v being Element of K st k in dom H & v = I . k holds H . k = v * a ; ::_thesis: Sum H = (Sum I) * a reconsider q = I | (Seg n) as FinSequence of K by FINSEQ_1:18; reconsider p = H | (Seg n) as FinSequence of V1 by FINSEQ_1:18; A6: n <= n + 1 by NAT_1:12; then A7: len p = n by A4, FINSEQ_1:17; A8: dom p = Seg n by A4, A6, FINSEQ_1:17; A9: len q = n by A3, A4, A6, FINSEQ_1:17; A10: dom q = Seg n by A3, A4, A6, FINSEQ_1:17; A11: now__::_thesis:_for_k_being_Nat for_v_being_Element_of_K_st_k_in_dom_p_&_v_=_q_._k_holds_ p_._k_=_v_*_a len p <= len H by A4, A6, FINSEQ_1:17; then A12: dom p c= dom H by FINSEQ_3:30; let k be Nat; ::_thesis: for v being Element of K st k in dom p & v = q . k holds p . k = v * a let v be Element of K; ::_thesis: ( k in dom p & v = q . k implies p . k = v * a ) assume that A13: k in dom p and A14: v = q . k ; ::_thesis: p . k = v * a I . k = q . k by A8, A10, A13, FUNCT_1:47; then H . k = v * a by A5, A13, A14, A12; hence p . k = v * a by A13, FUNCT_1:47; ::_thesis: verum end; reconsider n = n as Element of NAT by ORDINAL1:def_12; n + 1 in Seg (n + 1) by FINSEQ_1:4; then A15: n + 1 in dom H by A4, FINSEQ_1:def_3; then reconsider v1 = H . (n + 1) as Element of V1 by FINSEQ_2:11; dom H = dom I by A3, FINSEQ_3:29; then reconsider v2 = I . (n + 1) as Element of K by A15, FINSEQ_2:11; A16: v1 = v2 * a by A5, A15; thus Sum H = (Sum p) + v1 by A4, A7, A8, RLVECT_1:38 .= ((Sum q) * a) + (v2 * a) by A2, A7, A9, A11, A16 .= ((Sum q) + v2) * a by VECTSP_1:def_15 .= (Sum I) * a by A3, A4, A9, A10, RLVECT_1:38 ; ::_thesis: verum end; A17: S1[ 0 ] proof let H be FinSequence of V1; ::_thesis: for I being FinSequence of K st len H = len I & len H = 0 & ( for k being Nat for v being Element of K st k in dom H & v = I . k holds H . k = v * a ) holds Sum H = (Sum I) * a let I be FinSequence of K; ::_thesis: ( len H = len I & len H = 0 & ( for k being Nat for v being Element of K st k in dom H & v = I . k holds H . k = v * a ) implies Sum H = (Sum I) * a ) assume that A18: len H = len I and A19: len H = 0 and for k being Nat for v being Element of K st k in dom H & v = I . k holds H . k = v * a ; ::_thesis: Sum H = (Sum I) * a H = <*> the carrier of V1 by A19; then A20: Sum H = 0. V1 by RLVECT_1:43; I = <*> the carrier of K by A18, A19; then Sum I = 0. K by RLVECT_1:43; hence Sum H = (Sum I) * a by A20, VECTSP_1:14; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A17, A1); hence ( len F = len G & ( for k being Nat for v being Element of K st k in dom F & v = G . k holds F . k = v * a ) implies Sum F = (Sum G) * a ) ; ::_thesis: verum end; theorem Th10: :: MATRLIN:10 for K being Field for V1 being finite-dimensional VectSp of K for a being Element of V1 for F being FinSequence of K for G being FinSequence of V1 st len F = len G & ( for k being Nat st k in dom F holds G . k = (F /. k) * a ) holds Sum G = (Sum F) * a proof let K be Field; ::_thesis: for V1 being finite-dimensional VectSp of K for a being Element of V1 for F being FinSequence of K for G being FinSequence of V1 st len F = len G & ( for k being Nat st k in dom F holds G . k = (F /. k) * a ) holds Sum G = (Sum F) * a let V1 be finite-dimensional VectSp of K; ::_thesis: for a being Element of V1 for F being FinSequence of K for G being FinSequence of V1 st len F = len G & ( for k being Nat st k in dom F holds G . k = (F /. k) * a ) holds Sum G = (Sum F) * a let a be Element of V1; ::_thesis: for F being FinSequence of K for G being FinSequence of V1 st len F = len G & ( for k being Nat st k in dom F holds G . k = (F /. k) * a ) holds Sum G = (Sum F) * a let F be FinSequence of K; ::_thesis: for G being FinSequence of V1 st len F = len G & ( for k being Nat st k in dom F holds G . k = (F /. k) * a ) holds Sum G = (Sum F) * a let G be FinSequence of V1; ::_thesis: ( len F = len G & ( for k being Nat st k in dom F holds G . k = (F /. k) * a ) implies Sum G = (Sum F) * a ) assume that A1: len F = len G and A2: for k being Nat st k in dom F holds G . k = (F /. k) * a ; ::_thesis: Sum G = (Sum F) * a now__::_thesis:_for_k_being_Nat for_v_being_Element_of_K_st_k_in_dom_G_&_v_=_F_._k_holds_ G_._k_=_v_*_a let k be Nat; ::_thesis: for v being Element of K st k in dom G & v = F . k holds G . k = v * a let v be Element of K; ::_thesis: ( k in dom G & v = F . k implies G . k = v * a ) assume that A3: k in dom G and A4: v = F . k ; ::_thesis: G . k = v * a A5: k in dom F by A1, A3, FINSEQ_3:29; then v = F /. k by A4, PARTFUN1:def_6; hence G . k = v * a by A2, A5; ::_thesis: verum end; hence Sum G = (Sum F) * a by A1, Th9; ::_thesis: verum end; theorem Th11: :: MATRLIN:11 for V1 being non empty right_complementable add-associative right_zeroed addLoopStr for F being FinSequence of V1 st ( for k being Nat st k in dom F holds F /. k = 0. V1 ) holds Sum F = 0. V1 proof let V1 be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for F being FinSequence of V1 st ( for k being Nat st k in dom F holds F /. k = 0. V1 ) holds Sum F = 0. V1 let F be FinSequence of V1; ::_thesis: ( ( for k being Nat st k in dom F holds F /. k = 0. V1 ) implies Sum F = 0. V1 ) assume A1: for k being Nat st k in dom F holds F /. k = 0. V1 ; ::_thesis: Sum F = 0. V1 defpred S1[ FinSequence of V1] means ( ( for k being Nat st k in dom $1 holds $1 /. k = 0. V1 ) implies Sum $1 = 0. V1 ); A2: for p being FinSequence of V1 for x being Element of V1 st S1[p] holds S1[p ^ <*x*>] proof let p be FinSequence of V1; ::_thesis: for x being Element of V1 st S1[p] holds S1[p ^ <*x*>] let x be Element of V1; ::_thesis: ( S1[p] implies S1[p ^ <*x*>] ) assume A3: ( ( for k being Nat st k in dom p holds p /. k = 0. V1 ) implies Sum p = 0. V1 ) ; ::_thesis: S1[p ^ <*x*>] A4: (len p) + 1 in Seg ((len p) + 1) by FINSEQ_1:4; assume A5: for k being Nat st k in dom (p ^ <*x*>) holds (p ^ <*x*>) /. k = 0. V1 ; ::_thesis: Sum (p ^ <*x*>) = 0. V1 A6: for k being Nat st k in dom p holds p /. k = 0. V1 proof A7: dom p c= dom (p ^ <*x*>) by FINSEQ_1:26; let k be Nat; ::_thesis: ( k in dom p implies p /. k = 0. V1 ) assume A8: k in dom p ; ::_thesis: p /. k = 0. V1 reconsider k1 = k as Element of NAT by ORDINAL1:def_12; thus p /. k = p . k by A8, PARTFUN1:def_6 .= (p ^ <*x*>) . k1 by A8, FINSEQ_1:def_7 .= (p ^ <*x*>) /. k by A8, A7, PARTFUN1:def_6 .= 0. V1 by A5, A8, A7 ; ::_thesis: verum end; len (p ^ <*x*>) = (len p) + (len <*x*>) by FINSEQ_1:22 .= (len p) + 1 by FINSEQ_1:39 ; then A9: (len p) + 1 in dom (p ^ <*x*>) by A4, FINSEQ_1:def_3; A10: x = (p ^ <*x*>) . ((len p) + 1) by FINSEQ_1:42; thus Sum (p ^ <*x*>) = (Sum p) + (Sum <*x*>) by RLVECT_1:41 .= (Sum p) + x by RLVECT_1:44 .= (Sum p) + ((p ^ <*x*>) /. ((len p) + 1)) by A9, A10, PARTFUN1:def_6 .= (0. V1) + (0. V1) by A3, A5, A6, A9 .= 0. V1 by RLVECT_1:def_4 ; ::_thesis: verum end; A11: S1[ <*> the carrier of V1] by RLVECT_1:43; for p being FinSequence of V1 holds S1[p] from FINSEQ_2:sch_2(A11, A2); hence Sum F = 0. V1 by A1; ::_thesis: verum end; definition let K be Field; let V1 be finite-dimensional VectSp of K; let p1 be FinSequence of K; let p2 be FinSequence of V1; func lmlt (p1,p2) -> FinSequence of V1 equals :: MATRLIN:def 5 the lmult of V1 .: (p1,p2); coherence the lmult of V1 .: (p1,p2) is FinSequence of V1 ; end; :: deftheorem defines lmlt MATRLIN:def_5_:_ for K being Field for V1 being finite-dimensional VectSp of K for p1 being FinSequence of K for p2 being FinSequence of V1 holds lmlt (p1,p2) = the lmult of V1 .: (p1,p2); theorem Th12: :: MATRLIN:12 for K being Field for V1 being finite-dimensional VectSp of K for p2 being FinSequence of V1 for p1 being FinSequence of K st dom p1 = dom p2 holds dom (lmlt (p1,p2)) = dom p1 proof let K be Field; ::_thesis: for V1 being finite-dimensional VectSp of K for p2 being FinSequence of V1 for p1 being FinSequence of K st dom p1 = dom p2 holds dom (lmlt (p1,p2)) = dom p1 let V1 be finite-dimensional VectSp of K; ::_thesis: for p2 being FinSequence of V1 for p1 being FinSequence of K st dom p1 = dom p2 holds dom (lmlt (p1,p2)) = dom p1 let p2 be FinSequence of V1; ::_thesis: for p1 being FinSequence of K st dom p1 = dom p2 holds dom (lmlt (p1,p2)) = dom p1 let p1 be FinSequence of K; ::_thesis: ( dom p1 = dom p2 implies dom (lmlt (p1,p2)) = dom p1 ) assume A1: dom p1 = dom p2 ; ::_thesis: dom (lmlt (p1,p2)) = dom p1 ( rng p1 c= the carrier of K & rng p2 c= the carrier of V1 ) by FINSEQ_1:def_4; then A2: [:(rng p1),(rng p2):] c= [: the carrier of K, the carrier of V1:] by ZFMISC_1:96; ( rng <:p1,p2:> c= [:(rng p1),(rng p2):] & [: the carrier of K, the carrier of V1:] = dom the lmult of V1 ) by FUNCT_2:def_1, FUNCT_3:51; hence dom (lmlt (p1,p2)) = dom <:p1,p2:> by A2, RELAT_1:27, XBOOLE_1:1 .= (dom p1) /\ (dom p2) by FUNCT_3:def_7 .= dom p1 by A1 ; ::_thesis: verum end; definition let V1 be non empty addLoopStr ; let M be FinSequence of the carrier of V1 * ; func Sum M -> FinSequence of V1 means :Def6: :: MATRLIN:def 6 ( len it = len M & ( for k being Nat st k in dom it holds it /. k = Sum (M /. k) ) ); existence ex b1 being FinSequence of V1 st ( len b1 = len M & ( for k being Nat st k in dom b1 holds b1 /. k = Sum (M /. k) ) ) proof deffunc H1( Nat) -> Element of the carrier of V1 = Sum (M /. $1); consider F being FinSequence of V1 such that A1: ( len F = len M & ( for k being Nat st k in dom F holds F . k = H1(k) ) ) from FINSEQ_2:sch_1(); take F ; ::_thesis: ( len F = len M & ( for k being Nat st k in dom F holds F /. k = Sum (M /. k) ) ) thus len F = len M by A1; ::_thesis: for k being Nat st k in dom F holds F /. k = Sum (M /. k) hereby ::_thesis: verum let k be Nat; ::_thesis: ( k in dom F implies F /. k = Sum (M /. k) ) assume A2: k in dom F ; ::_thesis: F /. k = Sum (M /. k) hence F /. k = F . k by PARTFUN1:def_6 .= Sum (M /. k) by A1, A2 ; ::_thesis: verum end; end; uniqueness for b1, b2 being FinSequence of V1 st len b1 = len M & ( for k being Nat st k in dom b1 holds b1 /. k = Sum (M /. k) ) & len b2 = len M & ( for k being Nat st k in dom b2 holds b2 /. k = Sum (M /. k) ) holds b1 = b2 proof let F1, F2 be FinSequence of V1; ::_thesis: ( len F1 = len M & ( for k being Nat st k in dom F1 holds F1 /. k = Sum (M /. k) ) & len F2 = len M & ( for k being Nat st k in dom F2 holds F2 /. k = Sum (M /. k) ) implies F1 = F2 ) assume that A3: len F1 = len M and A4: for k being Nat st k in dom F1 holds F1 /. k = Sum (M /. k) and A5: len F2 = len M and A6: for k being Nat st k in dom F2 holds F2 /. k = Sum (M /. k) ; ::_thesis: F1 = F2 A7: dom F1 = Seg (len F1) by FINSEQ_1:def_3; now__::_thesis:_for_k_being_Nat_st_k_in_dom_F1_holds_ F1_._k_=_F2_._k let k be Nat; ::_thesis: ( k in dom F1 implies F1 . k = F2 . k ) assume A8: k in dom F1 ; ::_thesis: F1 . k = F2 . k then A9: k in dom F2 by A3, A5, A7, FINSEQ_1:def_3; thus F1 . k = F1 /. k by A8, PARTFUN1:def_6 .= Sum (M /. k) by A4, A8 .= F2 /. k by A6, A9 .= F2 . k by A9, PARTFUN1:def_6 ; ::_thesis: verum end; hence F1 = F2 by A3, A5, FINSEQ_2:9; ::_thesis: verum end; end; :: deftheorem Def6 defines Sum MATRLIN:def_6_:_ for V1 being non empty addLoopStr for M being FinSequence of the carrier of V1 * for b3 being FinSequence of V1 holds ( b3 = Sum M iff ( len b3 = len M & ( for k being Nat st k in dom b3 holds b3 /. k = Sum (M /. k) ) ) ); theorem Th13: :: MATRLIN:13 for K being Field for V1 being finite-dimensional VectSp of K for M being Matrix of the carrier of V1 st len M = 0 holds Sum (Sum M) = 0. V1 proof let K be Field; ::_thesis: for V1 being finite-dimensional VectSp of K for M being Matrix of the carrier of V1 st len M = 0 holds Sum (Sum M) = 0. V1 let V1 be finite-dimensional VectSp of K; ::_thesis: for M being Matrix of the carrier of V1 st len M = 0 holds Sum (Sum M) = 0. V1 let M be Matrix of the carrier of V1; ::_thesis: ( len M = 0 implies Sum (Sum M) = 0. V1 ) assume len M = 0 ; ::_thesis: Sum (Sum M) = 0. V1 then len (Sum M) = 0 by Def6; then Sum M = <*> the carrier of V1 ; hence Sum (Sum M) = 0. V1 by RLVECT_1:43; ::_thesis: verum end; theorem Th14: :: MATRLIN:14 for m being Nat for K being Field for V1 being finite-dimensional VectSp of K for M being Matrix of m + 1, 0 , the carrier of V1 holds Sum (Sum M) = 0. V1 proof let m be Nat; ::_thesis: for K being Field for V1 being finite-dimensional VectSp of K for M being Matrix of m + 1, 0 , the carrier of V1 holds Sum (Sum M) = 0. V1 let K be Field; ::_thesis: for V1 being finite-dimensional VectSp of K for M being Matrix of m + 1, 0 , the carrier of V1 holds Sum (Sum M) = 0. V1 let V1 be finite-dimensional VectSp of K; ::_thesis: for M being Matrix of m + 1, 0 , the carrier of V1 holds Sum (Sum M) = 0. V1 let M be Matrix of m + 1, 0 , the carrier of V1; ::_thesis: Sum (Sum M) = 0. V1 for k being Nat st k in dom (Sum M) holds (Sum M) /. k = 0. V1 proof let k be Nat; ::_thesis: ( k in dom (Sum M) implies (Sum M) /. k = 0. V1 ) assume A1: k in dom (Sum M) ; ::_thesis: (Sum M) /. k = 0. V1 reconsider k1 = k as Element of NAT by ORDINAL1:def_12; len M = len (Sum M) by Def6; then dom M = dom (Sum M) by FINSEQ_3:29; then M /. k1 in rng M by A1, PARTFUN2:2; then len (M /. k) = 0 by MATRIX_1:def_2; then A2: M /. k = <*> the carrier of V1 ; thus (Sum M) /. k = Sum (M /. k) by A1, Def6 .= 0. V1 by A2, RLVECT_1:43 ; ::_thesis: verum end; hence Sum (Sum M) = 0. V1 by Th11; ::_thesis: verum end; theorem Th15: :: MATRLIN:15 for D being non empty set for x being Element of D holds <*<*x*>*> = <*<*x*>*> @ proof let D be non empty set ; ::_thesis: for x being Element of D holds <*<*x*>*> = <*<*x*>*> @ let x be Element of D; ::_thesis: <*<*x*>*> = <*<*x*>*> @ set P = <*<*x*>*>; set R = <*<*x*>*> @ ; A1: len <*<*x*>*> = 1 by FINSEQ_1:40; then A2: width <*<*x*>*> = len <*x*> by MATRIX_1:20 .= 1 by FINSEQ_1:40 ; then A3: len (<*<*x*>*> @) = 1 by MATRIX_2:10; A4: now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_<*<*x*>*>_holds_ <*<*x*>*>_*_(i,j)_=_(<*<*x*>*>_@)_*_(i,j) let i, j be Nat; ::_thesis: ( [i,j] in Indices <*<*x*>*> implies <*<*x*>*> * (i,j) = (<*<*x*>*> @) * (i,j) ) assume A5: [i,j] in Indices <*<*x*>*> ; ::_thesis: <*<*x*>*> * (i,j) = (<*<*x*>*> @) * (i,j) then A6: [i,j] in [:(dom <*<*x*>*>),(Seg 1):] by A2, MATRIX_1:def_4; then i in dom <*<*x*>*> by ZFMISC_1:87; then i in Seg 1 by A1, FINSEQ_1:def_3; then A7: i = 1 by FINSEQ_1:2, TARSKI:def_1; j in Seg 1 by A6, ZFMISC_1:87; then j = 1 by FINSEQ_1:2, TARSKI:def_1; hence <*<*x*>*> * (i,j) = (<*<*x*>*> @) * (i,j) by A5, A7, MATRIX_1:def_6; ::_thesis: verum end; width (<*<*x*>*> @) = 1 by A1, A2, MATRIX_2:10; hence <*<*x*>*> = <*<*x*>*> @ by A1, A2, A3, A4, MATRIX_1:21; ::_thesis: verum end; theorem Th16: :: MATRLIN:16 for K being Field for V1, V2 being VectSp of K for f being Function of V1,V2 for p being FinSequence of V1 st f is additive & f is homogeneous holds f . (Sum p) = Sum (f * p) proof let K be Field; ::_thesis: for V1, V2 being VectSp of K for f being Function of V1,V2 for p being FinSequence of V1 st f is additive & f is homogeneous holds f . (Sum p) = Sum (f * p) let V1, V2 be VectSp of K; ::_thesis: for f being Function of V1,V2 for p being FinSequence of V1 st f is additive & f is homogeneous holds f . (Sum p) = Sum (f * p) let f be Function of V1,V2; ::_thesis: for p being FinSequence of V1 st f is additive & f is homogeneous holds f . (Sum p) = Sum (f * p) let p be FinSequence of V1; ::_thesis: ( f is additive & f is homogeneous implies f . (Sum p) = Sum (f * p) ) defpred S1[ FinSequence of V1] means f . (Sum $1) = Sum (f * $1); assume A1: ( f is additive & f is homogeneous ) ; ::_thesis: f . (Sum p) = Sum (f * p) A2: for p being FinSequence of V1 for w being Element of V1 st S1[p] holds S1[p ^ <*w*>] proof let p be FinSequence of V1; ::_thesis: for w being Element of V1 st S1[p] holds S1[p ^ <*w*>] let w be Element of V1; ::_thesis: ( S1[p] implies S1[p ^ <*w*>] ) assume A3: f . (Sum p) = Sum (f * p) ; ::_thesis: S1[p ^ <*w*>] thus f . (Sum (p ^ <*w*>)) = f . ((Sum p) + (Sum <*w*>)) by RLVECT_1:41 .= (Sum (f * p)) + (f . (Sum <*w*>)) by A1, A3, VECTSP_1:def_20 .= (Sum (f * p)) + (f . w) by RLVECT_1:44 .= (Sum (f * p)) + (Sum <*(f . w)*>) by RLVECT_1:44 .= Sum ((f * p) ^ <*(f . w)*>) by RLVECT_1:41 .= Sum (f * (p ^ <*w*>)) by FINSEQOP:8 ; ::_thesis: verum end; f . (Sum (<*> the carrier of V1)) = f . (0. V1) by RLVECT_1:43 .= f . ((0. K) * (0. V1)) by VECTSP_1:14 .= (0. K) * (f . (0. V1)) by A1, MOD_2:def_2 .= 0. V2 by VECTSP_1:14 .= Sum (<*> the carrier of V2) by RLVECT_1:43 .= Sum (f * (<*> the carrier of V1)) ; then A4: S1[ <*> the carrier of V1] ; for p being FinSequence of V1 holds S1[p] from FINSEQ_2:sch_2(A4, A2); hence f . (Sum p) = Sum (f * p) ; ::_thesis: verum end; theorem Th17: :: MATRLIN:17 for K being Field for V2, V1 being finite-dimensional VectSp of K for f being Function of V1,V2 for a being FinSequence of K for p being FinSequence of V1 st len p = len a & f is additive & f is homogeneous holds f * (lmlt (a,p)) = lmlt (a,(f * p)) proof let K be Field; ::_thesis: for V2, V1 being finite-dimensional VectSp of K for f being Function of V1,V2 for a being FinSequence of K for p being FinSequence of V1 st len p = len a & f is additive & f is homogeneous holds f * (lmlt (a,p)) = lmlt (a,(f * p)) let V2, V1 be finite-dimensional VectSp of K; ::_thesis: for f being Function of V1,V2 for a being FinSequence of K for p being FinSequence of V1 st len p = len a & f is additive & f is homogeneous holds f * (lmlt (a,p)) = lmlt (a,(f * p)) let f be Function of V1,V2; ::_thesis: for a being FinSequence of K for p being FinSequence of V1 st len p = len a & f is additive & f is homogeneous holds f * (lmlt (a,p)) = lmlt (a,(f * p)) let a be FinSequence of K; ::_thesis: for p being FinSequence of V1 st len p = len a & f is additive & f is homogeneous holds f * (lmlt (a,p)) = lmlt (a,(f * p)) let p be FinSequence of V1; ::_thesis: ( len p = len a & f is additive & f is homogeneous implies f * (lmlt (a,p)) = lmlt (a,(f * p)) ) assume len p = len a ; ::_thesis: ( not f is additive or not f is homogeneous or f * (lmlt (a,p)) = lmlt (a,(f * p)) ) then A1: dom p = dom a by FINSEQ_3:29; dom f = the carrier of V1 by FUNCT_2:def_1; then rng p c= dom f by FINSEQ_1:def_4; then A2: dom p = dom (f * p) by RELAT_1:27; assume A3: ( f is additive & f is homogeneous ) ; ::_thesis: f * (lmlt (a,p)) = lmlt (a,(f * p)) A4: now__::_thesis:_for_k_being_Nat_st_k_in_dom_(f_*_(lmlt_(a,p)))_holds_ (f_*_(lmlt_(a,p)))_._k_=_(lmlt_(a,(f_*_p)))_._k set P = f * p; let k be Nat; ::_thesis: ( k in dom (f * (lmlt (a,p))) implies (f * (lmlt (a,p))) . k = (lmlt (a,(f * p))) . k ) assume A5: k in dom (f * (lmlt (a,p))) ; ::_thesis: (f * (lmlt (a,p))) . k = (lmlt (a,(f * p))) . k A6: dom (f * (lmlt (a,p))) c= dom (lmlt (a,p)) by RELAT_1:25; then k in dom (lmlt (a,p)) by A5; then A7: k in dom p by A1, Th12; then A8: p /. k = p . k by PARTFUN1:def_6; A9: k in dom (lmlt (a,(f * p))) by A1, A2, A7, Th12; A10: a /. k = a . k by A1, A7, PARTFUN1:def_6; A11: (f * p) /. k = (f * p) . k by A2, A7, PARTFUN1:def_6; thus (f * (lmlt (a,p))) . k = f . ((lmlt (a,p)) . k) by A5, FUNCT_1:12 .= f . ( the lmult of V1 . ((a . k),(p . k))) by A5, A6, FUNCOP_1:22 .= f . ((a /. k) * (p /. k)) by A10, A8, VECTSP_1:def_12 .= (a /. k) * (f . (p /. k)) by A3, MOD_2:def_2 .= (a /. k) * ((f * p) /. k) by A7, A8, A11, FUNCT_1:13 .= the lmult of V2 . ((a . k),((f * p) . k)) by A10, A11, VECTSP_1:def_12 .= (lmlt (a,(f * p))) . k by A9, FUNCOP_1:22 ; ::_thesis: verum end; dom (lmlt (a,p)) = dom p by A1, Th12 .= dom (lmlt (a,(f * p))) by A1, A2, Th12 ; then len (lmlt (a,p)) = len (lmlt (a,(f * p))) by FINSEQ_3:29; then len (f * (lmlt (a,p))) = len (lmlt (a,(f * p))) by FINSEQ_2:33; hence f * (lmlt (a,p)) = lmlt (a,(f * p)) by A4, FINSEQ_2:9; ::_thesis: verum end; theorem Th18: :: MATRLIN:18 for K being Field for V3, V2 being finite-dimensional VectSp of K for g being Function of V2,V3 for b2 being OrdBasis of V2 for a being FinSequence of K st len a = len b2 & g is additive & g is homogeneous holds g . (Sum (lmlt (a,b2))) = Sum (lmlt (a,(g * b2))) proof let K be Field; ::_thesis: for V3, V2 being finite-dimensional VectSp of K for g being Function of V2,V3 for b2 being OrdBasis of V2 for a being FinSequence of K st len a = len b2 & g is additive & g is homogeneous holds g . (Sum (lmlt (a,b2))) = Sum (lmlt (a,(g * b2))) let V3, V2 be finite-dimensional VectSp of K; ::_thesis: for g being Function of V2,V3 for b2 being OrdBasis of V2 for a being FinSequence of K st len a = len b2 & g is additive & g is homogeneous holds g . (Sum (lmlt (a,b2))) = Sum (lmlt (a,(g * b2))) let g be Function of V2,V3; ::_thesis: for b2 being OrdBasis of V2 for a being FinSequence of K st len a = len b2 & g is additive & g is homogeneous holds g . (Sum (lmlt (a,b2))) = Sum (lmlt (a,(g * b2))) let b2 be OrdBasis of V2; ::_thesis: for a being FinSequence of K st len a = len b2 & g is additive & g is homogeneous holds g . (Sum (lmlt (a,b2))) = Sum (lmlt (a,(g * b2))) let a be FinSequence of K; ::_thesis: ( len a = len b2 & g is additive & g is homogeneous implies g . (Sum (lmlt (a,b2))) = Sum (lmlt (a,(g * b2))) ) assume that A1: len a = len b2 and A2: ( g is additive & g is homogeneous ) ; ::_thesis: g . (Sum (lmlt (a,b2))) = Sum (lmlt (a,(g * b2))) thus g . (Sum (lmlt (a,b2))) = Sum (g * (lmlt (a,b2))) by A2, Th16 .= Sum (lmlt (a,(g * b2))) by A1, A2, Th17 ; ::_thesis: verum end; theorem Th19: :: MATRLIN:19 for K being Field for V1 being finite-dimensional VectSp of K for F, F1 being FinSequence of V1 for KL being Linear_Combination of V1 for p being Permutation of (dom F) st F1 = F * p holds KL (#) F1 = (KL (#) F) * p proof let K be Field; ::_thesis: for V1 being finite-dimensional VectSp of K for F, F1 being FinSequence of V1 for KL being Linear_Combination of V1 for p being Permutation of (dom F) st F1 = F * p holds KL (#) F1 = (KL (#) F) * p let V1 be finite-dimensional VectSp of K; ::_thesis: for F, F1 being FinSequence of V1 for KL being Linear_Combination of V1 for p being Permutation of (dom F) st F1 = F * p holds KL (#) F1 = (KL (#) F) * p let F, F1 be FinSequence of V1; ::_thesis: for KL being Linear_Combination of V1 for p being Permutation of (dom F) st F1 = F * p holds KL (#) F1 = (KL (#) F) * p let KL be Linear_Combination of V1; ::_thesis: for p being Permutation of (dom F) st F1 = F * p holds KL (#) F1 = (KL (#) F) * p let p be Permutation of (dom F); ::_thesis: ( F1 = F * p implies KL (#) F1 = (KL (#) F) * p ) assume A1: F1 = F * p ; ::_thesis: KL (#) F1 = (KL (#) F) * p dom F = Seg (len F) by FINSEQ_1:def_3; then dom F = Seg (len (KL (#) F)) by VECTSP_6:def_5; then A2: dom F = dom (KL (#) F) by FINSEQ_1:def_3; then reconsider F2 = (KL (#) F) * p as FinSequence of V1 by FINSEQ_2:47; len (KL (#) F1) = len F1 by VECTSP_6:def_5 .= len F by A1, FINSEQ_2:44 .= len (KL (#) F) by VECTSP_6:def_5 .= len F2 by A2, FINSEQ_2:44 ; then A3: dom (KL (#) F1) = dom ((KL (#) F) * p) by FINSEQ_3:29; len (KL (#) F1) = len F1 by VECTSP_6:def_5; then A4: dom (KL (#) F1) = dom F1 by FINSEQ_3:29; now__::_thesis:_for_k_being_Nat_st_k_in_dom_(KL_(#)_F1)_holds_ (KL_(#)_F1)_._k_=_F2_._k let k be Nat; ::_thesis: ( k in dom (KL (#) F1) implies (KL (#) F1) . k = F2 . k ) reconsider k0 = k as Element of NAT by ORDINAL1:def_12; assume A5: k in dom (KL (#) F1) ; ::_thesis: (KL (#) F1) . k = F2 . k then k in dom p by A3, FUNCT_1:11; then p . k in rng p by FUNCT_1:def_3; then A6: p . k in dom F by FUNCT_2:def_3; then reconsider k1 = p . k0 as Element of NAT by FINSEQ_3:23; F1 /. k = F1 . k by A4, A5, PARTFUN1:def_6 .= F . (p . k) by A1, A4, A5, FUNCT_1:12 .= F /. (p . k) by A6, PARTFUN1:def_6 ; hence (KL (#) F1) . k = (KL . (F /. k1)) * (F /. k1) by A5, VECTSP_6:def_5 .= (KL (#) F) . k1 by A2, A6, VECTSP_6:def_5 .= F2 . k by A3, A5, FUNCT_1:12 ; ::_thesis: verum end; hence KL (#) F1 = (KL (#) F) * p by A3, FINSEQ_1:13; ::_thesis: verum end; theorem Th20: :: MATRLIN:20 for K being Field for V1 being finite-dimensional VectSp of K for F being FinSequence of V1 for KL being Linear_Combination of V1 st F is one-to-one & Carrier KL c= rng F holds Sum (KL (#) F) = Sum KL proof let K be Field; ::_thesis: for V1 being finite-dimensional VectSp of K for F being FinSequence of V1 for KL being Linear_Combination of V1 st F is one-to-one & Carrier KL c= rng F holds Sum (KL (#) F) = Sum KL let V1 be finite-dimensional VectSp of K; ::_thesis: for F being FinSequence of V1 for KL being Linear_Combination of V1 st F is one-to-one & Carrier KL c= rng F holds Sum (KL (#) F) = Sum KL let F be FinSequence of V1; ::_thesis: for KL being Linear_Combination of V1 st F is one-to-one & Carrier KL c= rng F holds Sum (KL (#) F) = Sum KL let KL be Linear_Combination of V1; ::_thesis: ( F is one-to-one & Carrier KL c= rng F implies Sum (KL (#) F) = Sum KL ) assume A1: F is one-to-one ; ::_thesis: ( not Carrier KL c= rng F or Sum (KL (#) F) = Sum KL ) assume A2: Carrier KL c= rng F ; ::_thesis: Sum (KL (#) F) = Sum KL then reconsider A = Carrier KL as Subset of (rng F) ; consider p1 being Permutation of (dom F) such that A3: (F - (A `)) ^ (F - A) = F * p1 by FINSEQ_3:115; reconsider G1 = F - (A `), G2 = F - A as FinSequence of V1 by FINSEQ_3:86; A4: G1 is one-to-one by A1, FINSEQ_3:87; len (KL (#) F) = len F by VECTSP_6:def_5; then dom (KL (#) F) = dom F by FINSEQ_3:29; then reconsider p1 = p1 as Permutation of (dom (KL (#) F)) ; A5: rng G1 = (rng F) \ (A `) by FINSEQ_3:65 .= (rng F) \ ((rng F) \ (Carrier KL)) by SUBSET_1:def_4 .= (rng F) /\ (Carrier KL) by XBOOLE_1:48 .= Carrier KL by A2, XBOOLE_1:28 ; for k being Nat st k in dom (KL (#) G2) holds (KL (#) G2) /. k = 0. V1 proof let k be Nat; ::_thesis: ( k in dom (KL (#) G2) implies (KL (#) G2) /. k = 0. V1 ) assume A6: k in dom (KL (#) G2) ; ::_thesis: (KL (#) G2) /. k = 0. V1 len (KL (#) G2) = len G2 by VECTSP_6:def_5; then A7: dom (KL (#) G2) = dom G2 by FINSEQ_3:29; then G2 . k in rng G2 by A6, FUNCT_1:def_3; then G2 . k in (rng F) \ (Carrier KL) by FINSEQ_3:65; then not G2 . k in Carrier KL by XBOOLE_0:def_5; then A8: not G2 /. k in Carrier KL by A6, A7, PARTFUN1:def_6; reconsider k1 = k as Element of NAT by ORDINAL1:def_12; thus (KL (#) G2) /. k = (KL (#) G2) . k by A6, PARTFUN1:def_6 .= (KL . (G2 /. k1)) * (G2 /. k1) by A6, VECTSP_6:def_5 .= (0. K) * (G2 /. k) by A8, VECTSP_6:2 .= 0. V1 by VECTSP_1:14 ; ::_thesis: verum end; then A9: Sum (KL (#) G2) = 0. V1 by Th11; KL (#) (G1 ^ G2) = (KL (#) F) * p1 by A3, Th19; hence Sum (KL (#) F) = Sum (KL (#) (G1 ^ G2)) by RLVECT_2:7 .= Sum ((KL (#) G1) ^ (KL (#) G2)) by VECTSP_6:13 .= (Sum (KL (#) G1)) + (Sum (KL (#) G2)) by RLVECT_1:41 .= (Sum KL) + (0. V1) by A4, A5, A9, VECTSP_6:def_6 .= Sum KL by RLVECT_1:4 ; ::_thesis: verum end; theorem Th21: :: MATRLIN:21 for K being Field for V2, V1 being finite-dimensional VectSp of K for f1, f2 being Function of V1,V2 for A being set for p being FinSequence of V1 st rng p c= A & f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous & ( for v being Element of V1 st v in A holds f1 . v = f2 . v ) holds f1 . (Sum p) = f2 . (Sum p) proof let K be Field; ::_thesis: for V2, V1 being finite-dimensional VectSp of K for f1, f2 being Function of V1,V2 for A being set for p being FinSequence of V1 st rng p c= A & f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous & ( for v being Element of V1 st v in A holds f1 . v = f2 . v ) holds f1 . (Sum p) = f2 . (Sum p) let V2, V1 be finite-dimensional VectSp of K; ::_thesis: for f1, f2 being Function of V1,V2 for A being set for p being FinSequence of V1 st rng p c= A & f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous & ( for v being Element of V1 st v in A holds f1 . v = f2 . v ) holds f1 . (Sum p) = f2 . (Sum p) let f1, f2 be Function of V1,V2; ::_thesis: for A being set for p being FinSequence of V1 st rng p c= A & f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous & ( for v being Element of V1 st v in A holds f1 . v = f2 . v ) holds f1 . (Sum p) = f2 . (Sum p) let A be set ; ::_thesis: for p being FinSequence of V1 st rng p c= A & f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous & ( for v being Element of V1 st v in A holds f1 . v = f2 . v ) holds f1 . (Sum p) = f2 . (Sum p) let p be FinSequence of V1; ::_thesis: ( rng p c= A & f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous & ( for v being Element of V1 st v in A holds f1 . v = f2 . v ) implies f1 . (Sum p) = f2 . (Sum p) ) assume A1: rng p c= A ; ::_thesis: ( not f1 is additive or not f1 is homogeneous or not f2 is additive or not f2 is homogeneous or ex v being Element of V1 st ( v in A & not f1 . v = f2 . v ) or f1 . (Sum p) = f2 . (Sum p) ) defpred S1[ FinSequence of V1] means ( rng $1 c= A implies f1 . (Sum $1) = f2 . (Sum $1) ); assume A2: ( f1 is additive & f1 is homogeneous ) ; ::_thesis: ( not f2 is additive or not f2 is homogeneous or ex v being Element of V1 st ( v in A & not f1 . v = f2 . v ) or f1 . (Sum p) = f2 . (Sum p) ) assume A3: ( f2 is additive & f2 is homogeneous ) ; ::_thesis: ( ex v being Element of V1 st ( v in A & not f1 . v = f2 . v ) or f1 . (Sum p) = f2 . (Sum p) ) assume A4: for v being Element of V1 st v in A holds f1 . v = f2 . v ; ::_thesis: f1 . (Sum p) = f2 . (Sum p) A5: for p being FinSequence of V1 for x being Element of V1 st S1[p] holds S1[p ^ <*x*>] proof let p be FinSequence of V1; ::_thesis: for x being Element of V1 st S1[p] holds S1[p ^ <*x*>] let x be Element of V1; ::_thesis: ( S1[p] implies S1[p ^ <*x*>] ) assume A6: ( rng p c= A implies f1 . (Sum p) = f2 . (Sum p) ) ; ::_thesis: S1[p ^ <*x*>] A7: rng p c= (rng p) \/ (rng <*x*>) by XBOOLE_1:7; assume rng (p ^ <*x*>) c= A ; ::_thesis: f1 . (Sum (p ^ <*x*>)) = f2 . (Sum (p ^ <*x*>)) then A8: (rng p) \/ (rng <*x*>) c= A by FINSEQ_1:31; rng <*x*> c= (rng p) \/ (rng <*x*>) by XBOOLE_1:7; then rng <*x*> c= A by A8, XBOOLE_1:1; then {x} c= A by FINSEQ_1:39; then A9: x in A by ZFMISC_1:31; thus f1 . (Sum (p ^ <*x*>)) = f1 . ((Sum p) + (Sum <*x*>)) by RLVECT_1:41 .= (f2 . (Sum p)) + (f1 . (Sum <*x*>)) by A2, A6, A8, A7, VECTSP_1:def_20, XBOOLE_1:1 .= (f2 . (Sum p)) + (f1 . x) by RLVECT_1:44 .= (f2 . (Sum p)) + (f2 . x) by A4, A9 .= (f2 . (Sum p)) + (f2 . (Sum <*x*>)) by RLVECT_1:44 .= f2 . ((Sum p) + (Sum <*x*>)) by A3, VECTSP_1:def_20 .= f2 . (Sum (p ^ <*x*>)) by RLVECT_1:41 ; ::_thesis: verum end; A10: S1[ <*> the carrier of V1] proof assume rng (<*> the carrier of V1) c= A ; ::_thesis: f1 . (Sum (<*> the carrier of V1)) = f2 . (Sum (<*> the carrier of V1)) thus f1 . (Sum (<*> the carrier of V1)) = f1 . (0. V1) by RLVECT_1:43 .= f1 . ((0. K) * (0. V1)) by VECTSP_1:14 .= (0. K) * (f1 . (0. V1)) by A2, MOD_2:def_2 .= 0. V2 by VECTSP_1:14 .= (0. K) * (f2 . (0. V1)) by VECTSP_1:14 .= f2 . ((0. K) * (0. V1)) by A3, MOD_2:def_2 .= f2 . (0. V1) by VECTSP_1:14 .= f2 . (Sum (<*> the carrier of V1)) by RLVECT_1:43 ; ::_thesis: verum end; for p being FinSequence of V1 holds S1[p] from FINSEQ_2:sch_2(A10, A5); hence f1 . (Sum p) = f2 . (Sum p) by A1; ::_thesis: verum end; theorem Th22: :: MATRLIN:22 for K being Field for V2, V1 being finite-dimensional VectSp of K for f1, f2 being Function of V1,V2 st f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous holds for b1 being OrdBasis of V1 st len b1 > 0 & f1 * b1 = f2 * b1 holds f1 = f2 proof let K be Field; ::_thesis: for V2, V1 being finite-dimensional VectSp of K for f1, f2 being Function of V1,V2 st f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous holds for b1 being OrdBasis of V1 st len b1 > 0 & f1 * b1 = f2 * b1 holds f1 = f2 let V2, V1 be finite-dimensional VectSp of K; ::_thesis: for f1, f2 being Function of V1,V2 st f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous holds for b1 being OrdBasis of V1 st len b1 > 0 & f1 * b1 = f2 * b1 holds f1 = f2 let f1, f2 be Function of V1,V2; ::_thesis: ( f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous implies for b1 being OrdBasis of V1 st len b1 > 0 & f1 * b1 = f2 * b1 holds f1 = f2 ) assume that A1: ( f1 is additive & f1 is homogeneous ) and A2: ( f2 is additive & f2 is homogeneous ) ; ::_thesis: for b1 being OrdBasis of V1 st len b1 > 0 & f1 * b1 = f2 * b1 holds f1 = f2 let b1 be OrdBasis of V1; ::_thesis: ( len b1 > 0 & f1 * b1 = f2 * b1 implies f1 = f2 ) assume A3: len b1 > 0 ; ::_thesis: ( not f1 * b1 = f2 * b1 or f1 = f2 ) reconsider b = rng b1 as Basis of V1 by Def2; assume A4: f1 * b1 = f2 * b1 ; ::_thesis: f1 = f2 now__::_thesis:_for_v_being_Element_of_V1_holds_f1_._v_=_f2_._v len b1 in Seg (len b1) by A3, FINSEQ_1:3; then reconsider D = dom b1 as non empty set by FINSEQ_1:def_3; let v be Element of V1; ::_thesis: f1 . v = f2 . v Lin b = VectSpStr(# the carrier of V1, the addF of V1, the ZeroF of V1, the lmult of V1 #) by VECTSP_7:def_3; then v in Lin b by RLVECT_1:1; then consider KL being Linear_Combination of b such that A5: v = Sum KL by VECTSP_7:7; set p = KL (#) b1; set A = { ((KL . (b1 /. i)) * (b1 /. i)) where i is Element of D : verum } ; A6: rng (KL (#) b1) c= { ((KL . (b1 /. i)) * (b1 /. i)) where i is Element of D : verum } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (KL (#) b1) or x in { ((KL . (b1 /. i)) * (b1 /. i)) where i is Element of D : verum } ) assume x in rng (KL (#) b1) ; ::_thesis: x in { ((KL . (b1 /. i)) * (b1 /. i)) where i is Element of D : verum } then consider i being Nat such that A7: i in dom (KL (#) b1) and A8: (KL (#) b1) . i = x by FINSEQ_2:10; dom (KL (#) b1) = Seg (len (KL (#) b1)) by FINSEQ_1:def_3; then i in Seg (len b1) by A7, VECTSP_6:def_5; then A9: i in dom b1 by FINSEQ_1:def_3; (KL (#) b1) . i = (KL . (b1 /. i)) * (b1 /. i) by A7, VECTSP_6:def_5; hence x in { ((KL . (b1 /. i)) * (b1 /. i)) where i is Element of D : verum } by A8, A9; ::_thesis: verum end; A10: for w being Element of V1 st w in { ((KL . (b1 /. i)) * (b1 /. i)) where i is Element of D : verum } holds f1 . w = f2 . w proof let w be Element of V1; ::_thesis: ( w in { ((KL . (b1 /. i)) * (b1 /. i)) where i is Element of D : verum } implies f1 . w = f2 . w ) assume w in { ((KL . (b1 /. i)) * (b1 /. i)) where i is Element of D : verum } ; ::_thesis: f1 . w = f2 . w then consider i being Element of D such that A11: w = (KL . (b1 /. i)) * (b1 /. i) ; f1 . (b1 /. i) = f1 . (b1 . i) by PARTFUN1:def_6 .= (f2 * b1) . i by A4, FUNCT_1:13 .= f2 . (b1 . i) by FUNCT_1:13 .= f2 . (b1 /. i) by PARTFUN1:def_6 ; then f1 . ((KL . (b1 /. i)) * (b1 /. i)) = (KL . (b1 /. i)) * (f2 . (b1 /. i)) by A1, MOD_2:def_2 .= f2 . ((KL . (b1 /. i)) * (b1 /. i)) by A2, MOD_2:def_2 ; hence f1 . w = f2 . w by A11; ::_thesis: verum end; A12: ( b1 is one-to-one & Carrier KL c= rng b1 ) by Def2, VECTSP_6:def_4; hence f1 . v = f1 . (Sum (KL (#) b1)) by A5, Th20 .= f2 . (Sum (KL (#) b1)) by A1, A2, A6, A10, Th21 .= f2 . v by A5, A12, Th20 ; ::_thesis: verum end; hence f1 = f2 by FUNCT_2:63; ::_thesis: verum end; registration let D be non empty set ; cluster tabular -> FinSequence-yielding for FinSequence of D * ; coherence for b1 being Matrix of D holds b1 is FinSequence-yielding ; end; definition let D be non empty set ; let F, G be Matrix of D; :: original: ^^ redefine funcF ^^ G -> Matrix of D; coherence F ^^ G is Matrix of D proof reconsider M = F ^^ G as FinSequence ; ex n being Nat st for x being set st x in rng M holds ex p being FinSequence of D st ( x = p & len p = n ) proof take n = (width F) + (width G); ::_thesis: for x being set st x in rng M holds ex p being FinSequence of D st ( x = p & len p = n ) let x be set ; ::_thesis: ( x in rng M implies ex p being FinSequence of D st ( x = p & len p = n ) ) A1: ( rng F c= D * & rng G c= D * ) by FINSEQ_1:def_4; assume x in rng M ; ::_thesis: ex p being FinSequence of D st ( x = p & len p = n ) then consider y being set such that A2: y in dom M and A3: x = M . y by FUNCT_1:def_3; A4: dom M = (dom F) /\ (dom G) by PRE_POLY:def_4; then A5: y in dom G by A2, XBOOLE_0:def_4; then A6: G . y in rng G by FUNCT_1:def_3; A7: y in dom F by A2, A4, XBOOLE_0:def_4; then F . y in rng F by FUNCT_1:def_3; then reconsider f = F . y, g = G . y as FinSequence of D by A6, A1, FINSEQ_1:def_11; reconsider y = y as Nat by A2, FINSEQ_3:23; A8: G . y = Line (G,y) by A5, MATRIX_2:16; A9: x = f ^ g by A2, A3, PRE_POLY:def_4; then reconsider p = x as FinSequence of D ; take p ; ::_thesis: ( x = p & len p = n ) thus x = p ; ::_thesis: len p = n F . y = Line (F,y) by A7, MATRIX_2:16; hence len p = (len (Line (F,y))) + (len (Line (G,y))) by A9, A8, FINSEQ_1:22 .= (width F) + (len (Line (G,y))) by MATRIX_1:def_7 .= n by MATRIX_1:def_7 ; ::_thesis: verum end; hence F ^^ G is Matrix of D by MATRIX_1:9; ::_thesis: verum end; end; definition let D be non empty set ; let n, m, k be Nat; let M1 be Matrix of n,k,D; let M2 be Matrix of m,k,D; :: original: ^ redefine funcM1 ^ M2 -> Matrix of n + m,k,D; coherence M1 ^ M2 is Matrix of n + m,k,D proof percases ( n = 0 or m = 0 or ( n <> 0 & m <> 0 ) ) ; supposeA1: n = 0 ; ::_thesis: M1 ^ M2 is Matrix of n + m,k,D then len M1 = 0 by MATRIX_1:def_2; then M1 = {} ; hence M1 ^ M2 is Matrix of n + m,k,D by A1, FINSEQ_1:34; ::_thesis: verum end; supposeA2: m = 0 ; ::_thesis: M1 ^ M2 is Matrix of n + m,k,D then len M2 = 0 by MATRIX_1:def_2; then M2 = {} ; hence M1 ^ M2 is Matrix of n + m,k,D by A2, FINSEQ_1:34; ::_thesis: verum end; supposethat A3: n <> 0 and A4: m <> 0 ; ::_thesis: M1 ^ M2 is Matrix of n + m,k,D len M2 = m by MATRIX_1:def_2; then A5: width M2 = k by A4, MATRIX_1:20; len M1 = n by MATRIX_1:def_2; then A6: width M1 = k by A3, MATRIX_1:20; ex n being Nat st for x being set st x in rng (M1 ^ M2) holds ex p being FinSequence of D st ( x = p & len p = n ) proof take k ; ::_thesis: for x being set st x in rng (M1 ^ M2) holds ex p being FinSequence of D st ( x = p & len p = k ) let x be set ; ::_thesis: ( x in rng (M1 ^ M2) implies ex p being FinSequence of D st ( x = p & len p = k ) ) assume A7: x in rng (M1 ^ M2) ; ::_thesis: ex p being FinSequence of D st ( x = p & len p = k ) rng (M1 ^ M2) c= D * by FINSEQ_1:def_4; then reconsider p = x as FinSequence of D by A7, FINSEQ_1:def_11; take p ; ::_thesis: ( x = p & len p = k ) A8: x in (rng M1) \/ (rng M2) by A7, FINSEQ_1:31; now__::_thesis:_len_p_=_k percases ( x in rng M1 or x in rng M2 ) by A8, XBOOLE_0:def_3; suppose x in rng M1 ; ::_thesis: len p = k then consider y1 being set such that A9: y1 in dom M1 and A10: x = M1 . y1 by FUNCT_1:def_3; reconsider y1 = y1 as Nat by A9, FINSEQ_3:23; x = Line (M1,y1) by A9, A10, MATRIX_2:16; hence len p = k by A6, MATRIX_1:def_7; ::_thesis: verum end; suppose x in rng M2 ; ::_thesis: len p = k then consider y2 being set such that A11: y2 in dom M2 and A12: x = M2 . y2 by FUNCT_1:def_3; reconsider y2 = y2 as Nat by A11, FINSEQ_3:23; x = Line (M2,y2) by A11, A12, MATRIX_2:16; hence len p = k by A5, MATRIX_1:def_7; ::_thesis: verum end; end; end; hence ( x = p & len p = k ) ; ::_thesis: verum end; then reconsider M3 = M1 ^ M2 as Matrix of D by MATRIX_1:9; ( len M1 = n & len M2 = m ) by MATRIX_1:def_2; then A13: len M3 = n + m by FINSEQ_1:22; then consider s being FinSequence such that A14: s in rng M3 and A15: len s = width M3 by A3, MATRIX_1:def_3; A16: s in (rng M1) \/ (rng M2) by A14, FINSEQ_1:31; now__::_thesis:_width_M3_=_k percases ( s in rng M1 or s in rng M2 ) by A16, XBOOLE_0:def_3; suppose s in rng M1 ; ::_thesis: width M3 = k then consider y1 being set such that A17: y1 in dom M1 and A18: s = M1 . y1 by FUNCT_1:def_3; reconsider y1 = y1 as Nat by A17, FINSEQ_3:23; s = Line (M1,y1) by A17, A18, MATRIX_2:16; hence width M3 = k by A6, A15, MATRIX_1:def_7; ::_thesis: verum end; suppose s in rng M2 ; ::_thesis: width M3 = k then consider y2 being set such that A19: y2 in dom M2 and A20: s = M2 . y2 by FUNCT_1:def_3; reconsider y2 = y2 as Nat by A19, FINSEQ_3:23; s = Line (M2,y2) by A19, A20, MATRIX_2:16; hence width M3 = k by A5, A15, MATRIX_1:def_7; ::_thesis: verum end; end; end; hence M1 ^ M2 is Matrix of n + m,k,D by A3, A13, MATRIX_1:20; ::_thesis: verum end; end; end; end; theorem :: MATRLIN:23 for n, k, m, i being Nat for D being non empty set for M1 being Matrix of n,k,D for M2 being Matrix of m,k,D st i in dom M1 holds Line ((M1 ^ M2),i) = Line (M1,i) proof let n, k, m, i be Nat; ::_thesis: for D being non empty set for M1 being Matrix of n,k,D for M2 being Matrix of m,k,D st i in dom M1 holds Line ((M1 ^ M2),i) = Line (M1,i) let D be non empty set ; ::_thesis: for M1 being Matrix of n,k,D for M2 being Matrix of m,k,D st i in dom M1 holds Line ((M1 ^ M2),i) = Line (M1,i) let M1 be Matrix of n,k,D; ::_thesis: for M2 being Matrix of m,k,D st i in dom M1 holds Line ((M1 ^ M2),i) = Line (M1,i) let M2 be Matrix of m,k,D; ::_thesis: ( i in dom M1 implies Line ((M1 ^ M2),i) = Line (M1,i) ) assume A1: i in dom M1 ; ::_thesis: Line ((M1 ^ M2),i) = Line (M1,i) reconsider i1 = i as Element of NAT by ORDINAL1:def_12; dom M1 c= dom (M1 ^ M2) by FINSEQ_1:26; hence Line ((M1 ^ M2),i) = (M1 ^ M2) . i by A1, MATRIX_2:16 .= M1 . i1 by A1, FINSEQ_1:def_7 .= Line (M1,i) by A1, MATRIX_2:16 ; ::_thesis: verum end; theorem Th24: :: MATRLIN:24 for n, k, m being Nat for D being non empty set for M1 being Matrix of n,k,D for M2 being Matrix of m,k,D st width M1 = width M2 holds width (M1 ^ M2) = width M1 proof let n, k, m be Nat; ::_thesis: for D being non empty set for M1 being Matrix of n,k,D for M2 being Matrix of m,k,D st width M1 = width M2 holds width (M1 ^ M2) = width M1 let D be non empty set ; ::_thesis: for M1 being Matrix of n,k,D for M2 being Matrix of m,k,D st width M1 = width M2 holds width (M1 ^ M2) = width M1 let M1 be Matrix of n,k,D; ::_thesis: for M2 being Matrix of m,k,D st width M1 = width M2 holds width (M1 ^ M2) = width M1 let M2 be Matrix of m,k,D; ::_thesis: ( width M1 = width M2 implies width (M1 ^ M2) = width M1 ) assume A1: width M1 = width M2 ; ::_thesis: width (M1 ^ M2) = width M1 consider n being Nat such that A2: for x being set st x in rng (M1 ^ M2) holds ex P being FinSequence of D st ( x = P & len P = n ) by MATRIX_1:9; percases ( len (M1 ^ M2) = 0 or len (M1 ^ M2) > 0 ) ; supposeA3: len (M1 ^ M2) = 0 ; ::_thesis: width (M1 ^ M2) = width M1 then (len M1) + (len M2) = 0 by FINSEQ_1:22; then A4: len M1 = 0 ; width (M1 ^ M2) = 0 by A3, MATRIX_1:def_3 .= width M1 by A4, MATRIX_1:def_3 ; hence width (M1 ^ M2) = width M1 ; ::_thesis: verum end; supposeA5: len (M1 ^ M2) > 0 ; ::_thesis: width (M1 ^ M2) = width M1 then A6: (len M1) + (len M2) > 0 + 0 by FINSEQ_1:22; consider s being FinSequence such that A7: s in rng (M1 ^ M2) and A8: len s = width (M1 ^ M2) by A5, MATRIX_1:def_3; A9: ex P being FinSequence of D st ( s = P & len P = n ) by A2, A7; percases ( len M1 > 0 or len M2 > 0 ) by A6; suppose len M1 > 0 ; ::_thesis: width (M1 ^ M2) = width M1 then consider s1 being FinSequence such that A10: s1 in rng M1 and A11: len s1 = width M1 by MATRIX_1:def_3; rng M1 c= rng (M1 ^ M2) by FINSEQ_1:29; then ex P1 being FinSequence of D st ( s1 = P1 & len P1 = n ) by A2, A10; hence width (M1 ^ M2) = width M1 by A8, A9, A11; ::_thesis: verum end; suppose len M2 > 0 ; ::_thesis: width (M1 ^ M2) = width M1 then consider s2 being FinSequence such that A12: s2 in rng M2 and A13: len s2 = width M2 by MATRIX_1:def_3; rng M2 c= rng (M1 ^ M2) by FINSEQ_1:30; then ex P2 being FinSequence of D st ( s2 = P2 & len P2 = n ) by A2, A12; hence width (M1 ^ M2) = width M1 by A1, A8, A9, A13; ::_thesis: verum end; end; end; end; end; theorem :: MATRLIN:25 for t, k, m, n, i being Nat for D being non empty set for M1 being Matrix of t,k,D for M2 being Matrix of m,k,D st n in dom M2 & i = (len M1) + n holds Line ((M1 ^ M2),i) = Line (M2,n) proof let t, k, m, n, i be Nat; ::_thesis: for D being non empty set for M1 being Matrix of t,k,D for M2 being Matrix of m,k,D st n in dom M2 & i = (len M1) + n holds Line ((M1 ^ M2),i) = Line (M2,n) let D be non empty set ; ::_thesis: for M1 being Matrix of t,k,D for M2 being Matrix of m,k,D st n in dom M2 & i = (len M1) + n holds Line ((M1 ^ M2),i) = Line (M2,n) let M1 be Matrix of t,k,D; ::_thesis: for M2 being Matrix of m,k,D st n in dom M2 & i = (len M1) + n holds Line ((M1 ^ M2),i) = Line (M2,n) let M2 be Matrix of m,k,D; ::_thesis: ( n in dom M2 & i = (len M1) + n implies Line ((M1 ^ M2),i) = Line (M2,n) ) assume that A1: n in dom M2 and A2: i = (len M1) + n ; ::_thesis: Line ((M1 ^ M2),i) = Line (M2,n) reconsider n1 = n as Element of NAT by ORDINAL1:def_12; i in dom (M1 ^ M2) by A1, A2, FINSEQ_1:28; hence Line ((M1 ^ M2),i) = (M1 ^ M2) . i by MATRIX_2:16 .= M2 . n1 by A1, A2, FINSEQ_1:def_7 .= Line (M2,n) by A1, MATRIX_2:16 ; ::_thesis: verum end; theorem Th26: :: MATRLIN:26 for n, k, m being Nat for D being non empty set for M1 being Matrix of n,k,D for M2 being Matrix of m,k,D st width M1 = width M2 holds for i being Nat st i in Seg (width M1) holds Col ((M1 ^ M2),i) = (Col (M1,i)) ^ (Col (M2,i)) proof let n, k, m be Nat; ::_thesis: for D being non empty set for M1 being Matrix of n,k,D for M2 being Matrix of m,k,D st width M1 = width M2 holds for i being Nat st i in Seg (width M1) holds Col ((M1 ^ M2),i) = (Col (M1,i)) ^ (Col (M2,i)) let D be non empty set ; ::_thesis: for M1 being Matrix of n,k,D for M2 being Matrix of m,k,D st width M1 = width M2 holds for i being Nat st i in Seg (width M1) holds Col ((M1 ^ M2),i) = (Col (M1,i)) ^ (Col (M2,i)) let M1 be Matrix of n,k,D; ::_thesis: for M2 being Matrix of m,k,D st width M1 = width M2 holds for i being Nat st i in Seg (width M1) holds Col ((M1 ^ M2),i) = (Col (M1,i)) ^ (Col (M2,i)) let M2 be Matrix of m,k,D; ::_thesis: ( width M1 = width M2 implies for i being Nat st i in Seg (width M1) holds Col ((M1 ^ M2),i) = (Col (M1,i)) ^ (Col (M2,i)) ) assume A1: width M1 = width M2 ; ::_thesis: for i being Nat st i in Seg (width M1) holds Col ((M1 ^ M2),i) = (Col (M1,i)) ^ (Col (M2,i)) let i be Nat; ::_thesis: ( i in Seg (width M1) implies Col ((M1 ^ M2),i) = (Col (M1,i)) ^ (Col (M2,i)) ) assume A2: i in Seg (width M1) ; ::_thesis: Col ((M1 ^ M2),i) = (Col (M1,i)) ^ (Col (M2,i)) A3: dom (Col ((M1 ^ M2),i)) = Seg (len (Col ((M1 ^ M2),i))) by FINSEQ_1:def_3; A4: len (Col ((M1 ^ M2),i)) = len (M1 ^ M2) by MATRIX_1:def_8 .= (len M1) + (len M2) by FINSEQ_1:22 .= (len M1) + (len (Col (M2,i))) by MATRIX_1:def_8 .= (len (Col (M1,i))) + (len (Col (M2,i))) by MATRIX_1:def_8 .= len ((Col (M1,i)) ^ (Col (M2,i))) by FINSEQ_1:22 ; now__::_thesis:_for_j_being_Nat_st_j_in_dom_(Col_((M1_^_M2),i))_holds_ (Col_((M1_^_M2),i))_._j_=_((Col_(M1,i))_^_(Col_(M2,i)))_._j let j be Nat; ::_thesis: ( j in dom (Col ((M1 ^ M2),i)) implies (Col ((M1 ^ M2),i)) . j = ((Col (M1,i)) ^ (Col (M2,i))) . j ) assume A5: j in dom (Col ((M1 ^ M2),i)) ; ::_thesis: (Col ((M1 ^ M2),i)) . j = ((Col (M1,i)) ^ (Col (M2,i))) . j then j in Seg (len (M1 ^ M2)) by A3, MATRIX_1:def_8; then A6: j in dom (M1 ^ M2) by FINSEQ_1:def_3; i in Seg (width (M1 ^ M2)) by A1, A2, Th24; then [j,i] in [:(dom (M1 ^ M2)),(Seg (width (M1 ^ M2))):] by A6, ZFMISC_1:87; then [j,i] in Indices (M1 ^ M2) by MATRIX_1:def_4; then consider P being FinSequence of D such that A7: P = (M1 ^ M2) . j and A8: (M1 ^ M2) * (j,i) = P . i by MATRIX_1:def_5; A9: j in dom ((Col (M1,i)) ^ (Col (M2,i))) by A4, A3, A5, FINSEQ_1:def_3; now__::_thesis:_(Col_((M1_^_M2),i))_._j_=_((Col_(M1,i))_^_(Col_(M2,i)))_._j percases ( j in dom (Col (M1,i)) or ex n being Nat st ( n in dom (Col (M2,i)) & j = (len (Col (M1,i))) + n ) ) by A9, FINSEQ_1:25; supposeA10: j in dom (Col (M1,i)) ; ::_thesis: (Col ((M1 ^ M2),i)) . j = ((Col (M1,i)) ^ (Col (M2,i))) . j then j in Seg (len (Col (M1,i))) by FINSEQ_1:def_3; then j in Seg (len M1) by MATRIX_1:def_8; then A11: j in dom M1 by FINSEQ_1:def_3; then [j,i] in [:(dom M1),(Seg (width M1)):] by A2, ZFMISC_1:87; then [j,i] in Indices M1 by MATRIX_1:def_4; then consider P1 being FinSequence of D such that A12: P1 = M1 . j and A13: M1 * (j,i) = P1 . i by MATRIX_1:def_5; P = P1 by A7, A11, A12, FINSEQ_1:def_7; hence (Col ((M1 ^ M2),i)) . j = M1 * (j,i) by A6, A8, A13, MATRIX_1:def_8 .= (Col (M1,i)) . j by A11, MATRIX_1:def_8 .= ((Col (M1,i)) ^ (Col (M2,i))) . j by A10, FINSEQ_1:def_7 ; ::_thesis: verum end; suppose ex n being Nat st ( n in dom (Col (M2,i)) & j = (len (Col (M1,i))) + n ) ; ::_thesis: (Col ((M1 ^ M2),i)) . j = ((Col (M1,i)) ^ (Col (M2,i))) . j then consider n being Nat such that A14: n in dom (Col (M2,i)) and A15: j = (len (Col (M1,i))) + n ; n in Seg (len (Col (M2,i))) by A14, FINSEQ_1:def_3; then n in Seg (len M2) by MATRIX_1:def_8; then A16: n in dom M2 by FINSEQ_1:def_3; then [n,i] in [:(dom M2),(Seg (width M2)):] by A1, A2, ZFMISC_1:87; then [n,i] in Indices M2 by MATRIX_1:def_4; then consider P2 being FinSequence of D such that A17: P2 = M2 . n and A18: M2 * (n,i) = P2 . i by MATRIX_1:def_5; len (Col (M2,i)) = len M2 by MATRIX_1:def_8; then ( len (Col (M1,i)) = len M1 & dom (Col (M2,i)) = dom M2 ) by FINSEQ_3:29, MATRIX_1:def_8; then P = P2 by A7, A14, A15, A17, FINSEQ_1:def_7; hence (Col ((M1 ^ M2),i)) . j = M2 * (n,i) by A6, A8, A18, MATRIX_1:def_8 .= (Col (M2,i)) . n by A16, MATRIX_1:def_8 .= ((Col (M1,i)) ^ (Col (M2,i))) . j by A14, A15, FINSEQ_1:def_7 ; ::_thesis: verum end; end; end; hence (Col ((M1 ^ M2),i)) . j = ((Col (M1,i)) ^ (Col (M2,i))) . j ; ::_thesis: verum end; hence Col ((M1 ^ M2),i) = (Col (M1,i)) ^ (Col (M2,i)) by A4, FINSEQ_2:9; ::_thesis: verum end; theorem Th27: :: MATRLIN:27 for n, k, m being Nat for K being Field for V being VectSp of K for M1 being Matrix of n,k, the carrier of V for M2 being Matrix of m,k, the carrier of V holds Sum (M1 ^ M2) = (Sum M1) ^ (Sum M2) proof let n, k, m be Nat; ::_thesis: for K being Field for V being VectSp of K for M1 being Matrix of n,k, the carrier of V for M2 being Matrix of m,k, the carrier of V holds Sum (M1 ^ M2) = (Sum M1) ^ (Sum M2) let K be Field; ::_thesis: for V being VectSp of K for M1 being Matrix of n,k, the carrier of V for M2 being Matrix of m,k, the carrier of V holds Sum (M1 ^ M2) = (Sum M1) ^ (Sum M2) let V be VectSp of K; ::_thesis: for M1 being Matrix of n,k, the carrier of V for M2 being Matrix of m,k, the carrier of V holds Sum (M1 ^ M2) = (Sum M1) ^ (Sum M2) let M1 be Matrix of n,k, the carrier of V; ::_thesis: for M2 being Matrix of m,k, the carrier of V holds Sum (M1 ^ M2) = (Sum M1) ^ (Sum M2) let M2 be Matrix of m,k, the carrier of V; ::_thesis: Sum (M1 ^ M2) = (Sum M1) ^ (Sum M2) A1: dom (Sum (M1 ^ M2)) = Seg (len (Sum (M1 ^ M2))) by FINSEQ_1:def_3; A2: now__::_thesis:_for_i_being_Nat_st_i_in_dom_(Sum_(M1_^_M2))_holds_ (Sum_(M1_^_M2))_._i_=_((Sum_M1)_^_(Sum_M2))_._i let i be Nat; ::_thesis: ( i in dom (Sum (M1 ^ M2)) implies (Sum (M1 ^ M2)) . i = ((Sum M1) ^ (Sum M2)) . i ) assume A3: i in dom (Sum (M1 ^ M2)) ; ::_thesis: (Sum (M1 ^ M2)) . i = ((Sum M1) ^ (Sum M2)) . i then i in Seg (len (M1 ^ M2)) by A1, Def6; then A4: i in dom (M1 ^ M2) by FINSEQ_1:def_3; now__::_thesis:_(Sum_(M1_^_M2))_._i_=_((Sum_M1)_^_(Sum_M2))_._i percases ( i in dom M1 or ex n being Nat st ( n in dom M2 & i = (len M1) + n ) ) by A4, FINSEQ_1:25; supposeA5: i in dom M1 ; ::_thesis: (Sum (M1 ^ M2)) . i = ((Sum M1) ^ (Sum M2)) . i len M1 = len (Sum M1) by Def6; then A6: dom M1 = dom (Sum M1) by FINSEQ_3:29; thus (Sum (M1 ^ M2)) . i = (Sum (M1 ^ M2)) /. i by A3, PARTFUN1:def_6 .= Sum ((M1 ^ M2) /. i) by A3, Def6 .= Sum (M1 /. i) by A5, FINSEQ_4:68 .= (Sum M1) /. i by A5, A6, Def6 .= (Sum M1) . i by A5, A6, PARTFUN1:def_6 .= ((Sum M1) ^ (Sum M2)) . i by A5, A6, FINSEQ_1:def_7 ; ::_thesis: verum end; supposeA7: ex n being Nat st ( n in dom M2 & i = (len M1) + n ) ; ::_thesis: (Sum (M1 ^ M2)) . i = ((Sum M1) ^ (Sum M2)) . i A8: len M1 = len (Sum M1) by Def6; len M2 = len (Sum M2) by Def6; then A9: dom M2 = dom (Sum M2) by FINSEQ_3:29; consider n being Nat such that A10: n in dom M2 and A11: i = (len M1) + n by A7; thus (Sum (M1 ^ M2)) . i = (Sum (M1 ^ M2)) /. i by A3, PARTFUN1:def_6 .= Sum ((M1 ^ M2) /. i) by A3, Def6 .= Sum (M2 /. n) by A10, A11, FINSEQ_4:69 .= (Sum M2) /. n by A10, A9, Def6 .= (Sum M2) . n by A10, A9, PARTFUN1:def_6 .= ((Sum M1) ^ (Sum M2)) . i by A10, A11, A8, A9, FINSEQ_1:def_7 ; ::_thesis: verum end; end; end; hence (Sum (M1 ^ M2)) . i = ((Sum M1) ^ (Sum M2)) . i ; ::_thesis: verum end; len (Sum (M1 ^ M2)) = len (M1 ^ M2) by Def6 .= (len M1) + (len M2) by FINSEQ_1:22 .= (len (Sum M1)) + (len M2) by Def6 .= (len (Sum M1)) + (len (Sum M2)) by Def6 .= len ((Sum M1) ^ (Sum M2)) by FINSEQ_1:22 ; hence Sum (M1 ^ M2) = (Sum M1) ^ (Sum M2) by A2, FINSEQ_2:9; ::_thesis: verum end; theorem Th28: :: MATRLIN:28 for n, k, m being Nat for D being non empty set for M1 being Matrix of n,k,D for M2 being Matrix of m,k,D st width M1 = width M2 holds (M1 ^ M2) @ = (M1 @) ^^ (M2 @) proof let n, k, m be Nat; ::_thesis: for D being non empty set for M1 being Matrix of n,k,D for M2 being Matrix of m,k,D st width M1 = width M2 holds (M1 ^ M2) @ = (M1 @) ^^ (M2 @) let D be non empty set ; ::_thesis: for M1 being Matrix of n,k,D for M2 being Matrix of m,k,D st width M1 = width M2 holds (M1 ^ M2) @ = (M1 @) ^^ (M2 @) let M1 be Matrix of n,k,D; ::_thesis: for M2 being Matrix of m,k,D st width M1 = width M2 holds (M1 ^ M2) @ = (M1 @) ^^ (M2 @) let M2 be Matrix of m,k,D; ::_thesis: ( width M1 = width M2 implies (M1 ^ M2) @ = (M1 @) ^^ (M2 @) ) assume A1: width M1 = width M2 ; ::_thesis: (M1 ^ M2) @ = (M1 @) ^^ (M2 @) A2: Seg (len ((M1 @) ^^ (M2 @))) = dom ((M1 @) ^^ (M2 @)) by FINSEQ_1:def_3 .= (dom (M1 @)) /\ (dom (M2 @)) by PRE_POLY:def_4 .= (dom (M1 @)) /\ (Seg (len (M2 @))) by FINSEQ_1:def_3 .= (Seg (len (M1 @))) /\ (Seg (len (M2 @))) by FINSEQ_1:def_3 .= (Seg (width M1)) /\ (Seg (len (M2 @))) by MATRIX_1:def_6 .= (Seg (width M1)) /\ (Seg (width M2)) by MATRIX_1:def_6 .= Seg (width M1) by A1 ; A3: dom ((M1 ^ M2) @) = Seg (len ((M1 ^ M2) @)) by FINSEQ_1:def_3; A4: len ((M1 ^ M2) @) = width (M1 ^ M2) by MATRIX_1:def_6 .= width M1 by A1, Th24 .= len ((M1 @) ^^ (M2 @)) by A2, FINSEQ_1:6 ; now__::_thesis:_for_i_being_Nat_st_i_in_dom_((M1_^_M2)_@)_holds_ ((M1_^_M2)_@)_._i_=_((M1_@)_^^_(M2_@))_._i let i be Nat; ::_thesis: ( i in dom ((M1 ^ M2) @) implies ((M1 ^ M2) @) . i = ((M1 @) ^^ (M2 @)) . i ) assume A5: i in dom ((M1 ^ M2) @) ; ::_thesis: ((M1 ^ M2) @) . i = ((M1 @) ^^ (M2 @)) . i then A6: i in Seg (width (M1 ^ M2)) by A3, MATRIX_1:def_6; A7: i in dom ((M1 @) ^^ (M2 @)) by A4, A3, A5, FINSEQ_1:def_3; then A8: i in (dom (M1 @)) /\ (dom (M2 @)) by PRE_POLY:def_4; then A9: i in dom (M2 @) by XBOOLE_0:def_4; A10: i in dom (M1 @) by A8, XBOOLE_0:def_4; reconsider m1 = (M1 @) . i, m2 = (M2 @) . i as FinSequence ; i in (Seg (len (M1 @))) /\ (dom (M2 @)) by A8, FINSEQ_1:def_3; then i in (Seg (len (M1 @))) /\ (Seg (len (M2 @))) by FINSEQ_1:def_3; then i in (Seg (width M1)) /\ (Seg (len (M2 @))) by MATRIX_1:def_6; then A11: i in (Seg (width M1)) /\ (Seg (width M2)) by MATRIX_1:def_6; thus ((M1 ^ M2) @) . i = Line (((M1 ^ M2) @),i) by A5, MATRIX_2:16 .= Col ((M1 ^ M2),i) by A6, MATRIX_2:15 .= (Col (M1,i)) ^ (Col (M2,i)) by A1, A11, Th26 .= (Line ((M1 @),i)) ^ (Col (M2,i)) by A1, A11, MATRIX_2:15 .= (Line ((M1 @),i)) ^ (Line ((M2 @),i)) by A1, A11, MATRIX_2:15 .= (Line ((M1 @),i)) ^ m2 by A9, MATRIX_2:16 .= m1 ^ m2 by A10, MATRIX_2:16 .= ((M1 @) ^^ (M2 @)) . i by A7, PRE_POLY:def_4 ; ::_thesis: verum end; hence (M1 ^ M2) @ = (M1 @) ^^ (M2 @) by A4, FINSEQ_2:9; ::_thesis: verum end; theorem Th29: :: MATRLIN:29 for K being Field for V1 being finite-dimensional VectSp of K for M1, M2 being Matrix of the carrier of V1 holds (Sum M1) + (Sum M2) = Sum (M1 ^^ M2) proof let K be Field; ::_thesis: for V1 being finite-dimensional VectSp of K for M1, M2 being Matrix of the carrier of V1 holds (Sum M1) + (Sum M2) = Sum (M1 ^^ M2) let V1 be finite-dimensional VectSp of K; ::_thesis: for M1, M2 being Matrix of the carrier of V1 holds (Sum M1) + (Sum M2) = Sum (M1 ^^ M2) let M1, M2 be Matrix of the carrier of V1; ::_thesis: (Sum M1) + (Sum M2) = Sum (M1 ^^ M2) reconsider m = min ((len M1),(len M2)) as Element of NAT by FINSEQ_2:1; A1: Seg m = (Seg (len M1)) /\ (Seg (len M2)) by FINSEQ_2:2 .= (Seg (len M1)) /\ (dom M2) by FINSEQ_1:def_3 .= (dom M1) /\ (dom M2) by FINSEQ_1:def_3 .= dom (M1 ^^ M2) by PRE_POLY:def_4 .= Seg (len (M1 ^^ M2)) by FINSEQ_1:def_3 ; A2: len ((Sum M1) + (Sum M2)) = min ((len (Sum M1)),(len (Sum M2))) by FINSEQ_2:71 .= min ((len M1),(len (Sum M2))) by Def6 .= min ((len M1),(len M2)) by Def6 .= len (M1 ^^ M2) by A1, FINSEQ_1:6 .= len (Sum (M1 ^^ M2)) by Def6 ; A3: dom ((Sum M1) + (Sum M2)) = Seg (len ((Sum M1) + (Sum M2))) by FINSEQ_1:def_3; now__::_thesis:_for_i_being_Nat_st_i_in_dom_((Sum_M1)_+_(Sum_M2))_holds_ ((Sum_M1)_+_(Sum_M2))_._i_=_(Sum_(M1_^^_M2))_._i let i be Nat; ::_thesis: ( i in dom ((Sum M1) + (Sum M2)) implies ((Sum M1) + (Sum M2)) . i = (Sum (M1 ^^ M2)) . i ) assume A4: i in dom ((Sum M1) + (Sum M2)) ; ::_thesis: ((Sum M1) + (Sum M2)) . i = (Sum (M1 ^^ M2)) . i then A5: i in dom (Sum (M1 ^^ M2)) by A2, A3, FINSEQ_1:def_3; i in Seg (len (M1 ^^ M2)) by A2, A3, A4, Def6; then A6: i in dom (M1 ^^ M2) by FINSEQ_1:def_3; then A7: i in (dom M1) /\ (dom M2) by PRE_POLY:def_4; then A8: i in dom M1 by XBOOLE_0:def_4; A9: i in dom M2 by A7, XBOOLE_0:def_4; reconsider m1 = M1 . i, m2 = M2 . i as FinSequence ; A10: (M1 /. i) ^ (M2 /. i) = m1 ^ (M2 /. i) by A8, PARTFUN1:def_6 .= m1 ^ m2 by A9, PARTFUN1:def_6 .= (M1 ^^ M2) . i by A6, PRE_POLY:def_4 .= (M1 ^^ M2) /. i by A6, PARTFUN1:def_6 ; i in Seg (len M2) by A9, FINSEQ_1:def_3; then i in Seg (len (Sum M2)) by Def6; then A11: i in dom (Sum M2) by FINSEQ_1:def_3; then A12: (Sum M2) /. i = (Sum M2) . i by PARTFUN1:def_6; i in Seg (len M1) by A8, FINSEQ_1:def_3; then i in Seg (len (Sum M1)) by Def6; then A13: i in dom (Sum M1) by FINSEQ_1:def_3; then (Sum M1) /. i = (Sum M1) . i by PARTFUN1:def_6; hence ((Sum M1) + (Sum M2)) . i = ((Sum M1) /. i) + ((Sum M2) /. i) by A4, A12, FUNCOP_1:22 .= (Sum (M1 /. i)) + ((Sum M2) /. i) by A13, Def6 .= (Sum (M1 /. i)) + (Sum (M2 /. i)) by A11, Def6 .= Sum ((M1 ^^ M2) /. i) by A10, RLVECT_1:41 .= (Sum (M1 ^^ M2)) /. i by A5, Def6 .= (Sum (M1 ^^ M2)) . i by A5, PARTFUN1:def_6 ; ::_thesis: verum end; hence (Sum M1) + (Sum M2) = Sum (M1 ^^ M2) by A2, FINSEQ_2:9; ::_thesis: verum end; theorem Th30: :: MATRLIN:30 for K being Field for V1 being finite-dimensional VectSp of K for P1, P2 being FinSequence of V1 st len P1 = len P2 holds Sum (P1 + P2) = (Sum P1) + (Sum P2) proof let K be Field; ::_thesis: for V1 being finite-dimensional VectSp of K for P1, P2 being FinSequence of V1 st len P1 = len P2 holds Sum (P1 + P2) = (Sum P1) + (Sum P2) let V1 be finite-dimensional VectSp of K; ::_thesis: for P1, P2 being FinSequence of V1 st len P1 = len P2 holds Sum (P1 + P2) = (Sum P1) + (Sum P2) let P1, P2 be FinSequence of V1; ::_thesis: ( len P1 = len P2 implies Sum (P1 + P2) = (Sum P1) + (Sum P2) ) assume len P1 = len P2 ; ::_thesis: Sum (P1 + P2) = (Sum P1) + (Sum P2) then reconsider R1 = P1, R2 = P2 as Element of (len P1) -tuples_on the carrier of V1 by FINSEQ_2:92; thus Sum (P1 + P2) = Sum (R1 + R2) .= (Sum P1) + (Sum P2) by FVSUM_1:76 ; ::_thesis: verum end; theorem Th31: :: MATRLIN:31 for K being Field for V1 being finite-dimensional VectSp of K for M1, M2 being Matrix of the carrier of V1 st len M1 = len M2 holds (Sum (Sum M1)) + (Sum (Sum M2)) = Sum (Sum (M1 ^^ M2)) proof let K be Field; ::_thesis: for V1 being finite-dimensional VectSp of K for M1, M2 being Matrix of the carrier of V1 st len M1 = len M2 holds (Sum (Sum M1)) + (Sum (Sum M2)) = Sum (Sum (M1 ^^ M2)) let V1 be finite-dimensional VectSp of K; ::_thesis: for M1, M2 being Matrix of the carrier of V1 st len M1 = len M2 holds (Sum (Sum M1)) + (Sum (Sum M2)) = Sum (Sum (M1 ^^ M2)) let M1, M2 be Matrix of the carrier of V1; ::_thesis: ( len M1 = len M2 implies (Sum (Sum M1)) + (Sum (Sum M2)) = Sum (Sum (M1 ^^ M2)) ) assume A1: len M1 = len M2 ; ::_thesis: (Sum (Sum M1)) + (Sum (Sum M2)) = Sum (Sum (M1 ^^ M2)) len (Sum M1) = len M1 by Def6 .= len (Sum M2) by A1, Def6 ; hence (Sum (Sum M1)) + (Sum (Sum M2)) = Sum ((Sum M1) + (Sum M2)) by Th30 .= Sum (Sum (M1 ^^ M2)) by Th29 ; ::_thesis: verum end; theorem Th32: :: MATRLIN:32 for K being Field for V1 being finite-dimensional VectSp of K for M being Matrix of the carrier of V1 holds Sum (Sum M) = Sum (Sum (M @)) proof let K be Field; ::_thesis: for V1 being finite-dimensional VectSp of K for M being Matrix of the carrier of V1 holds Sum (Sum M) = Sum (Sum (M @)) let V1 be finite-dimensional VectSp of K; ::_thesis: for M being Matrix of the carrier of V1 holds Sum (Sum M) = Sum (Sum (M @)) defpred S1[ Nat] means for M being Matrix of the carrier of V1 st len M = $1 holds Sum (Sum M) = Sum (Sum (M @)); let M be Matrix of the carrier of V1; ::_thesis: Sum (Sum M) = Sum (Sum (M @)) A1: for P being FinSequence of V1 holds Sum (Sum <*P*>) = Sum (Sum (<*P*> @)) proof defpred S2[ FinSequence of V1] means Sum (Sum <*$1*>) = Sum (Sum (<*$1*> @)); let P be FinSequence of V1; ::_thesis: Sum (Sum <*P*>) = Sum (Sum (<*P*> @)) len <*(<*> the carrier of V1)*> = 1 by MATRIX_1:def_2; then width <*(<*> the carrier of V1)*> = 0 by MATRIX_1:20; then A2: len (<*(<*> the carrier of V1)*> @) = 0 by MATRIX_1:def_6; A3: for P being FinSequence of V1 for x being Element of V1 st S2[P] holds S2[P ^ <*x*>] proof let P be FinSequence of V1; ::_thesis: for x being Element of V1 st S2[P] holds S2[P ^ <*x*>] let x be Element of V1; ::_thesis: ( S2[P] implies S2[P ^ <*x*>] ) assume A4: Sum (Sum <*P*>) = Sum (Sum (<*P*> @)) ; ::_thesis: S2[P ^ <*x*>] Seg (len (<*P*> ^^ <*<*x*>*>)) = dom (<*P*> ^^ <*<*x*>*>) by FINSEQ_1:def_3 .= (dom <*P*>) /\ (dom <*<*x*>*>) by PRE_POLY:def_4 .= (Seg 1) /\ (dom <*<*x*>*>) by FINSEQ_1:38 .= (Seg 1) /\ (Seg 1) by FINSEQ_1:38 .= Seg 1 ; then A5: len (<*P*> ^^ <*<*x*>*>) = 1 by FINSEQ_1:6 .= len <*(P ^ <*x*>)*> by FINSEQ_1:39 ; then A6: dom (<*P*> ^^ <*<*x*>*>) = Seg (len <*(P ^ <*x*>)*>) by FINSEQ_1:def_3; A7: now__::_thesis:_for_i_being_Nat_st_i_in_dom_(<*P*>_^^_<*<*x*>*>)_holds_ (<*P*>_^^_<*<*x*>*>)_._i_=_<*(P_^_<*x*>)*>_._i let i be Nat; ::_thesis: ( i in dom (<*P*> ^^ <*<*x*>*>) implies (<*P*> ^^ <*<*x*>*>) . i = <*(P ^ <*x*>)*> . i ) assume A8: i in dom (<*P*> ^^ <*<*x*>*>) ; ::_thesis: (<*P*> ^^ <*<*x*>*>) . i = <*(P ^ <*x*>)*> . i then i in {1} by A6, FINSEQ_1:2, FINSEQ_1:40; then A9: i = 1 by TARSKI:def_1; reconsider m1 = <*P*> . i, m2 = <*<*x*>*> . i as FinSequence ; thus (<*P*> ^^ <*<*x*>*>) . i = m1 ^ m2 by A8, PRE_POLY:def_4 .= P ^ m2 by A9, FINSEQ_1:40 .= P ^ <*x*> by A9, FINSEQ_1:40 .= <*(P ^ <*x*>)*> . i by A9, FINSEQ_1:40 ; ::_thesis: verum end; percases ( len P = 0 or len P <> 0 ) ; suppose len P = 0 ; ::_thesis: S2[P ^ <*x*>] then A10: P = {} ; hence Sum (Sum <*(P ^ <*x*>)*>) = Sum (Sum <*<*x*>*>) by FINSEQ_1:34 .= Sum (Sum (<*<*x*>*> @)) by Th15 .= Sum (Sum (<*(P ^ <*x*>)*> @)) by A10, FINSEQ_1:34 ; ::_thesis: verum end; supposeA11: len P <> 0 ; ::_thesis: S2[P ^ <*x*>] A12: len <*<*x*>*> = 1 by FINSEQ_1:40; then A13: width <*<*x*>*> = len <*x*> by MATRIX_1:20 .= 1 by FINSEQ_1:40 ; then A14: len (<*<*x*>*> @) = 1 by MATRIX_1:def_6; A15: len <*P*> = 1 by FINSEQ_1:40; then A16: width <*P*> = len P by MATRIX_1:20; then A17: len (<*P*> @) = len P by MATRIX_1:def_6; width (<*P*> @) = 1 by A11, A15, A16, MATRIX_2:10; then reconsider d1 = <*P*> @ as Matrix of len P,1, the carrier of V1 by A11, A17, MATRIX_1:20; A18: len <*(P ^ <*x*>)*> = 1 by FINSEQ_1:40; then A19: width <*(P ^ <*x*>)*> = len (P ^ <*x*>) by MATRIX_1:20 .= (len P) + (len <*x*>) by FINSEQ_1:22 .= (len P) + 1 by FINSEQ_1:40 ; A20: (<*<*x*>*> @) @ = <*<*x*>*> by A12, A13, MATRIX_2:13; A21: width (<*P*> @) = len <*P*> by A11, A16, MATRIX_2:10 .= width (<*<*x*>*> @) by A15, A12, A13, MATRIX_2:10 ; then width (<*<*x*>*> @) = 1 by A11, A15, A16, MATRIX_2:10; then reconsider d2 = <*<*x*>*> @ as Matrix of 1,1, the carrier of V1 by A14, MATRIX_1:20; A22: (d1 ^ d2) @ = ((<*P*> @) @) ^^ ((<*<*x*>*> @) @) by A21, Th28 .= <*P*> ^^ <*<*x*>*> by A11, A15, A16, A20, MATRIX_2:13 .= <*(P ^ <*x*>)*> by A5, A7, FINSEQ_2:9 .= (<*(P ^ <*x*>)*> @) @ by A18, A19, MATRIX_2:13 ; A23: len ((<*P*> @) ^ (<*<*x*>*> @)) = (len (<*P*> @)) + (len (<*<*x*>*> @)) by FINSEQ_1:22 .= (width <*P*>) + (len (<*<*x*>*> @)) by MATRIX_1:def_6 .= (width <*P*>) + (width <*<*x*>*>) by MATRIX_1:def_6 .= len (<*(P ^ <*x*>)*> @) by A16, A13, A19, MATRIX_1:def_6 ; thus Sum (Sum <*(P ^ <*x*>)*>) = Sum (Sum (<*P*> ^^ <*<*x*>*>)) by A5, A7, FINSEQ_2:9 .= (Sum (Sum (<*P*> @))) + (Sum (Sum <*<*x*>*>)) by A4, A15, A12, Th31 .= (Sum (Sum (<*P*> @))) + (Sum (Sum (<*<*x*>*> @))) by Th15 .= Sum ((Sum d1) ^ (Sum d2)) by RLVECT_1:41 .= Sum (Sum (d1 ^ d2)) by Th27 .= Sum (Sum (<*(P ^ <*x*>)*> @)) by A23, A22, MATRIX_2:9 ; ::_thesis: verum end; end; end; <*(<*> the carrier of V1)*> is Matrix of 0 + 1, 0 , the carrier of V1 ; then Sum (Sum <*(<*> the carrier of V1)*>) = 0. V1 by Th14 .= Sum (Sum (<*(<*> the carrier of V1)*> @)) by A2, Th13 ; then A24: S2[ <*> the carrier of V1] ; for P being FinSequence of V1 holds S2[P] from FINSEQ_2:sch_2(A24, A3); hence Sum (Sum <*P*>) = Sum (Sum (<*P*> @)) ; ::_thesis: verum end; A25: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A26: for M being Matrix of the carrier of V1 st len M = n holds Sum (Sum M) = Sum (Sum (M @)) ; ::_thesis: S1[n + 1] thus for M being Matrix of the carrier of V1 st len M = n + 1 holds Sum (Sum M) = Sum (Sum (M @)) ::_thesis: verum proof let M be Matrix of the carrier of V1; ::_thesis: ( len M = n + 1 implies Sum (Sum M) = Sum (Sum (M @)) ) assume A27: len M = n + 1 ; ::_thesis: Sum (Sum M) = Sum (Sum (M @)) A28: M <> {} by A27; A29: dom M = Seg (len M) by FINSEQ_1:def_3; percases ( n = 0 or n > 0 ) ; supposeA30: n = 0 ; ::_thesis: Sum (Sum M) = Sum (Sum (M @)) then M . 1 = Line (M,1) by A27, A29, FINSEQ_1:4, MATRIX_2:16; then reconsider G = M . 1 as FinSequence of V1 ; M = <*G*> by A27, A30, FINSEQ_1:40; hence Sum (Sum M) = Sum (Sum (M @)) by A1; ::_thesis: verum end; supposeA31: n > 0 ; ::_thesis: Sum (Sum M) = Sum (Sum (M @)) A32: M . (n + 1) = Line (M,(n + 1)) by A27, A29, FINSEQ_1:4, MATRIX_2:16; then reconsider M1 = M . (n + 1) as FinSequence of V1 ; reconsider R = <*M1*> as Matrix of 1, width M, the carrier of V1 by A32, MATRIX_1:def_7; reconsider M9 = M as Matrix of n + 1, width M, the carrier of V1 by A27, MATRIX_1:20; reconsider W = Del (M9,(n + 1)) as Matrix of n, width M, the carrier of V1 by Th3; A33: width W = width M9 by A31, Th2 .= width R by Th2 ; A34: len (W @) = width W by MATRIX_1:def_6 .= len (R @) by A33, MATRIX_1:def_6 ; A35: len (Del (M,(n + 1))) = n by A27, Th1; thus Sum (Sum M) = Sum (Sum (W ^ R)) by A28, Th4, A27 .= Sum ((Sum W) ^ (Sum R)) by Th27 .= (Sum (Sum (Del (M,(n + 1))))) + (Sum (Sum R)) by RLVECT_1:41 .= (Sum (Sum ((Del (M,(n + 1))) @))) + (Sum (Sum R)) by A26, A35 .= (Sum (Sum ((Del (M,(n + 1))) @))) + (Sum (Sum (R @))) by A1 .= Sum (Sum ((W @) ^^ (R @))) by A34, Th31 .= Sum (Sum ((W ^ R) @)) by A33, Th28 .= Sum (Sum (M @)) by A28, Th4, A27 ; ::_thesis: verum end; end; end; end; A36: S1[ 0 ] proof let M be Matrix of the carrier of V1; ::_thesis: ( len M = 0 implies Sum (Sum M) = Sum (Sum (M @)) ) assume A37: len M = 0 ; ::_thesis: Sum (Sum M) = Sum (Sum (M @)) then width M = 0 by MATRIX_1:def_3; then A38: len (M @) = 0 by MATRIX_1:def_6; thus Sum (Sum M) = 0. V1 by A37, Th13 .= Sum (Sum (M @)) by A38, Th13 ; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A36, A25); then S1[ len M] ; hence Sum (Sum M) = Sum (Sum (M @)) ; ::_thesis: verum end; theorem Th33: :: MATRLIN:33 for n, m being Nat for K being Field for V1 being finite-dimensional VectSp of K for M being Matrix of n,m, the carrier of K st n > 0 & m > 0 holds for p, d being FinSequence of K st len p = n & len d = m & ( for j being Nat st j in dom d holds d /. j = Sum (mlt (p,(Col (M,j)))) ) holds for b, c being FinSequence of V1 st len b = m & len c = n & ( for i being Nat st i in dom c holds c /. i = Sum (lmlt ((Line (M,i)),b)) ) holds Sum (lmlt (p,c)) = Sum (lmlt (d,b)) proof let n, m be Nat; ::_thesis: for K being Field for V1 being finite-dimensional VectSp of K for M being Matrix of n,m, the carrier of K st n > 0 & m > 0 holds for p, d being FinSequence of K st len p = n & len d = m & ( for j being Nat st j in dom d holds d /. j = Sum (mlt (p,(Col (M,j)))) ) holds for b, c being FinSequence of V1 st len b = m & len c = n & ( for i being Nat st i in dom c holds c /. i = Sum (lmlt ((Line (M,i)),b)) ) holds Sum (lmlt (p,c)) = Sum (lmlt (d,b)) let K be Field; ::_thesis: for V1 being finite-dimensional VectSp of K for M being Matrix of n,m, the carrier of K st n > 0 & m > 0 holds for p, d being FinSequence of K st len p = n & len d = m & ( for j being Nat st j in dom d holds d /. j = Sum (mlt (p,(Col (M,j)))) ) holds for b, c being FinSequence of V1 st len b = m & len c = n & ( for i being Nat st i in dom c holds c /. i = Sum (lmlt ((Line (M,i)),b)) ) holds Sum (lmlt (p,c)) = Sum (lmlt (d,b)) let V1 be finite-dimensional VectSp of K; ::_thesis: for M being Matrix of n,m, the carrier of K st n > 0 & m > 0 holds for p, d being FinSequence of K st len p = n & len d = m & ( for j being Nat st j in dom d holds d /. j = Sum (mlt (p,(Col (M,j)))) ) holds for b, c being FinSequence of V1 st len b = m & len c = n & ( for i being Nat st i in dom c holds c /. i = Sum (lmlt ((Line (M,i)),b)) ) holds Sum (lmlt (p,c)) = Sum (lmlt (d,b)) let M be Matrix of n,m, the carrier of K; ::_thesis: ( n > 0 & m > 0 implies for p, d being FinSequence of K st len p = n & len d = m & ( for j being Nat st j in dom d holds d /. j = Sum (mlt (p,(Col (M,j)))) ) holds for b, c being FinSequence of V1 st len b = m & len c = n & ( for i being Nat st i in dom c holds c /. i = Sum (lmlt ((Line (M,i)),b)) ) holds Sum (lmlt (p,c)) = Sum (lmlt (d,b)) ) assume that A1: n > 0 and A2: m > 0 ; ::_thesis: for p, d being FinSequence of K st len p = n & len d = m & ( for j being Nat st j in dom d holds d /. j = Sum (mlt (p,(Col (M,j)))) ) holds for b, c being FinSequence of V1 st len b = m & len c = n & ( for i being Nat st i in dom c holds c /. i = Sum (lmlt ((Line (M,i)),b)) ) holds Sum (lmlt (p,c)) = Sum (lmlt (d,b)) A3: len M = n by A1, MATRIX_1:23; reconsider n1 = n, m1 = m as Element of NAT by ORDINAL1:def_12; let p, d be FinSequence of K; ::_thesis: ( len p = n & len d = m & ( for j being Nat st j in dom d holds d /. j = Sum (mlt (p,(Col (M,j)))) ) implies for b, c being FinSequence of V1 st len b = m & len c = n & ( for i being Nat st i in dom c holds c /. i = Sum (lmlt ((Line (M,i)),b)) ) holds Sum (lmlt (p,c)) = Sum (lmlt (d,b)) ) assume that A4: len p = n and A5: len d = m and A6: for j being Nat st j in dom d holds d /. j = Sum (mlt (p,(Col (M,j)))) ; ::_thesis: for b, c being FinSequence of V1 st len b = m & len c = n & ( for i being Nat st i in dom c holds c /. i = Sum (lmlt ((Line (M,i)),b)) ) holds Sum (lmlt (p,c)) = Sum (lmlt (d,b)) let b, c be FinSequence of V1; ::_thesis: ( len b = m & len c = n & ( for i being Nat st i in dom c holds c /. i = Sum (lmlt ((Line (M,i)),b)) ) implies Sum (lmlt (p,c)) = Sum (lmlt (d,b)) ) assume that A7: len b = m and A8: len c = n and A9: for i being Nat st i in dom c holds c /. i = Sum (lmlt ((Line (M,i)),b)) ; ::_thesis: Sum (lmlt (p,c)) = Sum (lmlt (d,b)) deffunc H1( Nat, Nat) -> Element of the carrier of V1 = ((p /. $1) * (M * ($1,$2))) * (b /. $2); consider M1 being Matrix of n1,m1, the carrier of V1 such that A10: for i, j being Nat st [i,j] in Indices M1 holds M1 * (i,j) = H1(i,j) from MATRIX_1:sch_1(); A11: width M1 = len (M1 @) by MATRIX_1:def_6 .= len (Sum (M1 @)) by Def6 ; A12: dom d = dom b by A5, A7, FINSEQ_3:29; then A13: dom (lmlt (d,b)) = dom b by Th12; then A14: len (lmlt (d,b)) = len b by FINSEQ_3:29 .= len (Sum (M1 @)) by A1, A7, A11, MATRIX_1:23 ; then A15: dom (lmlt (d,b)) = Seg (len (Sum (M1 @))) by FINSEQ_1:def_3; A16: width M1 = m by A1, MATRIX_1:23; A17: len M1 = n by A1, MATRIX_1:23; A18: dom (lmlt (d,b)) = dom d by A12, Th12; A19: now__::_thesis:_for_j_being_Nat_st_j_in_dom_(lmlt_(d,b))_holds_ (lmlt_(d,b))_._j_=_(Sum_(M1_@))_._j A20: Seg (len (Sum (M1 @))) = dom (Sum (M1 @)) by FINSEQ_1:def_3; let j be Nat; ::_thesis: ( j in dom (lmlt (d,b)) implies (lmlt (d,b)) . j = (Sum (M1 @)) . j ) assume A21: j in dom (lmlt (d,b)) ; ::_thesis: (lmlt (d,b)) . j = (Sum (M1 @)) . j A22: j in dom (Sum (M1 @)) by A15, A21, FINSEQ_1:def_3; A23: j in dom d by A12, A21, Th12; A24: ( d /. j = d . j & b /. j = b . j ) by A18, A13, A21, PARTFUN1:def_6; len (Sum (M1 @)) = len (M1 @) by Def6; then A25: dom (Sum (M1 @)) = dom (M1 @) by FINSEQ_3:29; then A26: (M1 @) /. j = (M1 @) . j by A22, PARTFUN1:def_6 .= Line ((M1 @),j) by A22, A25, MATRIX_2:16 ; reconsider H = mlt (p,(Col (M,j))) as FinSequence of K ; deffunc H2( Nat) -> Element of the carrier of V1 = (H /. $1) * (b /. j); consider G being FinSequence of V1 such that A27: ( len G = len p & ( for i being Nat st i in dom G holds G . i = H2(i) ) ) from FINSEQ_2:sch_1(); A28: len p = len (Col (M,j)) by A4, A3, MATRIX_1:def_8; then A29: len ( the multF of K .: (p,(Col (M,j)))) = len p by FINSEQ_2:72; then A30: dom H = dom G by A27, FINSEQ_3:29; A31: dom p = dom G by A27, FINSEQ_3:29; A32: len (Line ((M1 @),j)) = width (M1 @) by MATRIX_1:def_7 .= len ((M1 @) @) by MATRIX_1:def_6 .= len G by A1, A2, A4, A17, A16, A27, MATRIX_2:13 ; then A33: dom (Line ((M1 @),j)) = Seg (len G) by FINSEQ_1:def_3; A34: dom G = Seg (len p) by A27, FINSEQ_1:def_3; A35: now__::_thesis:_for_i_being_Nat_st_i_in_dom_(Line_((M1_@),j))_holds_ (Line_((M1_@),j))_._i_=_G_._i let i be Nat; ::_thesis: ( i in dom (Line ((M1 @),j)) implies (Line ((M1 @),j)) . i = G . i ) A36: dom M = Seg (len M) by FINSEQ_1:def_3; assume A37: i in dom (Line ((M1 @),j)) ; ::_thesis: (Line ((M1 @),j)) . i = G . i then A38: i in Seg (len ( the multF of K .: (p,(Col (M,j))))) by A27, A28, A33, FINSEQ_2:72; then A39: i in dom H by FINSEQ_1:def_3; A40: i in dom ( the multF of K .: (p,(Col (M,j)))) by A38, FINSEQ_1:def_3; A41: Seg (len G) = dom G by FINSEQ_1:def_3; then A42: (p /. i) * (M * (i,j)) = the multF of K . ((p . i),(M * (i,j))) by A31, A33, A37, PARTFUN1:def_6 .= the multF of K . ((p . i),((Col (M,j)) . i)) by A4, A3, A27, A33, A37, A36, MATRIX_1:def_8 .= ( the multF of K .: (p,(Col (M,j)))) . i by A40, FUNCOP_1:22 .= H /. i by A39, PARTFUN1:def_6 ; dom M1 = dom G by A4, A17, A27, FINSEQ_3:29; then [i,j] in [:(dom M1),(Seg (width M1)):] by A11, A15, A21, A33, A37, A41, ZFMISC_1:87; then A43: [i,j] in Indices M1 by MATRIX_1:def_4; i in Seg (width (M1 @)) by A32, A33, A37, MATRIX_1:def_7; hence (Line ((M1 @),j)) . i = (M1 @) * (j,i) by MATRIX_1:def_7 .= M1 * (i,j) by A43, MATRIX_1:def_6 .= (H /. i) * (b /. j) by A10, A43, A42 .= G . i by A27, A34, A33, A37 ; ::_thesis: verum end; thus (lmlt (d,b)) . j = the lmult of V1 . ((d . j),(b . j)) by A21, FUNCOP_1:22 .= (d /. j) * (b /. j) by A24, VECTSP_1:def_12 .= (Sum H) * (b /. j) by A6, A23 .= Sum G by A27, A29, A30, Th10 .= Sum ((M1 @) /. j) by A32, A35, A26, FINSEQ_2:9 .= (Sum (M1 @)) /. j by A22, Def6 .= (Sum (M1 @)) . j by A15, A21, A20, PARTFUN1:def_6 ; ::_thesis: verum end; A44: dom p = dom c by A4, A8, FINSEQ_3:29; then A45: dom (lmlt (p,c)) = dom p by Th12; then A46: len (lmlt (p,c)) = len p by FINSEQ_3:29 .= len M1 by A4, MATRIX_1:def_2 .= len (Sum M1) by Def6 ; now__::_thesis:_for_i_being_Nat_st_i_in_dom_(Sum_M1)_holds_ (lmlt_(p,c))_._i_=_(Sum_M1)_._i let i be Nat; ::_thesis: ( i in dom (Sum M1) implies (lmlt (p,c)) . i = (Sum M1) . i ) assume A47: i in dom (Sum M1) ; ::_thesis: (lmlt (p,c)) . i = (Sum M1) . i A48: i in dom c by A44, A45, A46, A47, FINSEQ_3:29; then A49: ( c . i = c /. i & p . i = p /. i ) by A44, PARTFUN1:def_6; i in Seg (len (Sum M1)) by A47, FINSEQ_1:def_3; then i in Seg (len M1) by Def6; then A50: i in dom M1 by FINSEQ_1:def_3; then A51: M1 /. i = M1 . i by PARTFUN1:def_6 .= Line (M1,i) by A50, MATRIX_2:16 ; deffunc H2( Nat) -> Element of the carrier of V1 = (p /. i) * ((lmlt ((Line (M,i)),b)) /. $1); consider F being FinSequence of V1 such that A52: ( len F = len b & ( for j being Nat st j in dom F holds F . j = H2(j) ) ) from FINSEQ_2:sch_1(); A53: len F = width M by A1, A7, A52, MATRIX_1:23; A54: dom (Line (M,i)) = Seg (len (Line (M,i))) by FINSEQ_1:def_3 .= Seg (len F) by A53, MATRIX_1:def_7 .= dom b by A52, FINSEQ_1:def_3 ; then dom (lmlt ((Line (M,i)),b)) = dom b by Th12; then A55: ( len F = len (lmlt ((Line (M,i)),b)) & dom F = dom (lmlt ((Line (M,i)),b)) ) by A52, FINSEQ_3:29; A56: len F = width M1 by A1, A7, A52, MATRIX_1:23; then A57: len (Line (M1,i)) = len F by MATRIX_1:def_7; then A58: dom (M1 /. i) = Seg (len F) by A51, FINSEQ_1:def_3; A59: dom F = Seg (len b) by A52, FINSEQ_1:def_3; A60: now__::_thesis:_for_j_being_Nat_st_j_in_dom_(M1_/._i)_holds_ (M1_/._i)_._j_=_F_._j let j be Nat; ::_thesis: ( j in dom (M1 /. i) implies (M1 /. i) . j = F . j ) assume A61: j in dom (M1 /. i) ; ::_thesis: (M1 /. i) . j = F . j then A62: (Line (M,i)) . j = M * (i,j) by A53, A58, MATRIX_1:def_7; [i,j] in [:(dom M1),(Seg (width M1)):] by A56, A50, A58, A61, ZFMISC_1:87; then A63: [i,j] in Indices M1 by MATRIX_1:def_4; A64: j in dom b by A52, A58, A61, FINSEQ_1:def_3; then A65: b . j = b /. j by PARTFUN1:def_6; A66: j in dom (lmlt ((Line (M,i)),b)) by A54, A64, Th12; then A67: (lmlt ((Line (M,i)),b)) /. j = (lmlt ((Line (M,i)),b)) . j by PARTFUN1:def_6 .= the lmult of V1 . (((Line (M,i)) . j),(b . j)) by A66, FUNCOP_1:22 .= (M * (i,j)) * (b /. j) by A65, A62, VECTSP_1:def_12 ; thus (M1 /. i) . j = M1 * (i,j) by A56, A51, A58, A61, MATRIX_1:def_7 .= ((p /. i) * (M * (i,j))) * (b /. j) by A10, A63 .= (p /. i) * ((lmlt ((Line (M,i)),b)) /. j) by A67, VECTSP_1:def_16 .= F . j by A52, A59, A58, A61 ; ::_thesis: verum end; A68: for j being Element of NAT st j in dom F holds F . j = (p /. i) * ((lmlt ((Line (M,i)),b)) /. j) by A52; i in dom ( the lmult of V1 .: (p,c)) by A46, A47, FINSEQ_3:29; hence (lmlt (p,c)) . i = the lmult of V1 . ((p . i),(c . i)) by FUNCOP_1:22 .= (p /. i) * (c /. i) by A49, VECTSP_1:def_12 .= (p /. i) * (Sum (lmlt ((Line (M,i)),b))) by A9, A48 .= Sum F by A55, A68, RLVECT_2:67 .= Sum (M1 /. i) by A57, A51, A60, FINSEQ_2:9 .= (Sum M1) /. i by A47, Def6 .= (Sum M1) . i by A47, PARTFUN1:def_6 ; ::_thesis: verum end; hence Sum (lmlt (p,c)) = Sum (Sum M1) by A46, FINSEQ_2:9 .= Sum (Sum (M1 @)) by Th32 .= Sum (lmlt (d,b)) by A14, A19, FINSEQ_2:9 ; ::_thesis: verum end; begin definition let K be Field; let V be finite-dimensional VectSp of K; let b1 be OrdBasis of V; let W be Element of V; funcW |-- b1 -> FinSequence of K means :Def7: :: MATRLIN:def 7 ( len it = len b1 & ex KL being Linear_Combination of V st ( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len it holds it /. k = KL . (b1 /. k) ) ) ); existence ex b1 being FinSequence of K st ( len b1 = len b1 & ex KL being Linear_Combination of V st ( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len b1 holds b1 /. k = KL . (b1 /. k) ) ) ) proof reconsider b2 = rng b1 as Basis of V by Def2; consider KL being Linear_Combination of V such that A1: W = Sum KL and A2: Carrier KL c= b2 by Th8; deffunc H1( Nat) -> Element of the carrier of K = KL . (b1 /. $1); consider A being FinSequence of K such that A3: len A = len b1 and A4: for k being Nat st k in dom A holds A . k = H1(k) from FINSEQ_2:sch_1(); take A ; ::_thesis: ( len A = len b1 & ex KL being Linear_Combination of V st ( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len A holds A /. k = KL . (b1 /. k) ) ) ) thus len A = len b1 by A3; ::_thesis: ex KL being Linear_Combination of V st ( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len A holds A /. k = KL . (b1 /. k) ) ) take KL ; ::_thesis: ( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len A holds A /. k = KL . (b1 /. k) ) ) thus W = Sum KL by A1; ::_thesis: ( Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len A holds A /. k = KL . (b1 /. k) ) ) thus Carrier KL c= rng b1 by A2; ::_thesis: for k being Nat st 1 <= k & k <= len A holds A /. k = KL . (b1 /. k) let k be Nat; ::_thesis: ( 1 <= k & k <= len A implies A /. k = KL . (b1 /. k) ) A5: dom A = Seg (len b1) by A3, FINSEQ_1:def_3; assume ( 1 <= k & k <= len A ) ; ::_thesis: A /. k = KL . (b1 /. k) then A6: k in Seg (len b1) by A3, FINSEQ_1:1; then k in dom A by A3, FINSEQ_1:def_3; then A . k = A /. k by PARTFUN1:def_6; hence A /. k = KL . (b1 /. k) by A4, A5, A6; ::_thesis: verum end; uniqueness for b1, b2 being FinSequence of K st len b1 = len b1 & ex KL being Linear_Combination of V st ( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len b1 holds b1 /. k = KL . (b1 /. k) ) ) & len b2 = len b1 & ex KL being Linear_Combination of V st ( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len b2 holds b2 /. k = KL . (b1 /. k) ) ) holds b1 = b2 proof reconsider b = rng b1 as Basis of V by Def2; let F1, F2 be FinSequence of K; ::_thesis: ( len F1 = len b1 & ex KL being Linear_Combination of V st ( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len F1 holds F1 /. k = KL . (b1 /. k) ) ) & len F2 = len b1 & ex KL being Linear_Combination of V st ( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len F2 holds F2 /. k = KL . (b1 /. k) ) ) implies F1 = F2 ) assume A7: len F1 = len b1 ; ::_thesis: ( for KL being Linear_Combination of V holds ( not W = Sum KL or not Carrier KL c= rng b1 or ex k being Nat st ( 1 <= k & k <= len F1 & not F1 /. k = KL . (b1 /. k) ) ) or not len F2 = len b1 or for KL being Linear_Combination of V holds ( not W = Sum KL or not Carrier KL c= rng b1 or ex k being Nat st ( 1 <= k & k <= len F2 & not F2 /. k = KL . (b1 /. k) ) ) or F1 = F2 ) given KL1 being Linear_Combination of V such that A8: ( W = Sum KL1 & Carrier KL1 c= rng b1 ) and A9: for k being Nat st 1 <= k & k <= len F1 holds F1 /. k = KL1 . (b1 /. k) ; ::_thesis: ( not len F2 = len b1 or for KL being Linear_Combination of V holds ( not W = Sum KL or not Carrier KL c= rng b1 or ex k being Nat st ( 1 <= k & k <= len F2 & not F2 /. k = KL . (b1 /. k) ) ) or F1 = F2 ) assume A10: len F2 = len b1 ; ::_thesis: ( for KL being Linear_Combination of V holds ( not W = Sum KL or not Carrier KL c= rng b1 or ex k being Nat st ( 1 <= k & k <= len F2 & not F2 /. k = KL . (b1 /. k) ) ) or F1 = F2 ) given KL2 being Linear_Combination of V such that A11: ( W = Sum KL2 & Carrier KL2 c= rng b1 ) and A12: for k being Nat st 1 <= k & k <= len F2 holds F2 /. k = KL2 . (b1 /. k) ; ::_thesis: F1 = F2 A13: b is linearly-independent by VECTSP_7:def_3; for k being Nat st 1 <= k & k <= len F1 holds F1 . k = F2 . k proof let k be Nat; ::_thesis: ( 1 <= k & k <= len F1 implies F1 . k = F2 . k ) assume A14: ( 1 <= k & k <= len F1 ) ; ::_thesis: F1 . k = F2 . k then A15: k in dom F2 by A7, A10, FINSEQ_3:25; k in dom F1 by A14, FINSEQ_3:25; hence F1 . k = F1 /. k by PARTFUN1:def_6 .= KL1 . (b1 /. k) by A9, A14 .= KL2 . (b1 /. k) by A8, A11, A13, Th5 .= F2 /. k by A7, A10, A12, A14 .= F2 . k by A15, PARTFUN1:def_6 ; ::_thesis: verum end; hence F1 = F2 by A7, A10, FINSEQ_1:14; ::_thesis: verum end; end; :: deftheorem Def7 defines |-- MATRLIN:def_7_:_ for K being Field for V being finite-dimensional VectSp of K for b1 being OrdBasis of V for W being Element of V for b5 being FinSequence of K holds ( b5 = W |-- b1 iff ( len b5 = len b1 & ex KL being Linear_Combination of V st ( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len b5 holds b5 /. k = KL . (b1 /. k) ) ) ) ); Lm1: for K being Field for V being finite-dimensional VectSp of K for b being OrdBasis of V for W being Element of V holds dom (W |-- b) = dom b proof let K be Field; ::_thesis: for V being finite-dimensional VectSp of K for b being OrdBasis of V for W being Element of V holds dom (W |-- b) = dom b let V be finite-dimensional VectSp of K; ::_thesis: for b being OrdBasis of V for W being Element of V holds dom (W |-- b) = dom b let b be OrdBasis of V; ::_thesis: for W being Element of V holds dom (W |-- b) = dom b let W be Element of V; ::_thesis: dom (W |-- b) = dom b len (W |-- b) = len b by Def7; hence dom (W |-- b) = dom b by FINSEQ_3:29; ::_thesis: verum end; theorem Th34: :: MATRLIN:34 for K being Field for V2 being finite-dimensional VectSp of K for b2 being OrdBasis of V2 for v1, v2 being Vector of V2 st v1 |-- b2 = v2 |-- b2 holds v1 = v2 proof let K be Field; ::_thesis: for V2 being finite-dimensional VectSp of K for b2 being OrdBasis of V2 for v1, v2 being Vector of V2 st v1 |-- b2 = v2 |-- b2 holds v1 = v2 let V2 be finite-dimensional VectSp of K; ::_thesis: for b2 being OrdBasis of V2 for v1, v2 being Vector of V2 st v1 |-- b2 = v2 |-- b2 holds v1 = v2 let b2 be OrdBasis of V2; ::_thesis: for v1, v2 being Vector of V2 st v1 |-- b2 = v2 |-- b2 holds v1 = v2 let v1, v2 be Vector of V2; ::_thesis: ( v1 |-- b2 = v2 |-- b2 implies v1 = v2 ) consider KL1 being Linear_Combination of V2 such that A1: v1 = Sum KL1 and A2: Carrier KL1 c= rng b2 and A3: for t being Nat st 1 <= t & t <= len (v1 |-- b2) holds (v1 |-- b2) /. t = KL1 . (b2 /. t) by Def7; consider KL2 being Linear_Combination of V2 such that A4: v2 = Sum KL2 and A5: Carrier KL2 c= rng b2 and A6: for t being Nat st 1 <= t & t <= len (v2 |-- b2) holds (v2 |-- b2) /. t = KL2 . (b2 /. t) by Def7; assume A7: v1 |-- b2 = v2 |-- b2 ; ::_thesis: v1 = v2 A8: now__::_thesis:_for_t_being_Nat_st_1_<=_t_&_t_<=_len_(v1_|--_b2)_holds_ KL1_._(b2_/._t)_=_KL2_._(b2_/._t) let t be Nat; ::_thesis: ( 1 <= t & t <= len (v1 |-- b2) implies KL1 . (b2 /. t) = KL2 . (b2 /. t) ) assume A9: ( 1 <= t & t <= len (v1 |-- b2) ) ; ::_thesis: KL1 . (b2 /. t) = KL2 . (b2 /. t) hence KL1 . (b2 /. t) = (v2 |-- b2) /. t by A7, A3 .= KL2 . (b2 /. t) by A7, A6, A9 ; ::_thesis: verum end; A10: (Carrier KL1) \/ (Carrier KL2) c= rng b2 by A2, A5, XBOOLE_1:8; now__::_thesis:_for_v_being_Vector_of_V2_holds_KL1_._v_=_KL2_._v let v be Vector of V2; ::_thesis: KL1 . b1 = KL2 . b1 percases ( not v in (Carrier KL1) \/ (Carrier KL2) or v in (Carrier KL1) \/ (Carrier KL2) ) ; supposeA11: not v in (Carrier KL1) \/ (Carrier KL2) ; ::_thesis: KL1 . b1 = KL2 . b1 then not v in Carrier KL2 by XBOOLE_0:def_3; then A12: KL2 . v = 0. K by VECTSP_6:2; not v in Carrier KL1 by A11, XBOOLE_0:def_3; hence KL1 . v = KL2 . v by A12, VECTSP_6:2; ::_thesis: verum end; suppose v in (Carrier KL1) \/ (Carrier KL2) ; ::_thesis: KL1 . b1 = KL2 . b1 then consider x being set such that A13: x in dom b2 and A14: v = b2 . x by A10, FUNCT_1:def_3; reconsider x = x as Nat by A13, FINSEQ_3:23; x <= len b2 by A13, FINSEQ_3:25; then A15: x <= len (v1 |-- b2) by Def7; ( v = b2 /. x & 1 <= x ) by A13, A14, FINSEQ_3:25, PARTFUN1:def_6; hence KL1 . v = KL2 . v by A8, A15; ::_thesis: verum end; end; end; hence v1 = v2 by A1, A4, VECTSP_6:def_7; ::_thesis: verum end; theorem Th35: :: MATRLIN:35 for K being Field for V1 being finite-dimensional VectSp of K for b1 being OrdBasis of V1 for v being Element of V1 holds v = Sum (lmlt ((v |-- b1),b1)) proof let K be Field; ::_thesis: for V1 being finite-dimensional VectSp of K for b1 being OrdBasis of V1 for v being Element of V1 holds v = Sum (lmlt ((v |-- b1),b1)) let V1 be finite-dimensional VectSp of K; ::_thesis: for b1 being OrdBasis of V1 for v being Element of V1 holds v = Sum (lmlt ((v |-- b1),b1)) let b1 be OrdBasis of V1; ::_thesis: for v being Element of V1 holds v = Sum (lmlt ((v |-- b1),b1)) let v be Element of V1; ::_thesis: v = Sum (lmlt ((v |-- b1),b1)) consider KL being Linear_Combination of V1 such that A1: ( v = Sum KL & Carrier KL c= rng b1 ) and A2: for k being Nat st 1 <= k & k <= len (v |-- b1) holds (v |-- b1) /. k = KL . (b1 /. k) by Def7; len (v |-- b1) = len b1 by Def7; then A3: dom (v |-- b1) = dom b1 by FINSEQ_3:29; then A4: dom b1 = dom (lmlt ((v |-- b1),b1)) by Th12; len (KL (#) b1) = len b1 by VECTSP_6:def_5 .= len (lmlt ((v |-- b1),b1)) by A4, FINSEQ_3:29 ; then A5: dom (KL (#) b1) = dom (lmlt ((v |-- b1),b1)) by FINSEQ_3:29; A6: now__::_thesis:_for_t_being_Nat_st_t_in_dom_(lmlt_((v_|--_b1),b1))_holds_ (KL_(#)_b1)_._t_=_(lmlt_((v_|--_b1),b1))_._t let t be Nat; ::_thesis: ( t in dom (lmlt ((v |-- b1),b1)) implies (KL (#) b1) . t = (lmlt ((v |-- b1),b1)) . t ) assume A7: t in dom (lmlt ((v |-- b1),b1)) ; ::_thesis: (KL (#) b1) . t = (lmlt ((v |-- b1),b1)) . t then A8: b1 /. t = b1 . t by A4, PARTFUN1:def_6; t in dom (v |-- b1) by A3, A7, Th12; then A9: t <= len (v |-- b1) by FINSEQ_3:25; A10: 1 <= t by A7, FINSEQ_3:25; then A11: (v |-- b1) /. t = (v |-- b1) . t by A9, FINSEQ_4:15; t in dom (KL (#) b1) by A5, A7; hence (KL (#) b1) . t = (KL . (b1 /. t)) * (b1 /. t) by VECTSP_6:def_5 .= ((v |-- b1) /. t) * (b1 /. t) by A2, A10, A9 .= the lmult of V1 . (((v |-- b1) . t),(b1 . t)) by A8, A11, VECTSP_1:def_12 .= (lmlt ((v |-- b1),b1)) . t by A7, FUNCOP_1:22 ; ::_thesis: verum end; b1 is one-to-one by Def2; hence v = Sum (KL (#) b1) by A1, Th20 .= Sum (lmlt ((v |-- b1),b1)) by A5, A6, FINSEQ_1:13 ; ::_thesis: verum end; theorem Th36: :: MATRLIN:36 for K being Field for V1 being finite-dimensional VectSp of K for b1 being OrdBasis of V1 for d being FinSequence of K st len d = len b1 holds d = (Sum (lmlt (d,b1))) |-- b1 proof let K be Field; ::_thesis: for V1 being finite-dimensional VectSp of K for b1 being OrdBasis of V1 for d being FinSequence of K st len d = len b1 holds d = (Sum (lmlt (d,b1))) |-- b1 let V1 be finite-dimensional VectSp of K; ::_thesis: for b1 being OrdBasis of V1 for d being FinSequence of K st len d = len b1 holds d = (Sum (lmlt (d,b1))) |-- b1 let b1 be OrdBasis of V1; ::_thesis: for d being FinSequence of K st len d = len b1 holds d = (Sum (lmlt (d,b1))) |-- b1 let d be FinSequence of K; ::_thesis: ( len d = len b1 implies d = (Sum (lmlt (d,b1))) |-- b1 ) reconsider T = rng b1 as finite Subset of V1 by Def2; defpred S1[ Element of V1, Element of K] means ( ( $1 in rng b1 implies for k being Nat st k in dom b1 & b1 /. k = $1 holds $2 = d /. k ) & ( not $1 in rng b1 implies $2 = 0. K ) ); A1: for v being Element of V1 ex u being Element of K st S1[v,u] proof let v be Element of V1; ::_thesis: ex u being Element of K st S1[v,u] percases ( v in rng b1 or not v in rng b1 ) ; supposeA2: v in rng b1 ; ::_thesis: ex u being Element of K st S1[v,u] then consider k being Element of NAT such that A3: k in dom b1 and A4: b1 /. k = v by PARTFUN2:2; take u = d /. k; ::_thesis: S1[v,u] now__::_thesis:_for_i_being_Nat_st_i_in_dom_b1_&_b1_/._i_=_v_holds_ u_=_d_/._i A5: b1 is one-to-one by Def2; let i be Nat; ::_thesis: ( i in dom b1 & b1 /. i = v implies u = d /. i ) assume that A6: i in dom b1 and A7: b1 /. i = v ; ::_thesis: u = d /. i b1 . i = b1 /. k by A4, A6, A7, PARTFUN1:def_6 .= b1 . k by A3, PARTFUN1:def_6 ; hence u = d /. i by A3, A6, A5, FUNCT_1:def_4; ::_thesis: verum end; hence S1[v,u] by A2; ::_thesis: verum end; supposeA8: not v in rng b1 ; ::_thesis: ex u being Element of K st S1[v,u] take 0. K ; ::_thesis: S1[v, 0. K] thus S1[v, 0. K] by A8; ::_thesis: verum end; end; end; consider KL being Function of V1,K such that A9: for v being Element of V1 holds S1[v,KL . v] from FUNCT_2:sch_3(A1); A10: now__::_thesis:_ex_T_being_finite_Subset_of_V1_st_ for_v_being_Element_of_V1_st_not_v_in_T_holds_ KL_._v_=_0._K take T = T; ::_thesis: for v being Element of V1 st not v in T holds KL . v = 0. K let v be Element of V1; ::_thesis: ( not v in T implies KL . v = 0. K ) assume not v in T ; ::_thesis: KL . v = 0. K hence KL . v = 0. K by A9; ::_thesis: verum end; now__::_thesis:_ex_f_being_Function_of_V1,K_st_ (_KL_=_f_&_dom_f_=_the_carrier_of_V1_&_rng_f_c=_the_carrier_of_K_) take f = KL; ::_thesis: ( KL = f & dom f = the carrier of V1 & rng f c= the carrier of K ) thus ( KL = f & dom f = the carrier of V1 & rng f c= the carrier of K ) by FUNCT_2:def_1, RELAT_1:def_19; ::_thesis: verum end; then KL in Funcs ( the carrier of V1, the carrier of K) by FUNCT_2:def_2; then reconsider KL1 = KL as Linear_Combination of V1 by A10, VECTSP_6:def_1; assume A11: len d = len b1 ; ::_thesis: d = (Sum (lmlt (d,b1))) |-- b1 now__::_thesis:_ex_KL1_being_Linear_Combination_of_V1_st_ (_(_for_k_being_Nat_st_1_<=_k_&_k_<=_len_d_holds_ d_/._k_=_KL1_._(b1_/._k)_)_&_Carrier_KL1_c=_rng_b1_&_Sum_(lmlt_(d,b1))_=_Sum_KL1_) take KL1 = KL1; ::_thesis: ( ( for k being Nat st 1 <= k & k <= len d holds d /. k = KL1 . (b1 /. k) ) & Carrier KL1 c= rng b1 & Sum (lmlt (d,b1)) = Sum KL1 ) A12: b1 is one-to-one by Def2; thus A13: for k being Nat st 1 <= k & k <= len d holds d /. k = KL1 . (b1 /. k) ::_thesis: ( Carrier KL1 c= rng b1 & Sum (lmlt (d,b1)) = Sum KL1 ) proof let k be Nat; ::_thesis: ( 1 <= k & k <= len d implies d /. k = KL1 . (b1 /. k) ) assume ( 1 <= k & k <= len d ) ; ::_thesis: d /. k = KL1 . (b1 /. k) then A14: k in dom b1 by A11, FINSEQ_3:25; then b1 . k = b1 /. k by PARTFUN1:def_6; then b1 /. k in rng b1 by A14, FUNCT_1:def_3; hence d /. k = KL1 . (b1 /. k) by A9, A14; ::_thesis: verum end; for x being set st x in Carrier KL1 holds x in rng b1 proof let x be set ; ::_thesis: ( x in Carrier KL1 implies x in rng b1 ) assume x in Carrier KL1 ; ::_thesis: x in rng b1 then A15: ex v being Element of V1 st ( x = v & KL1 . v <> 0. K ) by VECTSP_6:1; assume not x in rng b1 ; ::_thesis: contradiction hence contradiction by A9, A15; ::_thesis: verum end; hence A16: Carrier KL1 c= rng b1 by TARSKI:def_3; ::_thesis: Sum (lmlt (d,b1)) = Sum KL1 A17: dom d = dom b1 by A11, FINSEQ_3:29; then A18: dom (lmlt (d,b1)) = dom b1 by Th12; then A19: len (lmlt (d,b1)) = len b1 by FINSEQ_3:29 .= len (KL1 (#) b1) by VECTSP_6:def_5 ; now__::_thesis:_for_k_being_Nat_st_k_in_dom_(lmlt_(d,b1))_holds_ (lmlt_(d,b1))_._k_=_(KL1_(#)_b1)_._k let k be Nat; ::_thesis: ( k in dom (lmlt (d,b1)) implies (lmlt (d,b1)) . k = (KL1 (#) b1) . k ) assume A20: k in dom (lmlt (d,b1)) ; ::_thesis: (lmlt (d,b1)) . k = (KL1 (#) b1) . k then A21: k in dom (KL1 (#) b1) by A19, FINSEQ_3:29; A22: ( 1 <= k & k <= len d ) by A11, A18, A20, FINSEQ_3:25; A23: ( d /. k = d . k & b1 /. k = b1 . k ) by A17, A18, A20, PARTFUN1:def_6; thus (lmlt (d,b1)) . k = the lmult of V1 . ((d . k),(b1 . k)) by A20, FUNCOP_1:22 .= (d /. k) * (b1 /. k) by A23, VECTSP_1:def_12 .= (KL1 . (b1 /. k)) * (b1 /. k) by A13, A22 .= (KL1 (#) b1) . k by A21, VECTSP_6:def_5 ; ::_thesis: verum end; hence Sum (lmlt (d,b1)) = Sum (KL1 (#) b1) by A19, FINSEQ_2:9 .= Sum KL1 by A16, A12, Th20 ; ::_thesis: verum end; hence d = (Sum (lmlt (d,b1))) |-- b1 by A11, Def7; ::_thesis: verum end; Lm2: for p being FinSequence for k being set st k in dom p holds len p > 0 proof let p be FinSequence; ::_thesis: for k being set st k in dom p holds len p > 0 let k be set ; ::_thesis: ( k in dom p implies len p > 0 ) assume k in dom p ; ::_thesis: len p > 0 then p <> {} ; hence len p > 0 ; ::_thesis: verum end; theorem Th37: :: MATRLIN:37 for K being Field for V1, V2 being finite-dimensional VectSp of K for f being Function of V1,V2 for b1 being OrdBasis of V1 for b2 being OrdBasis of V2 for a, d being FinSequence of K st len a = len b1 holds for j being Nat st j in dom b2 & len d = len b1 & ( for k being Nat st k in dom b1 holds d . k = ((f . (b1 /. k)) |-- b2) /. j ) & len b1 > 0 holds ((Sum (lmlt (a,(f * b1)))) |-- b2) /. j = Sum (mlt (a,d)) proof let K be Field; ::_thesis: for V1, V2 being finite-dimensional VectSp of K for f being Function of V1,V2 for b1 being OrdBasis of V1 for b2 being OrdBasis of V2 for a, d being FinSequence of K st len a = len b1 holds for j being Nat st j in dom b2 & len d = len b1 & ( for k being Nat st k in dom b1 holds d . k = ((f . (b1 /. k)) |-- b2) /. j ) & len b1 > 0 holds ((Sum (lmlt (a,(f * b1)))) |-- b2) /. j = Sum (mlt (a,d)) let V1, V2 be finite-dimensional VectSp of K; ::_thesis: for f being Function of V1,V2 for b1 being OrdBasis of V1 for b2 being OrdBasis of V2 for a, d being FinSequence of K st len a = len b1 holds for j being Nat st j in dom b2 & len d = len b1 & ( for k being Nat st k in dom b1 holds d . k = ((f . (b1 /. k)) |-- b2) /. j ) & len b1 > 0 holds ((Sum (lmlt (a,(f * b1)))) |-- b2) /. j = Sum (mlt (a,d)) let f be Function of V1,V2; ::_thesis: for b1 being OrdBasis of V1 for b2 being OrdBasis of V2 for a, d being FinSequence of K st len a = len b1 holds for j being Nat st j in dom b2 & len d = len b1 & ( for k being Nat st k in dom b1 holds d . k = ((f . (b1 /. k)) |-- b2) /. j ) & len b1 > 0 holds ((Sum (lmlt (a,(f * b1)))) |-- b2) /. j = Sum (mlt (a,d)) let b1 be OrdBasis of V1; ::_thesis: for b2 being OrdBasis of V2 for a, d being FinSequence of K st len a = len b1 holds for j being Nat st j in dom b2 & len d = len b1 & ( for k being Nat st k in dom b1 holds d . k = ((f . (b1 /. k)) |-- b2) /. j ) & len b1 > 0 holds ((Sum (lmlt (a,(f * b1)))) |-- b2) /. j = Sum (mlt (a,d)) let b2 be OrdBasis of V2; ::_thesis: for a, d being FinSequence of K st len a = len b1 holds for j being Nat st j in dom b2 & len d = len b1 & ( for k being Nat st k in dom b1 holds d . k = ((f . (b1 /. k)) |-- b2) /. j ) & len b1 > 0 holds ((Sum (lmlt (a,(f * b1)))) |-- b2) /. j = Sum (mlt (a,d)) let a, d be FinSequence of K; ::_thesis: ( len a = len b1 implies for j being Nat st j in dom b2 & len d = len b1 & ( for k being Nat st k in dom b1 holds d . k = ((f . (b1 /. k)) |-- b2) /. j ) & len b1 > 0 holds ((Sum (lmlt (a,(f * b1)))) |-- b2) /. j = Sum (mlt (a,d)) ) assume A1: len a = len b1 ; ::_thesis: for j being Nat st j in dom b2 & len d = len b1 & ( for k being Nat st k in dom b1 holds d . k = ((f . (b1 /. k)) |-- b2) /. j ) & len b1 > 0 holds ((Sum (lmlt (a,(f * b1)))) |-- b2) /. j = Sum (mlt (a,d)) reconsider B3 = f * b1 as FinSequence of V2 ; deffunc H1( Nat, Nat) -> Element of the carrier of K = ((B3 /. $1) |-- b2) /. $2; consider M being Matrix of len b1, len b2, the carrier of K such that A2: for i, j being Nat st [i,j] in Indices M holds M * (i,j) = H1(i,j) from MATRIX_1:sch_1(); deffunc H2( Nat) -> Element of the carrier of K = Sum (mlt (a,(Col (M,$1)))); consider dd being FinSequence of K such that A3: ( len dd = len b2 & ( for j being Nat st j in dom dd holds dd /. j = H2(j) ) ) from FINSEQ_4:sch_2(); let j be Nat; ::_thesis: ( j in dom b2 & len d = len b1 & ( for k being Nat st k in dom b1 holds d . k = ((f . (b1 /. k)) |-- b2) /. j ) & len b1 > 0 implies ((Sum (lmlt (a,(f * b1)))) |-- b2) /. j = Sum (mlt (a,d)) ) assume A4: j in dom b2 ; ::_thesis: ( not len d = len b1 or ex k being Nat st ( k in dom b1 & not d . k = ((f . (b1 /. k)) |-- b2) /. j ) or not len b1 > 0 or ((Sum (lmlt (a,(f * b1)))) |-- b2) /. j = Sum (mlt (a,d)) ) A5: j in dom dd by A4, A3, FINSEQ_3:29; assume that A6: len d = len b1 and A7: for k being Nat st k in dom b1 holds d . k = ((f . (b1 /. k)) |-- b2) /. j ; ::_thesis: ( not len b1 > 0 or ((Sum (lmlt (a,(f * b1)))) |-- b2) /. j = Sum (mlt (a,d)) ) A8: len (Col (M,j)) = len M by MATRIX_1:def_8 .= len d by A6, MATRIX_1:def_2 ; len M = len b1 by MATRIX_1:def_2; then A9: dom M = dom b1 by FINSEQ_3:29; A10: len b1 = len B3 by FINSEQ_2:33; then A11: dom b1 = dom B3 by FINSEQ_3:29; assume A12: len b1 > 0 ; ::_thesis: ((Sum (lmlt (a,(f * b1)))) |-- b2) /. j = Sum (mlt (a,d)) then A13: width M = len b2 by MATRIX_1:23; A14: now__::_thesis:_for_i_being_Nat_st_i_in_dom_B3_holds_ B3_/._i_=_Sum_(lmlt_((Line_(M,i)),b2)) let i be Nat; ::_thesis: ( i in dom B3 implies B3 /. i = Sum (lmlt ((Line (M,i)),b2)) ) assume A15: i in dom B3 ; ::_thesis: B3 /. i = Sum (lmlt ((Line (M,i)),b2)) A16: now__::_thesis:_for_j_being_Nat_st_j_in_dom_((B3_/._i)_|--_b2)_holds_ (Line_(M,i))_._j_=_((B3_/._i)_|--_b2)_._j let j be Nat; ::_thesis: ( j in dom ((B3 /. i) |-- b2) implies (Line (M,i)) . j = ((B3 /. i) |-- b2) . j ) assume A17: j in dom ((B3 /. i) |-- b2) ; ::_thesis: (Line (M,i)) . j = ((B3 /. i) |-- b2) . j then j in Seg (len ((B3 /. i) |-- b2)) by FINSEQ_1:def_3; then A18: j in Seg (width M) by A13, Def7; then [i,j] in [:(dom M),(Seg (width M)):] by A9, A11, A15, ZFMISC_1:87; then A19: [i,j] in Indices M by MATRIX_1:def_4; thus (Line (M,i)) . j = M * (i,j) by A18, MATRIX_1:def_7 .= ((B3 /. i) |-- b2) /. j by A2, A19 .= ((B3 /. i) |-- b2) . j by A17, PARTFUN1:def_6 ; ::_thesis: verum end; A20: len (Line (M,i)) = width M by MATRIX_1:def_7 .= len ((B3 /. i) |-- b2) by A13, Def7 ; thus B3 /. i = Sum (lmlt (((B3 /. i) |-- b2),b2)) by Th35 .= Sum (lmlt ((Line (M,i)),b2)) by A20, A16, FINSEQ_2:9 ; ::_thesis: verum end; Seg (len b2) = dom b2 by FINSEQ_1:def_3; then A21: j in Seg (width M) by A4, A12, MATRIX_1:23; A22: now__::_thesis:_for_i_being_Nat_st_i_in_dom_d_holds_ (Col_(M,j))_._i_=_d_._i let i be Nat; ::_thesis: ( i in dom d implies (Col (M,j)) . i = d . i ) assume i in dom d ; ::_thesis: (Col (M,j)) . i = d . i then A23: i in dom b1 by A6, FINSEQ_3:29; then A24: B3 /. i = B3 . i by A11, PARTFUN1:def_6 .= f . (b1 . i) by A23, FUNCT_1:13 .= f . (b1 /. i) by A23, PARTFUN1:def_6 ; [i,j] in [:(dom M),(Seg (width M)):] by A9, A21, A23, ZFMISC_1:87; then A25: [i,j] in Indices M by MATRIX_1:def_4; thus (Col (M,j)) . i = M * (i,j) by A9, A23, MATRIX_1:def_8 .= ((f . (b1 /. i)) |-- b2) /. j by A2, A24, A25 .= d . i by A7, A23 ; ::_thesis: verum end; len b2 > 0 by A4, Lm2; hence ((Sum (lmlt (a,(f * b1)))) |-- b2) /. j = ((Sum (lmlt (dd,b2))) |-- b2) /. j by A1, A12, A3, A10, A14, Th33 .= dd /. j by A3, Th36 .= Sum (mlt (a,(Col (M,j)))) by A3, A5 .= Sum (mlt (a,d)) by A8, A22, FINSEQ_2:9 ; ::_thesis: verum end; begin definition let K be Field; let V1, V2 be finite-dimensional VectSp of K; let f be Function of V1,V2; let b1 be FinSequence of V1; let b2 be OrdBasis of V2; func AutMt (f,b1,b2) -> Matrix of K means :Def8: :: MATRLIN:def 8 ( len it = len b1 & ( for k being Nat st k in dom b1 holds it /. k = (f . (b1 /. k)) |-- b2 ) ); existence ex b1 being Matrix of K st ( len b1 = len b1 & ( for k being Nat st k in dom b1 holds b1 /. k = (f . (b1 /. k)) |-- b2 ) ) proof deffunc H1( Nat) -> FinSequence of K = (f . (b1 /. $1)) |-- b2; consider M being FinSequence such that A1: len M = len b1 and A2: for k being Nat st k in dom M holds M . k = H1(k) from FINSEQ_1:sch_2(); A3: dom M = Seg (len b1) by A1, FINSEQ_1:def_3; ex n being Nat st for x being set st x in rng M holds ex s being FinSequence st ( s = x & len s = n ) proof take n = len ((f . (b1 /. 1)) |-- b2); ::_thesis: for x being set st x in rng M holds ex s being FinSequence st ( s = x & len s = n ) let x be set ; ::_thesis: ( x in rng M implies ex s being FinSequence st ( s = x & len s = n ) ) assume x in rng M ; ::_thesis: ex s being FinSequence st ( s = x & len s = n ) then consider y being set such that A4: y in dom M and A5: x = M . y by FUNCT_1:def_3; reconsider y = y as Nat by A4, FINSEQ_3:23; M . y = (f . (b1 /. y)) |-- b2 by A2, A4; then reconsider s = M . y as FinSequence ; take s ; ::_thesis: ( s = x & len s = n ) thus s = x by A5; ::_thesis: len s = n thus len s = len ((f . (b1 /. y)) |-- b2) by A2, A4 .= len b2 by Def7 .= n by Def7 ; ::_thesis: verum end; then reconsider M = M as tabular FinSequence by MATRIX_1:def_1; now__::_thesis:_for_x_being_set_st_x_in_rng_M_holds_ x_in_the_carrier_of_K_* let x be set ; ::_thesis: ( x in rng M implies x in the carrier of K * ) assume x in rng M ; ::_thesis: x in the carrier of K * then consider y being set such that A6: y in dom M and A7: x = M . y by FUNCT_1:def_3; reconsider y = y as Nat by A6, FINSEQ_3:23; M . y = (f . (b1 /. y)) |-- b2 by A2, A6; then reconsider s = M . y as FinSequence of K ; s = x by A7; hence x in the carrier of K * by FINSEQ_1:def_11; ::_thesis: verum end; then rng M c= the carrier of K * by TARSKI:def_3; then reconsider M = M as Matrix of K by FINSEQ_1:def_4; take M1 = M; ::_thesis: ( len M1 = len b1 & ( for k being Nat st k in dom b1 holds M1 /. k = (f . (b1 /. k)) |-- b2 ) ) for k being Nat st k in dom b1 holds M1 /. k = (f . (b1 /. k)) |-- b2 proof let k be Nat; ::_thesis: ( k in dom b1 implies M1 /. k = (f . (b1 /. k)) |-- b2 ) assume A8: k in dom b1 ; ::_thesis: M1 /. k = (f . (b1 /. k)) |-- b2 then A9: k in Seg (len b1) by FINSEQ_1:def_3; dom M1 = dom b1 by A1, FINSEQ_3:29; hence M1 /. k = M1 . k by A8, PARTFUN1:def_6 .= (f . (b1 /. k)) |-- b2 by A2, A3, A9 ; ::_thesis: verum end; hence ( len M1 = len b1 & ( for k being Nat st k in dom b1 holds M1 /. k = (f . (b1 /. k)) |-- b2 ) ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Matrix of K st len b1 = len b1 & ( for k being Nat st k in dom b1 holds b1 /. k = (f . (b1 /. k)) |-- b2 ) & len b2 = len b1 & ( for k being Nat st k in dom b1 holds b2 /. k = (f . (b1 /. k)) |-- b2 ) holds b1 = b2 proof let K1, K2 be Matrix of K; ::_thesis: ( len K1 = len b1 & ( for k being Nat st k in dom b1 holds K1 /. k = (f . (b1 /. k)) |-- b2 ) & len K2 = len b1 & ( for k being Nat st k in dom b1 holds K2 /. k = (f . (b1 /. k)) |-- b2 ) implies K1 = K2 ) assume that A10: len K1 = len b1 and A11: for k being Nat st k in dom b1 holds K1 /. k = (f . (b1 /. k)) |-- b2 and A12: len K2 = len b1 and A13: for k being Nat st k in dom b1 holds K2 /. k = (f . (b1 /. k)) |-- b2 ; ::_thesis: K1 = K2 for k being Nat st 1 <= k & k <= len K1 holds K1 . k = K2 . k proof let k be Nat; ::_thesis: ( 1 <= k & k <= len K1 implies K1 . k = K2 . k ) assume A14: ( 1 <= k & k <= len K1 ) ; ::_thesis: K1 . k = K2 . k then A15: k in dom b1 by A10, FINSEQ_3:25; A16: k in dom K2 by A10, A12, A14, FINSEQ_3:25; k in dom K1 by A14, FINSEQ_3:25; hence K1 . k = K1 /. k by PARTFUN1:def_6 .= (f . (b1 /. k)) |-- b2 by A11, A15 .= K2 /. k by A13, A15 .= K2 . k by A16, PARTFUN1:def_6 ; ::_thesis: verum end; hence K1 = K2 by A10, A12, FINSEQ_1:14; ::_thesis: verum end; end; :: deftheorem Def8 defines AutMt MATRLIN:def_8_:_ for K being Field for V1, V2 being finite-dimensional VectSp of K for f being Function of V1,V2 for b1 being FinSequence of V1 for b2 being OrdBasis of V2 for b7 being Matrix of K holds ( b7 = AutMt (f,b1,b2) iff ( len b7 = len b1 & ( for k being Nat st k in dom b1 holds b7 /. k = (f . (b1 /. k)) |-- b2 ) ) ); Lm3: for K being Field for V1, V2 being finite-dimensional VectSp of K for f being Function of V1,V2 for b1 being OrdBasis of V1 for b2 being OrdBasis of V2 holds dom (AutMt (f,b1,b2)) = dom b1 proof let K be Field; ::_thesis: for V1, V2 being finite-dimensional VectSp of K for f being Function of V1,V2 for b1 being OrdBasis of V1 for b2 being OrdBasis of V2 holds dom (AutMt (f,b1,b2)) = dom b1 let V1, V2 be finite-dimensional VectSp of K; ::_thesis: for f being Function of V1,V2 for b1 being OrdBasis of V1 for b2 being OrdBasis of V2 holds dom (AutMt (f,b1,b2)) = dom b1 let f be Function of V1,V2; ::_thesis: for b1 being OrdBasis of V1 for b2 being OrdBasis of V2 holds dom (AutMt (f,b1,b2)) = dom b1 let b1 be OrdBasis of V1; ::_thesis: for b2 being OrdBasis of V2 holds dom (AutMt (f,b1,b2)) = dom b1 let b2 be OrdBasis of V2; ::_thesis: dom (AutMt (f,b1,b2)) = dom b1 len (AutMt (f,b1,b2)) = len b1 by Def8; hence dom (AutMt (f,b1,b2)) = dom b1 by FINSEQ_3:29; ::_thesis: verum end; theorem Th38: :: MATRLIN:38 for K being Field for V1, V2 being finite-dimensional VectSp of K for f being Function of V1,V2 for b1 being OrdBasis of V1 for b2 being OrdBasis of V2 st len b1 = 0 holds AutMt (f,b1,b2) = {} proof let K be Field; ::_thesis: for V1, V2 being finite-dimensional VectSp of K for f being Function of V1,V2 for b1 being OrdBasis of V1 for b2 being OrdBasis of V2 st len b1 = 0 holds AutMt (f,b1,b2) = {} let V1, V2 be finite-dimensional VectSp of K; ::_thesis: for f being Function of V1,V2 for b1 being OrdBasis of V1 for b2 being OrdBasis of V2 st len b1 = 0 holds AutMt (f,b1,b2) = {} let f be Function of V1,V2; ::_thesis: for b1 being OrdBasis of V1 for b2 being OrdBasis of V2 st len b1 = 0 holds AutMt (f,b1,b2) = {} let b1 be OrdBasis of V1; ::_thesis: for b2 being OrdBasis of V2 st len b1 = 0 holds AutMt (f,b1,b2) = {} let b2 be OrdBasis of V2; ::_thesis: ( len b1 = 0 implies AutMt (f,b1,b2) = {} ) assume len b1 = 0 ; ::_thesis: AutMt (f,b1,b2) = {} then len (AutMt (f,b1,b2)) = 0 by Def8; hence AutMt (f,b1,b2) = {} ; ::_thesis: verum end; theorem Th39: :: MATRLIN:39 for K being Field for V1, V2 being finite-dimensional VectSp of K for f being Function of V1,V2 for b1 being OrdBasis of V1 for b2 being OrdBasis of V2 st len b1 > 0 holds width (AutMt (f,b1,b2)) = len b2 proof let K be Field; ::_thesis: for V1, V2 being finite-dimensional VectSp of K for f being Function of V1,V2 for b1 being OrdBasis of V1 for b2 being OrdBasis of V2 st len b1 > 0 holds width (AutMt (f,b1,b2)) = len b2 let V1, V2 be finite-dimensional VectSp of K; ::_thesis: for f being Function of V1,V2 for b1 being OrdBasis of V1 for b2 being OrdBasis of V2 st len b1 > 0 holds width (AutMt (f,b1,b2)) = len b2 let f be Function of V1,V2; ::_thesis: for b1 being OrdBasis of V1 for b2 being OrdBasis of V2 st len b1 > 0 holds width (AutMt (f,b1,b2)) = len b2 let b1 be OrdBasis of V1; ::_thesis: for b2 being OrdBasis of V2 st len b1 > 0 holds width (AutMt (f,b1,b2)) = len b2 let b2 be OrdBasis of V2; ::_thesis: ( len b1 > 0 implies width (AutMt (f,b1,b2)) = len b2 ) assume len b1 > 0 ; ::_thesis: width (AutMt (f,b1,b2)) = len b2 then len (AutMt (f,b1,b2)) > 0 by Def8; then consider s being FinSequence such that A1: s in rng (AutMt (f,b1,b2)) and A2: len s = width (AutMt (f,b1,b2)) by MATRIX_1:def_3; consider i being Nat such that A3: i in dom (AutMt (f,b1,b2)) and A4: (AutMt (f,b1,b2)) . i = s by A1, FINSEQ_2:10; len (AutMt (f,b1,b2)) = len b1 by Def8; then A5: i in dom b1 by A3, FINSEQ_3:29; s = (AutMt (f,b1,b2)) /. i by A3, A4, PARTFUN1:def_6 .= (f . (b1 /. i)) |-- b2 by A5, Def8 ; hence width (AutMt (f,b1,b2)) = len b2 by A2, Def7; ::_thesis: verum end; theorem :: MATRLIN:40 for K being Field for V1, V2 being finite-dimensional VectSp of K for f1, f2 being Function of V1,V2 for b1 being OrdBasis of V1 for b2 being OrdBasis of V2 st f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous & AutMt (f1,b1,b2) = AutMt (f2,b1,b2) & len b1 > 0 holds f1 = f2 proof let K be Field; ::_thesis: for V1, V2 being finite-dimensional VectSp of K for f1, f2 being Function of V1,V2 for b1 being OrdBasis of V1 for b2 being OrdBasis of V2 st f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous & AutMt (f1,b1,b2) = AutMt (f2,b1,b2) & len b1 > 0 holds f1 = f2 let V1, V2 be finite-dimensional VectSp of K; ::_thesis: for f1, f2 being Function of V1,V2 for b1 being OrdBasis of V1 for b2 being OrdBasis of V2 st f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous & AutMt (f1,b1,b2) = AutMt (f2,b1,b2) & len b1 > 0 holds f1 = f2 let f1, f2 be Function of V1,V2; ::_thesis: for b1 being OrdBasis of V1 for b2 being OrdBasis of V2 st f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous & AutMt (f1,b1,b2) = AutMt (f2,b1,b2) & len b1 > 0 holds f1 = f2 let b1 be OrdBasis of V1; ::_thesis: for b2 being OrdBasis of V2 st f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous & AutMt (f1,b1,b2) = AutMt (f2,b1,b2) & len b1 > 0 holds f1 = f2 let b2 be OrdBasis of V2; ::_thesis: ( f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous & AutMt (f1,b1,b2) = AutMt (f2,b1,b2) & len b1 > 0 implies f1 = f2 ) assume that A1: ( f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous ) and A2: AutMt (f1,b1,b2) = AutMt (f2,b1,b2) and A3: len b1 > 0 ; ::_thesis: f1 = f2 rng b1 is Basis of V1 by Def2; then A4: rng b1 c= the carrier of V1 ; then A5: rng b1 c= dom f2 by FUNCT_2:def_1; rng b1 c= dom f1 by A4, FUNCT_2:def_1; then A6: dom (f1 * b1) = dom b1 by RELAT_1:27 .= dom (f2 * b1) by A5, RELAT_1:27 ; now__::_thesis:_for_x_being_set_st_x_in_dom_(f1_*_b1)_holds_ (f1_*_b1)_._x_=_(f2_*_b1)_._x let x be set ; ::_thesis: ( x in dom (f1 * b1) implies (f1 * b1) . x = (f2 * b1) . x ) assume A7: x in dom (f1 * b1) ; ::_thesis: (f1 * b1) . x = (f2 * b1) . x then reconsider k = x as Nat by FINSEQ_3:23; A8: dom (f1 * b1) c= dom b1 by RELAT_1:25; then A9: (f1 . (b1 /. k)) |-- b2 = (AutMt (f2,b1,b2)) /. k by A2, A7, Def8 .= (f2 . (b1 /. k)) |-- b2 by A7, A8, Def8 ; thus (f1 * b1) . x = f1 . (b1 . x) by A7, FUNCT_1:12 .= f1 . (b1 /. x) by A7, A8, PARTFUN1:def_6 .= f2 . (b1 /. x) by A9, Th34 .= f2 . (b1 . x) by A7, A8, PARTFUN1:def_6 .= (f2 * b1) . x by A6, A7, FUNCT_1:12 ; ::_thesis: verum end; hence f1 = f2 by A1, A3, A6, Th22, FUNCT_1:2; ::_thesis: verum end; theorem :: MATRLIN:41 for K being Field for V1, V2, V3 being finite-dimensional VectSp of K for f being Function of V1,V2 for g being Function of V2,V3 for b1 being OrdBasis of V1 for b2 being OrdBasis of V2 for b3 being OrdBasis of V3 st g is additive & g is homogeneous & len b1 > 0 & len b2 > 0 holds AutMt ((g * f),b1,b3) = (AutMt (f,b1,b2)) * (AutMt (g,b2,b3)) proof let K be Field; ::_thesis: for V1, V2, V3 being finite-dimensional VectSp of K for f being Function of V1,V2 for g being Function of V2,V3 for b1 being OrdBasis of V1 for b2 being OrdBasis of V2 for b3 being OrdBasis of V3 st g is additive & g is homogeneous & len b1 > 0 & len b2 > 0 holds AutMt ((g * f),b1,b3) = (AutMt (f,b1,b2)) * (AutMt (g,b2,b3)) let V1, V2, V3 be finite-dimensional VectSp of K; ::_thesis: for f being Function of V1,V2 for g being Function of V2,V3 for b1 being OrdBasis of V1 for b2 being OrdBasis of V2 for b3 being OrdBasis of V3 st g is additive & g is homogeneous & len b1 > 0 & len b2 > 0 holds AutMt ((g * f),b1,b3) = (AutMt (f,b1,b2)) * (AutMt (g,b2,b3)) let f be Function of V1,V2; ::_thesis: for g being Function of V2,V3 for b1 being OrdBasis of V1 for b2 being OrdBasis of V2 for b3 being OrdBasis of V3 st g is additive & g is homogeneous & len b1 > 0 & len b2 > 0 holds AutMt ((g * f),b1,b3) = (AutMt (f,b1,b2)) * (AutMt (g,b2,b3)) let g be Function of V2,V3; ::_thesis: for b1 being OrdBasis of V1 for b2 being OrdBasis of V2 for b3 being OrdBasis of V3 st g is additive & g is homogeneous & len b1 > 0 & len b2 > 0 holds AutMt ((g * f),b1,b3) = (AutMt (f,b1,b2)) * (AutMt (g,b2,b3)) let b1 be OrdBasis of V1; ::_thesis: for b2 being OrdBasis of V2 for b3 being OrdBasis of V3 st g is additive & g is homogeneous & len b1 > 0 & len b2 > 0 holds AutMt ((g * f),b1,b3) = (AutMt (f,b1,b2)) * (AutMt (g,b2,b3)) let b2 be OrdBasis of V2; ::_thesis: for b3 being OrdBasis of V3 st g is additive & g is homogeneous & len b1 > 0 & len b2 > 0 holds AutMt ((g * f),b1,b3) = (AutMt (f,b1,b2)) * (AutMt (g,b2,b3)) let b3 be OrdBasis of V3; ::_thesis: ( g is additive & g is homogeneous & len b1 > 0 & len b2 > 0 implies AutMt ((g * f),b1,b3) = (AutMt (f,b1,b2)) * (AutMt (g,b2,b3)) ) assume A1: ( g is additive & g is homogeneous ) ; ::_thesis: ( not len b1 > 0 or not len b2 > 0 or AutMt ((g * f),b1,b3) = (AutMt (f,b1,b2)) * (AutMt (g,b2,b3)) ) assume that A2: len b1 > 0 and A3: len b2 > 0 ; ::_thesis: AutMt ((g * f),b1,b3) = (AutMt (f,b1,b2)) * (AutMt (g,b2,b3)) A4: width (AutMt (f,b1,b2)) = len b2 by A2, Th39 .= len (AutMt (g,b2,b3)) by Def8 ; A5: width (AutMt ((g * f),b1,b3)) = len b3 by A2, Th39 .= width (AutMt (g,b2,b3)) by A3, Th39 ; then A6: width (AutMt ((g * f),b1,b3)) = width ((AutMt (f,b1,b2)) * (AutMt (g,b2,b3))) by A4, MATRIX_3:def_4; A7: len (AutMt ((g * f),b1,b3)) = len b1 by Def8 .= len (AutMt (f,b1,b2)) by Def8 .= len ((AutMt (f,b1,b2)) * (AutMt (g,b2,b3))) by A4, MATRIX_3:def_4 ; then A8: dom (AutMt ((g * f),b1,b3)) = dom ((AutMt (f,b1,b2)) * (AutMt (g,b2,b3))) by FINSEQ_3:29; for i, j being Nat st [i,j] in Indices (AutMt ((g * f),b1,b3)) holds (AutMt ((g * f),b1,b3)) * (i,j) = ((AutMt (f,b1,b2)) * (AutMt (g,b2,b3))) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (AutMt ((g * f),b1,b3)) implies (AutMt ((g * f),b1,b3)) * (i,j) = ((AutMt (f,b1,b2)) * (AutMt (g,b2,b3))) * (i,j) ) deffunc H1( Nat) -> Element of the carrier of K = ((g . (b2 /. $1)) |-- b3) /. j; consider d being FinSequence of K such that A9: ( len d = len b2 & ( for k being Nat st k in dom d holds d . k = H1(k) ) ) from FINSEQ_2:sch_1(); assume A10: [i,j] in Indices (AutMt ((g * f),b1,b3)) ; ::_thesis: (AutMt ((g * f),b1,b3)) * (i,j) = ((AutMt (f,b1,b2)) * (AutMt (g,b2,b3))) * (i,j) then A11: [i,j] in [:(dom (AutMt ((g * f),b1,b3))),(Seg (width (AutMt ((g * f),b1,b3)))):] by MATRIX_1:def_4; then A12: j in Seg (width (AutMt ((g * f),b1,b3))) by ZFMISC_1:87; A13: len (Col ((AutMt (g,b2,b3)),j)) = len (AutMt (g,b2,b3)) by MATRIX_1:def_8 .= len d by A9, Def8 ; A14: dom d = Seg (len b2) by A9, FINSEQ_1:def_3; A15: [i,j] in Indices ((AutMt (f,b1,b2)) * (AutMt (g,b2,b3))) by A8, A6, A11, MATRIX_1:def_4; A16: i in dom (AutMt ((g * f),b1,b3)) by A11, ZFMISC_1:87; A17: width (AutMt ((g * f),b1,b3)) <> {} by A12; len b1 = len (AutMt ((g * f),b1,b3)) by Def8; then len b1 > 0 by A17, MATRIX_1:def_3; then A18: j in Seg (len b3) by A12, Th39; then A19: j in dom b3 by FINSEQ_1:def_3; A20: now__::_thesis:_for_k_being_Nat_st_1_<=_k_&_k_<=_len_d_holds_ (Col_((AutMt_(g,b2,b3)),j))_._k_=_d_._k let k be Nat; ::_thesis: ( 1 <= k & k <= len d implies (Col ((AutMt (g,b2,b3)),j)) . k = d . k ) assume A21: ( 1 <= k & k <= len d ) ; ::_thesis: (Col ((AutMt (g,b2,b3)),j)) . k = d . k then A22: k in dom d by FINSEQ_3:25; A23: k in dom b2 by A9, A21, FINSEQ_3:25; A24: len (AutMt (g,b2,b3)) = len b2 by Def8; then A25: k in dom (AutMt (g,b2,b3)) by A9, A21, FINSEQ_3:25; j in Seg (width (AutMt (g,b2,b3))) by A5, A11, ZFMISC_1:87; then [k,j] in [:(dom (AutMt (g,b2,b3))),(Seg (width (AutMt (g,b2,b3)))):] by A25, ZFMISC_1:87; then [k,j] in Indices (AutMt (g,b2,b3)) by MATRIX_1:def_4; then consider p2 being FinSequence of K such that A26: p2 = (AutMt (g,b2,b3)) . k and A27: (AutMt (g,b2,b3)) * (k,j) = p2 . j by MATRIX_1:def_5; A28: p2 = (AutMt (g,b2,b3)) /. k by A25, A26, PARTFUN1:def_6 .= (g . (b2 /. k)) |-- b3 by A23, Def8 ; then j in Seg (len p2) by A18, Def7; then A29: j in dom p2 by FINSEQ_1:def_3; k in dom (AutMt (g,b2,b3)) by A9, A21, A24, FINSEQ_3:25; hence (Col ((AutMt (g,b2,b3)),j)) . k = p2 . j by A27, MATRIX_1:def_8 .= ((g . (b2 /. k)) |-- b3) /. j by A28, A29, PARTFUN1:def_6 .= d . k by A9, A22 ; ::_thesis: verum end; b1 /. i in the carrier of V1 ; then A30: b1 /. i in dom f by FUNCT_2:def_1; consider p1 being FinSequence of K such that A31: p1 = (AutMt ((g * f),b1,b3)) . i and A32: (AutMt ((g * f),b1,b3)) * (i,j) = p1 . j by A10, MATRIX_1:def_5; A33: len ((f . (b1 /. i)) |-- b2) = len b2 by Def7; A34: len (AutMt ((g * f),b1,b3)) = len b1 by Def8; then A35: i in dom b1 by A16, FINSEQ_3:29; A36: p1 = (AutMt ((g * f),b1,b3)) /. i by A16, A31, PARTFUN1:def_6 .= ((g * f) . (b1 /. i)) |-- b3 by A35, Def8 ; len (AutMt (f,b1,b2)) = len b1 by Def8; then A37: i in dom (AutMt (f,b1,b2)) by A16, A34, FINSEQ_3:29; then A38: Line ((AutMt (f,b1,b2)),i) = (AutMt (f,b1,b2)) . i by MATRIX_2:16 .= (AutMt (f,b1,b2)) /. i by A37, PARTFUN1:def_6 .= (f . (b1 /. i)) |-- b2 by A35, Def8 ; A39: Seg (len b2) = dom b2 by FINSEQ_1:def_3; j in Seg (len (((g * f) . (b1 /. i)) |-- b3)) by A18, Def7; then j in dom p1 by A36, FINSEQ_1:def_3; hence (AutMt ((g * f),b1,b3)) * (i,j) = (((g * f) . (b1 /. i)) |-- b3) /. j by A32, A36, PARTFUN1:def_6 .= ((g . (f . (b1 /. i))) |-- b3) /. j by A30, FUNCT_1:13 .= ((g . (Sum (lmlt (((f . (b1 /. i)) |-- b2),b2)))) |-- b3) /. j by Th35 .= ((Sum (lmlt (((f . (b1 /. i)) |-- b2),(g * b2)))) |-- b3) /. j by A1, A33, Th18 .= Sum (mlt (((f . (b1 /. i)) |-- b2),d)) by A3, A19, A9, A14, A39, A33, Th37 .= (Line ((AutMt (f,b1,b2)),i)) "*" (Col ((AutMt (g,b2,b3)),j)) by A38, A13, A20, FINSEQ_1:14 .= ((AutMt (f,b1,b2)) * (AutMt (g,b2,b3))) * (i,j) by A4, A15, MATRIX_3:def_4 ; ::_thesis: verum end; hence AutMt ((g * f),b1,b3) = (AutMt (f,b1,b2)) * (AutMt (g,b2,b3)) by A7, A6, MATRIX_1:21; ::_thesis: verum end; theorem :: MATRLIN:42 for K being Field for V1, V2 being finite-dimensional VectSp of K for f1, f2 being Function of V1,V2 for b1 being OrdBasis of V1 for b2 being OrdBasis of V2 holds AutMt ((f1 + f2),b1,b2) = (AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2)) proof let K be Field; ::_thesis: for V1, V2 being finite-dimensional VectSp of K for f1, f2 being Function of V1,V2 for b1 being OrdBasis of V1 for b2 being OrdBasis of V2 holds AutMt ((f1 + f2),b1,b2) = (AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2)) let V1, V2 be finite-dimensional VectSp of K; ::_thesis: for f1, f2 being Function of V1,V2 for b1 being OrdBasis of V1 for b2 being OrdBasis of V2 holds AutMt ((f1 + f2),b1,b2) = (AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2)) let f1, f2 be Function of V1,V2; ::_thesis: for b1 being OrdBasis of V1 for b2 being OrdBasis of V2 holds AutMt ((f1 + f2),b1,b2) = (AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2)) let b1 be OrdBasis of V1; ::_thesis: for b2 being OrdBasis of V2 holds AutMt ((f1 + f2),b1,b2) = (AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2)) let b2 be OrdBasis of V2; ::_thesis: AutMt ((f1 + f2),b1,b2) = (AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2)) A1: len (AutMt ((f1 + f2),b1,b2)) = len b1 by Def8 .= len (AutMt (f1,b1,b2)) by Def8 ; then A2: dom (AutMt ((f1 + f2),b1,b2)) = dom (AutMt (f1,b1,b2)) by FINSEQ_3:29; A3: width (AutMt (f1,b1,b2)) = width (AutMt (f2,b1,b2)) proof percases ( len b1 = 0 or len b1 > 0 ) ; supposeA4: len b1 = 0 ; ::_thesis: width (AutMt (f1,b1,b2)) = width (AutMt (f2,b1,b2)) then AutMt (f1,b1,b2) = {} by Th38 .= AutMt (f2,b1,b2) by A4, Th38 ; hence width (AutMt (f1,b1,b2)) = width (AutMt (f2,b1,b2)) ; ::_thesis: verum end; supposeA5: len b1 > 0 ; ::_thesis: width (AutMt (f1,b1,b2)) = width (AutMt (f2,b1,b2)) hence width (AutMt (f1,b1,b2)) = len b2 by Th39 .= width (AutMt (f2,b1,b2)) by A5, Th39 ; ::_thesis: verum end; end; end; A6: width (AutMt ((f1 + f2),b1,b2)) = width (AutMt (f1,b1,b2)) proof percases ( len b1 = 0 or len b1 > 0 ) ; supposeA7: len b1 = 0 ; ::_thesis: width (AutMt ((f1 + f2),b1,b2)) = width (AutMt (f1,b1,b2)) then AutMt ((f1 + f2),b1,b2) = {} by Th38 .= AutMt (f1,b1,b2) by A7, Th38 ; hence width (AutMt ((f1 + f2),b1,b2)) = width (AutMt (f1,b1,b2)) ; ::_thesis: verum end; supposeA8: len b1 > 0 ; ::_thesis: width (AutMt ((f1 + f2),b1,b2)) = width (AutMt (f1,b1,b2)) hence width (AutMt ((f1 + f2),b1,b2)) = len b2 by Th39 .= width (AutMt (f1,b1,b2)) by A8, Th39 ; ::_thesis: verum end; end; end; then A9: width (AutMt ((f1 + f2),b1,b2)) = width ((AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2))) by MATRIX_3:def_3; len (AutMt (f1,b1,b2)) = len b1 by Def8 .= len (AutMt (f2,b1,b2)) by Def8 ; then A10: dom (AutMt (f1,b1,b2)) = dom (AutMt (f2,b1,b2)) by FINSEQ_3:29; A11: for i, j being Nat st [i,j] in Indices (AutMt ((f1 + f2),b1,b2)) holds (AutMt ((f1 + f2),b1,b2)) * (i,j) = ((AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2))) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (AutMt ((f1 + f2),b1,b2)) implies (AutMt ((f1 + f2),b1,b2)) * (i,j) = ((AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2))) * (i,j) ) assume A12: [i,j] in Indices (AutMt ((f1 + f2),b1,b2)) ; ::_thesis: (AutMt ((f1 + f2),b1,b2)) * (i,j) = ((AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2))) * (i,j) then A13: [i,j] in [:(dom (AutMt ((f1 + f2),b1,b2))),(Seg (width (AutMt ((f1 + f2),b1,b2)))):] by MATRIX_1:def_4; then A14: [i,j] in Indices (AutMt (f1,b1,b2)) by A2, A6, MATRIX_1:def_4; A15: [i,j] in Indices (AutMt (f2,b1,b2)) by A10, A3, A2, A6, A13, MATRIX_1:def_4; (AutMt ((f1 + f2),b1,b2)) * (i,j) = ((AutMt (f1,b1,b2)) * (i,j)) + ((AutMt (f2,b1,b2)) * (i,j)) proof consider KL3 being Linear_Combination of V2 such that A16: ( f2 . (b1 /. i) = Sum KL3 & Carrier KL3 c= rng b2 ) and A17: for t being Nat st 1 <= t & t <= len ((f2 . (b1 /. i)) |-- b2) holds ((f2 . (b1 /. i)) |-- b2) /. t = KL3 . (b2 /. t) by Def7; consider KL2 being Linear_Combination of V2 such that A18: ( f1 . (b1 /. i) = Sum KL2 & Carrier KL2 c= rng b2 ) and A19: for t being Nat st 1 <= t & t <= len ((f1 . (b1 /. i)) |-- b2) holds ((f1 . (b1 /. i)) |-- b2) /. t = KL2 . (b2 /. t) by Def7; A20: i in dom (AutMt ((f1 + f2),b1,b2)) by A13, ZFMISC_1:87; then A21: i in dom b1 by Lm3; reconsider b4 = rng b2 as Basis of V2 by Def2; consider p1 being FinSequence of K such that A22: p1 = (AutMt ((f1 + f2),b1,b2)) . i and A23: (AutMt ((f1 + f2),b1,b2)) * (i,j) = p1 . j by A12, MATRIX_1:def_5; consider KL1 being Linear_Combination of V2 such that A24: ( (f1 + f2) . (b1 /. i) = Sum KL1 & Carrier KL1 c= rng b2 ) and A25: for t being Nat st 1 <= t & t <= len (((f1 + f2) . (b1 /. i)) |-- b2) holds (((f1 + f2) . (b1 /. i)) |-- b2) /. t = KL1 . (b2 /. t) by Def7; ( b4 is linearly-independent & (f1 + f2) . (b1 /. i) = (f1 . (b1 /. i)) + (f2 . (b1 /. i)) ) by Def3, VECTSP_7:def_3; then A26: KL1 . (b2 /. j) = (KL2 + KL3) . (b2 /. j) by A24, A18, A16, Th6 .= (KL2 . (b2 /. j)) + (KL3 . (b2 /. j)) by VECTSP_6:22 ; A27: p1 = (AutMt ((f1 + f2),b1,b2)) /. i by A22, A20, PARTFUN1:def_6 .= ((f1 + f2) . (b1 /. i)) |-- b2 by A21, Def8 ; consider p3 being FinSequence of K such that A28: p3 = (AutMt (f2,b1,b2)) . i and A29: (AutMt (f2,b1,b2)) * (i,j) = p3 . j by A15, MATRIX_1:def_5; consider p2 being FinSequence of K such that A30: p2 = (AutMt (f1,b1,b2)) . i and A31: (AutMt (f1,b1,b2)) * (i,j) = p2 . j by A14, MATRIX_1:def_5; A32: j in Seg (width (AutMt ((f1 + f2),b1,b2))) by A13, ZFMISC_1:87; then A33: 1 <= j by FINSEQ_1:1; len b1 = len (AutMt ((f1 + f2),b1,b2)) by Def8; then dom b1 = dom (AutMt ((f1 + f2),b1,b2)) by FINSEQ_3:29; then dom b1 <> {} by A13, ZFMISC_1:87; then Seg (len b1) <> {} by FINSEQ_1:def_3; then len b1 > 0 ; then A34: j in Seg (len b2) by A32, Th39; then A35: j <= len b2 by FINSEQ_1:1; then j <= len (((f1 + f2) . (b1 /. i)) |-- b2) by Def7; then A36: p1 /. j = KL1 . (b2 /. j) by A33, A27, A25; A37: j in dom b2 by A34, FINSEQ_1:def_3; i in dom (AutMt (f2,b1,b2)) by A21, Lm3; then A38: p3 = (AutMt (f2,b1,b2)) /. i by A28, PARTFUN1:def_6 .= (f2 . (b1 /. i)) |-- b2 by A21, Def8 ; then j in dom p3 by A37, Lm1; then A39: (AutMt (f2,b1,b2)) * (i,j) = p3 /. j by A29, PARTFUN1:def_6; i in dom (AutMt (f1,b1,b2)) by A21, Lm3; then A40: p2 = (AutMt (f1,b1,b2)) /. i by A30, PARTFUN1:def_6 .= (f1 . (b1 /. i)) |-- b2 by A21, Def8 ; then j in dom p2 by A37, Lm1; then A41: (AutMt (f1,b1,b2)) * (i,j) = p2 /. j by A31, PARTFUN1:def_6; j <= len ((f2 . (b1 /. i)) |-- b2) by A35, Def7; then A42: p3 /. j = KL3 . (b2 /. j) by A33, A38, A17; j <= len ((f1 . (b1 /. i)) |-- b2) by A35, Def7; then A43: p2 /. j = KL2 . (b2 /. j) by A33, A40, A19; j in dom p1 by A37, A27, Lm1; hence (AutMt ((f1 + f2),b1,b2)) * (i,j) = ((AutMt (f1,b1,b2)) * (i,j)) + ((AutMt (f2,b1,b2)) * (i,j)) by A23, A41, A39, A36, A43, A42, A26, PARTFUN1:def_6; ::_thesis: verum end; hence (AutMt ((f1 + f2),b1,b2)) * (i,j) = ((AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2))) * (i,j) by A14, MATRIX_3:def_3; ::_thesis: verum end; len (AutMt ((f1 + f2),b1,b2)) = len ((AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2))) by A1, MATRIX_3:def_3; hence AutMt ((f1 + f2),b1,b2) = (AutMt (f1,b1,b2)) + (AutMt (f2,b1,b2)) by A9, A11, MATRIX_1:21; ::_thesis: verum end; theorem :: MATRLIN:43 for K being Field for a being Element of K for V1, V2 being finite-dimensional VectSp of K for f being Function of V1,V2 for b1 being OrdBasis of V1 for b2 being OrdBasis of V2 st a <> 0. K holds AutMt ((a * f),b1,b2) = a * (AutMt (f,b1,b2)) proof let K be Field; ::_thesis: for a being Element of K for V1, V2 being finite-dimensional VectSp of K for f being Function of V1,V2 for b1 being OrdBasis of V1 for b2 being OrdBasis of V2 st a <> 0. K holds AutMt ((a * f),b1,b2) = a * (AutMt (f,b1,b2)) let a be Element of K; ::_thesis: for V1, V2 being finite-dimensional VectSp of K for f being Function of V1,V2 for b1 being OrdBasis of V1 for b2 being OrdBasis of V2 st a <> 0. K holds AutMt ((a * f),b1,b2) = a * (AutMt (f,b1,b2)) let V1, V2 be finite-dimensional VectSp of K; ::_thesis: for f being Function of V1,V2 for b1 being OrdBasis of V1 for b2 being OrdBasis of V2 st a <> 0. K holds AutMt ((a * f),b1,b2) = a * (AutMt (f,b1,b2)) let f be Function of V1,V2; ::_thesis: for b1 being OrdBasis of V1 for b2 being OrdBasis of V2 st a <> 0. K holds AutMt ((a * f),b1,b2) = a * (AutMt (f,b1,b2)) let b1 be OrdBasis of V1; ::_thesis: for b2 being OrdBasis of V2 st a <> 0. K holds AutMt ((a * f),b1,b2) = a * (AutMt (f,b1,b2)) let b2 be OrdBasis of V2; ::_thesis: ( a <> 0. K implies AutMt ((a * f),b1,b2) = a * (AutMt (f,b1,b2)) ) assume A1: a <> 0. K ; ::_thesis: AutMt ((a * f),b1,b2) = a * (AutMt (f,b1,b2)) A2: width (AutMt ((a * f),b1,b2)) = width (AutMt (f,b1,b2)) proof percases ( len b1 = 0 or len b1 > 0 ) ; supposeA3: len b1 = 0 ; ::_thesis: width (AutMt ((a * f),b1,b2)) = width (AutMt (f,b1,b2)) then AutMt ((a * f),b1,b2) = {} by Th38 .= AutMt (f,b1,b2) by A3, Th38 ; hence width (AutMt ((a * f),b1,b2)) = width (AutMt (f,b1,b2)) ; ::_thesis: verum end; supposeA4: len b1 > 0 ; ::_thesis: width (AutMt ((a * f),b1,b2)) = width (AutMt (f,b1,b2)) hence width (AutMt ((a * f),b1,b2)) = len b2 by Th39 .= width (AutMt (f,b1,b2)) by A4, Th39 ; ::_thesis: verum end; end; end; then A5: width (AutMt ((a * f),b1,b2)) = width (a * (AutMt (f,b1,b2))) by MATRIX_3:def_5; A6: len (AutMt ((a * f),b1,b2)) = len b1 by Def8 .= len (AutMt (f,b1,b2)) by Def8 ; then A7: dom (AutMt ((a * f),b1,b2)) = dom (AutMt (f,b1,b2)) by FINSEQ_3:29; A8: for i, j being Nat st [i,j] in Indices (AutMt ((a * f),b1,b2)) holds (AutMt ((a * f),b1,b2)) * (i,j) = (a * (AutMt (f,b1,b2))) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (AutMt ((a * f),b1,b2)) implies (AutMt ((a * f),b1,b2)) * (i,j) = (a * (AutMt (f,b1,b2))) * (i,j) ) assume A9: [i,j] in Indices (AutMt ((a * f),b1,b2)) ; ::_thesis: (AutMt ((a * f),b1,b2)) * (i,j) = (a * (AutMt (f,b1,b2))) * (i,j) then A10: [i,j] in [:(dom (AutMt ((a * f),b1,b2))),(Seg (width (AutMt ((a * f),b1,b2)))):] by MATRIX_1:def_4; then A11: [i,j] in Indices (AutMt (f,b1,b2)) by A7, A2, MATRIX_1:def_4; (AutMt ((a * f),b1,b2)) * (i,j) = a * ((AutMt (f,b1,b2)) * (i,j)) proof consider p2 being FinSequence of K such that A12: p2 = (AutMt (f,b1,b2)) . i and A13: (AutMt (f,b1,b2)) * (i,j) = p2 . j by A11, MATRIX_1:def_5; A14: i in dom (AutMt ((a * f),b1,b2)) by A10, ZFMISC_1:87; then A15: i in dom b1 by Lm3; then i in dom (AutMt (f,b1,b2)) by Lm3; then A16: p2 = (AutMt (f,b1,b2)) /. i by A12, PARTFUN1:def_6 .= (f . (b1 /. i)) |-- b2 by A15, Def8 ; reconsider b4 = rng b2 as Basis of V2 by Def2; consider p1 being FinSequence of K such that A17: p1 = (AutMt ((a * f),b1,b2)) . i and A18: (AutMt ((a * f),b1,b2)) * (i,j) = p1 . j by A9, MATRIX_1:def_5; consider KL1 being Linear_Combination of V2 such that A19: ( (a * f) . (b1 /. i) = Sum KL1 & Carrier KL1 c= rng b2 ) and A20: for t being Nat st 1 <= t & t <= len (((a * f) . (b1 /. i)) |-- b2) holds (((a * f) . (b1 /. i)) |-- b2) /. t = KL1 . (b2 /. t) by Def7; consider KL2 being Linear_Combination of V2 such that A21: ( f . (b1 /. i) = Sum KL2 & Carrier KL2 c= rng b2 ) and A22: for t being Nat st 1 <= t & t <= len ((f . (b1 /. i)) |-- b2) holds ((f . (b1 /. i)) |-- b2) /. t = KL2 . (b2 /. t) by Def7; ( b4 is linearly-independent & (a * f) . (b1 /. i) = a * (f . (b1 /. i)) ) by Def4, VECTSP_7:def_3; then A23: KL1 . (b2 /. j) = (a * KL2) . (b2 /. j) by A1, A19, A21, Th7 .= a * (KL2 . (b2 /. j)) by VECTSP_6:def_9 ; A24: j in Seg (width (AutMt ((a * f),b1,b2))) by A10, ZFMISC_1:87; then A25: 1 <= j by FINSEQ_1:1; len b1 = len (AutMt ((a * f),b1,b2)) by Def8; then dom b1 = dom (AutMt ((a * f),b1,b2)) by FINSEQ_3:29; then dom b1 <> {} by A10, ZFMISC_1:87; then Seg (len b1) <> {} by FINSEQ_1:def_3; then len b1 > 0 ; then A26: j in Seg (len b2) by A24, Th39; then A27: j <= len b2 by FINSEQ_1:1; then j <= len ((f . (b1 /. i)) |-- b2) by Def7; then A28: p2 /. j = KL2 . (b2 /. j) by A25, A16, A22; A29: j in dom b2 by A26, FINSEQ_1:def_3; then j in dom ((f . (b1 /. i)) |-- b2) by Lm1; then A30: (AutMt (f,b1,b2)) * (i,j) = p2 /. j by A13, A16, PARTFUN1:def_6; A31: p1 = (AutMt ((a * f),b1,b2)) /. i by A17, A14, PARTFUN1:def_6 .= ((a * f) . (b1 /. i)) |-- b2 by A15, Def8 ; then A32: j in dom p1 by A29, Lm1; j <= len (((a * f) . (b1 /. i)) |-- b2) by A27, Def7; then p1 /. j = KL1 . (b2 /. j) by A25, A31, A20; hence (AutMt ((a * f),b1,b2)) * (i,j) = a * ((AutMt (f,b1,b2)) * (i,j)) by A18, A32, A30, A28, A23, PARTFUN1:def_6; ::_thesis: verum end; hence (AutMt ((a * f),b1,b2)) * (i,j) = (a * (AutMt (f,b1,b2))) * (i,j) by A11, MATRIX_3:def_5; ::_thesis: verum end; len (AutMt ((a * f),b1,b2)) = len (a * (AutMt (f,b1,b2))) by A6, MATRIX_3:def_5; hence AutMt ((a * f),b1,b2) = a * (AutMt (f,b1,b2)) by A5, A8, MATRIX_1:21; ::_thesis: verum end;