let R be Ring; :: thesis: for n being Nat
for A being Matrix of n,R st ( for B being Matrix of n,R holds A * B = B * A ) holds
ex z being Element of R st
( z in center R & A = z * (1. (R,n)) )
let n be Nat; :: thesis: for A being Matrix of n,R st ( for B being Matrix of n,R holds A * B = B * A ) holds
ex z being Element of R st
( z in center R & A = z * (1. (R,n)) )
let A be Matrix of n,R; :: thesis: ( ( for B being Matrix of n,R holds A * B = B * A ) implies ex z being Element of R st
( z in center R & A = z * (1. (R,n)) ) )
assume A1: for B being Matrix of n,R holds A * B = B * A ; :: thesis: ex z being Element of R st
( z in center R & A = z * (1. (R,n)) )
A2: for i, j being Nat st [i,j] in Indices A & i <> j holds
A * (i,j) = 0. R

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices A & i <> j implies A * (i,j) = 0. R )
assume A3: [i,j] in Indices A ; :: thesis: ( not i <> j or A * (i,j) = 0. R )
assume A4: i <> j ; :: thesis: A * (i,j) = 0. R
[i,j] in [:(Seg n),(Seg n):] by A3, MATRIX_0:24;
then i in Seg n by ZFMISC_1:87;
then [i,i] in [:(Seg n),(Seg n):] by ZFMISC_1:87;
then A5: [i,i] in Indices (canMat (i,i,n,R)) by MATRIX_0:24;
hence 0. R = (A * (canMat (i,i,n,R))) * (i,j) by A3, A4, Th55
.= ((canMat (i,i,n,R)) * A) * (i,j) by A1
.= A * (i,j) by A3, A5, Th54 ;
:: thesis: verum

end;

A6: for i, j being Nat st [i,j] in Indices A holds
A * (i,i) = A * (j,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices A implies A * (i,i) = A * (j,j) )
assume A7: [i,j] in Indices A ; :: thesis: A * (i,i) = A * (j,j)
A8: Indices A = [:(Seg n),(Seg n):] by MATRIX_0:24
.= Indices (canMat (i,j,n,R)) by MATRIX_0:24 ;
hence A * (i,i) = (A * (canMat (i,j,n,R))) * (i,j) by A7, Th55
.= ((canMat (i,j,n,R)) * A) * (i,j) by A1
.= A * (j,j) by A7, A8, Th54 ;
:: thesis: verum

end;

per cases ( n = 0 or n > 0 ) ;

suppose A9: n = 0 ; :: thesis: ex z being Element of R st
( z in center R & A = z * (1. (R,n)) )

take z = 1. R; :: thesis: ( z in center R & A = z * (1. (R,n)) )
A10: z = 1_ R ;
A11: ( len A = len (z * (1. (R,n))) & width A = width (z * (1. (R,n))) )

proof

thus len A = n by MATRIX_0:25
.= len (z * (1. (R,n))) by MATRIX_0:25 ; :: thesis: width A = width (z * (1. (R,n)))
thus width A = n by MATRIX_0:24
.= width (z * (1. (R,n))) by MATRIX_0:24 ; :: thesis: verum

end;

for i, j being Nat st [i,j] in Indices A holds
A * (i,j) = (z * (1. (R,n))) * (i,j) by A9, MATRIX_0:22;
hence ( z in center R & A = z * (1. (R,n)) ) by A10, A11, MATRIX_0:21, WEDDWITT:19; :: thesis: verum

end;

suppose n > 0 ; :: thesis: ex z being Element of R st
( z in center R & A = z * (1. (R,n)) )

then 0 < 0 + n ;
then 1 <= n by NAT_1:19;
then A12: [1,1] in Indices A by MATRIX_0:31;
take z = A * (1,1); :: thesis: ( z in center R & A = z * (1. (R,n)) )
A13: ( len A = len (z * (1. (R,n))) & width A = width (z * (1. (R,n))) )

proof

thus len A = n by MATRIX_0:25
.= len (z * (1. (R,n))) by MATRIX_0:25 ; :: thesis: width A = width (z * (1. (R,n)))
thus width A = n by MATRIX_0:24
.= width (z * (1. (R,n))) by MATRIX_0:24 ; :: thesis: verum

end;

for i, j being Nat st [i,j] in Indices A holds
A * (i,j) = (z * (1. (R,n))) * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices A implies A * (i,j) = (z * (1. (R,n))) * (i,j) )
assume A14: [i,j] in Indices A ; :: thesis: A * (i,j) = (z * (1. (R,n))) * (i,j)
A15: Indices A = [:(Seg n),(Seg n):] by MATRIX_0:24
.= Indices (1. (R,n)) by MATRIX_0:24 ;

per cases ( i = j or i <> j ) ;

suppose A16: i = j ; :: thesis: A * (i,j) = (z * (1. (R,n))) * (i,j)

[1,i] in Indices A

proof

[1,1] in [:(Seg n),(Seg n):] by A12, MATRIX_0:24;
then A17: 1 in Seg n by ZFMISC_1:87;
[i,j] in [:(Seg n),(Seg n):] by A14, MATRIX_0:24;
then i in Seg n by ZFMISC_1:87;
then [1,i] in [:(Seg n),(Seg n):] by A17, ZFMISC_1:87;
hence [1,i] in Indices A by MATRIX_0:24; :: thesis: verum

end;

hence A * (i,j) = z * (1. R) by A6, A16
.= z * ((1. (R,n)) * (i,j)) by A14, A15, A16, MATRIX_1:def 3
.= (z * (1. (R,n))) * (i,j) by A14, A15, MATRIX_3:def 5 ;
:: thesis: verum

end;

suppose A18: i <> j ; :: thesis: A * (i,j) = (z * (1. (R,n))) * (i,j)

hence A * (i,j) = z * (0. R) by A2, A14
.= z * ((1. (R,n)) * (i,j)) by A14, A15, A18, MATRIX_1:def 3
.= (z * (1. (R,n))) * (i,j) by A14, A15, MATRIX_3:def 5 ;
:: thesis: verum

end;

end;

end;

then A19: A = z * (1. (R,n)) by A13, MATRIX_0:21;
for x being Element of R holds z * x = x * z

proof

let x be Element of R; :: thesis: z * x = x * z
A20: (x * z) * (1. (R,n)) = ((x * z) * (1. (R,n))) * (1. (R,n)) by MATRIX_3:19
.= ((x * (1. (R,n))) * z) * (1. (R,n)) by Th101
.= (x * (1. (R,n))) * (z * (1. (R,n))) by Th102
.= A * (x * (1. (R,n))) by A1, A19
.= ((z * (1. (R,n))) * x) * (1. (R,n)) by A19, Th102
.= ((z * x) * (1. (R,n))) * (1. (R,n)) by Th101
.= (z * x) * (1. (R,n)) by MATRIX_3:19 ;
A21: Indices (1. (R,n)) = [:(Seg n),(Seg n):] by MATRIX_0:24
.= Indices A by MATRIX_0:24 ;
thus x * z = (x * z) * (1. R)
.= (x * z) * ((1. (R,n)) * (1,1)) by A12, A21, MATRIX_1:def 3
.= ((x * z) * (1. (R,n))) * (1,1) by A12, A21, MATRIX_3:def 5
.= (z * x) * ((1. (R,n)) * (1,1)) by A12, A20, A21, MATRIX_3:def 5
.= (z * x) * (1. R) by A12, A21, MATRIX_1:def 3
.= z * x ; :: thesis: verum

end;

hence ( z in center R & A = z * (1. (R,n)) ) by A19, WEDDWITT:17; :: thesis: verum

end;

end;