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