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