:: MATRIXC1 semantic presentation
begin
definition
let M be Matrix of COMPLEX;
funcM *' -> Matrix of COMPLEX means :Def1: :: MATRIXC1:def 1
( len it = len M & width it = width M & ( for i, j being Nat st [i,j] in Indices M holds
it * (i,j) = (M * (i,j)) *' ) );
existence
ex b1 being Matrix of COMPLEX st
( len b1 = len M & width b1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
b1 * (i,j) = (M * (i,j)) *' ) )
proof
deffunc H1( Nat, Nat) -> Element of COMPLEX = (M * ($1,$2)) *' ;
consider M1 being Matrix of len M, width M, COMPLEX such that
A1: for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = H1(i,j) from MATRIX_1:sch_1();
take M1 ; ::_thesis: ( len M1 = len M & width M1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
M1 * (i,j) = (M * (i,j)) *' ) )
A2: len M1 = len M by MATRIX_1:def_2;
A3: now__::_thesis:_(_(_len_M_=_0_&_width_M1_=_width_M_)_or_(_len_M_>_0_&_width_M1_=_width_M_)_)
percases ( len M = 0 or len M > 0 ) ;
caseA4: len M = 0 ; ::_thesis: width M1 = width M
then width M1 = 0 by A2, MATRIX_1:def_3;
hence width M1 = width M by A4, MATRIX_1:def_3; ::_thesis: verum
end;
case len M > 0 ; ::_thesis: width M1 = width M
hence width M1 = width M by MATRIX_1:23; ::_thesis: verum
end;
end;
end;
dom M = dom M1 by A2, FINSEQ_3:29;
hence ( len M1 = len M & width M1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
M1 * (i,j) = (M * (i,j)) *' ) ) by A1, A3, MATRIX_1:def_2; ::_thesis: verum
end;
uniqueness
for b1, b2 being Matrix of COMPLEX st len b1 = len M & width b1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
b1 * (i,j) = (M * (i,j)) *' ) & len b2 = len M & width b2 = width M & ( for i, j being Nat st [i,j] in Indices M holds
b2 * (i,j) = (M * (i,j)) *' ) holds
b1 = b2
proof
let M1, M2 be Matrix of COMPLEX; ::_thesis: ( len M1 = len M & width M1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
M1 * (i,j) = (M * (i,j)) *' ) & len M2 = len M & width M2 = width M & ( for i, j being Nat st [i,j] in Indices M holds
M2 * (i,j) = (M * (i,j)) *' ) implies M1 = M2 )
assume that
A5: len M1 = len M and
A6: width M1 = width M and
A7: for i, j being Nat st [i,j] in Indices M holds
M1 * (i,j) = (M * (i,j)) *' and
A8: len M2 = len M and
A9: width M2 = width M and
A10: for i, j being Nat st [i,j] in Indices M holds
M2 * (i,j) = (M * (i,j)) *' ; ::_thesis: M1 = M2
now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_M1_holds_
M1_*_(i,j)_=_M2_*_(i,j)
let i, j be Nat; ::_thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) )
assume A11: [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) = M2 * (i,j)
A12: dom M1 = dom M by A5, FINSEQ_3:29;
hence M1 * (i,j) = (M * (i,j)) *' by A6, A7, A11
.= M2 * (i,j) by A6, A10, A11, A12 ;
::_thesis: verum
end;
hence M1 = M2 by A5, A6, A8, A9, MATRIX_1:21; ::_thesis: verum
end;
involutiveness
for b1, b2 being Matrix of COMPLEX st len b1 = len b2 & width b1 = width b2 & ( for i, j being Nat st [i,j] in Indices b2 holds
b1 * (i,j) = (b2 * (i,j)) *' ) holds
( len b2 = len b1 & width b2 = width b1 & ( for i, j being Nat st [i,j] in Indices b1 holds
b2 * (i,j) = (b1 * (i,j)) *' ) )
proof
let N, M be Matrix of COMPLEX; ::_thesis: ( len N = len M & width N = width M & ( for i, j being Nat st [i,j] in Indices M holds
N * (i,j) = (M * (i,j)) *' ) implies ( len M = len N & width M = width N & ( for i, j being Nat st [i,j] in Indices N holds
M * (i,j) = (N * (i,j)) *' ) ) )
assume that
A13: len N = len M and
A14: width N = width M and
A15: for i, j being Nat st [i,j] in Indices M holds
N * (i,j) = (M * (i,j)) *' ; ::_thesis: ( len M = len N & width M = width N & ( for i, j being Nat st [i,j] in Indices N holds
M * (i,j) = (N * (i,j)) *' ) )
thus len M = len N by A13; ::_thesis: ( width M = width N & ( for i, j being Nat st [i,j] in Indices N holds
M * (i,j) = (N * (i,j)) *' ) )
thus width M = width N by A14; ::_thesis: for i, j being Nat st [i,j] in Indices N holds
M * (i,j) = (N * (i,j)) *'
let i, j be Nat; ::_thesis: ( [i,j] in Indices N implies M * (i,j) = (N * (i,j)) *' )
assume A16: [i,j] in Indices N ; ::_thesis: M * (i,j) = (N * (i,j)) *'
( 1 <= i & i <= len M & 1 <= j & j <= width M ) by A13, A14, A16, MATRIX_1:38;
then A17: [i,j] in Indices M by MATRIX_1:36;
thus M * (i,j) = ((M * (i,j)) *') *'
.= (N * (i,j)) *' by A17, A15 ; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines *' MATRIXC1:def_1_:_
for M, b2 being Matrix of COMPLEX holds
( b2 = M *' iff ( len b2 = len M & width b2 = width M & ( for i, j being Nat st [i,j] in Indices M holds
b2 * (i,j) = (M * (i,j)) *' ) ) );
theorem Th1: :: MATRIXC1:1
for i, j being Nat
for M being tabular FinSequence holds
( [i,j] in Indices M iff ( 1 <= i & i <= len M & 1 <= j & j <= width M ) )
proof
let i, j be Nat; ::_thesis: for M being tabular FinSequence holds
( [i,j] in Indices M iff ( 1 <= i & i <= len M & 1 <= j & j <= width M ) )
let M be tabular FinSequence; ::_thesis: ( [i,j] in Indices M iff ( 1 <= i & i <= len M & 1 <= j & j <= width M ) )
thus ( [i,j] in Indices M implies ( 1 <= i & i <= len M & 1 <= j & j <= width M ) ) ::_thesis: ( 1 <= i & i <= len M & 1 <= j & j <= width M implies [i,j] in Indices M )
proof
assume A1: [i,j] in Indices M ; ::_thesis: ( 1 <= i & i <= len M & 1 <= j & j <= width M )
then [i,j] in [:(Seg (len M)),(Seg (width M)):] by FINSEQ_1:def_3;
then A2: i in Seg (len M) by ZFMISC_1:87;
j in Seg (width M) by A1, ZFMISC_1:87;
hence ( 1 <= i & i <= len M & 1 <= j & j <= width M ) by A2, FINSEQ_1:1; ::_thesis: verum
end;
assume that
A3: 1 <= i and
A4: i <= len M and
A5: 1 <= j and
A6: j <= width M ; ::_thesis: [i,j] in Indices M
A7: j in Seg (width M) by A5, A6, FINSEQ_1:1;
i in dom M by A3, A4, FINSEQ_3:25;
hence [i,j] in Indices M by A7, ZFMISC_1:87; ::_thesis: verum
end;
theorem :: MATRIXC1:2
canceled;
theorem Th3: :: MATRIXC1:3
for a being complex number
for M being Matrix of COMPLEX holds
( len (a * M) = len M & width (a * M) = width M )
proof
let a be complex number ; ::_thesis: for M being Matrix of COMPLEX holds
( len (a * M) = len M & width (a * M) = width M )
let M be Matrix of COMPLEX; ::_thesis: ( len (a * M) = len M & width (a * M) = width M )
a in COMPLEX by XCMPLX_0:def_2;
then reconsider ea = a as Element of F_Complex by COMPLFLD:def_1;
A1: width (a * M) = width (COMPLEX2Field (a * M)) by MATRIX_5:7
.= width (COMPLEX2Field (Field2COMPLEX (ea * (COMPLEX2Field M)))) by MATRIX_5:def_7
.= width (ea * (COMPLEX2Field M)) by MATRIX_5:6
.= width (COMPLEX2Field M) by MATRIX_3:def_5
.= width M by MATRIX_5:def_1 ;
len (a * M) = len (COMPLEX2Field (a * M)) by MATRIX_5:7
.= len (COMPLEX2Field (Field2COMPLEX (ea * (COMPLEX2Field M)))) by MATRIX_5:def_7
.= len (ea * (COMPLEX2Field M)) by MATRIX_5:6
.= len (COMPLEX2Field M) by MATRIX_3:def_5
.= len M by MATRIX_5:def_1 ;
hence ( len (a * M) = len M & width (a * M) = width M ) by A1; ::_thesis: verum
end;
theorem Th4: :: MATRIXC1:4
for i, j being Nat
for a being complex number
for M being Matrix of COMPLEX st [i,j] in Indices M holds
(a * M) * (i,j) = a * (M * (i,j))
proof
let i, j be Nat; ::_thesis: for a being complex number
for M being Matrix of COMPLEX st [i,j] in Indices M holds
(a * M) * (i,j) = a * (M * (i,j))
let a be complex number ; ::_thesis: for M being Matrix of COMPLEX st [i,j] in Indices M holds
(a * M) * (i,j) = a * (M * (i,j))
let M be Matrix of COMPLEX; ::_thesis: ( [i,j] in Indices M implies (a * M) * (i,j) = a * (M * (i,j)) )
reconsider m1 = COMPLEX2Field M as Matrix of COMPLEX by COMPLFLD:def_1;
A1: M * (i,j) = m1 * (i,j) by MATRIX_5:def_1
.= (COMPLEX2Field M) * (i,j) by COMPLFLD:def_1 ;
assume [i,j] in Indices M ; ::_thesis: (a * M) * (i,j) = a * (M * (i,j))
then A2: [i,j] in Indices (COMPLEX2Field M) by MATRIX_5:def_1;
a in COMPLEX by XCMPLX_0:def_2;
then reconsider aa = a as Element of F_Complex by COMPLFLD:def_1;
reconsider m = COMPLEX2Field (a * M) as Matrix of COMPLEX by COMPLFLD:def_1;
A3: COMPLEX2Field (a * M) = COMPLEX2Field (Field2COMPLEX (aa * (COMPLEX2Field M))) by MATRIX_5:def_7
.= aa * (COMPLEX2Field M) by MATRIX_5:6 ;
(a * M) * (i,j) = m * (i,j) by MATRIX_5:def_1
.= (aa * (COMPLEX2Field M)) * (i,j) by A3, COMPLFLD:def_1
.= aa * ((COMPLEX2Field M) * (i,j)) by A2, MATRIX_3:def_5
.= a * ((COMPLEX2Field M) * (i,j)) ;
hence (a * M) * (i,j) = a * (M * (i,j)) by A1; ::_thesis: verum
end;
theorem Th5: :: MATRIXC1:5
for a being complex number
for M being Matrix of COMPLEX holds (a * M) *' = (a *') * (M *')
proof
let a be complex number ; ::_thesis: for M being Matrix of COMPLEX holds (a * M) *' = (a *') * (M *')
let M be Matrix of COMPLEX; ::_thesis: (a * M) *' = (a *') * (M *')
reconsider aa = a as Element of COMPLEX by XCMPLX_0:def_2;
A1: len (a * M) = len M by Th3;
A2: width (a * M) = width M by Th3;
A3: width M = width (M *') by Def1;
A4: len ((a * M) *') = len (a * M) by Def1;
A5: width ((a * M) *') = width (a * M) by Def1;
A6: len M = len (M *') by Def1;
A7: now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_((a_*_M)_*')_holds_
((a_*_M)_*')_*_(i,j)_=_((a_*')_*_(M_*'))_*_(i,j)
let i, j be Nat; ::_thesis: ( [i,j] in Indices ((a * M) *') implies ((a * M) *') * (i,j) = ((a *') * (M *')) * (i,j) )
assume A8: [i,j] in Indices ((a * M) *') ; ::_thesis: ((a * M) *') * (i,j) = ((a *') * (M *')) * (i,j)
then A9: 1 <= i by Th1;
A10: 1 <= j by A8, Th1;
A11: j <= width (a * M) by A5, A8, Th1;
A12: i <= len (a * M) by A4, A8, Th1;
then A13: [i,j] in Indices M by A1, A2, A9, A10, A11, Th1;
A14: [i,j] in Indices (M *') by A1, A6, A2, A3, A9, A12, A10, A11, Th1;
[i,j] in Indices (a * M) by A9, A12, A10, A11, Th1;
then ((a * M) *') * (i,j) = ((a * M) * (i,j)) *' by Def1;
hence ((a * M) *') * (i,j) = (aa * (M * (i,j))) *' by A13, Th4
.= (aa *') * ((M * (i,j)) *') by COMPLEX1:35
.= (a *') * ((M *') * (i,j)) by A13, Def1
.= ((a *') * (M *')) * (i,j) by A14, Th4 ;
::_thesis: verum
end;
len ((a *') * (M *')) = len (M *') by Th3;
then len ((a *') * (M *')) = len M by Def1;
then A15: len ((a * M) *') = len ((a *') * (M *')) by A4, Th3;
width ((a *') * (M *')) = width (M *') by Th3;
then width ((a *') * (M *')) = width M by Def1;
hence (a * M) *' = (a *') * (M *') by A15, A5, A7, Th3, MATRIX_1:21; ::_thesis: verum
end;
theorem Th6: :: MATRIXC1:6
for M1, M2 being Matrix of COMPLEX holds
( len (M1 + M2) = len M1 & width (M1 + M2) = width M1 )
proof
let M1, M2 be Matrix of COMPLEX; ::_thesis: ( len (M1 + M2) = len M1 & width (M1 + M2) = width M1 )
A1: width (M1 + M2) = width (COMPLEX2Field (M1 + M2)) by MATRIX_5:7
.= width (COMPLEX2Field (Field2COMPLEX ((COMPLEX2Field M1) + (COMPLEX2Field M2)))) by MATRIX_5:def_3
.= width ((COMPLEX2Field M1) + (COMPLEX2Field M2)) by MATRIX_5:6
.= width (COMPLEX2Field M1) by MATRIX_3:def_3
.= width M1 by MATRIX_5:def_1 ;
len (M1 + M2) = len (COMPLEX2Field (M1 + M2)) by MATRIX_5:7
.= len (COMPLEX2Field (Field2COMPLEX ((COMPLEX2Field M1) + (COMPLEX2Field M2)))) by MATRIX_5:def_3
.= len ((COMPLEX2Field M1) + (COMPLEX2Field M2)) by MATRIX_5:6
.= len (COMPLEX2Field M1) by MATRIX_3:def_3
.= len M1 by MATRIX_5:def_1 ;
hence ( len (M1 + M2) = len M1 & width (M1 + M2) = width M1 ) by A1; ::_thesis: verum
end;
theorem Th7: :: MATRIXC1:7
for i, j being Nat
for M1, M2 being Matrix of COMPLEX st [i,j] in Indices M1 holds
(M1 + M2) * (i,j) = (M1 * (i,j)) + (M2 * (i,j))
proof
let i, j be Nat; ::_thesis: for M1, M2 being Matrix of COMPLEX st [i,j] in Indices M1 holds
(M1 + M2) * (i,j) = (M1 * (i,j)) + (M2 * (i,j))
let M1, M2 be Matrix of COMPLEX; ::_thesis: ( [i,j] in Indices M1 implies (M1 + M2) * (i,j) = (M1 * (i,j)) + (M2 * (i,j)) )
A1: COMPLEX2Field (M1 + M2) = COMPLEX2Field (Field2COMPLEX ((COMPLEX2Field M1) + (COMPLEX2Field M2))) by MATRIX_5:def_3
.= (COMPLEX2Field M1) + (COMPLEX2Field M2) by MATRIX_5:6 ;
reconsider m1 = COMPLEX2Field M1, m2 = COMPLEX2Field M2 as Matrix of COMPLEX by COMPLFLD:def_1;
set m = COMPLEX2Field (M1 + M2);
reconsider m9 = COMPLEX2Field (M1 + M2) as Matrix of COMPLEX by COMPLFLD:def_1;
A2: M1 * (i,j) = m1 * (i,j) by MATRIX_5:def_1
.= (COMPLEX2Field M1) * (i,j) by COMPLFLD:def_1 ;
assume [i,j] in Indices M1 ; ::_thesis: (M1 + M2) * (i,j) = (M1 * (i,j)) + (M2 * (i,j))
then A3: [i,j] in Indices (COMPLEX2Field M1) by MATRIX_5:def_1;
A4: M2 * (i,j) = m2 * (i,j) by MATRIX_5:def_1
.= (COMPLEX2Field M2) * (i,j) by COMPLFLD:def_1 ;
(M1 + M2) * (i,j) = m9 * (i,j) by MATRIX_5:def_1
.= (COMPLEX2Field (M1 + M2)) * (i,j) by COMPLFLD:def_1
.= ((COMPLEX2Field M1) * (i,j)) + ((COMPLEX2Field M2) * (i,j)) by A1, A3, MATRIX_3:def_3 ;
hence (M1 + M2) * (i,j) = (M1 * (i,j)) + (M2 * (i,j)) by A2, A4; ::_thesis: verum
end;
theorem :: MATRIXC1:8
for M1, M2 being Matrix of COMPLEX st len M1 = len M2 & width M1 = width M2 holds
(M1 + M2) *' = (M1 *') + (M2 *')
proof
let M1, M2 be Matrix of COMPLEX; ::_thesis: ( len M1 = len M2 & width M1 = width M2 implies (M1 + M2) *' = (M1 *') + (M2 *') )
assume that
A1: len M1 = len M2 and
A2: width M1 = width M2 ; ::_thesis: (M1 + M2) *' = (M1 *') + (M2 *')
A3: len (M1 + M2) = len M1 by Th6;
A4: width ((M1 + M2) *') = width (M1 + M2) by Def1;
A5: width (M1 + M2) = width M1 by Th6;
A6: len ((M1 + M2) *') = len (M1 + M2) by Def1;
A7: now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_((M1_+_M2)_*')_holds_
((M1_+_M2)_*')_*_(i,j)_=_((M1_*')_+_(M2_*'))_*_(i,j)
let i, j be Nat; ::_thesis: ( [i,j] in Indices ((M1 + M2) *') implies ((M1 + M2) *') * (i,j) = ((M1 *') + (M2 *')) * (i,j) )
assume A8: [i,j] in Indices ((M1 + M2) *') ; ::_thesis: ((M1 + M2) *') * (i,j) = ((M1 *') + (M2 *')) * (i,j)
then A9: 1 <= j by Th1;
A10: 1 <= i by A8, Th1;
A11: j <= width (M1 + M2) by A4, A8, Th1;
then A12: j <= width (M1 *') by A5, Def1;
A13: i <= len (M1 + M2) by A6, A8, Th1;
then i <= len (M1 *') by A3, Def1;
then A14: [i,j] in Indices (M1 *') by A9, A10, A12, Th1;
A15: 1 <= i by A8, Th1;
then A16: [i,j] in Indices M1 by A3, A5, A13, A9, A11, Th1;
A17: [i,j] in Indices M2 by A1, A2, A3, A5, A15, A13, A9, A11, Th1;
[i,j] in Indices (M1 + M2) by A15, A13, A9, A11, Th1;
then ((M1 + M2) *') * (i,j) = ((M1 + M2) * (i,j)) *' by Def1;
hence ((M1 + M2) *') * (i,j) = ((M1 * (i,j)) + (M2 * (i,j))) *' by A16, Th7
.= ((M1 * (i,j)) *') + ((M2 * (i,j)) *') by COMPLEX1:32
.= ((M1 *') * (i,j)) + ((M2 * (i,j)) *') by A16, Def1
.= ((M1 *') * (i,j)) + ((M2 *') * (i,j)) by A17, Def1
.= ((M1 *') + (M2 *')) * (i,j) by A14, Th7 ;
::_thesis: verum
end;
A18: width (M1 *') = width M1 by Def1;
A19: width ((M1 *') + (M2 *')) = width (M1 *') by Th6;
A20: len ((M1 *') + (M2 *')) = len (M1 *') by Th6;
len (M1 *') = len M1 by Def1;
hence (M1 + M2) *' = (M1 *') + (M2 *') by A6, A3, A20, A4, A5, A19, A18, A7, MATRIX_1:21; ::_thesis: verum
end;
theorem Th9: :: MATRIXC1:9
for M being Matrix of COMPLEX holds
( len (- M) = len M & width (- M) = width M )
proof
let M be Matrix of COMPLEX; ::_thesis: ( len (- M) = len M & width (- M) = width M )
A1: width (- M) = width (COMPLEX2Field (- M)) by MATRIX_5:7
.= width (COMPLEX2Field (Field2COMPLEX (- (COMPLEX2Field M)))) by MATRIX_5:def_4
.= width (- (COMPLEX2Field M)) by MATRIX_5:6
.= width (COMPLEX2Field M) by MATRIX_3:def_2
.= width M by MATRIX_5:def_1 ;
len (- M) = len (COMPLEX2Field (- M)) by MATRIX_5:7
.= len (COMPLEX2Field (Field2COMPLEX (- (COMPLEX2Field M)))) by MATRIX_5:def_4
.= len (- (COMPLEX2Field M)) by MATRIX_5:6
.= len (COMPLEX2Field M) by MATRIX_3:def_2
.= len M by MATRIX_5:def_1 ;
hence ( len (- M) = len M & width (- M) = width M ) by A1; ::_thesis: verum
end;
theorem Th10: :: MATRIXC1:10
for i, j being Nat
for M being Matrix of COMPLEX st [i,j] in Indices M holds
(- M) * (i,j) = - (M * (i,j))
proof
let i, j be Nat; ::_thesis: for M being Matrix of COMPLEX st [i,j] in Indices M holds
(- M) * (i,j) = - (M * (i,j))
let M be Matrix of COMPLEX; ::_thesis: ( [i,j] in Indices M implies (- M) * (i,j) = - (M * (i,j)) )
A1: COMPLEX2Field (- M) = COMPLEX2Field (Field2COMPLEX (- (COMPLEX2Field M))) by MATRIX_5:def_4
.= - (COMPLEX2Field M) by MATRIX_5:6 ;
reconsider m = COMPLEX2Field (- M) as Matrix of COMPLEX by COMPLFLD:def_1;
reconsider m1 = COMPLEX2Field M as Matrix of COMPLEX by COMPLFLD:def_1;
A2: M * (i,j) = m1 * (i,j) by MATRIX_5:def_1
.= (COMPLEX2Field M) * (i,j) by COMPLFLD:def_1 ;
assume [i,j] in Indices M ; ::_thesis: (- M) * (i,j) = - (M * (i,j))
then A3: [i,j] in Indices (COMPLEX2Field M) by MATRIX_5:def_1;
(- M) * (i,j) = m * (i,j) by MATRIX_5:def_1
.= (- (COMPLEX2Field M)) * (i,j) by A1, COMPLFLD:def_1
.= - ((COMPLEX2Field M) * (i,j)) by A3, MATRIX_3:def_2 ;
hence (- M) * (i,j) = - (M * (i,j)) by A2, COMPLFLD:2; ::_thesis: verum
end;
theorem Th11: :: MATRIXC1:11
for M being Matrix of COMPLEX holds (- 1) * M = - M
proof
let M be Matrix of COMPLEX; ::_thesis: (- 1) * M = - M
A1: width (- M) = width M by Th9;
A2: width ((- 1) * M) = width M by Th3;
A3: len ((- 1) * M) = len M by Th3;
A4: now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_((-_1)_*_M)_holds_
((-_1)_*_M)_*_(i,j)_=_(-_M)_*_(i,j)
let i, j be Nat; ::_thesis: ( [i,j] in Indices ((- 1) * M) implies ((- 1) * M) * (i,j) = (- M) * (i,j) )
assume A5: [i,j] in Indices ((- 1) * M) ; ::_thesis: ((- 1) * M) * (i,j) = (- M) * (i,j)
then A6: 1 <= i by Th1;
A7: 1 <= j by A5, Th1;
A8: j <= width M by A2, A5, Th1;
i <= len M by A3, A5, Th1;
then A9: [i,j] in Indices M by A6, A7, A8, Th1;
hence ((- 1) * M) * (i,j) = (- 1) * (M * (i,j)) by Th4
.= - (M * (i,j))
.= (- M) * (i,j) by A9, Th10 ;
::_thesis: verum
end;
len (- M) = len M by Th9;
hence (- 1) * M = - M by A3, A1, A2, A4, MATRIX_1:21; ::_thesis: verum
end;
theorem :: MATRIXC1:12
for M being Matrix of COMPLEX holds (- M) *' = - (M *')
proof
let M be Matrix of COMPLEX; ::_thesis: (- M) *' = - (M *')
(- M) *' = ((- 1) * M) *' by Th11
.= ((- 1r) *') * (M *') by Th5, COMPLEX1:def_4
.= (- 1) * (M *') by COMPLEX1:30, COMPLEX1:33, COMPLEX1:def_4
.= - (M *') by Th11 ;
hence (- M) *' = - (M *') ; ::_thesis: verum
end;
theorem Th13: :: MATRIXC1:13
for M1, M2 being Matrix of COMPLEX holds
( len (M1 - M2) = len M1 & width (M1 - M2) = width M1 )
proof
let M1, M2 be Matrix of COMPLEX; ::_thesis: ( len (M1 - M2) = len M1 & width (M1 - M2) = width M1 )
A1: width (M1 - M2) = width (COMPLEX2Field (M1 - M2)) by MATRIX_5:7
.= width (COMPLEX2Field (Field2COMPLEX ((COMPLEX2Field M1) - (COMPLEX2Field M2)))) by MATRIX_5:def_5
.= width ((COMPLEX2Field M1) - (COMPLEX2Field M2)) by MATRIX_5:6
.= width ((COMPLEX2Field M1) + (- (COMPLEX2Field M2))) by MATRIX_4:def_1
.= width (COMPLEX2Field M1) by MATRIX_3:def_3
.= width M1 by MATRIX_5:def_1 ;
len (M1 - M2) = len (COMPLEX2Field (M1 - M2)) by MATRIX_5:7
.= len (COMPLEX2Field (Field2COMPLEX ((COMPLEX2Field M1) - (COMPLEX2Field M2)))) by MATRIX_5:def_5
.= len ((COMPLEX2Field M1) - (COMPLEX2Field M2)) by MATRIX_5:6
.= len ((COMPLEX2Field M1) + (- (COMPLEX2Field M2))) by MATRIX_4:def_1
.= len (COMPLEX2Field M1) by MATRIX_3:def_3
.= len M1 by MATRIX_5:def_1 ;
hence ( len (M1 - M2) = len M1 & width (M1 - M2) = width M1 ) by A1; ::_thesis: verum
end;
theorem Th14: :: MATRIXC1:14
for i, j being Nat
for M1, M2 being Matrix of COMPLEX st len M1 = len M2 & width M1 = width M2 & [i,j] in Indices M1 holds
(M1 - M2) * (i,j) = (M1 * (i,j)) - (M2 * (i,j))
proof
let i, j be Nat; ::_thesis: for M1, M2 being Matrix of COMPLEX st len M1 = len M2 & width M1 = width M2 & [i,j] in Indices M1 holds
(M1 - M2) * (i,j) = (M1 * (i,j)) - (M2 * (i,j))
let M1, M2 be Matrix of COMPLEX; ::_thesis: ( len M1 = len M2 & width M1 = width M2 & [i,j] in Indices M1 implies (M1 - M2) * (i,j) = (M1 * (i,j)) - (M2 * (i,j)) )
assume that
A1: len M1 = len M2 and
A2: width M1 = width M2 and
A3: [i,j] in Indices M1 ; ::_thesis: (M1 - M2) * (i,j) = (M1 * (i,j)) - (M2 * (i,j))
A4: j <= width M2 by A2, A3, Th1;
A5: 1 <= j by A3, Th1;
A6: 1 <= i by A3, Th1;
i <= len M2 by A1, A3, Th1;
then [i,j] in Indices M2 by A6, A5, A4, Th1;
then A7: [i,j] in Indices (COMPLEX2Field M2) by MATRIX_5:def_1;
reconsider m2 = COMPLEX2Field M2 as Matrix of COMPLEX by COMPLFLD:def_1;
reconsider m1 = COMPLEX2Field M1 as Matrix of COMPLEX by COMPLFLD:def_1;
set m = COMPLEX2Field (M1 - M2);
A8: COMPLEX2Field (M1 - M2) = COMPLEX2Field (Field2COMPLEX ((COMPLEX2Field M1) - (COMPLEX2Field M2))) by MATRIX_5:def_5
.= (COMPLEX2Field M1) - (COMPLEX2Field M2) by MATRIX_5:6 ;
reconsider m9 = COMPLEX2Field (M1 - M2) as Matrix of COMPLEX by COMPLFLD:def_1;
A9: M1 * (i,j) = m1 * (i,j) by MATRIX_5:def_1
.= (COMPLEX2Field M1) * (i,j) by COMPLFLD:def_1 ;
A10: [i,j] in Indices (COMPLEX2Field M1) by A3, MATRIX_5:def_1;
M2 * (i,j) = m2 * (i,j) by MATRIX_5:def_1
.= (COMPLEX2Field M2) * (i,j) by COMPLFLD:def_1 ;
then A11: - (M2 * (i,j)) = - ((COMPLEX2Field M2) * (i,j)) by COMPLFLD:2;
(M1 - M2) * (i,j) = m9 * (i,j) by MATRIX_5:def_1
.= (COMPLEX2Field (M1 - M2)) * (i,j) by COMPLFLD:def_1
.= ((COMPLEX2Field M1) + (- (COMPLEX2Field M2))) * (i,j) by A8, MATRIX_4:def_1
.= ((COMPLEX2Field M1) * (i,j)) + ((- (COMPLEX2Field M2)) * (i,j)) by A10, MATRIX_3:def_3
.= ((COMPLEX2Field M1) * (i,j)) + (- ((COMPLEX2Field M2) * (i,j))) by A7, MATRIX_3:def_2 ;
hence (M1 - M2) * (i,j) = (M1 * (i,j)) - (M2 * (i,j)) by A9, A11; ::_thesis: verum
end;
theorem :: MATRIXC1:15
for M1, M2 being Matrix of COMPLEX st len M1 = len M2 & width M1 = width M2 holds
(M1 - M2) *' = (M1 *') - (M2 *')
proof
let M1, M2 be Matrix of COMPLEX; ::_thesis: ( len M1 = len M2 & width M1 = width M2 implies (M1 - M2) *' = (M1 *') - (M2 *') )
assume that
A1: len M1 = len M2 and
A2: width M1 = width M2 ; ::_thesis: (M1 - M2) *' = (M1 *') - (M2 *')
A3: len ((M1 - M2) *') = len (M1 - M2) by Def1;
A4: width ((M1 - M2) *') = width (M1 - M2) by Def1;
A5: width (M1 - M2) = width M1 by Th13;
A6: width (M1 *') = width M1 by Def1;
A7: len (M1 *') = len M1 by Def1;
A8: width (M2 *') = width M2 by Def1;
A9: len (M1 - M2) = len M1 by Th13;
A10: len (M2 *') = len M2 by Def1;
A11: now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_((M1_-_M2)_*')_holds_
((M1_-_M2)_*')_*_(i,j)_=_((M1_*')_-_(M2_*'))_*_(i,j)
let i, j be Nat; ::_thesis: ( [i,j] in Indices ((M1 - M2) *') implies ((M1 - M2) *') * (i,j) = ((M1 *') - (M2 *')) * (i,j) )
assume A12: [i,j] in Indices ((M1 - M2) *') ; ::_thesis: ((M1 - M2) *') * (i,j) = ((M1 *') - (M2 *')) * (i,j)
then A13: 1 <= j by Th1;
A14: 1 <= i by A12, Th1;
A15: j <= width (M1 - M2) by A4, A12, Th1;
then A16: j <= width (M1 *') by A5, Def1;
A17: i <= len (M1 - M2) by A3, A12, Th1;
then i <= len (M1 *') by A9, Def1;
then A18: [i,j] in Indices (M1 *') by A13, A14, A16, Th1;
A19: 1 <= i by A12, Th1;
then A20: [i,j] in Indices M1 by A9, A5, A17, A13, A15, Th1;
A21: [i,j] in Indices M2 by A1, A2, A9, A5, A19, A17, A13, A15, Th1;
[i,j] in Indices (M1 - M2) by A19, A17, A13, A15, Th1;
then ((M1 - M2) *') * (i,j) = ((M1 - M2) * (i,j)) *' by Def1;
hence ((M1 - M2) *') * (i,j) = ((M1 * (i,j)) - (M2 * (i,j))) *' by A1, A2, A20, Th14
.= ((M1 * (i,j)) *') - ((M2 * (i,j)) *') by COMPLEX1:34
.= ((M1 *') * (i,j)) - ((M2 * (i,j)) *') by A20, Def1
.= ((M1 *') * (i,j)) - ((M2 *') * (i,j)) by A21, Def1
.= ((M1 *') - (M2 *')) * (i,j) by A1, A2, A7, A10, A6, A8, A18, Th14 ;
::_thesis: verum
end;
A22: width (M1 *') = width M1 by Def1;
A23: width ((M1 *') - (M2 *')) = width (M1 *') by Th13;
len ((M1 *') - (M2 *')) = len (M1 *') by Th13;
hence (M1 - M2) *' = (M1 *') - (M2 *') by A3, A7, A9, A4, A5, A23, A22, A11, MATRIX_1:21; ::_thesis: verum
end;
definition
let M be Matrix of COMPLEX;
funcM @" -> Matrix of COMPLEX equals :: MATRIXC1:def 2
(M @) *' ;
coherence
(M @) *' is Matrix of COMPLEX ;
end;
:: deftheorem defines @" MATRIXC1:def_2_:_
for M being Matrix of COMPLEX holds M @" = (M @) *' ;
definition
let x be FinSequence of COMPLEX ;
assume A1: len x > 0 ;
func FinSeq2Matrix x -> Matrix of COMPLEX means :: MATRIXC1:def 3
( len it = len x & width it = 1 & ( for j being Nat st j in Seg (len x) holds
it . j = <*(x . j)*> ) );
existence
ex b1 being Matrix of COMPLEX st
( len b1 = len x & width b1 = 1 & ( for j being Nat st j in Seg (len x) holds
b1 . j = <*(x . j)*> ) )
proof
reconsider n = len x as Element of NAT ;
deffunc H1( Nat) -> FinSequence of COMPLEX = <*(x . $1)*>;
consider M3 being FinSequence such that
A2: ( len M3 = n & ( for j being Nat st j in dom M3 holds
M3 . j = H1(j) ) ) from FINSEQ_1:sch_2();
for y being set st y in rng M3 holds
ex p being FinSequence of COMPLEX st
( y = p & len p = 1 )
proof
let y be set ; ::_thesis: ( y in rng M3 implies ex p being FinSequence of COMPLEX st
( y = p & len p = 1 ) )
assume y in rng M3 ; ::_thesis: ex p being FinSequence of COMPLEX st
( y = p & len p = 1 )
then consider z being set such that
A3: z in dom M3 and
A4: y = M3 . z by FUNCT_1:def_3;
reconsider z = z as Element of NAT by A3;
len <*(x . z)*> = 1 by FINSEQ_1:39;
hence ex p being FinSequence of COMPLEX st
( y = p & len p = 1 ) by A2, A3, A4; ::_thesis: verum
end;
then reconsider M2 = M3 as Matrix of COMPLEX by MATRIX_1:9;
for p being FinSequence of COMPLEX st p in rng M2 holds
len p = 1
proof
let p be FinSequence of COMPLEX ; ::_thesis: ( p in rng M2 implies len p = 1 )
assume p in rng M2 ; ::_thesis: len p = 1
then consider i being Nat such that
A5: i in dom M2 and
A6: M2 . i = p by FINSEQ_2:10;
len <*(x . i)*> = 1 by FINSEQ_1:39;
hence len p = 1 by A2, A5, A6; ::_thesis: verum
end;
then reconsider M1 = M2 as Matrix of len M2,1, COMPLEX by MATRIX_1:def_2;
take M2 ; ::_thesis: ( len M2 = len x & width M2 = 1 & ( for j being Nat st j in Seg (len x) holds
M2 . j = <*(x . j)*> ) )
A7: dom M3 = Seg n by A2, FINSEQ_1:def_3;
width M1 = 1 by A1, A2, MATRIX_1:23;
hence ( len M2 = len x & width M2 = 1 & ( for j being Nat st j in Seg (len x) holds
M2 . j = <*(x . j)*> ) ) by A2, A7; ::_thesis: verum
end;
uniqueness
for b1, b2 being Matrix of COMPLEX st len b1 = len x & width b1 = 1 & ( for j being Nat st j in Seg (len x) holds
b1 . j = <*(x . j)*> ) & len b2 = len x & width b2 = 1 & ( for j being Nat st j in Seg (len x) holds
b2 . j = <*(x . j)*> ) holds
b1 = b2
proof
let M1, M2 be Matrix of COMPLEX; ::_thesis: ( len M1 = len x & width M1 = 1 & ( for j being Nat st j in Seg (len x) holds
M1 . j = <*(x . j)*> ) & len M2 = len x & width M2 = 1 & ( for j being Nat st j in Seg (len x) holds
M2 . j = <*(x . j)*> ) implies M1 = M2 )
assume that
A8: len M1 = len x and
width M1 = 1 and
A9: for k being Nat st k in Seg (len x) holds
M1 . k = <*(x . k)*> and
A10: len M2 = len x and
width M2 = 1 and
A11: for k being Nat st k in Seg (len x) holds
M2 . k = <*(x . k)*> ; ::_thesis: M1 = M2
A12: dom M1 = Seg (len x) by A8, FINSEQ_1:def_3;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_M1_holds_
M1_._k_=_M2_._k
let k be Nat; ::_thesis: ( k in dom M1 implies M1 . k = M2 . k )
assume A13: k in dom M1 ; ::_thesis: M1 . k = M2 . k
hence M1 . k = <*(x . k)*> by A9, A12
.= M2 . k by A11, A12, A13 ;
::_thesis: verum
end;
hence M1 = M2 by A8, A10, FINSEQ_2:9; ::_thesis: verum
end;
end;
:: deftheorem defines FinSeq2Matrix MATRIXC1:def_3_:_
for x being FinSequence of COMPLEX st len x > 0 holds
for b2 being Matrix of COMPLEX holds
( b2 = FinSeq2Matrix x iff ( len b2 = len x & width b2 = 1 & ( for j being Nat st j in Seg (len x) holds
b2 . j = <*(x . j)*> ) ) );
definition
let M be Matrix of COMPLEX;
func Matrix2FinSeq M -> FinSequence of COMPLEX equals :: MATRIXC1:def 4
Col (M,1);
coherence
Col (M,1) is FinSequence of COMPLEX ;
end;
:: deftheorem defines Matrix2FinSeq MATRIXC1:def_4_:_
for M being Matrix of COMPLEX holds Matrix2FinSeq M = Col (M,1);
definition
let F1, F2 be FinSequence of COMPLEX ;
func mlt (F1,F2) -> FinSequence of COMPLEX equals :: MATRIXC1:def 5
multcomplex .: (F1,F2);
coherence
multcomplex .: (F1,F2) is FinSequence of COMPLEX ;
commutativity
for b1, F1, F2 being FinSequence of COMPLEX st b1 = multcomplex .: (F1,F2) holds
b1 = multcomplex .: (F2,F1)
proof
let F, F1, F2 be FinSequence of COMPLEX ; ::_thesis: ( F = multcomplex .: (F1,F2) implies F = multcomplex .: (F2,F1) )
A1: dom multcomplex = [:COMPLEX,COMPLEX:] by FUNCT_2:def_1;
then A2: [:(rng F2),(rng F1):] c= dom multcomplex by ZFMISC_1:96;
[:(rng F1),(rng F2):] c= dom multcomplex by A1, ZFMISC_1:96;
then A3: dom (multcomplex .: (F1,F2)) = (dom F1) /\ (dom F2) by FUNCOP_1:69
.= dom (multcomplex .: (F2,F1)) by A2, FUNCOP_1:69 ;
assume A4: F = multcomplex .: (F1,F2) ; ::_thesis: F = multcomplex .: (F2,F1)
for z being set st z in dom (multcomplex .: (F2,F1)) holds
F . z = multcomplex . ((F2 . z),(F1 . z))
proof
let z be set ; ::_thesis: ( z in dom (multcomplex .: (F2,F1)) implies F . z = multcomplex . ((F2 . z),(F1 . z)) )
assume A5: z in dom (multcomplex .: (F2,F1)) ; ::_thesis: F . z = multcomplex . ((F2 . z),(F1 . z))
set F1z = F1 . z;
set F2z = F2 . z;
thus F . z = multcomplex . ((F1 . z),(F2 . z)) by A4, A3, A5, FUNCOP_1:22
.= (F1 . z) * (F2 . z) by BINOP_2:def_5
.= multcomplex . ((F2 . z),(F1 . z)) by BINOP_2:def_5 ; ::_thesis: verum
end;
hence F = multcomplex .: (F2,F1) by A4, A3, FUNCOP_1:21; ::_thesis: verum
end;
end;
:: deftheorem defines mlt MATRIXC1:def_5_:_
for F1, F2 being FinSequence of COMPLEX holds mlt (F1,F2) = multcomplex .: (F1,F2);
definition
let M be Matrix of COMPLEX;
let F be FinSequence of COMPLEX ;
funcM * F -> FinSequence of COMPLEX means :Def6: :: MATRIXC1:def 6
( len it = len M & ( for i being Nat st i in Seg (len M) holds
it . i = Sum (mlt ((Line (M,i)),F)) ) );
existence
ex b1 being FinSequence of COMPLEX st
( len b1 = len M & ( for i being Nat st i in Seg (len M) holds
b1 . i = Sum (mlt ((Line (M,i)),F)) ) )
proof
deffunc H1( Nat) -> Element of COMPLEX = Sum (mlt ((Line (M,$1)),F));
consider z being FinSequence of COMPLEX such that
A1: ( len z = len M & ( for i being Nat st i in dom z holds
z . i = H1(i) ) ) from FINSEQ_2:sch_1();
take z ; ::_thesis: ( len z = len M & ( for i being Nat st i in Seg (len M) holds
z . i = Sum (mlt ((Line (M,i)),F)) ) )
dom z = Seg (len M) by A1, FINSEQ_1:def_3;
hence ( len z = len M & ( for i being Nat st i in Seg (len M) holds
z . i = Sum (mlt ((Line (M,i)),F)) ) ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being FinSequence of COMPLEX st len b1 = len M & ( for i being Nat st i in Seg (len M) holds
b1 . i = Sum (mlt ((Line (M,i)),F)) ) & len b2 = len M & ( for i being Nat st i in Seg (len M) holds
b2 . i = Sum (mlt ((Line (M,i)),F)) ) holds
b1 = b2
proof
let p1, p2 be FinSequence of COMPLEX ; ::_thesis: ( len p1 = len M & ( for i being Nat st i in Seg (len M) holds
p1 . i = Sum (mlt ((Line (M,i)),F)) ) & len p2 = len M & ( for i being Nat st i in Seg (len M) holds
p2 . i = Sum (mlt ((Line (M,i)),F)) ) implies p1 = p2 )
assume that
A2: len p1 = len M and
A3: for i being Nat st i in Seg (len M) holds
p1 . i = Sum (mlt ((Line (M,i)),F)) and
A4: len p2 = len M and
A5: for i being Nat st i in Seg (len M) holds
p2 . i = Sum (mlt ((Line (M,i)),F)) ; ::_thesis: p1 = p2
A6: dom p1 = Seg (len M) by A2, FINSEQ_1:def_3;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_p1_holds_
p1_._i_=_p2_._i
let i be Nat; ::_thesis: ( i in dom p1 implies p1 . i = p2 . i )
assume A7: i in dom p1 ; ::_thesis: p1 . i = p2 . i
then p1 . i = Sum (mlt ((Line (M,i)),F)) by A3, A6;
hence p1 . i = p2 . i by A5, A6, A7; ::_thesis: verum
end;
hence p1 = p2 by A2, A4, FINSEQ_2:9; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines * MATRIXC1:def_6_:_
for M being Matrix of COMPLEX
for F, b3 being FinSequence of COMPLEX holds
( b3 = M * F iff ( len b3 = len M & ( for i being Nat st i in Seg (len M) holds
b3 . i = Sum (mlt ((Line (M,i)),F)) ) ) );
Lm1: for a being Element of COMPLEX
for F being FinSequence of COMPLEX holds a * F = (multcomplex [;] (a,(id COMPLEX))) * F
proof
let a be Element of COMPLEX ; ::_thesis: for F being FinSequence of COMPLEX holds a * F = (multcomplex [;] (a,(id COMPLEX))) * F
let F be FinSequence of COMPLEX ; ::_thesis: a * F = (multcomplex [;] (a,(id COMPLEX))) * F
a multcomplex = multcomplex [;] (a,(id COMPLEX)) by SEQ_4:def_4;
hence a * F = (multcomplex [;] (a,(id COMPLEX))) * F by SEQ_4:def_9; ::_thesis: verum
end;
theorem Th16: :: MATRIXC1:16
for i being Nat
for a being Element of COMPLEX
for R1, R2 being Element of i -tuples_on COMPLEX holds a * (mlt (R1,R2)) = mlt ((a * R1),R2)
proof
let i be Nat; ::_thesis: for a being Element of COMPLEX
for R1, R2 being Element of i -tuples_on COMPLEX holds a * (mlt (R1,R2)) = mlt ((a * R1),R2)
let a be Element of COMPLEX ; ::_thesis: for R1, R2 being Element of i -tuples_on COMPLEX holds a * (mlt (R1,R2)) = mlt ((a * R1),R2)
let R1, R2 be Element of i -tuples_on COMPLEX; ::_thesis: a * (mlt (R1,R2)) = mlt ((a * R1),R2)
thus a * (mlt (R1,R2)) = (multcomplex [;] (a,(id COMPLEX))) * (mlt (R1,R2)) by Lm1
.= multcomplex .: (((multcomplex [;] (a,(id COMPLEX))) * R1),R2) by FINSEQOP:26
.= mlt ((a * R1),R2) by Lm1 ; ::_thesis: verum
end;
definition
let M be Matrix of COMPLEX;
let a be complex number ;
funcM * a -> Matrix of COMPLEX equals :: MATRIXC1:def 7
a * M;
coherence
a * M is Matrix of COMPLEX ;
end;
:: deftheorem defines * MATRIXC1:def_7_:_
for M being Matrix of COMPLEX
for a being complex number holds M * a = a * M;
theorem :: MATRIXC1:17
for a being Element of COMPLEX
for M being Matrix of COMPLEX holds (M * a) *' = (a *') * (M *') by Th5;
theorem Th18: :: MATRIXC1:18
for F1, F2 being FinSequence of COMPLEX
for i being Nat st i in dom (mlt (F1,F2)) holds
(mlt (F1,F2)) . i = (F1 . i) * (F2 . i)
proof
let F1, F2 be FinSequence of COMPLEX ; ::_thesis: for i being Nat st i in dom (mlt (F1,F2)) holds
(mlt (F1,F2)) . i = (F1 . i) * (F2 . i)
let i be Nat; ::_thesis: ( i in dom (mlt (F1,F2)) implies (mlt (F1,F2)) . i = (F1 . i) * (F2 . i) )
set r1 = F1 . i;
set r2 = F2 . i;
assume i in dom (mlt (F1,F2)) ; ::_thesis: (mlt (F1,F2)) . i = (F1 . i) * (F2 . i)
then (mlt (F1,F2)) . i = multcomplex . ((F1 . i),(F2 . i)) by FUNCOP_1:22;
hence (mlt (F1,F2)) . i = (F1 . i) * (F2 . i) by BINOP_2:def_5; ::_thesis: verum
end;
definition
let i be Element of NAT ;
let R1, R2 be Element of i -tuples_on COMPLEX;
:: original: mlt
redefine func mlt (R1,R2) -> Element of i -tuples_on COMPLEX;
coherence
mlt (R1,R2) is Element of i -tuples_on COMPLEX by FINSEQ_2:120;
end;
theorem Th19: :: MATRIXC1:19
for i, j being Nat
for R1, R2 being Element of i -tuples_on COMPLEX holds (mlt (R1,R2)) . j = (R1 . j) * (R2 . j)
proof
let i, j be Nat; ::_thesis: for R1, R2 being Element of i -tuples_on COMPLEX holds (mlt (R1,R2)) . j = (R1 . j) * (R2 . j)
let R1, R2 be Element of i -tuples_on COMPLEX; ::_thesis: (mlt (R1,R2)) . j = (R1 . j) * (R2 . j)
reconsider i = i, j1 = j as Element of NAT by ORDINAL1:def_12;
reconsider R1 = R1, R2 = R2 as Element of i -tuples_on COMPLEX ;
percases ( not j in Seg i or j in Seg i ) ;
supposeA1: not j in Seg i ; ::_thesis: (mlt (R1,R2)) . j = (R1 . j) * (R2 . j)
then A2: not j in dom R2 by FINSEQ_2:124;
not j in dom (mlt (R1,R2)) by A1, FINSEQ_2:124;
then (mlt (R1,R2)) . j = (R1 . j1) * 0 by FUNCT_1:def_2
.= (R1 . j) * (R2 . j) by A2, FUNCT_1:def_2 ;
hence (mlt (R1,R2)) . j = (R1 . j) * (R2 . j) ; ::_thesis: verum
end;
suppose j in Seg i ; ::_thesis: (mlt (R1,R2)) . j = (R1 . j) * (R2 . j)
then j in dom (mlt (R1,R2)) by FINSEQ_2:124;
hence (mlt (R1,R2)) . j = (R1 . j) * (R2 . j) by Th18; ::_thesis: verum
end;
end;
end;
theorem Th20: :: MATRIXC1:20
for a, b being Element of COMPLEX holds (addcomplex . (a,(b *'))) *' = addcomplex . ((a *'),b)
proof
let a, b be Element of COMPLEX ; ::_thesis: (addcomplex . (a,(b *'))) *' = addcomplex . ((a *'),b)
(addcomplex . (a,(b *'))) *' = (a + (b *')) *' by BINOP_2:def_3
.= (a *') + ((b *') *') by COMPLEX1:32
.= addcomplex . ((a *'),b) by BINOP_2:def_3 ;
hence (addcomplex . (a,(b *'))) *' = addcomplex . ((a *'),b) ; ::_thesis: verum
end;
theorem Th21: :: MATRIXC1:21
for F being FinSequence of COMPLEX ex G being Function of NAT,COMPLEX st
for n being Nat st 1 <= n & n <= len F holds
G . n = F . n
proof
let F be FinSequence of COMPLEX ; ::_thesis: ex G being Function of NAT,COMPLEX st
for n being Nat st 1 <= n & n <= len F holds
G . n = F . n
defpred S1[ set , set ] means ( ( $1 in Seg (len F) implies $2 = F . $1 ) & ( not $1 in Seg (len F) implies $2 = 0 ) );
A1: for x being set st x in NAT holds
ex y being set st
( y in COMPLEX & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in NAT implies ex y being set st
( y in COMPLEX & S1[x,y] ) )
assume x in NAT ; ::_thesis: ex y being set st
( y in COMPLEX & S1[x,y] )
percases ( x in Seg (len F) or not x in Seg (len F) ) ;
suppose x in Seg (len F) ; ::_thesis: ex y being set st
( y in COMPLEX & S1[x,y] )
hence ex y being set st
( y in COMPLEX & S1[x,y] ) ; ::_thesis: verum
end;
suppose not x in Seg (len F) ; ::_thesis: ex y being set st
( y in COMPLEX & S1[x,y] )
then not x in dom F by FINSEQ_1:def_3;
then S1[x,F . x] by FUNCT_1:def_2;
hence ex y being set st
( y in COMPLEX & S1[x,y] ) ; ::_thesis: verum
end;
end;
end;
ex G1 being Function of NAT,COMPLEX st
for x being set st x in NAT holds
S1[x,G1 . x] from FUNCT_2:sch_1(A1);
then consider G2 being Function of NAT,COMPLEX such that
A2: for x being set st x in NAT holds
( ( x in Seg (len F) implies G2 . x = F . x ) & ( not x in Seg (len F) implies G2 . x = 0 ) ) ;
for n being Nat st 1 <= n & n <= len F holds
G2 . n = F . n
proof
let n be Nat; ::_thesis: ( 1 <= n & n <= len F implies G2 . n = F . n )
assume that
A3: 1 <= n and
A4: n <= len F ; ::_thesis: G2 . n = F . n
n in Seg (len F) by A3, A4, FINSEQ_1:1;
hence G2 . n = F . n by A2; ::_thesis: verum
end;
hence ex G being Function of NAT,COMPLEX st
for n being Nat st 1 <= n & n <= len F holds
G . n = F . n ; ::_thesis: verum
end;
theorem Th22: :: MATRIXC1:22
for F being FinSequence of COMPLEX st len (F *') >= 1 holds
addcomplex $$ (F *') = (addcomplex $$ F) *'
proof
let F be FinSequence of COMPLEX ; ::_thesis: ( len (F *') >= 1 implies addcomplex $$ (F *') = (addcomplex $$ F) *' )
A1: len F = len (F *') by COMPLSP2:def_1;
assume A2: len (F *') >= 1 ; ::_thesis: addcomplex $$ (F *') = (addcomplex $$ F) *'
then consider f22 being Function of NAT,COMPLEX such that
A3: f22 . 1 = (F *') . 1 and
A4: for n being Element of NAT st 0 <> n & n < len (F *') holds
f22 . (n + 1) = addcomplex . ((f22 . n),((F *') . (n + 1))) and
A5: addcomplex $$ (F *') = f22 . (len (F *')) by FINSOP_1:1;
A6: len (F *') in Seg (len (F *')) by A2, FINSEQ_1:1;
defpred S1[ set , set ] means $2 = f22 . $1;
A7: for k being Nat st k in Seg (len (F *')) holds
ex x being Element of COMPLEX st S1[k,x] ;
ex f2 being FinSequence of COMPLEX st
( dom f2 = Seg (len (F *')) & ( for k being Nat st k in Seg (len (F *')) holds
S1[k,f2 . k] ) ) from FINSEQ_1:sch_5(A7);
then consider f2 being FinSequence of COMPLEX such that
A8: dom f2 = Seg (len (F *')) and
A9: for k being Nat st k in Seg (len (F *')) holds
S1[k,f2 . k] ;
consider f9 being Function of NAT,COMPLEX such that
A10: for n being Nat st 1 <= n & n <= len (f2 *') holds
f9 . n = (f2 *') . n by Th21;
A11: len (f2 *') = len f2 by COMPLSP2:def_1;
then 1 <= len (f2 *') by A2, A8, FINSEQ_1:def_3;
then A12: f9 . 1 = (f2 *') . 1 by A10;
A13: len f2 = len (F *') by A8, FINSEQ_1:def_3;
A14: for n being Nat st 0 <> n & n < len (F *') holds
f2 . (n + 1) = addcomplex . ((f2 . n),((F *') . (n + 1)))
proof
let n be Nat; ::_thesis: ( 0 <> n & n < len (F *') implies f2 . (n + 1) = addcomplex . ((f2 . n),((F *') . (n + 1))) )
assume that
A15: 0 <> n and
A16: n < len (F *') ; ::_thesis: f2 . (n + 1) = addcomplex . ((f2 . n),((F *') . (n + 1)))
A17: n + 1 <= len (F *') by A16, NAT_1:13;
A18: 0 + 1 <= n by A15, NAT_1:13;
then A19: n in Seg (len (F *')) by A16, FINSEQ_1:1;
1 <= n + 1 by A18, NAT_1:13;
then n + 1 in Seg (len (F *')) by A17, FINSEQ_1:1;
then f2 . (n + 1) = f22 . (n + 1) by A9
.= addcomplex . ((f22 . n),((F *') . (n + 1))) by A4, A15, A16, A19
.= addcomplex . ((f2 . n),((F *') . (n + 1))) by A9, A19 ;
hence f2 . (n + 1) = addcomplex . ((f2 . n),((F *') . (n + 1))) ; ::_thesis: verum
end;
A20: for n being Element of NAT st 0 <> n & n < len F holds
(f2 *') . (n + 1) = addcomplex . (((f2 *') . n),(F . (n + 1)))
proof
let n be Element of NAT ; ::_thesis: ( 0 <> n & n < len F implies (f2 *') . (n + 1) = addcomplex . (((f2 *') . n),(F . (n + 1))) )
assume that
A21: 0 <> n and
A22: n < len F ; ::_thesis: (f2 *') . (n + 1) = addcomplex . (((f2 *') . n),(F . (n + 1)))
A23: n <= len f2 by A1, A8, A22, FINSEQ_1:def_3;
A24: 0 + 1 <= n by A21, NAT_1:13;
then A25: 1 <= n + 1 by NAT_1:13;
A26: n + 1 <= len F by A22, NAT_1:13;
then n + 1 <= len f2 by A1, A8, FINSEQ_1:def_3;
then (f2 *') . (n + 1) = (f2 . (n + 1)) *' by A25, COMPLSP2:def_1
.= (addcomplex . ((f2 . n),((F *') . (n + 1)))) *' by A1, A14, A21, A22
.= (addcomplex . ((f2 . n),((F . (n + 1)) *'))) *' by A25, A26, COMPLSP2:def_1
.= addcomplex . (((f2 . n) *'),(F . (n + 1))) by Th20 ;
hence (f2 *') . (n + 1) = addcomplex . (((f2 *') . n),(F . (n + 1))) by A24, A23, COMPLSP2:def_1; ::_thesis: verum
end;
A27: for n being Element of NAT st 0 <> n & n < len F holds
f9 . (n + 1) = addcomplex . ((f9 . n),(F . (n + 1)))
proof
let n be Element of NAT ; ::_thesis: ( 0 <> n & n < len F implies f9 . (n + 1) = addcomplex . ((f9 . n),(F . (n + 1))) )
assume that
A28: 0 <> n and
A29: n < len F ; ::_thesis: f9 . (n + 1) = addcomplex . ((f9 . n),(F . (n + 1)))
A30: 0 + 1 <= n by A28, NAT_1:13;
n + 1 <= len (f2 *') by A1, A13, A11, A29, NAT_1:13;
then A31: f9 . (n + 1) = (f2 *') . (n + 1) by A10, NAT_1:11;
n <= len (f2 *') by A1, A13, A29, COMPLSP2:def_1;
then f9 . n = (f2 *') . n by A10, A30;
hence f9 . (n + 1) = addcomplex . ((f9 . n),(F . (n + 1))) by A20, A28, A29, A31; ::_thesis: verum
end;
A32: 1 in Seg (len (F *')) by A2, FINSEQ_1:1;
set d = (addcomplex $$ (F *')) *' ;
A33: len F >= 1 by A2, COMPLSP2:def_1;
(f2 *') . (len F) = (f2 *') . (len (F *')) by COMPLSP2:def_1
.= (f2 . (len (F *'))) *' by A2, A13, COMPLSP2:def_1
.= (addcomplex $$ (F *')) *' by A5, A9, A6 ;
then A34: (addcomplex $$ (F *')) *' = f9 . (len F) by A2, A1, A13, A10, A11;
F . 1 = ((F . 1) *') *'
.= ((F *') . 1) *' by A33, COMPLSP2:def_1
.= (f2 . 1) *' by A3, A9, A32
.= (f2 *') . 1 by A2, A13, COMPLSP2:def_1 ;
then (addcomplex $$ (F *')) *' = addcomplex $$ F by A33, A12, A27, A34, FINSOP_1:2;
hence addcomplex $$ (F *') = (addcomplex $$ F) *' ; ::_thesis: verum
end;
theorem Th23: :: MATRIXC1:23
for F being FinSequence of COMPLEX st len F >= 1 holds
Sum (F *') = (Sum F) *'
proof
let F be FinSequence of COMPLEX ; ::_thesis: ( len F >= 1 implies Sum (F *') = (Sum F) *' )
assume len F >= 1 ; ::_thesis: Sum (F *') = (Sum F) *'
then len (F *') >= 1 by COMPLSP2:def_1;
hence Sum (F *') = (Sum F) *' by Th22; ::_thesis: verum
end;
theorem Th24: :: MATRIXC1:24
for x, y being FinSequence of COMPLEX st len x = len y holds
(mlt (x,(y *'))) *' = mlt (y,(x *'))
proof
let x, y be FinSequence of COMPLEX ; ::_thesis: ( len x = len y implies (mlt (x,(y *'))) *' = mlt (y,(x *')) )
assume A1: len x = len y ; ::_thesis: (mlt (x,(y *'))) *' = mlt (y,(x *'))
reconsider x19 = x *' as Element of (len (x *')) -tuples_on COMPLEX by FINSEQ_2:92;
reconsider y19 = y as Element of (len y) -tuples_on COMPLEX by FINSEQ_2:92;
reconsider y9 = y *' as Element of (len (y *')) -tuples_on COMPLEX by FINSEQ_2:92;
reconsider x9 = x as Element of (len x) -tuples_on COMPLEX by FINSEQ_2:92;
A2: len (x *') = len x by COMPLSP2:def_1;
A3: len (y *') = len y by COMPLSP2:def_1;
then A4: len (mlt (x,(y *'))) = len x by A1, FINSEQ_2:72;
A5: len (mlt (x,(y *'))) = len (y *') by A1, A3, FINSEQ_2:72;
A6: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_((mlt_(x,(y_*')))_*')_holds_
((mlt_(x,(y_*')))_*')_._i_=_(mlt_(y,(x_*')))_._i
let i be Nat; ::_thesis: ( 1 <= i & i <= len ((mlt (x,(y *'))) *') implies ((mlt (x,(y *'))) *') . i = (mlt (y,(x *'))) . i )
assume that
A7: 1 <= i and
A8: i <= len ((mlt (x,(y *'))) *') ; ::_thesis: ((mlt (x,(y *'))) *') . i = (mlt (y,(x *'))) . i
A9: i <= len (mlt (x,(y *'))) by A8, COMPLSP2:def_1;
hence ((mlt (x,(y *'))) *') . i = ((mlt (x,(y *'))) . i) *' by A7, COMPLSP2:def_1
.= ((x9 . i) * (y9 . i)) *' by A1, A3, Th19
.= ((x . i) *') * (((y *') . i) *') by COMPLEX1:35
.= ((x . i) *') * (((y *') *') . i) by A5, A7, A9, COMPLSP2:def_1
.= ((x . i) *') * (y . i) by COMPLSP2:22
.= ((x *') . i) * (y . i) by A4, A7, A9, COMPLSP2:def_1
.= (mlt (x19,y19)) . i by A1, A2, Th19
.= (mlt (y,(x *'))) . i ;
::_thesis: verum
end;
len (mlt (x,(y *'))) = len ((mlt (x,(y *'))) *') by COMPLSP2:def_1;
then len ((mlt (x,(y *'))) *') = len (mlt (y,(x *'))) by A1, A2, A4, FINSEQ_2:72;
hence (mlt (x,(y *'))) *' = mlt (y,(x *')) by A6, FINSEQ_1:14; ::_thesis: verum
end;
theorem Th25: :: MATRIXC1:25
for x, y being FinSequence of COMPLEX
for a being Element of COMPLEX st len x = len y holds
mlt (x,(a * y)) = a * (mlt (x,y))
proof
let x, y be FinSequence of COMPLEX ; ::_thesis: for a being Element of COMPLEX st len x = len y holds
mlt (x,(a * y)) = a * (mlt (x,y))
let a be Element of COMPLEX ; ::_thesis: ( len x = len y implies mlt (x,(a * y)) = a * (mlt (x,y)) )
reconsider x9 = x as Element of (len x) -tuples_on COMPLEX by FINSEQ_2:92;
reconsider y9 = y as Element of (len y) -tuples_on COMPLEX by FINSEQ_2:92;
assume len x = len y ; ::_thesis: mlt (x,(a * y)) = a * (mlt (x,y))
then mlt (x,(a * y)) = a * (mlt (x9,y9)) by Th16
.= a * (mlt (x,y)) ;
hence mlt (x,(a * y)) = a * (mlt (x,y)) ; ::_thesis: verum
end;
theorem Th26: :: MATRIXC1:26
for x, y being FinSequence of COMPLEX
for a being Element of COMPLEX st len x = len y holds
mlt ((a * x),y) = a * (mlt (x,y))
proof
let x, y be FinSequence of COMPLEX ; ::_thesis: for a being Element of COMPLEX st len x = len y holds
mlt ((a * x),y) = a * (mlt (x,y))
let a be Element of COMPLEX ; ::_thesis: ( len x = len y implies mlt ((a * x),y) = a * (mlt (x,y)) )
reconsider x9 = x as Element of (len x) -tuples_on COMPLEX by FINSEQ_2:92;
reconsider y9 = y as Element of (len y) -tuples_on COMPLEX by FINSEQ_2:92;
assume len x = len y ; ::_thesis: mlt ((a * x),y) = a * (mlt (x,y))
then mlt ((a * x),y) = a * (mlt (x9,y9)) by Th16
.= a * (mlt (x,y)) ;
hence mlt ((a * x),y) = a * (mlt (x,y)) ; ::_thesis: verum
end;
theorem Th27: :: MATRIXC1:27
for x, y being FinSequence of COMPLEX st len x = len y holds
(mlt (x,y)) *' = mlt ((x *'),(y *'))
proof
let x, y be FinSequence of COMPLEX ; ::_thesis: ( len x = len y implies (mlt (x,y)) *' = mlt ((x *'),(y *')) )
A1: len ((mlt (x,y)) *') = len (mlt (x,y)) by COMPLSP2:def_1;
A2: len (x *') = len x by COMPLSP2:def_1;
assume A3: len x = len y ; ::_thesis: (mlt (x,y)) *' = mlt ((x *'),(y *'))
A4: for i being Nat st 1 <= i & i <= len ((mlt (x,y)) *') holds
((mlt (x,y)) *') . i = (mlt ((x *'),(y *'))) . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len ((mlt (x,y)) *') implies ((mlt (x,y)) *') . i = (mlt ((x *'),(y *'))) . i )
((mlt (x,y)) *') . i = ((mlt (y,((x *') *'))) *') . i by COMPLSP2:22
.= (mlt ((x *'),(y *'))) . i by A3, A2, Th24 ;
hence ( 1 <= i & i <= len ((mlt (x,y)) *') implies ((mlt (x,y)) *') . i = (mlt ((x *'),(y *'))) . i ) ; ::_thesis: verum
end;
len (y *') = len y by COMPLSP2:def_1;
then len (mlt ((x *'),(y *'))) = len (x *') by A3, A2, FINSEQ_2:72;
then len ((mlt (x,y)) *') = len (mlt ((x *'),(y *'))) by A3, A1, A2, FINSEQ_2:72;
hence (mlt (x,y)) *' = mlt ((x *'),(y *')) by A4, FINSEQ_1:14; ::_thesis: verum
end;
Lm2: for a, b being Element of COMPLEX holds (multcomplex [;] (a,(id COMPLEX))) . b = a * b
proof
let a, b be Element of COMPLEX ; ::_thesis: (multcomplex [;] (a,(id COMPLEX))) . b = a * b
thus (multcomplex [;] (a,(id COMPLEX))) . b = multcomplex . (a,((id COMPLEX) . b)) by FUNCOP_1:53
.= multcomplex . (a,b) by FUNCT_1:18
.= a * b by BINOP_2:def_5 ; ::_thesis: verum
end;
theorem Th28: :: MATRIXC1:28
for F being FinSequence of COMPLEX
for a being Element of COMPLEX holds Sum (a * F) = a * (Sum F)
proof
let F be FinSequence of COMPLEX ; ::_thesis: for a being Element of COMPLEX holds Sum (a * F) = a * (Sum F)
let a be Element of COMPLEX ; ::_thesis: Sum (a * F) = a * (Sum F)
set rM = multcomplex [;] (a,(id COMPLEX));
thus Sum (a * F) = addcomplex $$ ((multcomplex [;] (a,(id COMPLEX))) * F) by Lm1
.= (multcomplex [;] (a,(id COMPLEX))) . (addcomplex $$ F) by SEQ_4:51, SEQ_4:54, SETWOP_2:30
.= a * (Sum F) by Lm2 ; ::_thesis: verum
end;
definition
let x be FinSequence of REAL ;
func FR2FC x -> FinSequence of COMPLEX equals :: MATRIXC1:def 8
x;
coherence
x is FinSequence of COMPLEX
proof
rng x c= COMPLEX by NUMBERS:11, XBOOLE_1:1;
hence x is FinSequence of COMPLEX by FINSEQ_1:def_4; ::_thesis: verum
end;
end;
:: deftheorem defines FR2FC MATRIXC1:def_8_:_
for x being FinSequence of REAL holds FR2FC x = x;
theorem :: MATRIXC1:29
for R being FinSequence of REAL
for F being FinSequence of COMPLEX st R = F & len R >= 1 holds
addreal $$ R = addcomplex $$ F
proof
let R be FinSequence of REAL ; ::_thesis: for F being FinSequence of COMPLEX st R = F & len R >= 1 holds
addreal $$ R = addcomplex $$ F
let F be FinSequence of COMPLEX ; ::_thesis: ( R = F & len R >= 1 implies addreal $$ R = addcomplex $$ F )
assume that
A1: R = F and
A2: len R >= 1 ; ::_thesis: addreal $$ R = addcomplex $$ F
consider f22 being Function of NAT,REAL such that
A3: f22 . 1 = R . 1 and
A4: for n being Element of NAT st 0 <> n & n < len R holds
f22 . (n + 1) = addreal . ((f22 . n),(R . (n + 1))) and
A5: addreal $$ R = f22 . (len R) by A2, FINSOP_1:1;
defpred S1[ set , set ] means $2 = f22 . $1;
A6: for k being Nat st k in Seg (len R) holds
ex x being Element of REAL st S1[k,x] ;
ex f2 being FinSequence of REAL st
( dom f2 = Seg (len R) & ( for k being Nat st k in Seg (len R) holds
S1[k,f2 . k] ) ) from FINSEQ_1:sch_5(A6);
then consider f2 being FinSequence of REAL such that
A7: dom f2 = Seg (len R) and
A8: for k being Nat st k in Seg (len R) holds
S1[k,f2 . k] ;
consider f9 being Function of NAT,COMPLEX such that
A9: for n being Nat st 1 <= n & n <= len (FR2FC f2) holds
f9 . n = (FR2FC f2) . n by Th21;
A10: len f2 = len R by A7, FINSEQ_1:def_3;
then A11: (FR2FC f2) . (len F) = f9 . (len F) by A1, A2, A9;
A12: for n being Nat st 0 <> n & n < len R holds
f2 . (n + 1) = addreal . ((f2 . n),(R . (n + 1)))
proof
let n be Nat; ::_thesis: ( 0 <> n & n < len R implies f2 . (n + 1) = addreal . ((f2 . n),(R . (n + 1))) )
assume that
A13: 0 <> n and
A14: n < len R ; ::_thesis: f2 . (n + 1) = addreal . ((f2 . n),(R . (n + 1)))
A15: n + 1 <= len R by A14, NAT_1:13;
A16: 0 + 1 <= n by A13, NAT_1:13;
then A17: n in Seg (len R) by A14, FINSEQ_1:1;
1 <= n + 1 by A16, NAT_1:13;
then n + 1 in Seg (len R) by A15, FINSEQ_1:1;
then f2 . (n + 1) = f22 . (n + 1) by A8
.= addreal . ((f22 . n),(R . (n + 1))) by A4, A13, A14, A17
.= addreal . ((f2 . n),(R . (n + 1))) by A8, A17 ;
hence f2 . (n + 1) = addreal . ((f2 . n),(R . (n + 1))) ; ::_thesis: verum
end;
A18: for n being Element of NAT st 0 <> n & n < len F holds
f9 . (n + 1) = addcomplex . ((f9 . n),(F . (n + 1)))
proof
let n be Element of NAT ; ::_thesis: ( 0 <> n & n < len F implies f9 . (n + 1) = addcomplex . ((f9 . n),(F . (n + 1))) )
assume that
A19: 0 <> n and
A20: n < len F ; ::_thesis: f9 . (n + 1) = addcomplex . ((f9 . n),(F . (n + 1)))
A21: 0 + 1 <= n by A19, NAT_1:13;
n <= len (FR2FC f2) by A1, A7, A20, FINSEQ_1:def_3;
then f9 . n = (FR2FC f2) . n by A9, A21;
then A22: addcomplex . ((f9 . n),(F . (n + 1))) = addreal . ((f2 . n),(R . (n + 1))) by A1, COMPLSP2:44;
n + 1 <= len (FR2FC f2) by A1, A10, A20, NAT_1:13;
then f9 . (n + 1) = (FR2FC f2) . (n + 1) by A9, NAT_1:11;
hence f9 . (n + 1) = addcomplex . ((f9 . n),(F . (n + 1))) by A1, A12, A19, A20, A22; ::_thesis: verum
end;
set d = addreal $$ R;
A23: 1 in Seg (len R) by A2, FINSEQ_1:1;
A24: f9 . 1 = (FR2FC f2) . 1 by A2, A10, A9;
len R in Seg (len R) by A2, FINSEQ_1:1;
then (FR2FC f2) . (len F) = addreal $$ R by A1, A5, A8;
hence addreal $$ R = addcomplex $$ F by A1, A2, A3, A8, A23, A24, A18, A11, FINSOP_1:2; ::_thesis: verum
end;
theorem :: MATRIXC1:30
for x being FinSequence of REAL
for y being FinSequence of COMPLEX st x = y & len x >= 1 holds
Sum x = Sum y ;
theorem Th31: :: MATRIXC1:31
for F1, F2 being FinSequence of COMPLEX st len F1 = len F2 holds
Sum (F1 - F2) = (Sum F1) - (Sum F2)
proof
let F1, F2 be FinSequence of COMPLEX ; ::_thesis: ( len F1 = len F2 implies Sum (F1 - F2) = (Sum F1) - (Sum F2) )
assume A1: len F1 = len F2 ; ::_thesis: Sum (F1 - F2) = (Sum F1) - (Sum F2)
reconsider y2 = F2 as Element of (len F2) -tuples_on COMPLEX by FINSEQ_2:92;
reconsider x2 = F1 as Element of (len F1) -tuples_on COMPLEX by FINSEQ_2:92;
Sum (F1 - F2) = addcomplex $$ (diffcomplex .: (F1,F2)) by SEQ_4:def_7
.= diffcomplex . ((addcomplex $$ x2),(addcomplex $$ y2)) by A1, SEQ_4:51, SEQ_4:52, SEQ_4:def_3, SETWOP_2:37
.= (Sum F1) - (Sum F2) by BINOP_2:def_4 ;
hence Sum (F1 - F2) = (Sum F1) - (Sum F2) ; ::_thesis: verum
end;
theorem :: MATRIXC1:32
for x, y, z being FinSequence of COMPLEX st len x = len y & len y = len z holds
mlt ((x - y),z) = (mlt (x,z)) - (mlt (y,z))
proof
let x, y, z be FinSequence of COMPLEX ; ::_thesis: ( len x = len y & len y = len z implies mlt ((x - y),z) = (mlt (x,z)) - (mlt (y,z)) )
assume that
A1: len x = len y and
A2: len y = len z ; ::_thesis: mlt ((x - y),z) = (mlt (x,z)) - (mlt (y,z))
reconsider x2 = x, y2 = y, z2 = z as Element of (len x) -tuples_on COMPLEX by A1, A2, FINSEQ_2:92;
A3: dom (mlt ((x - y),z)) = Seg (len (mlt ((x2 - y2),z2))) by FINSEQ_1:def_3
.= Seg (len x) by CARD_1:def_7
.= Seg (len ((mlt (x2,z2)) - (mlt (y2,z2)))) by CARD_1:def_7
.= dom ((mlt (x2,z2)) - (mlt (y2,z2))) by FINSEQ_1:def_3 ;
A4: dom (mlt (x,z)) = Seg (len (mlt (x2,z2))) by FINSEQ_1:def_3
.= Seg (len x) by CARD_1:def_7
.= Seg (len ((mlt (x2,z2)) - (mlt (y2,z2)))) by CARD_1:def_7
.= dom ((mlt (x2,z2)) - (mlt (y2,z2))) by FINSEQ_1:def_3 ;
A5: dom (mlt (y,z)) = Seg (len (mlt (y2,z2))) by FINSEQ_1:def_3
.= Seg (len x) by CARD_1:def_7
.= Seg (len ((mlt (x2,z2)) - (mlt (y2,z2)))) by CARD_1:def_7
.= dom ((mlt (x2,z2)) - (mlt (y2,z2))) by FINSEQ_1:def_3 ;
for i being Nat st i in dom (mlt ((x - y),z)) holds
(mlt ((x - y),z)) . i = ((mlt (x,z)) - (mlt (y,z))) . i
proof
let i be Nat; ::_thesis: ( i in dom (mlt ((x - y),z)) implies (mlt ((x - y),z)) . i = ((mlt (x,z)) - (mlt (y,z))) . i )
assume A6: i in dom (mlt ((x - y),z)) ; ::_thesis: (mlt ((x - y),z)) . i = ((mlt (x,z)) - (mlt (y,z))) . i
set a = x . i;
set b = y . i;
set d = (x - y) . i;
set e = z . i;
len (x2 - y2) = len x by CARD_1:def_7;
then dom (x2 - y2) = Seg (len x) by FINSEQ_1:def_3
.= Seg (len (mlt (x2,z2))) by CARD_1:def_7
.= dom (mlt (x,z)) by FINSEQ_1:def_3 ;
then A7: (x - y) . i = (x . i) - (y . i) by A3, A4, A6, COMPLSP2:2;
thus (mlt ((x - y),z)) . i = ((x - y) . i) * (z . i) by A6, Th18
.= ((x . i) * (z . i)) - ((y . i) * (z . i)) by A7
.= ((mlt (x,z)) . i) - ((y . i) * (z . i)) by A3, A4, A6, Th18
.= ((mlt (x,z)) . i) - ((mlt (y,z)) . i) by A3, A5, A6, Th18
.= ((mlt (x,z)) - (mlt (y,z))) . i by A3, A6, COMPLSP2:2 ; ::_thesis: verum
end;
hence mlt ((x - y),z) = (mlt (x,z)) - (mlt (y,z)) by A3, FINSEQ_1:13; ::_thesis: verum
end;
theorem Th33: :: MATRIXC1:33
for x, y, z being FinSequence of COMPLEX st len x = len y & len y = len z holds
mlt (x,(y - z)) = (mlt (x,y)) - (mlt (x,z))
proof
let x, y, z be FinSequence of COMPLEX ; ::_thesis: ( len x = len y & len y = len z implies mlt (x,(y - z)) = (mlt (x,y)) - (mlt (x,z)) )
assume that
A1: len x = len y and
A2: len y = len z ; ::_thesis: mlt (x,(y - z)) = (mlt (x,y)) - (mlt (x,z))
reconsider x2 = x, y2 = y, z2 = z as Element of (len x) -tuples_on COMPLEX by A1, A2, FINSEQ_2:92;
A3: dom (mlt (x,(y - z))) = Seg (len (mlt (x2,(y2 - z2)))) by FINSEQ_1:def_3
.= Seg (len x) by CARD_1:def_7
.= Seg (len ((mlt (x2,y2)) - (mlt (x2,z2)))) by CARD_1:def_7
.= dom ((mlt (x2,y2)) - (mlt (x2,z2))) by FINSEQ_1:def_3 ;
A4: dom (mlt (x,y)) = Seg (len (mlt (x2,y2))) by FINSEQ_1:def_3
.= Seg (len x) by CARD_1:def_7
.= Seg (len ((mlt (x2,y2)) - (mlt (x2,z2)))) by CARD_1:def_7
.= dom ((mlt (x2,y2)) - (mlt (x2,z2))) by FINSEQ_1:def_3 ;
A5: dom (mlt (x,z)) = Seg (len (mlt (x2,z2))) by FINSEQ_1:def_3
.= Seg (len x) by CARD_1:def_7
.= Seg (len ((mlt (x2,y2)) - (mlt (x2,z2)))) by CARD_1:def_7
.= dom ((mlt (x2,y2)) - (mlt (x2,z2))) by FINSEQ_1:def_3 ;
for i being Nat st i in dom (mlt (x,(y - z))) holds
(mlt (x,(y - z))) . i = ((mlt (x,y)) - (mlt (x,z))) . i
proof
let i be Nat; ::_thesis: ( i in dom (mlt (x,(y - z))) implies (mlt (x,(y - z))) . i = ((mlt (x,y)) - (mlt (x,z))) . i )
assume A6: i in dom (mlt (x,(y - z))) ; ::_thesis: (mlt (x,(y - z))) . i = ((mlt (x,y)) - (mlt (x,z))) . i
set a = y . i;
set b = z . i;
set d = (y - z) . i;
set e = x . i;
len (y2 - z2) = len x by CARD_1:def_7;
then dom (y2 - z2) = Seg (len x) by FINSEQ_1:def_3
.= Seg (len (mlt (x2,y2))) by CARD_1:def_7
.= dom (mlt (x,y)) by FINSEQ_1:def_3 ;
then A7: (y - z) . i = (y . i) - (z . i) by A3, A4, A6, COMPLSP2:2;
thus (mlt (x,(y - z))) . i = (x . i) * ((y - z) . i) by A6, Th18
.= ((x . i) * (y . i)) - ((x . i) * (z . i)) by A7
.= ((mlt (x,y)) . i) - ((x . i) * (z . i)) by A3, A4, A6, Th18
.= ((mlt (x,y)) . i) - ((mlt (x,z)) . i) by A3, A5, A6, Th18
.= ((mlt (x,y)) - (mlt (x,z))) . i by A3, A6, COMPLSP2:2 ; ::_thesis: verum
end;
hence mlt (x,(y - z)) = (mlt (x,y)) - (mlt (x,z)) by A3, FINSEQ_1:13; ::_thesis: verum
end;
theorem :: MATRIXC1:34
for x, y, z being FinSequence of COMPLEX st len x = len y & len y = len z holds
mlt (x,(y + z)) = (mlt (x,y)) + (mlt (x,z))
proof
let x, y, z be FinSequence of COMPLEX ; ::_thesis: ( len x = len y & len y = len z implies mlt (x,(y + z)) = (mlt (x,y)) + (mlt (x,z)) )
assume that
A1: len x = len y and
A2: len y = len z ; ::_thesis: mlt (x,(y + z)) = (mlt (x,y)) + (mlt (x,z))
reconsider x2 = x, y2 = y, z2 = z as Element of (len x) -tuples_on COMPLEX by A1, A2, FINSEQ_2:92;
A3: dom (mlt (x,(y + z))) = Seg (len (mlt (x2,(y2 + z2)))) by FINSEQ_1:def_3
.= Seg (len x) by CARD_1:def_7
.= Seg (len ((mlt (x2,y2)) + (mlt (x2,z2)))) by CARD_1:def_7
.= dom ((mlt (x2,y2)) + (mlt (x2,z2))) by FINSEQ_1:def_3 ;
A4: dom (mlt (x,y)) = Seg (len (mlt (x2,y2))) by FINSEQ_1:def_3
.= Seg (len x) by CARD_1:def_7
.= Seg (len ((mlt (x2,y2)) + (mlt (x2,z2)))) by CARD_1:def_7
.= dom ((mlt (x2,y2)) + (mlt (x2,z2))) by FINSEQ_1:def_3 ;
A5: dom (mlt (x,z)) = Seg (len (mlt (x2,z2))) by FINSEQ_1:def_3
.= Seg (len x) by CARD_1:def_7
.= Seg (len ((mlt (x2,y2)) + (mlt (x2,z2)))) by CARD_1:def_7
.= dom ((mlt (x2,y2)) + (mlt (x2,z2))) by FINSEQ_1:def_3 ;
for i being Nat st i in dom (mlt (x,(y + z))) holds
(mlt (x,(y + z))) . i = ((mlt (x,y)) + (mlt (x,z))) . i
proof
let i be Nat; ::_thesis: ( i in dom (mlt (x,(y + z))) implies (mlt (x,(y + z))) . i = ((mlt (x,y)) + (mlt (x,z))) . i )
assume A6: i in dom (mlt (x,(y + z))) ; ::_thesis: (mlt (x,(y + z))) . i = ((mlt (x,y)) + (mlt (x,z))) . i
set a = y . i;
set b = z . i;
set d = (y + z) . i;
set e = x . i;
len (y2 + z2) = len x by CARD_1:def_7;
then dom (y2 + z2) = Seg (len x) by FINSEQ_1:def_3
.= Seg (len (mlt (x2,y2))) by CARD_1:def_7
.= dom (mlt (x,y)) by FINSEQ_1:def_3 ;
then A7: (y + z) . i = (y . i) + (z . i) by A3, A4, A6, COMPLSP2:1;
thus (mlt (x,(y + z))) . i = (x . i) * ((y + z) . i) by A6, Th18
.= ((x . i) * (y . i)) + ((x . i) * (z . i)) by A7
.= ((mlt (x,y)) . i) + ((x . i) * (z . i)) by A3, A4, A6, Th18
.= ((mlt (x,y)) . i) + ((mlt (x,z)) . i) by A3, A5, A6, Th18
.= ((mlt (x,y)) + (mlt (x,z))) . i by A3, A6, COMPLSP2:1 ; ::_thesis: verum
end;
hence mlt (x,(y + z)) = (mlt (x,y)) + (mlt (x,z)) by A3, FINSEQ_1:13; ::_thesis: verum
end;
theorem Th35: :: MATRIXC1:35
for x, y, z being FinSequence of COMPLEX st len x = len y & len y = len z holds
mlt ((x + y),z) = (mlt (x,z)) + (mlt (y,z))
proof
let x, y, z be FinSequence of COMPLEX ; ::_thesis: ( len x = len y & len y = len z implies mlt ((x + y),z) = (mlt (x,z)) + (mlt (y,z)) )
assume that
A1: len x = len y and
A2: len y = len z ; ::_thesis: mlt ((x + y),z) = (mlt (x,z)) + (mlt (y,z))
reconsider x2 = x, y2 = y, z2 = z as Element of (len x) -tuples_on COMPLEX by A1, A2, FINSEQ_2:92;
A3: dom (mlt ((x + y),z)) = Seg (len (mlt ((x2 + y2),z2))) by FINSEQ_1:def_3
.= Seg (len x) by CARD_1:def_7
.= Seg (len ((mlt (x2,z2)) + (mlt (y2,z2)))) by CARD_1:def_7
.= dom ((mlt (x2,z2)) + (mlt (y2,z2))) by FINSEQ_1:def_3 ;
A4: dom (mlt (x,z)) = Seg (len (mlt (x2,z2))) by FINSEQ_1:def_3
.= Seg (len x) by CARD_1:def_7
.= Seg (len ((mlt (x2,z2)) + (mlt (y2,z2)))) by CARD_1:def_7
.= dom ((mlt (x2,z2)) + (mlt (y2,z2))) by FINSEQ_1:def_3 ;
A5: dom (mlt (y,z)) = Seg (len (mlt (y2,z2))) by FINSEQ_1:def_3
.= Seg (len x) by CARD_1:def_7
.= Seg (len ((mlt (x2,z2)) + (mlt (y2,z2)))) by CARD_1:def_7
.= dom ((mlt (x2,z2)) + (mlt (y2,z2))) by FINSEQ_1:def_3 ;
for i being Nat st i in dom (mlt ((x + y),z)) holds
(mlt ((x + y),z)) . i = ((mlt (x,z)) + (mlt (y,z))) . i
proof
let i be Nat; ::_thesis: ( i in dom (mlt ((x + y),z)) implies (mlt ((x + y),z)) . i = ((mlt (x,z)) + (mlt (y,z))) . i )
assume A6: i in dom (mlt ((x + y),z)) ; ::_thesis: (mlt ((x + y),z)) . i = ((mlt (x,z)) + (mlt (y,z))) . i
set a = x . i;
set b = y . i;
set d = (x + y) . i;
set e = z . i;
len (x2 + y2) = len x by CARD_1:def_7;
then dom (x2 + y2) = Seg (len x) by FINSEQ_1:def_3
.= Seg (len (mlt (x2,z2))) by CARD_1:def_7
.= dom (mlt (x,z)) by FINSEQ_1:def_3 ;
then A7: (x + y) . i = (x . i) + (y . i) by A3, A4, A6, COMPLSP2:1;
thus (mlt ((x + y),z)) . i = ((x + y) . i) * (z . i) by A6, Th18
.= ((x . i) * (z . i)) + ((y . i) * (z . i)) by A7
.= ((mlt (x,z)) . i) + ((y . i) * (z . i)) by A3, A4, A6, Th18
.= ((mlt (x,z)) . i) + ((mlt (y,z)) . i) by A3, A5, A6, Th18
.= ((mlt (x,z)) + (mlt (y,z))) . i by A3, A6, COMPLSP2:1 ; ::_thesis: verum
end;
hence mlt ((x + y),z) = (mlt (x,z)) + (mlt (y,z)) by A3, FINSEQ_1:13; ::_thesis: verum
end;
theorem Th36: :: MATRIXC1:36
for F1, F2 being FinSequence of COMPLEX st len F1 = len F2 holds
Sum (F1 + F2) = (Sum F1) + (Sum F2)
proof
let F1, F2 be FinSequence of COMPLEX ; ::_thesis: ( len F1 = len F2 implies Sum (F1 + F2) = (Sum F1) + (Sum F2) )
assume A1: len F1 = len F2 ; ::_thesis: Sum (F1 + F2) = (Sum F1) + (Sum F2)
reconsider y2 = F2 as Element of (len F2) -tuples_on COMPLEX by FINSEQ_2:92;
reconsider x2 = F1 as Element of (len F1) -tuples_on COMPLEX by FINSEQ_2:92;
Sum (F1 + F2) = addcomplex $$ (addcomplex .: (F1,F2)) by SEQ_4:def_6
.= addcomplex . ((addcomplex $$ x2),(addcomplex $$ y2)) by A1, SETWOP_2:35
.= (Sum F1) + (Sum F2) by BINOP_2:def_3 ;
hence Sum (F1 + F2) = (Sum F1) + (Sum F2) ; ::_thesis: verum
end;
theorem Th37: :: MATRIXC1:37
for x1, y1 being FinSequence of COMPLEX
for x2, y2 being FinSequence of REAL st x1 = x2 & y1 = y2 & len x1 = len y2 holds
multcomplex .: (x1,y1) = multreal .: (x2,y2)
proof
let x1, y1 be FinSequence of COMPLEX ; ::_thesis: for x2, y2 being FinSequence of REAL st x1 = x2 & y1 = y2 & len x1 = len y2 holds
multcomplex .: (x1,y1) = multreal .: (x2,y2)
let x2, y2 be FinSequence of REAL ; ::_thesis: ( x1 = x2 & y1 = y2 & len x1 = len y2 implies multcomplex .: (x1,y1) = multreal .: (x2,y2) )
assume that
A1: x1 = x2 and
A2: y1 = y2 and
A3: len x1 = len y2 ; ::_thesis: multcomplex .: (x1,y1) = multreal .: (x2,y2)
for i being Element of NAT st i in dom x1 holds
multcomplex . ((x1 . i),(y1 . i)) = multreal . ((x2 . i),(y2 . i))
proof
let i be Element of NAT ; ::_thesis: ( i in dom x1 implies multcomplex . ((x1 . i),(y1 . i)) = multreal . ((x2 . i),(y2 . i)) )
(x1 . i) * (y1 . i) = multcomplex . ((x1 . i),(y1 . i)) by BINOP_2:def_5;
hence ( i in dom x1 implies multcomplex . ((x1 . i),(y1 . i)) = multreal . ((x2 . i),(y2 . i)) ) by A1, A2, BINOP_2:def_11; ::_thesis: verum
end;
hence multcomplex .: (x1,y1) = multreal .: (x2,y2) by A1, A2, A3, COMPLSP2:45; ::_thesis: verum
end;
theorem :: MATRIXC1:38
for x, y being FinSequence of REAL st len x = len y holds
FR2FC (mlt (x,y)) = mlt ((FR2FC x),(FR2FC y)) by Th37;
theorem Th39: :: MATRIXC1:39
for x, y being FinSequence of COMPLEX st len x = len y holds
|(x,y)| = Sum (mlt (x,(y *')))
proof
let x, y be FinSequence of COMPLEX ; ::_thesis: ( len x = len y implies |(x,y)| = Sum (mlt (x,(y *'))) )
A1: len (Im y) = len y by COMPLSP2:48;
A2: len (y *') = len (y *') ;
A3: y *' = - (- (y *'))
.= ((- 1) * (- 1)) * (y *') by COMPLSP2:53
.= 1 * (y *') ;
A4: len (x *') = len x by COMPLSP2:def_1;
then A5: len (x + (x *')) = len x by COMPLSP2:6;
A6: len ((x *') + x) = len x by A4, COMPLSP2:6;
A7: len x = len x ;
A8: x = - (- x)
.= ((- 1) * (- 1)) * x by COMPLSP2:53
.= 1 * x ;
set Imx = FR2FC (Im x);
assume A9: len x = len y ; ::_thesis: |(x,y)| = Sum (mlt (x,(y *')))
A10: len (FR2FC (Im x)) = len y by A9, COMPLSP2:48
.= len (y *') by COMPLSP2:def_1 ;
set Imy = FR2FC (Im y);
set Rey = FR2FC (Re y);
set Rex = FR2FC (Re x);
A11: len (* * (FR2FC (Im x))) = len (FR2FC (Im x)) by COMPLSP2:3
.= len x by COMPLSP2:48
.= len (FR2FC (Re x)) by COMPLSP2:48 ;
A12: len (FR2FC (Re x)) = len x by COMPLSP2:48;
A13: len (Im x) = len x by COMPLSP2:48;
then A14: mlt ((Im x),(Im y)) = mlt ((FR2FC (Im x)),(FR2FC (Im y))) by A9, A1, Th37;
A15: len (Re y) = len y by COMPLSP2:48;
then A16: mlt ((Im x),(Re y)) = mlt ((FR2FC (Im x)),(FR2FC (Re y))) by A9, A13, Th37;
A17: len (Re x) = len x by COMPLSP2:48;
then A18: mlt ((Re x),(Re y)) = mlt ((FR2FC (Re x)),(FR2FC (Re y))) by A9, A15, Th37;
A19: mlt ((Re x),(Im y)) = mlt ((FR2FC (Re x)),(FR2FC (Im y))) by A9, A17, A1, Th37;
A20: len (** * (FR2FC (Im x))) = len (FR2FC (Im x)) by COMPLSP2:3
.= len y by A9, COMPLSP2:48
.= len (y *') by COMPLSP2:def_1 ;
FR2FC (Im x) = (- ((1 / 2) * **)) * (x - (x *')) by COMPLSP2:def_3;
then A21: ** * (FR2FC (Im x)) = (** * (- ((1 / 2) * **))) * (x - (x *')) by COMPLSP2:53
.= (1 / 2) * (x - (x *')) ;
FR2FC (Im y) = (- ((1 / 2) * **)) * (y - (y *')) by COMPLSP2:def_3;
then A22: ** * (FR2FC (Im y)) = (** * (- ((1 / 2) * **))) * (y - (y *')) by COMPLSP2:53
.= (1 / 2) * (y - (y *')) ;
A23: FR2FC (Re x) = (1 / 2) * (x + (x *')) by COMPLSP2:def_2;
A24: len (y *') = len y by COMPLSP2:def_1;
then A25: len (y + (y *')) = len y by COMPLSP2:6;
len (x - (x *')) = len x by A4, COMPLSP2:7;
then A26: (FR2FC (Re x)) + (** * (FR2FC (Im x))) = (1 / 2) * ((x + (x *')) + (x - (x *'))) by A23, A21, A5, COMPLSP2:30
.= (1 / 2) * ((x + ((x *') + x)) - (x *')) by A4, A5, COMPLSP2:37
.= (1 / 2) * (x + ((x + (x *')) - (x *'))) by A4, A6, COMPLSP2:37
.= (1 / 2) * (x + (x + ((x *') - (x *')))) by A4, COMPLSP2:37
.= (1 / 2) * (x + (x + (0c (len (x *'))))) by COMPLSP2:34
.= (1 / 2) * (x + (x + (0c (len x)))) by COMPLSP2:def_1
.= (1 / 2) * (x + x) by COMPLSP2:33
.= ((1 / 2) * x) + ((1 / 2) * x) by A7, COMPLSP2:30
.= ((1 / 2) + (1 / 2)) * x by COMPLSP2:63
.= x by A8 ;
A27: FR2FC (Re y) = (1 / 2) * (y + (y *')) by COMPLSP2:def_2;
len (y - (y *')) = len y by A24, COMPLSP2:7;
then A28: (FR2FC (Re y)) - (** * (FR2FC (Im y))) = (1 / 2) * ((y + (y *')) - (y - (y *'))) by A27, A22, A25, COMPLSP2:43
.= (1 / 2) * ((((y *') + y) - y) + (y *')) by A24, A25, COMPLSP2:40
.= (1 / 2) * (((y *') + (y - y)) + (y *')) by A24, COMPLSP2:37
.= (1 / 2) * (((y *') + (0c (len y))) + (y *')) by COMPLSP2:34
.= (1 / 2) * ((y *') + (y *')) by A24, COMPLSP2:33
.= ((1 / 2) * (y *')) + ((1 / 2) * (y *')) by A2, COMPLSP2:30
.= ((1 / 2) + (1 / 2)) * (y *') by COMPLSP2:63
.= y *' by A3 ;
A29: len (FR2FC (Re y)) = len y by COMPLSP2:48;
then A30: len (mlt ((FR2FC (Re x)),(FR2FC (Re y)))) = len x by A9, A12, FINSEQ_2:72;
A31: len (** * (FR2FC (Im y))) = len (FR2FC (Im y)) by COMPLSP2:3
.= len y by COMPLSP2:48 ;
then len (mlt ((FR2FC (Re x)),(** * (FR2FC (Im y))))) = len (FR2FC (Re x)) by A9, A12, FINSEQ_2:72;
then A32: len ((mlt ((FR2FC (Re x)),(FR2FC (Re y)))) - (mlt ((FR2FC (Re x)),(** * (FR2FC (Im y)))))) = len (mlt ((FR2FC (Re x)),(FR2FC (Re y)))) by A12, A30, COMPLSP2:7;
A33: len (FR2FC (Im x)) = len x by COMPLSP2:48;
then len (mlt ((FR2FC (Im x)),(FR2FC (Re y)))) = len x by A9, A29, FINSEQ_2:72;
then A34: len (mlt ((FR2FC (Im x)),(FR2FC (Re y)))) = len (mlt ((FR2FC (Im x)),(** * (FR2FC (Im y))))) by A9, A31, A33, FINSEQ_2:72;
A35: len (FR2FC (Im y)) = len y by COMPLSP2:48;
then A36: len (mlt ((FR2FC (Im x)),(FR2FC (Im y)))) = len x by A9, A33, FINSEQ_2:72;
A37: len (** * (mlt ((FR2FC (Re x)),(FR2FC (Im y))))) = len (mlt ((FR2FC (Re x)),(FR2FC (Im y)))) by COMPLSP2:3
.= len x by A9, A12, A35, FINSEQ_2:72 ;
A38: len (** * (mlt ((FR2FC (Im x)),(FR2FC (Re y))))) = len (mlt ((FR2FC (Im x)),(FR2FC (Re y)))) by COMPLSP2:3
.= len x by A9, A29, A33, FINSEQ_2:72 ;
then A39: len ((mlt ((FR2FC (Re x)),(FR2FC (Re y)))) - (** * (mlt ((FR2FC (Re x)),(FR2FC (Im y)))))) = len (** * (mlt ((FR2FC (Im x)),(FR2FC (Re y))))) by A30, A37, COMPLSP2:7;
len ((mlt ((FR2FC (Re x)),(FR2FC (Re y)))) - (** * (mlt ((FR2FC (Re x)),(FR2FC (Im y)))))) = len (** * (mlt ((FR2FC (Im x)),(FR2FC (Re y))))) by A30, A37, A38, COMPLSP2:7;
then A40: len (((mlt ((FR2FC (Re x)),(FR2FC (Re y)))) - (** * (mlt ((FR2FC (Re x)),(FR2FC (Im y)))))) + (** * (mlt ((FR2FC (Im x)),(FR2FC (Re y)))))) = len ((mlt ((FR2FC (Re x)),(FR2FC (Re y)))) - (** * (mlt ((FR2FC (Re x)),(FR2FC (Im y)))))) by COMPLSP2:6
.= len (mlt ((FR2FC (Im x)),(FR2FC (Im y)))) by A36, A30, A37, COMPLSP2:7 ;
|(x,y)| = ((|((Re x),(Re y))| - (** * |((Re x),(Im y))|)) + (** * |((Im x),(Re y))|)) + |((Im x),(Im y))| by COMPLSP2:def_4
.= (((Sum (mlt ((Re x),(Re y)))) - (** * |((Re x),(Im y))|)) + (** * |((Im x),(Re y))|)) + |((Im x),(Im y))|
.= (((Sum (mlt ((Re x),(Re y)))) - (** * (Sum (mlt ((Re x),(Im y)))))) + (** * |((Im x),(Re y))|)) + |((Im x),(Im y))|
.= (((Sum (mlt ((Re x),(Re y)))) - (** * (Sum (mlt ((Re x),(Im y)))))) + (** * (Sum (mlt ((Im x),(Re y)))))) + |((Im x),(Im y))|
.= (((Sum (mlt ((FR2FC (Re x)),(FR2FC (Re y))))) - (** * (Sum (mlt ((FR2FC (Re x)),(FR2FC (Im y))))))) + (** * (Sum (mlt ((FR2FC (Im x)),(FR2FC (Re y))))))) + (Sum (mlt ((Im x),(Im y)))) by A16, A18, A19
.= (((Sum (mlt ((FR2FC (Re x)),(FR2FC (Re y))))) - (Sum (** * (mlt ((FR2FC (Re x)),(FR2FC (Im y))))))) + (** * (Sum (mlt ((FR2FC (Im x)),(FR2FC (Re y))))))) + (Sum (mlt ((FR2FC (Im x)),(FR2FC (Im y))))) by A14, Th28
.= (((Sum (mlt ((FR2FC (Re x)),(FR2FC (Re y))))) - (Sum (** * (mlt ((FR2FC (Re x)),(FR2FC (Im y))))))) + (Sum (** * (mlt ((FR2FC (Im x)),(FR2FC (Re y))))))) + (Sum (mlt ((FR2FC (Im x)),(FR2FC (Im y))))) by Th28
.= ((Sum ((mlt ((FR2FC (Re x)),(FR2FC (Re y)))) - (** * (mlt ((FR2FC (Re x)),(FR2FC (Im y))))))) + (Sum (** * (mlt ((FR2FC (Im x)),(FR2FC (Re y))))))) + (Sum (mlt ((FR2FC (Im x)),(FR2FC (Im y))))) by A30, A37, Th31
.= (Sum (((mlt ((FR2FC (Re x)),(FR2FC (Re y)))) - (** * (mlt ((FR2FC (Re x)),(FR2FC (Im y)))))) + (** * (mlt ((FR2FC (Im x)),(FR2FC (Re y))))))) + (Sum (mlt ((FR2FC (Im x)),(FR2FC (Im y))))) by A39, Th36
.= Sum ((((mlt ((FR2FC (Re x)),(FR2FC (Re y)))) - (** * (mlt ((FR2FC (Re x)),(FR2FC (Im y)))))) + (** * (mlt ((FR2FC (Im x)),(FR2FC (Re y)))))) + (mlt ((FR2FC (Im x)),(FR2FC (Im y))))) by A40, Th36
.= Sum ((((mlt ((FR2FC (Re x)),(FR2FC (Re y)))) - (mlt ((FR2FC (Re x)),(** * (FR2FC (Im y)))))) + (** * (mlt ((FR2FC (Im x)),(FR2FC (Re y)))))) + (mlt ((FR2FC (Im x)),(FR2FC (Im y))))) by A9, A12, A35, Th25
.= Sum (((mlt ((FR2FC (Re x)),(FR2FC (Re y)))) - (mlt ((FR2FC (Re x)),(** * (FR2FC (Im y)))))) + ((** * (mlt ((FR2FC (Im x)),(FR2FC (Re y))))) + (- (- (mlt ((FR2FC (Im x)),(FR2FC (Im y)))))))) by A36, A30, A38, A32, COMPLSP2:28
.= Sum (((mlt ((FR2FC (Re x)),(FR2FC (Re y)))) - (mlt ((FR2FC (Re x)),(** * (FR2FC (Im y)))))) + ((** * (mlt ((FR2FC (Im x)),(FR2FC (Re y))))) - ((** * **) * (mlt ((FR2FC (Im x)),(FR2FC (Im y)))))))
.= Sum (((mlt ((FR2FC (Re x)),(FR2FC (Re y)))) - (mlt ((FR2FC (Re x)),(** * (FR2FC (Im y)))))) + ((** * (mlt ((FR2FC (Im x)),(FR2FC (Re y))))) - (** * (** * (mlt ((FR2FC (Im x)),(FR2FC (Im y)))))))) by COMPLSP2:53
.= Sum (((mlt ((FR2FC (Re x)),(FR2FC (Re y)))) - (mlt ((FR2FC (Re x)),(** * (FR2FC (Im y)))))) + ((** * (mlt ((FR2FC (Im x)),(FR2FC (Re y))))) - (** * (mlt ((FR2FC (Im x)),(** * (FR2FC (Im y)))))))) by A9, A35, A33, Th25
.= Sum (((mlt ((FR2FC (Re x)),(FR2FC (Re y)))) - (mlt ((FR2FC (Re x)),(** * (FR2FC (Im y)))))) + (** * ((mlt ((FR2FC (Im x)),(FR2FC (Re y)))) - (mlt ((FR2FC (Im x)),(** * (FR2FC (Im y)))))))) by A34, COMPLSP2:43
.= Sum (((mlt ((FR2FC (Re x)),(FR2FC (Re y)))) - (mlt ((FR2FC (Re x)),(** * (FR2FC (Im y)))))) + (** * (mlt ((FR2FC (Im x)),(y *'))))) by A9, A31, A29, A33, A28, Th33
.= Sum ((mlt ((FR2FC (Re x)),((FR2FC (Re y)) - (** * (FR2FC (Im y)))))) + (** * (mlt ((FR2FC (Im x)),(y *'))))) by A9, A31, A29, A12, Th33
.= Sum ((mlt ((FR2FC (Re x)),(y *'))) + (mlt ((** * (FR2FC (Im x))),(y *')))) by A10, A28, Th26
.= Sum (mlt (x,(y *'))) by A11, A20, A26, Th35 ;
hence |(x,y)| = Sum (mlt (x,(y *'))) ; ::_thesis: verum
end;
theorem :: MATRIXC1:40
for i, j being Nat
for M1, M2 being Matrix of COMPLEX st width M1 = width M2 & j in Seg (len M1) holds
Line ((M1 + M2),j) = (Line (M1,j)) + (Line (M2,j))
proof
let i, j be Nat; ::_thesis: for M1, M2 being Matrix of COMPLEX st width M1 = width M2 & j in Seg (len M1) holds
Line ((M1 + M2),j) = (Line (M1,j)) + (Line (M2,j))
let M1, M2 be Matrix of COMPLEX; ::_thesis: ( width M1 = width M2 & j in Seg (len M1) implies Line ((M1 + M2),j) = (Line (M1,j)) + (Line (M2,j)) )
assume that
A1: width M1 = width M2 and
A2: j in Seg (len M1) ; ::_thesis: Line ((M1 + M2),j) = (Line (M1,j)) + (Line (M2,j))
len (Line (M2,j)) = width M1 by A1, MATRIX_1:def_7
.= len (Line (M1,j)) by MATRIX_1:def_7 ;
then A3: len ((Line (M1,j)) + (Line (M2,j))) = len (Line (M1,j)) by COMPLSP2:6
.= width M1 by MATRIX_1:def_7 ;
A4: len (Line ((M1 + M2),j)) = width (M1 + M2) by MATRIX_1:def_7
.= width M1 by Th6 ;
A5: width (M1 + M2) = width M1 by Th6;
now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_(Line_((M1_+_M2),j))_holds_
(Line_((M1_+_M2),j))_._i_=_((Line_(M1,j))_+_(Line_(M2,j)))_._i
let i be Nat; ::_thesis: ( 1 <= i & i <= len (Line ((M1 + M2),j)) implies (Line ((M1 + M2),j)) . i = ((Line (M1,j)) + (Line (M2,j))) . i )
assume that
A6: 1 <= i and
A7: i <= len (Line ((M1 + M2),j)) ; ::_thesis: (Line ((M1 + M2),j)) . i = ((Line (M1,j)) + (Line (M2,j))) . i
A8: i in Seg (width M1) by A4, A6, A7, FINSEQ_1:1;
i in Seg (width M1) by A4, A6, A7, FINSEQ_1:1;
then [j,i] in [:(Seg (len M1)),(Seg (width M1)):] by A2, ZFMISC_1:87;
then A9: [j,i] in Indices M1 by FINSEQ_1:def_3;
i in Seg (len ((Line (M1,j)) + (Line (M2,j)))) by A3, A4, A6, A7, FINSEQ_1:1;
then A10: i in dom ((Line (M1,j)) + (Line (M2,j))) by FINSEQ_1:def_3;
A11: i in Seg (width M2) by A1, A4, A6, A7, FINSEQ_1:1;
i in Seg (width (M1 + M2)) by A5, A4, A6, A7, FINSEQ_1:1;
hence (Line ((M1 + M2),j)) . i = (M1 + M2) * (j,i) by MATRIX_1:def_7
.= (M1 * (j,i)) + (M2 * (j,i)) by A9, Th7
.= (M1 * (j,i)) + ((Line (M2,j)) . i) by A11, MATRIX_1:def_7
.= ((Line (M1,j)) . i) + ((Line (M2,j)) . i) by A8, MATRIX_1:def_7
.= ((Line (M1,j)) + (Line (M2,j))) . i by A10, COMPLSP2:1 ;
::_thesis: verum
end;
hence Line ((M1 + M2),j) = (Line (M1,j)) + (Line (M2,j)) by A3, A4, FINSEQ_1:14; ::_thesis: verum
end;
theorem Th41: :: MATRIXC1:41
for i being Nat
for M being Matrix of COMPLEX st i in Seg (len M) holds
Line (M,i) = (Line ((M *'),i)) *'
proof
let i be Nat; ::_thesis: for M being Matrix of COMPLEX st i in Seg (len M) holds
Line (M,i) = (Line ((M *'),i)) *'
let M be Matrix of COMPLEX; ::_thesis: ( i in Seg (len M) implies Line (M,i) = (Line ((M *'),i)) *' )
assume A1: i in Seg (len M) ; ::_thesis: Line (M,i) = (Line ((M *'),i)) *'
A2: len (Line (M,i)) = width M by MATRIX_1:def_7;
A3: len ((Line ((M *'),i)) *') = len (Line ((M *'),i)) by COMPLSP2:def_1
.= width (M *') by MATRIX_1:def_7
.= width M by Def1 ;
for j being Nat st 1 <= j & j <= len (Line (M,i)) holds
(Line (M,i)) . j = ((Line ((M *'),i)) *') . j
proof
A4: i <= len M by A1, FINSEQ_1:1;
A5: 1 <= i by A1, FINSEQ_1:1;
let j be Nat; ::_thesis: ( 1 <= j & j <= len (Line (M,i)) implies (Line (M,i)) . j = ((Line ((M *'),i)) *') . j )
assume that
A6: 1 <= j and
A7: j <= len (Line (M,i)) ; ::_thesis: (Line (M,i)) . j = ((Line ((M *'),i)) *') . j
A8: j in Seg (width M) by A2, A6, A7, FINSEQ_1:1;
then A9: j in Seg (width (M *')) by Def1;
j <= len ((Line ((M *'),i)) *') by A3, A7, MATRIX_1:def_7;
then A10: j <= len (Line ((M *'),i)) by COMPLSP2:def_1;
j <= width M by A7, MATRIX_1:def_7;
then A11: [i,j] in Indices M by A6, A5, A4, Th1;
(Line (M,i)) . j = ((M * (i,j)) *') *' by A8, MATRIX_1:def_7
.= ((M *') * (i,j)) *' by A11, Def1
.= ((Line ((M *'),i)) . j) *' by A9, MATRIX_1:def_7
.= ((Line ((M *'),i)) *') . j by A6, A10, COMPLSP2:def_1 ;
hence (Line (M,i)) . j = ((Line ((M *'),i)) *') . j ; ::_thesis: verum
end;
hence Line (M,i) = (Line ((M *'),i)) *' by A2, A3, FINSEQ_1:14; ::_thesis: verum
end;
theorem Th42: :: MATRIXC1:42
for i being Nat
for F being FinSequence of COMPLEX
for M being Matrix of COMPLEX st len F = width M holds
mlt (F,((Line ((M *'),i)) *')) = (mlt ((Line ((M *'),i)),(F *'))) *'
proof
let i be Nat; ::_thesis: for F being FinSequence of COMPLEX
for M being Matrix of COMPLEX st len F = width M holds
mlt (F,((Line ((M *'),i)) *')) = (mlt ((Line ((M *'),i)),(F *'))) *'
let F be FinSequence of COMPLEX ; ::_thesis: for M being Matrix of COMPLEX st len F = width M holds
mlt (F,((Line ((M *'),i)) *')) = (mlt ((Line ((M *'),i)),(F *'))) *'
let M be Matrix of COMPLEX; ::_thesis: ( len F = width M implies mlt (F,((Line ((M *'),i)) *')) = (mlt ((Line ((M *'),i)),(F *'))) *' )
assume A1: len F = width M ; ::_thesis: mlt (F,((Line ((M *'),i)) *')) = (mlt ((Line ((M *'),i)),(F *'))) *'
len (Line ((M *'),i)) = width (M *') by MATRIX_1:def_7
.= width M by Def1 ;
hence mlt (F,((Line ((M *'),i)) *')) = (mlt ((Line ((M *'),i)),(F *'))) *' by A1, Th24; ::_thesis: verum
end;
theorem Th43: :: MATRIXC1:43
for F being FinSequence of COMPLEX
for M being Matrix of COMPLEX st len F = width M & len F >= 1 holds
(M * F) *' = (M *') * (F *')
proof
let F be FinSequence of COMPLEX ; ::_thesis: for M being Matrix of COMPLEX st len F = width M & len F >= 1 holds
(M * F) *' = (M *') * (F *')
let M be Matrix of COMPLEX; ::_thesis: ( len F = width M & len F >= 1 implies (M * F) *' = (M *') * (F *') )
assume that
A1: len F = width M and
A2: len F >= 1 ; ::_thesis: (M * F) *' = (M *') * (F *')
A3: len (F *') = len F by COMPLSP2:def_1;
A4: width (M *') = width M by Def1;
A5: len ((M * F) *') = len (M * F) by COMPLSP2:def_1
.= len M by Def6 ;
A6: len (M *') = len M by Def1;
A7: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_((M_*_F)_*')_holds_
((M_*_F)_*')_._i_=_((M_*')_*_(F_*'))_._i
let i be Nat; ::_thesis: ( 1 <= i & i <= len ((M * F) *') implies ((M * F) *') . i = ((M *') * (F *')) . i )
assume that
A8: 1 <= i and
A9: i <= len ((M * F) *') ; ::_thesis: ((M * F) *') . i = ((M *') * (F *')) . i
A10: i in Seg (len M) by A5, A8, A9, FINSEQ_1:1;
len (Line ((M *'),i)) = len (F *') by A1, A3, A4, MATRIX_1:def_7;
then A11: len (mlt ((Line ((M *'),i)),(F *'))) >= 1 by A2, A3, FINSEQ_2:72;
A12: i in Seg (len (M *')) by A5, A6, A8, A9, FINSEQ_1:1;
i <= len (M * F) by A9, COMPLSP2:def_1;
hence ((M * F) *') . i = ((M * F) . i) *' by A8, COMPLSP2:def_1
.= (Sum (mlt (F,(Line (M,i))))) *' by A10, Def6
.= (Sum (mlt (F,((Line ((M *'),i)) *')))) *' by A10, Th41
.= (Sum ((mlt ((Line ((M *'),i)),(F *'))) *')) *' by A1, Th42
.= ((Sum (mlt ((Line ((M *'),i)),(F *')))) *') *' by A11, Th23
.= ((M *') * (F *')) . i by A12, Def6 ;
::_thesis: verum
end;
len ((M *') * (F *')) = len (M *') by Def6
.= len M by Def1 ;
hence (M * F) *' = (M *') * (F *') by A5, A7, FINSEQ_1:14; ::_thesis: verum
end;
theorem :: MATRIXC1:44
for F1, F2, F3 being FinSequence of COMPLEX st len F1 = len F2 & len F2 = len F3 holds
mlt (F1,(mlt (F2,F3))) = mlt ((mlt (F1,F2)),F3)
proof
let F1, F2, F3 be FinSequence of COMPLEX ; ::_thesis: ( len F1 = len F2 & len F2 = len F3 implies mlt (F1,(mlt (F2,F3))) = mlt ((mlt (F1,F2)),F3) )
assume that
A1: len F1 = len F2 and
A2: len F2 = len F3 ; ::_thesis: mlt (F1,(mlt (F2,F3))) = mlt ((mlt (F1,F2)),F3)
reconsider f3 = F3 as Element of (len F3) -tuples_on COMPLEX by FINSEQ_2:92;
reconsider f2 = F2 as Element of (len F2) -tuples_on COMPLEX by FINSEQ_2:92;
reconsider f1 = F1 as Element of (len F1) -tuples_on COMPLEX by FINSEQ_2:92;
thus mlt (F1,(mlt (F2,F3))) = multcomplex .: ((multcomplex .: (f1,f2)),f3) by A1, A2, FINSEQOP:28
.= mlt ((mlt (F1,F2)),F3) ; ::_thesis: verum
end;
theorem :: MATRIXC1:45
for F being FinSequence of COMPLEX holds Sum (- F) = - (Sum F)
proof
let F be FinSequence of COMPLEX ; ::_thesis: Sum (- F) = - (Sum F)
thus Sum (- F) = addcomplex $$ (compcomplex * F) by SEQ_4:def_8
.= compcomplex . (addcomplex $$ F) by SEQ_4:51, SEQ_4:52, SETWOP_2:31
.= - (Sum F) by BINOP_2:def_1 ; ::_thesis: verum
end;
theorem Th46: :: MATRIXC1:46
for F1, F2 being FinSequence of COMPLEX holds Sum (F1 ^ F2) = (Sum F1) + (Sum F2)
proof
let F1, F2 be FinSequence of COMPLEX ; ::_thesis: Sum (F1 ^ F2) = (Sum F1) + (Sum F2)
thus Sum (F1 ^ F2) = addcomplex . ((addcomplex $$ F1),(addcomplex $$ F2)) by FINSOP_1:5
.= (Sum F1) + (Sum F2) by BINOP_2:def_3 ; ::_thesis: verum
end;
definition
let M be Matrix of COMPLEX;
func LineSum M -> FinSequence of COMPLEX means :Def9: :: MATRIXC1:def 9
( len it = len M & ( for i being Nat st i in Seg (len M) holds
it . i = Sum (Line (M,i)) ) );
existence
ex b1 being FinSequence of COMPLEX st
( len b1 = len M & ( for i being Nat st i in Seg (len M) holds
b1 . i = Sum (Line (M,i)) ) )
proof
deffunc H1( Nat) -> Element of COMPLEX = Sum (Line (M,$1));
consider z being FinSequence of COMPLEX such that
A1: len z = len M and
A2: for j being Nat st j in dom z holds
z . j = H1(j) from FINSEQ_2:sch_1();
take z ; ::_thesis: ( len z = len M & ( for i being Nat st i in Seg (len M) holds
z . i = Sum (Line (M,i)) ) )
thus len z = len M by A1; ::_thesis: for i being Nat st i in Seg (len M) holds
z . i = Sum (Line (M,i))
let j be Nat; ::_thesis: ( j in Seg (len M) implies z . j = Sum (Line (M,j)) )
dom z = Seg (len M) by A1, FINSEQ_1:def_3;
hence ( j in Seg (len M) implies z . j = Sum (Line (M,j)) ) by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being FinSequence of COMPLEX st len b1 = len M & ( for i being Nat st i in Seg (len M) holds
b1 . i = Sum (Line (M,i)) ) & len b2 = len M & ( for i being Nat st i in Seg (len M) holds
b2 . i = Sum (Line (M,i)) ) holds
b1 = b2
proof
let p1, p2 be FinSequence of COMPLEX ; ::_thesis: ( len p1 = len M & ( for i being Nat st i in Seg (len M) holds
p1 . i = Sum (Line (M,i)) ) & len p2 = len M & ( for i being Nat st i in Seg (len M) holds
p2 . i = Sum (Line (M,i)) ) implies p1 = p2 )
assume that
A3: len p1 = len M and
A4: for j being Nat st j in Seg (len M) holds
p1 . j = Sum (Line (M,j)) and
A5: len p2 = len M and
A6: for j being Nat st j in Seg (len M) holds
p2 . j = Sum (Line (M,j)) ; ::_thesis: p1 = p2
A7: dom p1 = Seg (len M) by A3, FINSEQ_1:def_3;
for j being Nat st j in dom p1 holds
p1 . j = p2 . j
proof
let j be Nat; ::_thesis: ( j in dom p1 implies p1 . j = p2 . j )
assume A8: j in dom p1 ; ::_thesis: p1 . j = p2 . j
then p1 . j = Sum (Line (M,j)) by A4, A7;
hence p1 . j = p2 . j by A6, A7, A8; ::_thesis: verum
end;
hence p1 = p2 by A3, A5, FINSEQ_2:9; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines LineSum MATRIXC1:def_9_:_
for M being Matrix of COMPLEX
for b2 being FinSequence of COMPLEX holds
( b2 = LineSum M iff ( len b2 = len M & ( for i being Nat st i in Seg (len M) holds
b2 . i = Sum (Line (M,i)) ) ) );
definition
let M be Matrix of COMPLEX;
func ColSum M -> FinSequence of COMPLEX means :Def10: :: MATRIXC1:def 10
( len it = width M & ( for j being Nat st j in Seg (width M) holds
it . j = Sum (Col (M,j)) ) );
existence
ex b1 being FinSequence of COMPLEX st
( len b1 = width M & ( for j being Nat st j in Seg (width M) holds
b1 . j = Sum (Col (M,j)) ) )
proof
deffunc H1( Nat) -> Element of COMPLEX = Sum (Col (M,$1));
consider f being FinSequence of COMPLEX such that
A1: len f = width M and
A2: for j being Nat st j in dom f holds
f . j = H1(j) from FINSEQ_2:sch_1();
take f ; ::_thesis: ( len f = width M & ( for j being Nat st j in Seg (width M) holds
f . j = Sum (Col (M,j)) ) )
thus len f = width M by A1; ::_thesis: for j being Nat st j in Seg (width M) holds
f . j = Sum (Col (M,j))
let j be Nat; ::_thesis: ( j in Seg (width M) implies f . j = Sum (Col (M,j)) )
dom f = Seg (width M) by A1, FINSEQ_1:def_3;
hence ( j in Seg (width M) implies f . j = Sum (Col (M,j)) ) by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being FinSequence of COMPLEX st len b1 = width M & ( for j being Nat st j in Seg (width M) holds
b1 . j = Sum (Col (M,j)) ) & len b2 = width M & ( for j being Nat st j in Seg (width M) holds
b2 . j = Sum (Col (M,j)) ) holds
b1 = b2
proof
let p1, p2 be FinSequence of COMPLEX ; ::_thesis: ( len p1 = width M & ( for j being Nat st j in Seg (width M) holds
p1 . j = Sum (Col (M,j)) ) & len p2 = width M & ( for j being Nat st j in Seg (width M) holds
p2 . j = Sum (Col (M,j)) ) implies p1 = p2 )
assume that
A3: len p1 = width M and
A4: for j being Nat st j in Seg (width M) holds
p1 . j = Sum (Col (M,j)) and
A5: len p2 = width M and
A6: for j being Nat st j in Seg (width M) holds
p2 . j = Sum (Col (M,j)) ; ::_thesis: p1 = p2
A7: dom p1 = Seg (width M) by A3, FINSEQ_1:def_3;
for j being Nat st j in dom p1 holds
p1 . j = p2 . j
proof
let j be Nat; ::_thesis: ( j in dom p1 implies p1 . j = p2 . j )
assume A8: j in dom p1 ; ::_thesis: p1 . j = p2 . j
then p1 . j = Sum (Col (M,j)) by A4, A7;
hence p1 . j = p2 . j by A6, A7, A8; ::_thesis: verum
end;
hence p1 = p2 by A3, A5, FINSEQ_2:9; ::_thesis: verum
end;
end;
:: deftheorem Def10 defines ColSum MATRIXC1:def_10_:_
for M being Matrix of COMPLEX
for b2 being FinSequence of COMPLEX holds
( b2 = ColSum M iff ( len b2 = width M & ( for j being Nat st j in Seg (width M) holds
b2 . j = Sum (Col (M,j)) ) ) );
theorem Th47: :: MATRIXC1:47
for F being FinSequence of COMPLEX st len F = 1 holds
Sum F = F . 1
proof
let F be FinSequence of COMPLEX ; ::_thesis: ( len F = 1 implies Sum F = F . 1 )
assume len F = 1 ; ::_thesis: Sum F = F . 1
then F = <*(F . 1)*> by FINSEQ_1:40;
hence Sum F = F . 1 by FINSOP_1:11; ::_thesis: verum
end;
theorem Th48: :: MATRIXC1:48
for f, g being FinSequence of COMPLEX
for n being Nat st len f = n + 1 & g = f | n holds
Sum f = (Sum g) + (f /. (len f))
proof
let f, g be FinSequence of COMPLEX ; ::_thesis: for n being Nat st len f = n + 1 & g = f | n holds
Sum f = (Sum g) + (f /. (len f))
let n be Nat; ::_thesis: ( len f = n + 1 & g = f | n implies Sum f = (Sum g) + (f /. (len f)) )
assume that
A1: len f = n + 1 and
A2: g = f | n ; ::_thesis: Sum f = (Sum g) + (f /. (len f))
A3: dom f = Seg (n + 1) by A1, FINSEQ_1:def_3;
set q = <*(f /. (len f))*>;
set p = g ^ <*(f /. (len f))*>;
A4: len <*(f /. (len f))*> = 1 by FINSEQ_1:39;
set n9 = Seg n;
A5: g = f | (Seg n) by A2, FINSEQ_1:def_15;
A6: n <= len f by A1, NAT_1:11;
A7: now__::_thesis:_for_u_being_set_st_u_in_dom_f_holds_
f_._u_=_(g_^_<*(f_/._(len_f))*>)_._u
let u be set ; ::_thesis: ( u in dom f implies f . u = (g ^ <*(f /. (len f))*>) . u )
assume A8: u in dom f ; ::_thesis: f . u = (g ^ <*(f /. (len f))*>) . u
then u in { k where k is Element of NAT : ( 1 <= k & k <= n + 1 ) } by A3, FINSEQ_1:def_1;
then consider i being Element of NAT such that
A9: u = i and
A10: 1 <= i and
A11: i <= n + 1 ;
now__::_thesis:_(_(_i_=_n_+_1_&_(g_^_<*(f_/._(len_f))*>)_._i_=_f_._i_)_or_(_i_<>_n_+_1_&_(g_^_<*(f_/._(len_f))*>)_._i_=_f_._i_)_)
percases ( i = n + 1 or i <> n + 1 ) ;
caseA12: i = n + 1 ; ::_thesis: (g ^ <*(f /. (len f))*>) . i = f . i
then A13: (len g) + 1 <= i by A1, A2, FINSEQ_1:59, NAT_1:11;
i <= (len g) + (len <*(f /. (len f))*>) by A1, A2, A4, A12, FINSEQ_1:59, NAT_1:11;
hence (g ^ <*(f /. (len f))*>) . i = <*(f /. (len f))*> . (i - (len g)) by A13, FINSEQ_1:23
.= <*(f /. (len f))*> . ((n + 1) - n) by A1, A2, A12, FINSEQ_1:59, NAT_1:11
.= f /. (n + 1) by A1, FINSEQ_1:40
.= f . i by A8, A9, A12, PARTFUN1:def_6 ;
::_thesis: verum
end;
case i <> n + 1 ; ::_thesis: (g ^ <*(f /. (len f))*>) . i = f . i
then i < n + 1 by A11, XXREAL_0:1;
then i <= n by NAT_1:13;
then i in { k where k is Element of NAT : ( 1 <= k & k <= n ) } by A10;
then i in Seg n by FINSEQ_1:def_1;
then A14: i in dom g by A5, A6, FINSEQ_1:17;
then (g ^ <*(f /. (len f))*>) . i = g . i by FINSEQ_1:def_7;
hence (g ^ <*(f /. (len f))*>) . i = f . i by A5, A14, FUNCT_1:47; ::_thesis: verum
end;
end;
end;
hence f . u = (g ^ <*(f /. (len f))*>) . u by A9; ::_thesis: verum
end;
len (g ^ <*(f /. (len f))*>) = (len g) + (len <*(f /. (len f))*>) by FINSEQ_1:22
.= (len g) + 1 by FINSEQ_1:40
.= len f by A1, A2, FINSEQ_1:59, NAT_1:11 ;
then dom f = Seg (len (g ^ <*(f /. (len f))*>)) by FINSEQ_1:def_3
.= dom (g ^ <*(f /. (len f))*>) by FINSEQ_1:def_3 ;
then f = g ^ <*(f /. (len f))*> by A7, FUNCT_1:2;
hence Sum f = (Sum g) + (Sum <*(f /. (len f))*>) by Th46
.= (Sum g) + (f /. (len f)) by FINSOP_1:11 ;
::_thesis: verum
end;
theorem Th49: :: MATRIXC1:49
for M being Matrix of COMPLEX st len M > 0 holds
Sum (LineSum M) = Sum (ColSum M)
proof
defpred S1[ Nat] means for N being Matrix of COMPLEX st $1 + 1 = len N holds
Sum (LineSum N) = Sum (ColSum N);
let M be Matrix of COMPLEX; ::_thesis: ( len M > 0 implies Sum (LineSum M) = Sum (ColSum M) )
assume len M > 0 ; ::_thesis: Sum (LineSum M) = Sum (ColSum M)
then 0 + 1 <= len M by NAT_1:8;
then (0 + 1) - 1 <= (len M) - 1 by XREAL_1:9;
then A1: (len M) -' 1 = (len M) - 1 by XREAL_0:def_2;
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; ::_thesis: S1[k + 1]
for N being Matrix of COMPLEX st (k + 1) + 1 = len N holds
Sum (LineSum N) = Sum (ColSum N)
proof
reconsider k1 = k + 1 as Element of NAT ;
let N be Matrix of COMPLEX; ::_thesis: ( (k + 1) + 1 = len N implies Sum (LineSum N) = Sum (ColSum N) )
consider n being Nat such that
A4: for x being set st x in rng N holds
ex p being FinSequence of COMPLEX st
( x = p & len p = n ) by MATRIX_1:9;
A5: rng (N | k1) c= rng N by FINSEQ_5:19;
then for x being set st x in rng (N | k1) holds
ex p being FinSequence of COMPLEX st
( x = p & len p = n ) by A4;
then reconsider N2 = N | k1 as Matrix of COMPLEX by MATRIX_1:9;
set g1 = LineSum N2;
consider n3 being Nat such that
A6: for x2 being set st x2 in rng N holds
ex s being FinSequence st
( s = x2 & len s = n3 ) by MATRIX_1:def_1;
set f3 = LineSum N;
A7: len (Line (N,((k + 1) + 1))) = width N by MATRIX_1:def_7;
assume A8: (k + 1) + 1 = len N ; ::_thesis: Sum (LineSum N) = Sum (ColSum N)
then A9: len N2 = k + 1 by FINSEQ_1:59, NAT_1:11;
A10: len (LineSum N2) = len N2 by Def9
.= k1 by A8, FINSEQ_1:59, NAT_1:11 ;
1 + k >= 1 by NAT_1:11;
then A11: len N2 >= 1 by A8, FINSEQ_1:59, NAT_1:11;
then A12: len N2 > 0 ;
1 in Seg (len N2) by FINSEQ_1:1, A11;
then 1 in dom N2 by FINSEQ_1:def_3;
then A13: N2 . 1 in rng N2 by FUNCT_1:3;
then ex s3 being FinSequence st
( s3 = N2 . 1 & len s3 = n3 ) by A5, A6;
then A14: width N2 = n3 by A13, MATRIX_1:def_3, A12;
A15: len N >= 1 by A8, NAT_1:11;
then A16: len N > 0 ;
1 in Seg (len N) by FINSEQ_1:1, A15;
then A17: 1 in dom N by FINSEQ_1:def_3;
then A18: N . 1 in rng N by FUNCT_1:3;
A19: ex s2 being FinSequence st
( s2 = N . 1 & len s2 = n3 ) by A6, A17, FUNCT_1:3;
then A20: width N2 = width N by A18, A14, MATRIX_1:def_3, A16;
len (LineSum N) = k1 + 1 by A8, Def9;
then A21: len ((LineSum N) | k1) = len (LineSum N2) by A10, FINSEQ_1:59, NAT_1:11;
A22: for n being Nat st 1 <= n & n <= len ((LineSum N) | k1) holds
((LineSum N) | k1) . n = (LineSum N2) . n
proof
let n be Nat; ::_thesis: ( 1 <= n & n <= len ((LineSum N) | k1) implies ((LineSum N) | k1) . n = (LineSum N2) . n )
assume that
A23: 1 <= n and
A24: n <= len ((LineSum N) | k1) ; ::_thesis: ((LineSum N) | k1) . n = (LineSum N2) . n
A25: n <= k1 + 1 by A10, A21, A24, NAT_1:13;
then A26: n in Seg (len N) by A8, A23, FINSEQ_1:1;
A27: for n1 being Nat st 1 <= n1 & n1 <= len (Line (N,n)) holds
(Line (N,n)) . n1 = (Line (N2,n)) . n1
proof
A28: N2 . n = N . n by A10, A21, A24, FINSEQ_3:112;
A29: n <= len N2 by A21, A24, Def9;
let n1 be Nat; ::_thesis: ( 1 <= n1 & n1 <= len (Line (N,n)) implies (Line (N,n)) . n1 = (Line (N2,n)) . n1 )
assume that
A30: 1 <= n1 and
A31: n1 <= len (Line (N,n)) ; ::_thesis: (Line (N,n)) . n1 = (Line (N2,n)) . n1
A32: n1 in Seg (len (Line (N,n))) by A30, A31, FINSEQ_1:1;
then A33: n1 in Seg (width N2) by A20, MATRIX_1:def_7;
A34: n1 in Seg (width N) by A32, MATRIX_1:def_7;
then n1 <= width N by FINSEQ_1:1;
then [n,n1] in Indices N by A8, A23, A25, A30, Th1;
then A35: ex pn being FinSequence of COMPLEX st
( pn = N . n & N * (n,n1) = pn . n1 ) by MATRIX_1:def_5;
n1 <= width N by A34, FINSEQ_1:1;
then n1 <= width N2 by A8, A18, A19, A14, MATRIX_1:def_3, A12;
then A36: [n,n1] in Indices N2 by A23, A30, A29, Th1;
n1 in Seg (width N) by A32, MATRIX_1:def_7;
then (Line (N,n)) . n1 = N * (n,n1) by MATRIX_1:def_7
.= N2 * (n,n1) by A36, A35, A28, MATRIX_1:def_5
.= (Line (N2,n)) . n1 by A33, MATRIX_1:def_7 ;
hence (Line (N,n)) . n1 = (Line (N2,n)) . n1 ; ::_thesis: verum
end;
len (Line (N,n)) = width N by MATRIX_1:def_7
.= width N2 by A8, A18, A19, A14, MATRIX_1:def_3, A12
.= len (Line (N2,n)) by MATRIX_1:def_7 ;
then A37: Line (N,n) = Line (N2,n) by A27, FINSEQ_1:14;
n in Seg (len ((LineSum N) | k1)) by A23, A24, FINSEQ_1:1;
then n in dom ((LineSum N) | k1) by FINSEQ_1:def_3;
then A38: n in dom ((LineSum N) | (Seg k1)) by FINSEQ_1:def_15;
n in Seg k1 by A10, A21, A23, A24, FINSEQ_1:1;
then A39: n in Seg (len N2) by A8, FINSEQ_1:59, NAT_1:11;
((LineSum N) | k1) . n = ((LineSum N) | (Seg k1)) . n by FINSEQ_1:def_15
.= (LineSum N) . n by A38, FUNCT_1:47
.= Sum (Line (N2,n)) by A26, A37, Def9
.= (LineSum N2) . n by A39, Def9 ;
hence ((LineSum N) | k1) . n = (LineSum N2) . n ; ::_thesis: verum
end;
len (ColSum N2) = width N2 by Def10;
then A40: len ((ColSum N2) + (Line (N,((k + 1) + 1)))) = width N by A20, A7, COMPLSP2:6
.= len (ColSum N) by Def10 ;
A41: len (ColSum N2) = width N2 by Def10
.= width N by A8, A18, A19, A14, MATRIX_1:def_3, A12
.= len (Line (N,((k + 1) + 1))) by MATRIX_1:def_7 ;
A42: (k + 1) + 1 in Seg (len N) by A8, FINSEQ_1:3;
then (k + 1) + 1 in Seg (len (LineSum N)) by Def9;
then A43: (k + 1) + 1 in dom (LineSum N) by FINSEQ_1:def_3;
A44: len N >= k + 1 by A8, NAT_1:11;
A45: for j being Nat st 1 <= j & j <= width N holds
((ColSum N2) . j) + (N * (((k + 1) + 1),j)) = (ColSum N) . j
proof
let j be Nat; ::_thesis: ( 1 <= j & j <= width N implies ((ColSum N2) . j) + (N * (((k + 1) + 1),j)) = (ColSum N) . j )
assume that
A46: 1 <= j and
A47: j <= width N ; ::_thesis: ((ColSum N2) . j) + (N * (((k + 1) + 1),j)) = (ColSum N) . j
set g = Col (N2,j);
set f = Col (N,j);
A48: k1 <= len (Col (N,j)) by A44, MATRIX_1:def_8;
A49: for n being Nat st 1 <= n & n <= len ((Col (N,j)) | k1) holds
((Col (N,j)) | k1) . n = (Col (N2,j)) . n
proof
let n be Nat; ::_thesis: ( 1 <= n & n <= len ((Col (N,j)) | k1) implies ((Col (N,j)) | k1) . n = (Col (N2,j)) . n )
assume that
A50: 1 <= n and
A51: n <= len ((Col (N,j)) | k1) ; ::_thesis: ((Col (N,j)) | k1) . n = (Col (N2,j)) . n
A52: n <= k1 by A48, A51, FINSEQ_1:59;
then A53: N2 . n = N . n by FINSEQ_3:112;
n <= k1 + 1 by A52, NAT_1:13;
then n in Seg (len N) by A8, A50, FINSEQ_1:1;
then A54: n in dom N by FINSEQ_1:def_3;
n <= len N by A8, A52, NAT_1:13;
then [n,j] in Indices N by A46, A47, A50, Th1;
then A55: ex pn being FinSequence of COMPLEX st
( pn = N . n & N * (n,j) = pn . j ) by MATRIX_1:def_5;
A56: j <= width N2 by A8, A18, A19, A14, A47, MATRIX_1:def_3, A12;
n in Seg k1 by A50, A52, FINSEQ_1:1;
then A57: n in dom N2 by A9, FINSEQ_1:def_3;
n in Seg (len ((Col (N,j)) | k1)) by A50, A51, FINSEQ_1:1;
then n in dom ((Col (N,j)) | k1) by FINSEQ_1:def_3;
then A58: n in dom ((Col (N,j)) | (Seg k1)) by FINSEQ_1:def_15;
n <= len N2 by A9, A48, A51, FINSEQ_1:59;
then A59: [n,j] in Indices N2 by A46, A50, A56, Th1;
((Col (N,j)) | k1) . n = ((Col (N,j)) | (Seg k1)) . n by FINSEQ_1:def_15
.= (Col (N,j)) . n by A58, FUNCT_1:47
.= N * (n,j) by A54, MATRIX_1:def_8
.= N2 * (n,j) by A59, A55, A53, MATRIX_1:def_5
.= (Col (N2,j)) . n by A57, MATRIX_1:def_8 ;
hence ((Col (N,j)) | k1) . n = (Col (N2,j)) . n ; ::_thesis: verum
end;
A60: (k + 1) + 1 in Seg (len N) by A8, FINSEQ_1:4;
then A61: (k + 1) + 1 in dom N by FINSEQ_1:def_3;
len (Col (N2,j)) = len N2 by MATRIX_1:def_8
.= k1 by A8, FINSEQ_1:59, NAT_1:11 ;
then A62: Col (N2,j) = (Col (N,j)) | k1 by A48, A49, FINSEQ_1:14, FINSEQ_1:59;
A63: len (Col (N,j)) = len N by MATRIX_1:def_8;
(k + 1) + 1 in Seg (len (Col (N,j))) by A60, MATRIX_1:def_8;
then A64: (k + 1) + 1 in dom (Col (N,j)) by FINSEQ_1:def_3;
A65: j in Seg (width N) by A46, A47, FINSEQ_1:1;
then ((ColSum N2) . j) + (N * (((k + 1) + 1),j)) = (Sum (Col (N2,j))) + (N * (((k + 1) + 1),j)) by A20, Def10
.= (Sum (Col (N2,j))) + ((Col (N,j)) . ((k + 1) + 1)) by A61, MATRIX_1:def_8
.= (Sum (Col (N2,j))) + ((Col (N,j)) /. ((k + 1) + 1)) by A64, PARTFUN1:def_6
.= Sum (Col (N,j)) by A8, A63, A62, Th48
.= (ColSum N) . j by A65, Def10 ;
hence ((ColSum N2) . j) + (N * (((k + 1) + 1),j)) = (ColSum N) . j ; ::_thesis: verum
end;
A66: for j being Nat st 1 <= j & j <= len (ColSum N) holds
((ColSum N2) + (Line (N,((k + 1) + 1)))) . j = (ColSum N) . j
proof
let j be Nat; ::_thesis: ( 1 <= j & j <= len (ColSum N) implies ((ColSum N2) + (Line (N,((k + 1) + 1)))) . j = (ColSum N) . j )
assume that
A67: 1 <= j and
A68: j <= len (ColSum N) ; ::_thesis: ((ColSum N2) + (Line (N,((k + 1) + 1)))) . j = (ColSum N) . j
j in Seg (len (ColSum N)) by A67, A68, FINSEQ_1:1;
then A69: j in Seg (width N2) by A20, Def10;
then A70: j <= width N by A20, FINSEQ_1:1;
j in Seg (len ((ColSum N2) + (Line (N,((k + 1) + 1))))) by A40, A67, A68, FINSEQ_1:1;
then j in dom ((ColSum N2) + (Line (N,((k + 1) + 1)))) by FINSEQ_1:def_3;
then ((ColSum N2) + (Line (N,((k + 1) + 1)))) . j = ((ColSum N2) . j) + ((Line (N,((k + 1) + 1))) . j) by COMPLSP2:1
.= ((ColSum N2) . j) + (N * (((k + 1) + 1),j)) by A20, A69, MATRIX_1:def_7
.= (ColSum N) . j by A45, A67, A70 ;
hence ((ColSum N2) + (Line (N,((k + 1) + 1)))) . j = (ColSum N) . j ; ::_thesis: verum
end;
len (LineSum N) = len N by Def9;
then Sum (LineSum N) = (Sum (LineSum N2)) + ((LineSum N) /. ((k + 1) + 1)) by A8, A21, A22, Th48, FINSEQ_1:14
.= (Sum (LineSum N2)) + ((LineSum N) . ((k + 1) + 1)) by A43, PARTFUN1:def_6
.= (Sum (ColSum N2)) + ((LineSum N) . ((k + 1) + 1)) by A3, A9
.= (Sum (ColSum N2)) + (Sum (Line (N,((k + 1) + 1)))) by A42, Def9
.= Sum ((ColSum N2) + (Line (N,((k + 1) + 1)))) by A41, Th36
.= Sum (ColSum N) by A40, A66, FINSEQ_1:14 ;
hence Sum (LineSum N) = Sum (ColSum N) ; ::_thesis: verum
end;
hence S1[k + 1] ; ::_thesis: verum
end;
for N being Matrix of COMPLEX st 0 + 1 = len N holds
Sum (LineSum N) = Sum (ColSum N)
proof
let N be Matrix of COMPLEX; ::_thesis: ( 0 + 1 = len N implies Sum (LineSum N) = Sum (ColSum N) )
A71: len (Line (N,1)) = width N by MATRIX_1:def_7;
assume A72: 0 + 1 = len N ; ::_thesis: Sum (LineSum N) = Sum (ColSum N)
then A73: 1 in Seg (len N) by FINSEQ_1:3;
A74: 1 in Seg 1 by FINSEQ_1:3;
A75: for j being Nat st 1 <= j & j <= width N holds
(ColSum N) . j = (Line (N,1)) . j
proof
A76: 1 in dom N by A72, A74, FINSEQ_1:def_3;
let j be Nat; ::_thesis: ( 1 <= j & j <= width N implies (ColSum N) . j = (Line (N,1)) . j )
assume that
A77: 1 <= j and
A78: j <= width N ; ::_thesis: (ColSum N) . j = (Line (N,1)) . j
A79: len (Col (N,j)) = 1 by A72, MATRIX_1:def_8;
A80: j in Seg (width N) by A77, A78, FINSEQ_1:1;
then (ColSum N) . j = Sum (Col (N,j)) by Def10
.= (Col (N,j)) . 1 by A79, Th47
.= N * (1,j) by A76, MATRIX_1:def_8
.= (Line (N,1)) . j by A80, MATRIX_1:def_7 ;
hence (ColSum N) . j = (Line (N,1)) . j ; ::_thesis: verum
end;
A81: len (LineSum N) = 1 by A72, Def9;
len (ColSum N) = width N by Def10;
then Sum (ColSum N) = Sum (Line (N,1)) by A71, A75, FINSEQ_1:14
.= (LineSum N) . 1 by A73, Def9
.= Sum (LineSum N) by A81, Th47 ;
hence Sum (LineSum N) = Sum (ColSum N) ; ::_thesis: verum
end;
then A82: S1[ 0 ] ;
for i being Nat holds S1[i] from NAT_1:sch_2(A82, A2);
then ( ((len M) -' 1) + 1 = len M implies Sum (LineSum M) = Sum (ColSum M) ) ;
hence Sum (LineSum M) = Sum (ColSum M) by A1; ::_thesis: verum
end;
definition
let M be Matrix of COMPLEX;
func SumAll M -> Element of COMPLEX equals :: MATRIXC1:def 11
Sum (LineSum M);
coherence
Sum (LineSum M) is Element of COMPLEX ;
end;
:: deftheorem defines SumAll MATRIXC1:def_11_:_
for M being Matrix of COMPLEX holds SumAll M = Sum (LineSum M);
theorem Th50: :: MATRIXC1:50
for M being Matrix of COMPLEX holds ColSum M = LineSum (M @)
proof
let M be Matrix of COMPLEX; ::_thesis: ColSum M = LineSum (M @)
A1: len (ColSum M) = width M by Def10;
A2: len (LineSum (M @)) = len (M @) by Def9;
A3: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_(ColSum_M)_holds_
(ColSum_M)_._i_=_(LineSum_(M_@))_._i
let i be Nat; ::_thesis: ( 1 <= i & i <= len (ColSum M) implies (ColSum M) . i = (LineSum (M @)) . i )
assume that
A4: 1 <= i and
A5: i <= len (ColSum M) ; ::_thesis: (ColSum M) . i = (LineSum (M @)) . i
i <= len (LineSum (M @)) by A2, A1, A5, MATRIX_1:def_6;
then i in Seg (len (LineSum (M @))) by A4, FINSEQ_1:1;
then A6: i in Seg (len (M @)) by Def9;
A7: i in Seg (width M) by A1, A4, A5, FINSEQ_1:1;
hence (ColSum M) . i = Sum (Col (M,i)) by Def10
.= Sum (Line ((M @),i)) by A7, MATRIX_2:15
.= (LineSum (M @)) . i by A6, Def9 ;
::_thesis: verum
end;
len (ColSum M) = len (LineSum (M @)) by A2, A1, MATRIX_1:def_6;
hence ColSum M = LineSum (M @) by A3, FINSEQ_1:14; ::_thesis: verum
end;
theorem Th51: :: MATRIXC1:51
for M being Matrix of COMPLEX st len M > 0 holds
SumAll M = SumAll (M @)
proof
let M be Matrix of COMPLEX; ::_thesis: ( len M > 0 implies SumAll M = SumAll (M @) )
assume len M > 0 ; ::_thesis: SumAll M = SumAll (M @)
then SumAll M = Sum (ColSum M) by Th49
.= SumAll (M @) by Th50 ;
hence SumAll M = SumAll (M @) ; ::_thesis: verum
end;
definition
let x, y be FinSequence of COMPLEX ;
let M be Matrix of COMPLEX;
assume that
A1: len x = len M and
A2: len y = width M ;
func QuadraticForm (x,M,y) -> Matrix of COMPLEX means :Def12: :: MATRIXC1:def 12
( len it = len x & width it = len y & ( for i, j being Nat st [i,j] in Indices M holds
it * (i,j) = ((x . i) * (M * (i,j))) * ((y . j) *') ) );
existence
ex b1 being Matrix of COMPLEX st
( len b1 = len x & width b1 = len y & ( for i, j being Nat st [i,j] in Indices M holds
b1 * (i,j) = ((x . i) * (M * (i,j))) * ((y . j) *') ) )
proof
deffunc H1( Nat, Nat) -> Element of COMPLEX = ((x . $1) * (M * ($1,$2))) * ((y . $2) *');
consider M1 being Matrix of len M, width M, COMPLEX such that
A3: for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = H1(i,j) from MATRIX_1:sch_1();
take M1 ; ::_thesis: ( len M1 = len x & width M1 = len y & ( for i, j being Nat st [i,j] in Indices M holds
M1 * (i,j) = ((x . i) * (M * (i,j))) * ((y . j) *') ) )
A4: len M1 = len x by A1, MATRIX_1:def_2;
A5: now__::_thesis:_(_(_len_M_=_0_&_width_M1_=_len_y_)_or_(_len_M_>_0_&_width_M1_=_len_y_)_)
percases ( len M = 0 or len M > 0 ) ;
caseA6: len M = 0 ; ::_thesis: width M1 = len y
then width M1 = 0 by A1, A4, MATRIX_1:def_3;
hence width M1 = len y by A2, A6, MATRIX_1:def_3; ::_thesis: verum
end;
case len M > 0 ; ::_thesis: width M1 = len y
hence width M1 = len y by A2, MATRIX_1:23; ::_thesis: verum
end;
end;
end;
dom M = dom M1 by A1, A4, FINSEQ_3:29;
hence ( len M1 = len x & width M1 = len y & ( for i, j being Nat st [i,j] in Indices M holds
M1 * (i,j) = ((x . i) * (M * (i,j))) * ((y . j) *') ) ) by A1, A2, A3, A5, MATRIX_1:def_2; ::_thesis: verum
end;
uniqueness
for b1, b2 being Matrix of COMPLEX st len b1 = len x & width b1 = len y & ( for i, j being Nat st [i,j] in Indices M holds
b1 * (i,j) = ((x . i) * (M * (i,j))) * ((y . j) *') ) & len b2 = len x & width b2 = len y & ( for i, j being Nat st [i,j] in Indices M holds
b2 * (i,j) = ((x . i) * (M * (i,j))) * ((y . j) *') ) holds
b1 = b2
proof
let M1, M2 be Matrix of COMPLEX; ::_thesis: ( len M1 = len x & width M1 = len y & ( for i, j being Nat st [i,j] in Indices M holds
M1 * (i,j) = ((x . i) * (M * (i,j))) * ((y . j) *') ) & len M2 = len x & width M2 = len y & ( for i, j being Nat st [i,j] in Indices M holds
M2 * (i,j) = ((x . i) * (M * (i,j))) * ((y . j) *') ) implies M1 = M2 )
assume that
A7: len M1 = len x and
A8: width M1 = len y and
A9: for i, j being Nat st [i,j] in Indices M holds
M1 * (i,j) = ((x . i) * (M * (i,j))) * ((y . j) *') and
A10: len M2 = len x and
A11: width M2 = len y and
A12: for i, j being Nat st [i,j] in Indices M holds
M2 * (i,j) = ((x . i) * (M * (i,j))) * ((y . j) *') ; ::_thesis: M1 = M2
now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_M1_holds_
M1_*_(i,j)_=_M2_*_(i,j)
let i, j be Nat; ::_thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) )
assume A13: [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) = M2 * (i,j)
A14: dom M1 = dom M by A1, A7, FINSEQ_3:29;
hence M1 * (i,j) = ((x . i) * (M * (i,j))) * ((y . j) *') by A2, A8, A9, A13
.= M2 * (i,j) by A2, A8, A12, A13, A14 ;
::_thesis: verum
end;
hence M1 = M2 by A7, A8, A10, A11, MATRIX_1:21; ::_thesis: verum
end;
end;
:: deftheorem Def12 defines QuadraticForm MATRIXC1:def_12_:_
for x, y being FinSequence of COMPLEX
for M being Matrix of COMPLEX st len x = len M & len y = width M holds
for b4 being Matrix of COMPLEX holds
( b4 = QuadraticForm (x,M,y) iff ( len b4 = len x & width b4 = len y & ( for i, j being Nat st [i,j] in Indices M holds
b4 * (i,j) = ((x . i) * (M * (i,j))) * ((y . j) *') ) ) );
theorem Th52: :: MATRIXC1:52
for x, y being FinSequence of COMPLEX
for M being Matrix of COMPLEX st len x = len M & len y = width M & len y > 0 holds
(QuadraticForm (x,M,y)) @ = (QuadraticForm (y,(M @"),x)) *'
proof
let x, y be FinSequence of COMPLEX ; ::_thesis: for M being Matrix of COMPLEX st len x = len M & len y = width M & len y > 0 holds
(QuadraticForm (x,M,y)) @ = (QuadraticForm (y,(M @"),x)) *'
let M be Matrix of COMPLEX; ::_thesis: ( len x = len M & len y = width M & len y > 0 implies (QuadraticForm (x,M,y)) @ = (QuadraticForm (y,(M @"),x)) *' )
assume that
A1: len x = len M and
A2: len y = width M and
A3: len y > 0 ; ::_thesis: (QuadraticForm (x,M,y)) @ = (QuadraticForm (y,(M @"),x)) *'
A4: width (M @") = width (M @) by Def1
.= len x by A1, A2, A3, MATRIX_2:10 ;
A5: width (QuadraticForm (x,M,y)) = len y by A1, A2, Def12;
then A6: width ((QuadraticForm (x,M,y)) @) = len (QuadraticForm (x,M,y)) by A3, MATRIX_2:10;
len (M @") = len (M @) by Def1;
then A7: len (M @") = width M by MATRIX_1:def_6;
A8: len (x *') = len x by COMPLSP2:def_1;
A9: len ((QuadraticForm (x,M,y)) @) = width (QuadraticForm (x,M,y)) by MATRIX_1:def_6;
A10: len (M @") = len (M @) by Def1
.= len y by A2, MATRIX_1:def_6 ;
then A11: width (QuadraticForm (y,(M @"),x)) = len x by A4, Def12;
A12: len ((QuadraticForm (y,(M @"),x)) *') = len (QuadraticForm (y,(M @"),x)) by Def1
.= len y by A10, A4, Def12 ;
A13: len ((QuadraticForm (x,M,y)) @) = width (QuadraticForm (x,M,y)) by MATRIX_1:def_6
.= len y by A1, A2, Def12 ;
A14: len (QuadraticForm (y,(M @"),x)) = len y by A10, A4, Def12;
A15: for i, j being Nat st [i,j] in Indices ((QuadraticForm (x,M,y)) @) holds
((QuadraticForm (y,(M @"),x)) *') * (i,j) = ((QuadraticForm (x,M,y)) @) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices ((QuadraticForm (x,M,y)) @) implies ((QuadraticForm (y,(M @"),x)) *') * (i,j) = ((QuadraticForm (x,M,y)) @) * (i,j) )
reconsider i9 = i, j9 = j as Element of NAT by ORDINAL1:def_12;
assume A16: [i,j] in Indices ((QuadraticForm (x,M,y)) @) ; ::_thesis: ((QuadraticForm (y,(M @"),x)) *') * (i,j) = ((QuadraticForm (x,M,y)) @) * (i,j)
then A17: 1 <= j by Th1;
A18: j <= len (QuadraticForm (x,M,y)) by A6, A16, Th1;
then A19: j <= len M by A1, A2, Def12;
A20: 1 <= i by A16, Th1;
A21: i <= width (QuadraticForm (x,M,y)) by A9, A16, Th1;
then i <= width M by A1, A2, Def12;
then A22: [j,i] in Indices M by A17, A20, A19, Th1;
A23: j <= width (M @") by A1, A2, A4, A18, Def12;
A24: 1 <= i by A16, Th1;
1 <= i by A16, Th1;
then A25: [j,i] in Indices (QuadraticForm (x,M,y)) by A21, A17, A18, Th1;
i <= len (M @") by A1, A2, A7, A21, Def12;
then A26: [i,j] in Indices (M @") by A17, A24, A23, Th1;
A27: j <= len x by A1, A2, A18, Def12;
A28: j <= len x by A1, A2, A18, Def12;
A29: j <= width (QuadraticForm (y,(M @"),x)) by A1, A2, A11, A18, Def12;
A30: 1 <= i by A16, Th1;
i <= len (QuadraticForm (y,(M @"),x)) by A1, A2, A14, A21, Def12;
then [i,j] in Indices (QuadraticForm (y,(M @"),x)) by A17, A30, A29, Th1;
then ((QuadraticForm (y,(M @"),x)) *') * (i,j) = ((QuadraticForm (y,(M @"),x)) * (i,j)) *' by Def1
.= (((y . i) * ((M @") * (i,j))) * ((x . j) *')) *' by A10, A4, A26, Def12
.= (((y . i) * ((M @") * (i9,j9))) * ((x *') . j)) *' by A17, A27, COMPLSP2:def_1
.= (((y . i) * ((M @") * (i,j))) *') * (((x *') . j) *') by COMPLEX1:35
.= (((y . i) * ((M @") * (i9,j9))) *') * (((x *') *') . j) by A8, A17, A28, COMPLSP2:def_1
.= (((y . i) *') * (((M @") * (i,j)) *')) * (((x *') *') . j) by COMPLEX1:35
.= (((y . i) *') * (((M @") *') * (i,j))) * (((x *') *') . j) by A26, Def1
.= (((y . i) *') * (((M @") *') * (i,j))) * (x . j) by COMPLSP2:22
.= (((y . i) *') * ((M @) * (i,j))) * (x . j)
.= (((y . i) *') * (M * (j,i))) * (x . j) by A22, MATRIX_1:def_6
.= ((x . j) * (M * (j,i))) * ((y . i) *')
.= (QuadraticForm (x,M,y)) * (j,i) by A1, A2, A22, Def12
.= ((QuadraticForm (x,M,y)) @) * (i,j) by A25, MATRIX_1:def_6 ;
hence ((QuadraticForm (y,(M @"),x)) *') * (i,j) = ((QuadraticForm (x,M,y)) @) * (i,j) ; ::_thesis: verum
end;
A31: width ((QuadraticForm (y,(M @"),x)) *') = width (QuadraticForm (y,(M @"),x)) by Def1
.= len x by A10, A4, Def12 ;
width ((QuadraticForm (x,M,y)) @) = len (QuadraticForm (x,M,y)) by A3, A5, MATRIX_2:10
.= len x by A1, A2, Def12 ;
hence (QuadraticForm (x,M,y)) @ = (QuadraticForm (y,(M @"),x)) *' by A13, A12, A31, A15, MATRIX_1:21; ::_thesis: verum
end;
theorem Th53: :: MATRIXC1:53
for x, y being FinSequence of COMPLEX
for M being Matrix of COMPLEX st len x = len M & len y = width M holds
(QuadraticForm (x,M,y)) *' = QuadraticForm ((x *'),(M *'),(y *'))
proof
let x, y be FinSequence of COMPLEX ; ::_thesis: for M being Matrix of COMPLEX st len x = len M & len y = width M holds
(QuadraticForm (x,M,y)) *' = QuadraticForm ((x *'),(M *'),(y *'))
let M be Matrix of COMPLEX; ::_thesis: ( len x = len M & len y = width M implies (QuadraticForm (x,M,y)) *' = QuadraticForm ((x *'),(M *'),(y *')) )
assume that
A1: len x = len M and
A2: len y = width M ; ::_thesis: (QuadraticForm (x,M,y)) *' = QuadraticForm ((x *'),(M *'),(y *'))
A3: len (y *') = len y by COMPLSP2:def_1;
then A4: len (y *') = width (M *') by A2, Def1;
len (M *') = len M by Def1;
then A5: len (x *') = len (M *') by A1, COMPLSP2:def_1;
then A6: len (QuadraticForm ((x *'),(M *'),(y *'))) = len (x *') by A4, Def12
.= len M by A1, COMPLSP2:def_1 ;
A7: width ((QuadraticForm (x,M,y)) *') = width (QuadraticForm (x,M,y)) by Def1;
A8: len ((QuadraticForm (x,M,y)) *') = len (QuadraticForm (x,M,y)) by Def1;
A9: for i, j being Nat st [i,j] in Indices ((QuadraticForm (x,M,y)) *') holds
((QuadraticForm (x,M,y)) *') * (i,j) = (QuadraticForm ((x *'),(M *'),(y *'))) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices ((QuadraticForm (x,M,y)) *') implies ((QuadraticForm (x,M,y)) *') * (i,j) = (QuadraticForm ((x *'),(M *'),(y *'))) * (i,j) )
reconsider i9 = i, j9 = j as Element of NAT by ORDINAL1:def_12;
assume A10: [i,j] in Indices ((QuadraticForm (x,M,y)) *') ; ::_thesis: ((QuadraticForm (x,M,y)) *') * (i,j) = (QuadraticForm ((x *'),(M *'),(y *'))) * (i,j)
then A11: 1 <= i by Th1;
A12: i <= len (QuadraticForm (x,M,y)) by A8, A10, Th1;
then A13: i <= len x by A1, A2, Def12;
i <= len M by A1, A2, A12, Def12;
then A14: i <= len (M *') by Def1;
A15: j <= width (QuadraticForm (x,M,y)) by A7, A10, Th1;
then A16: j <= len y by A1, A2, Def12;
j <= width M by A1, A2, A15, Def12;
then A17: j <= width (M *') by Def1;
1 <= j by A10, Th1;
then A18: [i,j] in Indices (M *') by A11, A14, A17, Th1;
A19: j <= width M by A1, A2, A15, Def12;
A20: 1 <= i by A10, Th1;
A21: 1 <= j by A10, Th1;
i <= len M by A1, A2, A12, Def12;
then A22: [i,j] in Indices M by A21, A20, A19, Th1;
[i,j] in Indices (QuadraticForm (x,M,y)) by A11, A12, A21, A15, Th1;
then ((QuadraticForm (x,M,y)) *') * (i,j) = ((QuadraticForm (x,M,y)) * (i,j)) *' by Def1
.= (((x . i) * (M * (i,j))) * ((y . j) *')) *' by A1, A2, A22, Def12
.= (((x . i) * (M * (i9,j9))) * ((y *') . j)) *' by A21, A16, COMPLSP2:def_1
.= (((x . i) * (M * (i,j))) *') * (((y *') . j) *') by COMPLEX1:35
.= (((x . i) * (M * (i9,j9))) *') * (((y *') *') . j) by A3, A21, A16, COMPLSP2:def_1
.= (((x . i) *') * ((M * (i,j)) *')) * (((y *') *') . j) by COMPLEX1:35
.= (((x . i) *') * ((M *') * (i,j))) * (((y *') *') . j) by A22, Def1
.= (((x . i) *') * ((M *') * (i9,j9))) * (((y *') . j) *') by A3, A21, A16, COMPLSP2:def_1
.= (((x *') . i) * ((M *') * (i9,j9))) * (((y *') . j) *') by A11, A13, COMPLSP2:def_1
.= (QuadraticForm ((x *'),(M *'),(y *'))) * (i,j) by A5, A4, A18, Def12 ;
hence ((QuadraticForm (x,M,y)) *') * (i,j) = (QuadraticForm ((x *'),(M *'),(y *'))) * (i,j) ; ::_thesis: verum
end;
A23: width ((QuadraticForm (x,M,y)) *') = width (QuadraticForm (x,M,y)) by Def1
.= len y by A1, A2, Def12 ;
A24: width (QuadraticForm ((x *'),(M *'),(y *'))) = len (y *') by A5, A4, Def12
.= len y by COMPLSP2:def_1 ;
len ((QuadraticForm (x,M,y)) *') = len (QuadraticForm (x,M,y)) by Def1
.= len M by A1, A2, Def12 ;
hence (QuadraticForm (x,M,y)) *' = QuadraticForm ((x *'),(M *'),(y *')) by A6, A23, A24, A9, MATRIX_1:21; ::_thesis: verum
end;
theorem Th54: :: MATRIXC1:54
for x, y being FinSequence of COMPLEX st len x = len y & 0 < len y holds
|(x,y)| = |(y,x)| *'
proof
let x, y be FinSequence of COMPLEX ; ::_thesis: ( len x = len y & 0 < len y implies |(x,y)| = |(y,x)| *' )
assume that
A1: len x = len y and
A2: 0 < len y ; ::_thesis: |(x,y)| = |(y,x)| *'
A3: 0 + 1 <= len x by A1, A2, NAT_1:8;
len (x *') = len x by COMPLSP2:def_1;
then A4: len (mlt (y,(x *'))) = len y by A1, FINSEQ_2:72;
|(y,x)| *' = (Sum (mlt (y,(x *')))) *' by A1, Th39
.= Sum ((mlt (y,(x *'))) *') by A1, A3, A4, Th23
.= Sum (mlt (x,(y *'))) by A1, Th24
.= |(x,y)| by A1, Th39 ;
hence |(x,y)| = |(y,x)| *' ; ::_thesis: verum
end;
theorem Th55: :: MATRIXC1:55
for x, y being FinSequence of COMPLEX st len x = len y & 0 < len y holds
|(x,y)| *' = |((x *'),(y *'))|
proof
let x, y be FinSequence of COMPLEX ; ::_thesis: ( len x = len y & 0 < len y implies |(x,y)| *' = |((x *'),(y *'))| )
assume that
A1: len x = len y and
A2: 0 < len y ; ::_thesis: |(x,y)| *' = |((x *'),(y *'))|
A3: 0 + 1 <= len x by A1, A2, NAT_1:8;
A4: len (y *') = len y by COMPLSP2:def_1;
then A5: len (mlt (x,(y *'))) = len x by A1, FINSEQ_2:72;
len (x *') = len x by COMPLSP2:def_1;
then |((x *'),(y *'))| = Sum (mlt ((x *'),((y *') *'))) by A1, A4, Th39
.= Sum ((mlt (x,(y *'))) *') by A1, A4, Th27
.= (Sum (mlt (x,(y *')))) *' by A3, A5, Th23
.= |(x,y)| *' by A1, Th39 ;
hence |(x,y)| *' = |((x *'),(y *'))| ; ::_thesis: verum
end;
theorem :: MATRIXC1:56
for M being Matrix of COMPLEX st width M > 0 holds
(M @) *' = (M *') @
proof
let M be Matrix of COMPLEX; ::_thesis: ( width M > 0 implies (M @) *' = (M *') @ )
assume A1: width M > 0 ; ::_thesis: (M @) *' = (M *') @
width (M *') = width M by Def1;
then A2: width ((M *') @) = len (M *') by A1, MATRIX_2:10
.= len M by Def1 ;
A3: width ((M @) *') = width (M @) by Def1;
A4: len ((M @) *') = len (M @) by Def1
.= width M by MATRIX_1:def_6 ;
A5: width ((M @) *') = width (M @) by Def1
.= len M by A1, MATRIX_2:10 ;
A6: len ((M @) *') = len (M @) by Def1;
A7: for i, j being Nat st [i,j] in Indices ((M @) *') holds
((M @) *') * (i,j) = ((M *') @) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices ((M @) *') implies ((M @) *') * (i,j) = ((M *') @) * (i,j) )
assume A8: [i,j] in Indices ((M @) *') ; ::_thesis: ((M @) *') * (i,j) = ((M *') @) * (i,j)
then A9: 1 <= i by Th1;
A10: 1 <= j by A8, Th1;
A11: j <= width (M @) by A3, A8, Th1;
i <= len (M @) by A6, A8, Th1;
then A12: [i,j] in Indices (M @) by A9, A10, A11, Th1;
then A13: [j,i] in Indices M by MATRIX_1:def_6;
j <= width ((M @) *') by A8, Th1;
then A14: j <= len (M *') by A5, Def1;
i <= len ((M @) *') by A8, Th1;
then A15: i <= width (M *') by A4, Def1;
A16: 1 <= i by A8, Th1;
1 <= j by A8, Th1;
then A17: [j,i] in Indices (M *') by A14, A16, A15, Th1;
((M @) *') * (i,j) = ((M @) * (i,j)) *' by A12, Def1
.= (M * (j,i)) *' by A13, MATRIX_1:def_6
.= (M *') * (j,i) by A13, Def1
.= ((M *') @) * (i,j) by A17, MATRIX_1:def_6 ;
hence ((M @) *') * (i,j) = ((M *') @) * (i,j) ; ::_thesis: verum
end;
len ((M *') @) = width (M *') by MATRIX_1:def_6
.= width M by Def1 ;
hence (M @) *' = (M *') @ by A4, A5, A2, A7, MATRIX_1:21; ::_thesis: verum
end;
theorem Th57: :: MATRIXC1:57
for x, y being FinSequence of COMPLEX
for M being Matrix of COMPLEX st len x = width M & len y = len M & len x > 0 & len y > 0 holds
|(x,((M @") * y))| = SumAll (QuadraticForm (x,(M @),y))
proof
let x, y be FinSequence of COMPLEX ; ::_thesis: for M being Matrix of COMPLEX st len x = width M & len y = len M & len x > 0 & len y > 0 holds
|(x,((M @") * y))| = SumAll (QuadraticForm (x,(M @),y))
let M be Matrix of COMPLEX; ::_thesis: ( len x = width M & len y = len M & len x > 0 & len y > 0 implies |(x,((M @") * y))| = SumAll (QuadraticForm (x,(M @),y)) )
assume that
A1: len x = width M and
A2: len y = len M and
A3: len x > 0 and
A4: len y > 0 ; ::_thesis: |(x,((M @") * y))| = SumAll (QuadraticForm (x,(M @),y))
A5: width (M @) = len y by A1, A2, A3, MATRIX_2:10;
then A6: width ((M @) *') = len y by Def1;
A7: dom (LineSum (QuadraticForm (x,(M @),y))) = Seg (len (LineSum (QuadraticForm (x,(M @),y)))) by FINSEQ_1:def_3
.= Seg (len (QuadraticForm (x,(M @),y))) by Def9 ;
A8: len (M @) = len x by A1, MATRIX_1:def_6;
A9: len (LineSum (QuadraticForm (x,(M @),y))) = len (QuadraticForm (x,(M @),y)) by Def9
.= len x by A8, A5, Def12 ;
A10: len (M @") = len (M @) by Def1
.= len x by A1, MATRIX_1:def_6 ;
then A11: len ((M @") * y) = len x by Def6;
then len (((M @") * y) *') = len x by COMPLSP2:def_1;
then A12: len (LineSum (QuadraticForm (x,(M @),y))) = len (mlt (x,(((M @") * y) *'))) by A9, FINSEQ_2:72;
A13: 0 + 1 <= len y by A4, NAT_1:13;
for i being Nat st 1 <= i & i <= len (LineSum (QuadraticForm (x,(M @),y))) holds
(LineSum (QuadraticForm (x,(M @),y))) . i = (mlt (x,(((M @") * y) *'))) . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len (LineSum (QuadraticForm (x,(M @),y))) implies (LineSum (QuadraticForm (x,(M @),y))) . i = (mlt (x,(((M @") * y) *'))) . i )
assume that
A14: 1 <= i and
A15: i <= len (LineSum (QuadraticForm (x,(M @),y))) ; ::_thesis: (LineSum (QuadraticForm (x,(M @),y))) . i = (mlt (x,(((M @") * y) *'))) . i
A16: len y = width (QuadraticForm (x,(M @),y)) by A8, A5, Def12
.= len (Line ((QuadraticForm (x,(M @),y)),i)) by MATRIX_1:def_7 ;
A17: len (Line ((M @"),i)) = len y by A6, MATRIX_1:def_7;
then A18: len (mlt ((Line ((M @"),i)),y)) >= 1 by A13, FINSEQ_2:72;
len (M @) = len (QuadraticForm (x,(M @),y)) by A8, A5, Def12;
then A19: len (M @) = len (LineSum (QuadraticForm (x,(M @),y))) by Def9;
then A20: i in Seg (len (M @")) by A8, A10, A14, A15, FINSEQ_1:1;
A21: for j being Nat st 1 <= j & j <= len (Line ((QuadraticForm (x,(M @),y)),i)) holds
((x . i) * ((mlt ((Line ((M @"),i)),y)) *')) . j = (Line ((QuadraticForm (x,(M @),y)),i)) . j
proof
A22: len (Line ((M @),i)) = width (M @) by MATRIX_1:def_7
.= len y by A1, A2, A3, MATRIX_2:10
.= len (y *') by COMPLSP2:def_1 ;
let j be Nat; ::_thesis: ( 1 <= j & j <= len (Line ((QuadraticForm (x,(M @),y)),i)) implies ((x . i) * ((mlt ((Line ((M @"),i)),y)) *')) . j = (Line ((QuadraticForm (x,(M @),y)),i)) . j )
assume that
A23: 1 <= j and
A24: j <= len (Line ((QuadraticForm (x,(M @),y)),i)) ; ::_thesis: ((x . i) * ((mlt ((Line ((M @"),i)),y)) *')) . j = (Line ((QuadraticForm (x,(M @),y)),i)) . j
A25: j in Seg (width (M @)) by A5, A16, A23, A24, FINSEQ_1:1;
j in Seg (len y) by A16, A23, A24, FINSEQ_1:1;
then j in Seg (len (y *')) by COMPLSP2:def_1;
then j in Seg (len (mlt ((Line ((M @),i)),(y *')))) by A22, FINSEQ_2:72;
then A26: j in dom (mlt ((Line ((M @),i)),(y *'))) by FINSEQ_1:def_3;
j in Seg (len (Line ((QuadraticForm (x,(M @),y)),i))) by A23, A24, FINSEQ_1:1;
then A27: j in Seg (width (QuadraticForm (x,(M @),y))) by MATRIX_1:def_7;
j <= width (M @) by A1, A2, A3, A16, A24, MATRIX_2:10;
then A28: [i,j] in Indices (M @) by A14, A15, A19, A23, Th1;
((x . i) * ((mlt ((Line ((M @"),i)),y)) *')) . j = (x . i) * (((mlt ((Line ((M @"),i)),y)) *') . j) by COMPLSP2:16
.= (x . i) * ((mlt (((Line ((M @"),i)) *'),(y *'))) . j) by A17, Th27
.= (x . i) * ((mlt ((Line ((M @),i)),(y *'))) . j) by A8, A10, A20, Th41
.= (x . i) * (((Line ((M @),i)) . j) * ((y *') . j)) by A26, Th18
.= (x . i) * (((Line ((M @),i)) . j) * ((y . j) *')) by A16, A23, A24, COMPLSP2:def_1
.= ((x . i) * ((Line ((M @),i)) . j)) * ((y . j) *')
.= ((x . i) * ((M @) * (i,j))) * ((y . j) *') by A25, MATRIX_1:def_7
.= (QuadraticForm (x,(M @),y)) * (i,j) by A8, A5, A28, Def12 ;
hence ((x . i) * ((mlt ((Line ((M @"),i)),y)) *')) . j = (Line ((QuadraticForm (x,(M @),y)),i)) . j by A27, MATRIX_1:def_7; ::_thesis: verum
end;
i in Seg (len (LineSum (QuadraticForm (x,(M @),y)))) by A14, A15, FINSEQ_1:1;
then A29: i in dom (LineSum (QuadraticForm (x,(M @),y))) by FINSEQ_1:def_3;
A30: len (Line ((M @"),i)) = len y by A6, MATRIX_1:def_7;
A31: len ((x . i) * ((mlt ((Line ((M @"),i)),y)) *')) = len ((mlt ((Line ((M @"),i)),y)) *') by COMPLSP2:3
.= len (mlt ((Line ((M @"),i)),y)) by COMPLSP2:def_1
.= len (Line ((QuadraticForm (x,(M @),y)),i)) by A16, A30, FINSEQ_2:72 ;
i in Seg (len (mlt (x,(((M @") * y) *')))) by A12, A14, A15, FINSEQ_1:1;
then i in dom (mlt (x,(((M @") * y) *'))) by FINSEQ_1:def_3;
then (mlt (x,(((M @") * y) *'))) . i = (x . i) * ((((M @") * y) *') . i) by Th18
.= (x . i) * ((((M @") * y) . i) *') by A11, A9, A14, A15, COMPLSP2:def_1 ;
then (mlt (x,(((M @") * y) *'))) . i = (x . i) * ((Sum (mlt ((Line ((M @"),i)),y))) *') by A20, Def6
.= (x . i) * (Sum ((mlt ((Line ((M @"),i)),y)) *')) by A18, Th23
.= Sum ((x . i) * ((mlt ((Line ((M @"),i)),y)) *')) by Th28 ;
then (mlt (x,(((M @") * y) *'))) . i = Sum (Line ((QuadraticForm (x,(M @),y)),i)) by A31, A21, FINSEQ_1:14;
hence (LineSum (QuadraticForm (x,(M @),y))) . i = (mlt (x,(((M @") * y) *'))) . i by A7, A29, Def9; ::_thesis: verum
end;
then Sum (LineSum (QuadraticForm (x,(M @),y))) = Sum (mlt (x,(((M @") * y) *'))) by A12, FINSEQ_1:14;
hence |(x,((M @") * y))| = SumAll (QuadraticForm (x,(M @),y)) by A11, Th39; ::_thesis: verum
end;
theorem Th58: :: MATRIXC1:58
for x, y being FinSequence of COMPLEX
for M being Matrix of COMPLEX st len y = len M & len x = width M & len x > 0 & len y > 0 holds
|((M * x),y)| = SumAll (QuadraticForm (x,(M @),y))
proof
let x, y be FinSequence of COMPLEX ; ::_thesis: for M being Matrix of COMPLEX st len y = len M & len x = width M & len x > 0 & len y > 0 holds
|((M * x),y)| = SumAll (QuadraticForm (x,(M @),y))
let M be Matrix of COMPLEX; ::_thesis: ( len y = len M & len x = width M & len x > 0 & len y > 0 implies |((M * x),y)| = SumAll (QuadraticForm (x,(M @),y)) )
assume that
A1: len y = len M and
A2: len x = width M and
A3: len x > 0 and
A4: len y > 0 ; ::_thesis: |((M * x),y)| = SumAll (QuadraticForm (x,(M @),y))
A5: (M @) @" = M *' by A1, A2, A3, A4, MATRIX_2:13;
A6: width (M @) = len M by A2, A3, MATRIX_2:10;
A7: len (x *') = width M by A2, COMPLSP2:def_1;
len (y *') = len M by A1, COMPLSP2:def_1;
then A8: len (QuadraticForm ((y *'),M,(x *'))) = len M by A7, Def12;
A9: len (x *') = len x by COMPLSP2:def_1;
A10: 0 + 1 <= len x by A3, NAT_1:13;
A11: len (y *') = len y by COMPLSP2:def_1;
A12: len (M @) = width M by MATRIX_1:def_6;
A13: len (M * x) = len M by Def6;
hence |((M * x),y)| = |(y,(M * x))| *' by A1, A4, Th54
.= |((y *'),((M * x) *'))| by A1, A4, A13, Th55
.= |((y *'),((M *') * (x *')))| by A2, A10, Th43
.= SumAll (QuadraticForm ((y *'),((M @) @),(x *'))) by A1, A2, A3, A4, A9, A11, A12, A6, A5, Th57
.= SumAll (QuadraticForm ((y *'),M,(x *'))) by A1, A2, A3, A4, MATRIX_2:13
.= SumAll ((QuadraticForm ((y *'),M,(x *'))) @) by A1, A4, A8, Th51
.= SumAll ((QuadraticForm ((x *'),(M @"),(y *'))) *') by A1, A2, A3, A9, A11, Th52
.= SumAll (((QuadraticForm (x,(M @),y)) *') *') by A1, A2, A12, A6, Th53
.= SumAll (QuadraticForm (x,(M @),y)) ;
::_thesis: verum
end;
theorem Th59: :: MATRIXC1:59
for x, y being FinSequence of COMPLEX
for M being Matrix of COMPLEX st len x = width M & len y = len M & width M > 0 & len M > 0 holds
|((M * x),y)| = |(x,((M @") * y))|
proof
let x, y be FinSequence of COMPLEX ; ::_thesis: for M being Matrix of COMPLEX st len x = width M & len y = len M & width M > 0 & len M > 0 holds
|((M * x),y)| = |(x,((M @") * y))|
let M be Matrix of COMPLEX; ::_thesis: ( len x = width M & len y = len M & width M > 0 & len M > 0 implies |((M * x),y)| = |(x,((M @") * y))| )
assume that
A1: len x = width M and
A2: len y = len M and
A3: width M > 0 and
A4: len M > 0 ; ::_thesis: |((M * x),y)| = |(x,((M @") * y))|
|(x,((M @") * y))| = SumAll (QuadraticForm (x,(M @),y)) by A1, A2, A3, A4, Th57;
hence |((M * x),y)| = |(x,((M @") * y))| by A1, A2, A3, A4, Th58; ::_thesis: verum
end;
theorem :: MATRIXC1:60
for x, y being FinSequence of COMPLEX
for M being Matrix of COMPLEX st len x = len M & len y = width M & width M > 0 & len M > 0 holds
|(x,(M * y))| = |(((M @") * x),y)|
proof
let x, y be FinSequence of COMPLEX ; ::_thesis: for M being Matrix of COMPLEX st len x = len M & len y = width M & width M > 0 & len M > 0 holds
|(x,(M * y))| = |(((M @") * x),y)|
let M be Matrix of COMPLEX; ::_thesis: ( len x = len M & len y = width M & width M > 0 & len M > 0 implies |(x,(M * y))| = |(((M @") * x),y)| )
assume that
A1: len x = len M and
A2: len y = width M and
A3: width M > 0 and
A4: len M > 0 ; ::_thesis: |(x,(M * y))| = |(((M @") * x),y)|
A5: len ((M @") * x) = len (M @") by Def6
.= len (M @) by Def1
.= width M by MATRIX_1:def_6 ;
len (M * y) = len x by A1, Def6;
hence |(x,(M * y))| = |((M * y),x)| *' by A1, A4, Th54
.= |(y,((M @") * x))| *' by A1, A2, A3, A4, Th59
.= |(((M @") * x),y)| by A2, A3, A5, Th54 ;
::_thesis: verum
end;
*