:: MATRIX10 semantic presentation begin definition let M be Matrix of REAL; attrM is Positive means :Def1: :: MATRIX10:def 1 for i, j being Nat st [i,j] in Indices M holds M * (i,j) > 0 ; attrM is Negative means :Def2: :: MATRIX10:def 2 for i, j being Nat st [i,j] in Indices M holds M * (i,j) < 0 ; attrM is Nonpositive means :Def3: :: MATRIX10:def 3 for i, j being Nat st [i,j] in Indices M holds M * (i,j) <= 0 ; attrM is Nonnegative means :Def4: :: MATRIX10:def 4 for i, j being Nat st [i,j] in Indices M holds M * (i,j) >= 0 ; end; :: deftheorem Def1 defines Positive MATRIX10:def_1_:_ for M being Matrix of REAL holds ( M is Positive iff for i, j being Nat st [i,j] in Indices M holds M * (i,j) > 0 ); :: deftheorem Def2 defines Negative MATRIX10:def_2_:_ for M being Matrix of REAL holds ( M is Negative iff for i, j being Nat st [i,j] in Indices M holds M * (i,j) < 0 ); :: deftheorem Def3 defines Nonpositive MATRIX10:def_3_:_ for M being Matrix of REAL holds ( M is Nonpositive iff for i, j being Nat st [i,j] in Indices M holds M * (i,j) <= 0 ); :: deftheorem Def4 defines Nonnegative MATRIX10:def_4_:_ for M being Matrix of REAL holds ( M is Nonnegative iff for i, j being Nat st [i,j] in Indices M holds M * (i,j) >= 0 ); definition let M1, M2 be Matrix of REAL; predM1 is_less_than M2 means :Def5: :: MATRIX10:def 5 for i, j being Nat st [i,j] in Indices M1 holds M1 * (i,j) < M2 * (i,j); predM1 is_less_or_equal_with M2 means :Def6: :: MATRIX10:def 6 for i, j being Nat st [i,j] in Indices M1 holds M1 * (i,j) <= M2 * (i,j); end; :: deftheorem Def5 defines is_less_than MATRIX10:def_5_:_ for M1, M2 being Matrix of REAL holds ( M1 is_less_than M2 iff for i, j being Nat st [i,j] in Indices M1 holds M1 * (i,j) < M2 * (i,j) ); :: deftheorem Def6 defines is_less_or_equal_with MATRIX10:def_6_:_ for M1, M2 being Matrix of REAL holds ( M1 is_less_or_equal_with M2 iff for i, j being Nat st [i,j] in Indices M1 holds M1 * (i,j) <= M2 * (i,j) ); definition let M be Matrix of REAL; func|:M:| -> Matrix of REAL means :Def7: :: MATRIX10:def 7 ( len it = len M & width it = width M & ( for i, j being Nat st [i,j] in Indices M holds it * (i,j) = abs (M * (i,j)) ) ); existence ex b1 being Matrix of REAL st ( len b1 = len M & width b1 = width M & ( for i, j being Nat st [i,j] in Indices M holds b1 * (i,j) = abs (M * (i,j)) ) ) proof deffunc H1( Nat, Nat) -> Element of REAL = abs (M * (\$1,\$2)); consider M1 being Matrix of len M, width M, REAL 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) = abs (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) = abs (M * (i,j)) ) ) by A1, A3, MATRIX_1:def_2; ::_thesis: verum end; uniqueness for b1, b2 being Matrix of REAL st len b1 = len M & width b1 = width M & ( for i, j being Nat st [i,j] in Indices M holds b1 * (i,j) = abs (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) = abs (M * (i,j)) ) holds b1 = b2 proof let M1, M2 be Matrix of REAL; ::_thesis: ( len M1 = len M & width M1 = width M & ( for i, j being Nat st [i,j] in Indices M holds M1 * (i,j) = abs (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) = abs (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) = abs (M * (i,j)) and A8: ( len M2 = len M & width M2 = width M ) and A9: for i, j being Nat st [i,j] in Indices M holds M2 * (i,j) = abs (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 A10: [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) = M2 * (i,j) A11: dom M1 = dom M by A5, FINSEQ_3:29; hence M1 * (i,j) = abs (M * (i,j)) by A6, A7, A10 .= M2 * (i,j) by A6, A9, A10, A11 ; ::_thesis: verum end; hence M1 = M2 by A5, A6, A8, MATRIX_1:21; ::_thesis: verum end; end; :: deftheorem Def7 defines |: MATRIX10:def_7_:_ for M, b2 being Matrix of REAL 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) = abs (M * (i,j)) ) ) ); definition let n be Nat; let M be Matrix of n, REAL ; :: original: - redefine func - M -> Matrix of n, REAL ; coherence - M is Matrix of n, REAL proof len M = n by MATRIX_1:24; then A1: len (- M) = n by MATRIX_3:def_2; width M = n by MATRIX_1:24; then width (- M) = n by MATRIX_3:def_2; hence - M is Matrix of n, REAL by A1, MATRIX_2:7; ::_thesis: verum end; end; definition let n be Nat; let M1, M2 be Matrix of n, REAL ; :: original: + redefine funcM1 + M2 -> Matrix of n, REAL ; coherence M1 + M2 is Matrix of n, REAL proof A1: width M2 = n by MATRIX_1:24; width M1 = n by MATRIX_1:24; then ( len (M1 + M2) = len M1 & width (M1 + M2) = width M2 ) by A1, MATRIX_3:def_3; hence M1 + M2 is Matrix of n, REAL by A1, MATRIX_1:24, MATRIX_2:7; ::_thesis: verum end; end; definition let n be Nat; let M1, M2 be Matrix of n, REAL ; :: original: - redefine funcM1 - M2 -> Matrix of n, REAL ; coherence M1 - M2 is Matrix of n, REAL proof len (M1 + (- M2)) = len M1 by MATRIX_3:def_3; hence M1 - M2 is Matrix of n, REAL by MATRIX_4:def_1; ::_thesis: verum end; end; definition let n be Nat; let a be Element of REAL ; let M be Matrix of n, REAL ; :: original: * redefine funca * M -> Matrix of n, REAL ; coherence a * M is Matrix of n, REAL proof A1: width (a * M) = width M by MATRIXR1:27; ( width M = n & len (a * M) = len M ) by MATRIXR1:27, MATRIX_1:24; hence a * M is Matrix of n, REAL by A1, MATRIX_1:24, MATRIX_2:7; ::_thesis: verum end; end; registration cluster(1,1) --> 1 -> Positive for Matrix of REAL; coherence for b1 being Matrix of REAL st b1 = (1,1) --> 1 holds b1 is Positive proof for i, j being Nat st [i,j] in Indices ((1,1) --> 1) holds ((1,1) --> 1) * (i,j) > 0 by MATRIX_2:1; hence for b1 being Matrix of REAL st b1 = (1,1) --> 1 holds b1 is Positive by Def1; ::_thesis: verum end; cluster(1,1) --> 1 -> Nonnegative for Matrix of REAL; coherence for b1 being Matrix of REAL st b1 = (1,1) --> 1 holds b1 is Nonnegative proof for i, j being Nat st [i,j] in Indices ((1,1) --> 1) holds ((1,1) --> 1) * (i,j) >= 0 by MATRIX_2:1; hence for b1 being Matrix of REAL st b1 = (1,1) --> 1 holds b1 is Nonnegative by Def4; ::_thesis: verum end; cluster(1,1) --> (- 1) -> Negative for Matrix of REAL; coherence for b1 being Matrix of REAL st b1 = (1,1) --> (- 1) holds b1 is Negative proof for i, j being Nat st [i,j] in Indices ((1,1) --> (- 1)) holds ((1,1) --> (- 1)) * (i,j) < 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices ((1,1) --> (- 1)) implies ((1,1) --> (- 1)) * (i,j) < 0 ) assume [i,j] in Indices ((1,1) --> (- 1)) ; ::_thesis: ((1,1) --> (- 1)) * (i,j) < 0 then ((1,1) --> (- 1)) * (i,j) = - 1 by MATRIX_2:1; hence ((1,1) --> (- 1)) * (i,j) < 0 ; ::_thesis: verum end; hence for b1 being Matrix of REAL st b1 = (1,1) --> (- 1) holds b1 is Negative by Def2; ::_thesis: verum end; cluster(1,1) --> (- 1) -> Nonpositive for Matrix of REAL; coherence for b1 being Matrix of REAL st b1 = (1,1) --> (- 1) holds b1 is Nonpositive proof for i, j being Nat st [i,j] in Indices ((1,1) --> (- 1)) holds ((1,1) --> (- 1)) * (i,j) <= 0 by MATRIX_2:1; hence for b1 being Matrix of REAL st b1 = (1,1) --> (- 1) holds b1 is Nonpositive by Def3; ::_thesis: verum end; end; registration clusterV16() V19( NAT ) V20(K291(REAL)) V21() FinSequence-like tabular Positive Nonnegative for FinSequence of K291(REAL); existence ex b1 being Matrix of REAL st ( b1 is Positive & b1 is Nonnegative ) proof take (1,1) --> 1 ; ::_thesis: ( (1,1) --> 1 is Positive & (1,1) --> 1 is Nonnegative ) thus ( (1,1) --> 1 is Positive & (1,1) --> 1 is Nonnegative ) ; ::_thesis: verum end; clusterV16() V19( NAT ) V20(K291(REAL)) V21() FinSequence-like tabular Negative Nonpositive for FinSequence of K291(REAL); existence ex b1 being Matrix of REAL st ( b1 is Negative & b1 is Nonpositive ) proof take (1,1) --> (- 1) ; ::_thesis: ( (1,1) --> (- 1) is Negative & (1,1) --> (- 1) is Nonpositive ) thus ( (1,1) --> (- 1) is Negative & (1,1) --> (- 1) is Nonpositive ) ; ::_thesis: verum end; end; registration let M be Positive Matrix of REAL; clusterM @ -> Positive ; coherence M @ is Positive proof for i, j being Nat st [i,j] in Indices (M @) holds (M @) * (i,j) > 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M @) implies (M @) * (i,j) > 0 ) assume [i,j] in Indices (M @) ; ::_thesis: (M @) * (i,j) > 0 then A1: [j,i] in Indices M by MATRIX_1:def_6; then (M @) * (i,j) = M * (j,i) by MATRIX_1:def_6; hence (M @) * (i,j) > 0 by A1, Def1; ::_thesis: verum end; hence M @ is Positive by Def1; ::_thesis: verum end; end; registration let M be Negative Matrix of REAL; clusterM @ -> Negative ; coherence M @ is Negative proof for i, j being Nat st [i,j] in Indices (M @) holds (M @) * (i,j) < 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M @) implies (M @) * (i,j) < 0 ) assume [i,j] in Indices (M @) ; ::_thesis: (M @) * (i,j) < 0 then A1: [j,i] in Indices M by MATRIX_1:def_6; then (M @) * (i,j) = M * (j,i) by MATRIX_1:def_6; hence (M @) * (i,j) < 0 by A1, Def2; ::_thesis: verum end; hence M @ is Negative by Def2; ::_thesis: verum end; end; registration let M be Nonpositive Matrix of REAL; clusterM @ -> Nonpositive ; coherence M @ is Nonpositive proof for i, j being Nat st [i,j] in Indices (M @) holds (M @) * (i,j) <= 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M @) implies (M @) * (i,j) <= 0 ) assume [i,j] in Indices (M @) ; ::_thesis: (M @) * (i,j) <= 0 then A1: [j,i] in Indices M by MATRIX_1:def_6; then (M @) * (i,j) = M * (j,i) by MATRIX_1:def_6; hence (M @) * (i,j) <= 0 by A1, Def3; ::_thesis: verum end; hence M @ is Nonpositive by Def3; ::_thesis: verum end; end; registration let M be Nonnegative Matrix of REAL; clusterM @ -> Nonnegative ; coherence M @ is Nonnegative proof for i, j being Nat st [i,j] in Indices (M @) holds (M @) * (i,j) >= 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M @) implies (M @) * (i,j) >= 0 ) assume [i,j] in Indices (M @) ; ::_thesis: (M @) * (i,j) >= 0 then A1: [j,i] in Indices M by MATRIX_1:def_6; then (M @) * (i,j) = M * (j,i) by MATRIX_1:def_6; hence (M @) * (i,j) >= 0 by A1, Def4; ::_thesis: verum end; hence M @ is Nonnegative by Def4; ::_thesis: verum end; end; registration let n be Nat; cluster(n,n) --> 1 -> Positive for Matrix of n, REAL ; coherence for b1 being Matrix of n, REAL st b1 = (n,n) --> 1 holds b1 is Positive proof for i, j being Nat st [i,j] in Indices ((n,n) --> 1) holds ((n,n) --> 1) * (i,j) > 0 by MATRIX_2:1; hence for b1 being Matrix of n, REAL st b1 = (n,n) --> 1 holds b1 is Positive by Def1; ::_thesis: verum end; cluster(n,n) --> (- 1) -> Negative for Matrix of n, REAL ; coherence for b1 being Matrix of n, REAL st b1 = (n,n) --> (- 1) holds b1 is Negative proof for i, j being Nat st [i,j] in Indices ((n,n) --> (- 1)) holds ((n,n) --> (- 1)) * (i,j) < 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices ((n,n) --> (- 1)) implies ((n,n) --> (- 1)) * (i,j) < 0 ) assume [i,j] in Indices ((n,n) --> (- 1)) ; ::_thesis: ((n,n) --> (- 1)) * (i,j) < 0 then ((n,n) --> (- 1)) * (i,j) = - 1 by MATRIX_2:1; hence ((n,n) --> (- 1)) * (i,j) < 0 ; ::_thesis: verum end; hence for b1 being Matrix of n, REAL st b1 = (n,n) --> (- 1) holds b1 is Negative by Def2; ::_thesis: verum end; cluster(n,n) --> (- 1) -> Nonpositive for Matrix of n, REAL ; coherence for b1 being Matrix of n, REAL st b1 = (n,n) --> (- 1) holds b1 is Nonpositive proof for i, j being Nat st [i,j] in Indices ((n,n) --> (- 1)) holds ((n,n) --> (- 1)) * (i,j) <= 0 by MATRIX_2:1; hence for b1 being Matrix of n, REAL st b1 = (n,n) --> (- 1) holds b1 is Nonpositive by Def3; ::_thesis: verum end; cluster(n,n) --> 1 -> Nonnegative for Matrix of n, REAL ; coherence for b1 being Matrix of n, REAL st b1 = (n,n) --> 1 holds b1 is Nonnegative proof for i, j being Nat st [i,j] in Indices ((n,n) --> 1) holds ((n,n) --> 1) * (i,j) >= 0 by MATRIX_2:1; hence for b1 being Matrix of n, REAL st b1 = (n,n) --> 1 holds b1 is Nonnegative by Def4; ::_thesis: verum end; end; registration let n be Nat; clusterV16() V19( NAT ) V20(K291(REAL)) V21() FinSequence-like tabular Positive Nonnegative for Matrix of n,n, REAL ; existence ex b1 being Matrix of n, REAL st ( b1 is Positive & b1 is Nonnegative ) proof take (n,n) --> 1 ; ::_thesis: ( (n,n) --> 1 is Positive & (n,n) --> 1 is Nonnegative ) thus ( (n,n) --> 1 is Positive & (n,n) --> 1 is Nonnegative ) ; ::_thesis: verum end; clusterV16() V19( NAT ) V20(K291(REAL)) V21() FinSequence-like tabular Negative Nonpositive for Matrix of n,n, REAL ; existence ex b1 being Matrix of n, REAL st ( b1 is Negative & b1 is Nonpositive ) proof take (n,n) --> (- 1) ; ::_thesis: ( (n,n) --> (- 1) is Negative & (n,n) --> (- 1) is Nonpositive ) thus ( (n,n) --> (- 1) is Negative & (n,n) --> (- 1) is Nonpositive ) ; ::_thesis: verum end; end; Lm1: for n being Nat for M1, M2 being Matrix of n, REAL holds ( len M1 = len M2 & width M1 = width M2 ) proof let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL holds ( len M1 = len M2 & width M1 = width M2 ) let M1, M2 be Matrix of n, REAL ; ::_thesis: ( len M1 = len M2 & width M1 = width M2 ) ( width M1 = n & len M1 = n ) by MATRIX_1:24; hence ( len M1 = len M2 & width M1 = width M2 ) by MATRIX_1:24; ::_thesis: verum end; theorem :: MATRIX10:1 for x1 being Element of F_Real for x2 being Real st x1 = x2 holds - x1 = - x2 ; theorem Th2: :: MATRIX10:2 for i, j being Nat for M being Matrix of REAL 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 REAL st [i,j] in Indices M holds (- M) * (i,j) = - (M * (i,j)) let M be Matrix of REAL; ::_thesis: ( [i,j] in Indices M implies (- M) * (i,j) = - (M * (i,j)) ) assume [i,j] in Indices M ; ::_thesis: (- M) * (i,j) = - (M * (i,j)) then (- M) * (i,j) = - ((MXR2MXF M) * (i,j)) by MATRIX_3:def_2, VECTSP_1:def_5; hence (- M) * (i,j) = - (M * (i,j)) by VECTSP_1:def_5; ::_thesis: verum end; theorem Th3: :: MATRIX10:3 for i, j being Nat for M1, M2 being Matrix of REAL 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 REAL 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 REAL; ::_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: ( 1 <= j & j <= width M2 ) by A2, A3, MATRIXC1:1; ( 1 <= i & i <= len M2 ) by A1, A3, MATRIXC1:1; then A5: [i,j] in Indices (MXR2MXF M2) by A4, MATRIXC1:1; (M1 - M2) * (i,j) = ((MXR2MXF M1) + (- (MXR2MXF M2))) * (i,j) by MATRIX_4:def_1, VECTSP_1:def_5 .= ((MXR2MXF M1) * (i,j)) + ((- (MXR2MXF M2)) * (i,j)) by A3, MATRIX_3:def_3 .= ((MXR2MXF M1) * (i,j)) + (- ((MXR2MXF M2) * (i,j))) by A5, MATRIX_3:def_2 ; hence (M1 - M2) * (i,j) = (M1 * (i,j)) - (M2 * (i,j)) by VECTSP_1:def_5; ::_thesis: verum end; theorem Th4: :: MATRIX10:4 for a being Element of REAL for i, j being Nat for M being Matrix of REAL st [i,j] in Indices M holds (a * M) * (i,j) = a * (M * (i,j)) proof let a be Element of REAL ; ::_thesis: for i, j being Nat for M being Matrix of REAL st [i,j] in Indices M holds (a * M) * (i,j) = a * (M * (i,j)) let i, j be Nat; ::_thesis: for M being Matrix of REAL st [i,j] in Indices M holds (a * M) * (i,j) = a * (M * (i,j)) let M be Matrix of REAL; ::_thesis: ( [i,j] in Indices M implies (a * M) * (i,j) = a * (M * (i,j)) ) reconsider aa = a as Element of F_Real by VECTSP_1:def_5; A1: MXR2MXF (a * M) = MXR2MXF (MXF2MXR (aa * (MXR2MXF M))) by MATRIXR1:def_7 .= aa * (MXR2MXF M) ; assume [i,j] in Indices M ; ::_thesis: (a * M) * (i,j) = a * (M * (i,j)) then (a * M) * (i,j) = aa * ((MXR2MXF M) * (i,j)) by A1, MATRIX_3:def_5, VECTSP_1:def_5; hence (a * M) * (i,j) = a * (M * (i,j)) by VECTSP_1:def_5; ::_thesis: verum end; theorem Th5: :: MATRIX10:5 for n being Nat for M being Matrix of n, REAL holds Indices M = Indices |:M:| proof let n be Nat; ::_thesis: for M being Matrix of n, REAL holds Indices M = Indices |:M:| let M be Matrix of n, REAL ; ::_thesis: Indices M = Indices |:M:| A1: Seg (len M) = dom M by FINSEQ_1:def_3; ( len |:M:| = len M & width |:M:| = width M ) by Def7; hence Indices M = Indices |:M:| by A1, FINSEQ_1:def_3; ::_thesis: verum end; theorem :: MATRIX10:6 for a being Element of REAL for n being Nat for M being Matrix of n, REAL holds |:(a * M):| = (abs a) * |:M:| proof let a be Element of REAL ; ::_thesis: for n being Nat for M being Matrix of n, REAL holds |:(a * M):| = (abs a) * |:M:| let n be Nat; ::_thesis: for M being Matrix of n, REAL holds |:(a * M):| = (abs a) * |:M:| let M be Matrix of n, REAL ; ::_thesis: |:(a * M):| = (abs a) * |:M:| A1: ( len (a * M) = len M & width (a * M) = width M ) by MATRIXR1:27; len ((abs a) * |:M:|) = len |:M:| by MATRIXR1:27; then A2: len ((abs a) * |:M:|) = len M by Def7; A3: for i, j being Nat st [i,j] in Indices |:(a * M):| holds |:(a * M):| * (i,j) = ((abs a) * |:M:|) * (i,j) proof A4: Indices (a * M) = Indices M by MATRIXR1:28; A5: Indices (a * M) = Indices M by MATRIXR1:28; let i, j be Nat; ::_thesis: ( [i,j] in Indices |:(a * M):| implies |:(a * M):| * (i,j) = ((abs a) * |:M:|) * (i,j) ) assume A6: [i,j] in Indices |:(a * M):| ; ::_thesis: |:(a * M):| * (i,j) = ((abs a) * |:M:|) * (i,j) A7: Indices |:(a * M):| = Indices (a * M) by Th5; then A8: |:(a * M):| * (i,j) = abs ((a * M) * (i,j)) by A6, Def7 .= abs (a * (M * (i,j))) by A6, A7, A4, Th4 .= (abs a) * (abs (M * (i,j))) by COMPLEX1:65 ; Indices |:M:| = Indices M by Th5; then ((abs a) * |:M:|) * (i,j) = (abs a) * (|:M:| * (i,j)) by A6, A7, A5, Th4 .= |:(a * M):| * (i,j) by A6, A7, A8, A5, Def7 ; hence |:(a * M):| * (i,j) = ((abs a) * |:M:|) * (i,j) ; ::_thesis: verum end; width ((abs a) * |:M:|) = width |:M:| by MATRIXR1:27; then A9: width ((abs a) * |:M:|) = width M by Def7; ( len |:(a * M):| = len (a * M) & width |:(a * M):| = width (a * M) ) by Def7; hence |:(a * M):| = (abs a) * |:M:| by A1, A2, A9, A3, MATRIX_1:21; ::_thesis: verum end; theorem :: MATRIX10:7 for n being Nat for M being Matrix of n, REAL st M is Negative holds - M is Positive proof let n be Nat; ::_thesis: for M being Matrix of n, REAL st M is Negative holds - M is Positive let M be Matrix of n, REAL ; ::_thesis: ( M is Negative implies - M is Positive ) A1: ( Indices M = [:(Seg n),(Seg n):] & Indices (- M) = [:(Seg n),(Seg n):] ) by MATRIX_1:24; assume A2: M is Negative ; ::_thesis: - M is Positive for i, j being Nat st [i,j] in Indices (- M) holds (- M) * (i,j) > 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (- M) implies (- M) * (i,j) > 0 ) assume A3: [i,j] in Indices (- M) ; ::_thesis: (- M) * (i,j) > 0 then M * (i,j) < 0 by A2, A1, Def2; then - (M * (i,j)) > 0 by XREAL_1:58; hence (- M) * (i,j) > 0 by A1, A3, Th2; ::_thesis: verum end; hence - M is Positive by Def1; ::_thesis: verum end; theorem :: MATRIX10:8 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is Positive & M2 is Positive holds M1 + M2 is Positive proof let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is Positive & M2 is Positive holds M1 + M2 is Positive let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Positive & M2 is Positive implies M1 + M2 is Positive ) A1: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24; A2: ( Indices M1 = [:(Seg n),(Seg n):] & Indices (M1 + M2) = [:(Seg n),(Seg n):] ) by MATRIX_1:24; assume A3: ( M1 is Positive & M2 is Positive ) ; ::_thesis: M1 + M2 is Positive for i, j being Nat st [i,j] in Indices (M1 + M2) holds (M1 + M2) * (i,j) > 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M2) implies (M1 + M2) * (i,j) > 0 ) assume A4: [i,j] in Indices (M1 + M2) ; ::_thesis: (M1 + M2) * (i,j) > 0 then ( M1 * (i,j) > 0 & M2 * (i,j) > 0 ) by A3, A1, A2, Def1; then (M1 * (i,j)) + (M2 * (i,j)) > 0 ; hence (M1 + M2) * (i,j) > 0 by A2, A4, MATRIXR1:25; ::_thesis: verum end; hence M1 + M2 is Positive by Def1; ::_thesis: verum end; theorem :: MATRIX10:9 for n being Nat for M2, M1 being Matrix of n, REAL st - M2 is_less_than M1 holds M1 + M2 is Positive proof let n be Nat; ::_thesis: for M2, M1 being Matrix of n, REAL st - M2 is_less_than M1 holds M1 + M2 is Positive let M2, M1 be Matrix of n, REAL ; ::_thesis: ( - M2 is_less_than M1 implies M1 + M2 is Positive ) A1: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; A2: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24; A3: Indices (- M2) = [:(Seg n),(Seg n):] by MATRIX_1:24; A4: Indices (M1 + M2) = [:(Seg n),(Seg n):] by MATRIX_1:24; assume A5: - M2 is_less_than M1 ; ::_thesis: M1 + M2 is Positive for i, j being Nat st [i,j] in Indices (M1 + M2) holds (M1 + M2) * (i,j) > 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M2) implies (M1 + M2) * (i,j) > 0 ) assume A6: [i,j] in Indices (M1 + M2) ; ::_thesis: (M1 + M2) * (i,j) > 0 then (- M2) * (i,j) < M1 * (i,j) by A5, A3, A4, Def5; then - (M2 * (i,j)) < M1 * (i,j) by A2, A4, A6, Th2; then (M1 * (i,j)) + (M2 * (i,j)) > 0 by XREAL_1:62; hence (M1 + M2) * (i,j) > 0 by A1, A4, A6, MATRIXR1:25; ::_thesis: verum end; hence M1 + M2 is Positive by Def1; ::_thesis: verum end; theorem :: MATRIX10:10 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is Nonnegative & M2 is Positive holds M1 + M2 is Positive proof let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is Nonnegative & M2 is Positive holds M1 + M2 is Positive let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Nonnegative & M2 is Positive implies M1 + M2 is Positive ) A1: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24; A2: ( Indices M1 = [:(Seg n),(Seg n):] & Indices (M1 + M2) = [:(Seg n),(Seg n):] ) by MATRIX_1:24; assume A3: ( M1 is Nonnegative & M2 is Positive ) ; ::_thesis: M1 + M2 is Positive for i, j being Nat st [i,j] in Indices (M1 + M2) holds (M1 + M2) * (i,j) > 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M2) implies (M1 + M2) * (i,j) > 0 ) assume A4: [i,j] in Indices (M1 + M2) ; ::_thesis: (M1 + M2) * (i,j) > 0 then ( M1 * (i,j) >= 0 & M2 * (i,j) > 0 ) by A3, A1, A2, Def1, Def4; then (M1 * (i,j)) + (M2 * (i,j)) > 0 ; hence (M1 + M2) * (i,j) > 0 by A2, A4, MATRIXR1:25; ::_thesis: verum end; hence M1 + M2 is Positive by Def1; ::_thesis: verum end; theorem :: MATRIX10:11 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is Positive & M2 is Negative & |:M2:| is_less_than |:M1:| holds M1 + M2 is Positive proof let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is Positive & M2 is Negative & |:M2:| is_less_than |:M1:| holds M1 + M2 is Positive let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Positive & M2 is Negative & |:M2:| is_less_than |:M1:| implies M1 + M2 is Positive ) assume that A1: M1 is Positive and A2: M2 is Negative and A3: |:M2:| is_less_than |:M1:| ; ::_thesis: M1 + M2 is Positive A4: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24; A5: Indices (M1 + M2) = [:(Seg n),(Seg n):] by MATRIX_1:24; A6: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; for i, j being Nat st [i,j] in Indices (M1 + M2) holds (M1 + M2) * (i,j) > 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M2) implies (M1 + M2) * (i,j) > 0 ) assume A7: [i,j] in Indices (M1 + M2) ; ::_thesis: (M1 + M2) * (i,j) > 0 then [i,j] in Indices |:M2:| by A4, A5, Th5; then |:M2:| * (i,j) < |:M1:| * (i,j) by A3, Def5; then abs (M2 * (i,j)) < |:M1:| * (i,j) by A4, A5, A7, Def7; then abs (M2 * (i,j)) < abs (M1 * (i,j)) by A6, A5, A7, Def7; then A8: (abs (M1 * (i,j))) - (abs (M2 * (i,j))) > 0 by XREAL_1:50; M2 * (i,j) < 0 by A2, A4, A5, A7, Def2; then A9: - (M2 * (i,j)) = abs (M2 * (i,j)) by ABSVALUE:def_1; M1 * (i,j) > 0 by A1, A6, A5, A7, Def1; then M1 * (i,j) = abs (M1 * (i,j)) by ABSVALUE:def_1; then (M1 * (i,j)) + (M2 * (i,j)) > 0 by A9, A8; hence (M1 + M2) * (i,j) > 0 by A6, A5, A7, MATRIXR1:25; ::_thesis: verum end; hence M1 + M2 is Positive by Def1; ::_thesis: verum end; theorem :: MATRIX10:12 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is Positive & M2 is Negative holds M1 - M2 is Positive proof let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is Positive & M2 is Negative holds M1 - M2 is Positive let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Positive & M2 is Negative implies M1 - M2 is Positive ) assume A1: ( M1 is Positive & M2 is Negative ) ; ::_thesis: M1 - M2 is Positive A2: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24; A3: ( Indices M1 = [:(Seg n),(Seg n):] & Indices (M1 - M2) = [:(Seg n),(Seg n):] ) by MATRIX_1:24; A4: ( len M1 = len M2 & width M1 = width M2 ) by Lm1; for i, j being Nat st [i,j] in Indices (M1 - M2) holds (M1 - M2) * (i,j) > 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 - M2) implies (M1 - M2) * (i,j) > 0 ) assume A5: [i,j] in Indices (M1 - M2) ; ::_thesis: (M1 - M2) * (i,j) > 0 then ( M1 * (i,j) > 0 & M2 * (i,j) < 0 ) by A1, A2, A3, Def1, Def2; then (M1 * (i,j)) - (M2 * (i,j)) > 0 - 0 ; hence (M1 - M2) * (i,j) > 0 by A3, A4, A5, Th3; ::_thesis: verum end; hence M1 - M2 is Positive by Def1; ::_thesis: verum end; theorem :: MATRIX10:13 for n being Nat for M2, M1 being Matrix of n, REAL st M2 is_less_than M1 holds M1 - M2 is Positive proof let n be Nat; ::_thesis: for M2, M1 being Matrix of n, REAL st M2 is_less_than M1 holds M1 - M2 is Positive let M2, M1 be Matrix of n, REAL ; ::_thesis: ( M2 is_less_than M1 implies M1 - M2 is Positive ) assume A1: M2 is_less_than M1 ; ::_thesis: M1 - M2 is Positive A2: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24; A3: width M1 = width M2 by Lm1; A4: Indices (M1 - M2) = [:(Seg n),(Seg n):] by MATRIX_1:24; A5: ( Indices M1 = [:(Seg n),(Seg n):] & len M1 = len M2 ) by Lm1, MATRIX_1:24; for i, j being Nat st [i,j] in Indices (M1 - M2) holds (M1 - M2) * (i,j) > 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 - M2) implies (M1 - M2) * (i,j) > 0 ) assume A6: [i,j] in Indices (M1 - M2) ; ::_thesis: (M1 - M2) * (i,j) > 0 then M1 * (i,j) > M2 * (i,j) by A1, A2, A4, Def5; then (M1 * (i,j)) - (M2 * (i,j)) > 0 by XREAL_1:50; hence (M1 - M2) * (i,j) > 0 by A4, A5, A3, A6, Th3; ::_thesis: verum end; hence M1 - M2 is Positive by Def1; ::_thesis: verum end; theorem :: MATRIX10:14 for a being Element of REAL for n being Nat for M being Matrix of n, REAL st a > 0 & M is Positive holds a * M is Positive proof let a be Element of REAL ; ::_thesis: for n being Nat for M being Matrix of n, REAL st a > 0 & M is Positive holds a * M is Positive let n be Nat; ::_thesis: for M being Matrix of n, REAL st a > 0 & M is Positive holds a * M is Positive let M be Matrix of n, REAL ; ::_thesis: ( a > 0 & M is Positive implies a * M is Positive ) assume that A1: a > 0 and A2: M is Positive ; ::_thesis: a * M is Positive for i, j being Nat st [i,j] in Indices (a * M) holds (a * M) * (i,j) > 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M) implies (a * M) * (i,j) > 0 ) assume [i,j] in Indices (a * M) ; ::_thesis: (a * M) * (i,j) > 0 then A3: [i,j] in Indices M by MATRIXR1:28; then M * (i,j) > 0 by A2, Def1; then a * (M * (i,j)) > 0 by A1, XREAL_1:129; hence (a * M) * (i,j) > 0 by A3, Th4; ::_thesis: verum end; hence a * M is Positive by Def1; ::_thesis: verum end; theorem :: MATRIX10:15 for a being Element of REAL for n being Nat for M being Matrix of n, REAL st a < 0 & M is Negative holds a * M is Positive proof let a be Element of REAL ; ::_thesis: for n being Nat for M being Matrix of n, REAL st a < 0 & M is Negative holds a * M is Positive let n be Nat; ::_thesis: for M being Matrix of n, REAL st a < 0 & M is Negative holds a * M is Positive let M be Matrix of n, REAL ; ::_thesis: ( a < 0 & M is Negative implies a * M is Positive ) assume that A1: a < 0 and A2: M is Negative ; ::_thesis: a * M is Positive A3: Indices (a * M) = Indices M by MATRIXR1:28; for i, j being Nat st [i,j] in Indices (a * M) holds (a * M) * (i,j) > 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M) implies (a * M) * (i,j) > 0 ) assume A4: [i,j] in Indices (a * M) ; ::_thesis: (a * M) * (i,j) > 0 then M * (i,j) < 0 by A2, A3, Def2; then a * (M * (i,j)) > 0 by A1, XREAL_1:130; hence (a * M) * (i,j) > 0 by A3, A4, Th4; ::_thesis: verum end; hence a * M is Positive by Def1; ::_thesis: verum end; theorem :: MATRIX10:16 for n being Nat for M being Matrix of n, REAL st M is Positive holds - M is Negative proof let n be Nat; ::_thesis: for M being Matrix of n, REAL st M is Positive holds - M is Negative let M be Matrix of n, REAL ; ::_thesis: ( M is Positive implies - M is Negative ) A1: ( Indices M = [:(Seg n),(Seg n):] & Indices (- M) = [:(Seg n),(Seg n):] ) by MATRIX_1:24; assume A2: M is Positive ; ::_thesis: - M is Negative for i, j being Nat st [i,j] in Indices (- M) holds (- M) * (i,j) < 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (- M) implies (- M) * (i,j) < 0 ) assume A3: [i,j] in Indices (- M) ; ::_thesis: (- M) * (i,j) < 0 then M * (i,j) > 0 by A2, A1, Def1; then (- 1) * (M * (i,j)) < 0 * (- 1) by XREAL_1:69; then - (M * (i,j)) < 0 ; hence (- M) * (i,j) < 0 by A1, A3, Th2; ::_thesis: verum end; hence - M is Negative by Def2; ::_thesis: verum end; theorem :: MATRIX10:17 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is Negative & M2 is Negative holds M1 + M2 is Negative proof let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is Negative & M2 is Negative holds M1 + M2 is Negative let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Negative & M2 is Negative implies M1 + M2 is Negative ) assume that A1: M1 is Negative and A2: M2 is Negative ; ::_thesis: M1 + M2 is Negative A3: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; A4: Indices (M1 + M2) = [:(Seg n),(Seg n):] by MATRIX_1:24; A5: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24; for i, j being Nat st [i,j] in Indices (M1 + M2) holds (M1 + M2) * (i,j) < 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M2) implies (M1 + M2) * (i,j) < 0 ) assume A6: [i,j] in Indices (M1 + M2) ; ::_thesis: (M1 + M2) * (i,j) < 0 then M1 * (i,j) < 0 by A1, A3, A4, Def2; then (M1 * (i,j)) + (M2 * (i,j)) < M2 * (i,j) by XREAL_1:30; then (M1 * (i,j)) + (M2 * (i,j)) < 0 by A2, A5, A4, A6, Def2; hence (M1 + M2) * (i,j) < 0 by A3, A4, A6, MATRIXR1:25; ::_thesis: verum end; hence M1 + M2 is Negative by Def2; ::_thesis: verum end; theorem :: MATRIX10:18 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is_less_than - M2 holds M1 + M2 is Negative proof let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is_less_than - M2 holds M1 + M2 is Negative let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_than - M2 implies M1 + M2 is Negative ) A1: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; A2: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24; A3: Indices (M1 + M2) = [:(Seg n),(Seg n):] by MATRIX_1:24; assume A4: M1 is_less_than - M2 ; ::_thesis: M1 + M2 is Negative for i, j being Nat st [i,j] in Indices (M1 + M2) holds (M1 + M2) * (i,j) < 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M2) implies (M1 + M2) * (i,j) < 0 ) assume A5: [i,j] in Indices (M1 + M2) ; ::_thesis: (M1 + M2) * (i,j) < 0 then M1 * (i,j) < (- M2) * (i,j) by A4, A1, A3, Def5; then M1 * (i,j) < - (M2 * (i,j)) by A2, A3, A5, Th2; then (M1 * (i,j)) + (M2 * (i,j)) < 0 by XREAL_1:61; hence (M1 + M2) * (i,j) < 0 by A1, A3, A5, MATRIXR1:25; ::_thesis: verum end; hence M1 + M2 is Negative by Def2; ::_thesis: verum end; theorem :: MATRIX10:19 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is Positive & M2 is Negative & |:M1:| is_less_than |:M2:| holds M1 + M2 is Negative proof let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is Positive & M2 is Negative & |:M1:| is_less_than |:M2:| holds M1 + M2 is Negative let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Positive & M2 is Negative & |:M1:| is_less_than |:M2:| implies M1 + M2 is Negative ) assume that A1: M1 is Positive and A2: M2 is Negative and A3: |:M1:| is_less_than |:M2:| ; ::_thesis: M1 + M2 is Negative A4: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; A5: Indices (M1 + M2) = [:(Seg n),(Seg n):] by MATRIX_1:24; A6: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24; for i, j being Nat st [i,j] in Indices (M1 + M2) holds (M1 + M2) * (i,j) < 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M2) implies (M1 + M2) * (i,j) < 0 ) assume A7: [i,j] in Indices (M1 + M2) ; ::_thesis: (M1 + M2) * (i,j) < 0 then [i,j] in Indices |:M1:| by A4, A5, Th5; then |:M1:| * (i,j) < |:M2:| * (i,j) by A3, Def5; then abs (M1 * (i,j)) < |:M2:| * (i,j) by A4, A5, A7, Def7; then abs (M1 * (i,j)) < abs (M2 * (i,j)) by A6, A5, A7, Def7; then A8: (abs (M1 * (i,j))) - (abs (M2 * (i,j))) < (abs (M2 * (i,j))) - (abs (M2 * (i,j))) by XREAL_1:9; M2 * (i,j) < 0 by A2, A6, A5, A7, Def2; then A9: - (M2 * (i,j)) = abs (M2 * (i,j)) by ABSVALUE:def_1; M1 * (i,j) > 0 by A1, A4, A5, A7, Def1; then abs (M1 * (i,j)) = M1 * (i,j) by ABSVALUE:def_1; then (M1 * (i,j)) + (M2 * (i,j)) = (abs (M1 * (i,j))) - (abs (M2 * (i,j))) by A9; hence (M1 + M2) * (i,j) < 0 by A4, A5, A7, A8, MATRIXR1:25; ::_thesis: verum end; hence M1 + M2 is Negative by Def2; ::_thesis: verum end; theorem :: MATRIX10:20 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is_less_than M2 holds M1 - M2 is Negative proof let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is_less_than M2 holds M1 - M2 is Negative let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_than M2 implies M1 - M2 is Negative ) assume A1: M1 is_less_than M2 ; ::_thesis: M1 - M2 is Negative A2: ( Indices M1 = [:(Seg n),(Seg n):] & Indices (M1 - M2) = [:(Seg n),(Seg n):] ) by MATRIX_1:24; A3: ( len M1 = len M2 & width M1 = width M2 ) by Lm1; for i, j being Nat st [i,j] in Indices (M1 - M2) holds (M1 - M2) * (i,j) < 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 - M2) implies (M1 - M2) * (i,j) < 0 ) assume A4: [i,j] in Indices (M1 - M2) ; ::_thesis: (M1 - M2) * (i,j) < 0 then M1 * (i,j) < M2 * (i,j) by A1, A2, Def5; then (M1 * (i,j)) - (M2 * (i,j)) < 0 by XREAL_1:49; hence (M1 - M2) * (i,j) < 0 by A2, A3, A4, Th3; ::_thesis: verum end; hence M1 - M2 is Negative by Def2; ::_thesis: verum end; theorem :: MATRIX10:21 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is Positive & M2 is Negative holds M2 - M1 is Negative proof let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is Positive & M2 is Negative holds M2 - M1 is Negative let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Positive & M2 is Negative implies M2 - M1 is Negative ) assume A1: ( M1 is Positive & M2 is Negative ) ; ::_thesis: M2 - M1 is Negative A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; A3: ( Indices M2 = [:(Seg n),(Seg n):] & Indices (M2 - M1) = [:(Seg n),(Seg n):] ) by MATRIX_1:24; A4: ( len M1 = len M2 & width M1 = width M2 ) by Lm1; for i, j being Nat st [i,j] in Indices (M2 - M1) holds (M2 - M1) * (i,j) < 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M2 - M1) implies (M2 - M1) * (i,j) < 0 ) assume A5: [i,j] in Indices (M2 - M1) ; ::_thesis: (M2 - M1) * (i,j) < 0 then ( M1 * (i,j) > 0 & M2 * (i,j) < 0 ) by A1, A2, A3, Def1, Def2; then (M2 * (i,j)) - (M1 * (i,j)) < 0 ; hence (M2 - M1) * (i,j) < 0 by A3, A4, A5, Th3; ::_thesis: verum end; hence M2 - M1 is Negative by Def2; ::_thesis: verum end; theorem :: MATRIX10:22 for a being Element of REAL for n being Nat for M being Matrix of n, REAL st a < 0 & M is Positive holds a * M is Negative proof let a be Element of REAL ; ::_thesis: for n being Nat for M being Matrix of n, REAL st a < 0 & M is Positive holds a * M is Negative let n be Nat; ::_thesis: for M being Matrix of n, REAL st a < 0 & M is Positive holds a * M is Negative let M be Matrix of n, REAL ; ::_thesis: ( a < 0 & M is Positive implies a * M is Negative ) assume that A1: a < 0 and A2: M is Positive ; ::_thesis: a * M is Negative A3: Indices (a * M) = Indices M by MATRIXR1:28; for i, j being Nat st [i,j] in Indices (a * M) holds (a * M) * (i,j) < 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M) implies (a * M) * (i,j) < 0 ) assume A4: [i,j] in Indices (a * M) ; ::_thesis: (a * M) * (i,j) < 0 then M * (i,j) > 0 by A2, A3, Def1; then a * (M * (i,j)) < 0 by A1, XREAL_1:132; hence (a * M) * (i,j) < 0 by A3, A4, Th4; ::_thesis: verum end; hence a * M is Negative by Def2; ::_thesis: verum end; theorem :: MATRIX10:23 for a being Element of REAL for n being Nat for M being Matrix of n, REAL st a > 0 & M is Negative holds a * M is Negative proof let a be Element of REAL ; ::_thesis: for n being Nat for M being Matrix of n, REAL st a > 0 & M is Negative holds a * M is Negative let n be Nat; ::_thesis: for M being Matrix of n, REAL st a > 0 & M is Negative holds a * M is Negative let M be Matrix of n, REAL ; ::_thesis: ( a > 0 & M is Negative implies a * M is Negative ) assume that A1: a > 0 and A2: M is Negative ; ::_thesis: a * M is Negative A3: Indices (a * M) = Indices M by MATRIXR1:28; for i, j being Nat st [i,j] in Indices (a * M) holds (a * M) * (i,j) < 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M) implies (a * M) * (i,j) < 0 ) assume A4: [i,j] in Indices (a * M) ; ::_thesis: (a * M) * (i,j) < 0 then M * (i,j) < 0 by A2, A3, Def2; then a * (M * (i,j)) < 0 by A1, XREAL_1:132; hence (a * M) * (i,j) < 0 by A3, A4, Th4; ::_thesis: verum end; hence a * M is Negative by Def2; ::_thesis: verum end; theorem :: MATRIX10:24 for n being Nat for M being Matrix of n, REAL st M is Nonnegative holds - M is Nonpositive proof let n be Nat; ::_thesis: for M being Matrix of n, REAL st M is Nonnegative holds - M is Nonpositive let M be Matrix of n, REAL ; ::_thesis: ( M is Nonnegative implies - M is Nonpositive ) A1: ( Indices M = [:(Seg n),(Seg n):] & Indices (- M) = [:(Seg n),(Seg n):] ) by MATRIX_1:24; assume A2: M is Nonnegative ; ::_thesis: - M is Nonpositive for i, j being Nat st [i,j] in Indices (- M) holds (- M) * (i,j) <= 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (- M) implies (- M) * (i,j) <= 0 ) assume A3: [i,j] in Indices (- M) ; ::_thesis: (- M) * (i,j) <= 0 then M * (i,j) >= 0 by A2, A1, Def4; then - (M * (i,j)) <= 0 ; hence (- M) * (i,j) <= 0 by A1, A3, Th2; ::_thesis: verum end; hence - M is Nonpositive by Def3; ::_thesis: verum end; theorem :: MATRIX10:25 for n being Nat for M being Matrix of n, REAL st M is Negative holds M is Nonpositive proof let n be Nat; ::_thesis: for M being Matrix of n, REAL st M is Negative holds M is Nonpositive let M be Matrix of n, REAL ; ::_thesis: ( M is Negative implies M is Nonpositive ) assume M is Negative ; ::_thesis: M is Nonpositive then for i, j being Nat st [i,j] in Indices M holds M * (i,j) <= 0 by Def2; hence M is Nonpositive by Def3; ::_thesis: verum end; theorem :: MATRIX10:26 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is Nonpositive & M2 is Nonpositive holds M1 + M2 is Nonpositive proof let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is Nonpositive & M2 is Nonpositive holds M1 + M2 is Nonpositive let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Nonpositive & M2 is Nonpositive implies M1 + M2 is Nonpositive ) assume that A1: M1 is Nonpositive and A2: M2 is Nonpositive ; ::_thesis: M1 + M2 is Nonpositive A3: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; A4: Indices (M1 + M2) = [:(Seg n),(Seg n):] by MATRIX_1:24; A5: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24; for i, j being Nat st [i,j] in Indices (M1 + M2) holds (M1 + M2) * (i,j) <= 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M2) implies (M1 + M2) * (i,j) <= 0 ) assume A6: [i,j] in Indices (M1 + M2) ; ::_thesis: (M1 + M2) * (i,j) <= 0 then M1 * (i,j) <= 0 by A1, A3, A4, Def3; then A7: (M1 * (i,j)) + (M2 * (i,j)) <= M2 * (i,j) by XREAL_1:32; M2 * (i,j) <= 0 by A2, A5, A4, A6, Def3; hence (M1 + M2) * (i,j) <= 0 by A3, A4, A6, A7, MATRIXR1:25; ::_thesis: verum end; hence M1 + M2 is Nonpositive by Def3; ::_thesis: verum end; theorem :: MATRIX10:27 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is_less_or_equal_with - M2 holds M1 + M2 is Nonpositive proof let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is_less_or_equal_with - M2 holds M1 + M2 is Nonpositive let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_or_equal_with - M2 implies M1 + M2 is Nonpositive ) A1: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; A2: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24; A3: Indices (M1 + M2) = [:(Seg n),(Seg n):] by MATRIX_1:24; assume A4: M1 is_less_or_equal_with - M2 ; ::_thesis: M1 + M2 is Nonpositive for i, j being Nat st [i,j] in Indices (M1 + M2) holds (M1 + M2) * (i,j) <= 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M2) implies (M1 + M2) * (i,j) <= 0 ) assume A5: [i,j] in Indices (M1 + M2) ; ::_thesis: (M1 + M2) * (i,j) <= 0 then M1 * (i,j) <= (- M2) * (i,j) by A4, A1, A3, Def6; then M1 * (i,j) <= - (M2 * (i,j)) by A2, A3, A5, Th2; then (M1 * (i,j)) + (M2 * (i,j)) <= 0 by XREAL_1:59; hence (M1 + M2) * (i,j) <= 0 by A1, A3, A5, MATRIXR1:25; ::_thesis: verum end; hence M1 + M2 is Nonpositive by Def3; ::_thesis: verum end; theorem :: MATRIX10:28 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is_less_or_equal_with M2 holds M1 - M2 is Nonpositive proof let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is_less_or_equal_with M2 holds M1 - M2 is Nonpositive let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_or_equal_with M2 implies M1 - M2 is Nonpositive ) assume A1: M1 is_less_or_equal_with M2 ; ::_thesis: M1 - M2 is Nonpositive A2: ( Indices M1 = [:(Seg n),(Seg n):] & Indices (M1 - M2) = [:(Seg n),(Seg n):] ) by MATRIX_1:24; A3: ( len M1 = len M2 & width M1 = width M2 ) by Lm1; for i, j being Nat st [i,j] in Indices (M1 - M2) holds (M1 - M2) * (i,j) <= 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 - M2) implies (M1 - M2) * (i,j) <= 0 ) assume A4: [i,j] in Indices (M1 - M2) ; ::_thesis: (M1 - M2) * (i,j) <= 0 then M1 * (i,j) <= M2 * (i,j) by A1, A2, Def6; then (M1 * (i,j)) - (M2 * (i,j)) <= 0 by XREAL_1:47; hence (M1 - M2) * (i,j) <= 0 by A2, A3, A4, Th3; ::_thesis: verum end; hence M1 - M2 is Nonpositive by Def3; ::_thesis: verum end; theorem :: MATRIX10:29 for a being Element of REAL for n being Nat for M being Matrix of n, REAL st a <= 0 & M is Positive holds a * M is Nonpositive proof let a be Element of REAL ; ::_thesis: for n being Nat for M being Matrix of n, REAL st a <= 0 & M is Positive holds a * M is Nonpositive let n be Nat; ::_thesis: for M being Matrix of n, REAL st a <= 0 & M is Positive holds a * M is Nonpositive let M be Matrix of n, REAL ; ::_thesis: ( a <= 0 & M is Positive implies a * M is Nonpositive ) assume that A1: a <= 0 and A2: M is Positive ; ::_thesis: a * M is Nonpositive A3: Indices (a * M) = Indices M by MATRIXR1:28; for i, j being Nat st [i,j] in Indices (a * M) holds (a * M) * (i,j) <= 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M) implies (a * M) * (i,j) <= 0 ) assume A4: [i,j] in Indices (a * M) ; ::_thesis: (a * M) * (i,j) <= 0 then M * (i,j) > 0 by A2, A3, Def1; then a * (M * (i,j)) <= 0 by A1; hence (a * M) * (i,j) <= 0 by A3, A4, Th4; ::_thesis: verum end; hence a * M is Nonpositive by Def3; ::_thesis: verum end; theorem :: MATRIX10:30 for a being Element of REAL for n being Nat for M being Matrix of n, REAL st a >= 0 & M is Negative holds a * M is Nonpositive proof let a be Element of REAL ; ::_thesis: for n being Nat for M being Matrix of n, REAL st a >= 0 & M is Negative holds a * M is Nonpositive let n be Nat; ::_thesis: for M being Matrix of n, REAL st a >= 0 & M is Negative holds a * M is Nonpositive let M be Matrix of n, REAL ; ::_thesis: ( a >= 0 & M is Negative implies a * M is Nonpositive ) assume that A1: a >= 0 and A2: M is Negative ; ::_thesis: a * M is Nonpositive A3: Indices (a * M) = Indices M by MATRIXR1:28; for i, j being Nat st [i,j] in Indices (a * M) holds (a * M) * (i,j) <= 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M) implies (a * M) * (i,j) <= 0 ) assume A4: [i,j] in Indices (a * M) ; ::_thesis: (a * M) * (i,j) <= 0 then M * (i,j) < 0 by A2, A3, Def2; then a * (M * (i,j)) <= 0 by A1; hence (a * M) * (i,j) <= 0 by A3, A4, Th4; ::_thesis: verum end; hence a * M is Nonpositive by Def3; ::_thesis: verum end; theorem :: MATRIX10:31 for a being Element of REAL for n being Nat for M being Matrix of n, REAL st a >= 0 & M is Nonpositive holds a * M is Nonpositive proof let a be Element of REAL ; ::_thesis: for n being Nat for M being Matrix of n, REAL st a >= 0 & M is Nonpositive holds a * M is Nonpositive let n be Nat; ::_thesis: for M being Matrix of n, REAL st a >= 0 & M is Nonpositive holds a * M is Nonpositive let M be Matrix of n, REAL ; ::_thesis: ( a >= 0 & M is Nonpositive implies a * M is Nonpositive ) assume that A1: a >= 0 and A2: M is Nonpositive ; ::_thesis: a * M is Nonpositive A3: Indices (a * M) = Indices M by MATRIXR1:28; for i, j being Nat st [i,j] in Indices (a * M) holds (a * M) * (i,j) <= 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M) implies (a * M) * (i,j) <= 0 ) assume A4: [i,j] in Indices (a * M) ; ::_thesis: (a * M) * (i,j) <= 0 then M * (i,j) <= 0 by A2, A3, Def3; then a * (M * (i,j)) <= 0 by A1; hence (a * M) * (i,j) <= 0 by A3, A4, Th4; ::_thesis: verum end; hence a * M is Nonpositive by Def3; ::_thesis: verum end; theorem :: MATRIX10:32 for a being Element of REAL for n being Nat for M being Matrix of n, REAL st a <= 0 & M is Nonnegative holds a * M is Nonpositive proof let a be Element of REAL ; ::_thesis: for n being Nat for M being Matrix of n, REAL st a <= 0 & M is Nonnegative holds a * M is Nonpositive let n be Nat; ::_thesis: for M being Matrix of n, REAL st a <= 0 & M is Nonnegative holds a * M is Nonpositive let M be Matrix of n, REAL ; ::_thesis: ( a <= 0 & M is Nonnegative implies a * M is Nonpositive ) assume that A1: a <= 0 and A2: M is Nonnegative ; ::_thesis: a * M is Nonpositive A3: Indices (a * M) = Indices M by MATRIXR1:28; for i, j being Nat st [i,j] in Indices (a * M) holds (a * M) * (i,j) <= 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M) implies (a * M) * (i,j) <= 0 ) assume A4: [i,j] in Indices (a * M) ; ::_thesis: (a * M) * (i,j) <= 0 then M * (i,j) >= 0 by A2, A3, Def4; then a * (M * (i,j)) <= 0 by A1; hence (a * M) * (i,j) <= 0 by A3, A4, Th4; ::_thesis: verum end; hence a * M is Nonpositive by Def3; ::_thesis: verum end; theorem :: MATRIX10:33 for n being Nat for M being Matrix of n, REAL holds |:M:| is Nonnegative proof let n be Nat; ::_thesis: for M being Matrix of n, REAL holds |:M:| is Nonnegative let M be Matrix of n, REAL ; ::_thesis: |:M:| is Nonnegative for i, j being Nat st [i,j] in Indices |:M:| holds |:M:| * (i,j) >= 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices |:M:| implies |:M:| * (i,j) >= 0 ) assume A1: [i,j] in Indices |:M:| ; ::_thesis: |:M:| * (i,j) >= 0 Indices |:M:| = Indices M by Th5; then |:M:| * (i,j) = abs (M * (i,j)) by A1, Def7; hence |:M:| * (i,j) >= 0 by COMPLEX1:46; ::_thesis: verum end; hence |:M:| is Nonnegative by Def4; ::_thesis: verum end; theorem :: MATRIX10:34 for n being Nat for M1 being Matrix of n, REAL st M1 is Positive holds M1 is Nonnegative proof let n be Nat; ::_thesis: for M1 being Matrix of n, REAL st M1 is Positive holds M1 is Nonnegative let M1 be Matrix of n, REAL ; ::_thesis: ( M1 is Positive implies M1 is Nonnegative ) assume M1 is Positive ; ::_thesis: M1 is Nonnegative then for i, j being Nat st [i,j] in Indices M1 holds M1 * (i,j) >= 0 by Def1; hence M1 is Nonnegative by Def4; ::_thesis: verum end; theorem :: MATRIX10:35 for n being Nat for M being Matrix of n, REAL st M is Nonpositive holds - M is Nonnegative proof let n be Nat; ::_thesis: for M being Matrix of n, REAL st M is Nonpositive holds - M is Nonnegative let M be Matrix of n, REAL ; ::_thesis: ( M is Nonpositive implies - M is Nonnegative ) A1: ( Indices M = [:(Seg n),(Seg n):] & Indices (- M) = [:(Seg n),(Seg n):] ) by MATRIX_1:24; assume A2: M is Nonpositive ; ::_thesis: - M is Nonnegative for i, j being Nat st [i,j] in Indices (- M) holds (- M) * (i,j) >= 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (- M) implies (- M) * (i,j) >= 0 ) assume A3: [i,j] in Indices (- M) ; ::_thesis: (- M) * (i,j) >= 0 then M * (i,j) <= 0 by A2, A1, Def3; then - (M * (i,j)) >= 0 ; hence (- M) * (i,j) >= 0 by A1, A3, Th2; ::_thesis: verum end; hence - M is Nonnegative by Def4; ::_thesis: verum end; theorem Th36: :: MATRIX10:36 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is Nonnegative & M2 is Nonnegative holds M1 + M2 is Nonnegative proof let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is Nonnegative & M2 is Nonnegative holds M1 + M2 is Nonnegative let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Nonnegative & M2 is Nonnegative implies M1 + M2 is Nonnegative ) A1: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24; A2: ( Indices M1 = [:(Seg n),(Seg n):] & Indices (M1 + M2) = [:(Seg n),(Seg n):] ) by MATRIX_1:24; assume A3: ( M1 is Nonnegative & M2 is Nonnegative ) ; ::_thesis: M1 + M2 is Nonnegative for i, j being Nat st [i,j] in Indices (M1 + M2) holds (M1 + M2) * (i,j) >= 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M2) implies (M1 + M2) * (i,j) >= 0 ) assume A4: [i,j] in Indices (M1 + M2) ; ::_thesis: (M1 + M2) * (i,j) >= 0 then ( M1 * (i,j) >= 0 & M2 * (i,j) >= 0 ) by A3, A1, A2, Def4; then (M1 * (i,j)) + (M2 * (i,j)) >= 0 ; hence (M1 + M2) * (i,j) >= 0 by A2, A4, MATRIXR1:25; ::_thesis: verum end; hence M1 + M2 is Nonnegative by Def4; ::_thesis: verum end; theorem :: MATRIX10:37 for n being Nat for M1, M2 being Matrix of n, REAL st - M1 is_less_or_equal_with M2 holds M1 + M2 is Nonnegative proof let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st - M1 is_less_or_equal_with M2 holds M1 + M2 is Nonnegative let M1, M2 be Matrix of n, REAL ; ::_thesis: ( - M1 is_less_or_equal_with M2 implies M1 + M2 is Nonnegative ) A1: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; A2: Indices (- M1) = [:(Seg n),(Seg n):] by MATRIX_1:24; A3: Indices (M1 + M2) = [:(Seg n),(Seg n):] by MATRIX_1:24; assume A4: - M1 is_less_or_equal_with M2 ; ::_thesis: M1 + M2 is Nonnegative for i, j being Nat st [i,j] in Indices (M1 + M2) holds (M1 + M2) * (i,j) >= 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M2) implies (M1 + M2) * (i,j) >= 0 ) assume A5: [i,j] in Indices (M1 + M2) ; ::_thesis: (M1 + M2) * (i,j) >= 0 then (- M1) * (i,j) <= M2 * (i,j) by A4, A2, A3, Def6; then - (M1 * (i,j)) <= M2 * (i,j) by A1, A3, A5, Th2; then (M1 * (i,j)) + (M2 * (i,j)) >= 0 by XREAL_1:60; hence (M1 + M2) * (i,j) >= 0 by A1, A3, A5, MATRIXR1:25; ::_thesis: verum end; hence M1 + M2 is Nonnegative by Def4; ::_thesis: verum end; theorem :: MATRIX10:38 for n being Nat for M2, M1 being Matrix of n, REAL st M2 is_less_or_equal_with M1 holds M1 - M2 is Nonnegative proof let n be Nat; ::_thesis: for M2, M1 being Matrix of n, REAL st M2 is_less_or_equal_with M1 holds M1 - M2 is Nonnegative let M2, M1 be Matrix of n, REAL ; ::_thesis: ( M2 is_less_or_equal_with M1 implies M1 - M2 is Nonnegative ) assume A1: M2 is_less_or_equal_with M1 ; ::_thesis: M1 - M2 is Nonnegative A2: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24; A3: width M1 = width M2 by Lm1; A4: Indices (M1 - M2) = [:(Seg n),(Seg n):] by MATRIX_1:24; A5: ( Indices M1 = [:(Seg n),(Seg n):] & len M1 = len M2 ) by Lm1, MATRIX_1:24; for i, j being Nat st [i,j] in Indices (M1 - M2) holds (M1 - M2) * (i,j) >= 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 - M2) implies (M1 - M2) * (i,j) >= 0 ) assume A6: [i,j] in Indices (M1 - M2) ; ::_thesis: (M1 - M2) * (i,j) >= 0 then M1 * (i,j) >= M2 * (i,j) by A1, A2, A4, Def6; then (M1 * (i,j)) - (M2 * (i,j)) >= 0 by XREAL_1:48; hence (M1 - M2) * (i,j) >= 0 by A4, A5, A3, A6, Th3; ::_thesis: verum end; hence M1 - M2 is Nonnegative by Def4; ::_thesis: verum end; theorem :: MATRIX10:39 for a being Element of REAL for n being Nat for M being Matrix of n, REAL st a >= 0 & M is Positive holds a * M is Nonnegative proof let a be Element of REAL ; ::_thesis: for n being Nat for M being Matrix of n, REAL st a >= 0 & M is Positive holds a * M is Nonnegative let n be Nat; ::_thesis: for M being Matrix of n, REAL st a >= 0 & M is Positive holds a * M is Nonnegative let M be Matrix of n, REAL ; ::_thesis: ( a >= 0 & M is Positive implies a * M is Nonnegative ) assume that A1: a >= 0 and A2: M is Positive ; ::_thesis: a * M is Nonnegative for i, j being Nat st [i,j] in Indices (a * M) holds (a * M) * (i,j) >= 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M) implies (a * M) * (i,j) >= 0 ) assume [i,j] in Indices (a * M) ; ::_thesis: (a * M) * (i,j) >= 0 then A3: [i,j] in Indices M by MATRIXR1:28; then M * (i,j) > 0 by A2, Def1; then a * (M * (i,j)) >= 0 by A1; hence (a * M) * (i,j) >= 0 by A3, Th4; ::_thesis: verum end; hence a * M is Nonnegative by Def4; ::_thesis: verum end; theorem :: MATRIX10:40 for a being Element of REAL for n being Nat for M being Matrix of n, REAL st a <= 0 & M is Negative holds a * M is Nonnegative proof let a be Element of REAL ; ::_thesis: for n being Nat for M being Matrix of n, REAL st a <= 0 & M is Negative holds a * M is Nonnegative let n be Nat; ::_thesis: for M being Matrix of n, REAL st a <= 0 & M is Negative holds a * M is Nonnegative let M be Matrix of n, REAL ; ::_thesis: ( a <= 0 & M is Negative implies a * M is Nonnegative ) assume that A1: a <= 0 and A2: M is Negative ; ::_thesis: a * M is Nonnegative A3: Indices (a * M) = Indices M by MATRIXR1:28; for i, j being Nat st [i,j] in Indices (a * M) holds (a * M) * (i,j) >= 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M) implies (a * M) * (i,j) >= 0 ) assume A4: [i,j] in Indices (a * M) ; ::_thesis: (a * M) * (i,j) >= 0 then M * (i,j) < 0 by A2, A3, Def2; then a * (M * (i,j)) >= 0 by A1; hence (a * M) * (i,j) >= 0 by A3, A4, Th4; ::_thesis: verum end; hence a * M is Nonnegative by Def4; ::_thesis: verum end; theorem :: MATRIX10:41 for a being Element of REAL for n being Nat for M being Matrix of n, REAL st a <= 0 & M is Nonpositive holds a * M is Nonnegative proof let a be Element of REAL ; ::_thesis: for n being Nat for M being Matrix of n, REAL st a <= 0 & M is Nonpositive holds a * M is Nonnegative let n be Nat; ::_thesis: for M being Matrix of n, REAL st a <= 0 & M is Nonpositive holds a * M is Nonnegative let M be Matrix of n, REAL ; ::_thesis: ( a <= 0 & M is Nonpositive implies a * M is Nonnegative ) assume that A1: a <= 0 and A2: M is Nonpositive ; ::_thesis: a * M is Nonnegative A3: Indices (a * M) = Indices M by MATRIXR1:28; for i, j being Nat st [i,j] in Indices (a * M) holds (a * M) * (i,j) >= 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M) implies (a * M) * (i,j) >= 0 ) assume A4: [i,j] in Indices (a * M) ; ::_thesis: (a * M) * (i,j) >= 0 then M * (i,j) <= 0 by A2, A3, Def3; then a * (M * (i,j)) >= 0 by A1; hence (a * M) * (i,j) >= 0 by A3, A4, Th4; ::_thesis: verum end; hence a * M is Nonnegative by Def4; ::_thesis: verum end; theorem Th42: :: MATRIX10:42 for a being Element of REAL for n being Nat for M being Matrix of n, REAL st a >= 0 & M is Nonnegative holds a * M is Nonnegative proof let a be Element of REAL ; ::_thesis: for n being Nat for M being Matrix of n, REAL st a >= 0 & M is Nonnegative holds a * M is Nonnegative let n be Nat; ::_thesis: for M being Matrix of n, REAL st a >= 0 & M is Nonnegative holds a * M is Nonnegative let M be Matrix of n, REAL ; ::_thesis: ( a >= 0 & M is Nonnegative implies a * M is Nonnegative ) assume that A1: a >= 0 and A2: M is Nonnegative ; ::_thesis: a * M is Nonnegative A3: Indices (a * M) = Indices M by MATRIXR1:28; for i, j being Nat st [i,j] in Indices (a * M) holds (a * M) * (i,j) >= 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M) implies (a * M) * (i,j) >= 0 ) assume A4: [i,j] in Indices (a * M) ; ::_thesis: (a * M) * (i,j) >= 0 then M * (i,j) >= 0 by A2, A3, Def4; then a * (M * (i,j)) >= 0 by A1; hence (a * M) * (i,j) >= 0 by A3, A4, Th4; ::_thesis: verum end; hence a * M is Nonnegative by Def4; ::_thesis: verum end; theorem :: MATRIX10:43 for a, b being Element of REAL for n being Nat for M1, M2 being Matrix of n, REAL st a >= 0 & b >= 0 & M1 is Nonnegative & M2 is Nonnegative holds (a * M1) + (b * M2) is Nonnegative proof let a, b be Element of REAL ; ::_thesis: for n being Nat for M1, M2 being Matrix of n, REAL st a >= 0 & b >= 0 & M1 is Nonnegative & M2 is Nonnegative holds (a * M1) + (b * M2) is Nonnegative let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st a >= 0 & b >= 0 & M1 is Nonnegative & M2 is Nonnegative holds (a * M1) + (b * M2) is Nonnegative let M1, M2 be Matrix of n, REAL ; ::_thesis: ( a >= 0 & b >= 0 & M1 is Nonnegative & M2 is Nonnegative implies (a * M1) + (b * M2) is Nonnegative ) assume ( a >= 0 & b >= 0 & M1 is Nonnegative & M2 is Nonnegative ) ; ::_thesis: (a * M1) + (b * M2) is Nonnegative then ( a * M1 is Nonnegative & b * M2 is Nonnegative ) by Th42; hence (a * M1) + (b * M2) is Nonnegative by Th36; ::_thesis: verum end; begin theorem :: MATRIX10:44 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is_less_than M2 holds M1 is_less_or_equal_with M2 proof let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is_less_than M2 holds M1 is_less_or_equal_with M2 let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_than M2 implies M1 is_less_or_equal_with M2 ) assume M1 is_less_than M2 ; ::_thesis: M1 is_less_or_equal_with M2 then for i, j being Nat st [i,j] in Indices M1 holds M1 * (i,j) <= M2 * (i,j) by Def5; hence M1 is_less_or_equal_with M2 by Def6; ::_thesis: verum end; theorem :: MATRIX10:45 for n being Nat for M1, M2, M3 being Matrix of n, REAL st M1 is_less_than M2 & M2 is_less_than M3 holds M1 is_less_than M3 proof let n be Nat; ::_thesis: for M1, M2, M3 being Matrix of n, REAL st M1 is_less_than M2 & M2 is_less_than M3 holds M1 is_less_than M3 let M1, M2, M3 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_than M2 & M2 is_less_than M3 implies M1 is_less_than M3 ) A1: ( Indices M1 = [:(Seg n),(Seg n):] & Indices M2 = [:(Seg n),(Seg n):] ) by MATRIX_1:24; assume A2: ( M1 is_less_than M2 & M2 is_less_than M3 ) ; ::_thesis: M1 is_less_than M3 for i, j being Nat st [i,j] in Indices M1 holds M1 * (i,j) < M3 * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices M1 implies M1 * (i,j) < M3 * (i,j) ) assume [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) < M3 * (i,j) then ( M1 * (i,j) < M2 * (i,j) & M2 * (i,j) < M3 * (i,j) ) by A2, A1, Def5; hence M1 * (i,j) < M3 * (i,j) by XXREAL_0:2; ::_thesis: verum end; hence M1 is_less_than M3 by Def5; ::_thesis: verum end; theorem :: MATRIX10:46 for n being Nat for M1, M2, M3, M4 being Matrix of n, REAL st M1 is_less_than M2 & M3 is_less_than M4 holds M1 + M3 is_less_than M2 + M4 proof let n be Nat; ::_thesis: for M1, M2, M3, M4 being Matrix of n, REAL st M1 is_less_than M2 & M3 is_less_than M4 holds M1 + M3 is_less_than M2 + M4 let M1, M2, M3, M4 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_than M2 & M3 is_less_than M4 implies M1 + M3 is_less_than M2 + M4 ) A1: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24; A2: Indices M3 = [:(Seg n),(Seg n):] by MATRIX_1:24; A3: ( Indices M1 = [:(Seg n),(Seg n):] & Indices (M1 + M3) = [:(Seg n),(Seg n):] ) by MATRIX_1:24; assume A4: ( M1 is_less_than M2 & M3 is_less_than M4 ) ; ::_thesis: M1 + M3 is_less_than M2 + M4 for i, j being Nat st [i,j] in Indices (M1 + M3) holds (M1 + M3) * (i,j) < (M2 + M4) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M3) implies (M1 + M3) * (i,j) < (M2 + M4) * (i,j) ) assume A5: [i,j] in Indices (M1 + M3) ; ::_thesis: (M1 + M3) * (i,j) < (M2 + M4) * (i,j) then A6: ( (M1 + M3) * (i,j) = (M1 * (i,j)) + (M3 * (i,j)) & (M2 * (i,j)) + (M4 * (i,j)) = (M2 + M4) * (i,j) ) by A1, A3, MATRIXR1:25; ( M1 * (i,j) < M2 * (i,j) & M3 * (i,j) < M4 * (i,j) ) by A4, A2, A3, A5, Def5; hence (M1 + M3) * (i,j) < (M2 + M4) * (i,j) by A6, XREAL_1:8; ::_thesis: verum end; hence M1 + M3 is_less_than M2 + M4 by Def5; ::_thesis: verum end; theorem :: MATRIX10:47 for n being Nat for M1, M2, M3 being Matrix of n, REAL st M1 is_less_than M2 holds M1 + M3 is_less_than M2 + M3 proof let n be Nat; ::_thesis: for M1, M2, M3 being Matrix of n, REAL st M1 is_less_than M2 holds M1 + M3 is_less_than M2 + M3 let M1, M2, M3 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_than M2 implies M1 + M3 is_less_than M2 + M3 ) A1: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; A2: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24; A3: Indices (M1 + M3) = [:(Seg n),(Seg n):] by MATRIX_1:24; assume A4: M1 is_less_than M2 ; ::_thesis: M1 + M3 is_less_than M2 + M3 for i, j being Nat st [i,j] in Indices (M1 + M3) holds (M1 + M3) * (i,j) < (M2 + M3) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M3) implies (M1 + M3) * (i,j) < (M2 + M3) * (i,j) ) assume A5: [i,j] in Indices (M1 + M3) ; ::_thesis: (M1 + M3) * (i,j) < (M2 + M3) * (i,j) then M1 * (i,j) < M2 * (i,j) by A4, A1, A3, Def5; then (M1 * (i,j)) + (M3 * (i,j)) < (M2 * (i,j)) + (M3 * (i,j)) by XREAL_1:8; then (M1 + M3) * (i,j) < (M2 * (i,j)) + (M3 * (i,j)) by A1, A3, A5, MATRIXR1:25; hence (M1 + M3) * (i,j) < (M2 + M3) * (i,j) by A2, A3, A5, MATRIXR1:25; ::_thesis: verum end; hence M1 + M3 is_less_than M2 + M3 by Def5; ::_thesis: verum end; theorem :: MATRIX10:48 for n being Nat for M1, M2, M3 being Matrix of n, REAL st M1 is_less_than M2 holds M3 - M2 is_less_than M3 - M1 proof let n be Nat; ::_thesis: for M1, M2, M3 being Matrix of n, REAL st M1 is_less_than M2 holds M3 - M2 is_less_than M3 - M1 let M1, M2, M3 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_than M2 implies M3 - M2 is_less_than M3 - M1 ) assume A1: M1 is_less_than M2 ; ::_thesis: M3 - M2 is_less_than M3 - M1 A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; A3: Indices (M3 - M1) = [:(Seg n),(Seg n):] by MATRIX_1:24; A4: width M2 = width M3 by Lm1; A5: ( Indices M3 = [:(Seg n),(Seg n):] & len M2 = len M3 ) by Lm1, MATRIX_1:24; A6: ( len M1 = len M2 & width M1 = width M2 ) by Lm1; A7: for i, j being Nat st [i,j] in Indices (M3 - M1) holds (M3 - M2) * (i,j) < (M3 - M1) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M3 - M1) implies (M3 - M2) * (i,j) < (M3 - M1) * (i,j) ) assume A8: [i,j] in Indices (M3 - M1) ; ::_thesis: (M3 - M2) * (i,j) < (M3 - M1) * (i,j) then M1 * (i,j) < M2 * (i,j) by A1, A2, A3, Def5; then (M3 * (i,j)) - (M2 * (i,j)) < (M3 * (i,j)) - (M1 * (i,j)) by XREAL_1:15; then (M3 - M2) * (i,j) < (M3 * (i,j)) - (M1 * (i,j)) by A3, A5, A4, A8, Th3; hence (M3 - M2) * (i,j) < (M3 - M1) * (i,j) by A3, A6, A5, A4, A8, Th3; ::_thesis: verum end; Indices (M3 - M2) = [:(Seg n),(Seg n):] by MATRIX_1:24; hence M3 - M2 is_less_than M3 - M1 by A3, A7, Def5; ::_thesis: verum end; theorem :: MATRIX10:49 for n being Nat for M1, M2 being Matrix of n, REAL holds |:(M1 + M2):| is_less_or_equal_with |:M1:| + |:M2:| proof let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL holds |:(M1 + M2):| is_less_or_equal_with |:M1:| + |:M2:| let M1, M2 be Matrix of n, REAL ; ::_thesis: |:(M1 + M2):| is_less_or_equal_with |:M1:| + |:M2:| A1: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; A2: Indices (M1 + M2) = [:(Seg n),(Seg n):] by MATRIX_1:24; A3: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24; for i, j being Nat st [i,j] in Indices |:(M1 + M2):| holds |:(M1 + M2):| * (i,j) <= (|:M1:| + |:M2:|) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices |:(M1 + M2):| implies |:(M1 + M2):| * (i,j) <= (|:M1:| + |:M2:|) * (i,j) ) assume [i,j] in Indices |:(M1 + M2):| ; ::_thesis: |:(M1 + M2):| * (i,j) <= (|:M1:| + |:M2:|) * (i,j) then A4: [i,j] in Indices (M1 + M2) by Th5; then [i,j] in Indices |:M1:| by A1, A2, Th5; then A5: (|:M1:| + |:M2:|) * (i,j) = (|:M1:| * (i,j)) + (|:M2:| * (i,j)) by MATRIXR1:25 .= (abs (M1 * (i,j))) + (|:M2:| * (i,j)) by A1, A2, A4, Def7 .= (abs (M1 * (i,j))) + (abs (M2 * (i,j))) by A3, A2, A4, Def7 ; |:(M1 + M2):| * (i,j) = abs ((M1 + M2) * (i,j)) by A4, Def7 .= abs ((M1 * (i,j)) + (M2 * (i,j))) by A1, A2, A4, MATRIXR1:25 ; hence |:(M1 + M2):| * (i,j) <= (|:M1:| + |:M2:|) * (i,j) by A5, COMPLEX1:56; ::_thesis: verum end; hence |:(M1 + M2):| is_less_or_equal_with |:M1:| + |:M2:| by Def6; ::_thesis: verum end; theorem :: MATRIX10:50 for n being Nat for M1, M2, M3 being Matrix of n, REAL st M1 is_less_or_equal_with M2 holds M1 - M3 is_less_or_equal_with M2 - M3 proof let n be Nat; ::_thesis: for M1, M2, M3 being Matrix of n, REAL st M1 is_less_or_equal_with M2 holds M1 - M3 is_less_or_equal_with M2 - M3 let M1, M2, M3 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_or_equal_with M2 implies M1 - M3 is_less_or_equal_with M2 - M3 ) assume A1: M1 is_less_or_equal_with M2 ; ::_thesis: M1 - M3 is_less_or_equal_with M2 - M3 A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; A3: width M2 = width M3 by Lm1; A4: ( Indices M2 = [:(Seg n),(Seg n):] & len M2 = len M3 ) by Lm1, MATRIX_1:24; A5: Indices (M1 - M3) = [:(Seg n),(Seg n):] by MATRIX_1:24; A6: ( len M1 = len M3 & width M1 = width M3 ) by Lm1; for i, j being Nat st [i,j] in Indices (M1 - M3) holds (M1 - M3) * (i,j) <= (M2 - M3) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 - M3) implies (M1 - M3) * (i,j) <= (M2 - M3) * (i,j) ) assume A7: [i,j] in Indices (M1 - M3) ; ::_thesis: (M1 - M3) * (i,j) <= (M2 - M3) * (i,j) then M1 * (i,j) <= M2 * (i,j) by A1, A2, A5, Def6; then (M1 * (i,j)) - (M3 * (i,j)) <= (M2 * (i,j)) - (M3 * (i,j)) by XREAL_1:9; then (M1 - M3) * (i,j) <= (M2 * (i,j)) - (M3 * (i,j)) by A2, A5, A6, A7, Th3; hence (M1 - M3) * (i,j) <= (M2 - M3) * (i,j) by A5, A4, A3, A7, Th3; ::_thesis: verum end; hence M1 - M3 is_less_or_equal_with M2 - M3 by Def6; ::_thesis: verum end; theorem :: MATRIX10:51 for n being Nat for M1, M3, M2 being Matrix of n, REAL st M1 - M3 is_less_or_equal_with M2 - M3 holds M1 is_less_or_equal_with M2 proof let n be Nat; ::_thesis: for M1, M3, M2 being Matrix of n, REAL st M1 - M3 is_less_or_equal_with M2 - M3 holds M1 is_less_or_equal_with M2 let M1, M3, M2 be Matrix of n, REAL ; ::_thesis: ( M1 - M3 is_less_or_equal_with M2 - M3 implies M1 is_less_or_equal_with M2 ) assume A1: M1 - M3 is_less_or_equal_with M2 - M3 ; ::_thesis: M1 is_less_or_equal_with M2 A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; A3: width M2 = width M3 by Lm1; A4: ( Indices M2 = [:(Seg n),(Seg n):] & len M2 = len M3 ) by Lm1, MATRIX_1:24; A5: Indices (M1 - M3) = [:(Seg n),(Seg n):] by MATRIX_1:24; A6: ( len M1 = len M3 & width M1 = width M3 ) by Lm1; for i, j being Nat st [i,j] in Indices M1 holds M1 * (i,j) <= M2 * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices M1 implies M1 * (i,j) <= M2 * (i,j) ) assume A7: [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) <= M2 * (i,j) then (M1 - M3) * (i,j) <= (M2 - M3) * (i,j) by A1, A2, A5, Def6; then (M1 * (i,j)) - (M3 * (i,j)) <= (M2 - M3) * (i,j) by A6, A7, Th3; then (M1 * (i,j)) - (M3 * (i,j)) <= (M2 * (i,j)) - (M3 * (i,j)) by A2, A4, A3, A7, Th3; then ((M1 * (i,j)) - (M3 * (i,j))) + (M3 * (i,j)) <= ((M2 * (i,j)) - (M3 * (i,j))) + (M3 * (i,j)) by XREAL_1:6; hence M1 * (i,j) <= M2 * (i,j) ; ::_thesis: verum end; hence M1 is_less_or_equal_with M2 by Def6; ::_thesis: verum end; theorem :: MATRIX10:52 for n being Nat for M1, M2, M3 being Matrix of n, REAL st M1 is_less_or_equal_with M2 - M3 holds M3 is_less_or_equal_with M2 - M1 proof let n be Nat; ::_thesis: for M1, M2, M3 being Matrix of n, REAL st M1 is_less_or_equal_with M2 - M3 holds M3 is_less_or_equal_with M2 - M1 let M1, M2, M3 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_or_equal_with M2 - M3 implies M3 is_less_or_equal_with M2 - M1 ) assume A1: M1 is_less_or_equal_with M2 - M3 ; ::_thesis: M3 is_less_or_equal_with M2 - M1 A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; A3: Indices M3 = [:(Seg n),(Seg n):] by MATRIX_1:24; A4: ( len M2 = len M3 & width M2 = width M3 ) by Lm1; A5: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24; A6: ( len M1 = len M2 & width M1 = width M2 ) by Lm1; for i, j being Nat st [i,j] in Indices M3 holds M3 * (i,j) <= (M2 - M1) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices M3 implies M3 * (i,j) <= (M2 - M1) * (i,j) ) assume A7: [i,j] in Indices M3 ; ::_thesis: M3 * (i,j) <= (M2 - M1) * (i,j) then M1 * (i,j) <= (M2 - M3) * (i,j) by A1, A2, A3, Def6; then M1 * (i,j) <= (M2 * (i,j)) - (M3 * (i,j)) by A5, A3, A4, A7, Th3; then M3 * (i,j) <= (M2 * (i,j)) - (M1 * (i,j)) by XREAL_1:11; hence M3 * (i,j) <= (M2 - M1) * (i,j) by A5, A3, A6, A7, Th3; ::_thesis: verum end; hence M3 is_less_or_equal_with M2 - M1 by Def6; ::_thesis: verum end; theorem :: MATRIX10:53 for n being Nat for M1, M2, M3 being Matrix of n, REAL st M1 - M2 is_less_or_equal_with M3 holds M1 - M3 is_less_or_equal_with M2 proof let n be Nat; ::_thesis: for M1, M2, M3 being Matrix of n, REAL st M1 - M2 is_less_or_equal_with M3 holds M1 - M3 is_less_or_equal_with M2 let M1, M2, M3 be Matrix of n, REAL ; ::_thesis: ( M1 - M2 is_less_or_equal_with M3 implies M1 - M3 is_less_or_equal_with M2 ) assume A1: M1 - M2 is_less_or_equal_with M3 ; ::_thesis: M1 - M3 is_less_or_equal_with M2 A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; A3: ( len M1 = len M3 & width M1 = width M3 ) by Lm1; A4: Indices (M1 - M2) = [:(Seg n),(Seg n):] by MATRIX_1:24; A5: Indices (M1 - M3) = [:(Seg n),(Seg n):] by MATRIX_1:24; A6: ( len M1 = len M2 & width M1 = width M2 ) by Lm1; for i, j being Nat st [i,j] in Indices (M1 - M3) holds (M1 - M3) * (i,j) <= M2 * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 - M3) implies (M1 - M3) * (i,j) <= M2 * (i,j) ) assume A7: [i,j] in Indices (M1 - M3) ; ::_thesis: (M1 - M3) * (i,j) <= M2 * (i,j) then (M1 - M2) * (i,j) <= M3 * (i,j) by A1, A4, A5, Def6; then (M1 * (i,j)) - (M2 * (i,j)) <= M3 * (i,j) by A2, A5, A6, A7, Th3; then (M1 * (i,j)) - (M3 * (i,j)) <= M2 * (i,j) by XREAL_1:12; hence (M1 - M3) * (i,j) <= M2 * (i,j) by A2, A5, A3, A7, Th3; ::_thesis: verum end; hence M1 - M3 is_less_or_equal_with M2 by Def6; ::_thesis: verum end; theorem :: MATRIX10:54 for n being Nat for M1, M2, M3, M4 being Matrix of n, REAL st M1 is_less_than M2 & M3 is_less_or_equal_with M4 holds M1 - M4 is_less_than M2 - M3 proof let n be Nat; ::_thesis: for M1, M2, M3, M4 being Matrix of n, REAL st M1 is_less_than M2 & M3 is_less_or_equal_with M4 holds M1 - M4 is_less_than M2 - M3 let M1, M2, M3, M4 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_than M2 & M3 is_less_or_equal_with M4 implies M1 - M4 is_less_than M2 - M3 ) assume A1: ( M1 is_less_than M2 & M3 is_less_or_equal_with M4 ) ; ::_thesis: M1 - M4 is_less_than M2 - M3 A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; A3: ( Indices M2 = [:(Seg n),(Seg n):] & len M2 = len M3 ) by Lm1, MATRIX_1:24; A4: Indices M3 = [:(Seg n),(Seg n):] by MATRIX_1:24; A5: width M2 = width M3 by Lm1; A6: Indices (M1 - M4) = [:(Seg n),(Seg n):] by MATRIX_1:24; A7: ( len M1 = len M4 & width M1 = width M4 ) by Lm1; for i, j being Nat st [i,j] in Indices (M1 - M4) holds (M1 - M4) * (i,j) < (M2 - M3) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 - M4) implies (M1 - M4) * (i,j) < (M2 - M3) * (i,j) ) assume A8: [i,j] in Indices (M1 - M4) ; ::_thesis: (M1 - M4) * (i,j) < (M2 - M3) * (i,j) then ( M1 * (i,j) < M2 * (i,j) & M3 * (i,j) <= M4 * (i,j) ) by A1, A2, A4, A6, Def5, Def6; then (M1 * (i,j)) - (M4 * (i,j)) < (M2 * (i,j)) - (M3 * (i,j)) by XREAL_1:14; then (M1 - M4) * (i,j) < (M2 * (i,j)) - (M3 * (i,j)) by A2, A6, A7, A8, Th3; hence (M1 - M4) * (i,j) < (M2 - M3) * (i,j) by A6, A3, A5, A8, Th3; ::_thesis: verum end; hence M1 - M4 is_less_than M2 - M3 by Def5; ::_thesis: verum end; theorem :: MATRIX10:55 for n being Nat for M1, M2, M3, M4 being Matrix of n, REAL st M1 is_less_or_equal_with M2 & M3 is_less_than M4 holds M1 - M4 is_less_than M2 - M3 proof let n be Nat; ::_thesis: for M1, M2, M3, M4 being Matrix of n, REAL st M1 is_less_or_equal_with M2 & M3 is_less_than M4 holds M1 - M4 is_less_than M2 - M3 let M1, M2, M3, M4 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_or_equal_with M2 & M3 is_less_than M4 implies M1 - M4 is_less_than M2 - M3 ) assume A1: ( M1 is_less_or_equal_with M2 & M3 is_less_than M4 ) ; ::_thesis: M1 - M4 is_less_than M2 - M3 A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; A3: ( Indices M2 = [:(Seg n),(Seg n):] & len M2 = len M3 ) by Lm1, MATRIX_1:24; A4: Indices M3 = [:(Seg n),(Seg n):] by MATRIX_1:24; A5: width M2 = width M3 by Lm1; A6: Indices (M1 - M4) = [:(Seg n),(Seg n):] by MATRIX_1:24; A7: ( len M1 = len M4 & width M1 = width M4 ) by Lm1; for i, j being Nat st [i,j] in Indices (M1 - M4) holds (M1 - M4) * (i,j) < (M2 - M3) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 - M4) implies (M1 - M4) * (i,j) < (M2 - M3) * (i,j) ) assume A8: [i,j] in Indices (M1 - M4) ; ::_thesis: (M1 - M4) * (i,j) < (M2 - M3) * (i,j) then ( M1 * (i,j) <= M2 * (i,j) & M3 * (i,j) < M4 * (i,j) ) by A1, A2, A4, A6, Def5, Def6; then (M1 * (i,j)) - (M4 * (i,j)) < (M2 * (i,j)) - (M3 * (i,j)) by XREAL_1:15; then (M1 - M4) * (i,j) < (M2 * (i,j)) - (M3 * (i,j)) by A2, A6, A7, A8, Th3; hence (M1 - M4) * (i,j) < (M2 - M3) * (i,j) by A6, A3, A5, A8, Th3; ::_thesis: verum end; hence M1 - M4 is_less_than M2 - M3 by Def5; ::_thesis: verum end; theorem :: MATRIX10:56 for n being Nat for M1, M2, M3, M4 being Matrix of n, REAL st M1 - M2 is_less_or_equal_with M3 - M4 holds M1 - M3 is_less_or_equal_with M2 - M4 proof let n be Nat; ::_thesis: for M1, M2, M3, M4 being Matrix of n, REAL st M1 - M2 is_less_or_equal_with M3 - M4 holds M1 - M3 is_less_or_equal_with M2 - M4 let M1, M2, M3, M4 be Matrix of n, REAL ; ::_thesis: ( M1 - M2 is_less_or_equal_with M3 - M4 implies M1 - M3 is_less_or_equal_with M2 - M4 ) A1: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; A2: Indices (M1 - M2) = [:(Seg n),(Seg n):] by MATRIX_1:24; A3: Indices (M1 - M3) = [:(Seg n),(Seg n):] by MATRIX_1:24; A4: Indices M3 = [:(Seg n),(Seg n):] by MATRIX_1:24; A5: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24; A6: ( len M1 = len M2 & width M1 = width M2 ) by Lm1; A7: ( len M1 = len M3 & width M1 = width M3 ) by Lm1; A8: ( len M3 = len M4 & width M3 = width M4 ) by Lm1; assume A9: M1 - M2 is_less_or_equal_with M3 - M4 ; ::_thesis: M1 - M3 is_less_or_equal_with M2 - M4 for i, j being Nat st [i,j] in Indices (M1 - M3) holds (M1 - M3) * (i,j) <= (M2 - M4) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 - M3) implies (M1 - M3) * (i,j) <= (M2 - M4) * (i,j) ) assume A10: [i,j] in Indices (M1 - M3) ; ::_thesis: (M1 - M3) * (i,j) <= (M2 - M4) * (i,j) then (M1 - M2) * (i,j) <= (M3 - M4) * (i,j) by A9, A2, A3, Def6; then (M1 * (i,j)) - (M2 * (i,j)) <= (M3 - M4) * (i,j) by A1, A3, A6, A10, Th3; then (M1 * (i,j)) - (M2 * (i,j)) <= (M3 * (i,j)) - (M4 * (i,j)) by A4, A3, A8, A10, Th3; then (M1 * (i,j)) - (M3 * (i,j)) <= (M2 * (i,j)) - (M4 * (i,j)) by XREAL_1:16; then (M1 - M3) * (i,j) <= (M2 * (i,j)) - (M4 * (i,j)) by A1, A3, A7, A10, Th3; hence (M1 - M3) * (i,j) <= (M2 - M4) * (i,j) by A5, A3, A6, A8, A7, A10, Th3; ::_thesis: verum end; hence M1 - M3 is_less_or_equal_with M2 - M4 by Def6; ::_thesis: verum end; theorem :: MATRIX10:57 for n being Nat for M1, M2, M3, M4 being Matrix of n, REAL st M1 - M2 is_less_or_equal_with M3 - M4 holds M4 - M2 is_less_or_equal_with M3 - M1 proof let n be Nat; ::_thesis: for M1, M2, M3, M4 being Matrix of n, REAL st M1 - M2 is_less_or_equal_with M3 - M4 holds M4 - M2 is_less_or_equal_with M3 - M1 let M1, M2, M3, M4 be Matrix of n, REAL ; ::_thesis: ( M1 - M2 is_less_or_equal_with M3 - M4 implies M4 - M2 is_less_or_equal_with M3 - M1 ) A1: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; A2: Indices M3 = [:(Seg n),(Seg n):] by MATRIX_1:24; A3: Indices (M1 - M2) = [:(Seg n),(Seg n):] by MATRIX_1:24; A4: Indices M4 = [:(Seg n),(Seg n):] by MATRIX_1:24; A5: Indices (M4 - M2) = [:(Seg n),(Seg n):] by MATRIX_1:24; A6: ( len M1 = len M3 & width M1 = width M3 ) by Lm1; A7: ( len M3 = len M4 & width M3 = width M4 ) by Lm1; A8: ( len M1 = len M2 & width M1 = width M2 ) by Lm1; assume A9: M1 - M2 is_less_or_equal_with M3 - M4 ; ::_thesis: M4 - M2 is_less_or_equal_with M3 - M1 for i, j being Nat st [i,j] in Indices (M4 - M2) holds (M4 - M2) * (i,j) <= (M3 - M1) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M4 - M2) implies (M4 - M2) * (i,j) <= (M3 - M1) * (i,j) ) assume A10: [i,j] in Indices (M4 - M2) ; ::_thesis: (M4 - M2) * (i,j) <= (M3 - M1) * (i,j) then (M1 - M2) * (i,j) <= (M3 - M4) * (i,j) by A9, A3, A5, Def6; then (M1 * (i,j)) - (M2 * (i,j)) <= (M3 - M4) * (i,j) by A1, A5, A8, A10, Th3; then (M1 * (i,j)) - (M2 * (i,j)) <= (M3 * (i,j)) - (M4 * (i,j)) by A2, A5, A7, A10, Th3; then (M4 * (i,j)) - (M2 * (i,j)) <= (M3 * (i,j)) - (M1 * (i,j)) by XREAL_1:17; then (M4 - M2) * (i,j) <= (M3 * (i,j)) - (M1 * (i,j)) by A4, A5, A8, A7, A6, A10, Th3; hence (M4 - M2) * (i,j) <= (M3 - M1) * (i,j) by A2, A5, A6, A10, Th3; ::_thesis: verum end; hence M4 - M2 is_less_or_equal_with M3 - M1 by Def6; ::_thesis: verum end; theorem :: MATRIX10:58 for n being Nat for M1, M2, M3, M4 being Matrix of n, REAL st M1 - M2 is_less_or_equal_with M3 - M4 holds M4 - M3 is_less_or_equal_with M2 - M1 proof let n be Nat; ::_thesis: for M1, M2, M3, M4 being Matrix of n, REAL st M1 - M2 is_less_or_equal_with M3 - M4 holds M4 - M3 is_less_or_equal_with M2 - M1 let M1, M2, M3, M4 be Matrix of n, REAL ; ::_thesis: ( M1 - M2 is_less_or_equal_with M3 - M4 implies M4 - M3 is_less_or_equal_with M2 - M1 ) A1: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; A2: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24; A3: Indices M4 = [:(Seg n),(Seg n):] by MATRIX_1:24; A4: Indices M3 = [:(Seg n),(Seg n):] by MATRIX_1:24; A5: Indices (M1 - M2) = [:(Seg n),(Seg n):] by MATRIX_1:24; A6: Indices (M4 - M3) = [:(Seg n),(Seg n):] by MATRIX_1:24; A7: ( len M3 = len M4 & width M3 = width M4 ) by Lm1; A8: ( len M1 = len M2 & width M1 = width M2 ) by Lm1; assume A9: M1 - M2 is_less_or_equal_with M3 - M4 ; ::_thesis: M4 - M3 is_less_or_equal_with M2 - M1 for i, j being Nat st [i,j] in Indices (M4 - M3) holds (M4 - M3) * (i,j) <= (M2 - M1) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M4 - M3) implies (M4 - M3) * (i,j) <= (M2 - M1) * (i,j) ) assume A10: [i,j] in Indices (M4 - M3) ; ::_thesis: (M4 - M3) * (i,j) <= (M2 - M1) * (i,j) then (M1 - M2) * (i,j) <= (M3 - M4) * (i,j) by A9, A5, A6, Def6; then (M1 * (i,j)) - (M2 * (i,j)) <= (M3 - M4) * (i,j) by A1, A6, A8, A10, Th3; then (M1 * (i,j)) - (M2 * (i,j)) <= (M3 * (i,j)) - (M4 * (i,j)) by A4, A6, A7, A10, Th3; then (M4 * (i,j)) - (M3 * (i,j)) <= (M2 * (i,j)) - (M1 * (i,j)) by XREAL_1:18; then (M4 - M3) * (i,j) <= (M2 * (i,j)) - (M1 * (i,j)) by A3, A6, A7, A10, Th3; hence (M4 - M3) * (i,j) <= (M2 - M1) * (i,j) by A2, A6, A8, A10, Th3; ::_thesis: verum end; hence M4 - M3 is_less_or_equal_with M2 - M1 by Def6; ::_thesis: verum end; theorem :: MATRIX10:59 for n being Nat for M1, M2, M3 being Matrix of n, REAL st M1 + M2 is_less_or_equal_with M3 holds M1 is_less_or_equal_with M3 - M2 proof let n be Nat; ::_thesis: for M1, M2, M3 being Matrix of n, REAL st M1 + M2 is_less_or_equal_with M3 holds M1 is_less_or_equal_with M3 - M2 let M1, M2, M3 be Matrix of n, REAL ; ::_thesis: ( M1 + M2 is_less_or_equal_with M3 implies M1 is_less_or_equal_with M3 - M2 ) assume A1: M1 + M2 is_less_or_equal_with M3 ; ::_thesis: M1 is_less_or_equal_with M3 - M2 A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; A3: width M2 = width M3 by Lm1; A4: Indices (M1 + M2) = [:(Seg n),(Seg n):] by MATRIX_1:24; A5: ( Indices M3 = [:(Seg n),(Seg n):] & len M2 = len M3 ) by Lm1, MATRIX_1:24; for i, j being Nat st [i,j] in Indices M1 holds M1 * (i,j) <= (M3 - M2) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices M1 implies M1 * (i,j) <= (M3 - M2) * (i,j) ) assume A6: [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) <= (M3 - M2) * (i,j) then (M1 + M2) * (i,j) <= M3 * (i,j) by A1, A2, A4, Def6; then (M1 * (i,j)) + (M2 * (i,j)) <= M3 * (i,j) by A6, MATRIXR1:25; then M1 * (i,j) <= (M3 * (i,j)) - (M2 * (i,j)) by XREAL_1:19; hence M1 * (i,j) <= (M3 - M2) * (i,j) by A2, A5, A3, A6, Th3; ::_thesis: verum end; hence M1 is_less_or_equal_with M3 - M2 by Def6; ::_thesis: verum end; theorem :: MATRIX10:60 for n being Nat for M1, M2, M3, M4 being Matrix of n, REAL st M1 + M2 is_less_or_equal_with M3 + M4 holds M1 - M3 is_less_or_equal_with M4 - M2 proof let n be Nat; ::_thesis: for M1, M2, M3, M4 being Matrix of n, REAL st M1 + M2 is_less_or_equal_with M3 + M4 holds M1 - M3 is_less_or_equal_with M4 - M2 let M1, M2, M3, M4 be Matrix of n, REAL ; ::_thesis: ( M1 + M2 is_less_or_equal_with M3 + M4 implies M1 - M3 is_less_or_equal_with M4 - M2 ) assume A1: M1 + M2 is_less_or_equal_with M3 + M4 ; ::_thesis: M1 - M3 is_less_or_equal_with M4 - M2 A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; A3: width M2 = width M4 by Lm1; A4: Indices (M1 + M2) = [:(Seg n),(Seg n):] by MATRIX_1:24; A5: ( Indices M4 = [:(Seg n),(Seg n):] & len M2 = len M4 ) by Lm1, MATRIX_1:24; A6: Indices M3 = [:(Seg n),(Seg n):] by MATRIX_1:24; A7: Indices (M1 - M3) = [:(Seg n),(Seg n):] by MATRIX_1:24; A8: ( len M1 = len M3 & width M1 = width M3 ) by Lm1; for i, j being Nat st [i,j] in Indices (M1 - M3) holds (M1 - M3) * (i,j) <= (M4 - M2) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 - M3) implies (M1 - M3) * (i,j) <= (M4 - M2) * (i,j) ) assume A9: [i,j] in Indices (M1 - M3) ; ::_thesis: (M1 - M3) * (i,j) <= (M4 - M2) * (i,j) then (M1 + M2) * (i,j) <= (M3 + M4) * (i,j) by A1, A4, A7, Def6; then (M1 * (i,j)) + (M2 * (i,j)) <= (M3 + M4) * (i,j) by A2, A7, A9, MATRIXR1:25; then (M1 * (i,j)) + (M2 * (i,j)) <= (M3 * (i,j)) + (M4 * (i,j)) by A6, A7, A9, MATRIXR1:25; then (M1 * (i,j)) - (M3 * (i,j)) <= (M4 * (i,j)) - (M2 * (i,j)) by XREAL_1:21; then (M1 - M3) * (i,j) <= (M4 * (i,j)) - (M2 * (i,j)) by A2, A7, A8, A9, Th3; hence (M1 - M3) * (i,j) <= (M4 - M2) * (i,j) by A7, A5, A3, A9, Th3; ::_thesis: verum end; hence M1 - M3 is_less_or_equal_with M4 - M2 by Def6; ::_thesis: verum end; theorem :: MATRIX10:61 for n being Nat for M1, M2, M3, M4 being Matrix of n, REAL st M1 + M2 is_less_or_equal_with M3 - M4 holds M1 + M4 is_less_or_equal_with M3 - M2 proof let n be Nat; ::_thesis: for M1, M2, M3, M4 being Matrix of n, REAL st M1 + M2 is_less_or_equal_with M3 - M4 holds M1 + M4 is_less_or_equal_with M3 - M2 let M1, M2, M3, M4 be Matrix of n, REAL ; ::_thesis: ( M1 + M2 is_less_or_equal_with M3 - M4 implies M1 + M4 is_less_or_equal_with M3 - M2 ) assume A1: M1 + M2 is_less_or_equal_with M3 - M4 ; ::_thesis: M1 + M4 is_less_or_equal_with M3 - M2 A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; A3: Indices (M1 + M2) = [:(Seg n),(Seg n):] by MATRIX_1:24; A4: Indices (M1 + M4) = [:(Seg n),(Seg n):] by MATRIX_1:24; A5: ( len M2 = len M3 & width M2 = width M3 ) by Lm1; A6: Indices M3 = [:(Seg n),(Seg n):] by MATRIX_1:24; A7: ( len M3 = len M4 & width M3 = width M4 ) by Lm1; for i, j being Nat st [i,j] in Indices (M1 + M4) holds (M1 + M4) * (i,j) <= (M3 - M2) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M4) implies (M1 + M4) * (i,j) <= (M3 - M2) * (i,j) ) assume A8: [i,j] in Indices (M1 + M4) ; ::_thesis: (M1 + M4) * (i,j) <= (M3 - M2) * (i,j) then (M1 + M2) * (i,j) <= (M3 - M4) * (i,j) by A1, A3, A4, Def6; then (M1 * (i,j)) + (M2 * (i,j)) <= (M3 - M4) * (i,j) by A2, A4, A8, MATRIXR1:25; then (M1 * (i,j)) + (M2 * (i,j)) <= (M3 * (i,j)) - (M4 * (i,j)) by A6, A4, A7, A8, Th3; then (M1 * (i,j)) + (M4 * (i,j)) <= (M3 * (i,j)) - (M2 * (i,j)) by XREAL_1:22; then (M1 + M4) * (i,j) <= (M3 * (i,j)) - (M2 * (i,j)) by A2, A4, A8, MATRIXR1:25; hence (M1 + M4) * (i,j) <= (M3 - M2) * (i,j) by A6, A4, A5, A8, Th3; ::_thesis: verum end; hence M1 + M4 is_less_or_equal_with M3 - M2 by Def6; ::_thesis: verum end; theorem :: MATRIX10:62 for n being Nat for M1, M2, M3, M4 being Matrix of n, REAL st M1 - M2 is_less_or_equal_with M3 + M4 holds M1 - M4 is_less_or_equal_with M3 + M2 proof let n be Nat; ::_thesis: for M1, M2, M3, M4 being Matrix of n, REAL st M1 - M2 is_less_or_equal_with M3 + M4 holds M1 - M4 is_less_or_equal_with M3 + M2 let M1, M2, M3, M4 be Matrix of n, REAL ; ::_thesis: ( M1 - M2 is_less_or_equal_with M3 + M4 implies M1 - M4 is_less_or_equal_with M3 + M2 ) assume A1: M1 - M2 is_less_or_equal_with M3 + M4 ; ::_thesis: M1 - M4 is_less_or_equal_with M3 + M2 A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; A3: Indices (M1 - M2) = [:(Seg n),(Seg n):] by MATRIX_1:24; A4: Indices (M1 - M4) = [:(Seg n),(Seg n):] by MATRIX_1:24; A5: ( len M1 = len M2 & width M1 = width M2 ) by Lm1; A6: Indices M3 = [:(Seg n),(Seg n):] by MATRIX_1:24; A7: ( len M1 = len M4 & width M1 = width M4 ) by Lm1; for i, j being Nat st [i,j] in Indices (M1 - M4) holds (M1 - M4) * (i,j) <= (M3 + M2) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 - M4) implies (M1 - M4) * (i,j) <= (M3 + M2) * (i,j) ) assume A8: [i,j] in Indices (M1 - M4) ; ::_thesis: (M1 - M4) * (i,j) <= (M3 + M2) * (i,j) then (M1 - M2) * (i,j) <= (M3 + M4) * (i,j) by A1, A3, A4, Def6; then (M1 * (i,j)) - (M2 * (i,j)) <= (M3 + M4) * (i,j) by A2, A4, A5, A8, Th3; then (M1 * (i,j)) - (M2 * (i,j)) <= (M3 * (i,j)) + (M4 * (i,j)) by A6, A4, A8, MATRIXR1:25; then (M1 * (i,j)) - (M4 * (i,j)) <= (M3 * (i,j)) + (M2 * (i,j)) by XREAL_1:23; then (M1 - M4) * (i,j) <= (M3 * (i,j)) + (M2 * (i,j)) by A2, A4, A7, A8, Th3; hence (M1 - M4) * (i,j) <= (M3 + M2) * (i,j) by A6, A4, A8, MATRIXR1:25; ::_thesis: verum end; hence M1 - M4 is_less_or_equal_with M3 + M2 by Def6; ::_thesis: verum end; theorem :: MATRIX10:63 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is_less_or_equal_with M2 holds - M2 is_less_or_equal_with - M1 proof let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is_less_or_equal_with M2 holds - M2 is_less_or_equal_with - M1 let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_or_equal_with M2 implies - M2 is_less_or_equal_with - M1 ) A1: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; A2: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24; A3: Indices (- M2) = [:(Seg n),(Seg n):] by MATRIX_1:24; assume A4: M1 is_less_or_equal_with M2 ; ::_thesis: - M2 is_less_or_equal_with - M1 for i, j being Nat st [i,j] in Indices (- M2) holds (- M2) * (i,j) <= (- M1) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (- M2) implies (- M2) * (i,j) <= (- M1) * (i,j) ) assume A5: [i,j] in Indices (- M2) ; ::_thesis: (- M2) * (i,j) <= (- M1) * (i,j) then M1 * (i,j) <= M2 * (i,j) by A4, A1, A3, Def6; then - (M2 * (i,j)) <= - (M1 * (i,j)) by XREAL_1:24; then (- M2) * (i,j) <= - (M1 * (i,j)) by A2, A3, A5, Th2; hence (- M2) * (i,j) <= (- M1) * (i,j) by A1, A3, A5, Th2; ::_thesis: verum end; hence - M2 is_less_or_equal_with - M1 by Def6; ::_thesis: verum end; theorem :: MATRIX10:64 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is_less_or_equal_with - M2 holds M2 is_less_or_equal_with - M1 proof let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is_less_or_equal_with - M2 holds M2 is_less_or_equal_with - M1 let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_or_equal_with - M2 implies M2 is_less_or_equal_with - M1 ) A1: ( Indices M1 = [:(Seg n),(Seg n):] & Indices M2 = [:(Seg n),(Seg n):] ) by MATRIX_1:24; assume A2: M1 is_less_or_equal_with - M2 ; ::_thesis: M2 is_less_or_equal_with - M1 for i, j being Nat st [i,j] in Indices M2 holds M2 * (i,j) <= (- M1) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices M2 implies M2 * (i,j) <= (- M1) * (i,j) ) assume A3: [i,j] in Indices M2 ; ::_thesis: M2 * (i,j) <= (- M1) * (i,j) then M1 * (i,j) <= (- M2) * (i,j) by A2, A1, Def6; then M1 * (i,j) <= - (M2 * (i,j)) by A3, Th2; then M2 * (i,j) <= - (M1 * (i,j)) by XREAL_1:25; hence M2 * (i,j) <= (- M1) * (i,j) by A1, A3, Th2; ::_thesis: verum end; hence M2 is_less_or_equal_with - M1 by Def6; ::_thesis: verum end; theorem :: MATRIX10:65 for n being Nat for M2, M1 being Matrix of n, REAL st - M2 is_less_or_equal_with M1 holds - M1 is_less_or_equal_with M2 proof let n be Nat; ::_thesis: for M2, M1 being Matrix of n, REAL st - M2 is_less_or_equal_with M1 holds - M1 is_less_or_equal_with M2 let M2, M1 be Matrix of n, REAL ; ::_thesis: ( - M2 is_less_or_equal_with M1 implies - M1 is_less_or_equal_with M2 ) A1: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; A2: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24; A3: Indices (- M2) = [:(Seg n),(Seg n):] by MATRIX_1:24; A4: Indices (- M1) = [:(Seg n),(Seg n):] by MATRIX_1:24; assume A5: - M2 is_less_or_equal_with M1 ; ::_thesis: - M1 is_less_or_equal_with M2 for i, j being Nat st [i,j] in Indices (- M1) holds (- M1) * (i,j) <= M2 * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (- M1) implies (- M1) * (i,j) <= M2 * (i,j) ) assume A6: [i,j] in Indices (- M1) ; ::_thesis: (- M1) * (i,j) <= M2 * (i,j) then (- M2) * (i,j) <= M1 * (i,j) by A5, A4, A3, Def6; then - (M2 * (i,j)) <= M1 * (i,j) by A2, A4, A6, Th2; then - (M1 * (i,j)) <= M2 * (i,j) by XREAL_1:26; hence (- M1) * (i,j) <= M2 * (i,j) by A1, A4, A6, Th2; ::_thesis: verum end; hence - M1 is_less_or_equal_with M2 by Def6; ::_thesis: verum end; theorem :: MATRIX10:66 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is Positive holds M2 is_less_than M2 + M1 proof let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is Positive holds M2 is_less_than M2 + M1 let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Positive implies M2 is_less_than M2 + M1 ) A1: ( Indices M1 = [:(Seg n),(Seg n):] & Indices M2 = [:(Seg n),(Seg n):] ) by MATRIX_1:24; assume A2: M1 is Positive ; ::_thesis: M2 is_less_than M2 + M1 for i, j being Nat st [i,j] in Indices M2 holds M2 * (i,j) < (M2 + M1) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices M2 implies M2 * (i,j) < (M2 + M1) * (i,j) ) assume A3: [i,j] in Indices M2 ; ::_thesis: M2 * (i,j) < (M2 + M1) * (i,j) then M1 * (i,j) > 0 by A2, A1, Def1; then M2 * (i,j) < (M2 * (i,j)) + (M1 * (i,j)) by XREAL_1:29; hence M2 * (i,j) < (M2 + M1) * (i,j) by A3, MATRIXR1:25; ::_thesis: verum end; hence M2 is_less_than M2 + M1 by Def5; ::_thesis: verum end; theorem :: MATRIX10:67 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is Negative holds M1 + M2 is_less_than M2 proof let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is Negative holds M1 + M2 is_less_than M2 let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Negative implies M1 + M2 is_less_than M2 ) A1: ( Indices M1 = [:(Seg n),(Seg n):] & Indices (M1 + M2) = [:(Seg n),(Seg n):] ) by MATRIX_1:24; assume A2: M1 is Negative ; ::_thesis: M1 + M2 is_less_than M2 for i, j being Nat st [i,j] in Indices (M1 + M2) holds (M1 + M2) * (i,j) < M2 * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M2) implies (M1 + M2) * (i,j) < M2 * (i,j) ) assume A3: [i,j] in Indices (M1 + M2) ; ::_thesis: (M1 + M2) * (i,j) < M2 * (i,j) then M1 * (i,j) < 0 by A2, A1, Def2; then (M1 * (i,j)) + (M2 * (i,j)) < M2 * (i,j) by XREAL_1:30; hence (M1 + M2) * (i,j) < M2 * (i,j) by A1, A3, MATRIXR1:25; ::_thesis: verum end; hence M1 + M2 is_less_than M2 by Def5; ::_thesis: verum end; theorem :: MATRIX10:68 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is Nonnegative holds M2 is_less_or_equal_with M1 + M2 proof let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is Nonnegative holds M2 is_less_or_equal_with M1 + M2 let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Nonnegative implies M2 is_less_or_equal_with M1 + M2 ) A1: ( Indices M1 = [:(Seg n),(Seg n):] & Indices M2 = [:(Seg n),(Seg n):] ) by MATRIX_1:24; assume A2: M1 is Nonnegative ; ::_thesis: M2 is_less_or_equal_with M1 + M2 for i, j being Nat st [i,j] in Indices M2 holds M2 * (i,j) <= (M1 + M2) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices M2 implies M2 * (i,j) <= (M1 + M2) * (i,j) ) assume A3: [i,j] in Indices M2 ; ::_thesis: M2 * (i,j) <= (M1 + M2) * (i,j) then M1 * (i,j) >= 0 by A2, A1, Def4; then M2 * (i,j) <= (M1 * (i,j)) + (M2 * (i,j)) by XREAL_1:31; hence M2 * (i,j) <= (M1 + M2) * (i,j) by A1, A3, MATRIXR1:25; ::_thesis: verum end; hence M2 is_less_or_equal_with M1 + M2 by Def6; ::_thesis: verum end; theorem :: MATRIX10:69 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is Nonpositive holds M1 + M2 is_less_or_equal_with M2 proof let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is Nonpositive holds M1 + M2 is_less_or_equal_with M2 let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Nonpositive implies M1 + M2 is_less_or_equal_with M2 ) A1: ( Indices M1 = [:(Seg n),(Seg n):] & Indices (M1 + M2) = [:(Seg n),(Seg n):] ) by MATRIX_1:24; assume A2: M1 is Nonpositive ; ::_thesis: M1 + M2 is_less_or_equal_with M2 for i, j being Nat st [i,j] in Indices (M1 + M2) holds (M1 + M2) * (i,j) <= M2 * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M1 + M2) implies (M1 + M2) * (i,j) <= M2 * (i,j) ) assume A3: [i,j] in Indices (M1 + M2) ; ::_thesis: (M1 + M2) * (i,j) <= M2 * (i,j) then M1 * (i,j) <= 0 by A2, A1, Def3; then (M1 * (i,j)) + (M2 * (i,j)) <= M2 * (i,j) by XREAL_1:32; hence (M1 + M2) * (i,j) <= M2 * (i,j) by A1, A3, MATRIXR1:25; ::_thesis: verum end; hence M1 + M2 is_less_or_equal_with M2 by Def6; ::_thesis: verum end; theorem :: MATRIX10:70 for n being Nat for M1, M3, M2 being Matrix of n, REAL st M1 is Nonpositive & M3 is_less_or_equal_with M2 holds M3 + M1 is_less_or_equal_with M2 proof let n be Nat; ::_thesis: for M1, M3, M2 being Matrix of n, REAL st M1 is Nonpositive & M3 is_less_or_equal_with M2 holds M3 + M1 is_less_or_equal_with M2 let M1, M3, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Nonpositive & M3 is_less_or_equal_with M2 implies M3 + M1 is_less_or_equal_with M2 ) A1: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; A2: ( Indices M3 = [:(Seg n),(Seg n):] & Indices (M3 + M1) = [:(Seg n),(Seg n):] ) by MATRIX_1:24; assume A3: ( M1 is Nonpositive & M3 is_less_or_equal_with M2 ) ; ::_thesis: M3 + M1 is_less_or_equal_with M2 for i, j being Nat st [i,j] in Indices (M3 + M1) holds (M3 + M1) * (i,j) <= M2 * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M3 + M1) implies (M3 + M1) * (i,j) <= M2 * (i,j) ) assume A4: [i,j] in Indices (M3 + M1) ; ::_thesis: (M3 + M1) * (i,j) <= M2 * (i,j) then ( M1 * (i,j) <= 0 & M3 * (i,j) <= M2 * (i,j) ) by A3, A1, A2, Def3, Def6; then (M3 * (i,j)) + (M1 * (i,j)) <= M2 * (i,j) by XREAL_1:35; hence (M3 + M1) * (i,j) <= M2 * (i,j) by A2, A4, MATRIXR1:25; ::_thesis: verum end; hence M3 + M1 is_less_or_equal_with M2 by Def6; ::_thesis: verum end; theorem :: MATRIX10:71 for n being Nat for M1, M3, M2 being Matrix of n, REAL st M1 is Nonpositive & M3 is_less_than M2 holds M3 + M1 is_less_than M2 proof let n be Nat; ::_thesis: for M1, M3, M2 being Matrix of n, REAL st M1 is Nonpositive & M3 is_less_than M2 holds M3 + M1 is_less_than M2 let M1, M3, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Nonpositive & M3 is_less_than M2 implies M3 + M1 is_less_than M2 ) A1: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; A2: ( Indices M3 = [:(Seg n),(Seg n):] & Indices (M3 + M1) = [:(Seg n),(Seg n):] ) by MATRIX_1:24; assume A3: ( M1 is Nonpositive & M3 is_less_than M2 ) ; ::_thesis: M3 + M1 is_less_than M2 for i, j being Nat st [i,j] in Indices (M3 + M1) holds (M3 + M1) * (i,j) < M2 * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M3 + M1) implies (M3 + M1) * (i,j) < M2 * (i,j) ) assume A4: [i,j] in Indices (M3 + M1) ; ::_thesis: (M3 + M1) * (i,j) < M2 * (i,j) then ( M1 * (i,j) <= 0 & M3 * (i,j) < M2 * (i,j) ) by A3, A1, A2, Def3, Def5; then (M3 * (i,j)) + (M1 * (i,j)) < M2 * (i,j) by XREAL_1:36; hence (M3 + M1) * (i,j) < M2 * (i,j) by A2, A4, MATRIXR1:25; ::_thesis: verum end; hence M3 + M1 is_less_than M2 by Def5; ::_thesis: verum end; theorem :: MATRIX10:72 for n being Nat for M1, M3, M2 being Matrix of n, REAL st M1 is Negative & M3 is_less_or_equal_with M2 holds M3 + M1 is_less_than M2 proof let n be Nat; ::_thesis: for M1, M3, M2 being Matrix of n, REAL st M1 is Negative & M3 is_less_or_equal_with M2 holds M3 + M1 is_less_than M2 let M1, M3, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Negative & M3 is_less_or_equal_with M2 implies M3 + M1 is_less_than M2 ) A1: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; A2: ( Indices M3 = [:(Seg n),(Seg n):] & Indices (M3 + M1) = [:(Seg n),(Seg n):] ) by MATRIX_1:24; assume A3: ( M1 is Negative & M3 is_less_or_equal_with M2 ) ; ::_thesis: M3 + M1 is_less_than M2 for i, j being Nat st [i,j] in Indices (M3 + M1) holds (M3 + M1) * (i,j) < M2 * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M3 + M1) implies (M3 + M1) * (i,j) < M2 * (i,j) ) assume A4: [i,j] in Indices (M3 + M1) ; ::_thesis: (M3 + M1) * (i,j) < M2 * (i,j) then ( M1 * (i,j) < 0 & M3 * (i,j) <= M2 * (i,j) ) by A3, A1, A2, Def2, Def6; then (M3 * (i,j)) + (M1 * (i,j)) < M2 * (i,j) by XREAL_1:37; hence (M3 + M1) * (i,j) < M2 * (i,j) by A2, A4, MATRIXR1:25; ::_thesis: verum end; hence M3 + M1 is_less_than M2 by Def5; ::_thesis: verum end; theorem :: MATRIX10:73 for n being Nat for M1, M2, M3 being Matrix of n, REAL st M1 is Nonnegative & M2 is_less_or_equal_with M3 holds M2 is_less_or_equal_with M1 + M3 proof let n be Nat; ::_thesis: for M1, M2, M3 being Matrix of n, REAL st M1 is Nonnegative & M2 is_less_or_equal_with M3 holds M2 is_less_or_equal_with M1 + M3 let M1, M2, M3 be Matrix of n, REAL ; ::_thesis: ( M1 is Nonnegative & M2 is_less_or_equal_with M3 implies M2 is_less_or_equal_with M1 + M3 ) A1: ( Indices M1 = [:(Seg n),(Seg n):] & Indices M2 = [:(Seg n),(Seg n):] ) by MATRIX_1:24; assume A2: ( M1 is Nonnegative & M2 is_less_or_equal_with M3 ) ; ::_thesis: M2 is_less_or_equal_with M1 + M3 for i, j being Nat st [i,j] in Indices M2 holds M2 * (i,j) <= (M1 + M3) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices M2 implies M2 * (i,j) <= (M1 + M3) * (i,j) ) assume A3: [i,j] in Indices M2 ; ::_thesis: M2 * (i,j) <= (M1 + M3) * (i,j) then ( M1 * (i,j) >= 0 & M2 * (i,j) <= M3 * (i,j) ) by A2, A1, Def4, Def6; then M2 * (i,j) <= (M1 * (i,j)) + (M3 * (i,j)) by XREAL_1:38; hence M2 * (i,j) <= (M1 + M3) * (i,j) by A1, A3, MATRIXR1:25; ::_thesis: verum end; hence M2 is_less_or_equal_with M1 + M3 by Def6; ::_thesis: verum end; theorem :: MATRIX10:74 for n being Nat for M1, M2, M3 being Matrix of n, REAL st M1 is Positive & M2 is_less_or_equal_with M3 holds M2 is_less_than M1 + M3 proof let n be Nat; ::_thesis: for M1, M2, M3 being Matrix of n, REAL st M1 is Positive & M2 is_less_or_equal_with M3 holds M2 is_less_than M1 + M3 let M1, M2, M3 be Matrix of n, REAL ; ::_thesis: ( M1 is Positive & M2 is_less_or_equal_with M3 implies M2 is_less_than M1 + M3 ) A1: ( Indices M1 = [:(Seg n),(Seg n):] & Indices M2 = [:(Seg n),(Seg n):] ) by MATRIX_1:24; assume A2: ( M1 is Positive & M2 is_less_or_equal_with M3 ) ; ::_thesis: M2 is_less_than M1 + M3 for i, j being Nat st [i,j] in Indices M2 holds M2 * (i,j) < (M1 + M3) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices M2 implies M2 * (i,j) < (M1 + M3) * (i,j) ) assume A3: [i,j] in Indices M2 ; ::_thesis: M2 * (i,j) < (M1 + M3) * (i,j) then ( M1 * (i,j) > 0 & M2 * (i,j) <= M3 * (i,j) ) by A2, A1, Def1, Def6; then M2 * (i,j) < (M1 * (i,j)) + (M3 * (i,j)) by XREAL_1:39; hence M2 * (i,j) < (M1 + M3) * (i,j) by A1, A3, MATRIXR1:25; ::_thesis: verum end; hence M2 is_less_than M1 + M3 by Def5; ::_thesis: verum end; theorem :: MATRIX10:75 for n being Nat for M1, M2, M3 being Matrix of n, REAL st M1 is Nonnegative & M2 is_less_than M3 holds M2 is_less_than M1 + M3 proof let n be Nat; ::_thesis: for M1, M2, M3 being Matrix of n, REAL st M1 is Nonnegative & M2 is_less_than M3 holds M2 is_less_than M1 + M3 let M1, M2, M3 be Matrix of n, REAL ; ::_thesis: ( M1 is Nonnegative & M2 is_less_than M3 implies M2 is_less_than M1 + M3 ) A1: ( Indices M1 = [:(Seg n),(Seg n):] & Indices M2 = [:(Seg n),(Seg n):] ) by MATRIX_1:24; assume A2: ( M1 is Nonnegative & M2 is_less_than M3 ) ; ::_thesis: M2 is_less_than M1 + M3 for i, j being Nat st [i,j] in Indices M2 holds M2 * (i,j) < (M1 + M3) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices M2 implies M2 * (i,j) < (M1 + M3) * (i,j) ) assume A3: [i,j] in Indices M2 ; ::_thesis: M2 * (i,j) < (M1 + M3) * (i,j) then ( M1 * (i,j) >= 0 & M2 * (i,j) < M3 * (i,j) ) by A2, A1, Def4, Def5; then M2 * (i,j) < (M1 * (i,j)) + (M3 * (i,j)) by XREAL_1:40; hence M2 * (i,j) < (M1 + M3) * (i,j) by A1, A3, MATRIXR1:25; ::_thesis: verum end; hence M2 is_less_than M1 + M3 by Def5; ::_thesis: verum end; theorem :: MATRIX10:76 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is Nonnegative holds M2 - M1 is_less_or_equal_with M2 proof let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is Nonnegative holds M2 - M1 is_less_or_equal_with M2 let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Nonnegative implies M2 - M1 is_less_or_equal_with M2 ) assume A1: M1 is Nonnegative ; ::_thesis: M2 - M1 is_less_or_equal_with M2 A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; A3: width M1 = width M2 by Lm1; A4: Indices (M2 - M1) = [:(Seg n),(Seg n):] by MATRIX_1:24; A5: ( Indices M2 = [:(Seg n),(Seg n):] & len M1 = len M2 ) by Lm1, MATRIX_1:24; for i, j being Nat st [i,j] in Indices (M2 - M1) holds (M2 - M1) * (i,j) <= M2 * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M2 - M1) implies (M2 - M1) * (i,j) <= M2 * (i,j) ) assume A6: [i,j] in Indices (M2 - M1) ; ::_thesis: (M2 - M1) * (i,j) <= M2 * (i,j) then M1 * (i,j) >= 0 by A1, A2, A4, Def4; then (M2 * (i,j)) - (M1 * (i,j)) <= M2 * (i,j) by XREAL_1:43; hence (M2 - M1) * (i,j) <= M2 * (i,j) by A4, A5, A3, A6, Th3; ::_thesis: verum end; hence M2 - M1 is_less_or_equal_with M2 by Def6; ::_thesis: verum end; theorem :: MATRIX10:77 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is Positive holds M2 - M1 is_less_than M2 proof let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is Positive holds M2 - M1 is_less_than M2 let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Positive implies M2 - M1 is_less_than M2 ) assume A1: M1 is Positive ; ::_thesis: M2 - M1 is_less_than M2 A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; A3: width M1 = width M2 by Lm1; A4: Indices (M2 - M1) = [:(Seg n),(Seg n):] by MATRIX_1:24; A5: ( Indices M2 = [:(Seg n),(Seg n):] & len M1 = len M2 ) by Lm1, MATRIX_1:24; for i, j being Nat st [i,j] in Indices (M2 - M1) holds (M2 - M1) * (i,j) < M2 * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M2 - M1) implies (M2 - M1) * (i,j) < M2 * (i,j) ) assume A6: [i,j] in Indices (M2 - M1) ; ::_thesis: (M2 - M1) * (i,j) < M2 * (i,j) then M1 * (i,j) > 0 by A1, A2, A4, Def1; then (M2 * (i,j)) - (M1 * (i,j)) < M2 * (i,j) by XREAL_1:44; hence (M2 - M1) * (i,j) < M2 * (i,j) by A4, A5, A3, A6, Th3; ::_thesis: verum end; hence M2 - M1 is_less_than M2 by Def5; ::_thesis: verum end; theorem :: MATRIX10:78 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is Nonpositive holds M2 is_less_or_equal_with M2 - M1 proof let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is Nonpositive holds M2 is_less_or_equal_with M2 - M1 let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Nonpositive implies M2 is_less_or_equal_with M2 - M1 ) assume A1: M1 is Nonpositive ; ::_thesis: M2 is_less_or_equal_with M2 - M1 A2: ( Indices M1 = [:(Seg n),(Seg n):] & Indices M2 = [:(Seg n),(Seg n):] ) by MATRIX_1:24; A3: ( len M1 = len M2 & width M1 = width M2 ) by Lm1; for i, j being Nat st [i,j] in Indices M2 holds M2 * (i,j) <= (M2 - M1) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices M2 implies M2 * (i,j) <= (M2 - M1) * (i,j) ) assume A4: [i,j] in Indices M2 ; ::_thesis: M2 * (i,j) <= (M2 - M1) * (i,j) then M1 * (i,j) <= 0 by A1, A2, Def3; then M2 * (i,j) <= (M2 * (i,j)) - (M1 * (i,j)) by XREAL_1:45; hence M2 * (i,j) <= (M2 - M1) * (i,j) by A3, A4, Th3; ::_thesis: verum end; hence M2 is_less_or_equal_with M2 - M1 by Def6; ::_thesis: verum end; theorem :: MATRIX10:79 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is Negative holds M2 is_less_than M2 - M1 proof let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is Negative holds M2 is_less_than M2 - M1 let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is Negative implies M2 is_less_than M2 - M1 ) assume A1: M1 is Negative ; ::_thesis: M2 is_less_than M2 - M1 A2: ( Indices M1 = [:(Seg n),(Seg n):] & Indices M2 = [:(Seg n),(Seg n):] ) by MATRIX_1:24; A3: ( len M1 = len M2 & width M1 = width M2 ) by Lm1; for i, j being Nat st [i,j] in Indices M2 holds M2 * (i,j) < (M2 - M1) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices M2 implies M2 * (i,j) < (M2 - M1) * (i,j) ) assume A4: [i,j] in Indices M2 ; ::_thesis: M2 * (i,j) < (M2 - M1) * (i,j) then M1 * (i,j) < 0 by A1, A2, Def2; then M2 * (i,j) < (M2 * (i,j)) - (M1 * (i,j)) by XREAL_1:46; hence M2 * (i,j) < (M2 - M1) * (i,j) by A3, A4, Th3; ::_thesis: verum end; hence M2 is_less_than M2 - M1 by Def5; ::_thesis: verum end; theorem :: MATRIX10:80 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is_less_or_equal_with M2 holds M2 - M1 is Nonnegative proof let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is_less_or_equal_with M2 holds M2 - M1 is Nonnegative let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_or_equal_with M2 implies M2 - M1 is Nonnegative ) assume A1: M1 is_less_or_equal_with M2 ; ::_thesis: M2 - M1 is Nonnegative A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; A3: width M1 = width M2 by Lm1; A4: Indices (M2 - M1) = [:(Seg n),(Seg n):] by MATRIX_1:24; A5: ( Indices M2 = [:(Seg n),(Seg n):] & len M1 = len M2 ) by Lm1, MATRIX_1:24; for i, j being Nat st [i,j] in Indices (M2 - M1) holds (M2 - M1) * (i,j) >= 0 proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M2 - M1) implies (M2 - M1) * (i,j) >= 0 ) assume A6: [i,j] in Indices (M2 - M1) ; ::_thesis: (M2 - M1) * (i,j) >= 0 then M1 * (i,j) <= M2 * (i,j) by A1, A2, A4, Def6; then (M2 * (i,j)) - (M1 * (i,j)) >= 0 by XREAL_1:48; hence (M2 - M1) * (i,j) >= 0 by A4, A5, A3, A6, Th3; ::_thesis: verum end; hence M2 - M1 is Nonnegative by Def4; ::_thesis: verum end; theorem :: MATRIX10:81 for n being Nat for M1, M2, M3 being Matrix of n, REAL st M1 is Nonnegative & M2 is_less_than M3 holds M2 - M1 is_less_than M3 proof let n be Nat; ::_thesis: for M1, M2, M3 being Matrix of n, REAL st M1 is Nonnegative & M2 is_less_than M3 holds M2 - M1 is_less_than M3 let M1, M2, M3 be Matrix of n, REAL ; ::_thesis: ( M1 is Nonnegative & M2 is_less_than M3 implies M2 - M1 is_less_than M3 ) assume A1: ( M1 is Nonnegative & M2 is_less_than M3 ) ; ::_thesis: M2 - M1 is_less_than M3 A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; A3: ( Indices M2 = [:(Seg n),(Seg n):] & Indices (M2 - M1) = [:(Seg n),(Seg n):] ) by MATRIX_1:24; A4: ( len M1 = len M2 & width M1 = width M2 ) by Lm1; for i, j being Nat st [i,j] in Indices (M2 - M1) holds (M2 - M1) * (i,j) < M3 * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (M2 - M1) implies (M2 - M1) * (i,j) < M3 * (i,j) ) assume A5: [i,j] in Indices (M2 - M1) ; ::_thesis: (M2 - M1) * (i,j) < M3 * (i,j) then ( M1 * (i,j) >= 0 & M2 * (i,j) < M3 * (i,j) ) by A1, A2, A3, Def4, Def5; then (M2 * (i,j)) - (M1 * (i,j)) < M3 * (i,j) by XREAL_1:51; hence (M2 - M1) * (i,j) < M3 * (i,j) by A3, A4, A5, Th3; ::_thesis: verum end; hence M2 - M1 is_less_than M3 by Def5; ::_thesis: verum end; theorem :: MATRIX10:82 for n being Nat for M1, M2, M3 being Matrix of n, REAL st M1 is Nonpositive & M2 is_less_or_equal_with M3 holds M2 is_less_or_equal_with M3 - M1 proof let n be Nat; ::_thesis: for M1, M2, M3 being Matrix of n, REAL st M1 is Nonpositive & M2 is_less_or_equal_with M3 holds M2 is_less_or_equal_with M3 - M1 let M1, M2, M3 be Matrix of n, REAL ; ::_thesis: ( M1 is Nonpositive & M2 is_less_or_equal_with M3 implies M2 is_less_or_equal_with M3 - M1 ) assume A1: ( M1 is Nonpositive & M2 is_less_or_equal_with M3 ) ; ::_thesis: M2 is_less_or_equal_with M3 - M1 A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; A3: width M2 = width M3 by Lm1; A4: ( width M1 = width M2 & len M2 = len M3 ) by Lm1; A5: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24; A6: ( Indices M3 = [:(Seg n),(Seg n):] & len M1 = len M2 ) by Lm1, MATRIX_1:24; for i, j being Nat st [i,j] in Indices M2 holds M2 * (i,j) <= (M3 - M1) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices M2 implies M2 * (i,j) <= (M3 - M1) * (i,j) ) assume A7: [i,j] in Indices M2 ; ::_thesis: M2 * (i,j) <= (M3 - M1) * (i,j) then ( M1 * (i,j) <= 0 & M2 * (i,j) <= M3 * (i,j) ) by A1, A2, A5, Def3, Def6; then M2 * (i,j) <= (M3 * (i,j)) - (M1 * (i,j)) by XREAL_1:52; hence M2 * (i,j) <= (M3 - M1) * (i,j) by A5, A6, A4, A3, A7, Th3; ::_thesis: verum end; hence M2 is_less_or_equal_with M3 - M1 by Def6; ::_thesis: verum end; theorem :: MATRIX10:83 for n being Nat for M1, M2, M3 being Matrix of n, REAL st M1 is Nonpositive & M2 is_less_than M3 holds M2 is_less_than M3 - M1 proof let n be Nat; ::_thesis: for M1, M2, M3 being Matrix of n, REAL st M1 is Nonpositive & M2 is_less_than M3 holds M2 is_less_than M3 - M1 let M1, M2, M3 be Matrix of n, REAL ; ::_thesis: ( M1 is Nonpositive & M2 is_less_than M3 implies M2 is_less_than M3 - M1 ) assume A1: ( M1 is Nonpositive & M2 is_less_than M3 ) ; ::_thesis: M2 is_less_than M3 - M1 A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; A3: width M2 = width M3 by Lm1; A4: ( width M1 = width M2 & len M2 = len M3 ) by Lm1; A5: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24; A6: ( Indices M3 = [:(Seg n),(Seg n):] & len M1 = len M2 ) by Lm1, MATRIX_1:24; for i, j being Nat st [i,j] in Indices M2 holds M2 * (i,j) < (M3 - M1) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices M2 implies M2 * (i,j) < (M3 - M1) * (i,j) ) assume A7: [i,j] in Indices M2 ; ::_thesis: M2 * (i,j) < (M3 - M1) * (i,j) then ( M1 * (i,j) <= 0 & M2 * (i,j) < M3 * (i,j) ) by A1, A2, A5, Def3, Def5; then M2 * (i,j) < (M3 * (i,j)) - (M1 * (i,j)) by XREAL_1:53; hence M2 * (i,j) < (M3 - M1) * (i,j) by A5, A6, A4, A3, A7, Th3; ::_thesis: verum end; hence M2 is_less_than M3 - M1 by Def5; ::_thesis: verum end; theorem :: MATRIX10:84 for n being Nat for M1, M2, M3 being Matrix of n, REAL st M1 is Negative & M2 is_less_or_equal_with M3 holds M2 is_less_than M3 - M1 proof let n be Nat; ::_thesis: for M1, M2, M3 being Matrix of n, REAL st M1 is Negative & M2 is_less_or_equal_with M3 holds M2 is_less_than M3 - M1 let M1, M2, M3 be Matrix of n, REAL ; ::_thesis: ( M1 is Negative & M2 is_less_or_equal_with M3 implies M2 is_less_than M3 - M1 ) assume A1: ( M1 is Negative & M2 is_less_or_equal_with M3 ) ; ::_thesis: M2 is_less_than M3 - M1 A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; A3: width M2 = width M3 by Lm1; A4: ( width M1 = width M2 & len M2 = len M3 ) by Lm1; A5: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24; A6: ( Indices M3 = [:(Seg n),(Seg n):] & len M1 = len M2 ) by Lm1, MATRIX_1:24; for i, j being Nat st [i,j] in Indices M2 holds M2 * (i,j) < (M3 - M1) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices M2 implies M2 * (i,j) < (M3 - M1) * (i,j) ) assume A7: [i,j] in Indices M2 ; ::_thesis: M2 * (i,j) < (M3 - M1) * (i,j) then ( M1 * (i,j) < 0 & M2 * (i,j) <= M3 * (i,j) ) by A1, A2, A5, Def2, Def6; then M2 * (i,j) < (M3 * (i,j)) - (M1 * (i,j)) by XREAL_1:54; hence M2 * (i,j) < (M3 - M1) * (i,j) by A5, A6, A4, A3, A7, Th3; ::_thesis: verum end; hence M2 is_less_than M3 - M1 by Def5; ::_thesis: verum end; theorem :: MATRIX10:85 for a being Element of REAL for n being Nat for M1, M2 being Matrix of n, REAL st M1 is_less_than M2 & a > 0 holds a * M1 is_less_than a * M2 proof let a be Element of REAL ; ::_thesis: for n being Nat for M1, M2 being Matrix of n, REAL st M1 is_less_than M2 & a > 0 holds a * M1 is_less_than a * M2 let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is_less_than M2 & a > 0 holds a * M1 is_less_than a * M2 let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_than M2 & a > 0 implies a * M1 is_less_than a * M2 ) assume that A1: M1 is_less_than M2 and A2: a > 0 ; ::_thesis: a * M1 is_less_than a * M2 A3: Indices (a * M1) = Indices M1 by MATRIXR1:28; A4: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24; for i, j being Nat st [i,j] in Indices (a * M1) holds (a * M1) * (i,j) < (a * M2) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M1) implies (a * M1) * (i,j) < (a * M2) * (i,j) ) assume A5: [i,j] in Indices (a * M1) ; ::_thesis: (a * M1) * (i,j) < (a * M2) * (i,j) then M1 * (i,j) < M2 * (i,j) by A1, A3, Def5; then a * (M1 * (i,j)) < a * (M2 * (i,j)) by A2, XREAL_1:68; then A6: (a * M1) * (i,j) < a * (M2 * (i,j)) by A3, A5, Th4; [i,j] in Indices M2 by A4, A5, MATRIX_1:24; hence (a * M1) * (i,j) < (a * M2) * (i,j) by A6, Th4; ::_thesis: verum end; hence a * M1 is_less_than a * M2 by Def5; ::_thesis: verum end; theorem :: MATRIX10:86 for a being Element of REAL for n being Nat for M1, M2 being Matrix of n, REAL st M1 is_less_than M2 & a >= 0 holds a * M1 is_less_or_equal_with a * M2 proof let a be Element of REAL ; ::_thesis: for n being Nat for M1, M2 being Matrix of n, REAL st M1 is_less_than M2 & a >= 0 holds a * M1 is_less_or_equal_with a * M2 let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is_less_than M2 & a >= 0 holds a * M1 is_less_or_equal_with a * M2 let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_than M2 & a >= 0 implies a * M1 is_less_or_equal_with a * M2 ) assume that A1: M1 is_less_than M2 and A2: a >= 0 ; ::_thesis: a * M1 is_less_or_equal_with a * M2 A3: Indices (a * M1) = Indices M1 by MATRIXR1:28; A4: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24; for i, j being Nat st [i,j] in Indices (a * M1) holds (a * M1) * (i,j) <= (a * M2) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M1) implies (a * M1) * (i,j) <= (a * M2) * (i,j) ) assume A5: [i,j] in Indices (a * M1) ; ::_thesis: (a * M1) * (i,j) <= (a * M2) * (i,j) then M1 * (i,j) < M2 * (i,j) by A1, A3, Def5; then a * (M1 * (i,j)) <= a * (M2 * (i,j)) by A2, XREAL_1:64; then A6: (a * M1) * (i,j) <= a * (M2 * (i,j)) by A3, A5, Th4; [i,j] in Indices M2 by A4, A5, MATRIX_1:24; hence (a * M1) * (i,j) <= (a * M2) * (i,j) by A6, Th4; ::_thesis: verum end; hence a * M1 is_less_or_equal_with a * M2 by Def6; ::_thesis: verum end; theorem :: MATRIX10:87 for a being Element of REAL for n being Nat for M1, M2 being Matrix of n, REAL st M1 is_less_than M2 & a < 0 holds a * M2 is_less_than a * M1 proof let a be Element of REAL ; ::_thesis: for n being Nat for M1, M2 being Matrix of n, REAL st M1 is_less_than M2 & a < 0 holds a * M2 is_less_than a * M1 let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is_less_than M2 & a < 0 holds a * M2 is_less_than a * M1 let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_than M2 & a < 0 implies a * M2 is_less_than a * M1 ) assume that A1: M1 is_less_than M2 and A2: a < 0 ; ::_thesis: a * M2 is_less_than a * M1 A3: Indices (a * M2) = Indices M2 by MATRIXR1:28; A4: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; for i, j being Nat st [i,j] in Indices (a * M2) holds (a * M2) * (i,j) < (a * M1) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M2) implies (a * M2) * (i,j) < (a * M1) * (i,j) ) assume A5: [i,j] in Indices (a * M2) ; ::_thesis: (a * M2) * (i,j) < (a * M1) * (i,j) then A6: [i,j] in Indices M1 by A4, MATRIX_1:24; then M1 * (i,j) < M2 * (i,j) by A1, Def5; then a * (M2 * (i,j)) < a * (M1 * (i,j)) by A2, XREAL_1:69; then (a * M2) * (i,j) < a * (M1 * (i,j)) by A3, A5, Th4; hence (a * M2) * (i,j) < (a * M1) * (i,j) by A6, Th4; ::_thesis: verum end; hence a * M2 is_less_than a * M1 by Def5; ::_thesis: verum end; theorem :: MATRIX10:88 for a being Element of REAL for n being Nat for M1, M2 being Matrix of n, REAL st M1 is_less_than M2 & a <= 0 holds a * M2 is_less_or_equal_with a * M1 proof let a be Element of REAL ; ::_thesis: for n being Nat for M1, M2 being Matrix of n, REAL st M1 is_less_than M2 & a <= 0 holds a * M2 is_less_or_equal_with a * M1 let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is_less_than M2 & a <= 0 holds a * M2 is_less_or_equal_with a * M1 let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_than M2 & a <= 0 implies a * M2 is_less_or_equal_with a * M1 ) assume that A1: M1 is_less_than M2 and A2: a <= 0 ; ::_thesis: a * M2 is_less_or_equal_with a * M1 A3: Indices (a * M2) = Indices M2 by MATRIXR1:28; A4: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; for i, j being Nat st [i,j] in Indices (a * M2) holds (a * M2) * (i,j) <= (a * M1) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M2) implies (a * M2) * (i,j) <= (a * M1) * (i,j) ) assume A5: [i,j] in Indices (a * M2) ; ::_thesis: (a * M2) * (i,j) <= (a * M1) * (i,j) then A6: [i,j] in Indices M1 by A4, MATRIX_1:24; then M1 * (i,j) < M2 * (i,j) by A1, Def5; then a * (M2 * (i,j)) <= a * (M1 * (i,j)) by A2, XREAL_1:65; then (a * M2) * (i,j) <= a * (M1 * (i,j)) by A3, A5, Th4; hence (a * M2) * (i,j) <= (a * M1) * (i,j) by A6, Th4; ::_thesis: verum end; hence a * M2 is_less_or_equal_with a * M1 by Def6; ::_thesis: verum end; theorem :: MATRIX10:89 for a being Element of REAL for n being Nat for M1, M2 being Matrix of n, REAL st M1 is_less_or_equal_with M2 & a >= 0 holds a * M1 is_less_or_equal_with a * M2 proof let a be Element of REAL ; ::_thesis: for n being Nat for M1, M2 being Matrix of n, REAL st M1 is_less_or_equal_with M2 & a >= 0 holds a * M1 is_less_or_equal_with a * M2 let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is_less_or_equal_with M2 & a >= 0 holds a * M1 is_less_or_equal_with a * M2 let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_or_equal_with M2 & a >= 0 implies a * M1 is_less_or_equal_with a * M2 ) assume that A1: M1 is_less_or_equal_with M2 and A2: a >= 0 ; ::_thesis: a * M1 is_less_or_equal_with a * M2 A3: Indices (a * M1) = Indices M1 by MATRIXR1:28; A4: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_1:24; for i, j being Nat st [i,j] in Indices (a * M1) holds (a * M1) * (i,j) <= (a * M2) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M1) implies (a * M1) * (i,j) <= (a * M2) * (i,j) ) assume A5: [i,j] in Indices (a * M1) ; ::_thesis: (a * M1) * (i,j) <= (a * M2) * (i,j) then M1 * (i,j) <= M2 * (i,j) by A1, A3, Def6; then a * (M1 * (i,j)) <= a * (M2 * (i,j)) by A2, XREAL_1:64; then A6: (a * M1) * (i,j) <= a * (M2 * (i,j)) by A3, A5, Th4; [i,j] in Indices M2 by A4, A5, MATRIX_1:24; hence (a * M1) * (i,j) <= (a * M2) * (i,j) by A6, Th4; ::_thesis: verum end; hence a * M1 is_less_or_equal_with a * M2 by Def6; ::_thesis: verum end; theorem :: MATRIX10:90 for a being Element of REAL for n being Nat for M1, M2 being Matrix of n, REAL st M1 is_less_or_equal_with M2 & a <= 0 holds a * M2 is_less_or_equal_with a * M1 proof let a be Element of REAL ; ::_thesis: for n being Nat for M1, M2 being Matrix of n, REAL st M1 is_less_or_equal_with M2 & a <= 0 holds a * M2 is_less_or_equal_with a * M1 let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st M1 is_less_or_equal_with M2 & a <= 0 holds a * M2 is_less_or_equal_with a * M1 let M1, M2 be Matrix of n, REAL ; ::_thesis: ( M1 is_less_or_equal_with M2 & a <= 0 implies a * M2 is_less_or_equal_with a * M1 ) assume that A1: M1 is_less_or_equal_with M2 and A2: a <= 0 ; ::_thesis: a * M2 is_less_or_equal_with a * M1 A3: Indices (a * M2) = Indices M2 by MATRIXR1:28; A4: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; for i, j being Nat st [i,j] in Indices (a * M2) holds (a * M2) * (i,j) <= (a * M1) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M2) implies (a * M2) * (i,j) <= (a * M1) * (i,j) ) assume A5: [i,j] in Indices (a * M2) ; ::_thesis: (a * M2) * (i,j) <= (a * M1) * (i,j) then A6: [i,j] in Indices M1 by A4, MATRIX_1:24; then M1 * (i,j) <= M2 * (i,j) by A1, Def6; then a * (M2 * (i,j)) <= a * (M1 * (i,j)) by A2, XREAL_1:65; then (a * M2) * (i,j) <= a * (M1 * (i,j)) by A3, A5, Th4; hence (a * M2) * (i,j) <= (a * M1) * (i,j) by A6, Th4; ::_thesis: verum end; hence a * M2 is_less_or_equal_with a * M1 by Def6; ::_thesis: verum end; theorem :: MATRIX10:91 for a, b being Element of REAL for n being Nat for M1, M2 being Matrix of n, REAL st a >= 0 & a <= b & M1 is Nonnegative & M1 is_less_or_equal_with M2 holds a * M1 is_less_or_equal_with b * M2 proof let a, b be Element of REAL ; ::_thesis: for n being Nat for M1, M2 being Matrix of n, REAL st a >= 0 & a <= b & M1 is Nonnegative & M1 is_less_or_equal_with M2 holds a * M1 is_less_or_equal_with b * M2 let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st a >= 0 & a <= b & M1 is Nonnegative & M1 is_less_or_equal_with M2 holds a * M1 is_less_or_equal_with b * M2 let M1, M2 be Matrix of n, REAL ; ::_thesis: ( a >= 0 & a <= b & M1 is Nonnegative & M1 is_less_or_equal_with M2 implies a * M1 is_less_or_equal_with b * M2 ) assume that A1: ( a >= 0 & a <= b ) and A2: ( M1 is Nonnegative & M1 is_less_or_equal_with M2 ) ; ::_thesis: a * M1 is_less_or_equal_with b * M2 A3: Indices (a * M1) = Indices M1 by MATRIXR1:28; A4: ( Indices M1 = [:(Seg n),(Seg n):] & Indices M2 = [:(Seg n),(Seg n):] ) by MATRIX_1:24; for i, j being Nat st [i,j] in Indices (a * M1) holds (a * M1) * (i,j) <= (b * M2) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M1) implies (a * M1) * (i,j) <= (b * M2) * (i,j) ) assume A5: [i,j] in Indices (a * M1) ; ::_thesis: (a * M1) * (i,j) <= (b * M2) * (i,j) then ( M1 * (i,j) >= 0 & M1 * (i,j) <= M2 * (i,j) ) by A2, A3, Def4, Def6; then a * (M1 * (i,j)) <= b * (M2 * (i,j)) by A1, XREAL_1:66; then (a * M1) * (i,j) <= b * (M2 * (i,j)) by A3, A5, Th4; hence (a * M1) * (i,j) <= (b * M2) * (i,j) by A4, A3, A5, Th4; ::_thesis: verum end; hence a * M1 is_less_or_equal_with b * M2 by Def6; ::_thesis: verum end; theorem :: MATRIX10:92 for a, b being Element of REAL for n being Nat for M1, M2 being Matrix of n, REAL st a <= 0 & b <= a & M1 is Nonpositive & M2 is_less_or_equal_with M1 holds a * M1 is_less_or_equal_with b * M2 proof let a, b be Element of REAL ; ::_thesis: for n being Nat for M1, M2 being Matrix of n, REAL st a <= 0 & b <= a & M1 is Nonpositive & M2 is_less_or_equal_with M1 holds a * M1 is_less_or_equal_with b * M2 let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st a <= 0 & b <= a & M1 is Nonpositive & M2 is_less_or_equal_with M1 holds a * M1 is_less_or_equal_with b * M2 let M1, M2 be Matrix of n, REAL ; ::_thesis: ( a <= 0 & b <= a & M1 is Nonpositive & M2 is_less_or_equal_with M1 implies a * M1 is_less_or_equal_with b * M2 ) assume that A1: ( a <= 0 & b <= a ) and A2: ( M1 is Nonpositive & M2 is_less_or_equal_with M1 ) ; ::_thesis: a * M1 is_less_or_equal_with b * M2 A3: Indices (a * M1) = Indices M1 by MATRIXR1:28; A4: ( Indices M1 = [:(Seg n),(Seg n):] & Indices M2 = [:(Seg n),(Seg n):] ) by MATRIX_1:24; for i, j being Nat st [i,j] in Indices (a * M1) holds (a * M1) * (i,j) <= (b * M2) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M1) implies (a * M1) * (i,j) <= (b * M2) * (i,j) ) assume A5: [i,j] in Indices (a * M1) ; ::_thesis: (a * M1) * (i,j) <= (b * M2) * (i,j) then ( M1 * (i,j) <= 0 & M2 * (i,j) <= M1 * (i,j) ) by A2, A4, A3, Def3, Def6; then a * (M1 * (i,j)) <= b * (M2 * (i,j)) by A1, XREAL_1:67; then (a * M1) * (i,j) <= b * (M2 * (i,j)) by A3, A5, Th4; hence (a * M1) * (i,j) <= (b * M2) * (i,j) by A4, A3, A5, Th4; ::_thesis: verum end; hence a * M1 is_less_or_equal_with b * M2 by Def6; ::_thesis: verum end; theorem :: MATRIX10:93 for a, b being Element of REAL for n being Nat for M1, M2 being Matrix of n, REAL st a < 0 & b <= a & M1 is Negative & M2 is_less_than M1 holds a * M1 is_less_than b * M2 proof let a, b be Element of REAL ; ::_thesis: for n being Nat for M1, M2 being Matrix of n, REAL st a < 0 & b <= a & M1 is Negative & M2 is_less_than M1 holds a * M1 is_less_than b * M2 let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st a < 0 & b <= a & M1 is Negative & M2 is_less_than M1 holds a * M1 is_less_than b * M2 let M1, M2 be Matrix of n, REAL ; ::_thesis: ( a < 0 & b <= a & M1 is Negative & M2 is_less_than M1 implies a * M1 is_less_than b * M2 ) assume that A1: ( a < 0 & b <= a ) and A2: ( M1 is Negative & M2 is_less_than M1 ) ; ::_thesis: a * M1 is_less_than b * M2 A3: Indices (a * M1) = Indices M1 by MATRIXR1:28; A4: ( Indices M1 = [:(Seg n),(Seg n):] & Indices M2 = [:(Seg n),(Seg n):] ) by MATRIX_1:24; for i, j being Nat st [i,j] in Indices (a * M1) holds (a * M1) * (i,j) < (b * M2) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M1) implies (a * M1) * (i,j) < (b * M2) * (i,j) ) assume A5: [i,j] in Indices (a * M1) ; ::_thesis: (a * M1) * (i,j) < (b * M2) * (i,j) then ( M1 * (i,j) < 0 & M2 * (i,j) < M1 * (i,j) ) by A2, A4, A3, Def2, Def5; then a * (M1 * (i,j)) < b * (M2 * (i,j)) by A1, XREAL_1:70; then (a * M1) * (i,j) < b * (M2 * (i,j)) by A3, A5, Th4; hence (a * M1) * (i,j) < (b * M2) * (i,j) by A4, A3, A5, Th4; ::_thesis: verum end; hence a * M1 is_less_than b * M2 by Def5; ::_thesis: verum end; theorem :: MATRIX10:94 for a, b being Element of REAL for n being Nat for M1, M2 being Matrix of n, REAL st a >= 0 & a < b & M1 is Nonnegative & M1 is_less_than M2 holds a * M1 is_less_than b * M2 proof let a, b be Element of REAL ; ::_thesis: for n being Nat for M1, M2 being Matrix of n, REAL st a >= 0 & a < b & M1 is Nonnegative & M1 is_less_than M2 holds a * M1 is_less_than b * M2 let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st a >= 0 & a < b & M1 is Nonnegative & M1 is_less_than M2 holds a * M1 is_less_than b * M2 let M1, M2 be Matrix of n, REAL ; ::_thesis: ( a >= 0 & a < b & M1 is Nonnegative & M1 is_less_than M2 implies a * M1 is_less_than b * M2 ) assume that A1: ( a >= 0 & a < b ) and A2: ( M1 is Nonnegative & M1 is_less_than M2 ) ; ::_thesis: a * M1 is_less_than b * M2 A3: Indices (a * M1) = Indices M1 by MATRIXR1:28; A4: ( Indices M1 = [:(Seg n),(Seg n):] & Indices M2 = [:(Seg n),(Seg n):] ) by MATRIX_1:24; for i, j being Nat st [i,j] in Indices (a * M1) holds (a * M1) * (i,j) < (b * M2) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M1) implies (a * M1) * (i,j) < (b * M2) * (i,j) ) assume A5: [i,j] in Indices (a * M1) ; ::_thesis: (a * M1) * (i,j) < (b * M2) * (i,j) then ( M1 * (i,j) >= 0 & M1 * (i,j) < M2 * (i,j) ) by A2, A3, Def4, Def5; then a * (M1 * (i,j)) < b * (M2 * (i,j)) by A1, XREAL_1:96; then (a * M1) * (i,j) < b * (M2 * (i,j)) by A3, A5, Th4; hence (a * M1) * (i,j) < (b * M2) * (i,j) by A4, A3, A5, Th4; ::_thesis: verum end; hence a * M1 is_less_than b * M2 by Def5; ::_thesis: verum end; theorem :: MATRIX10:95 for a, b being Element of REAL for n being Nat for M1, M2 being Matrix of n, REAL st a >= 0 & a < b & M1 is Positive & M1 is_less_or_equal_with M2 holds a * M1 is_less_than b * M2 proof let a, b be Element of REAL ; ::_thesis: for n being Nat for M1, M2 being Matrix of n, REAL st a >= 0 & a < b & M1 is Positive & M1 is_less_or_equal_with M2 holds a * M1 is_less_than b * M2 let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st a >= 0 & a < b & M1 is Positive & M1 is_less_or_equal_with M2 holds a * M1 is_less_than b * M2 let M1, M2 be Matrix of n, REAL ; ::_thesis: ( a >= 0 & a < b & M1 is Positive & M1 is_less_or_equal_with M2 implies a * M1 is_less_than b * M2 ) assume that A1: ( a >= 0 & a < b ) and A2: ( M1 is Positive & M1 is_less_or_equal_with M2 ) ; ::_thesis: a * M1 is_less_than b * M2 A3: Indices (a * M1) = Indices M1 by MATRIXR1:28; A4: ( Indices M1 = [:(Seg n),(Seg n):] & Indices M2 = [:(Seg n),(Seg n):] ) by MATRIX_1:24; for i, j being Nat st [i,j] in Indices (a * M1) holds (a * M1) * (i,j) < (b * M2) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M1) implies (a * M1) * (i,j) < (b * M2) * (i,j) ) assume A5: [i,j] in Indices (a * M1) ; ::_thesis: (a * M1) * (i,j) < (b * M2) * (i,j) then ( M1 * (i,j) > 0 & M1 * (i,j) <= M2 * (i,j) ) by A2, A3, Def1, Def6; then a * (M1 * (i,j)) < b * (M2 * (i,j)) by A1, XREAL_1:97; then (a * M1) * (i,j) < b * (M2 * (i,j)) by A3, A5, Th4; hence (a * M1) * (i,j) < (b * M2) * (i,j) by A4, A3, A5, Th4; ::_thesis: verum end; hence a * M1 is_less_than b * M2 by Def5; ::_thesis: verum end; theorem :: MATRIX10:96 for a, b being Element of REAL for n being Nat for M1, M2 being Matrix of n, REAL st a > 0 & a <= b & M1 is Positive & M1 is_less_than M2 holds a * M1 is_less_than b * M2 proof let a, b be Element of REAL ; ::_thesis: for n being Nat for M1, M2 being Matrix of n, REAL st a > 0 & a <= b & M1 is Positive & M1 is_less_than M2 holds a * M1 is_less_than b * M2 let n be Nat; ::_thesis: for M1, M2 being Matrix of n, REAL st a > 0 & a <= b & M1 is Positive & M1 is_less_than M2 holds a * M1 is_less_than b * M2 let M1, M2 be Matrix of n, REAL ; ::_thesis: ( a > 0 & a <= b & M1 is Positive & M1 is_less_than M2 implies a * M1 is_less_than b * M2 ) assume that A1: ( a > 0 & a <= b ) and A2: ( M1 is Positive & M1 is_less_than M2 ) ; ::_thesis: a * M1 is_less_than b * M2 A3: Indices (a * M1) = Indices M1 by MATRIXR1:28; A4: ( Indices M1 = [:(Seg n),(Seg n):] & Indices M2 = [:(Seg n),(Seg n):] ) by MATRIX_1:24; for i, j being Nat st [i,j] in Indices (a * M1) holds (a * M1) * (i,j) < (b * M2) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * M1) implies (a * M1) * (i,j) < (b * M2) * (i,j) ) assume A5: [i,j] in Indices (a * M1) ; ::_thesis: (a * M1) * (i,j) < (b * M2) * (i,j) then ( M1 * (i,j) > 0 & M1 * (i,j) < M2 * (i,j) ) by A2, A3, Def1, Def5; then a * (M1 * (i,j)) < b * (M2 * (i,j)) by A1, XREAL_1:98; then (a * M1) * (i,j) < b * (M2 * (i,j)) by A3, A5, Th4; hence (a * M1) * (i,j) < (b * M2) * (i,j) by A4, A3, A5, Th4; ::_thesis: verum end; hence a * M1 is_less_than b * M2 by Def5; ::_thesis: verum end;