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