let R be Ring; :: thesis: for n being Nat
for A being invertible Matrix of n,R st ( for B being invertible Matrix of n,R holds A * B = B * A ) holds
ex z being Element of R st A = z * (1. (R,n))
let n be Nat; :: thesis: for A being invertible Matrix of n,R st ( for B being invertible Matrix of n,R holds A * B = B * A ) holds
ex z being Element of R st A = z * (1. (R,n))
let A be invertible Matrix of n,R; :: thesis: ( ( for B being invertible Matrix of n,R holds A * B = B * A ) implies ex z being Element of R st A = z * (1. (R,n)) )
assume A1: for B being invertible Matrix of n,R holds A * B = B * A ; :: thesis: ex z being Element of R st A = z * (1. (R,n))
A2: for i, j being Nat st i <> j holds
A * (canMat (i,j,n,R)) = (canMat (i,j,n,R)) * A

proof

let i, j be Nat; :: thesis: ( i <> j implies A * (canMat (i,j,n,R)) = (canMat (i,j,n,R)) * A )
assume A3: i <> j ; :: thesis: A * (canMat (i,j,n,R)) = (canMat (i,j,n,R)) * A
(1. R) * (canMat (i,j,n,R)) = canMat (i,j,n,R) ;
then (1. (R,n)) + (canMat (i,j,n,R)) is invertible Matrix of n,R by A3, Th57;
then A * ((1. (R,n)) + (canMat (i,j,n,R))) = ((1. (R,n)) + (canMat (i,j,n,R))) * A by A1;
hence A * (canMat (i,j,n,R)) = (canMat (i,j,n,R)) * A by Th59; :: thesis: verum

end;

A4: 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 )
set i2 = i;
set j2 = i;
set i0 = j;
set j0 = i;
assume A5: [i,j] in Indices A ; :: thesis: ( not i <> j or A * (i,j) = 0. R )
assume A6: i <> j ; :: thesis: A * (i,j) = 0. R
[i,j] in [:(Seg n),(Seg n):] by A5, MATRIX_0:24;
then A7: ( i in Seg n & j in Seg n ) by ZFMISC_1:87;
then [j,i] in [:(Seg n),(Seg n):] by ZFMISC_1:87;
then A8: [j,i] in Indices (canMat (j,i,n,R)) by MATRIX_0:24;
[i,i] in [:(Seg n),(Seg n):] by A7, ZFMISC_1:87;
then A9: [i,i] in Indices A by MATRIX_0:24;
hence A * (i,j) = (A * (canMat (j,i,n,R))) * (i,i) by A8, Th55
.= ((canMat (j,i,n,R)) * A) * (i,i) by A2, A6
.= 0. R by A6, A8, A9, Th54 ;
:: thesis: verum

end;

A10: 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 A11: [i,j] in Indices A ; :: thesis: A * (i,i) = A * (j,j)

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

suppose i = j ; :: thesis: A * (i,i) = A * (j,j)

hence A * (i,i) = A * (j,j) ; :: thesis: verum

end;

suppose A12: i <> j ; :: thesis: A * (i,i) = A * (j,j)

A13: 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 A11, Th55
.= ((canMat (i,j,n,R)) * A) * (i,j) by A2, A12
.= A * (j,j) by A11, A13, Th54 ;
:: thesis: verum

end;

end;

end;

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

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

take z = 1. R; :: thesis: A = z * (1. (R,n))
thus A = z * (1. (R,n)) by A14, MATRIX_0:45; :: thesis: verum

end;

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

then 0 < 0 + n ;
then 1 <= n by NAT_1:19;
then A15: [1,1] in Indices A by MATRIX_0:31;
take z = A * (1,1); :: thesis: A = z * (1. (R,n))
A16: ( 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 A17: [i,j] in Indices A ; :: thesis: A * (i,j) = (z * (1. (R,n))) * (i,j)
Indices A = [:(Seg n),(Seg n):] by MATRIX_0:24
.= Indices (1. (R,n)) by MATRIX_0:24 ;
then A18: [i,j] in Indices (1. (R,n)) by A17;

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

suppose A19: 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 A15, MATRIX_0:24;
then A20: 1 in Seg n by ZFMISC_1:87;
[i,j] in [:(Seg n),(Seg n):] by A17, MATRIX_0:24;
then i in Seg n by ZFMISC_1:87;
then [1,i] in [:(Seg n),(Seg n):] by A20, ZFMISC_1:87;
hence [1,i] in Indices A by MATRIX_0:24; :: thesis: verum

end;

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

end;

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

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

end;

end;

end;

hence A = z * (1. (R,n)) by A16, MATRIX_0:21; :: thesis: verum

end;

end;