let n be Nat; :: thesis: for K being Field

for M1, M2 being Matrix of n,K holds (M1 + M2) @ = (M1 @) + (M2 @)

let K be Field; :: thesis: for M1, M2 being Matrix of n,K holds (M1 + M2) @ = (M1 @) + (M2 @)

let M1, M2 be Matrix of n,K; :: thesis: (M1 + M2) @ = (M1 @) + (M2 @)

for i, j being Nat st [i,j] in Indices ((M1 + M2) @) holds

((M1 + M2) @) * (i,j) = ((M1 @) + (M2 @)) * (i,j)

for M1, M2 being Matrix of n,K holds (M1 + M2) @ = (M1 @) + (M2 @)

let K be Field; :: thesis: for M1, M2 being Matrix of n,K holds (M1 + M2) @ = (M1 @) + (M2 @)

let M1, M2 be Matrix of n,K; :: thesis: (M1 + M2) @ = (M1 @) + (M2 @)

for i, j being Nat st [i,j] in Indices ((M1 + M2) @) holds

((M1 + M2) @) * (i,j) = ((M1 @) + (M2 @)) * (i,j)

proof

hence
(M1 + M2) @ = (M1 @) + (M2 @)
by MATRIX_0:27; :: thesis: verum
let i, j be Nat; :: thesis: ( [i,j] in Indices ((M1 + M2) @) implies ((M1 + M2) @) * (i,j) = ((M1 @) + (M2 @)) * (i,j) )

assume [i,j] in Indices ((M1 + M2) @) ; :: thesis: ((M1 + M2) @) * (i,j) = ((M1 @) + (M2 @)) * (i,j)

then A1: [i,j] in [:(Seg n),(Seg n):] by MATRIX_0:24;

then A2: [i,j] in Indices (M1 @) by MATRIX_0:24;

( i in Seg n & j in Seg n ) by A1, ZFMISC_1:87;

then A3: [j,i] in [:(Seg n),(Seg n):] by ZFMISC_1:87;

then A4: [j,i] in Indices M1 by MATRIX_0:24;

A5: [j,i] in Indices M2 by A3, MATRIX_0:24;

[j,i] in Indices (M1 + M2) by A3, MATRIX_0:24;

then ((M1 + M2) @) * (i,j) = (M1 + M2) * (j,i) by MATRIX_0:def 6

.= (M1 * (j,i)) + (M2 * (j,i)) by A4, MATRIX_3:def 3

.= ((M1 @) * (i,j)) + (M2 * (j,i)) by A4, MATRIX_0:def 6

.= ((M1 @) * (i,j)) + ((M2 @) * (i,j)) by A5, MATRIX_0:def 6

.= ((M1 @) + (M2 @)) * (i,j) by A2, MATRIX_3:def 3 ;

hence ((M1 + M2) @) * (i,j) = ((M1 @) + (M2 @)) * (i,j) ; :: thesis: verum

end;assume [i,j] in Indices ((M1 + M2) @) ; :: thesis: ((M1 + M2) @) * (i,j) = ((M1 @) + (M2 @)) * (i,j)

then A1: [i,j] in [:(Seg n),(Seg n):] by MATRIX_0:24;

then A2: [i,j] in Indices (M1 @) by MATRIX_0:24;

( i in Seg n & j in Seg n ) by A1, ZFMISC_1:87;

then A3: [j,i] in [:(Seg n),(Seg n):] by ZFMISC_1:87;

then A4: [j,i] in Indices M1 by MATRIX_0:24;

A5: [j,i] in Indices M2 by A3, MATRIX_0:24;

[j,i] in Indices (M1 + M2) by A3, MATRIX_0:24;

then ((M1 + M2) @) * (i,j) = (M1 + M2) * (j,i) by MATRIX_0:def 6

.= (M1 * (j,i)) + (M2 * (j,i)) by A4, MATRIX_3:def 3

.= ((M1 @) * (i,j)) + (M2 * (j,i)) by A4, MATRIX_0:def 6

.= ((M1 @) * (i,j)) + ((M2 @) * (i,j)) by A5, MATRIX_0:def 6

.= ((M1 @) + (M2 @)) * (i,j) by A2, MATRIX_3:def 3 ;

hence ((M1 + M2) @) * (i,j) = ((M1 @) + (M2 @)) * (i,j) ; :: thesis: verum