:: MATRIX_4 semantic presentation begin definition let K be Field; let M1, M2 be Matrix of K; funcM1 - M2 -> Matrix of K equals :: MATRIX_4:def 1 M1 + (- M2); coherence M1 + (- M2) is Matrix of K ; end; :: deftheorem defines - MATRIX_4:def_1_:_ for K being Field for M1, M2 being Matrix of K holds M1 - M2 = M1 + (- M2); theorem Th1: :: MATRIX_4:1 for K being Field for M being Matrix of K holds - (- M) = M proof let K be Field; ::_thesis: for M being Matrix of K holds - (- M) = M let M be Matrix of K; ::_thesis: - (- M) = M percases ( len M = 0 or len M > 0 ) by NAT_1:3; supposeA1: len M = 0 ; ::_thesis: - (- M) = M then len (- M) = 0 by MATRIX_3:def_2; then len (- (- M)) = 0 by MATRIX_3:def_2; hence - (- M) = M by A1, CARD_2:64; ::_thesis: verum end; supposeA2: len M > 0 ; ::_thesis: - (- M) = M ( len (- M) = len M & width (- M) = width M ) by MATRIX_3:def_2; then A3: - M is Matrix of len M, width M,K by A2, MATRIX_1:20; M is Matrix of len M, width M,K by A2, MATRIX_1:20; then A4: Indices (- M) = Indices M by A3, MATRIX_1:26; A5: for i, j being Nat st [i,j] in Indices M holds M * (i,j) = (- (- M)) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices M implies M * (i,j) = (- (- M)) * (i,j) ) assume A6: [i,j] in Indices M ; ::_thesis: M * (i,j) = (- (- M)) * (i,j) then (- M) * (i,j) = - (M * (i,j)) by MATRIX_3:def_2; then (- (- M)) * (i,j) = - (- (M * (i,j))) by A4, A6, MATRIX_3:def_2; hence M * (i,j) = (- (- M)) * (i,j) by RLVECT_1:17; ::_thesis: verum end; width (- (- M)) = width (- M) by MATRIX_3:def_2; then A7: width (- (- M)) = width M by MATRIX_3:def_2; len (- (- M)) = len (- M) by MATRIX_3:def_2; then len (- (- M)) = len M by MATRIX_3:def_2; hence - (- M) = M by A7, A5, MATRIX_1:21; ::_thesis: verum end; end; end; theorem Th2: :: MATRIX_4:2 for K being Field for M being Matrix of K holds M + (- M) = 0. (K,(len M),(width M)) proof let K be Field; ::_thesis: for M being Matrix of K holds M + (- M) = 0. (K,(len M),(width M)) let M be Matrix of K; ::_thesis: M + (- M) = 0. (K,(len M),(width M)) percases ( len M > 0 or len M = 0 ) by NAT_1:3; suppose len M > 0 ; ::_thesis: M + (- M) = 0. (K,(len M),(width M)) then M is Matrix of len M, width M,K by MATRIX_1:20; hence M + (- M) = 0. (K,(len M),(width M)) by MATRIX_3:5; ::_thesis: verum end; supposeA1: len M = 0 ; ::_thesis: M + (- M) = 0. (K,(len M),(width M)) A2: len (M + (- M)) = len M by MATRIX_3:def_3; len (0. (K,(len M),(width M))) = 0 by A1; hence M + (- M) = 0. (K,(len M),(width M)) by A1, A2, CARD_2:64; ::_thesis: verum end; end; end; theorem :: MATRIX_4:3 for K being Field for M being Matrix of K holds M - M = 0. (K,(len M),(width M)) by Th2; theorem :: MATRIX_4:4 for K being Field for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 & M1 + M3 = M2 + M3 holds M1 = M2 proof let K be Field; ::_thesis: for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 & M1 + M3 = M2 + M3 holds M1 = M2 let M1, M2, M3 be Matrix of K; ::_thesis: ( len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 & M1 + M3 = M2 + M3 implies M1 = M2 ) assume that A1: len M1 = len M2 and A2: len M2 = len M3 and A3: width M1 = width M2 and A4: width M2 = width M3 and A5: M1 + M3 = M2 + M3 ; ::_thesis: M1 = M2 A6: M3 + (- M3) = 0. (K,(len M1),(width M1)) by A1, A2, A3, A4, Th2; M1 + (M3 + (- M3)) = (M2 + M3) + (- M3) by A1, A2, A3, A4, A5, MATRIX_3:3; then A7: M1 + (M3 + (- M3)) = M2 + (M3 + (- M3)) by A2, A4, MATRIX_3:3; percases ( len M1 > 0 or len M1 = 0 ) by NAT_1:3; supposeA8: len M1 > 0 ; ::_thesis: M1 = M2 then M2 is Matrix of len M1, width M1,K by A1, A3, MATRIX_1:20; then A9: M2 + (0. (K,(len M1),(width M1))) = M2 by MATRIX_3:4; M1 is Matrix of len M1, width M1,K by A8, MATRIX_1:20; hence M1 = M2 by A7, A6, A9, MATRIX_3:4; ::_thesis: verum end; suppose len M1 = 0 ; ::_thesis: M1 = M2 hence M1 = M2 by A1, CARD_2:64; ::_thesis: verum end; end; end; theorem :: MATRIX_4:5 for K being Field for M1, M2 being Matrix of K holds M1 - (- M2) = M1 + M2 by Th1; theorem :: MATRIX_4:6 for K being Field for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 & M1 = M1 + M2 holds M2 = 0. (K,(len M1),(width M1)) proof let K be Field; ::_thesis: for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 & M1 = M1 + M2 holds M2 = 0. (K,(len M1),(width M1)) let M1, M2 be Matrix of K; ::_thesis: ( len M1 = len M2 & width M1 = width M2 & M1 = M1 + M2 implies M2 = 0. (K,(len M1),(width M1)) ) assume that A1: len M1 = len M2 and A2: width M1 = width M2 and A3: M1 = M1 + M2 ; ::_thesis: M2 = 0. (K,(len M1),(width M1)) 0. (K,(len M1),(width M1)) = (M1 + M2) + (- M1) by A3, Th2; then 0. (K,(len M1),(width M1)) = (M2 + M1) + (- M1) by A1, A2, MATRIX_3:2; then 0. (K,(len M1),(width M1)) = M2 + (M1 + (- M1)) by A1, A2, MATRIX_3:3; then A4: 0. (K,(len M1),(width M1)) = M2 + (0. (K,(len M1),(width M1))) by Th2; percases ( len M1 > 0 or len M1 = 0 ) by NAT_1:3; suppose len M1 > 0 ; ::_thesis: M2 = 0. (K,(len M1),(width M1)) then M2 is Matrix of len M1, width M1,K by A1, A2, MATRIX_1:20; hence M2 = 0. (K,(len M1),(width M1)) by A4, MATRIX_3:4; ::_thesis: verum end; supposeA5: len M1 = 0 ; ::_thesis: M2 = 0. (K,(len M1),(width M1)) then len (0. (K,(len M1),(width M1))) = 0 ; hence M2 = 0. (K,(len M1),(width M1)) by A1, A5, CARD_2:64; ::_thesis: verum end; end; end; theorem Th7: :: MATRIX_4:7 for K being Field for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 & M1 - M2 = 0. (K,(len M1),(width M1)) holds M1 = M2 proof let K be Field; ::_thesis: for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 & M1 - M2 = 0. (K,(len M1),(width M1)) holds M1 = M2 let M1, M2 be Matrix of K; ::_thesis: ( len M1 = len M2 & width M1 = width M2 & M1 - M2 = 0. (K,(len M1),(width M1)) implies M1 = M2 ) assume that A1: len M1 = len M2 and A2: width M1 = width M2 and A3: M1 - M2 = 0. (K,(len M1),(width M1)) ; ::_thesis: M1 = M2 percases ( len M1 > 0 or len M1 = 0 ) by NAT_1:3; supposeA4: len M1 > 0 ; ::_thesis: M1 = M2 then A5: M2 is Matrix of len M1, width M1,K by A1, A2, MATRIX_1:20; A6: ( len (- M2) = len M2 & width (- M2) = width M2 ) by MATRIX_3:def_2; A7: len (0. (K,(len M1),(width M1))) = len M1 by MATRIX_1:def_2; then width (0. (K,(len M1),(width M1))) = width M1 by A4, MATRIX_1:20; then (M1 + (- M2)) + M2 = M2 + (0. (K,(len M1),(width M1))) by A1, A2, A3, A7, MATRIX_3:2 .= M2 by A5, MATRIX_3:4 ; then M1 + ((- M2) + M2) = M2 by A1, A2, A6, MATRIX_3:3; then M1 + (M2 + (- M2)) = M2 by A6, MATRIX_3:2; then A8: M1 + (0. (K,(len M1),(width M1))) = M2 by A5, MATRIX_3:5; M1 is Matrix of len M1, width M1,K by A4, MATRIX_1:20; hence M1 = M2 by A8, MATRIX_3:4; ::_thesis: verum end; suppose len M1 = 0 ; ::_thesis: M1 = M2 hence M1 = M2 by A1, CARD_2:64; ::_thesis: verum end; end; end; theorem Th8: :: MATRIX_4:8 for K being Field for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 & M1 + M2 = 0. (K,(len M1),(width M1)) holds M2 = - M1 proof let K be Field; ::_thesis: for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 & M1 + M2 = 0. (K,(len M1),(width M1)) holds M2 = - M1 let M1, M2 be Matrix of K; ::_thesis: ( len M1 = len M2 & width M1 = width M2 & M1 + M2 = 0. (K,(len M1),(width M1)) implies M2 = - M1 ) assume that A1: ( len M1 = len M2 & width M1 = width M2 ) and A2: M1 + M2 = 0. (K,(len M1),(width M1)) ; ::_thesis: M2 = - M1 A3: ( len (- M2) = len M2 & width (- M2) = width M2 ) by MATRIX_3:def_2; M1 - (- M2) = 0. (K,(len M1),(width M1)) by A2, Th1; then M1 = - M2 by A1, A3, Th7; hence M2 = - M1 by Th1; ::_thesis: verum end; theorem Th9: :: MATRIX_4:9 for n, m being Element of NAT for K being Field holds - (0. (K,n,m)) = 0. (K,n,m) proof let n, m be Element of NAT ; ::_thesis: for K being Field holds - (0. (K,n,m)) = 0. (K,n,m) let K be Field; ::_thesis: - (0. (K,n,m)) = 0. (K,n,m) percases ( n > 0 or n = 0 ) by NAT_1:3; supposeA1: n > 0 ; ::_thesis: - (0. (K,n,m)) = 0. (K,n,m) A2: (0. (K,n,m)) + (0. (K,n,m)) = 0. (K,n,m) by MATRIX_3:4; A3: len (0. (K,n,m)) = n by MATRIX_1:def_2; then width (0. (K,n,m)) = m by A1, MATRIX_1:20; hence - (0. (K,n,m)) = 0. (K,n,m) by A3, A2, Th8; ::_thesis: verum end; suppose n = 0 ; ::_thesis: - (0. (K,n,m)) = 0. (K,n,m) then A4: len (0. (K,n,m)) = 0 ; then len (- (0. (K,n,m))) = 0 by MATRIX_3:def_2; hence - (0. (K,n,m)) = 0. (K,n,m) by A4, CARD_2:64; ::_thesis: verum end; end; end; theorem :: MATRIX_4:10 for K being Field for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 & M2 - M1 = M2 holds M1 = 0. (K,(len M1),(width M1)) proof let K be Field; ::_thesis: for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 & M2 - M1 = M2 holds M1 = 0. (K,(len M1),(width M1)) let M1, M2 be Matrix of K; ::_thesis: ( len M1 = len M2 & width M1 = width M2 & M2 - M1 = M2 implies M1 = 0. (K,(len M1),(width M1)) ) assume that A1: ( len M1 = len M2 & width M1 = width M2 ) and A2: M2 - M1 = M2 ; ::_thesis: M1 = 0. (K,(len M1),(width M1)) percases ( len M1 > 0 or len M1 = 0 ) by NAT_1:3; supposeA3: len M1 > 0 ; ::_thesis: M1 = 0. (K,(len M1),(width M1)) A4: ( len (- M1) = len M1 & width (- M1) = width M1 ) by MATRIX_3:def_2; A5: M2 is Matrix of len M1, width M1,K by A1, A3, MATRIX_1:20; then (M2 + (- M1)) + (- M2) = 0. (K,(len M1),(width M1)) by A2, MATRIX_3:5; then ((- M1) + M2) + (- M2) = 0. (K,(len M1),(width M1)) by A1, A4, MATRIX_3:2; then (- M1) + (M2 + (- M2)) = 0. (K,(len M1),(width M1)) by A1, A4, MATRIX_3:3; then A6: (- M1) + (0. (K,(len M1),(width M1))) = 0. (K,(len M1),(width M1)) by A5, MATRIX_3:5; - M1 is Matrix of len M1, width M1,K by A3, A4, MATRIX_1:20; then - M1 = 0. (K,(len M1),(width M1)) by A6, MATRIX_3:4; then M1 = - (0. (K,(len M1),(width M1))) by Th1; hence M1 = 0. (K,(len M1),(width M1)) by Th9; ::_thesis: verum end; supposeA7: len M1 = 0 ; ::_thesis: M1 = 0. (K,(len M1),(width M1)) then len (0. (K,(len M1),(width M1))) = 0 ; hence M1 = 0. (K,(len M1),(width M1)) by A7, CARD_2:64; ::_thesis: verum end; end; end; theorem Th11: :: MATRIX_4:11 for K being Field for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds M1 = M1 - (M2 - M2) proof let K be Field; ::_thesis: for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds M1 = M1 - (M2 - M2) let M1, M2 be Matrix of K; ::_thesis: ( len M1 = len M2 & width M1 = width M2 implies M1 = M1 - (M2 - M2) ) assume ( len M1 = len M2 & width M1 = width M2 ) ; ::_thesis: M1 = M1 - (M2 - M2) then A1: M1 - (M2 - M2) = M1 - (0. (K,(len M1),(width M1))) by Th2 .= M1 + (0. (K,(len M1),(width M1))) by Th9 ; percases ( len M1 > 0 or len M1 = 0 ) by NAT_1:3; suppose len M1 > 0 ; ::_thesis: M1 = M1 - (M2 - M2) then M1 is Matrix of len M1, width M1,K by MATRIX_1:20; hence M1 = M1 - (M2 - M2) by A1, MATRIX_3:4; ::_thesis: verum end; supposeA2: len M1 = 0 ; ::_thesis: M1 = M1 - (M2 - M2) then len (M1 - (M2 - M2)) = 0 by MATRIX_3:def_3; hence M1 = M1 - (M2 - M2) by A2, CARD_2:64; ::_thesis: verum end; end; end; theorem Th12: :: MATRIX_4:12 for K being Field for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds - (M1 + M2) = (- M1) + (- M2) proof let K be Field; ::_thesis: for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds - (M1 + M2) = (- M1) + (- M2) let M1, M2 be Matrix of K; ::_thesis: ( len M1 = len M2 & width M1 = width M2 implies - (M1 + M2) = (- M1) + (- M2) ) assume A1: ( len M1 = len M2 & width M1 = width M2 ) ; ::_thesis: - (M1 + M2) = (- M1) + (- M2) A2: width (- M1) = width M1 by MATRIX_3:def_2; then A3: width ((- M1) + (- M2)) = width M1 by MATRIX_3:def_3; A4: ( len (M1 + M2) = len M1 & width (M1 + M2) = width M1 ) by MATRIX_3:def_3; A5: len (- M1) = len M1 by MATRIX_3:def_2; then A6: len ((- M1) + (- M2)) = len M1 by MATRIX_3:def_3; A7: ( len (- M2) = len M2 & width (- M2) = width M2 ) by MATRIX_3:def_2; percases ( len M1 > 0 or len M1 = 0 ) by NAT_1:3; supposeA8: len M1 > 0 ; ::_thesis: - (M1 + M2) = (- M1) + (- M2) then A9: M2 is Matrix of len M1, width M1,K by A1, MATRIX_1:20; A10: M1 is Matrix of len M1, width M1,K by A8, MATRIX_1:20; (M1 + M2) + ((- M1) + (- M2)) = (M1 + M2) + ((- M2) + (- M1)) by A1, A5, A2, A7, MATRIX_3:2 .= ((M1 + M2) + (- M2)) + (- M1) by A1, A7, A4, MATRIX_3:3 .= (M1 + (M2 + (- M2))) + (- M1) by A1, MATRIX_3:3 .= (M1 + (0. (K,(len M1),(width M1)))) + (- M1) by A9, MATRIX_3:5 .= M1 + (- M1) by A10, MATRIX_3:4 .= 0. (K,(len M1),(width M1)) by A10, MATRIX_3:5 ; hence - (M1 + M2) = (- M1) + (- M2) by A4, A6, A3, Th8; ::_thesis: verum end; supposeA11: len M1 = 0 ; ::_thesis: - (M1 + M2) = (- M1) + (- M2) then len (- M1) = 0 by MATRIX_3:def_2; then A12: len ((- M1) + (- M2)) = 0 by MATRIX_3:def_3; len (M1 + M2) = 0 by A11, MATRIX_3:def_3; then len (- (M1 + M2)) = 0 by MATRIX_3:def_2; hence - (M1 + M2) = (- M1) + (- M2) by A12, CARD_2:64; ::_thesis: verum end; end; end; theorem :: MATRIX_4:13 for K being Field for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds M1 - (M1 - M2) = M2 proof let K be Field; ::_thesis: for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds M1 - (M1 - M2) = M2 let M1, M2 be Matrix of K; ::_thesis: ( len M1 = len M2 & width M1 = width M2 implies M1 - (M1 - M2) = M2 ) assume that A1: len M1 = len M2 and A2: width M1 = width M2 ; ::_thesis: M1 - (M1 - M2) = M2 A3: ( len (- M1) = len M1 & width (- M1) = width M1 ) by MATRIX_3:def_2; A4: ( len (- M2) = len M2 & width (- M2) = width M2 ) by MATRIX_3:def_2; percases ( len M1 > 0 or len M1 = 0 ) by NAT_1:3; supposeA5: len M1 > 0 ; ::_thesis: M1 - (M1 - M2) = M2 A6: len (0. (K,(len M1),(width M1))) = len M1 by MATRIX_1:def_2; then A7: width (0. (K,(len M1),(width M1))) = width M1 by A5, MATRIX_1:20; A8: M2 is Matrix of len M1, width M1,K by A1, A2, A5, MATRIX_1:20; A9: M1 is Matrix of len M1, width M1,K by A5, MATRIX_1:20; M1 - (M1 - M2) = M1 + ((- M1) + (- (- M2))) by A1, A2, A4, Th12 .= M1 + ((- M1) + M2) by Th1 .= (M1 + (- M1)) + M2 by A3, MATRIX_3:3 .= (0. (K,(len M1),(width M1))) + M2 by A9, MATRIX_3:5 .= M2 + (0. (K,(len M1),(width M1))) by A1, A2, A6, A7, MATRIX_3:2 .= M2 by A8, MATRIX_3:4 ; hence M1 - (M1 - M2) = M2 ; ::_thesis: verum end; supposeA10: len M1 = 0 ; ::_thesis: M1 - (M1 - M2) = M2 then len (M1 - (M1 - M2)) = 0 by MATRIX_3:def_3; hence M1 - (M1 - M2) = M2 by A1, A10, CARD_2:64; ::_thesis: verum end; end; end; theorem Th14: :: MATRIX_4:14 for K being Field for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 & M1 - M3 = M2 - M3 holds M1 = M2 proof let K be Field; ::_thesis: for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 & M1 - M3 = M2 - M3 holds M1 = M2 let M1, M2, M3 be Matrix of K; ::_thesis: ( len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 & M1 - M3 = M2 - M3 implies M1 = M2 ) assume that A1: len M1 = len M2 and A2: len M2 = len M3 and A3: width M1 = width M2 and A4: width M2 = width M3 and A5: M1 - M3 = M2 - M3 ; ::_thesis: M1 = M2 A6: ( len (- M3) = len M3 & width (- M3) = width M3 ) by MATRIX_3:def_2; percases ( len M1 > 0 or len M1 = 0 ) by NAT_1:3; supposeA7: len M1 > 0 ; ::_thesis: M1 = M2 then A8: M2 is Matrix of len M1, width M1,K by A1, A3, MATRIX_1:20; A9: M3 is Matrix of len M1, width M1,K by A1, A2, A3, A4, A7, MATRIX_1:20; (M1 + (- M3)) + M3 = M2 + ((- M3) + M3) by A2, A4, A5, A6, MATRIX_3:3; then (M1 + (- M3)) + M3 = M2 + (M3 + (- M3)) by A6, MATRIX_3:2; then (M1 + (- M3)) + M3 = M2 + (0. (K,(len M1),(width M1))) by A9, MATRIX_3:5; then (M1 + (- M3)) + M3 = M2 by A8, MATRIX_3:4; then M1 + ((- M3) + M3) = M2 by A1, A2, A3, A4, A6, MATRIX_3:3; then M1 + (M3 + (- M3)) = M2 by A6, MATRIX_3:2; then A10: M1 + (0. (K,(len M1),(width M1))) = M2 by A9, MATRIX_3:5; M1 is Matrix of len M1, width M1,K by A7, MATRIX_1:20; hence M1 = M2 by A10, MATRIX_3:4; ::_thesis: verum end; suppose len M1 = 0 ; ::_thesis: M1 = M2 hence M1 = M2 by A1, CARD_2:64; ::_thesis: verum end; end; end; theorem Th15: :: MATRIX_4:15 for K being Field for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 & M3 - M1 = M3 - M2 holds M1 = M2 proof let K be Field; ::_thesis: for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 & M3 - M1 = M3 - M2 holds M1 = M2 let M1, M2, M3 be Matrix of K; ::_thesis: ( len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 & M3 - M1 = M3 - M2 implies M1 = M2 ) assume that A1: len M1 = len M2 and A2: len M2 = len M3 and A3: width M1 = width M2 and A4: width M2 = width M3 and A5: M3 - M1 = M3 - M2 ; ::_thesis: M1 = M2 percases ( len M1 > 0 or len M1 = 0 ) by NAT_1:3; supposeA6: len M1 > 0 ; ::_thesis: M1 = M2 then A7: M3 is Matrix of len M1, width M1,K by A1, A2, A3, A4, MATRIX_1:20; A8: ( len (- M2) = len M2 & width (- M2) = width M2 ) by MATRIX_3:def_2; then A9: - M2 is Matrix of len M1, width M1,K by A1, A3, A6, MATRIX_1:20; A10: ( len (- M1) = len M1 & width (- M1) = width M1 ) by MATRIX_3:def_2; then (- M1) + M3 = M3 + (- M2) by A1, A2, A3, A4, A5, MATRIX_3:2; then (- M1) + M3 = (- M2) + M3 by A2, A4, A8, MATRIX_3:2; then ((- M1) + M3) + (- M3) = (- M2) + (M3 + (- M3)) by A2, A4, A8, MATRIX_3:3; then ((- M1) + M3) + (- M3) = (- M2) + (0. (K,(len M1),(width M1))) by A7, MATRIX_3:5; then ((- M1) + M3) + (- M3) = - M2 by A9, MATRIX_3:4; then (- M1) + (M3 + (- M3)) = - M2 by A1, A2, A3, A4, A10, MATRIX_3:3; then A11: (- M1) + (0. (K,(len M1),(width M1))) = - M2 by A7, MATRIX_3:5; - M1 is Matrix of len M1, width M1,K by A6, A10, MATRIX_1:20; then - M1 = - M2 by A11, MATRIX_3:4; then - (- M1) = M2 by Th1; hence M1 = M2 by Th1; ::_thesis: verum end; suppose len M1 = 0 ; ::_thesis: M1 = M2 hence M1 = M2 by A1, CARD_2:64; ::_thesis: verum end; end; end; theorem Th16: :: MATRIX_4:16 for K being Field for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds (M1 - M2) - M3 = (M1 - M3) - M2 proof let K be Field; ::_thesis: for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds (M1 - M2) - M3 = (M1 - M3) - M2 let M1, M2, M3 be Matrix of K; ::_thesis: ( len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 implies (M1 - M2) - M3 = (M1 - M3) - M2 ) assume that A1: len M1 = len M2 and A2: len M2 = len M3 and A3: width M1 = width M2 and A4: width M2 = width M3 ; ::_thesis: (M1 - M2) - M3 = (M1 - M3) - M2 A5: ( len (- M3) = len M3 & width (- M3) = width M3 ) by MATRIX_3:def_2; A6: ( len (- M2) = len M2 & width (- M2) = width M2 ) by MATRIX_3:def_2; hence (M1 - M2) - M3 = M1 + ((- M2) + (- M3)) by A1, A3, MATRIX_3:3 .= M1 + ((- M3) + (- M2)) by A2, A4, A6, A5, MATRIX_3:2 .= (M1 - M3) - M2 by A1, A2, A3, A4, A5, MATRIX_3:3 ; ::_thesis: verum end; theorem :: MATRIX_4:17 for K being Field for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds M1 - M3 = (M1 - M2) - (M3 - M2) proof let K be Field; ::_thesis: for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds M1 - M3 = (M1 - M2) - (M3 - M2) let M1, M2, M3 be Matrix of K; ::_thesis: ( len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 implies M1 - M3 = (M1 - M2) - (M3 - M2) ) assume that A1: len M1 = len M2 and A2: len M2 = len M3 and A3: width M1 = width M2 and A4: width M2 = width M3 ; ::_thesis: M1 - M3 = (M1 - M2) - (M3 - M2) A5: ( len (- M2) = len M2 & width (- M2) = width M2 ) by MATRIX_3:def_2; A6: ( len (- M3) = len M3 & width (- M3) = width M3 ) by MATRIX_3:def_2; percases ( len M1 > 0 or len M1 = 0 ) by NAT_1:3; supposeA7: len M1 > 0 ; ::_thesis: M1 - M3 = (M1 - M2) - (M3 - M2) then A8: M2 is Matrix of len M1, width M1,K by A1, A3, MATRIX_1:20; A9: ( len (M1 + (- M2)) = len M1 & width (M1 + (- M2)) = width M1 ) by MATRIX_3:def_3; A10: M1 is Matrix of len M1, width M1,K by A7, MATRIX_1:20; (M1 - M2) - (M3 - M2) = (M1 + (- M2)) + ((- M3) + (- (- M2))) by A2, A4, A5, Th12 .= (M1 + (- M2)) + ((- M3) + M2) by Th1 .= (M1 + (- M2)) + (M2 + (- M3)) by A2, A4, A6, MATRIX_3:2 .= ((M1 + (- M2)) + M2) + (- M3) by A1, A3, A9, MATRIX_3:3 .= (M1 + ((- M2) + M2)) + (- M3) by A1, A3, A5, MATRIX_3:3 .= (M1 + (M2 + (- M2))) + (- M3) by A5, MATRIX_3:2 .= (M1 + (0. (K,(len M1),(width M1)))) + (- M3) by A8, MATRIX_3:5 .= M1 + (- M3) by A10, MATRIX_3:4 ; hence M1 - M3 = (M1 - M2) - (M3 - M2) ; ::_thesis: verum end; supposeA11: len M1 = 0 ; ::_thesis: M1 - M3 = (M1 - M2) - (M3 - M2) then len (M1 - M2) = 0 by MATRIX_3:def_3; then A12: len ((M1 - M2) - (M3 - M2)) = 0 by MATRIX_3:def_3; len (M1 - M3) = 0 by A11, MATRIX_3:def_3; hence M1 - M3 = (M1 - M2) - (M3 - M2) by A12, CARD_2:64; ::_thesis: verum end; end; end; theorem Th18: :: MATRIX_4:18 for K being Field for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds (M3 - M1) - (M3 - M2) = M2 - M1 proof let K be Field; ::_thesis: for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds (M3 - M1) - (M3 - M2) = M2 - M1 let M1, M2, M3 be Matrix of K; ::_thesis: ( len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 implies (M3 - M1) - (M3 - M2) = M2 - M1 ) assume that A1: len M1 = len M2 and A2: len M2 = len M3 and A3: width M1 = width M2 and A4: width M2 = width M3 ; ::_thesis: (M3 - M1) - (M3 - M2) = M2 - M1 percases ( len M1 > 0 or len M1 = 0 ) by NAT_1:3; supposeA5: len M1 > 0 ; ::_thesis: (M3 - M1) - (M3 - M2) = M2 - M1 then A6: M3 is Matrix of len M1, width M1,K by A1, A2, A3, A4, MATRIX_1:20; A7: ( len (- M2) = len M2 & width (- M2) = width M2 ) by MATRIX_3:def_2; A8: width (- M1) = width M1 by MATRIX_3:def_2; then A9: width ((- M1) + M3) = width M1 by MATRIX_3:def_3; A10: ( len (- M3) = len M3 & width (- M3) = width M3 ) by MATRIX_3:def_2; A11: len (- M1) = len M1 by MATRIX_3:def_2; then A12: len ((- M1) + M3) = len M1 by MATRIX_3:def_3; A13: - M1 is Matrix of len M1, width M1,K by A5, A11, A8, MATRIX_1:20; (M3 - M1) - (M3 - M2) = ((- M1) + M3) - (M3 + (- M2)) by A1, A2, A3, A4, A11, A8, MATRIX_3:2 .= ((- M1) + M3) + ((- M3) + (- (- M2))) by A2, A4, A7, Th12 .= ((- M1) + M3) + ((- M3) + M2) by Th1 .= (((- M1) + M3) + (- M3)) + M2 by A1, A2, A3, A4, A10, A12, A9, MATRIX_3:3 .= ((- M1) + (M3 + (- M3))) + M2 by A1, A2, A3, A4, A11, A8, MATRIX_3:3 .= ((- M1) + (0. (K,(len M1),(width M1)))) + M2 by A6, MATRIX_3:5 .= (- M1) + M2 by A13, MATRIX_3:4 .= M2 + (- M1) by A1, A3, A11, A8, MATRIX_3:2 ; hence (M3 - M1) - (M3 - M2) = M2 - M1 ; ::_thesis: verum end; supposeA14: len M1 = 0 ; ::_thesis: (M3 - M1) - (M3 - M2) = M2 - M1 A15: len (M2 - M1) = len M2 by MATRIX_3:def_3; len ((M3 - M1) - (M3 - M2)) = len (M3 - M1) by MATRIX_3:def_3 .= len M3 by MATRIX_3:def_3 ; hence (M3 - M1) - (M3 - M2) = M2 - M1 by A1, A2, A14, A15, CARD_2:64; ::_thesis: verum end; end; end; theorem :: MATRIX_4:19 for K being Field for M1, M2, M3, M4 being Matrix of K st len M1 = len M2 & len M2 = len M3 & len M3 = len M4 & width M1 = width M2 & width M2 = width M3 & width M3 = width M4 & M1 - M2 = M3 - M4 holds M1 - M3 = M2 - M4 proof let K be Field; ::_thesis: for M1, M2, M3, M4 being Matrix of K st len M1 = len M2 & len M2 = len M3 & len M3 = len M4 & width M1 = width M2 & width M2 = width M3 & width M3 = width M4 & M1 - M2 = M3 - M4 holds M1 - M3 = M2 - M4 let M1, M2, M3, M4 be Matrix of K; ::_thesis: ( len M1 = len M2 & len M2 = len M3 & len M3 = len M4 & width M1 = width M2 & width M2 = width M3 & width M3 = width M4 & M1 - M2 = M3 - M4 implies M1 - M3 = M2 - M4 ) assume that A1: len M1 = len M2 and A2: len M2 = len M3 and A3: len M3 = len M4 and A4: width M1 = width M2 and A5: width M2 = width M3 and A6: width M3 = width M4 and A7: M1 - M2 = M3 - M4 ; ::_thesis: M1 - M3 = M2 - M4 A8: ( len (- M4) = len M1 & width (- M4) = width M1 ) by A1, A2, A3, A4, A5, A6, MATRIX_3:def_2; A9: ( len (M3 + (- M4)) = len M1 & width (M3 + (- M4)) = width M1 ) by A1, A2, A4, A5, MATRIX_3:def_3; A10: ( len (- M2) = len M2 & width (- M2) = width M2 ) by MATRIX_3:def_2; A11: ( len (M1 + (- M3)) = len M1 & width (M1 + (- M3)) = width M1 ) by MATRIX_3:def_3; A12: ( len (M1 + (- M2)) = len M1 & width (M1 + (- M2)) = width M1 ) by MATRIX_3:def_3; A13: ( len (M1 + (- M3)) = len M1 & width (M1 + (- M3)) = width M1 ) by MATRIX_3:def_3; A14: ( len (M2 + (- M4)) = len M1 & width (M2 + (- M4)) = width M1 ) by A1, A4, MATRIX_3:def_3; A15: ( len (- M3) = len M3 & width (- M3) = width M3 ) by MATRIX_3:def_2; percases ( len M1 > 0 or len M1 = 0 ) by NAT_1:3; suppose len M1 > 0 ; ::_thesis: M1 - M3 = M2 - M4 then M3 + (- M4) is Matrix of len M1, width M1,K by A9, MATRIX_1:20; then (M1 + (- M2)) + (- (M3 + (- M4))) = 0. (K,(len M1),(width M1)) by A7, MATRIX_3:5; then (M1 + (- M2)) + ((- M3) + (- (- M4))) = 0. (K,(len M1),(width M1)) by A1, A2, A4, A5, A8, Th12; then (M1 + (- M2)) + ((- M3) + M4) = 0. (K,(len M1),(width M1)) by Th1; then ((M1 + (- M2)) + (- M3)) + M4 = 0. (K,(len M1),(width M1)) by A1, A2, A4, A5, A15, A12, MATRIX_3:3; then (M1 + ((- M2) + (- M3))) + M4 = 0. (K,(len M1),(width M1)) by A1, A4, A10, MATRIX_3:3; then (M1 + ((- M3) + (- M2))) + M4 = 0. (K,(len M1),(width M1)) by A2, A5, A10, A15, MATRIX_3:2; then ((M1 + (- M3)) + (- M2)) + M4 = 0. (K,(len M1),(width M1)) by A1, A2, A4, A5, A15, MATRIX_3:3; then (M1 + (- M3)) + ((- M2) + M4) = 0. (K,(len M1),(width M1)) by A1, A4, A10, A11, MATRIX_3:3; then (M1 + (- M3)) + ((- M2) + (- (- M4))) = 0. (K,(len M1),(width M1)) by Th1; then (M1 + (- M3)) - (M2 + (- M4)) = 0. (K,(len M1),(width M1)) by A1, A4, A8, Th12; hence M1 - M3 = M2 - M4 by A13, A14, Th7; ::_thesis: verum end; suppose len M1 = 0 ; ::_thesis: M1 - M3 = M2 - M4 then ( len (M1 - M3) = 0 & len (M2 - M4) = 0 ) by A1, MATRIX_3:def_3; hence M1 - M3 = M2 - M4 by CARD_2:64; ::_thesis: verum end; end; end; theorem Th20: :: MATRIX_4:20 for K being Field for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds M1 = M1 + (M2 - M2) proof let K be Field; ::_thesis: for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds M1 = M1 + (M2 - M2) let M1, M2 be Matrix of K; ::_thesis: ( len M1 = len M2 & width M1 = width M2 implies M1 = M1 + (M2 - M2) ) assume A1: ( len M1 = len M2 & width M1 = width M2 ) ; ::_thesis: M1 = M1 + (M2 - M2) percases ( len M1 > 0 or len M1 = 0 ) by NAT_1:3; supposeA2: len M1 > 0 ; ::_thesis: M1 = M1 + (M2 - M2) then A3: M1 is Matrix of len M1, width M1,K by MATRIX_1:20; M2 is Matrix of len M1, width M1,K by A1, A2, MATRIX_1:20; hence M1 + (M2 - M2) = M1 + (0. (K,(len M1),(width M1))) by MATRIX_3:5 .= M1 by A3, MATRIX_3:4 ; ::_thesis: verum end; supposeA4: len M1 = 0 ; ::_thesis: M1 = M1 + (M2 - M2) len (M1 + (M2 - M2)) = len M1 by MATRIX_3:def_3; hence M1 = M1 + (M2 - M2) by A4, CARD_2:64; ::_thesis: verum end; end; end; theorem Th21: :: MATRIX_4:21 for K being Field for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds M1 = (M1 + M2) - M2 proof let K be Field; ::_thesis: for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds M1 = (M1 + M2) - M2 let M1, M2 be Matrix of K; ::_thesis: ( len M1 = len M2 & width M1 = width M2 implies M1 = (M1 + M2) - M2 ) assume A1: ( len M1 = len M2 & width M1 = width M2 ) ; ::_thesis: M1 = (M1 + M2) - M2 hence (M1 + M2) - M2 = M1 + (M2 - M2) by MATRIX_3:3 .= M1 by A1, Th20 ; ::_thesis: verum end; theorem Th22: :: MATRIX_4:22 for K being Field for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds M1 = (M1 - M2) + M2 proof let K be Field; ::_thesis: for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds M1 = (M1 - M2) + M2 let M1, M2 be Matrix of K; ::_thesis: ( len M1 = len M2 & width M1 = width M2 implies M1 = (M1 - M2) + M2 ) assume A1: ( len M1 = len M2 & width M1 = width M2 ) ; ::_thesis: M1 = (M1 - M2) + M2 then A2: ( len (- M2) = len M1 & width (- M2) = width M1 ) by MATRIX_3:def_2; hence (M1 - M2) + M2 = M1 + ((- M2) + M2) by MATRIX_3:3 .= M1 + (M2 - M2) by A1, A2, MATRIX_3:2 .= M1 by A1, Th20 ; ::_thesis: verum end; theorem :: MATRIX_4:23 for K being Field for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds M1 + M3 = (M1 + M2) + (M3 - M2) proof let K be Field; ::_thesis: for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds M1 + M3 = (M1 + M2) + (M3 - M2) let M1, M2, M3 be Matrix of K; ::_thesis: ( len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 implies M1 + M3 = (M1 + M2) + (M3 - M2) ) assume that A1: len M1 = len M2 and A2: len M2 = len M3 and A3: width M1 = width M2 and A4: width M2 = width M3 ; ::_thesis: M1 + M3 = (M1 + M2) + (M3 - M2) A5: ( len (M1 + M2) = len M1 & width (M1 + M2) = width M1 ) by MATRIX_3:def_3; A6: ( len (- M2) = len M1 & width (- M2) = width M1 ) by A1, A3, MATRIX_3:def_2; hence (M1 + M2) + (M3 - M2) = (M1 + M2) + ((- M2) + M3) by A1, A2, A3, A4, MATRIX_3:2 .= ((M1 + M2) + (- M2)) + M3 by A6, A5, MATRIX_3:3 .= (M1 + (M2 - M2)) + M3 by A1, A3, MATRIX_3:3 .= M1 + M3 by A1, A3, Th20 ; ::_thesis: verum end; theorem :: MATRIX_4:24 for K being Field for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds (M1 + M2) - M3 = (M1 - M3) + M2 proof let K be Field; ::_thesis: for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds (M1 + M2) - M3 = (M1 - M3) + M2 let M1, M2, M3 be Matrix of K; ::_thesis: ( len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 implies (M1 + M2) - M3 = (M1 - M3) + M2 ) assume that A1: len M1 = len M2 and A2: len M2 = len M3 and A3: width M1 = width M2 and A4: width M2 = width M3 ; ::_thesis: (M1 + M2) - M3 = (M1 - M3) + M2 A5: ( len (- M3) = len M1 & width (- M3) = width M1 ) by A1, A2, A3, A4, MATRIX_3:def_2; thus (M1 + M2) - M3 = M1 + (M2 + (- M3)) by A1, A3, MATRIX_3:3 .= M1 + ((- M3) + M2) by A1, A3, A5, MATRIX_3:2 .= (M1 - M3) + M2 by A5, MATRIX_3:3 ; ::_thesis: verum end; theorem :: MATRIX_4:25 for K being Field for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds (M1 - M2) + M3 = (M3 - M2) + M1 proof let K be Field; ::_thesis: for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds (M1 - M2) + M3 = (M3 - M2) + M1 let M1, M2, M3 be Matrix of K; ::_thesis: ( len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 implies (M1 - M2) + M3 = (M3 - M2) + M1 ) assume that A1: len M1 = len M2 and A2: len M2 = len M3 and A3: width M1 = width M2 and A4: width M2 = width M3 ; ::_thesis: (M1 - M2) + M3 = (M3 - M2) + M1 A5: ( len (- M2) = len M1 & width (- M2) = width M1 ) by A1, A3, MATRIX_3:def_2; hence (M1 - M2) + M3 = ((- M2) + M1) + M3 by MATRIX_3:2 .= (- M2) + (M1 + M3) by A5, MATRIX_3:3 .= (- M2) + (M3 + M1) by A1, A2, A3, A4, MATRIX_3:2 .= ((- M2) + M3) + M1 by A1, A2, A3, A4, A5, MATRIX_3:3 .= (M3 - M2) + M1 by A1, A2, A3, A4, A5, MATRIX_3:2 ; ::_thesis: verum end; theorem Th26: :: MATRIX_4:26 for K being Field for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds M1 + M3 = (M1 + M2) - (M2 - M3) proof let K be Field; ::_thesis: for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds M1 + M3 = (M1 + M2) - (M2 - M3) let M1, M2, M3 be Matrix of K; ::_thesis: ( len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 implies M1 + M3 = (M1 + M2) - (M2 - M3) ) assume that A1: len M1 = len M2 and A2: len M2 = len M3 and A3: width M1 = width M2 and A4: width M2 = width M3 ; ::_thesis: M1 + M3 = (M1 + M2) - (M2 - M3) percases ( len M1 > 0 or len M1 = 0 ) by NAT_1:3; supposeA5: len M1 > 0 ; ::_thesis: M1 + M3 = (M1 + M2) - (M2 - M3) then A6: M2 is Matrix of len M1, width M1,K by A1, A3, MATRIX_1:20; A7: ( len (- M2) = len M1 & width (- M2) = width M1 ) by A1, A3, MATRIX_3:def_2; A8: ( len (- M3) = len M1 & width (- M3) = width M1 ) by A1, A2, A3, A4, MATRIX_3:def_2; A9: ( len (M1 + M2) = len M1 & width (M1 + M2) = width M1 ) by MATRIX_3:def_3; M1 is Matrix of len M1, width M1,K by A5, MATRIX_1:20; hence M1 + M3 = (M1 + (0. (K,(len M1),(width M1)))) + M3 by MATRIX_3:4 .= (M1 + (M2 + (- M2))) + M3 by A6, MATRIX_3:5 .= ((M1 + M2) + (- M2)) + M3 by A1, A3, MATRIX_3:3 .= (M1 + M2) + ((- M2) + M3) by A7, A9, MATRIX_3:3 .= (M1 + M2) + ((- M2) + (- (- M3))) by Th1 .= (M1 + M2) - (M2 - M3) by A1, A3, A8, Th12 ; ::_thesis: verum end; supposeA10: len M1 = 0 ; ::_thesis: M1 + M3 = (M1 + M2) - (M2 - M3) A11: len ((M1 + M2) - (M2 - M3)) = len (M1 + M2) by MATRIX_3:def_3 .= len M1 by MATRIX_3:def_3 ; len (M1 + M3) = len M1 by MATRIX_3:def_3; hence M1 + M3 = (M1 + M2) - (M2 - M3) by A10, A11, CARD_2:64; ::_thesis: verum end; end; end; theorem :: MATRIX_4:27 for K being Field for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds M1 - M3 = (M1 + M2) - (M3 + M2) proof let K be Field; ::_thesis: for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds M1 - M3 = (M1 + M2) - (M3 + M2) let M1, M2, M3 be Matrix of K; ::_thesis: ( len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 implies M1 - M3 = (M1 + M2) - (M3 + M2) ) assume that A1: len M1 = len M2 and A2: len M2 = len M3 and A3: width M1 = width M2 and A4: width M2 = width M3 ; ::_thesis: M1 - M3 = (M1 + M2) - (M3 + M2) ( len (- M3) = len M1 & width (- M3) = width M1 ) by A1, A2, A3, A4, MATRIX_3:def_2; hence M1 - M3 = (M1 + M2) - (M2 - (- M3)) by A1, A3, Th26 .= (M1 + M2) - (M2 + M3) by Th1 .= (M1 + M2) - (M3 + M2) by A2, A4, MATRIX_3:2 ; ::_thesis: verum end; theorem Th28: :: MATRIX_4:28 for K being Field for M1, M2, M3, M4 being Matrix of K st len M1 = len M2 & len M2 = len M3 & len M3 = len M4 & width M1 = width M2 & width M2 = width M3 & width M3 = width M4 & M1 + M2 = M3 + M4 holds M1 - M3 = M4 - M2 proof let K be Field; ::_thesis: for M1, M2, M3, M4 being Matrix of K st len M1 = len M2 & len M2 = len M3 & len M3 = len M4 & width M1 = width M2 & width M2 = width M3 & width M3 = width M4 & M1 + M2 = M3 + M4 holds M1 - M3 = M4 - M2 let M1, M2, M3, M4 be Matrix of K; ::_thesis: ( len M1 = len M2 & len M2 = len M3 & len M3 = len M4 & width M1 = width M2 & width M2 = width M3 & width M3 = width M4 & M1 + M2 = M3 + M4 implies M1 - M3 = M4 - M2 ) assume that A1: len M1 = len M2 and A2: len M2 = len M3 and A3: len M3 = len M4 and A4: width M1 = width M2 and A5: width M2 = width M3 and A6: width M3 = width M4 and A7: M1 + M2 = M3 + M4 ; ::_thesis: M1 - M3 = M4 - M2 A8: ( len (- M2) = len M1 & width (- M2) = width M1 ) by A1, A4, MATRIX_3:def_2; M1 + M2 = M4 + M3 by A3, A6, A7, MATRIX_3:2; then (M1 + M2) + (- M2) = M4 + (M3 + (- M2)) by A3, A6, MATRIX_3:3; then (M1 + M2) + (- M2) = M4 + ((- M2) + M3) by A1, A2, A4, A5, A8, MATRIX_3:2; then M1 + (M2 - M2) = M4 + ((- M2) + M3) by A1, A4, MATRIX_3:3; then M1 = M4 + ((- M2) + M3) by A1, A4, Th20; then A9: M1 = (M4 + (- M2)) + M3 by A1, A2, A3, A4, A5, A6, A8, MATRIX_3:3; ( len (M4 + (- M2)) = len M1 & width (M4 + (- M2)) = width M1 ) by A1, A2, A3, A4, A5, A6, MATRIX_3:def_3; hence M1 - M3 = M4 - M2 by A1, A2, A4, A5, A9, Th21; ::_thesis: verum end; theorem :: MATRIX_4:29 for K being Field for M1, M2, M3, M4 being Matrix of K st len M1 = len M2 & len M2 = len M3 & len M3 = len M4 & width M1 = width M2 & width M2 = width M3 & width M3 = width M4 & M1 - M3 = M4 - M2 holds M1 + M2 = M3 + M4 proof let K be Field; ::_thesis: for M1, M2, M3, M4 being Matrix of K st len M1 = len M2 & len M2 = len M3 & len M3 = len M4 & width M1 = width M2 & width M2 = width M3 & width M3 = width M4 & M1 - M3 = M4 - M2 holds M1 + M2 = M3 + M4 let M1, M2, M3, M4 be Matrix of K; ::_thesis: ( len M1 = len M2 & len M2 = len M3 & len M3 = len M4 & width M1 = width M2 & width M2 = width M3 & width M3 = width M4 & M1 - M3 = M4 - M2 implies M1 + M2 = M3 + M4 ) assume that A1: len M1 = len M2 and A2: len M2 = len M3 and A3: len M3 = len M4 and A4: width M1 = width M2 and A5: width M2 = width M3 and A6: width M3 = width M4 and A7: M1 - M3 = M4 - M2 ; ::_thesis: M1 + M2 = M3 + M4 A8: ( len (- M3) = len M1 & width (- M3) = width M1 ) by A1, A2, A4, A5, MATRIX_3:def_2; A9: ( len (- M2) = len M1 & width (- M2) = width M1 ) by A1, A4, MATRIX_3:def_2; then M1 + (- M3) = (- M2) + M4 by A1, A2, A3, A4, A5, A6, A7, MATRIX_3:2; then M1 - (- M2) = M4 - (- M3) by A1, A2, A3, A4, A5, A6, A9, A8, Th28; then M1 + M2 = M4 - (- M3) by Th1; then M1 + M2 = M4 + M3 by Th1; hence M1 + M2 = M3 + M4 by A3, A6, MATRIX_3:2; ::_thesis: verum end; theorem :: MATRIX_4:30 for K being Field for M1, M2, M3, M4 being Matrix of K st len M1 = len M2 & len M2 = len M3 & len M3 = len M4 & width M1 = width M2 & width M2 = width M3 & width M3 = width M4 & M1 + M2 = M3 - M4 holds M1 + M4 = M3 - M2 proof let K be Field; ::_thesis: for M1, M2, M3, M4 being Matrix of K st len M1 = len M2 & len M2 = len M3 & len M3 = len M4 & width M1 = width M2 & width M2 = width M3 & width M3 = width M4 & M1 + M2 = M3 - M4 holds M1 + M4 = M3 - M2 let M1, M2, M3, M4 be Matrix of K; ::_thesis: ( len M1 = len M2 & len M2 = len M3 & len M3 = len M4 & width M1 = width M2 & width M2 = width M3 & width M3 = width M4 & M1 + M2 = M3 - M4 implies M1 + M4 = M3 - M2 ) assume that A1: ( len M1 = len M2 & len M2 = len M3 ) and A2: len M3 = len M4 and A3: ( width M1 = width M2 & width M2 = width M3 ) and A4: width M3 = width M4 and A5: M1 + M2 = M3 - M4 ; ::_thesis: M1 + M4 = M3 - M2 A6: ( len (- M4) = len M1 & width (- M4) = width M1 ) by A1, A2, A3, A4, MATRIX_3:def_2; then M1 + M2 = (- M4) + M3 by A1, A3, A5, MATRIX_3:2; then M1 - (- M4) = M3 - M2 by A1, A3, A6, Th28; hence M1 + M4 = M3 - M2 by Th1; ::_thesis: verum end; theorem Th31: :: MATRIX_4:31 for K being Field for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds M1 - (M2 + M3) = (M1 - M2) - M3 proof let K be Field; ::_thesis: for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds M1 - (M2 + M3) = (M1 - M2) - M3 let M1, M2, M3 be Matrix of K; ::_thesis: ( len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 implies M1 - (M2 + M3) = (M1 - M2) - M3 ) assume that A1: len M1 = len M2 and A2: len M2 = len M3 and A3: width M1 = width M2 and A4: width M2 = width M3 ; ::_thesis: M1 - (M2 + M3) = (M1 - M2) - M3 A5: ( len (- M2) = len M1 & width (- M2) = width M1 ) by A1, A3, MATRIX_3:def_2; M1 - (M2 + M3) = M1 + ((- M2) + (- M3)) by A2, A4, Th12 .= (M1 - M2) + (- M3) by A5, MATRIX_3:3 ; hence M1 - (M2 + M3) = (M1 - M2) - M3 ; ::_thesis: verum end; theorem :: MATRIX_4:32 for K being Field for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds M1 - (M2 - M3) = (M1 - M2) + M3 proof let K be Field; ::_thesis: for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds M1 - (M2 - M3) = (M1 - M2) + M3 let M1, M2, M3 be Matrix of K; ::_thesis: ( len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 implies M1 - (M2 - M3) = (M1 - M2) + M3 ) assume that A1: len M1 = len M2 and A2: len M2 = len M3 and A3: width M1 = width M2 and A4: width M2 = width M3 ; ::_thesis: M1 - (M2 - M3) = (M1 - M2) + M3 ( len (- M3) = len M1 & width (- M3) = width M1 ) by A1, A2, A3, A4, MATRIX_3:def_2; then M1 - (M2 - M3) = (M1 - M2) - (- M3) by A1, A3, Th31 .= (M1 + (- M2)) + M3 by Th1 ; hence M1 - (M2 - M3) = (M1 - M2) + M3 ; ::_thesis: verum end; theorem :: MATRIX_4:33 for K being Field for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds M1 - (M2 - M3) = M1 + (M3 - M2) proof let K be Field; ::_thesis: for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds M1 - (M2 - M3) = M1 + (M3 - M2) let M1, M2, M3 be Matrix of K; ::_thesis: ( len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 implies M1 - (M2 - M3) = M1 + (M3 - M2) ) assume that A1: len M1 = len M2 and A2: len M2 = len M3 and A3: width M1 = width M2 and A4: width M2 = width M3 ; ::_thesis: M1 - (M2 - M3) = M1 + (M3 - M2) A5: ( len (- M3) = len M1 & width (- M3) = width M1 ) by A1, A2, A3, A4, MATRIX_3:def_2; then M1 - (M2 - M3) = M1 + (- ((- M3) + M2)) by A1, A3, MATRIX_3:2 .= M1 + ((- (- M3)) + (- M2)) by A1, A3, A5, Th12 .= M1 + (M3 + (- M2)) by Th1 ; hence M1 - (M2 - M3) = M1 + (M3 - M2) ; ::_thesis: verum end; theorem :: MATRIX_4:34 for K being Field for M1, M2, M3 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds M1 - M3 = (M1 - M2) + (M2 - M3) proof let K be Field; ::_thesis: for M1, M2, M3 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds M1 - M3 = (M1 - M2) + (M2 - M3) let M1, M2, M3 be Matrix of K; ::_thesis: ( len M1 = len M2 & width M1 = width M2 implies M1 - M3 = (M1 - M2) + (M2 - M3) ) assume A1: ( len M1 = len M2 & width M1 = width M2 ) ; ::_thesis: M1 - M3 = (M1 - M2) + (M2 - M3) then A2: ( len (- M2) = len M1 & width (- M2) = width M1 ) by MATRIX_3:def_2; ( len (M1 + (- M2)) = len M1 & width (M1 + (- M2)) = width M1 ) by MATRIX_3:def_3; then (M1 - M2) + (M2 - M3) = ((M1 + (- M2)) + M2) + (- M3) by A1, MATRIX_3:3 .= (M1 + ((- M2) + M2)) + (- M3) by A2, MATRIX_3:3 .= (M1 + (M2 - M2)) + (- M3) by A1, A2, MATRIX_3:2 .= M1 + (- M3) by A1, Th20 ; hence M1 - M3 = (M1 - M2) + (M2 - M3) ; ::_thesis: verum end; theorem :: MATRIX_4:35 for K being Field for M1, M2, M3 being Matrix of K st - M1 = - M2 holds M1 = M2 proof let K be Field; ::_thesis: for M1, M2, M3 being Matrix of K st - M1 = - M2 holds M1 = M2 let M1, M2, M3 be Matrix of K; ::_thesis: ( - M1 = - M2 implies M1 = M2 ) assume - M1 = - M2 ; ::_thesis: M1 = M2 then - (- M1) = M2 by Th1; hence M1 = M2 by Th1; ::_thesis: verum end; theorem :: MATRIX_4:36 for K being Field for M being Matrix of K st - M = 0. (K,(len M),(width M)) holds M = 0. (K,(len M),(width M)) proof let K be Field; ::_thesis: for M being Matrix of K st - M = 0. (K,(len M),(width M)) holds M = 0. (K,(len M),(width M)) let M be Matrix of K; ::_thesis: ( - M = 0. (K,(len M),(width M)) implies M = 0. (K,(len M),(width M)) ) assume - M = 0. (K,(len M),(width M)) ; ::_thesis: M = 0. (K,(len M),(width M)) then - (- M) = 0. (K,(len M),(width M)) by Th9; hence M = 0. (K,(len M),(width M)) by Th1; ::_thesis: verum end; theorem :: MATRIX_4:37 for K being Field for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 & M1 + (- M2) = 0. (K,(len M1),(width M1)) holds M1 = M2 proof let K be Field; ::_thesis: for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 & M1 + (- M2) = 0. (K,(len M1),(width M1)) holds M1 = M2 let M1, M2 be Matrix of K; ::_thesis: ( len M1 = len M2 & width M1 = width M2 & M1 + (- M2) = 0. (K,(len M1),(width M1)) implies M1 = M2 ) assume that A1: ( len M1 = len M2 & width M1 = width M2 ) and A2: M1 + (- M2) = 0. (K,(len M1),(width M1)) ; ::_thesis: M1 = M2 M1 - M2 = 0. (K,(len M1),(width M1)) by A2; hence M1 = M2 by A1, Th7; ::_thesis: verum end; theorem Th38: :: MATRIX_4:38 for K being Field for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds M1 = (M1 + M2) + (- M2) proof let K be Field; ::_thesis: for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds M1 = (M1 + M2) + (- M2) let M1, M2 be Matrix of K; ::_thesis: ( len M1 = len M2 & width M1 = width M2 implies M1 = (M1 + M2) + (- M2) ) A1: (M1 + M2) + (- M2) = (M1 + M2) - M2 ; assume ( len M1 = len M2 & width M1 = width M2 ) ; ::_thesis: M1 = (M1 + M2) + (- M2) hence M1 = (M1 + M2) + (- M2) by A1, Th21; ::_thesis: verum end; theorem :: MATRIX_4:39 for K being Field for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds M1 = M1 + (M2 + (- M2)) proof let K be Field; ::_thesis: for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds M1 = M1 + (M2 + (- M2)) let M1, M2 be Matrix of K; ::_thesis: ( len M1 = len M2 & width M1 = width M2 implies M1 = M1 + (M2 + (- M2)) ) A1: M1 + (M2 + (- M2)) = M1 + (M2 - M2) ; assume ( len M1 = len M2 & width M1 = width M2 ) ; ::_thesis: M1 = M1 + (M2 + (- M2)) hence M1 = M1 + (M2 + (- M2)) by A1, Th20; ::_thesis: verum end; theorem :: MATRIX_4:40 for K being Field for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds M1 = ((- M2) + M1) + M2 proof let K be Field; ::_thesis: for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds M1 = ((- M2) + M1) + M2 let M1, M2 be Matrix of K; ::_thesis: ( len M1 = len M2 & width M1 = width M2 implies M1 = ((- M2) + M1) + M2 ) assume A1: ( len M1 = len M2 & width M1 = width M2 ) ; ::_thesis: M1 = ((- M2) + M1) + M2 then ( len (- M2) = len M1 & width (- M2) = width M1 ) by MATRIX_3:def_2; then ((- M2) + M1) + M2 = (M1 - M2) + M2 by MATRIX_3:2; hence M1 = ((- M2) + M1) + M2 by A1, Th22; ::_thesis: verum end; theorem :: MATRIX_4:41 for K being Field for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds - ((- M1) + M2) = M1 + (- M2) proof let K be Field; ::_thesis: for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds - ((- M1) + M2) = M1 + (- M2) let M1, M2 be Matrix of K; ::_thesis: ( len M1 = len M2 & width M1 = width M2 implies - ((- M1) + M2) = M1 + (- M2) ) A1: ( len (- M1) = len M1 & width (- M1) = width M1 ) by MATRIX_3:def_2; assume ( len M1 = len M2 & width M1 = width M2 ) ; ::_thesis: - ((- M1) + M2) = M1 + (- M2) then - ((- M1) + M2) = (- (- M1)) + (- M2) by A1, Th12; hence - ((- M1) + M2) = M1 + (- M2) by Th1; ::_thesis: verum end; theorem :: MATRIX_4:42 for K being Field for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds M1 + M2 = - ((- M1) + (- M2)) proof let K be Field; ::_thesis: for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds M1 + M2 = - ((- M1) + (- M2)) let M1, M2 be Matrix of K; ::_thesis: ( len M1 = len M2 & width M1 = width M2 implies M1 + M2 = - ((- M1) + (- M2)) ) assume ( len M1 = len M2 & width M1 = width M2 ) ; ::_thesis: M1 + M2 = - ((- M1) + (- M2)) then A1: ( len (- M2) = len M1 & width (- M2) = width M1 ) by MATRIX_3:def_2; ( len (- M1) = len M1 & width (- M1) = width M1 ) by MATRIX_3:def_2; then - ((- M1) + (- M2)) = (- (- M1)) + (- (- M2)) by A1, Th12 .= M1 + (- (- M2)) by Th1 ; hence M1 + M2 = - ((- M1) + (- M2)) by Th1; ::_thesis: verum end; theorem :: MATRIX_4:43 for K being Field for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds - (M1 - M2) = M2 - M1 proof let K be Field; ::_thesis: for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds - (M1 - M2) = M2 - M1 let M1, M2 be Matrix of K; ::_thesis: ( len M1 = len M2 & width M1 = width M2 implies - (M1 - M2) = M2 - M1 ) A1: ( len (- M1) = len M1 & width (- M1) = width M1 ) by MATRIX_3:def_2; assume A2: ( len M1 = len M2 & width M1 = width M2 ) ; ::_thesis: - (M1 - M2) = M2 - M1 then ( len (- M2) = len M1 & width (- M2) = width M1 ) by MATRIX_3:def_2; then - (M1 - M2) = (- M1) + (- (- M2)) by Th12 .= (- M1) + M2 by Th1 .= M2 + (- M1) by A2, A1, MATRIX_3:2 ; hence - (M1 - M2) = M2 - M1 ; ::_thesis: verum end; theorem Th44: :: MATRIX_4:44 for K being Field for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds (- M1) - M2 = (- M2) - M1 proof let K be Field; ::_thesis: for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds (- M1) - M2 = (- M2) - M1 let M1, M2 be Matrix of K; ::_thesis: ( len M1 = len M2 & width M1 = width M2 implies (- M1) - M2 = (- M2) - M1 ) assume ( len M1 = len M2 & width M1 = width M2 ) ; ::_thesis: (- M1) - M2 = (- M2) - M1 then A1: ( len (- M2) = len M1 & width (- M2) = width M1 ) by MATRIX_3:def_2; ( len (- M1) = len M1 & width (- M1) = width M1 ) by MATRIX_3:def_2; hence (- M1) - M2 = (- M2) - M1 by A1, MATRIX_3:2; ::_thesis: verum end; theorem :: MATRIX_4:45 for K being Field for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds M1 = (- M2) - ((- M1) - M2) proof let K be Field; ::_thesis: for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds M1 = (- M2) - ((- M1) - M2) let M1, M2 be Matrix of K; ::_thesis: ( len M1 = len M2 & width M1 = width M2 implies M1 = (- M2) - ((- M1) - M2) ) A1: ( len (M1 + M2) = len M1 & width (M1 + M2) = width M1 ) by MATRIX_3:def_3; assume A2: ( len M1 = len M2 & width M1 = width M2 ) ; ::_thesis: M1 = (- M2) - ((- M1) - M2) then A3: ( len (- M2) = len M1 & width (- M2) = width M1 ) by MATRIX_3:def_2; ( len (- M1) = len M1 & width (- M1) = width M1 ) by MATRIX_3:def_2; then (- M2) - ((- M1) - M2) = (- M2) + ((- (- M1)) + (- (- M2))) by A3, Th12 .= (- M2) + (M1 + (- (- M2))) by Th1 .= (- M2) + (M1 + M2) by Th1 .= (M1 + M2) + (- M2) by A3, A1, MATRIX_3:2 ; hence M1 = (- M2) - ((- M1) - M2) by A2, Th38; ::_thesis: verum end; theorem Th46: :: MATRIX_4:46 for K being Field for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds ((- M1) - M2) - M3 = ((- M1) - M3) - M2 proof let K be Field; ::_thesis: for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds ((- M1) - M2) - M3 = ((- M1) - M3) - M2 let M1, M2, M3 be Matrix of K; ::_thesis: ( len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 implies ((- M1) - M2) - M3 = ((- M1) - M3) - M2 ) A1: ( len (- M1) = len M1 & width (- M1) = width M1 ) by MATRIX_3:def_2; assume ( len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 ) ; ::_thesis: ((- M1) - M2) - M3 = ((- M1) - M3) - M2 hence ((- M1) - M2) - M3 = ((- M1) - M3) - M2 by A1, Th16; ::_thesis: verum end; theorem Th47: :: MATRIX_4:47 for K being Field for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds ((- M1) - M2) - M3 = ((- M2) - M3) - M1 proof let K be Field; ::_thesis: for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds ((- M1) - M2) - M3 = ((- M2) - M3) - M1 let M1, M2, M3 be Matrix of K; ::_thesis: ( len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 implies ((- M1) - M2) - M3 = ((- M2) - M3) - M1 ) assume that A1: len M1 = len M2 and A2: len M2 = len M3 and A3: width M1 = width M2 and A4: width M2 = width M3 ; ::_thesis: ((- M1) - M2) - M3 = ((- M2) - M3) - M1 ((- M1) - M2) - M3 = ((- M2) - M1) - M3 by A1, A3, Th44; hence ((- M1) - M2) - M3 = ((- M2) - M3) - M1 by A1, A2, A3, A4, Th46; ::_thesis: verum end; theorem :: MATRIX_4:48 for K being Field for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds ((- M1) - M2) - M3 = ((- M3) - M2) - M1 proof let K be Field; ::_thesis: for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds ((- M1) - M2) - M3 = ((- M3) - M2) - M1 let M1, M2, M3 be Matrix of K; ::_thesis: ( len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 implies ((- M1) - M2) - M3 = ((- M3) - M2) - M1 ) assume A1: ( len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 ) ; ::_thesis: ((- M1) - M2) - M3 = ((- M3) - M2) - M1 then ((- M1) - M2) - M3 = ((- M1) - M3) - M2 by Th46; hence ((- M1) - M2) - M3 = ((- M3) - M2) - M1 by A1, Th47; ::_thesis: verum end; theorem :: MATRIX_4:49 for K being Field for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds (M3 - M1) - (M3 - M2) = - (M1 - M2) proof let K be Field; ::_thesis: for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 holds (M3 - M1) - (M3 - M2) = - (M1 - M2) let M1, M2, M3 be Matrix of K; ::_thesis: ( len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 implies (M3 - M1) - (M3 - M2) = - (M1 - M2) ) assume that A1: len M1 = len M2 and A2: len M2 = len M3 and A3: width M1 = width M2 and A4: width M2 = width M3 ; ::_thesis: (M3 - M1) - (M3 - M2) = - (M1 - M2) A5: ( len (- M1) = len M1 & width (- M1) = width M1 ) by MATRIX_3:def_2; A6: ( len (- M2) = len M2 & width (- M2) = width M2 ) by MATRIX_3:def_2; (M3 - M1) - (M3 - M2) = M2 - M1 by A1, A2, A3, A4, Th18 .= (- M1) + M2 by A1, A3, A5, MATRIX_3:2 .= (- M1) + (- (- M2)) by Th1 .= - (M1 + (- M2)) by A1, A3, A6, Th12 ; hence (M3 - M1) - (M3 - M2) = - (M1 - M2) ; ::_thesis: verum end; theorem :: MATRIX_4:50 for K being Field for M being Matrix of K holds (0. (K,(len M),(width M))) - M = - M proof let K be Field; ::_thesis: for M being Matrix of K holds (0. (K,(len M),(width M))) - M = - M let M be Matrix of K; ::_thesis: (0. (K,(len M),(width M))) - M = - M A1: len (- M) = len M by MATRIX_3:def_2; A2: width (- M) = width M by MATRIX_3:def_2; A3: len (0. (K,(len M),(width M))) = len M by MATRIX_1:def_2; percases ( len M > 0 or len M = 0 ) by NAT_1:3; supposeA4: len M > 0 ; ::_thesis: (0. (K,(len M),(width M))) - M = - M then width (0. (K,(len M),(width M))) = width M by A3, MATRIX_1:20; then A5: (0. (K,(len M),(width M))) - M = (- M) + (0. (K,(len M),(width M))) by A1, A2, A3, MATRIX_3:2; - M is Matrix of len M, width M,K by A1, A2, A4, MATRIX_1:20; hence (0. (K,(len M),(width M))) - M = - M by A5, MATRIX_3:4; ::_thesis: verum end; supposeA6: len M = 0 ; ::_thesis: (0. (K,(len M),(width M))) - M = - M len ((0. (K,(len M),(width M))) - M) = len (0. (K,(len M),(width M))) by MATRIX_3:def_3; hence (0. (K,(len M),(width M))) - M = - M by A1, A3, A6, CARD_2:64; ::_thesis: verum end; end; end; theorem :: MATRIX_4:51 for K being Field for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds M1 + M2 = M1 - (- M2) by Th1; theorem :: MATRIX_4:52 for K being Field for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds M1 = M1 - (M2 + (- M2)) proof let K be Field; ::_thesis: for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds M1 = M1 - (M2 + (- M2)) let M1, M2 be Matrix of K; ::_thesis: ( len M1 = len M2 & width M1 = width M2 implies M1 = M1 - (M2 + (- M2)) ) assume ( len M1 = len M2 & width M1 = width M2 ) ; ::_thesis: M1 = M1 - (M2 + (- M2)) then M1 = M1 - (M2 - M2) by Th11; hence M1 = M1 - (M2 + (- M2)) ; ::_thesis: verum end; theorem :: MATRIX_4:53 for K being Field for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 & M1 - M3 = M2 + (- M3) holds M1 = M2 proof let K be Field; ::_thesis: for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 & M1 - M3 = M2 + (- M3) holds M1 = M2 let M1, M2, M3 be Matrix of K; ::_thesis: ( len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 & M1 - M3 = M2 + (- M3) implies M1 = M2 ) assume that A1: ( len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 ) and A2: M1 - M3 = M2 + (- M3) ; ::_thesis: M1 = M2 M1 - M3 = M2 - M3 by A2; hence M1 = M2 by A1, Th14; ::_thesis: verum end; theorem :: MATRIX_4:54 for K being Field for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 & M3 - M1 = M3 + (- M2) holds M1 = M2 proof let K be Field; ::_thesis: for M1, M2, M3 being Matrix of K st len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 & M3 - M1 = M3 + (- M2) holds M1 = M2 let M1, M2, M3 be Matrix of K; ::_thesis: ( len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 & M3 - M1 = M3 + (- M2) implies M1 = M2 ) assume that A1: ( len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 = width M3 ) and A2: M3 - M1 = M3 + (- M2) ; ::_thesis: M1 = M2 M3 - M1 = M3 - M2 by A2; hence M1 = M2 by A1, Th15; ::_thesis: verum end; theorem Th55: :: MATRIX_4:55 for K being set for A, B being Matrix of K st len A = len B & width A = width B holds Indices A = Indices B proof let K be set ; ::_thesis: for A, B being Matrix of K st len A = len B & width A = width B holds Indices A = Indices B let A, B be Matrix of K; ::_thesis: ( len A = len B & width A = width B implies Indices A = Indices B ) A1: dom A = Seg (len A) by FINSEQ_1:def_3; assume ( len A = len B & width A = width B ) ; ::_thesis: Indices A = Indices B hence Indices A = Indices B by A1, FINSEQ_1:def_3; ::_thesis: verum end; theorem Th56: :: MATRIX_4:56 for K being Field for x, y, z being FinSequence of K st len x = len y & len y = len z holds mlt ((x + y),z) = (mlt (x,z)) + (mlt (y,z)) proof let K be Field; ::_thesis: for x, y, z being FinSequence of K st len x = len y & len y = len z holds mlt ((x + y),z) = (mlt (x,z)) + (mlt (y,z)) let x, y, z be FinSequence of K; ::_thesis: ( len x = len y & len y = len z implies mlt ((x + y),z) = (mlt (x,z)) + (mlt (y,z)) ) assume that A1: len x = len y and A2: len y = len z ; ::_thesis: mlt ((x + y),z) = (mlt (x,z)) + (mlt (y,z)) A3: dom z = Seg (len x) by A1, A2, FINSEQ_1:def_3; reconsider x2 = x, y2 = y, z2 = z as Element of (len x) -tuples_on the carrier of K by A1, A2, FINSEQ_2:92; A4: dom (x + y) = Seg (len (x2 + y2)) by FINSEQ_1:def_3 .= Seg (len x) by CARD_1:def_7 .= dom z by A1, A2, FINSEQ_1:def_3 ; A5: dom (mlt (y,z)) = Seg (len (mlt (y2,z2))) by FINSEQ_1:def_3 .= Seg (len x) by CARD_1:def_7 ; then A6: dom (mlt (y,z)) = Seg (len ((mlt (x2,z2)) + (mlt (y2,z2)))) by CARD_1:def_7 .= dom ((mlt (x2,z2)) + (mlt (y2,z2))) by FINSEQ_1:def_3 ; A7: dom x = Seg (len x) by FINSEQ_1:def_3; A8: dom y = Seg (len x) by A1, FINSEQ_1:def_3; A9: dom (mlt (x,z)) = Seg (len (mlt (x2,z2))) by FINSEQ_1:def_3 .= Seg (len x) by CARD_1:def_7 ; then A10: dom (mlt (x,z)) = Seg (len ((mlt (x2,z2)) + (mlt (y2,z2)))) by CARD_1:def_7 .= dom ((mlt (x2,z2)) + (mlt (y2,z2))) by FINSEQ_1:def_3 ; A11: for i being Nat st i in dom (mlt ((x + y),z)) holds (mlt ((x + y),z)) . i = ((mlt (x,z)) + (mlt (y,z))) . i proof let i be Nat; ::_thesis: ( i in dom (mlt ((x + y),z)) implies (mlt ((x + y),z)) . i = ((mlt (x,z)) + (mlt (y,z))) . i ) A12: ( rng x c= the carrier of K & rng y c= the carrier of K ) by FINSEQ_1:def_4; A13: ( rng z c= the carrier of K & rng (x + y) c= the carrier of K ) by FINSEQ_1:def_4; dom the multF of K = [: the carrier of K, the carrier of K:] by FUNCT_2:def_1; then ( mlt ((x + y),z) = the multF of K .: ((x + y),z) & [:(rng (x + y)),(rng z):] c= dom the multF of K ) by A13, FVSUM_1:def_7, ZFMISC_1:96; then A14: dom (mlt ((x + y),z)) = (dom (x + y)) /\ (dom z) by FUNCOP_1:69; assume A15: i in dom (mlt ((x + y),z)) ; ::_thesis: (mlt ((x + y),z)) . i = ((mlt (x,z)) + (mlt (y,z))) . i then i in dom z by A14, XBOOLE_0:def_4; then A16: z . i in rng z by FUNCT_1:def_3; len (x2 + y2) = len x by CARD_1:def_7; then A17: dom (x2 + y2) = Seg (len x) by FINSEQ_1:def_3; then A18: i in Seg (len x) by A15, A14, XBOOLE_0:def_4; then A19: (x + y) . i in rng (x + y) by A17, FUNCT_1:def_3; i in dom y by A1, A18, FINSEQ_1:def_3; then A20: y . i in rng y by FUNCT_1:def_3; A21: i in dom x by A18, FINSEQ_1:def_3; then x . i in rng x by FUNCT_1:def_3; then reconsider a = x . i, b = y . i, d = (x + y) . i, e = z . i as Element of K by A12, A13, A20, A16, A19; dom <:y,z:> = (dom x) /\ (dom x) by A8, A3, A7, FUNCT_3:def_7 .= dom x ; then A22: i in dom <:y,z:> by A18, FINSEQ_1:def_3; dom [:y,z:] = [:(dom y),(dom z):] by FUNCT_3:def_8; then A23: [i,i] in dom [:y,z:] by A8, A3, A15, A17, A14, ZFMISC_1:87; dom [:y,z:] = [:(dom y),(dom z):] by FUNCT_3:def_8; then A24: [i,i] in dom [:y,z:] by A8, A3, A15, A17, A14, ZFMISC_1:87; dom the multF of K = [: the carrier of K, the carrier of K:] by FUNCT_2:def_1; then [b,e] in dom the multF of K by ZFMISC_1:87; then ( dom ( the multF of K * (y,z)) = dom ( the multF of K * [:y,z:]) & [:y,z:] . (i,i) in dom the multF of K ) by A8, A3, A15, A17, A14, FINSEQOP:def_4, FUNCT_3:def_8; then [i,i] in dom ( the multF of K * (y,z)) by A24, FUNCT_1:11; then A25: b * e = ( the multF of K * (y,z)) . (i,i) by FINSEQOP:77 .= ( the multF of K * [:y,z:]) . (i,i) by FINSEQOP:def_4 .= the multF of K . ([:y,z:] . (i,i)) by A23, FUNCT_1:13 .= the multF of K . ((y . i),(z . i)) by A8, A3, A15, A17, A14, FUNCT_3:def_8 .= the multF of K . (<:y,z:> . i) by A8, A3, A15, A17, A14, FUNCT_3:49 .= ( the multF of K * <:y,z:>) . i by A22, FUNCT_1:13 .= ( the multF of K .: (y,z)) . i by FUNCOP_1:def_3 .= (mlt (y,z)) . i by FVSUM_1:def_7 ; dom <:(x + y),z:> = (dom (x + y)) /\ (dom z) by FUNCT_3:def_7 .= dom x by A3, A4, FINSEQ_1:def_3 ; then A26: i in dom <:(x + y),z:> by A18, FINSEQ_1:def_3; A27: (mlt ((x + y),z)) . i = ( the multF of K .: ((x + y),z)) . i by FVSUM_1:def_7 .= ( the multF of K * <:(x + y),z:>) . i by FUNCOP_1:def_3 .= the multF of K . (<:(x + y),z:> . i) by A26, FUNCT_1:13 .= d * e by A4, A15, A14, FUNCT_3:49 ; A28: dom <:(mlt (x,z)),(mlt (y,z)):> = (dom (mlt (x,z))) /\ (dom (mlt (y,z))) by FUNCT_3:def_7 .= dom x by A9, A5, FINSEQ_1:def_3 ; A29: dom <:x,y:> = (dom x) /\ (dom y) by FUNCT_3:def_7 .= dom x by A8, A7 ; A30: the addF of K .: ((mlt (x,z)),(mlt (y,z))) = (mlt (x,z)) + (mlt (y,z)) by FVSUM_1:def_3; dom [:x,z:] = [:(dom x),(dom z):] by FUNCT_3:def_8; then A31: [i,i] in dom [:x,z:] by A3, A7, A15, A17, A14, ZFMISC_1:87; dom [:x,z:] = [:(dom x),(dom z):] by FUNCT_3:def_8; then A32: [i,i] in dom [:x,z:] by A3, A7, A15, A17, A14, ZFMISC_1:87; dom <:x,z:> = (dom x) /\ (dom x) by A3, A7, FUNCT_3:def_7 .= dom x ; then A33: i in dom <:x,z:> by A18, FINSEQ_1:def_3; A34: (x + y) . i = ( the addF of K .: (x,y)) . i by FVSUM_1:def_3 .= ( the addF of K * <:x,y:>) . i by FUNCOP_1:def_3 .= the addF of K . (<:x,y:> . i) by A21, A29, FUNCT_1:13 .= a + b by A8, A7, A18, FUNCT_3:49 ; dom the multF of K = [: the carrier of K, the carrier of K:] by FUNCT_2:def_1; then [a,e] in dom the multF of K by ZFMISC_1:87; then ( dom ( the multF of K * (x,z)) = dom ( the multF of K * [:x,z:]) & [:x,z:] . (i,i) in dom the multF of K ) by A3, A7, A15, A17, A14, FINSEQOP:def_4, FUNCT_3:def_8; then [i,i] in dom ( the multF of K * (x,z)) by A32, FUNCT_1:11; then a * e = ( the multF of K * (x,z)) . (i,i) by FINSEQOP:77 .= ( the multF of K * [:x,z:]) . (i,i) by FINSEQOP:def_4 .= the multF of K . ([:x,z:] . (i,i)) by A31, FUNCT_1:13 .= the multF of K . ((x . i),(z . i)) by A3, A7, A15, A17, A14, FUNCT_3:def_8 .= the multF of K . (<:x,z:> . i) by A3, A7, A15, A17, A14, FUNCT_3:49 .= ( the multF of K * <:x,z:>) . i by A33, FUNCT_1:13 .= ( the multF of K .: (x,z)) . i by FUNCOP_1:def_3 .= (mlt (x,z)) . i by FVSUM_1:def_7 ; then (a * e) + (b * e) = the addF of K . (<:(mlt (x,z)),(mlt (y,z)):> . i) by A9, A10, A6, A18, A25, FUNCT_3:49 .= ( the addF of K * <:(mlt (x,z)),(mlt (y,z)):>) . i by A21, A28, FUNCT_1:13 .= ((mlt (x,z)) + (mlt (y,z))) . i by A30, FUNCOP_1:def_3 ; hence (mlt ((x + y),z)) . i = ((mlt (x,z)) + (mlt (y,z))) . i by A34, A27, VECTSP_1:def_7; ::_thesis: verum end; dom (mlt ((x + y),z)) = Seg (len (mlt ((x2 + y2),z2))) by FINSEQ_1:def_3 .= Seg (len x) by CARD_1:def_7 .= Seg (len ((mlt (x2,z2)) + (mlt (y2,z2)))) by CARD_1:def_7 .= dom ((mlt (x2,z2)) + (mlt (y2,z2))) by FINSEQ_1:def_3 ; hence mlt ((x + y),z) = (mlt (x,z)) + (mlt (y,z)) by A11, FINSEQ_1:13; ::_thesis: verum end; theorem Th57: :: MATRIX_4:57 for K being Field for x, y, z being FinSequence of K st len x = len y & len y = len z holds mlt (z,(x + y)) = (mlt (z,x)) + (mlt (z,y)) proof let K be Field; ::_thesis: for x, y, z being FinSequence of K st len x = len y & len y = len z holds mlt (z,(x + y)) = (mlt (z,x)) + (mlt (z,y)) let x, y, z be FinSequence of K; ::_thesis: ( len x = len y & len y = len z implies mlt (z,(x + y)) = (mlt (z,x)) + (mlt (z,y)) ) assume A1: ( len x = len y & len y = len z ) ; ::_thesis: mlt (z,(x + y)) = (mlt (z,x)) + (mlt (z,y)) then reconsider x2 = x, y2 = y, z2 = z as Element of (len x) -tuples_on the carrier of K by FINSEQ_2:92; mlt (z,(x + y)) = mlt ((x2 + y2),z2) by FVSUM_1:63 .= (mlt (x2,z2)) + (mlt (y,z)) by A1, Th56 .= (mlt (z,x)) + (mlt (y2,z2)) by FVSUM_1:63 ; hence mlt (z,(x + y)) = (mlt (z,x)) + (mlt (z,y)) by FVSUM_1:63; ::_thesis: verum end; theorem :: MATRIX_4:58 for D being non empty set for M being Matrix of D st len M > 0 holds for n being Element of NAT holds ( M is Matrix of n, width M,D iff n = len M ) by MATRIX_1:20, MATRIX_1:def_2; theorem Th59: :: MATRIX_4:59 for i being Nat for K being Field for j being Element of NAT for A, B being Matrix of K st width A = width B & ex j being Element of NAT st [i,j] in Indices A holds Line ((A + B),i) = (Line (A,i)) + (Line (B,i)) proof let i be Nat; ::_thesis: for K being Field for j being Element of NAT for A, B being Matrix of K st width A = width B & ex j being Element of NAT st [i,j] in Indices A holds Line ((A + B),i) = (Line (A,i)) + (Line (B,i)) let K be Field; ::_thesis: for j being Element of NAT for A, B being Matrix of K st width A = width B & ex j being Element of NAT st [i,j] in Indices A holds Line ((A + B),i) = (Line (A,i)) + (Line (B,i)) let j be Element of NAT ; ::_thesis: for A, B being Matrix of K st width A = width B & ex j being Element of NAT st [i,j] in Indices A holds Line ((A + B),i) = (Line (A,i)) + (Line (B,i)) let A, B be Matrix of K; ::_thesis: ( width A = width B & ex j being Element of NAT st [i,j] in Indices A implies Line ((A + B),i) = (Line (A,i)) + (Line (B,i)) ) assume that A1: width A = width B and A2: ex j being Element of NAT st [i,j] in Indices A ; ::_thesis: Line ((A + B),i) = (Line (A,i)) + (Line (B,i)) reconsider a = Line (A,i), b = Line (B,i) as Element of (width A) -tuples_on the carrier of K by A1; A3: width (A + B) = width A by MATRIX_3:def_3; i in dom A by A2, ZFMISC_1:87; then A4: i in Seg (len A) by FINSEQ_1:def_3; A5: len (A + B) = len A by MATRIX_3:def_3; then A6: Indices (A + B) = Indices A by A3, Th55; A7: for k being Nat st 1 <= k & k <= len (Line ((A + B),i)) holds (Line ((A + B),i)) . k = ((Line (A,i)) + (Line (B,i))) . k proof let k be Nat; ::_thesis: ( 1 <= k & k <= len (Line ((A + B),i)) implies (Line ((A + B),i)) . k = ((Line (A,i)) + (Line (B,i))) . k ) assume A8: ( 1 <= k & k <= len (Line ((A + B),i)) ) ; ::_thesis: (Line ((A + B),i)) . k = ((Line (A,i)) + (Line (B,i))) . k A9: len (Line ((A + B),i)) = width A by A3, MATRIX_1:def_7; then A10: k in Seg (width (A + B)) by A3, A8, FINSEQ_1:1; len (Line (B,i)) = width B by MATRIX_1:def_7; then k in Seg (len (Line (B,i))) by A1, A8, A9, FINSEQ_1:1; then k in dom (Line (B,i)) by FINSEQ_1:def_3; then reconsider e = (Line (B,i)) . k as Element of K by FINSEQ_2:11; i in dom (A + B) by A5, A4, FINSEQ_1:def_3; then A11: [i,k] in Indices (A + B) by A10, ZFMISC_1:87; A12: (Line ((A + B),i)) . k = (A + B) * (i,k) by A10, MATRIX_1:def_7 .= (A * (i,k)) + (B * (i,k)) by A6, A11, MATRIX_3:def_3 ; A13: len (Line (A,i)) = width A by MATRIX_1:def_7; then A14: k in Seg (len (Line (A,i))) by A8, A9, FINSEQ_1:1; then k in dom (Line (A,i)) by FINSEQ_1:def_3; then reconsider d = (Line (A,i)) . k as Element of K by FINSEQ_2:11; len ((Line (A,i)) + (Line (B,i))) = len (a + b) .= width A by CARD_1:def_7 .= len (Line (A,i)) by CARD_1:def_7 ; then k in dom ((Line (A,i)) + (Line (B,i))) by A14, FINSEQ_1:def_3; then A15: ((Line (A,i)) + (Line (B,i))) . k = d + e by FVSUM_1:17; (Line (A,i)) . k = A * (i,k) by A13, A14, MATRIX_1:def_7; hence (Line ((A + B),i)) . k = ((Line (A,i)) + (Line (B,i))) . k by A1, A13, A12, A14, A15, MATRIX_1:def_7; ::_thesis: verum end; A16: len ((Line (A,i)) + (Line (B,i))) = len (a + b) .= width A by CARD_1:def_7 ; len (Line ((A + B),i)) = width A by A3, MATRIX_1:def_7; hence Line ((A + B),i) = (Line (A,i)) + (Line (B,i)) by A16, A7, FINSEQ_1:14; ::_thesis: verum end; theorem Th60: :: MATRIX_4:60 for K being Field for j being Nat for A, B being Matrix of K st len A = len B & ex i being Nat st [i,j] in Indices A holds Col ((A + B),j) = (Col (A,j)) + (Col (B,j)) proof let K be Field; ::_thesis: for j being Nat for A, B being Matrix of K st len A = len B & ex i being Nat st [i,j] in Indices A holds Col ((A + B),j) = (Col (A,j)) + (Col (B,j)) let j be Nat; ::_thesis: for A, B being Matrix of K st len A = len B & ex i being Nat st [i,j] in Indices A holds Col ((A + B),j) = (Col (A,j)) + (Col (B,j)) let A, B be Matrix of K; ::_thesis: ( len A = len B & ex i being Nat st [i,j] in Indices A implies Col ((A + B),j) = (Col (A,j)) + (Col (B,j)) ) A1: len (A + B) = len A by MATRIX_3:def_3; assume A2: len A = len B ; ::_thesis: ( for i being Nat holds not [i,j] in Indices A or Col ((A + B),j) = (Col (A,j)) + (Col (B,j)) ) then reconsider a = Col (A,j), b = Col (B,j) as Element of (len A) -tuples_on the carrier of K ; given i being Nat such that A3: [i,j] in Indices A ; ::_thesis: Col ((A + B),j) = (Col (A,j)) + (Col (B,j)) A4: width (A + B) = width A by MATRIX_3:def_3; then A5: Indices (A + B) = Indices A by A1, Th55; A6: for k being Nat st 1 <= k & k <= len (Col ((A + B),j)) holds (Col ((A + B),j)) . k = ((Col (A,j)) + (Col (B,j))) . k proof let k be Nat; ::_thesis: ( 1 <= k & k <= len (Col ((A + B),j)) implies (Col ((A + B),j)) . k = ((Col (A,j)) + (Col (B,j))) . k ) assume A7: ( 1 <= k & k <= len (Col ((A + B),j)) ) ; ::_thesis: (Col ((A + B),j)) . k = ((Col (A,j)) + (Col (B,j))) . k A8: len (Col ((A + B),j)) = len A by A1, MATRIX_1:def_8; then k in Seg (len A) by A7, FINSEQ_1:1; then A9: k in dom (A + B) by A1, FINSEQ_1:def_3; len (Col (B,j)) = len B by MATRIX_1:def_8; then k in Seg (len (Col (B,j))) by A2, A7, A8, FINSEQ_1:1; then k in dom (Col (B,j)) by FINSEQ_1:def_3; then reconsider e = (Col (B,j)) . k as Element of K by FINSEQ_2:11; A10: dom A = Seg (len A) by FINSEQ_1:def_3 .= dom B by A2, FINSEQ_1:def_3 ; A11: len (Col (A,j)) = len A by MATRIX_1:def_8; then A12: k in Seg (len (Col (A,j))) by A7, A8, FINSEQ_1:1; then k in dom (Col (A,j)) by FINSEQ_1:def_3; then reconsider d = (Col (A,j)) . k as Element of K by FINSEQ_2:11; len ((Col (A,j)) + (Col (B,j))) = len (a + b) .= len A by CARD_1:def_7 .= len (Col (A,j)) by CARD_1:def_7 ; then k in dom ((Col (A,j)) + (Col (B,j))) by A12, FINSEQ_1:def_3; then A13: ((Col (A,j)) + (Col (B,j))) . k = d + e by FVSUM_1:17; j in Seg (width (A + B)) by A3, A4, ZFMISC_1:87; then A14: [k,j] in Indices (A + B) by A9, ZFMISC_1:87; A15: (Col ((A + B),j)) . k = (A + B) * (k,j) by A9, MATRIX_1:def_8 .= (A * (k,j)) + (B * (k,j)) by A5, A14, MATRIX_3:def_3 ; A16: k in dom A by A11, A12, FINSEQ_1:def_3; then (Col (A,j)) . k = A * (k,j) by MATRIX_1:def_8; hence (Col ((A + B),j)) . k = ((Col (A,j)) + (Col (B,j))) . k by A15, A13, A10, A16, MATRIX_1:def_8; ::_thesis: verum end; A17: len ((Col (A,j)) + (Col (B,j))) = len (a + b) .= len A by CARD_1:def_7 ; len (Col ((A + B),j)) = len A by A1, MATRIX_1:def_8; hence Col ((A + B),j) = (Col (A,j)) + (Col (B,j)) by A17, A6, FINSEQ_1:14; ::_thesis: verum end; theorem Th61: :: MATRIX_4:61 for V1 being Field for P1, P2 being FinSequence of V1 st len P1 = len P2 holds Sum (P1 + P2) = (Sum P1) + (Sum P2) proof let V1 be Field; ::_thesis: for P1, P2 being FinSequence of V1 st len P1 = len P2 holds Sum (P1 + P2) = (Sum P1) + (Sum P2) let P1, P2 be FinSequence of V1; ::_thesis: ( len P1 = len P2 implies Sum (P1 + P2) = (Sum P1) + (Sum P2) ) assume len P1 = len P2 ; ::_thesis: Sum (P1 + P2) = (Sum P1) + (Sum P2) then reconsider R1 = P1, R2 = P2 as Element of (len P1) -tuples_on the carrier of V1 by FINSEQ_2:92; thus Sum (P1 + P2) = Sum (R1 + R2) .= (Sum P1) + (Sum P2) by FVSUM_1:76 ; ::_thesis: verum end; theorem :: MATRIX_4:62 for K being Field for A, B, C being Matrix of K st len B = len C & width B = width C & width A = len B & len A > 0 & len B > 0 holds A * (B + C) = (A * B) + (A * C) proof let K be Field; ::_thesis: for A, B, C being Matrix of K st len B = len C & width B = width C & width A = len B & len A > 0 & len B > 0 holds A * (B + C) = (A * B) + (A * C) let A, B, C be Matrix of K; ::_thesis: ( len B = len C & width B = width C & width A = len B & len A > 0 & len B > 0 implies A * (B + C) = (A * B) + (A * C) ) assume that A1: len B = len C and A2: width B = width C and A3: width A = len B and A4: len A > 0 and A5: len B > 0 ; ::_thesis: A * (B + C) = (A * B) + (A * C) A6: len (B + C) = len B by MATRIX_3:def_3; then A7: len (A * (B + C)) = len A by A3, MATRIX_3:def_4; A8: ( width (B + C) = width B & width (A * (B + C)) = width (B + C) ) by A3, A6, MATRIX_3:def_3, MATRIX_3:def_4; then reconsider M1 = A * (B + C) as Matrix of len A, width B,K by A4, A7, MATRIX_1:20; A9: ( len (A * B) = len A & width (A * B) = width B ) by A3, MATRIX_3:def_4; then A10: Indices M1 = Indices (A * B) by A7, A8, Th55; A11: ( len ((A * B) + (A * C)) = len (A * B) & width ((A * B) + (A * C)) = width (A * B) ) by MATRIX_3:def_3; then reconsider M2 = (A * B) + (A * C) as Matrix of len A, width B,K by A4, A9, MATRIX_1:20; ( len (A * C) = len A & width (A * C) = width C ) by A1, A3, MATRIX_3:def_4; then A12: Indices M1 = Indices (A * C) by A2, A7, A8, Th55; 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) ) len (Line (A,i)) = len B by A3, MATRIX_1:def_7; then A13: len (Line (A,i)) = len (Col (B,j)) by MATRIX_1:def_8; reconsider q1 = Line (A,i), q2 = Col (B,j), q3 = Col (C,j) as Element of (len B) -tuples_on the carrier of K by A1, A3; A14: len (mlt ((Line (A,i)),(Col (B,j)))) = len (mlt (q1,q2)) .= len B by CARD_1:def_7 .= len (mlt (q1,q3)) by CARD_1:def_7 .= len (mlt ((Line (A,i)),(Col (C,j)))) ; ( dom B = Seg (len B) & 1 + 0 <= len B ) by A5, FINSEQ_1:def_3, NAT_1:13; then A15: 1 in dom B by FINSEQ_1:1; len (Line (A,i)) = len C by A1, A3, MATRIX_1:def_7; then A16: len (Line (A,i)) = len (Col (C,j)) by MATRIX_1:def_8; assume A17: [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) = M2 * (i,j) then A18: M2 * (i,j) = ((A * B) * (i,j)) + ((A * C) * (i,j)) by A10, MATRIX_3:def_3 .= ((Line (A,i)) "*" (Col (B,j))) + ((A * C) * (i,j)) by A3, A10, A17, MATRIX_3:def_4 .= ((Line (A,i)) "*" (Col (B,j))) + ((Line (A,i)) "*" (Col (C,j))) by A1, A3, A12, A17, MATRIX_3:def_4 .= ((Line (A,i)) "*" (Col (B,j))) + (Sum (mlt ((Line (A,i)),(Col (C,j))))) by FVSUM_1:def_9 .= (Sum (mlt ((Line (A,i)),(Col (B,j))))) + (Sum (mlt ((Line (A,i)),(Col (C,j))))) by FVSUM_1:def_9 ; j in Seg (width B) by A8, A17, ZFMISC_1:87; then A19: [1,j] in Indices B by A15, ZFMISC_1:87; M1 * (i,j) = (Line (A,i)) "*" (Col ((B + C),j)) by A3, A6, A17, MATRIX_3:def_4 .= Sum (mlt ((Line (A,i)),(Col ((B + C),j)))) by FVSUM_1:def_9 .= Sum (mlt ((Line (A,i)),((Col (B,j)) + (Col (C,j))))) by A1, A19, Th60 .= Sum ((mlt ((Line (A,i)),(Col (B,j)))) + (mlt ((Line (A,i)),(Col (C,j))))) by A13, A16, Th57 .= (Sum (mlt ((Line (A,i)),(Col (B,j))))) + (Sum (mlt ((Line (A,i)),(Col (C,j))))) by A14, Th61 ; hence M1 * (i,j) = M2 * (i,j) by A18; ::_thesis: verum end; hence A * (B + C) = (A * B) + (A * C) by A7, A8, A9, A11, MATRIX_1:21; ::_thesis: verum end; theorem :: MATRIX_4:63 for K being Field for A, B, C being Matrix of K st len B = len C & width B = width C & len A = width B & len B > 0 & len A > 0 holds (B + C) * A = (B * A) + (C * A) proof let K be Field; ::_thesis: for A, B, C being Matrix of K st len B = len C & width B = width C & len A = width B & len B > 0 & len A > 0 holds (B + C) * A = (B * A) + (C * A) let A, B, C be Matrix of K; ::_thesis: ( len B = len C & width B = width C & len A = width B & len B > 0 & len A > 0 implies (B + C) * A = (B * A) + (C * A) ) assume that A1: len B = len C and A2: width B = width C and A3: len A = width B and A4: len B > 0 and A5: len A > 0 ; ::_thesis: (B + C) * A = (B * A) + (C * A) A6: width (B + C) = width B by MATRIX_3:def_3; then A7: width ((B + C) * A) = width A by A3, MATRIX_3:def_4; len (B + C) = len B by MATRIX_3:def_3; then A8: len ((B + C) * A) = len B by A3, A6, MATRIX_3:def_4; then reconsider M1 = (B + C) * A as Matrix of len B, width A,K by A4, A7, MATRIX_1:20; A9: len (B * A) = len B by A3, MATRIX_3:def_4; A10: width (B * A) = width A by A3, MATRIX_3:def_4; then A11: Indices M1 = Indices (B * A) by A8, A7, A9, Th55; A12: ( len ((B * A) + (C * A)) = len (B * A) & width ((B * A) + (C * A)) = width (B * A) ) by MATRIX_3:def_3; then reconsider M2 = (B * A) + (C * A) as Matrix of len B, width A,K by A4, A9, A10, MATRIX_1:20; ( len (C * A) = len C & width (C * A) = width A ) by A2, A3, MATRIX_3:def_4; then A13: Indices M1 = Indices (C * A) by A1, A8, A7, Th55; 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) ) len (Col (A,j)) = width B by A3, MATRIX_1:def_8; then A14: len (Col (A,j)) = len (Line (B,i)) by MATRIX_1:def_7; reconsider q1 = Line (B,i), q2 = Line (C,i), q3 = Col (A,j) as Element of (len A) -tuples_on the carrier of K by A2, A3; A15: len (mlt ((Line (B,i)),(Col (A,j)))) = len (mlt (q1,q3)) .= len A by CARD_1:def_7 .= len (mlt (q2,q3)) by CARD_1:def_7 .= len (mlt ((Line (C,i)),(Col (A,j)))) ; 1 + 0 <= width B by A3, A5, NAT_1:13; then A16: 1 in Seg (width B) by FINSEQ_1:1; len (Col (A,j)) = width C by A2, A3, MATRIX_1:def_8; then A17: len (Col (A,j)) = len (Line (C,i)) by MATRIX_1:def_7; assume A18: [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) = M2 * (i,j) then A19: M2 * (i,j) = ((B * A) * (i,j)) + ((C * A) * (i,j)) by A11, MATRIX_3:def_3 .= ((Line (B,i)) "*" (Col (A,j))) + ((C * A) * (i,j)) by A3, A11, A18, MATRIX_3:def_4 .= ((Line (B,i)) "*" (Col (A,j))) + ((Line (C,i)) "*" (Col (A,j))) by A2, A3, A13, A18, MATRIX_3:def_4 .= ((Line (B,i)) "*" (Col (A,j))) + (Sum (mlt ((Line (C,i)),(Col (A,j))))) by FVSUM_1:def_9 .= (Sum (mlt ((Line (B,i)),(Col (A,j))))) + (Sum (mlt ((Line (C,i)),(Col (A,j))))) by FVSUM_1:def_9 ; i in dom (B * A) by A11, A18, ZFMISC_1:87; then i in Seg (len B) by A9, FINSEQ_1:def_3; then i in dom B by FINSEQ_1:def_3; then A20: [i,1] in Indices B by A16, ZFMISC_1:87; M1 * (i,j) = (Line ((B + C),i)) "*" (Col (A,j)) by A3, A6, A18, MATRIX_3:def_4 .= Sum (mlt ((Line ((B + C),i)),(Col (A,j)))) by FVSUM_1:def_9 .= Sum (mlt (((Line (B,i)) + (Line (C,i))),(Col (A,j)))) by A2, A20, Th59 .= Sum ((mlt ((Line (B,i)),(Col (A,j)))) + (mlt ((Line (C,i)),(Col (A,j))))) by A14, A17, Th56 .= (Sum (mlt ((Line (B,i)),(Col (A,j))))) + (Sum (mlt ((Line (C,i)),(Col (A,j))))) by A15, Th61 ; hence M1 * (i,j) = M2 * (i,j) by A19; ::_thesis: verum end; hence (B + C) * A = (B * A) + (C * A) by A8, A7, A9, A10, A12, MATRIX_1:21; ::_thesis: verum end; theorem :: MATRIX_4:64 for K being Field for n, m, k being Element of NAT for M1 being Matrix of n,m,K for M2 being Matrix of m,k,K st width M1 = len M2 & 0 < len M1 & 0 < len M2 holds M1 * M2 is Matrix of n,k,K proof let K be Field; ::_thesis: for n, m, k being Element of NAT for M1 being Matrix of n,m,K for M2 being Matrix of m,k,K st width M1 = len M2 & 0 < len M1 & 0 < len M2 holds M1 * M2 is Matrix of n,k,K let n, m, k be Element of NAT ; ::_thesis: for M1 being Matrix of n,m,K for M2 being Matrix of m,k,K st width M1 = len M2 & 0 < len M1 & 0 < len M2 holds M1 * M2 is Matrix of n,k,K let M1 be Matrix of n,m,K; ::_thesis: for M2 being Matrix of m,k,K st width M1 = len M2 & 0 < len M1 & 0 < len M2 holds M1 * M2 is Matrix of n,k,K let M2 be Matrix of m,k,K; ::_thesis: ( width M1 = len M2 & 0 < len M1 & 0 < len M2 implies M1 * M2 is Matrix of n,k,K ) assume that A1: width M1 = len M2 and A2: 0 < len M1 and A3: 0 < len M2 ; ::_thesis: M1 * M2 is Matrix of n,k,K width M1 = m by A1, MATRIX_1:def_2; then A4: ( len M1 = n & width M2 = k ) by A1, A3, MATRIX_1:20, MATRIX_1:def_2; ( len (M1 * M2) = len M1 & width (M1 * M2) = width M2 ) by A1, MATRIX_3:def_4; hence M1 * M2 is Matrix of n,k,K by A2, A4, MATRIX_1:20; ::_thesis: verum end;